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∈Cℋ
pjco.2 ⊢H∈Cℋ
Assertion pjss2coi ⊢G⊆H↔projℎ⁡G∘projℎ⁡H=projℎ⁡G

Proof

Step Hyp Ref Expression
1 pjco.1 ⊢G∈Cℋ
2 pjco.2 ⊢H∈Cℋ
3 1 2 pjcoi ⊢x∈ℋ→projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡G⁡projℎ⁡H⁡x
4 3 adantl ⊢G⊆H∧x∈ℋ→projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡G⁡projℎ⁡H⁡x
5 2fveq3 ⊢x=ifx∈ℋx0ℎ→projℎ⁡G⁡projℎ⁡H⁡x=projℎ⁡G⁡projℎ⁡H⁡ifx∈ℋx0ℎ
6 fveq2 ⊢x=ifx∈ℋx0ℎ→projℎ⁡G⁡x=projℎ⁡G⁡ifx∈ℋx0ℎ
7 5 6 eqeq12d ⊢x=ifx∈ℋx0ℎ→projℎ⁡G⁡projℎ⁡H⁡x=projℎ⁡G⁡x↔projℎ⁡G⁡projℎ⁡H⁡ifx∈ℋx0ℎ=projℎ⁡G⁡ifx∈ℋx0ℎ
8 7 imbi2d ⊢x=ifx∈ℋx0ℎ→G⊆H→projℎ⁡G⁡projℎ⁡H⁡x=projℎ⁡G⁡x↔G⊆H→projℎ⁡G⁡projℎ⁡H⁡ifx∈ℋx0ℎ=projℎ⁡G⁡ifx∈ℋx0ℎ
9 ifhvhv0 ⊢ifx∈ℋx0ℎ∈ℋ
10 1 9 2 pjss2i ⊢G⊆H→projℎ⁡G⁡projℎ⁡H⁡ifx∈ℋx0ℎ=projℎ⁡G⁡ifx∈ℋx0ℎ
11 8 10 dedth ⊢x∈ℋ→G⊆H→projℎ⁡G⁡projℎ⁡H⁡x=projℎ⁡G⁡x
12 11 impcom ⊢G⊆H∧x∈ℋ→projℎ⁡G⁡projℎ⁡H⁡x=projℎ⁡G⁡x
13 4 12 eqtrd ⊢G⊆H∧x∈ℋ→projℎ⁡G∘projℎ⁡H⁡x=projℎ⁡G⁡x
14 13 ralrimiva ⊢G⊆H→∀x∈ℋprojℎ⁡G∘projℎ⁡H⁡x=projℎ⁡G⁡x
15 1 pjfi ⊢projℎ⁡G:ℋ⟶ℋ
16 2 pjfi ⊢projℎ⁡H:ℋ⟶ℋ
17 15 16 hocofi ⊢projℎ⁡G∘projℎ⁡H:ℋ⟶ℋ
18 17 15 hoeqi ⊢∀x∈ℋprojℎ⁡G∘projℎ⁡H⁡x=projℎ⁡G⁡x↔projℎ⁡G∘projℎ⁡H=projℎ⁡G
19 14 18 sylib ⊢G⊆H→projℎ⁡G∘projℎ⁡H=projℎ⁡G
20 fveq1 ⊢projℎ⁡G∘projℎ⁡H=projℎ⁡G→projℎ⁡G∘projℎ⁡H⁡y=projℎ⁡G⁡y
21 20 oveq2d ⊢projℎ⁡G∘projℎ⁡H=projℎ⁡G→x⋅ihprojℎ⁡G∘projℎ⁡H⁡y=x⋅ihprojℎ⁡G⁡y
22 21 ad2antlr ⊢x∈ℋ∧projℎ⁡G∘projℎ⁡H=projℎ⁡G∧y∈ℋ→x⋅ihprojℎ⁡G∘projℎ⁡H⁡y=x⋅ihprojℎ⁡G⁡y
23 2 1 pjadjcoi ⊢x∈ℋ∧y∈ℋ→projℎ⁡H∘projℎ⁡G⁡x⋅ihy=x⋅ihprojℎ⁡G∘projℎ⁡H⁡y
24 23 adantlr ⊢x∈ℋ∧projℎ⁡G∘projℎ⁡H=projℎ⁡G∧y∈ℋ→projℎ⁡H∘projℎ⁡G⁡x⋅ihy=x⋅ihprojℎ⁡G∘projℎ⁡H⁡y
25 1 pjadji ⊢x∈ℋ∧y∈ℋ→projℎ⁡G⁡x⋅ihy=x⋅ihprojℎ⁡G⁡y
26 25 adantlr ⊢x∈ℋ∧projℎ⁡G∘projℎ⁡H=projℎ⁡G∧y∈ℋ→projℎ⁡G⁡x⋅ihy=x⋅ihprojℎ⁡G⁡y
27 22 24 26 3eqtr4d ⊢x∈ℋ∧projℎ⁡G∘projℎ⁡H=projℎ⁡G∧y∈ℋ→projℎ⁡H∘projℎ⁡G⁡x⋅ihy=projℎ⁡G⁡x⋅ihy
28 27 exp31 ⊢x∈ℋ→projℎ⁡G∘projℎ⁡H=projℎ⁡G→y∈ℋ→projℎ⁡H∘projℎ⁡G⁡x⋅ihy=projℎ⁡G⁡x⋅ihy
29 28 ralrimdv ⊢x∈ℋ→projℎ⁡G∘projℎ⁡H=projℎ⁡G→∀y∈ℋprojℎ⁡H∘projℎ⁡G⁡x⋅ihy=projℎ⁡G⁡x⋅ihy
30 2 1 pjcohcli ⊢x∈ℋ→projℎ⁡H∘projℎ⁡G⁡x∈ℋ
31 1 pjhcli ⊢x∈ℋ→projℎ⁡G⁡x∈ℋ
32 hial2eq ⊢projℎ⁡H∘projℎ⁡G⁡x∈ℋ∧projℎ⁡G⁡x∈ℋ→∀y∈ℋprojℎ⁡H∘projℎ⁡G⁡x⋅ihy=projℎ⁡G⁡x⋅ihy↔projℎ⁡H∘projℎ⁡G⁡x=projℎ⁡G⁡x
33 30 31 32 syl2anc ⊢x∈ℋ→∀y∈ℋprojℎ⁡H∘projℎ⁡G⁡x⋅ihy=projℎ⁡G⁡x⋅ihy↔projℎ⁡H∘projℎ⁡G⁡x=projℎ⁡G⁡x
34 29 33 sylibd ⊢x∈ℋ→projℎ⁡G∘projℎ⁡H=projℎ⁡G→projℎ⁡H∘projℎ⁡G⁡x=projℎ⁡G⁡x
35 34 com12 ⊢projℎ⁡G∘projℎ⁡H=projℎ⁡G→x∈ℋ→projℎ⁡H∘projℎ⁡G⁡x=projℎ⁡G⁡x
36 35 ralrimiv ⊢projℎ⁡G∘projℎ⁡H=projℎ⁡G→∀x∈ℋprojℎ⁡H∘projℎ⁡G⁡x=projℎ⁡G⁡x
37 16 15 hocofi ⊢projℎ⁡H∘projℎ⁡G:ℋ⟶ℋ
38 37 15 hoeqi ⊢∀x∈ℋprojℎ⁡H∘projℎ⁡G⁡x=projℎ⁡G⁡x↔projℎ⁡H∘projℎ⁡G=projℎ⁡G
39 36 38 sylib ⊢projℎ⁡G∘projℎ⁡H=projℎ⁡G→projℎ⁡H∘projℎ⁡G=projℎ⁡G
40 1 2 pjss1coi ⊢G⊆H↔projℎ⁡H∘projℎ⁡G=projℎ⁡G
41 39 40 sylibr ⊢projℎ⁡G∘projℎ⁡H=projℎ⁡G→G⊆H
42 19 41 impbii ⊢G⊆H↔projℎ⁡G∘projℎ⁡H=projℎ⁡G