# 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𝐺 ) )
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "http://metamath.tirix.org/mpeuni/pjss1coi", "fetch_time": 1719319505000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2024-26/segments/1718198865972.21/warc/CC-MAIN-20240625104040-20240625134040-00702.warc.gz", "warc_record_offset": 17667339, "warc_record_length": 2599, "token_count": 1084, "char_count": 1809, "score": 3.59375, "int_score": 4, "crawl": "CC-MAIN-2024-26", "snapshot_type": "latest", "language": "en", "language_score": 0.3939107656478882, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00001-of-00064.parquet"}