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 ⊢ 𝐹 ∈ Cℋ
pjadj2co.2 ⊢ 𝐺 ∈ Cℋ
pjadj2co.3 ⊢ 𝐻 ∈ Cℋ
Assertion pjadj2coi ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) ·ih 𝐵 ) = ( 𝐴 ·ih ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 pjadj2co.1 ⊢ 𝐹 ∈ Cℋ
2 pjadj2co.2 ⊢ 𝐺 ∈ Cℋ
3 pjadj2co.3 ⊢ 𝐻 ∈ Cℋ
4 3 pjhcli ⊢ ( 𝐴 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ )
5 1 2 pjadjcoi ⊢ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐵 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) )
6 4 5 sylan ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐵 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) )
7 2 1 pjcohcli ⊢ ( 𝐵 ∈ ℋ → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ∈ ℋ )
8 3 pjadji ⊢ ( ( 𝐴 ∈ ℋ ∧ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) = ( 𝐴 ·ih ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) ) )
9 7 8 sylan2 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ·ih ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) = ( 𝐴 ·ih ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) ) )
10 6 9 eqtrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐵 ) = ( 𝐴 ·ih ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) ) )
11 1 pjfi ⊢ ( projℎ ‘ 𝐹 ) : ℋ ⟶ ℋ
12 2 pjfi ⊢ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ
13 11 12 hocofi ⊢ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) : ℋ ⟶ ℋ
14 3 pjfi ⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
15 13 14 hocoi ⊢ ( 𝐴 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
16 15 oveq1d ⊢ ( 𝐴 ∈ ℋ → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) ·ih 𝐵 ) = ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐵 ) )
17 16 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) ·ih 𝐵 ) = ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ·ih 𝐵 ) )
18 coass ⊢ ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) )
19 18 fveq1i ⊢ ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ) ‘ 𝐵 )
20 12 11 hocofi ⊢ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) : ℋ ⟶ ℋ
21 14 20 hocoi ⊢ ( 𝐵 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ∘ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ) ‘ 𝐵 ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) )
22 19 21 syl5eq ⊢ ( 𝐵 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) )
23 22 oveq2d ⊢ ( 𝐵 ∈ ℋ → ( 𝐴 ·ih ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) = ( 𝐴 ·ih ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) ) )
24 23 adantl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) = ( 𝐴 ·ih ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) ) )
25 10 17 24 3eqtr4d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝐴 ) ·ih 𝐵 ) = ( 𝐴 ·ih ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝐵 ) ) )