# 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 ${⊢}{Q}=\mathrm{ran}\left({S}{\mathrm{evalSub}}_{1}{R}\right)$
Assertion ply1frcl ${⊢}{X}\in {Q}\to \left({S}\in \mathrm{V}\wedge {R}\in 𝒫{\mathrm{Base}}_{{S}}\right)$

### Proof

Step Hyp Ref Expression
1 ply1frcl.q ${⊢}{Q}=\mathrm{ran}\left({S}{\mathrm{evalSub}}_{1}{R}\right)$
2 ne0i ${⊢}{X}\in \mathrm{ran}\left({S}{\mathrm{evalSub}}_{1}{R}\right)\to \mathrm{ran}\left({S}{\mathrm{evalSub}}_{1}{R}\right)\ne \varnothing$
3 2 1 eleq2s ${⊢}{X}\in {Q}\to \mathrm{ran}\left({S}{\mathrm{evalSub}}_{1}{R}\right)\ne \varnothing$
4 rneq ${⊢}{S}{\mathrm{evalSub}}_{1}{R}=\varnothing \to \mathrm{ran}\left({S}{\mathrm{evalSub}}_{1}{R}\right)=\mathrm{ran}\varnothing$
5 rn0 ${⊢}\mathrm{ran}\varnothing =\varnothing$
6 4 5 syl6eq ${⊢}{S}{\mathrm{evalSub}}_{1}{R}=\varnothing \to \mathrm{ran}\left({S}{\mathrm{evalSub}}_{1}{R}\right)=\varnothing$
7 6 necon3i ${⊢}\mathrm{ran}\left({S}{\mathrm{evalSub}}_{1}{R}\right)\ne \varnothing \to {S}{\mathrm{evalSub}}_{1}{R}\ne \varnothing$
8 n0 ${⊢}{S}{\mathrm{evalSub}}_{1}{R}\ne \varnothing ↔\exists {e}\phantom{\rule{.4em}{0ex}}{e}\in \left({S}{\mathrm{evalSub}}_{1}{R}\right)$
9 df-evls1
10 9 dmmpossx ${⊢}\mathrm{dom}{\mathrm{evalSub}}_{1}\subseteq \bigcup _{{s}\in \mathrm{V}}\left(\left\{{s}\right\}×𝒫{\mathrm{Base}}_{{s}}\right)$
11 elfvdm ${⊢}{e}\in {\mathrm{evalSub}}_{1}\left(⟨{S},{R}⟩\right)\to ⟨{S},{R}⟩\in \mathrm{dom}{\mathrm{evalSub}}_{1}$
12 df-ov ${⊢}{S}{\mathrm{evalSub}}_{1}{R}={\mathrm{evalSub}}_{1}\left(⟨{S},{R}⟩\right)$
13 11 12 eleq2s ${⊢}{e}\in \left({S}{\mathrm{evalSub}}_{1}{R}\right)\to ⟨{S},{R}⟩\in \mathrm{dom}{\mathrm{evalSub}}_{1}$
14 10 13 sseldi ${⊢}{e}\in \left({S}{\mathrm{evalSub}}_{1}{R}\right)\to ⟨{S},{R}⟩\in \bigcup _{{s}\in \mathrm{V}}\left(\left\{{s}\right\}×𝒫{\mathrm{Base}}_{{s}}\right)$
15 fveq2 ${⊢}{s}={S}\to {\mathrm{Base}}_{{s}}={\mathrm{Base}}_{{S}}$
16 15 pweqd ${⊢}{s}={S}\to 𝒫{\mathrm{Base}}_{{s}}=𝒫{\mathrm{Base}}_{{S}}$
17 16 opeliunxp2 ${⊢}⟨{S},{R}⟩\in \bigcup _{{s}\in \mathrm{V}}\left(\left\{{s}\right\}×𝒫{\mathrm{Base}}_{{s}}\right)↔\left({S}\in \mathrm{V}\wedge {R}\in 𝒫{\mathrm{Base}}_{{S}}\right)$
18 14 17 sylib ${⊢}{e}\in \left({S}{\mathrm{evalSub}}_{1}{R}\right)\to \left({S}\in \mathrm{V}\wedge {R}\in 𝒫{\mathrm{Base}}_{{S}}\right)$
19 18 exlimiv ${⊢}\exists {e}\phantom{\rule{.4em}{0ex}}{e}\in \left({S}{\mathrm{evalSub}}_{1}{R}\right)\to \left({S}\in \mathrm{V}\wedge {R}\in 𝒫{\mathrm{Base}}_{{S}}\right)$
20 8 19 sylbi ${⊢}{S}{\mathrm{evalSub}}_{1}{R}\ne \varnothing \to \left({S}\in \mathrm{V}\wedge {R}\in 𝒫{\mathrm{Base}}_{{S}}\right)$
21 3 7 20 3syl ${⊢}{X}\in {Q}\to \left({S}\in \mathrm{V}\wedge {R}\in 𝒫{\mathrm{Base}}_{{S}}\right)$