# 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 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjclem1.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
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}}_{ℋ}$
2 pjclem1.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 1 2 pjcocli ${⊢}{x}\in ℋ\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 ℋ\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 ℋ\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}↔\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 ℋ\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 ℋ\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 ℋ\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 ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ$
12 hvsubcl ${⊢}\left({x}\in ℋ\wedge \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ\right)\to {x}{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ$
13 11 12 mpdan ${⊢}{x}\in ℋ\to {x}{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ$
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 ℋ\right)\to {x}{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ$
15 simpl ${⊢}\left({x}\in ℋ\wedge {y}\in \left({G}\cap {H}\right)\right)\to {x}\in ℋ$
16 11 adantr ${⊢}\left({x}\in ℋ\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 ℋ$
17 1 2 chincli ${⊢}{G}\cap {H}\in {\mathbf{C}}_{ℋ}$
18 17 cheli ${⊢}{y}\in \left({G}\cap {H}\right)\to {y}\in ℋ$
19 18 adantl ${⊢}\left({x}\in ℋ\wedge {y}\in \left({G}\cap {H}\right)\right)\to {y}\in ℋ$
20 15 16 19 3jca ${⊢}\left({x}\in ℋ\wedge {y}\in \left({G}\cap {H}\right)\right)\to \left({x}\in ℋ\wedge \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ\wedge {y}\in ℋ\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 ℋ\wedge {y}\in \left({G}\cap {H}\right)\right)\right)\to \left({x}\in ℋ\wedge \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ\wedge {y}\in ℋ\right)$
22 his2sub ${⊢}\left({x}\in ℋ\wedge \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ\wedge {y}\in ℋ\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 ℋ\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 ℋ\wedge {y}\in ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\wedge {y}\in ℋ\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 ℋ\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 ℋ\wedge {y}\in ℋ\right)$
35 hicl ${⊢}\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ\wedge {y}\in ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\right)\to \forall {y}\in \left({G}\cap {H}\right)\phantom{\rule{.4em}{0ex}}\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}}_{ℋ}$
42 shocel ${⊢}{G}\cap {H}\in {\mathbf{S}}_{ℋ}\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)↔\left({x}{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ\wedge \forall {y}\in \left({G}\cap {H}\right)\phantom{\rule{.4em}{0ex}}\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)↔\left({x}{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ\wedge \forall {y}\in \left({G}\cap {H}\right)\phantom{\rule{.4em}{0ex}}\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 ℋ\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 ℋ\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 ℋ\to {x}\in ℋ$
48 hvaddsub12 ${⊢}\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ\wedge {x}\in ℋ\wedge \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)\in ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\to {x}{+}_{ℎ}{0}_{ℎ}={x}$
54 49 52 53 3eqtrd ${⊢}{x}\in ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}\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):ℋ⟶ℋ$
60 2 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
61 59 60 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right):ℋ⟶ℋ$
62 17 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right):ℋ⟶ℋ$
63 61 62 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\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)↔{\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)$