Theorem pjss1coi

Description: Subset relationship for projections. Theorem 4.5(i)<->(iii) of Beran p. 112. (Contributed by NM, 1-Oct-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjss1coi	$$⊢G\subseteq H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3	2 1	pjcoi	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
4	3	adantl	$$⊢\left(G\subseteq H\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
5	1	pjcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in G$$
6		ssel2	$$⊢\left(G\subseteq H\wedge {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in G\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in H$$
7	5 6	sylan2	$$⊢\left(G\subseteq H\wedge x\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in H$$
8		pjid	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in H\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
9	2 7 8	sylancr	$$⊢\left(G\subseteq H\wedge x\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
10	4 9	eqtrd	$$⊢\left(G\subseteq H\wedge x\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
11	10	ralrimiva	$$⊢G\subseteq H\to \forall x\in \mathscr{H}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
12	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
13	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
14	12 13	hocofi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right):\mathscr{H}⟶\mathscr{H}$$
15	14 13	hoeqi	$$⊢\forall x\in \mathscr{H}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(G\right)$$
16	11 15	sylib	$$⊢G\subseteq H\to {\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(G\right)$$
17		rneq	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(G\right)\to \mathrm{ran}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)=\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)$$
18		rncoss	$$⊢\mathrm{ran}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\subseteq \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)$$
19	17 18	eqsstrrdi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(G\right)\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\subseteq \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)$$
20	1	pjrni	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)=G$$
21	2	pjrni	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)=H$$
22	19 20 21	3sstr3g	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(G\right)\to G\subseteq H$$
23	16 22	impbii	$$⊢G\subseteq H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(G\right)$$