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 ⊢ 𝐺 ∈ Cℋ
pjco.2 ⊢ 𝐻 ∈ Cℋ
Assertion pjss2coi ( 𝐺 ⊆ 𝐻 ↔ ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐺 ) )

Proof

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