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 syl6eq ( ( 𝑆 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 sseldi ( 𝑒 ∈ ( 𝑆 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 ‘ 𝑆 ) ) )