Metamath Proof Explorer

Theorem pjnormssi

Description: Theorem 4.5(i)<->(vi) of Beran p. 112. (Contributed by NM, 26-Sep-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 
|- G e. CH
pjco.2 
|- H e. CH
Assertion pjnormssi 
|- ( G C_ H <-> A. x e. ~H ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) )

Proof

Step Hyp Ref Expression
1 pjco.1 
 |-  G e. CH
2 pjco.2 
 |-  H e. CH
3 2 1 pjssmi 
 |-  ( x e. ~H -> ( G C_ H -> ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) = ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) ) )
4 2 1 pjssge0i 
 |-  ( x e. ~H -> ( ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) = ( ( projh ` ( H i^i ( _|_ ` G ) ) ) ` x ) -> 0 <_ ( ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) .ih x ) ) )
5 3 4 syld 
 |-  ( x e. ~H -> ( G C_ H -> 0 <_ ( ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) .ih x ) ) )
6 2 1 pjdifnormi 
 |-  ( x e. ~H -> ( 0 <_ ( ( ( ( projh ` H ) ` x ) -h ( ( projh ` G ) ` x ) ) .ih x ) <-> ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) )
7 5 6 sylibd 
 |-  ( x e. ~H -> ( G C_ H -> ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) )
8 7 com12 
 |-  ( G C_ H -> ( x e. ~H -> ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) )
9 8 ralrimiv 
 |-  ( G C_ H -> A. x e. ~H ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) )
10 2 choccli 
 |-  ( _|_ ` H ) e. CH
11 10 cheli 
 |-  ( x e. ( _|_ ` H ) -> x e. ~H )
12 breq2 
 |-  ( ( normh ` ( ( projh ` H ) ` x ) ) = 0 -> ( ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) <-> ( normh ` ( ( projh ` G ) ` x ) ) <_ 0 ) )
13 12 biimpac 
 |-  ( ( ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) /\ ( normh ` ( ( projh ` H ) ` x ) ) = 0 ) -> ( normh ` ( ( projh ` G ) ` x ) ) <_ 0 )
14 1 pjhcli 
 |-  ( x e. ~H -> ( ( projh ` G ) ` x ) e. ~H )
15 normge0 
 |-  ( ( ( projh ` G ) ` x ) e. ~H -> 0 <_ ( normh ` ( ( projh ` G ) ` x ) ) )
16 14 15 syl 
 |-  ( x e. ~H -> 0 <_ ( normh ` ( ( projh ` G ) ` x ) ) )
17 normcl 
 |-  ( ( ( projh ` G ) ` x ) e. ~H -> ( normh ` ( ( projh ` G ) ` x ) ) e. RR )
18 14 17 syl 
 |-  ( x e. ~H -> ( normh ` ( ( projh ` G ) ` x ) ) e. RR )
19 0re 
 |-  0 e. RR
20 letri3 
 |-  ( ( ( normh ` ( ( projh ` G ) ` x ) ) e. RR /\ 0 e. RR ) -> ( ( normh ` ( ( projh ` G ) ` x ) ) = 0 <-> ( ( normh ` ( ( projh ` G ) ` x ) ) <_ 0 /\ 0 <_ ( normh ` ( ( projh ` G ) ` x ) ) ) ) )
21 20 biimprd 
 |-  ( ( ( normh ` ( ( projh ` G ) ` x ) ) e. RR /\ 0 e. RR ) -> ( ( ( normh ` ( ( projh ` G ) ` x ) ) <_ 0 /\ 0 <_ ( normh ` ( ( projh ` G ) ` x ) ) ) -> ( normh ` ( ( projh ` G ) ` x ) ) = 0 ) )
22 18 19 21 sylancl 
 |-  ( x e. ~H -> ( ( ( normh ` ( ( projh ` G ) ` x ) ) <_ 0 /\ 0 <_ ( normh ` ( ( projh ` G ) ` x ) ) ) -> ( normh ` ( ( projh ` G ) ` x ) ) = 0 ) )
23 16 22 sylan2i 
 |-  ( x e. ~H -> ( ( ( normh ` ( ( projh ` G ) ` x ) ) <_ 0 /\ x e. ~H ) -> ( normh ` ( ( projh ` G ) ` x ) ) = 0 ) )
24 23 anabsi6 
 |-  ( ( x e. ~H /\ ( normh ` ( ( projh ` G ) ` x ) ) <_ 0 ) -> ( normh ` ( ( projh ` G ) ` x ) ) = 0 )
25 13 24 sylan2 
 |-  ( ( x e. ~H /\ ( ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) /\ ( normh ` ( ( projh ` H ) ` x ) ) = 0 ) ) -> ( normh ` ( ( projh ` G ) ` x ) ) = 0 )
26 25 expr 
 |-  ( ( x e. ~H /\ ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) -> ( ( normh ` ( ( projh ` H ) ` x ) ) = 0 -> ( normh ` ( ( projh ` G ) ` x ) ) = 0 ) )
27 2 pjhcli 
 |-  ( x e. ~H -> ( ( projh ` H ) ` x ) e. ~H )
28 norm-i 
 |-  ( ( ( projh ` H ) ` x ) e. ~H -> ( ( normh ` ( ( projh ` H ) ` x ) ) = 0 <-> ( ( projh ` H ) ` x ) = 0h ) )
29 27 28 syl 
 |-  ( x e. ~H -> ( ( normh ` ( ( projh ` H ) ` x ) ) = 0 <-> ( ( projh ` H ) ` x ) = 0h ) )
30 pjoc2 
 |-  ( ( H e. CH /\ x e. ~H ) -> ( x e. ( _|_ ` H ) <-> ( ( projh ` H ) ` x ) = 0h ) )
31 2 30 mpan 
 |-  ( x e. ~H -> ( x e. ( _|_ ` H ) <-> ( ( projh ` H ) ` x ) = 0h ) )
32 29 31 bitr4d 
 |-  ( x e. ~H -> ( ( normh ` ( ( projh ` H ) ` x ) ) = 0 <-> x e. ( _|_ ` H ) ) )
33 32 adantr 
 |-  ( ( x e. ~H /\ ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) -> ( ( normh ` ( ( projh ` H ) ` x ) ) = 0 <-> x e. ( _|_ ` H ) ) )
34 norm-i 
 |-  ( ( ( projh ` G ) ` x ) e. ~H -> ( ( normh ` ( ( projh ` G ) ` x ) ) = 0 <-> ( ( projh ` G ) ` x ) = 0h ) )
35 14 34 syl 
 |-  ( x e. ~H -> ( ( normh ` ( ( projh ` G ) ` x ) ) = 0 <-> ( ( projh ` G ) ` x ) = 0h ) )
36 pjoc2 
 |-  ( ( G e. CH /\ x e. ~H ) -> ( x e. ( _|_ ` G ) <-> ( ( projh ` G ) ` x ) = 0h ) )
37 1 36 mpan 
 |-  ( x e. ~H -> ( x e. ( _|_ ` G ) <-> ( ( projh ` G ) ` x ) = 0h ) )
38 35 37 bitr4d 
 |-  ( x e. ~H -> ( ( normh ` ( ( projh ` G ) ` x ) ) = 0 <-> x e. ( _|_ ` G ) ) )
39 38 adantr 
 |-  ( ( x e. ~H /\ ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) -> ( ( normh ` ( ( projh ` G ) ` x ) ) = 0 <-> x e. ( _|_ ` G ) ) )
40 26 33 39 3imtr3d 
 |-  ( ( x e. ~H /\ ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) -> ( x e. ( _|_ ` H ) -> x e. ( _|_ ` G ) ) )
41 40 ex 
 |-  ( x e. ~H -> ( ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) -> ( x e. ( _|_ ` H ) -> x e. ( _|_ ` G ) ) ) )
42 41 a2i 
 |-  ( ( x e. ~H -> ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) -> ( x e. ~H -> ( x e. ( _|_ ` H ) -> x e. ( _|_ ` G ) ) ) )
43 11 42 syl5 
 |-  ( ( x e. ~H -> ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) -> ( x e. ( _|_ ` H ) -> ( x e. ( _|_ ` H ) -> x e. ( _|_ ` G ) ) ) )
44 43 pm2.43d 
 |-  ( ( x e. ~H -> ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) -> ( x e. ( _|_ ` H ) -> x e. ( _|_ ` G ) ) )
45 44 alimi 
 |-  ( A. x ( x e. ~H -> ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) -> A. x ( x e. ( _|_ ` H ) -> x e. ( _|_ ` G ) ) )
46 df-ral 
 |-  ( A. x e. ~H ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) <-> A. x ( x e. ~H -> ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) ) )
47 dfss2 
 |-  ( ( _|_ ` H ) C_ ( _|_ ` G ) <-> A. x ( x e. ( _|_ ` H ) -> x e. ( _|_ ` G ) ) )
48 45 46 47 3imtr4i 
 |-  ( A. x e. ~H ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) -> ( _|_ ` H ) C_ ( _|_ ` G ) )
49 1 2 chsscon3i 
 |-  ( G C_ H <-> ( _|_ ` H ) C_ ( _|_ ` G ) )
50 48 49 sylibr 
 |-  ( A. x e. ~H ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) -> G C_ H )
51 9 50 impbii 
 |-  ( G C_ H <-> A. x e. ~H ( normh ` ( ( projh ` G ) ` x ) ) <_ ( normh ` ( ( projh ` H ) ` x ) ) )