Theorem pj3si

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

	Ref	Expression
Hypotheses	pjadj2co.1	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
	pjadj2co.2	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjadj2co.3	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pj3si	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjadj2co.1	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjadj2co.2	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
3		pjadj2co.3	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
4	1 2 3	pj2cocli	$$⊢x\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in F$$
5	4	adantl	$$⊢\left(\mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\wedge x\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in F$$
6	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(F\right):\mathscr{H}⟶\mathscr{H}$$
7	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
8	6 7	hocofi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right):\mathscr{H}⟶\mathscr{H}$$
9	3	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
10	8 9	hocofni	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)Fn\mathscr{H}$$
11		fnfvelrn	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)Fn\mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
12	10 11	mpan	$$⊢x\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
13		ssel	$$⊢\mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in G\right)$$
14	12 13	syl5	$$⊢\mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\to \left(x\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in G\right)$$
15	14	imp	$$⊢\left(\mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\wedge x\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in G$$
16	5 15	elind	$$⊢\left(\mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\wedge x\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \left(F\cap G\right)$$
17	16	adantll	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge x\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \left(F\cap G\right)$$
18	3 2 1	pj2cocli	$$⊢x\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(x\right)\in H$$
19		fveq1	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(x\right)$$
20	19	eleq1d	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in H\leftrightarrow \left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(x\right)\in H\right)$$
21	18 20	syl5ibr	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\to \left(x\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in H\right)$$
22	21	imp	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge x\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in H$$
23	22	adantlr	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge x\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in H$$
24	17 23	elind	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge x\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \left(\left(F\cap G\right)\cap H\right)$$
25	8 9	hococli	$$⊢x\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}$$
26		hvsubcl	$$⊢\left(x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\right)\to x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}$$
27	25 26	mpdan	$$⊢x\in \mathscr{H}\to x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}$$
28	27	adantl	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge x\in \mathscr{H}\right)\to x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}$$
29		simpl	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\to x\in \mathscr{H}$$
30	25	adantr	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}$$
31	1 2	chincli	$$⊢F\cap G\in {\mathbf{C}}_{\mathscr{H}}$$
32	31 3	chincli	$$⊢\left(F\cap G\right)\cap H\in {\mathbf{C}}_{\mathscr{H}}$$
33	32	cheli	$$⊢y\in \left(\left(F\cap G\right)\cap H\right)\to y\in \mathscr{H}$$
34	33	adantl	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\to y\in \mathscr{H}$$
35	29 30 34	3jca	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\to \left(x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)$$
36	35	adantl	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\right)\to \left(x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)$$
37		his2sub	$$⊢\left(x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to \left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=\left(x{\cdot }_{\mathrm{ih}}y\right)-\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
38	36 37	syl	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\right)\to \left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=\left(x{\cdot }_{\mathrm{ih}}y\right)-\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
39	19	adantr	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(x\right)$$
40	39	oveq1d	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y$$
41	3 2 1	pjadj2coi	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)$$
42	33 41	sylan2	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)$$
43	1 2 3	pj3lem1	$$⊢y\in \left(\left(F\cap G\right)\cap H\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=y$$
44	43	oveq2d	$$⊢y\in \left(\left(F\cap G\right)\cap H\right)\to x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}y$$
45	44	adantl	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\to x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}y$$
46	42 45	eqtrd	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}y$$
47	40 46	sylan9eq	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}y$$
48	47	oveq1d	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\right)\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)-\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)=\left(x{\cdot }_{\mathrm{ih}}y\right)-\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
49	25 33	anim12i	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)$$
50	49	adantl	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\right)\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)$$
51		hicl	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\in ℂ$$
52	50 51	syl	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\in ℂ$$
53	52	subidd	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\right)\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)-\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)=0$$
54	38 48 53	3eqtr2d	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(\left(F\cap G\right)\cap H\right)\right)\right)\to \left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=0$$
55	54	expr	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge x\in \mathscr{H}\right)\to \left(y\in \left(\left(F\cap G\right)\cap H\right)\to \left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=0\right)$$
56	55	ralrimiv	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge x\in \mathscr{H}\right)\to \forall y\in \left(\left(F\cap G\right)\cap H\right)\left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=0$$
57	32	chshii	$$⊢\left(F\cap G\right)\cap H\in {\mathbf{S}}_{\mathscr{H}}$$
58		shocel	$$⊢\left(F\cap G\right)\cap H\in {\mathbf{S}}_{\mathscr{H}}\to \left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \perp \left(\left(F\cap G\right)\cap H\right)\leftrightarrow \left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge \forall y\in \left(\left(F\cap G\right)\cap H\right)\left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=0\right)\right)$$
59	57 58	ax-mp	$$⊢x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \perp \left(\left(F\cap G\right)\cap H\right)\leftrightarrow \left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge \forall y\in \left(\left(F\cap G\right)\cap H\right)\left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=0\right)$$
60	28 56 59	sylanbrc	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge x\in \mathscr{H}\right)\to x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \perp \left(\left(F\cap G\right)\cap H\right)$$
61	32	pjvi	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \left(\left(F\cap G\right)\cap H\right)\wedge x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \perp \left(\left(F\cap G\right)\cap H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)$$
62	24 60 61	syl2anc	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge x\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)$$
63		id	$$⊢x\in \mathscr{H}\to x\in \mathscr{H}$$
64		hvaddsub12	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)=x{+}_{ℎ}\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)$$
65	25 63 25 64	syl3anc	$$⊢x\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)=x{+}_{ℎ}\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)$$
66		hvsubid	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=0_{ℎ}$$
67	25 66	syl	$$⊢x\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=0_{ℎ}$$
68	67	oveq2d	$$⊢x\in \mathscr{H}\to x{+}_{ℎ}\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)=x{+}_{ℎ}{0}_{ℎ}$$
69		ax-hvaddid	$$⊢x\in \mathscr{H}\to x{+}_{ℎ}{0}_{ℎ}=x$$
70	68 69	eqtrd	$$⊢x\in \mathscr{H}\to x{+}_{ℎ}\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)=x$$
71	65 70	eqtrd	$$⊢x\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)=x$$
72	71	fveq2d	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(x\right)$$
73	72	adantl	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge x\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(x\right)$$
74	62 73	eqtr3d	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\wedge x\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(x\right)$$
75	74	ralrimiva	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\to \forall x\in \mathscr{H}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(x\right)$$
76	8 9	hocofi	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right):\mathscr{H}⟶\mathscr{H}$$
77	32	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right):\mathscr{H}⟶\mathscr{H}$$
78	76 77	hoeqi	$$⊢\forall x\in \mathscr{H}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(x\right)\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)$$
79	75 78	sylib	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \mathrm{ran}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\subseteq G\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)$$