evlextv

Description: Evaluating a variable-extended polynomial is the same as evaluating the polynomial in the original set of variables (in both cases, the additionial variable is ignored). (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	evlextv.q	$⊢ Q = I eval R$
	evlextv.o	$⊢ O = J eval R$
	evlextv.j	$⊢ J = I ∖ \{Y\}$
	evlextv.m	$⊢ M = {Base}_{(J mPoly R)}$
	evlextv.b	$⊢ B = {Base}_{R}$
	evlextv.e	No typesetting found for \|- E = ( I extendVars R ) with typecode \|-
	evlextv.r	$⊢ φ \to R \in CRing$
	evlextv.i	$⊢ φ \to I \in V$
	evlextv.y	$⊢ φ \to Y \in I$
	evlextv.f	$⊢ φ \to F \in M$
	evlextv.a	$⊢ φ \to A : I ⟶ B$
Assertion	evlextv	$⊢ φ \to Q (E (Y) (F)) (A) = O (F) ({A ↾}_{J})$

Proof

Step	Hyp	Ref	Expression
1		evlextv.q	$⊢ Q = I eval R$
2		evlextv.o	$⊢ O = J eval R$
3		evlextv.j	$⊢ J = I ∖ \{Y\}$
4		evlextv.m	$⊢ M = {Base}_{(J mPoly R)}$
5		evlextv.b	$⊢ B = {Base}_{R}$
6		evlextv.e	Could not format E = ( I extendVars R ) : No typesetting found for \|- E = ( I extendVars R ) with typecode \|-
7		evlextv.r	$⊢ φ \to R \in CRing$
8		evlextv.i	$⊢ φ \to I \in V$
9		evlextv.y	$⊢ φ \to Y \in I$
10		evlextv.f	$⊢ φ \to F \in M$
11		evlextv.a	$⊢ φ \to A : I ⟶ B$
12	6	fveq1i	Could not format ( E ` Y ) = ( ( I extendVars R ) ` Y ) : No typesetting found for \|- ( E ` Y ) = ( ( I extendVars R ) ` Y ) with typecode \|-
13	12	fveq1i	Could not format ( ( E ` Y ) ` F ) = ( ( ( I extendVars R ) ` Y ) ` F ) : No typesetting found for \|- ( ( E ` Y ) ` F ) = ( ( ( I extendVars R ) ` Y ) ` F ) with typecode \|-
14	13	fveq1i	Could not format ( ( ( E ` Y ) ` F ) ` c ) = ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) : No typesetting found for \|- ( ( ( E ` Y ) ` F ) ` c ) = ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) with typecode \|-
15	14	a1i	Could not format ( ( ph /\ c e. { h e. ( NN0 ^m I ) \| ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( ( ( E ` Y ) ` F ) ` c ) = ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) ) : No typesetting found for \|- ( ( ph /\ c e. { h e. ( NN0 ^m I ) \| ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( ( ( E ` Y ) ` F ) ` c ) = ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) ) with typecode \|-
16		eqid	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
17		eqid	$⊢ 0_{R} = 0_{R}$
18	8	adantr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to I \in V$
19	7	adantr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to R \in CRing$
20	9	adantr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to Y \in I$
21	10	adantr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to F \in M$
22		breq1	$⊢ h = c \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (c))$
23		ssrab2	$⊢ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\} \subseteq {ℕ_{0}}^{I}$
24	23	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\} \subseteq {ℕ_{0}}^{I}$
25	24	sselda	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to c \in ({ℕ_{0}}^{I})$
26		fveq1	$⊢ h = c \to h (Y) = c (Y)$
27	26	eqeq1d	$⊢ h = c \to (h (Y) = 0 \leftrightarrow c (Y) = 0)$
28	22 27	anbi12d	$⊢ h = c \to (({finSupp}_{0} (h) \land h (Y) = 0) \leftrightarrow ({finSupp}_{0} (c) \land c (Y) = 0))$
29		simpr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}$
30	28 29	elrabrd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to ({finSupp}_{0} (c) \land c (Y) = 0)$
31	30	simpld	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to {finSupp}_{0} (c)$
32	22 25 31	elrabd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
33	16 17 18 19 20 3 4 21 32	extvfvv	Could not format ( ( ph /\ c e. { h e. ( NN0 ^m I ) \| ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) = if ( ( c ` Y ) = 0 , ( F ` ( c \|` J ) ) , ( 0g ` R ) ) ) : No typesetting found for \|- ( ( ph /\ c e. { h e. ( NN0 ^m I ) \| ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) = if ( ( c ` Y ) = 0 , ( F ` ( c \|` J ) ) , ( 0g ` R ) ) ) with typecode \|-
34	30	simprd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to c (Y) = 0$
35	34	iftrued	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to if (c (Y) = 0, F ({c ↾}_{J}), 0_{R}) = F ({c ↾}_{J})$
36	15 33 35	3eqtrd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to E (Y) (F) (c) = F ({c ↾}_{J})$
37		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
38	37 5	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
39		eqid	$⊢ 1_{R} = 1_{R}$
40	37 39	ringidval	$⊢ 1_{R} = 0_{{mulGrp}_{R}}$
41	37	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
42	19 41	syl	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to {mulGrp}_{R} \in CMnd$
43		simpr	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to i \in (I ∖ J)$
44	3	difeq2i	$⊢ I ∖ J = I ∖ (I ∖ \{Y\})$
45	9	snssd	$⊢ φ \to \{Y\} \subseteq I$
46		dfss4	$⊢ \{Y\} \subseteq I \leftrightarrow I ∖ (I ∖ \{Y\}) = \{Y\}$
47	45 46	sylib	$⊢ φ \to I ∖ (I ∖ \{Y\}) = \{Y\}$
48	44 47	eqtrid	$⊢ φ \to I ∖ J = \{Y\}$
49	48	ad2antrr	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to I ∖ J = \{Y\}$
50	43 49	eleqtrd	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to i \in \{Y\}$
51	50	elsnd	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to i = Y$
52	51	fveq2d	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to c (i) = c (Y)$
53	34	adantr	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to c (Y) = 0$
54	52 53	eqtrd	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to c (i) = 0$
55	54	oveq1d	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to c (i) \cdot_{{mulGrp}_{R}} A (i) = 0 \cdot_{{mulGrp}_{R}} A (i)$
56	11	ad2antrr	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to A : I ⟶ B$
57		difssd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to I ∖ J \subseteq I$
58	57	sselda	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to i \in I$
59	56 58	ffvelcdmd	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to A (i) \in B$
60		eqid	$⊢ \cdot_{{mulGrp}_{R}} = \cdot_{{mulGrp}_{R}}$
61	38 40 60	mulg0	$⊢ A (i) \in B \to 0 \cdot_{{mulGrp}_{R}} A (i) = 1_{R}$
62	59 61	syl	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to 0 \cdot_{{mulGrp}_{R}} A (i) = 1_{R}$
63	55 62	eqtrd	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in (I ∖ J)) \to c (i) \cdot_{{mulGrp}_{R}} A (i) = 1_{R}$
64		fvexd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to 1_{R} \in V$
65		0nn0	$⊢ 0 \in ℕ_{0}$
66	65	a1i	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to 0 \in ℕ_{0}$
67	8	adantr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to I \in V$
68		ssidd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to I \subseteq I$
69	11	adantr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to A : I ⟶ B$
70	69	ffvelcdmda	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \to A (i) \in B$
71		nn0ex	$⊢ ℕ_{0} \in V$
72	71	a1i	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to ℕ_{0} \in V$
73		ssrab2	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
74	73	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
75	74	sselda	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to c \in ({ℕ_{0}}^{I})$
76	67 72 75	elmaprd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to c : I ⟶ ℕ_{0}$
77		simpr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
78	22 77	elrabrd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} (c)$
79	38 40 60	mulg0	$⊢ x \in B \to 0 \cdot_{{mulGrp}_{R}} x = 1_{R}$
80	79	adantl	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land x \in B) \to 0 \cdot_{{mulGrp}_{R}} x = 1_{R}$
81	64 66 67 68 70 76 78 80	fisuppov1	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{1_{R}} ((i \in I ⟼ c (i) \cdot_{{mulGrp}_{R}} A (i)))$
82	32 81	syldan	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to {finSupp}_{1_{R}} ((i \in I ⟼ c (i) \cdot_{{mulGrp}_{R}} A (i)))$
83	7 41	syl	$⊢ φ \to {mulGrp}_{R} \in CMnd$
84	83	adantr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {mulGrp}_{R} \in CMnd$
85	84	cmnmndd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {mulGrp}_{R} \in Mnd$
86	85	adantr	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \to {mulGrp}_{R} \in Mnd$
87	76	ffvelcdmda	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \to c (i) \in ℕ_{0}$
88	38 60 86 87 70	mulgnn0cld	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \to c (i) \cdot_{{mulGrp}_{R}} A (i) \in B$
89	32 88	syldanl	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in I) \to c (i) \cdot_{{mulGrp}_{R}} A (i) \in B$
90		difss	$⊢ I ∖ \{Y\} \subseteq I$
91	3 90	eqsstri	$⊢ J \subseteq I$
92	91	a1i	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to J \subseteq I$
93	38 40 42 18 63 82 89 92	gsummptfsres	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to \underset{i \in I}{\sum_{{mulGrp}_{R}}} (c (i) \cdot_{{mulGrp}_{R}} A (i)) = \underset{i \in J}{\sum_{{mulGrp}_{R}}} (c (i) \cdot_{{mulGrp}_{R}} A (i))$
94		simpr	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in J) \to i \in J$
95	94	fvresd	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in J) \to ({c ↾}_{J}) (i) = c (i)$
96	94	fvresd	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in J) \to ({A ↾}_{J}) (i) = A (i)$
97	95 96	oveq12d	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in J) \to ({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i) = c (i) \cdot_{{mulGrp}_{R}} A (i)$
98	97	mpteq2dva	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to (i \in J ⟼ ({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)) = (i \in J ⟼ c (i) \cdot_{{mulGrp}_{R}} A (i))$
99	98	oveq2d	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to \underset{i \in J}{\sum_{{mulGrp}_{R}}} (({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)) = \underset{i \in J}{\sum_{{mulGrp}_{R}}} (c (i) \cdot_{{mulGrp}_{R}} A (i))$
100	93 99	eqtr4d	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to \underset{i \in I}{\sum_{{mulGrp}_{R}}} (c (i) \cdot_{{mulGrp}_{R}} A (i)) = \underset{i \in J}{\sum_{{mulGrp}_{R}}} (({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))$
101	36 100	oveq12d	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to E (Y) (F) (c) \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i))) = F ({c ↾}_{J}) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)))$
102	101	mpteq2dva	$⊢ φ \to (c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\} ⟼ E (Y) (F) (c) \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i)))) = (c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\} ⟼ F ({c ↾}_{J}) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))))$
103	102	oveq2d	$⊢ φ \to \underset{c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}}{\sum_{R}} (E (Y) (F) (c) \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i)))) = \underset{c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}}{\sum_{R}} (F ({c ↾}_{J}) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))))$
104	7	crngringd	$⊢ φ \to R \in Ring$
105	104	ringcmnd	$⊢ φ \to R \in CMnd$
106		ovex	$⊢ {ℕ_{0}}^{I} \in V$
107	106	rabex	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V$
108	107	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V$
109	14	a1i	Could not format ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) \| h finSupp 0 } \ { h e. ( NN0 ^m I ) \| ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> ( ( ( E ` Y ) ` F ) ` c ) = ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) ) : No typesetting found for \|- ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) \| h finSupp 0 } \ { h e. ( NN0 ^m I ) \| ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> ( ( ( E ` Y ) ` F ) ` c ) = ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) ) with typecode \|-
110	8	adantr	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to I \in V$
111	7	adantr	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to R \in CRing$
112	9	adantr	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to Y \in I$
113	10	adantr	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to F \in M$
114		difssd	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\} \subseteq \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
115	114	sselda	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
116	16 17 110 111 112 3 4 113 115	extvfvv	Could not format ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) \| h finSupp 0 } \ { h e. ( NN0 ^m I ) \| ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) = if ( ( c ` Y ) = 0 , ( F ` ( c \|` J ) ) , ( 0g ` R ) ) ) : No typesetting found for \|- ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) \| h finSupp 0 } \ { h e. ( NN0 ^m I ) \| ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) = if ( ( c ` Y ) = 0 , ( F ` ( c \|` J ) ) , ( 0g ` R ) ) ) with typecode \|-
117	115	adantr	$⊢ ((φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \land c (Y) = 0) \to c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
118	73 117	sselid	$⊢ ((φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \land c (Y) = 0) \to c \in ({ℕ_{0}}^{I})$
119	22 117	elrabrd	$⊢ ((φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \land c (Y) = 0) \to {finSupp}_{0} (c)$
120		simpr	$⊢ ((φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \land c (Y) = 0) \to c (Y) = 0$
121	119 120	jca	$⊢ ((φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \land c (Y) = 0) \to ({finSupp}_{0} (c) \land c (Y) = 0)$
122	28 118 121	elrabd	$⊢ ((φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \land c (Y) = 0) \to c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}$
123		simplr	$⊢ ((φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \land c (Y) = 0) \to c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})$
124	123	eldifbd	$⊢ ((φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \land c (Y) = 0) \to \neg c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}$
125	122 124	pm2.65da	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to \neg c (Y) = 0$
126	125	iffalsed	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to if (c (Y) = 0, F ({c ↾}_{J}), 0_{R}) = 0_{R}$
127	109 116 126	3eqtrd	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to E (Y) (F) (c) = 0_{R}$
128	127	oveq1d	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to E (Y) (F) (c) \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i))) = 0_{R} \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i)))$
129		eqid	$⊢ \cdot_{R} = \cdot_{R}$
130	104	adantr	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to R \in Ring$
131	88	fmpttd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (i \in I ⟼ c (i) \cdot_{{mulGrp}_{R}} A (i)) : I ⟶ B$
132	38 40 84 67 131 81	gsumcl	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to \underset{i \in I}{\sum_{{mulGrp}_{R}}} (c (i) \cdot_{{mulGrp}_{R}} A (i)) \in B$
133	115 132	syldan	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to \underset{i \in I}{\sum_{{mulGrp}_{R}}} (c (i) \cdot_{{mulGrp}_{R}} A (i)) \in B$
134	5 129 17 130 133	ringlzd	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to 0_{R} \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i))) = 0_{R}$
135	128 134	eqtrd	$⊢ (φ \land c \in (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ∖ \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\})) \to E (Y) (F) (c) \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i))) = 0_{R}$
136		eqid	$⊢ I mPoly R = I mPoly R$
137		eqid	$⊢ {Base}_{(I mPoly R)} = {Base}_{(I mPoly R)}$
138	16	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
139	16 17 8 104 5 3 4 9 10 137	extvfvcl	Could not format ( ph -> ( ( ( I extendVars R ) ` Y ) ` F ) e. ( Base ` ( I mPoly R ) ) ) : No typesetting found for \|- ( ph -> ( ( ( I extendVars R ) ` Y ) ` F ) e. ( Base ` ( I mPoly R ) ) ) with typecode \|-
140	13 139	eqeltrid	$⊢ φ \to E (Y) (F) \in {Base}_{(I mPoly R)}$
141	136 5 137 138 140	mplelf	$⊢ φ \to E (Y) (F) : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ B$
142	136 137 17 140	mplelsfi	$⊢ φ \to {finSupp}_{0_{R}} (E (Y) (F))$
143	5 104 108 132 141 142	rmfsupp2	$⊢ φ \to {finSupp}_{0_{R}} ((c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ E (Y) (F) (c) \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i)))))$
144	104	adantr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to R \in Ring$
145	141	ffvelcdmda	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to E (Y) (F) (c) \in B$
146	5 129 144 145 132	ringcld	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to E (Y) (F) (c) \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i))) \in B$
147		simpl	$⊢ ({finSupp}_{0} (h) \land h (Y) = 0) \to {finSupp}_{0} (h)$
148	147	a1i	$⊢ (φ \land h \in ({ℕ_{0}}^{I})) \to (({finSupp}_{0} (h) \land h (Y) = 0) \to {finSupp}_{0} (h))$
149	148	ss2rabdv	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\} \subseteq \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
150	5 17 105 108 135 143 146 149	gsummptfsres	$⊢ φ \to \underset{c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}}{\sum_{R}} (E (Y) (F) (c) \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i)))) = \underset{c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}}{\sum_{R}} (E (Y) (F) (c) \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i))))$
151		nfcv	$⊢ \underline{Ⅎ} b (F ({c ↾}_{J}) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))))$
152		fveq2	$⊢ b = {c ↾}_{J} \to F (b) = F ({c ↾}_{J})$
153		fveq1	$⊢ b = {c ↾}_{J} \to b (i) = ({c ↾}_{J}) (i)$
154	153	oveq1d	$⊢ b = {c ↾}_{J} \to b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i) = ({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)$
155	154	mpteq2dv	$⊢ b = {c ↾}_{J} \to (i \in J ⟼ b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)) = (i \in J ⟼ ({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))$
156	155	oveq2d	$⊢ b = {c ↾}_{J} \to \underset{i \in J}{\sum_{{mulGrp}_{R}}} (b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)) = \underset{i \in J}{\sum_{{mulGrp}_{R}}} (({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))$
157	152 156	oveq12d	$⊢ b = {c ↾}_{J} \to F (b) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))) = F ({c ↾}_{J}) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)))$
158		ovex	$⊢ {ℕ_{0}}^{J} \in V$
159	158	rabex	$⊢ \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} \in V$
160	159	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} \in V$
161		eqid	$⊢ J mPoly R = J mPoly R$
162		eqid	$⊢ \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
163	162	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{J}) \| h^{-1} [ℕ] \in Fin\}$
164	161 5 4 163 10	mplelf	$⊢ φ \to F : \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} ⟶ B$
165	164	feqmptd	$⊢ φ \to F = (b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} ⟼ F (b))$
166	161 4 17 10	mplelsfi	$⊢ φ \to {finSupp}_{0_{R}} (F)$
167	165 166	eqbrtrrd	$⊢ φ \to {finSupp}_{0_{R}} ((b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} ⟼ F (b)))$
168	104	adantr	$⊢ (φ \land x \in B) \to R \in Ring$
169		simpr	$⊢ (φ \land x \in B) \to x \in B$
170	5 129 17 168 169	ringlzd	$⊢ (φ \land x \in B) \to 0_{R} \cdot_{R} x = 0_{R}$
171	164	ffvelcdmda	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to F (b) \in B$
172	83	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to {mulGrp}_{R} \in CMnd$
173	91	a1i	$⊢ φ \to J \subseteq I$
174	8 173	ssexd	$⊢ φ \to J \in V$
175	174	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to J \in V$
176	172	cmnmndd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to {mulGrp}_{R} \in Mnd$
177	176	adantr	$⊢ ((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land i \in J) \to {mulGrp}_{R} \in Mnd$
178	71	a1i	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to ℕ_{0} \in V$
179		ssrab2	$⊢ \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{J}$
180	179	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{J}$
181	180	sselda	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to b \in ({ℕ_{0}}^{J})$
182	175 178 181	elmaprd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to b : J ⟶ ℕ_{0}$
183	182	ffvelcdmda	$⊢ ((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land i \in J) \to b (i) \in ℕ_{0}$
184	11	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to A : I ⟶ B$
185	91	a1i	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to J \subseteq I$
186	184 185	fssresd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to ({A ↾}_{J}) : J ⟶ B$
187	186	ffvelcdmda	$⊢ ((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land i \in J) \to ({A ↾}_{J}) (i) \in B$
188	38 60 177 183 187	mulgnn0cld	$⊢ ((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land i \in J) \to b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i) \in B$
189	188	fmpttd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to (i \in J ⟼ b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)) : J ⟶ B$
190	182	feqmptd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to b = (i \in J ⟼ b (i))$
191		breq1	$⊢ h = b \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (b))$
192		simpr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
193	191 192	elrabrd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} (b)$
194	190 193	eqbrtrrd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} ((i \in J ⟼ b (i)))$
195	79	adantl	$⊢ ((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land x \in B) \to 0 \cdot_{{mulGrp}_{R}} x = 1_{R}$
196		fvexd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to 1_{R} \in V$
197	194 195 183 187 196	fsuppssov1	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{1_{R}} ((i \in J ⟼ b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)))$
198	38 40 172 175 189 197	gsumcl	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to \underset{i \in J}{\sum_{{mulGrp}_{R}}} (b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)) \in B$
199		fvexd	$⊢ φ \to 0_{R} \in V$
200	167 170 171 198 199	fsuppssov1	$⊢ φ \to {finSupp}_{0_{R}} ((b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} ⟼ F (b) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)))))$
201		ssidd	$⊢ φ \to B \subseteq B$
202	104	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to R \in Ring$
203	5 129 202 171 198	ringcld	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to F (b) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))) \in B$
204		breq1	$⊢ h = {c ↾}_{J} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (({c ↾}_{J})))$
205	25 92	elmapssresd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to {c ↾}_{J} \in ({ℕ_{0}}^{J})$
206	65	a1i	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to 0 \in ℕ_{0}$
207	31 206	fsuppres	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to {finSupp}_{0} (({c ↾}_{J}))$
208	204 205 207	elrabd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to {c ↾}_{J} \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
209		breq1	$⊢ h = b \cup \{⟨Y, 0⟩\} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} ((b \cup \{⟨Y, 0⟩\})))$
210		fveq1	$⊢ h = b \cup \{⟨Y, 0⟩\} \to h (Y) = (b \cup \{⟨Y, 0⟩\}) (Y)$
211	210	eqeq1d	$⊢ h = b \cup \{⟨Y, 0⟩\} \to (h (Y) = 0 \leftrightarrow (b \cup \{⟨Y, 0⟩\}) (Y) = 0)$
212	209 211	anbi12d	$⊢ h = b \cup \{⟨Y, 0⟩\} \to (({finSupp}_{0} (h) \land h (Y) = 0) \leftrightarrow ({finSupp}_{0} ((b \cup \{⟨Y, 0⟩\})) \land (b \cup \{⟨Y, 0⟩\}) (Y) = 0))$
213	8	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to I \in V$
214	3	uneq1i	$⊢ J \cup \{Y\} = (I ∖ \{Y\}) \cup \{Y\}$
215		undifr	$⊢ \{Y\} \subseteq I \leftrightarrow (I ∖ \{Y\}) \cup \{Y\} = I$
216	45 215	sylib	$⊢ φ \to (I ∖ \{Y\}) \cup \{Y\} = I$
217	214 216	eqtrid	$⊢ φ \to J \cup \{Y\} = I$
218	217	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to J \cup \{Y\} = I$
219	65	a1i	$⊢ φ \to 0 \in ℕ_{0}$
220	9 219	fsnd	$⊢ φ \to \{⟨Y, 0⟩\} : \{Y\} ⟶ ℕ_{0}$
221	220	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to \{⟨Y, 0⟩\} : \{Y\} ⟶ ℕ_{0}$
222	3	ineq1i	$⊢ J \cap \{Y\} = (I ∖ \{Y\}) \cap \{Y\}$
223		disjdifr	$⊢ (I ∖ \{Y\}) \cap \{Y\} = \emptyset$
224	222 223	eqtri	$⊢ J \cap \{Y\} = \emptyset$
225	224	a1i	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to J \cap \{Y\} = \emptyset$
226	182 221 225	fun2d	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to (b \cup \{⟨Y, 0⟩\}) : J \cup \{Y\} ⟶ ℕ_{0}$
227	218 226	feq2dd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to (b \cup \{⟨Y, 0⟩\}) : I ⟶ ℕ_{0}$
228	178 213 227	elmapdd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to b \cup \{⟨Y, 0⟩\} \in ({ℕ_{0}}^{I})$
229	9 65	jctir	$⊢ φ \to (Y \in I \land 0 \in ℕ_{0})$
230	229	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to (Y \in I \land 0 \in ℕ_{0})$
231	182	ffund	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to Fun b$
232		neldifsnd	$⊢ φ \to \neg Y \in (I ∖ \{Y\})$
233	3	eleq2i	$⊢ Y \in J \leftrightarrow Y \in (I ∖ \{Y\})$
234	232 233	sylnibr	$⊢ φ \to \neg Y \in J$
235	234	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to \neg Y \in J$
236	182	fdmd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to dom b = J$
237	235 236	neleqtrrd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to \neg Y \in dom b$
238		df-nel	$⊢ Y \notin dom b \leftrightarrow \neg Y \in dom b$
239	237 238	sylibr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to Y \notin dom b$
240	231 239	jca	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to (Fun b \land Y \notin dom b)$
241		funsnfsupp	$⊢ ((Y \in I \land 0 \in ℕ_{0}) \land (Fun b \land Y \notin dom b)) \to ({finSupp}_{0} ((b \cup \{⟨Y, 0⟩\})) \leftrightarrow {finSupp}_{0} (b))$
242	241	biimpar	$⊢ (((Y \in I \land 0 \in ℕ_{0}) \land (Fun b \land Y \notin dom b)) \land {finSupp}_{0} (b)) \to {finSupp}_{0} ((b \cup \{⟨Y, 0⟩\}))$
243	230 240 193 242	syl21anc	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} ((b \cup \{⟨Y, 0⟩\}))$
244	9	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to Y \in I$
245	65	a1i	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to 0 \in ℕ_{0}$
246		fsnunfv	$⊢ (Y \in I \land 0 \in ℕ_{0} \land \neg Y \in dom b) \to (b \cup \{⟨Y, 0⟩\}) (Y) = 0$
247	244 245 237 246	syl3anc	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to (b \cup \{⟨Y, 0⟩\}) (Y) = 0$
248	243 247	jca	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to ({finSupp}_{0} ((b \cup \{⟨Y, 0⟩\})) \land (b \cup \{⟨Y, 0⟩\}) (Y) = 0)$
249	212 228 248	elrabd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to b \cup \{⟨Y, 0⟩\} \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}$
250		simpr	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land b = {c ↾}_{J}) \to b = {c ↾}_{J}$
251	250	uneq1d	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land b = {c ↾}_{J}) \to b \cup \{⟨Y, 0⟩\} = ({c ↾}_{J}) \cup \{⟨Y, 0⟩\}$
252	3	reseq2i	$⊢ {c ↾}_{J} = {c ↾}_{(I ∖ \{Y\})}$
253	252	uneq1i	$⊢ ({c ↾}_{J}) \cup \{⟨Y, 0⟩\} = ({c ↾}_{(I ∖ \{Y\})}) \cup \{⟨Y, 0⟩\}$
254	253	a1i	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land b = {c ↾}_{J}) \to ({c ↾}_{J}) \cup \{⟨Y, 0⟩\} = ({c ↾}_{(I ∖ \{Y\})}) \cup \{⟨Y, 0⟩\}$
255	71	a1i	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to ℕ_{0} \in V$
256	18 255 25	elmaprd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to c : I ⟶ ℕ_{0}$
257	256	ad4ant13	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land b = {c ↾}_{J}) \to c : I ⟶ ℕ_{0}$
258	257	ffnd	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land b = {c ↾}_{J}) \to c Fn I$
259	244	ad2antrr	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land b = {c ↾}_{J}) \to Y \in I$
260	30	ad4ant13	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land b = {c ↾}_{J}) \to ({finSupp}_{0} (c) \land c (Y) = 0)$
261	260	simprd	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land b = {c ↾}_{J}) \to c (Y) = 0$
262		fresunsn	$⊢ (c Fn I \land Y \in I \land c (Y) = 0) \to ({c ↾}_{(I ∖ \{Y\})}) \cup \{⟨Y, 0⟩\} = c$
263	258 259 261 262	syl3anc	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land b = {c ↾}_{J}) \to ({c ↾}_{(I ∖ \{Y\})}) \cup \{⟨Y, 0⟩\} = c$
264	251 254 263	3eqtrrd	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land b = {c ↾}_{J}) \to c = b \cup \{⟨Y, 0⟩\}$
265		simpr	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land c = b \cup \{⟨Y, 0⟩\}) \to c = b \cup \{⟨Y, 0⟩\}$
266	265	reseq1d	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land c = b \cup \{⟨Y, 0⟩\}) \to {c ↾}_{J} = {(b \cup \{⟨Y, 0⟩\}) ↾}_{J}$
267	182	ad2antrr	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land c = b \cup \{⟨Y, 0⟩\}) \to b : J ⟶ ℕ_{0}$
268	267	ffnd	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land c = b \cup \{⟨Y, 0⟩\}) \to b Fn J$
269	235	ad2antrr	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land c = b \cup \{⟨Y, 0⟩\}) \to \neg Y \in J$
270		fsnunres	$⊢ (b Fn J \land \neg Y \in J) \to {(b \cup \{⟨Y, 0⟩\}) ↾}_{J} = b$
271	268 269 270	syl2anc	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land c = b \cup \{⟨Y, 0⟩\}) \to {(b \cup \{⟨Y, 0⟩\}) ↾}_{J} = b$
272	266 271	eqtr2d	$⊢ (((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land c = b \cup \{⟨Y, 0⟩\}) \to b = {c ↾}_{J}$
273	264 272	impbida	$⊢ ((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to (b = {c ↾}_{J} \leftrightarrow c = b \cup \{⟨Y, 0⟩\})$
274	249 273	reu6dv	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to \exists! c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\} b = {c ↾}_{J}$
275	151 5 17 157 105 160 200 201 203 208 274	gsummptfsf1o	$⊢ φ \to \underset{b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}}{\sum_{R}} (F (b) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)))) = \underset{c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}}{\sum_{R}} (F ({c ↾}_{J}) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))))$
276	103 150 275	3eqtr4d	$⊢ φ \to \underset{c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}}{\sum_{R}} (E (Y) (F) (c) \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i)))) = \underset{b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}}{\sum_{R}} (F (b) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))))$
277	1 5	evlval	$⊢ Q = (I evalSub R) (B)$
278		eqid	$⊢ I mPoly (R ↾_{𝑠} B) = I mPoly (R ↾_{𝑠} B)$
279		eqid	$⊢ {Base}_{(I mPoly (R ↾_{𝑠} B))} = {Base}_{(I mPoly (R ↾_{𝑠} B))}$
280		eqid	$⊢ R ↾_{𝑠} B = R ↾_{𝑠} B$
281	5	subrgid	$⊢ R \in Ring \to B \in SubRing (R)$
282	104 281	syl	$⊢ φ \to B \in SubRing (R)$
283	5	ressid	$⊢ R \in CRing \to R ↾_{𝑠} B = R$
284	7 283	syl	$⊢ φ \to R ↾_{𝑠} B = R$
285	284	oveq2d	$⊢ φ \to I mPoly (R ↾_{𝑠} B) = I mPoly R$
286	285	fveq2d	$⊢ φ \to {Base}_{(I mPoly (R ↾_{𝑠} B))} = {Base}_{(I mPoly R)}$
287	140 286	eleqtrrd	$⊢ φ \to E (Y) (F) \in {Base}_{(I mPoly (R ↾_{𝑠} B))}$
288	5	fvexi	$⊢ B \in V$
289	288	a1i	$⊢ φ \to B \in V$
290	289 8 11	elmapdd	$⊢ φ \to A \in (B^{I})$
291	277 278 279 280 138 5 37 60 129 8 7 282 287 290	evlsvvval	$⊢ φ \to Q (E (Y) (F)) (A) = \underset{c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}}{\sum_{R}} (E (Y) (F) (c) \cdot_{R} (\underset{i \in I}{\sum_{{mulGrp}_{R}}}, (c (i) \cdot_{{mulGrp}_{R}} A (i))))$
292	2 5	evlval	$⊢ O = (J evalSub R) (B)$
293		eqid	$⊢ J mPoly (R ↾_{𝑠} B) = J mPoly (R ↾_{𝑠} B)$
294		eqid	$⊢ {Base}_{(J mPoly (R ↾_{𝑠} B))} = {Base}_{(J mPoly (R ↾_{𝑠} B))}$
295	10 4	eleqtrdi	$⊢ φ \to F \in {Base}_{(J mPoly R)}$
296	284	oveq2d	$⊢ φ \to J mPoly (R ↾_{𝑠} B) = J mPoly R$
297	296	fveq2d	$⊢ φ \to {Base}_{(J mPoly (R ↾_{𝑠} B))} = {Base}_{(J mPoly R)}$
298	295 297	eleqtrrd	$⊢ φ \to F \in {Base}_{(J mPoly (R ↾_{𝑠} B))}$
299	290 173	elmapssresd	$⊢ φ \to {A ↾}_{J} \in (B^{J})$
300	292 293 294 280 163 5 37 60 129 174 7 282 298 299	evlsvvval	$⊢ φ \to O (F) ({A ↾}_{J}) = \underset{b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}}{\sum_{R}} (F (b) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))))$
301	276 291 300	3eqtr4d	$⊢ φ \to Q (E (Y) (F)) (A) = O (F) ({A ↾}_{J})$

Metamath Proof Explorer

Theorem evlextv

Proof