Metamath Proof Explorer

Theorem pjclem4

Description: Lemma for projection commutation theorem. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjclem1.1 ⊢ 𝐺 ∈ Cℋ
pjclem1.2 ⊢ 𝐻 ∈ Cℋ
Assertion pjclem4 ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 pjclem1.1 ⊢ 𝐺 ∈ Cℋ
2 pjclem1.2 ⊢ 𝐻 ∈ Cℋ
3 1 2 pjcocli ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐺 )
4 3 adantl ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐺 )
5 2 1 pjcocli ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ∈ 𝐻 )
6 fveq1 ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) )
7 6 eleq1d ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐻 ↔ ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ∈ 𝐻 ) )
8 5 7 syl5ibr ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐻 ) )
9 8 imp ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ 𝐻 )
10 4 9 elind ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ( 𝐺 ∩ 𝐻 ) )
11 1 2 pjcohcli ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ )
12 hvsubcl ⊢ ( ( 𝑥 ∈ ℋ ∧ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ) → ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ℋ )
13 11 12 mpdan ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ℋ )
14 13 adantl ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ 𝑥 ∈ ℋ ) → ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ℋ )
15 simpl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) → 𝑥 ∈ ℋ )
16 11 adantr ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ )
17 1 2 chincli ⊢ ( 𝐺 ∩ 𝐻 ) ∈ Cℋ
18 17 cheli ⊢ ( 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) → 𝑦 ∈ ℋ )
19 18 adantl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) → 𝑦 ∈ ℋ )
20 15 16 19 3jca ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) → ( 𝑥 ∈ ℋ ∧ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
21 20 adantl ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) ) → ( 𝑥 ∈ ℋ ∧ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
22 his2sub ⊢ ( ( 𝑥 ∈ ℋ ∧ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = ( ( 𝑥 ·ih 𝑦 ) − ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
23 21 22 syl ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) ) → ( ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = ( ( 𝑥 ·ih 𝑦 ) − ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
24 6 oveq1d ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑦 ) )
25 2 1 pjadjcoi ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) )
26 18 25 sylan2 ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) → ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) )
27 1 2 pjclem4a ⊢ ( 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) = 𝑦 )
28 27 oveq2d ⊢ ( 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) → ( 𝑥 ·ih ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) )
29 28 adantl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) → ( 𝑥 ·ih ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) )
30 26 29 eqtrd ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) → ( ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih 𝑦 ) )
31 24 30 sylan9eq ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) ) → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih 𝑦 ) )
32 31 oveq1d ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) ) → ( ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) − ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) = ( ( 𝑥 ·ih 𝑦 ) − ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
33 11 18 anim12i ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
34 33 adantl ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) ) → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
35 hicl ⊢ ( ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ )
36 34 35 syl ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) ) → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ∈ ℂ )
37 36 subidd ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) ) → ( ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) − ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ·ih 𝑦 ) ) = 0 )
38 23 32 37 3eqtr2d ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ) ) → ( ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = 0 )
39 38 expr ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ 𝑥 ∈ ℋ ) → ( 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) → ( ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = 0 ) )
40 39 ralrimiv ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ 𝑥 ∈ ℋ ) → ∀ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ( ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = 0 )
41 17 chshii ⊢ ( 𝐺 ∩ 𝐻 ) ∈ Sℋ
42 shocel ⊢ ( ( 𝐺 ∩ 𝐻 ) ∈ Sℋ → ( ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ( 𝐺 ∩ 𝐻 ) ) ↔ ( ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ℋ ∧ ∀ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ( ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = 0 ) ) )
43 41 42 ax-mp ⊢ ( ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ( 𝐺 ∩ 𝐻 ) ) ↔ ( ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ℋ ∧ ∀ 𝑦 ∈ ( 𝐺 ∩ 𝐻 ) ( ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ·ih 𝑦 ) = 0 ) )
44 14 40 43 sylanbrc ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ 𝑥 ∈ ℋ ) → ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ( 𝐺 ∩ 𝐻 ) ) )
45 17 pjvi ⊢ ( ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ( 𝐺 ∩ 𝐻 ) ∧ ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ∈ ( ⊥ ‘ ( 𝐺 ∩ 𝐻 ) ) ) → ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ‘ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) )
46 10 44 45 syl2anc ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ 𝑥 ∈ ℋ ) → ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ‘ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) )
47 id ⊢ ( 𝑥 ∈ ℋ → 𝑥 ∈ ℋ )
48 hvaddsub12 ⊢ ( ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ∧ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 +ℎ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) )
49 11 47 11 48 syl3anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 +ℎ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) )
50 hvsubid ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ∈ ℋ → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) = 0ℎ )
51 11 50 syl ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) = 0ℎ )
52 51 oveq2d ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 +ℎ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 +ℎ 0ℎ ) )
53 ax-hvaddid ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 +ℎ 0ℎ ) = 𝑥 )
54 49 52 53 3eqtrd ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) = 𝑥 )
55 54 fveq2d ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ‘ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) ) = ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ‘ 𝑥 ) )
56 55 adantl ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ 𝑥 ∈ ℋ ) → ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ‘ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) +ℎ ( 𝑥 −ℎ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) ) ) ) = ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ‘ 𝑥 ) )
57 46 56 eqtr3d ⊢ ( ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ‘ 𝑥 ) )
58 57 ralrimiva ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ∀ 𝑥 ∈ ℋ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ‘ 𝑥 ) )
59 1 pjfi ⊢ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ
60 2 pjfi ⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
61 59 60 hocofi ⊢ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) : ℋ ⟶ ℋ
62 17 pjfi ⊢ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) : ℋ ⟶ ℋ
63 61 62 hoeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ‘ 𝑥 ) ↔ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) )
64 58 63 sylib ⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) )