This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1frcl

Description: Reverse closure for the set of univariate polynomial functions. (Contributed by AV, 9-Sep-2019)

Ref Expression
Hypothesis ply1frcl.q ⊢ 𝑄 = ran ( 𝑆 evalSub1 𝑅 )
Assertion ply1frcl ( 𝑋 ∈ 𝑄 → ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 ply1frcl.q ⊢ 𝑄 = ran ( 𝑆 evalSub1 𝑅 )
2 ne0i ⊢ ( 𝑋 ∈ ran ( 𝑆 evalSub1 𝑅 ) → ran ( 𝑆 evalSub1 𝑅 ) ≠ ∅ )
3 2 1 eleq2s ⊢ ( 𝑋 ∈ 𝑄 → ran ( 𝑆 evalSub1 𝑅 ) ≠ ∅ )
4 rneq ⊢ ( ( 𝑆 evalSub1 𝑅 ) = ∅ → ran ( 𝑆 evalSub1 𝑅 ) = ran ∅ )
5 rn0 ⊢ ran ∅ = ∅
6 4 5 eqtrdi ⊢ ( ( 𝑆 evalSub1 𝑅 ) = ∅ → ran ( 𝑆 evalSub1 𝑅 ) = ∅ )
7 6 necon3i ⊢ ( ran ( 𝑆 evalSub1 𝑅 ) ≠ ∅ → ( 𝑆 evalSub1 𝑅 ) ≠ ∅ )
8 n0 ⊢ ( ( 𝑆 evalSub1 𝑅 ) ≠ ∅ ↔ ∃ 𝑒 𝑒 ∈ ( 𝑆 evalSub1 𝑅 ) )
9 df-evls1 ⊢ evalSub1 = ( 𝑠 ∈ V , 𝑟 ∈ 𝒫 ( Base ‘ 𝑠 ) ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) )
10 9 dmmpossx ⊢ dom evalSub1 ⊆ ∪ 𝑠 ∈ V ( { 𝑠 } × 𝒫 ( Base ‘ 𝑠 ) )
11 elfvdm ⊢ ( 𝑒 ∈ ( evalSub1 ‘ ⟨ 𝑆 , 𝑅 ⟩ ) → ⟨ 𝑆 , 𝑅 ⟩ ∈ dom evalSub1 )
12 df-ov ⊢ ( 𝑆 evalSub1 𝑅 ) = ( evalSub1 ‘ ⟨ 𝑆 , 𝑅 ⟩ )
13 11 12 eleq2s ⊢ ( 𝑒 ∈ ( 𝑆 evalSub1 𝑅 ) → ⟨ 𝑆 , 𝑅 ⟩ ∈ dom evalSub1 )
14 10 13 sselid ⊢ ( 𝑒 ∈ ( 𝑆 evalSub1 𝑅 ) → ⟨ 𝑆 , 𝑅 ⟩ ∈ ∪ 𝑠 ∈ V ( { 𝑠 } × 𝒫 ( Base ‘ 𝑠 ) ) )
15 fveq2 ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
16 15 pweqd ⊢ ( 𝑠 = 𝑆 → 𝒫 ( Base ‘ 𝑠 ) = 𝒫 ( Base ‘ 𝑆 ) )
17 16 opeliunxp2 ⊢ ( ⟨ 𝑆 , 𝑅 ⟩ ∈ ∪ 𝑠 ∈ V ( { 𝑠 } × 𝒫 ( Base ‘ 𝑠 ) ) ↔ ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )
18 14 17 sylib ⊢ ( 𝑒 ∈ ( 𝑆 evalSub1 𝑅 ) → ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )
19 18 exlimiv ⊢ ( ∃ 𝑒 𝑒 ∈ ( 𝑆 evalSub1 𝑅 ) → ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )
20 8 19 sylbi ⊢ ( ( 𝑆 evalSub1 𝑅 ) ≠ ∅ → ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )
21 3 7 20 3syl ⊢ ( 𝑋 ∈ 𝑄 → ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )