Metamath Proof Explorer

Theorem pjci

Description: Two subspaces commute iff their projections commute. Lemma 4 of Kalmbach p. 67. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjclem1.1 
|- G e. CH
pjclem1.2 
|- H e. CH
Assertion pjci 
|- ( G C_H H <-> ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) )

Proof

Step Hyp Ref Expression
1 pjclem1.1 
 |-  G e. CH
2 pjclem1.2 
 |-  H e. CH
3 1 2 pjclem2 
 |-  ( G C_H H -> ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) )
4 1 2 pjclem4 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) )
5 1 2 pjclem3 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( projh ` ( _|_ ` H ) ) ) = ( ( projh ` ( _|_ ` H ) ) o. ( projh ` G ) ) )
6 2 choccli 
 |-  ( _|_ ` H ) e. CH
7 1 6 pjclem4 
 |-  ( ( ( projh ` G ) o. ( projh ` ( _|_ ` H ) ) ) = ( ( projh ` ( _|_ ` H ) ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( projh ` ( _|_ ` H ) ) ) = ( projh ` ( G i^i ( _|_ ` H ) ) ) )
8 5 7 syl 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( projh ` ( _|_ ` H ) ) ) = ( projh ` ( G i^i ( _|_ ` H ) ) ) )
9 4 8 oveq12d 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) +op ( ( projh ` G ) o. ( projh ` ( _|_ ` H ) ) ) ) = ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) ) )
10 df-iop 
 |-  Iop = ( projh ` ~H )
11 10 coeq2i 
 |-  ( ( projh ` G ) o. Iop ) = ( ( projh ` G ) o. ( projh ` ~H ) )
12 1 pjfi 
 |-  ( projh ` G ) : ~H --> ~H
13 12 hoid1i 
 |-  ( ( projh ` G ) o. Iop ) = ( projh ` G )
14 11 13 eqtr3i 
 |-  ( ( projh ` G ) o. ( projh ` ~H ) ) = ( projh ` G )
15 2 pjtoi 
 |-  ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) = ( projh ` ~H )
16 15 coeq2i 
 |-  ( ( projh ` G ) o. ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) ) = ( ( projh ` G ) o. ( projh ` ~H ) )
17 2 pjfi 
 |-  ( projh ` H ) : ~H --> ~H
18 6 pjfi 
 |-  ( projh ` ( _|_ ` H ) ) : ~H --> ~H
19 1 17 18 pjsdii 
 |-  ( ( projh ` G ) o. ( ( projh ` H ) +op ( projh ` ( _|_ ` H ) ) ) ) = ( ( ( projh ` G ) o. ( projh ` H ) ) +op ( ( projh ` G ) o. ( projh ` ( _|_ ` H ) ) ) )
20 16 19 eqtr3i 
 |-  ( ( projh ` G ) o. ( projh ` ~H ) ) = ( ( ( projh ` G ) o. ( projh ` H ) ) +op ( ( projh ` G ) o. ( projh ` ( _|_ ` H ) ) ) )
21 14 20 eqtr3i 
 |-  ( projh ` G ) = ( ( ( projh ` G ) o. ( projh ` H ) ) +op ( ( projh ` G ) o. ( projh ` ( _|_ ` H ) ) ) )
22 inss2 
 |-  ( G i^i H ) C_ H
23 1 choccli 
 |-  ( _|_ ` G ) e. CH
24 2 23 chub2i 
 |-  H C_ ( ( _|_ ` G ) vH H )
25 22 24 sstri 
 |-  ( G i^i H ) C_ ( ( _|_ ` G ) vH H )
26 1 2 chdmm3i 
 |-  ( _|_ ` ( G i^i ( _|_ ` H ) ) ) = ( ( _|_ ` G ) vH H )
27 25 26 sseqtrri 
 |-  ( G i^i H ) C_ ( _|_ ` ( G i^i ( _|_ ` H ) ) )
28 1 2 chincli 
 |-  ( G i^i H ) e. CH
29 1 6 chincli 
 |-  ( G i^i ( _|_ ` H ) ) e. CH
30 28 29 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 ) ) ) ) )
31 27 30 ax-mp 
 |-  ( projh ` ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) ) = ( ( projh ` ( G i^i H ) ) +op ( projh ` ( G i^i ( _|_ ` H ) ) ) )
32 9 21 31 3eqtr4g 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( projh ` G ) = ( projh ` ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) ) )
33 28 29 chjcli 
 |-  ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) e. CH
34 1 33 pj11i 
 |-  ( ( projh ` G ) = ( projh ` ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) ) <-> G = ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) )
35 32 34 sylib 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> G = ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) )
36 1 2 cmbri 
 |-  ( G C_H H <-> G = ( ( G i^i H ) vH ( G i^i ( _|_ ` H ) ) ) )
37 35 36 sylibr 
 |-  ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> G C_H H )
38 3 37 impbii 
 |-  ( G C_H H <-> ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) )