# Metamath Proof Explorer

## Theorem pf1rcl

Description: Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypothesis pf1rcl.q ${⊢}{Q}=\mathrm{ran}{\mathrm{eval}}_{1}\left({R}\right)$
Assertion pf1rcl ${⊢}{X}\in {Q}\to {R}\in \mathrm{CRing}$

### Proof

Step Hyp Ref Expression
1 pf1rcl.q ${⊢}{Q}=\mathrm{ran}{\mathrm{eval}}_{1}\left({R}\right)$
2 n0i ${⊢}{X}\in {Q}\to ¬{Q}=\varnothing$
3 eqid ${⊢}{\mathrm{eval}}_{1}\left({R}\right)={\mathrm{eval}}_{1}\left({R}\right)$
4 eqid ${⊢}{1}_{𝑜}\mathrm{eval}{R}={1}_{𝑜}\mathrm{eval}{R}$
5 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
6 3 4 5 evl1fval ${⊢}{\mathrm{eval}}_{1}\left({R}\right)=\left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ \left({1}_{𝑜}\mathrm{eval}{R}\right)$
7 6 rneqi ${⊢}\mathrm{ran}{\mathrm{eval}}_{1}\left({R}\right)=\mathrm{ran}\left(\left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ \left({1}_{𝑜}\mathrm{eval}{R}\right)\right)$
8 rnco2 ${⊢}\mathrm{ran}\left(\left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\circ \left({1}_{𝑜}\mathrm{eval}{R}\right)\right)=\left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\left[\mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)\right]$
9 1 7 8 3eqtri ${⊢}{Q}=\left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\left[\mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)\right]$
10 inss2 ${⊢}\mathrm{dom}\left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\cap \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)\subseteq \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)$
11 neq0 ${⊢}¬\mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)=\varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)$
12 4 5 evlval ${⊢}{1}_{𝑜}\mathrm{eval}{R}=\left({1}_{𝑜}\mathrm{evalSub}{R}\right)\left({\mathrm{Base}}_{{R}}\right)$
13 12 rneqi ${⊢}\mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)=\mathrm{ran}\left({1}_{𝑜}\mathrm{evalSub}{R}\right)\left({\mathrm{Base}}_{{R}}\right)$
14 13 mpfrcl ${⊢}{x}\in \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)\to \left({1}_{𝑜}\in \mathrm{V}\wedge {R}\in \mathrm{CRing}\wedge {\mathrm{Base}}_{{R}}\in \mathrm{SubRing}\left({R}\right)\right)$
15 14 simp2d ${⊢}{x}\in \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)\to {R}\in \mathrm{CRing}$
16 15 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)\to {R}\in \mathrm{CRing}$
17 11 16 sylbi ${⊢}¬\mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)=\varnothing \to {R}\in \mathrm{CRing}$
18 17 con1i ${⊢}¬{R}\in \mathrm{CRing}\to \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)=\varnothing$
19 sseq0 ${⊢}\left(\mathrm{dom}\left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\cap \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)\subseteq \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)\wedge \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)=\varnothing \right)\to \mathrm{dom}\left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\cap \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)=\varnothing$
20 10 18 19 sylancr ${⊢}¬{R}\in \mathrm{CRing}\to \mathrm{dom}\left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\cap \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)=\varnothing$
21 imadisj ${⊢}\left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\left[\mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)\right]=\varnothing ↔\mathrm{dom}\left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\cap \mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)=\varnothing$
22 20 21 sylibr ${⊢}¬{R}\in \mathrm{CRing}\to \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({{\mathrm{Base}}_{{R}}}^{{1}_{𝑜}}\right)}\right)⟼{x}\circ \left({y}\in {\mathrm{Base}}_{{R}}⟼{1}_{𝑜}×\left\{{y}\right\}\right)\right)\left[\mathrm{ran}\left({1}_{𝑜}\mathrm{eval}{R}\right)\right]=\varnothing$
23 9 22 syl5eq ${⊢}¬{R}\in \mathrm{CRing}\to {Q}=\varnothing$
24 2 23 nsyl2 ${⊢}{X}\in {Q}\to {R}\in \mathrm{CRing}$