Theorem pjclem4

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

	Ref	Expression
Hypotheses	pjclem1.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjclem1.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjclem4	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjclem1.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjclem1.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	pjcocli	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in G$$
4	3	adantl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in G$$
5	2 1	pjcocli	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)\in H$$
6		fveq1	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)$$
7	6	eleq1d	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in H\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)\in H\right)$$
8	5 7	syl5ibr	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to \left(x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in H\right)$$
9	8	imp	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in H$$
10	4 9	elind	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \left(G\cap H\right)$$
11	1 2	pjcohcli	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}$$
12		hvsubcl	$$⊢\left(x\in \mathscr{H}\wedge \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\right)\to x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}$$
13	11 12	mpdan	$$⊢x\in \mathscr{H}\to x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}$$
14	13	adantl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge x\in \mathscr{H}\right)\to x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}$$
15		simpl	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\to x\in \mathscr{H}$$
16	11	adantr	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}$$
17	1 2	chincli	$$⊢G\cap H\in {\mathbf{C}}_{\mathscr{H}}$$
18	17	cheli	$$⊢y\in \left(G\cap H\right)\to y\in \mathscr{H}$$
19	18	adantl	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\to y\in \mathscr{H}$$
20	15 16 19	3jca	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\to \left(x\in \mathscr{H}\wedge \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)$$
21	20	adantl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\right)\to \left(x\in \mathscr{H}\wedge \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)$$
22		his2sub	$$⊢\left(x\in \mathscr{H}\wedge \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to \left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\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({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
23	21 22	syl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\right)\to \left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\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({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
24	6	oveq1d	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y$$
25	2 1	pjadjcoi	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)$$
26	18 25	sylan2	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)$$
27	1 2	pjclem4a	$$⊢y\in \left(G\cap H\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=y$$
28	27	oveq2d	$$⊢y\in \left(G\cap H\right)\to x{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}y$$
29	28	adantl	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\to x{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}y$$
30	26 29	eqtrd	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}y$$
31	24 30	sylan9eq	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}y$$
32	31	oveq1d	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)-\left(\left({\mathrm{proj}}_{ℎ}\left(G\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({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
33	11 18	anim12i	$$⊢\left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)$$
34	33	adantl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)$$
35		hicl	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\in ℂ$$
36	34 35	syl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\in ℂ$$
37	36	subidd	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)-\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)=0$$
38	23 32 37	3eqtr2d	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge \left(x\in \mathscr{H}\wedge y\in \left(G\cap H\right)\right)\right)\to \left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=0$$
39	38	expr	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge x\in \mathscr{H}\right)\to \left(y\in \left(G\cap H\right)\to \left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=0\right)$$
40	39	ralrimiv	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge x\in \mathscr{H}\right)\to \forall y\in \left(G\cap H\right)\left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=0$$
41	17	chshii	$$⊢G\cap H\in {\mathbf{S}}_{\mathscr{H}}$$
42		shocel	$$⊢G\cap H\in {\mathbf{S}}_{\mathscr{H}}\to \left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \perp \left(G\cap H\right)\leftrightarrow \left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge \forall y\in \left(G\cap H\right)\left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=0\right)\right)$$
43	41 42	ax-mp	$$⊢x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \perp \left(G\cap H\right)\leftrightarrow \left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge \forall y\in \left(G\cap H\right)\left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right){\cdot }_{\mathrm{ih}}y=0\right)$$
44	14 40 43	sylanbrc	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge x\in \mathscr{H}\right)\to x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \perp \left(G\cap H\right)$$
45	17	pjvi	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \left(G\cap H\right)\wedge x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \perp \left(G\cap H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(G\cap H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)$$
46	10 44 45	syl2anc	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge x\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\cap H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)$$
47		id	$$⊢x\in \mathscr{H}\to x\in \mathscr{H}$$
48		hvaddsub12	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge x\in \mathscr{H}\wedge \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)=x{+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)$$
49	11 47 11 48	syl3anc	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)=x{+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)$$
50		hvsubid	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=0_{ℎ}$$
51	11 50	syl	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=0_{ℎ}$$
52	51	oveq2d	$$⊢x\in \mathscr{H}\to x{+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)=x{+}_{ℎ}{0}_{ℎ}$$
53		ax-hvaddid	$$⊢x\in \mathscr{H}\to x{+}_{ℎ}{0}_{ℎ}=x$$
54	49 52 53	3eqtrd	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)=x$$
55	54	fveq2d	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(G\cap H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)\left(x\right)$$
56	55	adantl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge x\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\cap H\right)\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){+}_{ℎ}\left(x{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\right)\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)\left(x\right)$$
57	46 56	eqtr3d	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)\left(x\right)$$
58	57	ralrimiva	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to \forall x\in \mathscr{H}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)\left(x\right)$$
59	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
60	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
61	59 60	hocofi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right):\mathscr{H}⟶\mathscr{H}$$
62	17	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap H\right):\mathscr{H}⟶\mathscr{H}$$
63	61 62	hoeqi	$$⊢\forall x\in \mathscr{H}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)\left(x\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$
64	58 63	sylib	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$