# Metamath Proof Explorer

## 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}}_{ℋ}$
pjadj2co.2 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjadj2co.3 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
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}}_{ℋ}$
2 pjadj2co.2 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
3 pjadj2co.3 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
4 1 2 3 pj2cocli ${⊢}{x}\in ℋ\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 ℋ\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):ℋ⟶ℋ$
7 2 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ$
8 6 7 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right):ℋ⟶ℋ$
9 3 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
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ℋ$
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ℋ\wedge {x}\in ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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}↔\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ$
26 hvsubcl ${⊢}\left({x}\in ℋ\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 ℋ\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 ℋ$
27 25 26 mpdan ${⊢}{x}\in ℋ\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 ℋ$
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 ℋ\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 ℋ$
29 simpl ${⊢}\left({x}\in ℋ\wedge {y}\in \left(\left({F}\cap {G}\right)\cap {H}\right)\right)\to {x}\in ℋ$
30 25 adantr ${⊢}\left({x}\in ℋ\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 ℋ$
31 1 2 chincli ${⊢}{F}\cap {G}\in {\mathbf{C}}_{ℋ}$
32 31 3 chincli ${⊢}\left({F}\cap {G}\right)\cap {H}\in {\mathbf{C}}_{ℋ}$
33 32 cheli ${⊢}{y}\in \left(\left({F}\cap {G}\right)\cap {H}\right)\to {y}\in ℋ$
34 33 adantl ${⊢}\left({x}\in ℋ\wedge {y}\in \left(\left({F}\cap {G}\right)\cap {H}\right)\right)\to {y}\in ℋ$
35 29 30 34 3jca ${⊢}\left({x}\in ℋ\wedge {y}\in \left(\left({F}\cap {G}\right)\cap {H}\right)\right)\to \left({x}\in ℋ\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 ℋ\wedge {y}\in ℋ\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 ℋ\wedge {y}\in \left(\left({F}\cap {G}\right)\cap {H}\right)\right)\right)\to \left({x}\in ℋ\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 ℋ\wedge {y}\in ℋ\right)$
37 his2sub ${⊢}\left({x}\in ℋ\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 ℋ\wedge {y}\in ℋ\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 ℋ\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 ℋ\wedge {y}\in ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\wedge {y}\in ℋ\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 ℋ\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 ℋ\wedge {y}\in ℋ\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 ℋ\wedge {y}\in ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\right)\to \forall {y}\in \left(\left({F}\cap {G}\right)\cap {H}\right)\phantom{\rule{.4em}{0ex}}\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}}_{ℋ}$
58 shocel ${⊢}\left({F}\cap {G}\right)\cap {H}\in {\mathbf{S}}_{ℋ}\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)↔\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 ℋ\wedge \forall {y}\in \left(\left({F}\cap {G}\right)\cap {H}\right)\phantom{\rule{.4em}{0ex}}\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)↔\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 ℋ\wedge \forall {y}\in \left(\left({F}\cap {G}\right)\cap {H}\right)\phantom{\rule{.4em}{0ex}}\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 ℋ\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 ℋ\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 ℋ\to {x}\in ℋ$
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 ℋ\wedge {x}\in ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\to {x}{+}_{ℎ}{0}_{ℎ}={x}$
70 68 69 eqtrd ${⊢}{x}\in ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}\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):ℋ⟶ℋ$
77 32 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left(\left({F}\cap {G}\right)\cap {H}\right):ℋ⟶ℋ$
78 76 77 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\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)↔\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)$