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 ⊢G∈Cℋ
pjclem1.2 ⊢H∈Cℋ
Assertion pjclem3 ⊢projℎ⁡G∘projℎ⁡H=projℎ⁡H∘projℎ⁡G→projℎ⁡G∘projℎ⁡⊥⁡H=projℎ⁡⊥⁡H∘projℎ⁡G

Proof

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