Metamath Proof Explorer

Theorem pjclem1

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

Ref Expression
Hypotheses pjclem1.1 
|- G e. CH
pjclem1.2 
|- H e. CH
Assertion pjclem1 
|- ( G C_H H -> ( ( 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 cmbri 
 |-  ( G C_H H <-> G = ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) )
4 fveq2 
 |-  ( G = ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) -> ( projh ` G ) = ( projh ` ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) ) )
5 3 4 sylbi 
 |-  ( G C_H H -> ( projh ` G ) = ( projh ` ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) ) )
6 inss2 
 |-  ( G i^i H ) C_ H
7 1 choccli 
 |-  ( _|_ ` G ) e. CH
8 2 7 chub2i 
 |-  H C_ ( ( _|_ ` G ) vH H )
9 1 2 chdmm3i 
 |-  ( _|_ ` ( G i^i ( _|_ ` H ) ) ) = ( ( _|_ ` G ) vH H )
10 8 9 sseqtrri 
 |-  H C_ ( _|_ ` ( G i^i ( _|_ ` H ) ) )
11 6 10 sstri 
 |-  ( G i^i H ) C_ ( _|_ ` ( G i^i ( _|_ ` H ) ) )
12 1 2 chincli 
 |-  ( G i^i H ) e. CH
13 2 choccli 
 |-  ( _|_ ` H ) e. CH
14 1 13 chincli 
 |-  ( G i^i ( _|_ ` H ) ) e. CH
15 12 14 pjscji 
 |-  ( ( G i^i H ) C_ ( _|_ ` ( G i^i ( _|_ ` H ) ) ) -> ( projh ` ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) ) = ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) ) )
16 11 15 ax-mp 
 |-  ( projh ` ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) ) = ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) )
17 16 eqeq2i 
 |-  ( ( projh ` G ) = ( projh ` ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) ) <-> ( projh ` G ) = ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) ) )
18 coeq2 
 |-  ( ( projh ` G ) = ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) ) -> ( ( projh ` H ) o. ( projh ` G ) ) = ( ( projh ` H ) o. ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) ) ) )
19 12 pjfi 
 |-  ( projh ` ( G i^i H ) ) : ~H --> ~H
20 14 pjfi 
 |-  ( projh ` ( G i^i ( _|_ ` H ) ) ) : ~H --> ~H
21 2 19 20 pjsdii 
 |-  ( ( projh ` H ) o. ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) ) ) = ( ( ( projh ` H ) o. ( projh ` ( G i^i H ) ) ) +op ( ( projh ` H ) o. ( projh ` ( G i^i ( _|_ ` H ) ) ) ) )
22 12 2 pjss1coi 
 |-  ( ( G i^i H ) C_ H <-> ( ( projh ` H ) o. ( projh ` ( G i^i H ) ) ) = ( projh ` ( G i^i H ) ) )
23 6 22 mpbi 
 |-  ( ( projh ` H ) o. ( projh ` ( G i^i H ) ) ) = ( projh ` ( G i^i H ) )
24 2 14 pjorthcoi 
 |-  ( H C_ ( _|_ ` ( G i^i ( _|_ ` H ) ) ) -> ( ( projh ` H ) o. ( projh ` ( G i^i ( _|_ ` H ) ) ) ) = 0hop )
25 10 24 ax-mp 
 |-  ( ( projh ` H ) o. ( projh ` ( G i^i ( _|_ ` H ) ) ) ) = 0hop
26 23 25 oveq12i 
 |-  ( ( ( projh ` H ) o. ( projh ` ( G i^i H ) ) ) +op ( ( projh ` H ) o. ( projh ` ( G i^i ( _|_ ` H ) ) ) ) ) = ( ( projh ` ( G i^i H ) ) +op 0hop )
27 19 hoaddridi 
 |-  ( ( projh ` ( G i^i H ) ) +op 0hop ) = ( projh ` ( G i^i H ) )
28 21 26 27 3eqtri 
 |-  ( ( projh ` H ) o. ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) ) ) = ( projh ` ( G i^i H ) )
29 28 eqeq2i 
 |-  ( ( ( projh ` H ) o. ( projh ` G ) ) = ( ( projh ` H ) o. ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) ) ) <-> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` ( G i^i H ) ) )
30 coeq2 
 |-  ( ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` ( G i^i H ) ) -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` G ) ) ) = ( ( projh ` G ) o. ( projh ` ( G i^i H ) ) ) )
31 inss1 
 |-  ( G i^i H ) C_ G
32 12 1 pjss1coi 
 |-  ( ( G i^i H ) C_ G <-> ( ( projh ` G ) o. ( projh ` ( G i^i H ) ) ) = ( projh ` ( G i^i H ) ) )
33 31 32 mpbi 
 |-  ( ( projh ` G ) o. ( projh ` ( G i^i H ) ) ) = ( projh ` ( G i^i H ) )
34 30 33 eqtrdi 
 |-  ( ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` ( G i^i H ) ) -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` G ) ) ) = ( projh ` ( G i^i H ) ) )
35 29 34 sylbi 
 |-  ( ( ( projh ` H ) o. ( projh ` G ) ) = ( ( projh ` H ) o. ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) ) ) -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` G ) ) ) = ( projh ` ( G i^i H ) ) )
36 18 35 syl 
 |-  ( ( projh ` G ) = ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) ) -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` G ) ) ) = ( projh ` ( G i^i H ) ) )
37 17 36 sylbi 
 |-  ( ( projh ` G ) = ( projh ` ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) ) -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` G ) ) ) = ( projh ` ( G i^i H ) ) )
38 5 37 syl 
 |-  ( G C_H H -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` G ) ) ) = ( projh ` ( G i^i H ) ) )
39 1 2 cmcm3i 
 |-  ( G C_H H <-> ( _|_ ` G ) C_H H )
40 7 2 cmbri 
 |-  ( ( _|_ ` G ) C_H H <-> ( _|_ ` G ) = ( ( ( _|_ ` G ) i^i H ) vH ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) )
41 39 40 bitri 
 |-  ( G C_H H <-> ( _|_ ` G ) = ( ( ( _|_ ` G ) i^i H ) vH ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) )
42 fveq2 
 |-  ( ( _|_ ` G ) = ( ( ( _|_ ` G ) i^i H ) vH ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) -> ( projh ` ( _|_ ` G ) ) = ( projh ` ( ( ( _|_ ` G ) i^i H ) vH ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) )
43 inss2 
 |-  ( ( _|_ ` G ) i^i H ) C_ H
44 2 1 chub2i 
 |-  H C_ ( G vH H )
45 1 2 chdmm4i 
 |-  ( _|_ ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) = ( G vH H )
46 44 45 sseqtrri 
 |-  H C_ ( _|_ ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) )
47 43 46 sstri 
 |-  ( ( _|_ ` G ) i^i H ) C_ ( _|_ ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) )
48 7 2 chincli 
 |-  ( ( _|_ ` G ) i^i H ) e. CH
49 7 13 chincli 
 |-  ( ( _|_ ` G ) i^i ( _|_ ` H ) ) e. CH
50 48 49 pjscji 
 |-  ( ( ( _|_ ` G ) i^i H ) C_ ( _|_ ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) -> ( projh ` ( ( ( _|_ ` G ) i^i H ) vH ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) = ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) )
51 47 50 ax-mp 
 |-  ( projh ` ( ( ( _|_ ` G ) i^i H ) vH ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) = ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) )
52 51 eqeq2i 
 |-  ( ( projh ` ( _|_ ` G ) ) = ( projh ` ( ( ( _|_ ` G ) i^i H ) vH ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) <-> ( projh ` ( _|_ ` G ) ) = ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) )
53 coeq2 
 |-  ( ( projh ` ( _|_ ` G ) ) = ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) -> ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) = ( ( projh ` H ) o. ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) ) )
54 48 pjfi 
 |-  ( projh ` ( ( _|_ ` G ) i^i H ) ) : ~H --> ~H
55 49 pjfi 
 |-  ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) : ~H --> ~H
56 2 54 55 pjsdii 
 |-  ( ( projh ` H ) o. ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) ) = ( ( ( projh ` H ) o. ( projh ` ( ( _|_ ` G ) i^i H ) ) ) +op ( ( projh ` H ) o. ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) )
57 48 2 pjss1coi 
 |-  ( ( ( _|_ ` G ) i^i H ) C_ H <-> ( ( projh ` H ) o. ( projh ` ( ( _|_ ` G ) i^i H ) ) ) = ( projh ` ( ( _|_ ` G ) i^i H ) ) )
58 43 57 mpbi 
 |-  ( ( projh ` H ) o. ( projh ` ( ( _|_ ` G ) i^i H ) ) ) = ( projh ` ( ( _|_ ` G ) i^i H ) )
59 2 49 pjorthcoi 
 |-  ( H C_ ( _|_ ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) -> ( ( projh ` H ) o. ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) = 0hop )
60 46 59 ax-mp 
 |-  ( ( projh ` H ) o. ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) = 0hop
61 58 60 oveq12i 
 |-  ( ( ( projh ` H ) o. ( projh ` ( ( _|_ ` G ) i^i H ) ) ) +op ( ( projh ` H ) o. ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) ) = ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op 0hop )
62 54 hoaddridi 
 |-  ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op 0hop ) = ( projh ` ( ( _|_ ` G ) i^i H ) )
63 56 61 62 3eqtri 
 |-  ( ( projh ` H ) o. ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) ) = ( projh ` ( ( _|_ ` G ) i^i H ) )
64 63 eqeq2i 
 |-  ( ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) = ( ( projh ` H ) o. ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) ) <-> ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) = ( projh ` ( ( _|_ ` G ) i^i H ) ) )
65 coeq2 
 |-  ( ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) = ( projh ` ( ( _|_ ` G ) i^i H ) ) -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) = ( ( projh ` G ) o. ( projh ` ( ( _|_ ` G ) i^i H ) ) ) )
66 1 13 chub1i 
 |-  G C_ ( G vH ( _|_ ` H ) )
67 1 2 chdmm2i 
 |-  ( _|_ ` ( ( _|_ ` G ) i^i H ) ) = ( G vH ( _|_ ` H ) )
68 66 67 sseqtrri 
 |-  G C_ ( _|_ ` ( ( _|_ ` G ) i^i H ) )
69 1 48 pjorthcoi 
 |-  ( G C_ ( _|_ ` ( ( _|_ ` G ) i^i H ) ) -> ( ( projh ` G ) o. ( projh ` ( ( _|_ ` G ) i^i H ) ) ) = 0hop )
70 68 69 ax-mp 
 |-  ( ( projh ` G ) o. ( projh ` ( ( _|_ ` G ) i^i H ) ) ) = 0hop
71 65 70 eqtrdi 
 |-  ( ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) = ( projh ` ( ( _|_ ` G ) i^i H ) ) -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) = 0hop )
72 64 71 sylbi 
 |-  ( ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) = ( ( projh ` H ) o. ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) ) -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) = 0hop )
73 53 72 syl 
 |-  ( ( projh ` ( _|_ ` G ) ) = ( ( projh ` ( ( _|_ ` G ) i^i H ) ) +op ( projh ` ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) = 0hop )
74 52 73 sylbi 
 |-  ( ( projh ` ( _|_ ` G ) ) = ( projh ` ( ( ( _|_ ` G ) i^i H ) vH ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) ) -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) = 0hop )
75 42 74 syl 
 |-  ( ( _|_ ` G ) = ( ( ( _|_ ` G ) i^i H ) vH ( ( _|_ ` G ) i^i ( _|_ ` H ) ) ) -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) = 0hop )
76 41 75 sylbi 
 |-  ( G C_H H -> ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) = 0hop )
77 38 76 oveq12d 
 |-  ( G C_H H -> ( ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` G ) ) ) +op ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) ) = ( ( projh ` ( G i^i H ) ) +op 0hop ) )
78 df-iop 
 |-  Iop = ( projh ` ~H )
79 78 coeq2i 
 |-  ( ( projh ` H ) o. Iop ) = ( ( projh ` H ) o. ( projh ` ~H ) )
80 2 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
81 80 hoid1i 
 |-  ( ( projh ` H ) o. Iop ) = ( projh ` H )
82 79 81 eqtr3i 
 |-  ( ( projh ` H ) o. ( projh ` ~H ) ) = ( projh ` H )
83 1 pjtoi 
 |-  ( ( projh ` G ) +op ( projh ` ( _|_ ` G ) ) ) = ( projh ` ~H )
84 83 coeq2i 
 |-  ( ( projh ` H ) o. ( ( projh ` G ) +op ( projh ` ( _|_ ` G ) ) ) ) = ( ( projh ` H ) o. ( projh ` ~H ) )
85 1 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
86 7 pjfi 
 |-  ( projh ` ( _|_ ` G ) ) : ~H --> ~H
87 2 85 86 pjsdii 
 |-  ( ( projh ` H ) o. ( ( projh ` G ) +op ( projh ` ( _|_ ` G ) ) ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) +op ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) )
88 84 87 eqtr3i 
 |-  ( ( projh ` H ) o. ( projh ` ~H ) ) = ( ( ( projh ` H ) o. ( projh ` G ) ) +op ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) )
89 82 88 eqtr3i 
 |-  ( projh ` H ) = ( ( ( projh ` H ) o. ( projh ` G ) ) +op ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) )
90 89 coeq2i 
 |-  ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` G ) o. ( ( ( projh ` H ) o. ( projh ` G ) ) +op ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) )
91 80 85 hocofi 
 |-  ( ( projh ` H ) o. ( projh ` G ) ) : ~H --> ~H
92 80 86 hocofi 
 |-  ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) : ~H --> ~H
93 1 91 92 pjsdii 
 |-  ( ( projh ` G ) o. ( ( ( projh ` H ) o. ( projh ` G ) ) +op ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) ) = ( ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` G ) ) ) +op ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) )
94 90 93 eqtr2i 
 |-  ( ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` G ) ) ) +op ( ( projh ` G ) o. ( ( projh ` H ) o. ( projh ` ( _|_ ` G ) ) ) ) ) = ( ( projh ` G ) o. ( projh ` H ) )
95 77 94 27 3eqtr3g 
 |-  ( G C_H H -> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) )