mpfrcl

Description: Reverse closure for the set of polynomial functions. (Contributed by Stefan O'Rear, 19-Mar-2015)

		Ref	Expression
	Hypothesis	mpfrcl.q	$⊢ Q = ran (I evalSub S) (R)$
	Assertion	mpfrcl	$⊢ X \in Q \to (I \in V \land S \in CRing \land R \in SubRing (S))$

Proof

Step	Hyp	Ref	Expression
1		mpfrcl.q	$⊢ Q = ran (I evalSub S) (R)$
2		ne0i	$⊢ X \in ran (I evalSub S) (R) \to ran (I evalSub S) (R) \neq \emptyset$
3	2 1	eleq2s	$⊢ X \in Q \to ran (I evalSub S) (R) \neq \emptyset$
4		rneq	$⊢ (I evalSub S) (R) = \emptyset \to ran (I evalSub S) (R) = ran \emptyset$
5		rn0	$⊢ ran \emptyset = \emptyset$
6	4 5	eqtrdi	$⊢ (I evalSub S) (R) = \emptyset \to ran (I evalSub S) (R) = \emptyset$
7	6	necon3i	$⊢ ran (I evalSub S) (R) \neq \emptyset \to (I evalSub S) (R) \neq \emptyset$
8		fveq1	$⊢ I evalSub S = \emptyset \to (I evalSub S) (R) = \emptyset (R)$
9		0fv	$⊢ \emptyset (R) = \emptyset$
10	8 9	eqtrdi	$⊢ I evalSub S = \emptyset \to (I evalSub S) (R) = \emptyset$
11	10	necon3i	$⊢ (I evalSub S) (R) \neq \emptyset \to I evalSub S \neq \emptyset$
12		reldmevls	$⊢ Rel dom evalSub$
13	12	ovprc1	$⊢ \neg I \in V \to I evalSub S = \emptyset$
14	13	necon1ai	$⊢ I evalSub S \neq \emptyset \to I \in V$
15		n0	$⊢ I evalSub S \neq \emptyset \leftrightarrow \exists a a \in (I evalSub S)$
16		df-evls	$⊢ evalSub = (i \in V, s \in CRing ⟼ ⦋ {Base}_{s} / b ⦌ (r \in SubRing (s) ⟼ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))))$
17	16	elmpocl2	$⊢ a \in (I evalSub S) \to S \in CRing$
18	17	a1d	$⊢ a \in (I evalSub S) \to (I \in V \to S \in CRing)$
19	18	exlimiv	$⊢ \exists a a \in (I evalSub S) \to (I \in V \to S \in CRing)$
20	15 19	sylbi	$⊢ I evalSub S \neq \emptyset \to (I \in V \to S \in CRing)$
21	14 20	jcai	$⊢ I evalSub S \neq \emptyset \to (I \in V \land S \in CRing)$
22	11 21	syl	$⊢ (I evalSub S) (R) \neq \emptyset \to (I \in V \land S \in CRing)$
23		fvex	$⊢ {Base}_{s} \in V$
24		nfcv	$⊢ \underline{Ⅎ} b SubRing (s)$
25		nfcsb1v	$⊢ \underline{Ⅎ} b ⦋ {Base}_{s} / b ⦌ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))$
26	24 25	nfmpt	$⊢ \underline{Ⅎ} b (r \in SubRing (s) ⟼ ⦋ {Base}_{s} / b ⦌ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))))$
27		csbeq1a	$⊢ b = {Base}_{s} \to ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))) = ⦋ {Base}_{s} / b ⦌ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))$
28	27	mpteq2dv	$⊢ b = {Base}_{s} \to (r \in SubRing (s) ⟼ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))) = (r \in SubRing (s) ⟼ ⦋ {Base}_{s} / b ⦌ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))))$
29	23 26 28	csbief	$⊢ ⦋ {Base}_{s} / b ⦌ (r \in SubRing (s) ⟼ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))) = (r \in SubRing (s) ⟼ ⦋ {Base}_{s} / b ⦌ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))))$
30		fveq2	$⊢ s = S \to SubRing (s) = SubRing (S)$
31	30	adantl	$⊢ (i = I \land s = S) \to SubRing (s) = SubRing (S)$
32		fveq2	$⊢ s = S \to {Base}_{s} = {Base}_{S}$
33	32	adantl	$⊢ (i = I \land s = S) \to {Base}_{s} = {Base}_{S}$
34	33	csbeq1d	$⊢ (i = I \land s = S) \to ⦋ {Base}_{s} / b ⦌ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))) = ⦋ {Base}_{S} / b ⦌ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))$
35		id	$⊢ i = I \to i = I$
36		oveq1	$⊢ s = S \to s ↾_{𝑠} r = S ↾_{𝑠} r$
37	35 36	oveqan12d	$⊢ (i = I \land s = S) \to i mPoly (s ↾_{𝑠} r) = I mPoly (S ↾_{𝑠} r)$
38	37	csbeq1d	$⊢ (i = I \land s = S) \to ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))) = ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))$
39		id	$⊢ s = S \to s = S$
40		oveq2	$⊢ i = I \to b^{i} = b^{I}$
41	39 40	oveqan12rd	$⊢ (i = I \land s = S) \to s ↑_{𝑠} (b^{i}) = S ↑_{𝑠} (b^{I})$
42	41	oveq2d	$⊢ (i = I \land s = S) \to w RingHom (s ↑_{𝑠} (b^{i})) = w RingHom (S ↑_{𝑠} (b^{I}))$
43	40	adantr	$⊢ (i = I \land s = S) \to b^{i} = b^{I}$
44	43	xpeq1d	$⊢ (i = I \land s = S) \to (b^{i}) \times \{x\} = (b^{I}) \times \{x\}$
45	44	mpteq2dv	$⊢ (i = I \land s = S) \to (x \in r ⟼ (b^{i}) \times \{x\}) = (x \in r ⟼ (b^{I}) \times \{x\})$
46	45	eqeq2d	$⊢ (i = I \land s = S) \to (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \leftrightarrow f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}))$
47	35 36	oveqan12d	$⊢ (i = I \land s = S) \to i mVar (s ↾_{𝑠} r) = I mVar (S ↾_{𝑠} r)$
48	47	coeq2d	$⊢ (i = I \land s = S) \to f \circ (i mVar (s ↾_{𝑠} r)) = f \circ (I mVar (S ↾_{𝑠} r))$
49		simpl	$⊢ (i = I \land s = S) \to i = I$
50	43	mpteq1d	$⊢ (i = I \land s = S) \to (g \in (b^{i}) ⟼ g (x)) = (g \in (b^{I}) ⟼ g (x))$
51	49 50	mpteq12dv	$⊢ (i = I \land s = S) \to (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x)))$
52	48 51	eqeq12d	$⊢ (i = I \land s = S) \to (f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))) \leftrightarrow f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x))))$
53	46 52	anbi12d	$⊢ (i = I \land s = S) \to ((f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))) \leftrightarrow (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x)))))$
54	42 53	riotaeqbidv	$⊢ (i = I \land s = S) \to (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))) = (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x)))))$
55	54	csbeq2dv	$⊢ (i = I \land s = S) \to ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))) = ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x)))))$
56	38 55	eqtrd	$⊢ (i = I \land s = S) \to ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))) = ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x)))))$
57	56	csbeq2dv	$⊢ (i = I \land s = S) \to ⦋ {Base}_{S} / b ⦌ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))) = ⦋ {Base}_{S} / b ⦌ ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x)))))$
58	34 57	eqtrd	$⊢ (i = I \land s = S) \to ⦋ {Base}_{s} / b ⦌ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x))))) = ⦋ {Base}_{S} / b ⦌ ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x)))))$
59	31 58	mpteq12dv	$⊢ (i = I \land s = S) \to (r \in SubRing (s) ⟼ ⦋ {Base}_{s} / b ⦌ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))) = (r \in SubRing (S) ⟼ ⦋ {Base}_{S} / b ⦌ ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x))))))$
60	29 59	syl5eq	$⊢ (i = I \land s = S) \to ⦋ {Base}_{s} / b ⦌ (r \in SubRing (s) ⟼ ⦋ (i mPoly (s ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (s ↑_{𝑠} (b^{i}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{i}) \times \{x\}) \land f \circ (i mVar (s ↾_{𝑠} r)) = (x \in i ⟼ (g \in (b^{i}) ⟼ g (x)))))) = (r \in SubRing (S) ⟼ ⦋ {Base}_{S} / b ⦌ ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x))))))$
61		fvex	$⊢ SubRing (S) \in V$
62	61	mptex	$⊢ (r \in SubRing (S) ⟼ ⦋ {Base}_{S} / b ⦌ ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x)))))) \in V$
63	60 16 62	ovmpoa	$⊢ (I \in V \land S \in CRing) \to I evalSub S = (r \in SubRing (S) ⟼ ⦋ {Base}_{S} / b ⦌ ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x))))))$
64	63	dmeqd	$⊢ (I \in V \land S \in CRing) \to dom (I evalSub S) = dom (r \in SubRing (S) ⟼ ⦋ {Base}_{S} / b ⦌ ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x))))))$
65		eqid	$⊢ (r \in SubRing (S) ⟼ ⦋ {Base}_{S} / b ⦌ ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x)))))) = (r \in SubRing (S) ⟼ ⦋ {Base}_{S} / b ⦌ ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x))))))$
66	65	dmmptss	$⊢ dom (r \in SubRing (S) ⟼ ⦋ {Base}_{S} / b ⦌ ⦋ (I mPoly (S ↾_{𝑠} r)) / w ⦌ (ι f \in (w RingHom (S ↑_{𝑠} (b^{I}))) \| (f \circ algSc (w) = (x \in r ⟼ (b^{I}) \times \{x\}) \land f \circ (I mVar (S ↾_{𝑠} r)) = (x \in I ⟼ (g \in (b^{I}) ⟼ g (x)))))) \subseteq SubRing (S)$
67	64 66	eqsstrdi	$⊢ (I \in V \land S \in CRing) \to dom (I evalSub S) \subseteq SubRing (S)$
68	67	ssneld	$⊢ (I \in V \land S \in CRing) \to (\neg R \in SubRing (S) \to \neg R \in dom (I evalSub S))$
69		ndmfv	$⊢ \neg R \in dom (I evalSub S) \to (I evalSub S) (R) = \emptyset$
70	68 69	syl6	$⊢ (I \in V \land S \in CRing) \to (\neg R \in SubRing (S) \to (I evalSub S) (R) = \emptyset)$
71	70	necon1ad	$⊢ (I \in V \land S \in CRing) \to ((I evalSub S) (R) \neq \emptyset \to R \in SubRing (S))$
72	71	com12	$⊢ (I evalSub S) (R) \neq \emptyset \to ((I \in V \land S \in CRing) \to R \in SubRing (S))$
73	22 72	jcai	$⊢ (I evalSub S) (R) \neq \emptyset \to ((I \in V \land S \in CRing) \land R \in SubRing (S))$
74		df-3an	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \leftrightarrow ((I \in V \land S \in CRing) \land R \in SubRing (S))$
75	73 74	sylibr	$⊢ (I evalSub S) (R) \neq \emptyset \to (I \in V \land S \in CRing \land R \in SubRing (S))$
76	3 7 75	3syl	$⊢ X \in Q \to (I \in V \land S \in CRing \land R \in SubRing (S))$

Metamath Proof Explorer

Theorem mpfrcl

Proof