# Metamath Proof Explorer

## 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}}_{ℋ}$
pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjss1coi ${⊢}{G}\subseteq {H}↔{\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}}_{ℋ}$
2 pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 2 1 pjcoi ${⊢}{x}\in ℋ\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 ℋ\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 ℋ\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 ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)\in {H}$
8 pjid ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\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 ℋ\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 ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}\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):ℋ⟶ℋ$
13 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ$
14 12 13 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right):ℋ⟶ℋ$
15 14 13 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)↔{\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}↔{\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)$