Metamath Proof Explorer

Theorem pjclem3

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

Ref Expression
Hypotheses pjclem1.1 ⊢ 𝐺 ∈ Cℋ
pjclem1.2 ⊢ 𝐻 ∈ Cℋ
Assertion pjclem3 ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ∘ ( projℎ ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 pjclem1.1 ⊢ 𝐺 ∈ Cℋ
2 pjclem1.2 ⊢ 𝐻 ∈ Cℋ
3 df-iop ⊢ Iop = ( projℎ ‘ ℋ )
4 3 coeq2i ⊢ ( ( projℎ ‘ 𝐺 ) ∘ Iop ) = ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ℋ ) )
5 1 pjfi ⊢ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ
6 5 hoid1i ⊢ ( ( projℎ ‘ 𝐺 ) ∘ Iop ) = ( projℎ ‘ 𝐺 )
7 4 6 eqtr3i ⊢ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ℋ ) ) = ( projℎ ‘ 𝐺 )
8 5 hoid1ri ⊢ ( Iop ∘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ 𝐺 )
9 3 coeq1i ⊢ ( Iop ∘ ( projℎ ‘ 𝐺 ) ) = ( ( projℎ ‘ ℋ ) ∘ ( projℎ ‘ 𝐺 ) )
10 7 8 9 3eqtr2i ⊢ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ℋ ) ) = ( ( projℎ ‘ ℋ ) ∘ ( projℎ ‘ 𝐺 ) )
11 10 oveq1i ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ℋ ) ) −op ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ) = ( ( ( projℎ ‘ ℋ ) ∘ ( projℎ ‘ 𝐺 ) ) −op ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) )
12 oveq2 ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( ( projℎ ‘ ℋ ) ∘ ( projℎ ‘ 𝐺 ) ) −op ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ) = ( ( ( projℎ ‘ ℋ ) ∘ ( projℎ ‘ 𝐺 ) ) −op ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ) )
13 11 12 syl5eq ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ℋ ) ) −op ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ) = ( ( ( projℎ ‘ ℋ ) ∘ ( projℎ ‘ 𝐺 ) ) −op ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ) )
14 helch ⊢ ℋ ∈ Cℋ
15 14 pjfi ⊢ ( projℎ ‘ ℋ ) : ℋ ⟶ ℋ
16 2 pjfi ⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
17 1 15 16 pjddii ⊢ ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ ℋ ) −op ( projℎ ‘ 𝐻 ) ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ℋ ) ) −op ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) )
18 15 16 5 hocsubdiri ⊢ ( ( ( projℎ ‘ ℋ ) −op ( projℎ ‘ 𝐻 ) ) ∘ ( projℎ ‘ 𝐺 ) ) = ( ( ( projℎ ‘ ℋ ) ∘ ( projℎ ‘ 𝐺 ) ) −op ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) )
19 13 17 18 3eqtr4g ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ ℋ ) −op ( projℎ ‘ 𝐻 ) ) ) = ( ( ( projℎ ‘ ℋ ) −op ( projℎ ‘ 𝐻 ) ) ∘ ( projℎ ‘ 𝐺 ) ) )
20 2 pjoci ⊢ ( ( projℎ ‘ ℋ ) −op ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( ⊥ ‘ 𝐻 ) )
21 20 coeq2i ⊢ ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ ℋ ) −op ( projℎ ‘ 𝐻 ) ) ) = ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) )
22 20 coeq1i ⊢ ( ( ( projℎ ‘ ℋ ) −op ( projℎ ‘ 𝐻 ) ) ∘ ( projℎ ‘ 𝐺 ) ) = ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ∘ ( projℎ ‘ 𝐺 ) )
23 19 21 22 3eqtr3g ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ∘ ( projℎ ‘ 𝐺 ) ) )