Theorem pjsslem

Description: Lemma for subset relationships of projections. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjidm.2	$$⊢A\in \mathscr{H}$$
	pjsslem.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjsslem	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjidm.2	$$⊢A\in \mathscr{H}$$
3		pjsslem.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
4		pjo	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
5	1 2 4	mp2an	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
6		pjo	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)$$
7	3 2 6	mp2an	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)$$
8	5 7	oveq12i	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)=\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$
9		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
10	9 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)\in \mathscr{H}$$
11	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
12	3 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathscr{H}$$
13	10 11 10 12	hvsubsub4i	$$⊢\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$
14		hvsubid	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)=0_{ℎ}$$
15	10 14	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)=0_{ℎ}$$
16	15	oveq1i	$$⊢\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(A\right)\right){-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)=0_{ℎ}{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$
17	8 13 16	3eqtri	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)=0_{ℎ}{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$
18	11 12	hvsubcli	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathscr{H}$$
19	18	hv2negi	$$⊢0_{ℎ}{-}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)=-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$
20	11 12	hvnegdii	$$⊢-1{\cdot }_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
21	17 19 20	3eqtri	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$