Metamath Proof Explorer

Theorem pjss2coi

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

Ref Expression
Hypotheses pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjss2coi ${⊢}{G}\subseteq {H}↔{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\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 1 2 pjcoi ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)$
4 3 adantl ${⊢}\left({G}\subseteq {H}\wedge {x}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)$
5 2fveq3 ${⊢}{x}=if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\right)\right)$
6 fveq2 ${⊢}{x}=if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\right)$
7 5 6 eqeq12d ${⊢}{x}=if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)↔{\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\right)\right)$
8 7 imbi2d ${⊢}{x}=if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\to \left(\left({G}\subseteq {H}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)\right)↔\left({G}\subseteq {H}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\right)\right)\right)$
9 ifhvhv0 ${⊢}if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\in ℋ$
10 1 9 2 pjss2i ${⊢}{G}\subseteq {H}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left(if\left({x}\in ℋ,{x},{0}_{ℎ}\right)\right)$
11 8 10 dedth ${⊢}{x}\in ℋ\to \left({G}\subseteq {H}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)\right)$
12 11 impcom ${⊢}\left({G}\subseteq {H}\wedge {x}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({x}\right)\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)$
13 4 12 eqtrd ${⊢}\left({G}\subseteq {H}\wedge {x}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)$
14 13 ralrimiva ${⊢}{G}\subseteq {H}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)$
15 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ$
16 2 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
17 15 16 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right):ℋ⟶ℋ$
18 17 15 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)↔{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)$
19 14 18 sylib ${⊢}{G}\subseteq {H}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)$
20 fveq1 ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({y}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({y}\right)$
21 20 oveq2d ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\to {x}{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({y}\right)$
22 21 ad2antlr ${⊢}\left(\left({x}\in ℋ\wedge {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\right)\wedge {y}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({y}\right)$
23 2 1 pjadjcoi ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({y}\right)$
24 23 adantlr ${⊢}\left(\left({x}\in ℋ\wedge {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\right)\wedge {y}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({y}\right)$
25 1 pjadji ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({y}\right)$
26 25 adantlr ${⊢}\left(\left({x}\in ℋ\wedge {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\right)\wedge {y}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({y}\right)$
27 22 24 26 3eqtr4d ${⊢}\left(\left({x}\in ℋ\wedge {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\right)\wedge {y}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
28 27 exp31 ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\to \left({y}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right)$
29 28 ralrimdv ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\to \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
30 2 1 pjcohcli ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)\in ℋ$
31 1 pjhcli ${⊢}{x}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)\in ℋ$
32 hial2eq ${⊢}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)\in ℋ\wedge {\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)\in ℋ\right)\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)\right)$
33 30 31 32 syl2anc ${⊢}{x}\in ℋ\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({x}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({x}\right)\right)$
34 29 33 sylibd ${⊢}{x}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\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)\right)$
35 34 com12 ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\to \left({x}\in ℋ\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)\right)$
36 35 ralrimiv ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\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)$
37 16 15 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right):ℋ⟶ℋ$
38 37 15 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)$
39 36 38 sylib ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)$
40 1 2 pjss1coi ${⊢}{G}\subseteq {H}↔{\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)$
41 39 40 sylibr ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\to {G}\subseteq {H}$
42 19 41 impbii ${⊢}{G}\subseteq {H}↔{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)$