Theorem pjnormss 10007

Description: Theorem 4.5(i)<->(vi) of [Beran] p. 112.

Hypotheses

Ref	Expression
pjco.1	|- G e. CH
pjco.2	|- H e. CH

Assertion

Ref	Expression
pjnormss	|- (G (_ H <-> A.x e. H~ (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x)))

Distinct variable groups:   x,H   x,G

Proof of Theorem pjnormss

Step	Hyp	Ref	Expression
1		pjco.2	. . . . . . 7 |- H e. CH
2		pjco.1	. . . . . . 7 |- G e. CH
3	1, 2	pjssmt 10004	. . . . . 6 |- (x e. H~ -> (G (_ H -> (((proj` H)` x) -h ((proj` G)` x)) = ((proj` (H i^i (_|_` G)))` x)))
4	1, 2	pjssge0t 10005	. . . . . 6 |- (x e. H~ -> ((((proj` H)` x) -h ((proj` G)` x)) = ((proj` (H i^i (_|_` G)))` x) -> 0 <_ ((((proj` H)` x) -h ((proj` G)` x)) .ih x)))
5	3, 4	syld 27	. . . . 5 |- (x e. H~ -> (G (_ H -> 0 <_ ((((proj` H)` x) -h ((proj` G)` x)) .ih x)))
6	1, 2	pjdifnormt 10006	. . . . 5 |- (x e. H~ -> (0 <_ ((((proj` H)` x) -h ((proj` G)` x)) .ih x) <-> (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))))
7	5, 6	sylibd 202	. . . 4 |- (x e. H~ -> (G (_ H -> (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))))
8	7	com12 11	. . 3 |- (G (_ H -> (x e. H~ -> (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))))
9	8	r19.21aiv 1705	. 2 |- (G (_ H -> A.x e. H~ (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x)))
10	2	pjhcl 9167	. . . . . . . . . . . . . . . . . 18 |- (x e. H~ -> ((proj` G)` x) e. H~)
11		normclt 8912	. . . . . . . . . . . . . . . . . 18 |- (((proj` G)` x) e. H~ -> (normh` ((proj` G)` x)) e. RR)
12	10, 11	syl 10	. . . . . . . . . . . . . . . . 17 |- (x e. H~ -> (normh` ((proj` G)` x)) e. RR)
13		0re 5412	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
14	12, 13	jctir 293	. . . . . . . . . . . . . . . 16 |- (x e. H~ -> ((normh` ((proj` G)` x)) e. RR /\ 0 e. RR))
15		letri3t 5490	. . . . . . . . . . . . . . . . 17 |- (((normh` ((proj` G)` x)) e. RR /\ 0 e. RR) -> ((normh` ((proj` G)` x)) = 0 <-> ((normh` ((proj` G)` x)) <_ 0 /\ 0 <_ (normh` ((proj` G)` x)))))
16	15	biimprd 154	. . . . . . . . . . . . . . . 16 |- (((normh` ((proj` G)` x)) e. RR /\ 0 e. RR) -> (((normh` ((proj` G)` x)) <_ 0 /\ 0 <_ (normh` ((proj` G)` x))) -> (normh` ((proj` G)` x)) = 0))
17	14, 16	syl 10	. . . . . . . . . . . . . . 15 |- (x e. H~ -> (((normh` ((proj` G)` x)) <_ 0 /\ 0 <_ (normh` ((proj` G)` x))) -> (normh` ((proj` G)` x)) = 0))
18		normge0t 8913	. . . . . . . . . . . . . . . 16 |- (((proj` G)` x) e. H~ -> 0 <_ (normh` ((proj` G)` x)))
19	10, 18	syl 10	. . . . . . . . . . . . . . 15 |- (x e. H~ -> 0 <_ (normh` ((proj` G)` x)))
20	17, 19	sylan2i 465	. . . . . . . . . . . . . 14 |- (x e. H~ -> (((normh` ((proj` G)` x)) <_ 0 /\ x e. H~) -> (normh` ((proj` G)` x)) = 0))
21	20	anabsi6 495	. . . . . . . . . . . . 13 |- ((x e. H~ /\ (normh` ((proj` G)` x)) <_ 0) -> (normh` ((proj` G)` x)) = 0)
22		breq2 2613	. . . . . . . . . . . . . 14 |- ((normh` ((proj` H)` x)) = 0 -> ((normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x)) <-> (normh` ((proj` G)` x)) <_ 0))
23	22	biimpac 418	. . . . . . . . . . . . 13 |- (((normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x)) /\ (normh` ((proj` H)` x)) = 0) -> (normh` ((proj` G)` x)) <_ 0)
24	21, 23	sylan2 451	. . . . . . . . . . . 12 |- ((x e. H~ /\ ((normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x)) /\ (normh` ((proj` H)` x)) = 0)) -> (normh` ((proj` G)` x)) = 0)
25	24	exp32 377	. . . . . . . . . . 11 |- (x e. H~ -> ((normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x)) -> ((normh` ((proj` H)` x)) = 0 -> (normh` ((proj` G)` x)) = 0)))
26	25	imp 350	. . . . . . . . . 10 |- ((x e. H~ /\ (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))) -> ((normh` ((proj` H)` x)) = 0 -> (normh` ((proj` G)` x)) = 0))
27	1	pjhcl 9167	. . . . . . . . . . . . 13 |- (x e. H~ -> ((proj` H)` x) e. H~)
28		norm-it 8917	. . . . . . . . . . . . 13 |- (((proj` H)` x) e. H~ -> ((normh` ((proj` H)` x)) = 0 <-> ((proj` H)` x) = 0h))
29	27, 28	syl 10	. . . . . . . . . . . 12 |- (x e. H~ -> ((normh` ((proj` H)` x)) = 0 <-> ((proj` H)` x) = 0h))
30		pjoc2t 9187	. . . . . . . . . . . . 13 |- ((H e. CH /\ x e. H~) -> (x e. (_|_` H) <-> ((proj` H)` x) = 0h))
31	1, 30	mpan 693	. . . . . . . . . . . 12 |- (x e. H~ -> (x e. (_|_` H) <-> ((proj` H)` x) = 0h))
32	29, 31	bitr4d 529	. . . . . . . . . . 11 |- (x e. H~ -> ((normh` ((proj` H)` x)) = 0 <-> x e. (_|_` H)))
33	32	adantr 389	. . . . . . . . . 10 |- ((x e. H~ /\ (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))) -> ((normh` ((proj` H)` x)) = 0 <-> x e. (_|_` H)))
34		norm-it 8917	. . . . . . . . . . . . 13 |- (((proj` G)` x) e. H~ -> ((normh` ((proj` G)` x)) = 0 <-> ((proj` G)` x) = 0h))
35	10, 34	syl 10	. . . . . . . . . . . 12 |- (x e. H~ -> ((normh` ((proj` G)` x)) = 0 <-> ((proj` G)` x) = 0h))
36		pjoc2t 9187	. . . . . . . . . . . . 13 |- ((G e. CH /\ x e. H~) -> (x e. (_|_` G) <-> ((proj` G)` x) = 0h))
37	2, 36	mpan 693	. . . . . . . . . . . 12 |- (x e. H~ -> (x e. (_|_` G) <-> ((proj` G)` x) = 0h))
38	35, 37	bitr4d 529	. . . . . . . . . . 11 |- (x e. H~ -> ((normh` ((proj` G)` x)) = 0 <-> x e. (_|_` G)))
39	38	adantr 389	. . . . . . . . . 10 |- ((x e. H~ /\ (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))) -> ((normh` ((proj` G)` x)) = 0 <-> x e. (_|_` G)))
40	26, 33, 39	3imtr3d 540	. . . . . . . . 9 |- ((x e. H~ /\ (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))) -> (x e. (_|_` H) -> x e. (_|_` G)))
41	40	ex 373	. . . . . . . 8 |- (x e. H~ -> ((normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x)) -> (x e. (_|_` H) -> x e. (_|_` G))))
42	41	a2i 9	. . . . . . 7 |- ((x e. H~ -> (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))) -> (x e. H~ -> (x e. (_|_` H) -> x e. (_|_` G))))
43	1	choccl 9101	. . . . . . . 8 |- (_|_` H) e. CH
44	43	chel 9023	. . . . . . 7 |- (x e. (_|_` H) -> x e. H~)
45	42, 44	syl5 21	. . . . . 6 |- ((x e. H~ -> (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))) -> (x e. (_|_` H) -> (x e. (_|_` H) -> x e. (_|_` G))))
46	45	pm2.43d 65	. . . . 5 |- ((x e. H~ -> (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))) -> (x e. (_|_` H) -> x e. (_|_` G)))
47	46	19.20i 989	. . . 4 |- (A.x(x e. H~ -> (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))) -> A.x(x e. (_|_` H) -> x e. (_|_` G)))
48		df-ral 1641	. . . 4 |- (A.x e. H~ (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x)) <-> A.x(x e. H~ -> (normh` ((proj` G)` x)) <_ (normh` ((proj` H)` x))))
49		dfss2 2048	. . . 4 |- ((_|_` H) (_ (_|_` G) <->