Theorem pjss2i

Description: Subset relationship for projections. Theorem 4.5(i)->(ii) of Beran p. 112. (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	pjss2i	$$⊢H\subseteq G\to {\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\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	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	4 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)$$
6	1 3	chsscon3i	$$⊢H\subseteq G\leftrightarrow \perp \left(G\right)\subseteq \perp \left(H\right)$$
7	3	choccli	$$⊢\perp \left(G\right)\in {\mathbf{C}}_{\mathscr{H}}$$
8	7 2	pjclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(G\right)$$
9		ssel	$$⊢\perp \left(G\right)\subseteq \perp \left(H\right)\to \left({\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(G\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(H\right)\right)$$
10	8 9	mpi	$$⊢\perp \left(G\right)\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(H\right)$$
11	6 10	sylbi	$$⊢H\subseteq G\to {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(H\right)$$
12	4	chshii	$$⊢\perp \left(H\right)\in {\mathbf{S}}_{\mathscr{H}}$$
13		shsubcl	$$⊢\left(\perp \left(H\right)\in {\mathbf{S}}_{\mathscr{H}}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(H\right)$$
14	12 13	mp3an1	$$⊢\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \perp \left(H\right)\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(H\right)$$
15	5 11 14	sylancr	$$⊢H\subseteq G\to {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(H\right)$$
16	1 2 3	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)$$
17	16	eleq1i	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \perp \left(H\right)$$
18	3 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathscr{H}$$
19	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
20	18 19	hvsubcli	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
21	1 20	pjoc2i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=0_{ℎ}$$
22	17 21	bitri	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=0_{ℎ}$$
23	1 18 19	pjsubii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
24	23	eqeq1i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=0_{ℎ}\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=0_{ℎ}$$
25	1 18	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)\in \mathscr{H}$$
26	1 19	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\in \mathscr{H}$$
27	25 26	hvsubeq0i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=0_{ℎ}\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
28	24 27	bitri	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)=0_{ℎ}\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
29	1 2	pjidmi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
30	29	eqeq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
31	22 28 30	3bitrri	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){-}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\left(A\right)\in \perp \left(H\right)$$
32	15 31	sylibr	$$⊢H\subseteq G\to {\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$