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

Proof

Step Hyp Ref Expression
1 pjco.1 ⊢ 𝐺 ∈ Cℋ
2 pjco.2 ⊢ 𝐻 ∈ Cℋ
3 2 1 pjcoi ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
4 3 adantl ⊢ ( ( 𝐺 ⊆ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
5 1 pjcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐺 )
6 ssel2 ⊢ ( ( 𝐺 ⊆ 𝐻 ∧ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐺 ) → ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐻 )
7 5 6 sylan2 ⊢ ( ( 𝐺 ⊆ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐻 )
8 pjid ⊢ ( ( 𝐻 ∈ Cℋ ∧ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐻 ) → ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) )
9 2 7 8 sylancr ⊢ ( ( 𝐺 ⊆ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) )
10 4 9 eqtrd ⊢ ( ( 𝐺 ⊆ 𝐻 ∧ 𝑥 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) )
11 10 ralrimiva ⊢ ( 𝐺 ⊆ 𝐻 → ∀ 𝑥 ∈ ℋ ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) )
12 2 pjfi ⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
13 1 pjfi ⊢ ( projℎ ‘ 𝐺 ) : ℋ ⟶ ℋ
14 12 13 hocofi ⊢ ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) : ℋ ⟶ ℋ
15 14 13 hoeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ↔ ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ 𝐺 ) )
16 11 15 sylib ⊢ ( 𝐺 ⊆ 𝐻 → ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ 𝐺 ) )
17 rneq ⊢ ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ 𝐺 ) → ran ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) = ran ( projℎ ‘ 𝐺 ) )
18 rncoss ⊢ ran ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ⊆ ran ( projℎ ‘ 𝐻 )
19 17 18 eqsstrrdi ⊢ ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ 𝐺 ) → ran ( projℎ ‘ 𝐺 ) ⊆ ran ( projℎ ‘ 𝐻 ) )
20 1 pjrni ⊢ ran ( projℎ ‘ 𝐺 ) = 𝐺
21 2 pjrni ⊢ ran ( projℎ ‘ 𝐻 ) = 𝐻
22 19 20 21 3sstr3g ⊢ ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ 𝐺 ) → 𝐺 ⊆ 𝐻 )
23 16 22 impbii ⊢ ( 𝐺 ⊆ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ 𝐺 ) )