Metamath Proof Explorer

Theorem pjclem4

Description: Lemma for projection commutation theorem. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjclem1.1 
|- G e. CH
pjclem1.2 
|- H e. CH
Assertion pjclem4 
|- ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) )

Proof

Step Hyp Ref Expression
1 pjclem1.1 
 |-  G e. CH
2 pjclem1.2 
 |-  H e. CH
3 1 2 pjcocli 
 |-  ( x e. ~H -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. G )
4 3 adantl 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ x e. ~H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. G )
5 2 1 pjcocli 
 |-  ( x e. ~H -> ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) e. H )
6 fveq1 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) )
7 6 eleq1d 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. H <-> ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) e. H ) )
8 5 7 imbitrrid 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( x e. ~H -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. H ) )
9 8 imp 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ x e. ~H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. H )
10 4 9 elind 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ x e. ~H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ( G i^i H ) )
11 1 2 pjcohcli 
 |-  ( x e. ~H -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H )
12 hvsubcl 
 |-  ( ( x e. ~H /\ ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H ) -> ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) e. ~H )
13 11 12 mpdan 
 |-  ( x e. ~H -> ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) e. ~H )
14 13 adantl 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ x e. ~H ) -> ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) e. ~H )
15 simpl 
 |-  ( ( x e. ~H /\ y e. ( G i^i H ) ) -> x e. ~H )
16 11 adantr 
 |-  ( ( x e. ~H /\ y e. ( G i^i H ) ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H )
17 1 2 chincli 
 |-  ( G i^i H ) e. CH
18 17 cheli 
 |-  ( y e. ( G i^i H ) -> y e. ~H )
19 18 adantl 
 |-  ( ( x e. ~H /\ y e. ( G i^i H ) ) -> y e. ~H )
20 15 16 19 3jca 
 |-  ( ( x e. ~H /\ y e. ( G i^i H ) ) -> ( x e. ~H /\ ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) )
21 20 adantl 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ ( x e. ~H /\ y e. ( G i^i H ) ) ) -> ( x e. ~H /\ ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) )
22 his2sub 
 |-  ( ( x e. ~H /\ ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) -> ( ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) .ih y ) = ( ( x .ih y ) - ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) .ih y ) ) )
23 21 22 syl 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ ( x e. ~H /\ y e. ( G i^i H ) ) ) -> ( ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) .ih y ) = ( ( x .ih y ) - ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) .ih y ) ) )
24 6 oveq1d 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) .ih y ) = ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) .ih y ) )
25 2 1 pjadjcoi 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) .ih y ) = ( x .ih ( ( ( projh ` G ) o. ( projh ` H ) ) ` y ) ) )
26 18 25 sylan2 
 |-  ( ( x e. ~H /\ y e. ( G i^i H ) ) -> ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) .ih y ) = ( x .ih ( ( ( projh ` G ) o. ( projh ` H ) ) ` y ) ) )
27 1 2 pjclem4a 
 |-  ( y e. ( G i^i H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` y ) = y )
28 27 oveq2d 
 |-  ( y e. ( G i^i H ) -> ( x .ih ( ( ( projh ` G ) o. ( projh ` H ) ) ` y ) ) = ( x .ih y ) )
29 28 adantl 
 |-  ( ( x e. ~H /\ y e. ( G i^i H ) ) -> ( x .ih ( ( ( projh ` G ) o. ( projh ` H ) ) ` y ) ) = ( x .ih y ) )
30 26 29 eqtrd 
 |-  ( ( x e. ~H /\ y e. ( G i^i H ) ) -> ( ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) .ih y ) = ( x .ih y ) )
31 24 30 sylan9eq 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ ( x e. ~H /\ y e. ( G i^i H ) ) ) -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) .ih y ) = ( x .ih y ) )
32 31 oveq1d 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ ( x e. ~H /\ y e. ( G i^i H ) ) ) -> ( ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) .ih y ) - ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) .ih y ) ) = ( ( x .ih y ) - ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) .ih y ) ) )
33 11 18 anim12i 
 |-  ( ( x e. ~H /\ y e. ( G i^i H ) ) -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) )
34 33 adantl 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ ( x e. ~H /\ y e. ( G i^i H ) ) ) -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) )
35 hicl 
 |-  ( ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H /\ y e. ~H ) -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) .ih y ) e. CC )
36 34 35 syl 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ ( x e. ~H /\ y e. ( G i^i H ) ) ) -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) .ih y ) e. CC )
37 36 subidd 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ ( x e. ~H /\ y e. ( G i^i H ) ) ) -> ( ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) .ih y ) - ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) .ih y ) ) = 0 )
38 23 32 37 3eqtr2d 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ ( x e. ~H /\ y e. ( G i^i H ) ) ) -> ( ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) .ih y ) = 0 )
39 38 expr 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ x e. ~H ) -> ( y e. ( G i^i H ) -> ( ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) .ih y ) = 0 ) )
40 39 ralrimiv 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ x e. ~H ) -> A. y e. ( G i^i H ) ( ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) .ih y ) = 0 )
41 17 chshii 
 |-  ( G i^i H ) e. SH
42 shocel 
 |-  ( ( G i^i H ) e. SH -> ( ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) e. ( _|_ ` ( G i^i H ) ) <-> ( ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) e. ~H /\ A. y e. ( G i^i H ) ( ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) .ih y ) = 0 ) ) )
43 41 42 ax-mp 
 |-  ( ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) e. ( _|_ ` ( G i^i H ) ) <-> ( ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) e. ~H /\ A. y e. ( G i^i H ) ( ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) .ih y ) = 0 ) )
44 14 40 43 sylanbrc 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ x e. ~H ) -> ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) e. ( _|_ ` ( G i^i H ) ) )
45 17 pjvi 
 |-  ( ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ( G i^i H ) /\ ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) e. ( _|_ ` ( G i^i H ) ) ) -> ( ( projh ` ( G i^i H ) ) ` ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) ) ) = ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) )
46 10 44 45 syl2anc 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ x e. ~H ) -> ( ( projh ` ( G i^i H ) ) ` ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) ) ) = ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) )
47 id 
 |-  ( x e. ~H -> x e. ~H )
48 hvaddsub12 
 |-  ( ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H /\ x e. ~H /\ ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H ) -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) ) = ( x +h ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) ) )
49 11 47 11 48 syl3anc 
 |-  ( x e. ~H -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) ) = ( x +h ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) ) )
50 hvsubid 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) e. ~H -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) = 0h )
51 11 50 syl 
 |-  ( x e. ~H -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) = 0h )
52 51 oveq2d 
 |-  ( x e. ~H -> ( x +h ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) ) = ( x +h 0h ) )
53 ax-hvaddid 
 |-  ( x e. ~H -> ( x +h 0h ) = x )
54 49 52 53 3eqtrd 
 |-  ( x e. ~H -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) ) = x )
55 54 fveq2d 
 |-  ( x e. ~H -> ( ( projh ` ( G i^i H ) ) ` ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) ) ) = ( ( projh ` ( G i^i H ) ) ` x ) )
56 55 adantl 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ x e. ~H ) -> ( ( projh ` ( G i^i H ) ) ` ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) +h ( x -h ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) ) ) ) = ( ( projh ` ( G i^i H ) ) ` x ) )
57 46 56 eqtr3d 
 |-  ( ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) /\ x e. ~H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( ( projh ` ( G i^i H ) ) ` x ) )
58 57 ralrimiva 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> A. x e. ~H ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( ( projh ` ( G i^i H ) ) ` x ) )
59 1 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
60 2 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
61 59 60 hocofi 
 |-  ( ( projh ` G ) o. ( projh ` H ) ) : ~H --> ~H
62 17 pjfi 
 |-  ( projh ` ( G i^i H ) ) : ~H --> ~H
63 61 62 hoeqi 
 |-  ( A. x e. ~H ( ( ( projh ` G ) o. ( projh ` H ) ) ` x ) = ( ( projh ` ( G i^i H ) ) ` x ) <-> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) )
64 58 63 sylib 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) )