Metamath Proof Explorer

Theorem pj3si

Description: Stronger projection triplet theorem. (Contributed by NM, 2-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjadj2co.1 ⊢ 𝐹 ∈ Cℋ
pjadj2co.2 ⊢ 𝐺 ∈ Cℋ
pjadj2co.3 ⊢ 𝐻 ∈ Cℋ
Assertion pj3si ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( 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 1 2 3 pj2cocli ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐹 )
5 4 adantl ⊢ ( ( ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐹 )
6 1 pjfi ⊢ ( projℎ ‘ 𝐹 ) : ℋ ⟶ ℋ
7 2 pjfi ⊢ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ
8 6 7 hocofi ⊢ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) : ℋ ⟶ ℋ
9 3 pjfi ⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
10 8 9 hocofni ⊢ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) Fn ℋ
11 fnfvelrn ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) Fn ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) )
12 10 11 mpan ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) )
13 ssel ⊢ ( ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐺 ) )
14 12 13 syl5 ⊢ ( ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 → ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐺 ) )
15 14 imp ⊢ ( ( ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐺 )
16 5 15 elind ⊢ ( ( ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ( 𝐹 ∩ 𝐺 ) )
17 16 adantll ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ( 𝐹 ∩ 𝐺 ) )
18 3 2 1 pj2cocli ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝑥 ) ∈ 𝐻 )
19 fveq1 ⊢ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝑥 ) )
20 19 eleq1d ⊢ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐻 ↔ ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝑥 ) ∈ 𝐻 ) )
21 18 20 imbitrrid ⊢ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) → ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐻 ) )
22 21 imp ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐻 )
23 22 adantlr ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐻 )
24 17 23 elind ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) )
25 8 9 hococli ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ )
26 hvsubcl ⊢ ( ( 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ) → ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ℋ )
27 25 26 mpdan ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ℋ )
28 27 adantl ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ 𝑥 ∈ ℋ ) → ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ℋ )
29 simpl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) → 𝑥 ∈ ℋ )
30 25 adantr ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ )
31 1 2 chincli ⊢ ( 𝐹 ∩ 𝐺 ) ∈ Cℋ
32 31 3 chincli ⊢ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ∈ Cℋ
33 32 cheli ⊢ ( 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) → 𝑦 ∈ ℋ )
34 33 adantl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) → 𝑦 ∈ ℋ )
35 29 30 34 3jca ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) → ( 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
36 35 adantl ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ) → ( 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
37 his2sub ⊢ ( ( 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = ( ( 𝑥 ·ih 𝑦 ) − ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
38 36 37 syl ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ) → ( ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = ( ( 𝑥 ·ih 𝑦 ) − ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
39 19 adantr ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝑥 ) )
40 39 oveq1d ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝑥 ) ·ih 𝑦 ) )
41 3 2 1 pjadj2coi ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) )
42 33 41 sylan2 ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) → ( ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) )
43 1 2 3 pj3lem1 ⊢ ( 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) = 𝑦 )
44 43 oveq2d ⊢ ( 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) → ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) )
45 44 adantl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) → ( 𝑥 ·ih ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) )
46 42 45 eqtrd ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) → ( ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih 𝑦 ) )
47 40 46 sylan9eq ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih 𝑦 ) )
48 47 oveq1d ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ) → ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) − ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) = ( ( 𝑥 ·ih 𝑦 ) − ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
49 25 33 anim12i ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
50 49 adantl ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
51 hicl ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ )
52 50 51 syl ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ )
53 52 subidd ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ) → ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) − ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) = 0 )
54 38 48 53 3eqtr2d ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ) → ( ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = 0 )
55 54 expr ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ 𝑥 ∈ ℋ ) → ( 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) → ( ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = 0 ) )
56 55 ralrimiv ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ 𝑥 ∈ ℋ ) → ∀ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ( ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = 0 )
57 32 chshii ⊢ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ∈ Sℋ
58 shocel ⊢ ( ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ∈ Sℋ → ( ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ↔ ( ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ℋ ∧ ∀ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ( ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = 0 ) ) )
59 57 58 ax-mp ⊢ ( ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ↔ ( ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ℋ ∧ ∀ 𝑦 ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ( ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = 0 ) )
60 28 56 59 sylanbrc ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ 𝑥 ∈ ℋ ) → ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) )
61 32 pjvi ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ∧ ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ) → ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) ) = ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) )
62 24 60 61 syl2anc ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ 𝑥 ∈ ℋ ) → ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) ) = ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) )
63 id ⊢ ( 𝑥 ∈ ℋ → 𝑥 ∈ ℋ )
64 hvaddsub12 ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ) → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 +ℎ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) )
65 25 63 25 64 syl3anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 +ℎ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) )
66 hvsubid ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) = 0ℎ )
67 25 66 syl ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) = 0ℎ )
68 67 oveq2d ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 +ℎ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 +ℎ 0ℎ ) )
69 ax-hvaddid ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 +ℎ 0ℎ ) = 𝑥 )
70 68 69 eqtrd ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 +ℎ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) = 𝑥 )
71 65 70 eqtrd ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) = 𝑥 )
72 71 fveq2d ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) ) = ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑥 ) )
73 72 adantl ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ 𝑥 ∈ ℋ ) → ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) ) = ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑥 ) )
74 62 73 eqtr3d ⊢ ( ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑥 ) )
75 74 ralrimiva ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) → ∀ 𝑥 ∈ ℋ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑥 ) )
76 8 9 hocofi ⊢ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) : ℋ ⟶ ℋ
77 32 pjfi ⊢ ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) : ℋ ⟶ ℋ
78 76 77 hoeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) ‘ 𝑥 ) ↔ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) )
79 75 78 sylib ⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) → ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) )