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	imbitrrid	⊢ ( ( ( 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ℎ ‘ ( 𝐺 ∩ 𝐻 ) ) )