pf1rcl

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

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

Proof

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

Metamath Proof Explorer

Theorem pf1rcl

Proof