Theorem pjnormss 5638

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~ (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x)))

Distinct variable group(s):   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 5635	. . . . . 6 |- (x e. H~ -> (G (_ H -> (((Proj` H)` x) -v ((Proj` G)` x)) = ((Proj` (H i^i (_|_` G)))` x)))
4	1, 2	pjssge0t 5636	. . . . . 6 |- (x e. H~ -> ((((Proj` H)` x) -v ((Proj` G)` x)) = ((Proj` (H i^i (_|_` G)))` x) -> 0 <_ ((((Proj` H)` x) -v ((Proj` G)` x)) .i x)))
5	3, 4	syld 27	. . . . 5 |- (x e. H~ -> (G (_ H -> 0 <_ ((((Proj` H)` x) -v ((Proj` G)` x)) .i x)))
6	1, 2	pjdifnormt 5637	. . . . 5 |- (x e. H~ -> (0 <_ ((((Proj` H)` x) -v ((Proj` G)` x)) .i x) <-> (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))))
7	5, 6	sylibd 177	. . . 4 |- (x e. H~ -> (G (_ H -> (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))))
8	7	com12 13	. . 3 |- (G (_ H -> (x e. H~ -> (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))))
9	8	r19.21aiv 1259	. 2 |- (G (_ H -> A.x e. H~ (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x)))
10	2	pjhcl 5256	. . . . . . . . . . . . . . . . . 18 |- (x e. H~ -> ((Proj` G)` x) e. H~)
11		normclt 5076	. . . . . . . . . . . . . . . . . 18 |- (((Proj` G)` x) e. H~ -> (norm` ((Proj` G)` x)) e. RR)
12	10, 11	syl 12	. . . . . . . . . . . . . . . . 17 |- (x e. H~ -> (norm` ((Proj` G)` x)) e. RR)
13		ax0re 4063	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
14	12, 13	jctir 241	. . . . . . . . . . . . . . . 16 |- (x e. H~ -> ((norm` ((Proj` G)` x)) e. RR /\ 0 e. RR))
15		letri3t 4283	. . . . . . . . . . . . . . . . 17 |- (((norm` ((Proj` G)` x)) e. RR /\ 0 e. RR) -> ((norm` ((Proj` G)` x)) = 0 <-> ((norm` ((Proj` G)` x)) <_ 0 /\ 0 <_ (norm` ((Proj` G)` x)))))
16	15	biimprd 136	. . . . . . . . . . . . . . . 16 |- (((norm` ((Proj` G)` x)) e. RR /\ 0 e. RR) -> (((norm` ((Proj` G)` x)) <_ 0 /\ 0 <_ (norm` ((Proj` G)` x))) -> (norm` ((Proj` G)` x)) = 0))
17	14, 16	syl 12	. . . . . . . . . . . . . . 15 |- (x e. H~ -> (((norm` ((Proj` G)` x)) <_ 0 /\ 0 <_ (norm` ((Proj` G)` x))) -> (norm` ((Proj` G)` x)) = 0))
18		normge0t 5077	. . . . . . . . . . . . . . . 16 |- (((Proj` G)` x) e. H~ -> 0 <_ (norm` ((Proj` G)` x)))
19	10, 18	syl 12	. . . . . . . . . . . . . . 15 |- (x e. H~ -> 0 <_ (norm` ((Proj` G)` x)))
20	17, 19	sylan2i 357	. . . . . . . . . . . . . 14 |- (x e. H~ -> (((norm` ((Proj` G)` x)) <_ 0 /\ x e. H~) -> (norm` ((Proj` G)` x)) = 0))
21	20	anabsi6 378	. . . . . . . . . . . . 13 |- ((x e. H~ /\ (norm` ((Proj` G)` x)) <_ 0) -> (norm` ((Proj` G)` x)) = 0)
22		breq2 2066	. . . . . . . . . . . . . 14 |- ((norm` ((Proj` H)` x)) = 0 -> ((norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x)) <-> (norm` ((Proj` G)` x)) <_ 0))
23	22	biimpac 326	. . . . . . . . . . . . 13 |- (((norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x)) /\ (norm` ((Proj` H)` x)) = 0) -> (norm` ((Proj` G)` x)) <_ 0)
24	21, 23	sylan2 346	. . . . . . . . . . . 12 |- ((x e. H~ /\ ((norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x)) /\ (norm` ((Proj` H)` x)) = 0)) -> (norm` ((Proj` G)` x)) = 0)
25	24	exp32 294	. . . . . . . . . . 11 |- (x e. H~ -> ((norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x)) -> ((norm` ((Proj` H)` x)) = 0 -> (norm` ((Proj` G)` x)) = 0)))
26	25	imp 277	. . . . . . . . . 10 |- ((x e. H~ /\ (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))) -> ((norm` ((Proj` H)` x)) = 0 -> (norm` ((Proj` G)` x)) = 0))
27	1	pjhcl 5256	. . . . . . . . . . . . 13 |- (x e. H~ -> ((Proj` H)` x) e. H~)
28		norm-it 5080	. . . . . . . . . . . . 13 |- (((Proj` H)` x) e. H~ -> ((norm` ((Proj` H)` x)) = 0 <-> ((Proj` H)` x) = 0v))
29	27, 28	syl 12	. . . . . . . . . . . 12 |- (x e. H~ -> ((norm` ((Proj` H)` x)) = 0 <-> ((Proj` H)` x) = 0v))
30	1	pjoc2t 5274	. . . . . . . . . . . 12 |- (x e. H~ -> (x e. (_|_` H) <-> ((Proj` H)` x) = 0v))
31	29, 30	bitr4d 409	. . . . . . . . . . 11 |- (x e. H~ -> ((norm` ((Proj` H)` x)) = 0 <-> x e. (_|_` H)))
32	31	adantr 306	. . . . . . . . . 10 |- ((x e. H~ /\ (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))) -> ((norm` ((Proj` H)` x)) = 0 <-> x e. (_|_` H)))
33		norm-it 5080	. . . . . . . . . . . . 13 |- (((Proj` G)` x) e. H~ -> ((norm` ((Proj` G)` x)) = 0 <-> ((Proj` G)` x) = 0v))
34	10, 33	syl 12	. . . . . . . . . . . 12 |- (x e. H~ -> ((norm` ((Proj` G)` x)) = 0 <-> ((Proj` G)` x) = 0v))
35	2	pjoc2t 5274	. . . . . . . . . . . 12 |- (x e. H~ -> (x e. (_|_` G) <-> ((Proj` G)` x) = 0v))
36	34, 35	bitr4d 409	. . . . . . . . . . 11 |- (x e. H~ -> ((norm` ((Proj` G)` x)) = 0 <-> x e. (_|_` G)))
37	36	adantr 306	. . . . . . . . . 10 |- ((x e. H~ /\ (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))) -> ((norm` ((Proj` G)` x)) = 0 <-> x e. (_|_` G)))
38	26, 32, 37	3imtr3d 420	. . . . . . . . 9 |- ((x e. H~ /\ (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))) -> (x e. (_|_` H) -> x e. (_|_` G)))
39	38	exp 291	. . . . . . . 8 |- (x e. H~ -> ((norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x)) -> (x e. (_|_` H) -> x e. (_|_` G))))
40	39	a2i 8	. . . . . . 7 |- ((x e. H~ -> (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))) -> (x e. H~ -> (x e. (_|_` H) -> x e. (_|_` G))))
41	1	chocl 5192	. . . . . . . 8 |- (_|_` H) e. CH
42	41	chel 5137	. . . . . . 7 |- (x e. (_|_` H) -> x e. H~)
43	40, 42	syl5 22	. . . . . 6 |- ((x e. H~ -> (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))) -> (x e. (_|_` H) -> (x e. (_|_` H) -> x e. (_|_` G))))
44	43	pm2.43d 59	. . . . 5 |- ((x e. H~ -> (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))) -> (x e. (_|_` H) -> x e. (_|_` G)))
45	44	19.20i 691	. . . 4 |- (A.x(x e. H~ -> (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))) -> A.x(x e. (_|_` H) -> x e. (_|_` G)))
46		df-ral 1205	. . . 4 |- (A.x e. H~ (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x)) <-> A.x(x e. H~ -> (norm` ((Proj` G)` x)) <_ (norm` ((Proj` H)` x))))
47		dfss2 1497	. . . 4 |- ((_|_` H) (_ (_|_` G) <-> A.x(x e. (_|_` H) -> x e. (_|_` G)))
48	45, 46, 47	3imtr4 192	. . 3 |- (A.x e.