Metamath Proof Explorer

Theorem pjcmul1i

Description: A necessary and sufficient condition for the product of two projectors to be a projector is that the projectors commute. Part 1 of Theorem 1 of AkhiezerGlazman p. 65. (Contributed by NM, 3-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjclem1.1 ⊢ 𝐺 ∈ Cℋ
pjclem1.2 ⊢ 𝐻 ∈ Cℋ
Assertion pjcmul1i ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ↔ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ∈ ran projℎ )

Proof

Step Hyp Ref Expression
1 pjclem1.1 ⊢ 𝐺 ∈ Cℋ
2 pjclem1.2 ⊢ 𝐻 ∈ Cℋ
3 1 2 pjclem4 ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) )
4 pjmfn ⊢ projℎ Fn Cℋ
5 1 2 chincli ⊢ ( 𝐺 ∩ 𝐻 ) ∈ Cℋ
6 fnfvelrn ⊢ ( ( projℎ Fn Cℋ ∧ ( 𝐺 ∩ 𝐻 ) ∈ Cℋ ) → ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ∈ ran projℎ )
7 4 5 6 mp2an ⊢ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ∈ ran projℎ
8 3 7 eqeltrdi ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ∈ ran projℎ )
9 pjadj2 ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ∈ ran projℎ → ( adjℎ ‘ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ) = ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) )
10 1 pjbdlni ⊢ ( projℎ ‘ 𝐺 ) ∈ BndLinOp
11 2 pjbdlni ⊢ ( projℎ ‘ 𝐻 ) ∈ BndLinOp
12 10 11 adjcoi ⊢ ( adjℎ ‘ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ) = ( ( adjℎ ‘ ( projℎ ‘ 𝐻 ) ) ∘ ( adjℎ ‘ ( projℎ ‘ 𝐺 ) ) )
13 pjadj3 ⊢ ( 𝐻 ∈ Cℋ → ( adjℎ ‘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐻 ) )
14 2 13 ax-mp ⊢ ( adjℎ ‘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐻 )
15 pjadj3 ⊢ ( 𝐺 ∈ Cℋ → ( adjℎ ‘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ 𝐺 ) )
16 1 15 ax-mp ⊢ ( adjℎ ‘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ 𝐺 )
17 14 16 coeq12i ⊢ ( ( adjℎ ‘ ( projℎ ‘ 𝐻 ) ) ∘ ( adjℎ ‘ ( projℎ ‘ 𝐺 ) ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) )
18 12 17 eqtri ⊢ ( adjℎ ‘ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) )
19 9 18 eqtr3di ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ∈ ran projℎ → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) )
20 8 19 impbii ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ↔ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ∈ ran projℎ )