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	eqtrdi	$$⊢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 \leftrightarrow \exists ee\in \left(S{\mathrm{evalSub}}_{1}R\right)$$
9		df-evls1	$$⊢{\mathrm{evalSub}}_1=\left(s\in \mathrm{V},r\in 𝒫{\mathrm{Base}}_s⟼⦋{\mathrm{Base}}_s/b⦌\left(\left(x\in \left(b^{\left(b^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in b⟼1_{𝑜}\times \left\{y\right\}\right)\right)\circ \left(1_{𝑜}\mathrm{evalSub}s\right)\left(r\right)\right)\right)$$
10	9	dmmpossx	$$⊢\mathrm{dom}{\mathrm{evalSub}}_1\subseteq \bigcup _{s\in \mathrm{V}}\left(\left\{s\right\}\times 𝒫{\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	sselid	$$⊢e\in \left(S{\mathrm{evalSub}}_{1}R\right)\to ⟨S,R⟩\in \bigcup _{s\in \mathrm{V}}\left(\left\{s\right\}\times 𝒫{\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\}\times 𝒫{\mathrm{Base}}_s\right)\leftrightarrow \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 ee\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)$$