Metamath Proof Explorer

Theorem pjadj2coi

Description: Adjoint of double composition of projections. Generalization of special case of Theorem 3.11(viii) of Beran p. 106. (Contributed by NM, 1-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjadj2co.1 ⊢F∈Cℋ
pjadj2co.2 ⊢G∈Cℋ
pjadj2co.3 ⊢H∈Cℋ
Assertion pjadj2coi ⊢A∈ℋ∧B∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A⋅ihB=A⋅ihprojℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡B

Proof

Step Hyp Ref Expression
1 pjadj2co.1 ⊢F∈Cℋ
2 pjadj2co.2 ⊢G∈Cℋ
3 pjadj2co.3 ⊢H∈Cℋ
4 3 pjhcli ⊢A∈ℋ→projℎ⁡H⁡A∈ℋ
5 1 2 pjadjcoi ⊢projℎ⁡H⁡A∈ℋ∧B∈ℋ→projℎ⁡F∘projℎ⁡G⁡projℎ⁡H⁡A⋅ihB=projℎ⁡H⁡A⋅ihprojℎ⁡G∘projℎ⁡F⁡B
6 4 5 sylan ⊢A∈ℋ∧B∈ℋ→projℎ⁡F∘projℎ⁡G⁡projℎ⁡H⁡A⋅ihB=projℎ⁡H⁡A⋅ihprojℎ⁡G∘projℎ⁡F⁡B
7 2 1 pjcohcli ⊢B∈ℋ→projℎ⁡G∘projℎ⁡F⁡B∈ℋ
8 3 pjadji ⊢A∈ℋ∧projℎ⁡G∘projℎ⁡F⁡B∈ℋ→projℎ⁡H⁡A⋅ihprojℎ⁡G∘projℎ⁡F⁡B=A⋅ihprojℎ⁡H⁡projℎ⁡G∘projℎ⁡F⁡B
9 7 8 sylan2 ⊢A∈ℋ∧B∈ℋ→projℎ⁡H⁡A⋅ihprojℎ⁡G∘projℎ⁡F⁡B=A⋅ihprojℎ⁡H⁡projℎ⁡G∘projℎ⁡F⁡B
10 6 9 eqtrd ⊢A∈ℋ∧B∈ℋ→projℎ⁡F∘projℎ⁡G⁡projℎ⁡H⁡A⋅ihB=A⋅ihprojℎ⁡H⁡projℎ⁡G∘projℎ⁡F⁡B
11 1 pjfi ⊢projℎ⁡F:ℋ⟶ℋ
12 2 pjfi ⊢projℎ⁡G:ℋ⟶ℋ
13 11 12 hocofi ⊢projℎ⁡F∘projℎ⁡G:ℋ⟶ℋ
14 3 pjfi ⊢projℎ⁡H:ℋ⟶ℋ
15 13 14 hocoi ⊢A∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A=projℎ⁡F∘projℎ⁡G⁡projℎ⁡H⁡A
16 15 oveq1d ⊢A∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A⋅ihB=projℎ⁡F∘projℎ⁡G⁡projℎ⁡H⁡A⋅ihB
17 16 adantr ⊢A∈ℋ∧B∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A⋅ihB=projℎ⁡F∘projℎ⁡G⁡projℎ⁡H⁡A⋅ihB
18 coass ⊢projℎ⁡H∘projℎ⁡G∘projℎ⁡F=projℎ⁡H∘projℎ⁡G∘projℎ⁡F
19 18 fveq1i ⊢projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡B=projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡B
20 12 11 hocofi ⊢projℎ⁡G∘projℎ⁡F:ℋ⟶ℋ
21 14 20 hocoi ⊢B∈ℋ→projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡B=projℎ⁡H⁡projℎ⁡G∘projℎ⁡F⁡B
22 19 21 eqtrid ⊢B∈ℋ→projℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡B=projℎ⁡H⁡projℎ⁡G∘projℎ⁡F⁡B
23 22 oveq2d ⊢B∈ℋ→A⋅ihprojℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡B=A⋅ihprojℎ⁡H⁡projℎ⁡G∘projℎ⁡F⁡B
24 23 adantl ⊢A∈ℋ∧B∈ℋ→A⋅ihprojℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡B=A⋅ihprojℎ⁡H⁡projℎ⁡G∘projℎ⁡F⁡B
25 10 17 24 3eqtr4d ⊢A∈ℋ∧B∈ℋ→projℎ⁡F∘projℎ⁡G∘projℎ⁡H⁡A⋅ihB=A⋅ihprojℎ⁡H∘projℎ⁡G∘projℎ⁡F⁡B