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 ⊢ 𝐺 ∈ Cℋ
pjclem1.2 ⊢ 𝐻 ∈ Cℋ
Assertion pjci ( 𝐺 𝐶ℋ 𝐻 ↔ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 pjclem1.1 ⊢ 𝐺 ∈ Cℋ
2 pjclem1.2 ⊢ 𝐻 ∈ Cℋ
3 1 2 pjclem2 ⊢ ( 𝐺 𝐶ℋ 𝐻 → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) )
4 1 2 pjclem4 ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) )
5 1 2 pjclem3 ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ∘ ( projℎ ‘ 𝐺 ) ) )
6 2 choccli ⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
7 1 6 pjclem4 ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) )
8 5 7 syl ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) )
9 4 8 oveq12d ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) +op ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) ) = ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) +op ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ) )
10 df-iop ⊢ Iop = ( projℎ ‘ ℋ )
11 10 coeq2i ⊢ ( ( projℎ ‘ 𝐺 ) ∘ Iop ) = ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ℋ ) )
12 1 pjfi ⊢ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ
13 12 hoid1i ⊢ ( ( projℎ ‘ 𝐺 ) ∘ Iop ) = ( projℎ ‘ 𝐺 )
14 11 13 eqtr3i ⊢ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ℋ ) ) = ( projℎ ‘ 𝐺 )
15 2 pjtoi ⊢ ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( projℎ ‘ ℋ )
16 15 coeq2i ⊢ ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) ) = ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ℋ ) )
17 2 pjfi ⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
18 6 pjfi ⊢ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) : ℋ ⟶ ℋ
19 1 17 18 pjsdii ⊢ ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ 𝐻 ) +op ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) +op ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) )
20 16 19 eqtr3i ⊢ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ℋ ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) +op ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) )
21 14 20 eqtr3i ⊢ ( projℎ ‘ 𝐺 ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) +op ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) )
22 inss2 ⊢ ( 𝐺 ∩ 𝐻 ) ⊆ 𝐻
23 1 choccli ⊢ ( ⊥ ‘ 𝐺 ) ∈ Cℋ
24 2 23 chub2i ⊢ 𝐻 ⊆ ( ( ⊥ ‘ 𝐺 ) ∨ℋ 𝐻 )
25 22 24 sstri ⊢ ( 𝐺 ∩ 𝐻 ) ⊆ ( ( ⊥ ‘ 𝐺 ) ∨ℋ 𝐻 )
26 1 2 chdmm3i ⊢ ( ⊥ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) = ( ( ⊥ ‘ 𝐺 ) ∨ℋ 𝐻 )
27 25 26 sseqtrri ⊢ ( 𝐺 ∩ 𝐻 ) ⊆ ( ⊥ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) )
28 1 2 chincli ⊢ ( 𝐺 ∩ 𝐻 ) ∈ Cℋ
29 1 6 chincli ⊢ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ∈ Cℋ
30 28 29 pjscji ⊢ ( ( 𝐺 ∩ 𝐻 ) ⊆ ( ⊥ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) → ( projℎ ‘ ( ( 𝐺 ∩ 𝐻 ) ∨ℋ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ) = ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) +op ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ) )
31 27 30 ax-mp ⊢ ( projℎ ‘ ( ( 𝐺 ∩ 𝐻 ) ∨ℋ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ) = ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) +op ( projℎ ‘ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) )
32 9 21 31 3eqtr4g ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( projℎ ‘ 𝐺 ) = ( projℎ ‘ ( ( 𝐺 ∩ 𝐻 ) ∨ℋ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ) )
33 28 29 chjcli ⊢ ( ( 𝐺 ∩ 𝐻 ) ∨ℋ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ∈ Cℋ
34 1 33 pj11i ⊢ ( ( projℎ ‘ 𝐺 ) = ( projℎ ‘ ( ( 𝐺 ∩ 𝐻 ) ∨ℋ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) ) ↔ 𝐺 = ( ( 𝐺 ∩ 𝐻 ) ∨ℋ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) )
35 32 34 sylib ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → 𝐺 = ( ( 𝐺 ∩ 𝐻 ) ∨ℋ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) )
36 1 2 cmbri ⊢ ( 𝐺 𝐶ℋ 𝐻 ↔ 𝐺 = ( ( 𝐺 ∩ 𝐻 ) ∨ℋ ( 𝐺 ∩ ( ⊥ ‘ 𝐻 ) ) ) )
37 35 36 sylibr ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → 𝐺 𝐶ℋ 𝐻 )
38 3 37 impbii ⊢ ( 𝐺 𝐶ℋ 𝐻 ↔ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) )