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_ℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) )

Metamath Proof Explorer

Theorem pj3si

Proof