Metamath Proof Explorer

Theorem pj3cor1i

Description: Projection triplet corollary. (Contributed by NM, 2-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjadj2co.1 ⊢ 𝐹 ∈ Cℋ
pjadj2co.2 ⊢ 𝐺 ∈ Cℋ
pjadj2co.3 ⊢ 𝐻 ∈ Cℋ
Assertion pj3cor1i ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 pjadj2co.1 ⊢ 𝐹 ∈ Cℋ
2 pjadj2co.2 ⊢ 𝐺 ∈ Cℋ
3 pjadj2co.3 ⊢ 𝐻 ∈ Cℋ
4 fveq1 ⊢ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) = ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) )
5 4 oveq2d ⊢ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) → ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) )
6 5 adantl ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) )
7 6 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) ) ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) )
8 1 2 chincli ⊢ ( 𝐹 ∩ 𝐺 ) ∈ Cℋ
9 8 3 chincli ⊢ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ∈ Cℋ
10 9 pjadji ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑦 ) ) )
11 10 adantlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) ) ∧ 𝑦 ∈ ℋ ) → ( ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑦 ) ) )
12 1 2 3 pj3i ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) )
13 12 fveq1d ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑥 ) )
14 13 oveq1d ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) )
15 14 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) ) ∧ 𝑦 ∈ ℋ ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) )
16 12 fveq1d ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) = ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑦 ) )
17 16 oveq2d ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑦 ) ) )
18 17 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) ) ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑦 ) ) )
19 11 15 18 3eqtr4d ⊢ ( ( ( 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) ) ∧ 𝑦 ∈ ℋ ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) )
20 3 1 2 pjadj2coi ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) )
21 20 adantlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) ) ∧ 𝑦 ∈ ℋ ) → ( ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) )
22 7 19 21 3eqtr4d ⊢ ( ( ( 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) ) ∧ 𝑦 ∈ ℋ ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑦 ) )
23 22 exp31 ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( 𝑦 ∈ ℋ → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) ) )
24 23 ralrimdv ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ∀ 𝑦 ∈ ℋ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
25 1 pjfi ⊢ ( projℎ ‘ 𝐹 ) : ℋ ⟶ ℋ
26 2 pjfi ⊢ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ
27 25 26 hocofi ⊢ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) : ℋ ⟶ ℋ
28 3 pjfi ⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
29 27 28 hococli ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ )
30 28 25 hocofi ⊢ ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) : ℋ ⟶ ℋ
31 30 26 hococli ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ∈ ℋ )
32 hial2eq ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ∈ ℋ ) → ( ∀ 𝑦 ∈ ℋ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ) )
33 29 31 32 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ) )
34 24 33 sylibd ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ) )
35 34 com12 ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ) )
36 35 ralrimiv ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ∀ 𝑥 ∈ ℋ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) )
37 27 28 hocofi ⊢ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) : ℋ ⟶ ℋ
38 30 26 hocofi ⊢ ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) : ℋ ⟶ ℋ
39 37 38 hoeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ↔ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) )
40 36 39 sylib ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐺 ) ) )