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		ssrab2	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
72	71	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
73	72	sselda	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to c \in ({ℕ_{0}}^{I})$
74	73	elmaprd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to c : I ⟶ ℕ_{0}$
75		simpr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
76	22 75	elrabrd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} (c)$
77	38 40 60	mulg0	$⊢ x \in B \to 0 \cdot_{{mulGrp}_{R}} x = 1_{R}$
78	77	adantl	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land x \in B) \to 0 \cdot_{{mulGrp}_{R}} x = 1_{R}$
79	64 66 67 68 70 74 76 78	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)))$
80	32 79	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)))$
81	7 41	syl	$⊢ φ \to {mulGrp}_{R} \in CMnd$
82	81	adantr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {mulGrp}_{R} \in CMnd$
83	82	cmnmndd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {mulGrp}_{R} \in Mnd$
84	83	adantr	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \to {mulGrp}_{R} \in Mnd$
85	74	ffvelcdmda	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land i \in I) \to c (i) \in ℕ_{0}$
86	38 60 84 85 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$
87	32 86	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$
88		difss	$⊢ I ∖ \{Y\} \subseteq I$
89	3 88	eqsstri	$⊢ J \subseteq I$
90	89	a1i	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to J \subseteq I$
91	38 40 42 18 63 80 87 90	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))$
92		simpr	$⊢ ((φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \land i \in J) \to i \in J$
93	92	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)$
94	92	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)$
95	93 94	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)$
96	95	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))$
97	96	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))$
98	91 97	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))$
99	36 98	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)))$
100	99	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))))$
101	100	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))))$
102	7	crngringd	$⊢ φ \to R \in Ring$
103	102	ringcmnd	$⊢ φ \to R \in CMnd$
104		ovex	$⊢ {ℕ_{0}}^{I} \in V$
105	104	rabex	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V$
106	105	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V$
107	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 \|-
108	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$
109	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$
110	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$
111	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$
112		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)\}$
113	112	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)\}$
114	16 17 108 109 110 3 4 111 113	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 \|-
115	113	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)\}$
116	71 115	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})$
117	22 115	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)$
118		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$
119	117 118	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)$
120	28 116 119	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)\}$
121		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)\})$
122	121	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)\}$
123	120 122	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$
124	123	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}$
125	107 114 124	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}$
126	125	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)))$
127		eqid	$⊢ \cdot_{R} = \cdot_{R}$
128	102	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$
129	86	fmpttd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (i \in I ⟼ c (i) \cdot_{{mulGrp}_{R}} A (i)) : I ⟶ B$
130	38 40 82 67 129 79	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$
131	113 130	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$
132	5 127 17 128 131	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}$
133	126 132	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}$
134		eqid	$⊢ I mPoly R = I mPoly R$
135		eqid	$⊢ {Base}_{(I mPoly R)} = {Base}_{(I mPoly R)}$
136	16	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
137	16 17 8 102 5 3 4 9 10 135	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 \|-
138	13 137	eqeltrid	$⊢ φ \to E (Y) (F) \in {Base}_{(I mPoly R)}$
139	134 5 135 136 138	mplelf	$⊢ φ \to E (Y) (F) : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ B$
140	134 135 17 138	mplelsfi	$⊢ φ \to {finSupp}_{0_{R}} (E (Y) (F))$
141	5 102 106 130 139 140	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)))))$
142	102	adantr	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to R \in Ring$
143	139	ffvelcdmda	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to E (Y) (F) (c) \in B$
144	5 127 142 143 130	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$
145		simpl	$⊢ ({finSupp}_{0} (h) \land h (Y) = 0) \to {finSupp}_{0} (h)$
146	145	a1i	$⊢ (φ \land h \in ({ℕ_{0}}^{I})) \to (({finSupp}_{0} (h) \land h (Y) = 0) \to {finSupp}_{0} (h))$
147	146	ss2rabdv	$⊢ φ \to \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\} \subseteq \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
148	5 17 103 106 133 141 144 147	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))))$
149		nfcv	$⊢ \underline{Ⅎ} b (F ({c ↾}_{J}) \cdot_{R} (\underset{i \in J}{\sum_{{mulGrp}_{R}}}, (({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i))))$
150		fveq2	$⊢ b = {c ↾}_{J} \to F (b) = F ({c ↾}_{J})$
151		fveq1	$⊢ b = {c ↾}_{J} \to b (i) = ({c ↾}_{J}) (i)$
152	151	oveq1d	$⊢ b = {c ↾}_{J} \to b (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i) = ({c ↾}_{J}) (i) \cdot_{{mulGrp}_{R}} ({A ↾}_{J}) (i)$
153	152	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))$
154	153	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))$
155	150 154	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)))$
156		ovex	$⊢ {ℕ_{0}}^{J} \in V$
157	156	rabex	$⊢ \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} \in V$
158	157	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} \in V$
159		eqid	$⊢ J mPoly R = J mPoly R$
160		eqid	$⊢ \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
161	160	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{J}) \| h^{-1} [ℕ] \in Fin\}$
162	159 5 4 161 10	mplelf	$⊢ φ \to F : \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} ⟶ B$
163	162	feqmptd	$⊢ φ \to F = (b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} ⟼ F (b))$
164	159 4 17 10	mplelsfi	$⊢ φ \to {finSupp}_{0_{R}} (F)$
165	163 164	eqbrtrrd	$⊢ φ \to {finSupp}_{0_{R}} ((b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} ⟼ F (b)))$
166	102	adantr	$⊢ (φ \land x \in B) \to R \in Ring$
167		simpr	$⊢ (φ \land x \in B) \to x \in B$
168	5 127 17 166 167	ringlzd	$⊢ (φ \land x \in B) \to 0_{R} \cdot_{R} x = 0_{R}$
169	162	ffvelcdmda	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to F (b) \in B$
170	81	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to {mulGrp}_{R} \in CMnd$
171	89	a1i	$⊢ φ \to J \subseteq I$
172	8 171	ssexd	$⊢ φ \to J \in V$
173	172	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to J \in V$
174	170	cmnmndd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to {mulGrp}_{R} \in Mnd$
175	174	adantr	$⊢ ((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land i \in J) \to {mulGrp}_{R} \in Mnd$
176		ssrab2	$⊢ \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{J}$
177	176	a1i	$⊢ φ \to \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{J}$
178	177	sselda	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to b \in ({ℕ_{0}}^{J})$
179	178	elmaprd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to b : J ⟶ ℕ_{0}$
180	179	ffvelcdmda	$⊢ ((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land i \in J) \to b (i) \in ℕ_{0}$
181	11	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to A : I ⟶ B$
182	89	a1i	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to J \subseteq I$
183	181 182	fssresd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to ({A ↾}_{J}) : J ⟶ B$
184	183	ffvelcdmda	$⊢ ((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land i \in J) \to ({A ↾}_{J}) (i) \in B$
185	38 60 175 180 184	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$
186	185	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$
187	179	feqmptd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to b = (i \in J ⟼ b (i))$
188		breq1	$⊢ h = b \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (b))$
189		simpr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
190	188 189	elrabrd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} (b)$
191	187 190	eqbrtrrd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} ((i \in J ⟼ b (i)))$
192	77	adantl	$⊢ ((φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \land x \in B) \to 0 \cdot_{{mulGrp}_{R}} x = 1_{R}$
193		fvexd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to 1_{R} \in V$
194	191 192 180 184 193	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)))$
195	38 40 170 173 186 194	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$
196		fvexd	$⊢ φ \to 0_{R} \in V$
197	165 168 169 195 196	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)))))$
198		ssidd	$⊢ φ \to B \subseteq B$
199	102	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to R \in Ring$
200	5 127 199 169 195	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$
201		breq1	$⊢ h = {c ↾}_{J} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (({c ↾}_{J})))$
202	25 90	elmapssresd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to {c ↾}_{J} \in ({ℕ_{0}}^{J})$
203	65	a1i	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to 0 \in ℕ_{0}$
204	31 203	fsuppres	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to {finSupp}_{0} (({c ↾}_{J}))$
205	201 202 204	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)\}$
206		breq1	$⊢ h = b \cup \{⟨Y, 0⟩\} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} ((b \cup \{⟨Y, 0⟩\})))$
207		fveq1	$⊢ h = b \cup \{⟨Y, 0⟩\} \to h (Y) = (b \cup \{⟨Y, 0⟩\}) (Y)$
208	207	eqeq1d	$⊢ h = b \cup \{⟨Y, 0⟩\} \to (h (Y) = 0 \leftrightarrow (b \cup \{⟨Y, 0⟩\}) (Y) = 0)$
209	206 208	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))$
210		nn0ex	$⊢ ℕ_{0} \in V$
211	210	a1i	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to ℕ_{0} \in V$
212	8	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to I \in V$
213	3	uneq1i	$⊢ J \cup \{Y\} = (I ∖ \{Y\}) \cup \{Y\}$
214		undifr	$⊢ \{Y\} \subseteq I \leftrightarrow (I ∖ \{Y\}) \cup \{Y\} = I$
215	45 214	sylib	$⊢ φ \to (I ∖ \{Y\}) \cup \{Y\} = I$
216	213 215	eqtrid	$⊢ φ \to J \cup \{Y\} = I$
217	216	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to J \cup \{Y\} = I$
218	65	a1i	$⊢ φ \to 0 \in ℕ_{0}$
219	9 218	fsnd	$⊢ φ \to \{⟨Y, 0⟩\} : \{Y\} ⟶ ℕ_{0}$
220	219	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to \{⟨Y, 0⟩\} : \{Y\} ⟶ ℕ_{0}$
221	3	ineq1i	$⊢ J \cap \{Y\} = (I ∖ \{Y\}) \cap \{Y\}$
222		disjdifr	$⊢ (I ∖ \{Y\}) \cap \{Y\} = \emptyset$
223	221 222	eqtri	$⊢ J \cap \{Y\} = \emptyset$
224	223	a1i	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to J \cap \{Y\} = \emptyset$
225	179 220 224	fun2d	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to (b \cup \{⟨Y, 0⟩\}) : J \cup \{Y\} ⟶ ℕ_{0}$
226	217 225	feq2dd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to (b \cup \{⟨Y, 0⟩\}) : I ⟶ ℕ_{0}$
227	211 212 226	elmapdd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to b \cup \{⟨Y, 0⟩\} \in ({ℕ_{0}}^{I})$
228	9 65	jctir	$⊢ φ \to (Y \in I \land 0 \in ℕ_{0})$
229	228	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to (Y \in I \land 0 \in ℕ_{0})$
230	179	ffund	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to Fun b$
231		neldifsnd	$⊢ φ \to \neg Y \in (I ∖ \{Y\})$
232	3	eleq2i	$⊢ Y \in J \leftrightarrow Y \in (I ∖ \{Y\})$
233	231 232	sylnibr	$⊢ φ \to \neg Y \in J$
234	233	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to \neg Y \in J$
235	179	fdmd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to dom b = J$
236	234 235	neleqtrrd	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to \neg Y \in dom b$
237		df-nel	$⊢ Y \notin dom b \leftrightarrow \neg Y \in dom b$
238	236 237	sylibr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to Y \notin dom b$
239	230 238	jca	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to (Fun b \land Y \notin dom b)$
240		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))$
241	240	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⟩\}))$
242	229 239 190 241	syl21anc	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} ((b \cup \{⟨Y, 0⟩\}))$
243	9	adantr	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to Y \in I$
244	65	a1i	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to 0 \in ℕ_{0}$
245		fsnunfv	$⊢ (Y \in I \land 0 \in ℕ_{0} \land \neg Y \in dom b) \to (b \cup \{⟨Y, 0⟩\}) (Y) = 0$
246	243 244 236 245	syl3anc	$⊢ (φ \land b \in \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}) \to (b \cup \{⟨Y, 0⟩\}) (Y) = 0$
247	242 246	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)$
248	209 227 247	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)\}$
249		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}$
250	249	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⟩\}$
251	3	reseq2i	$⊢ {c ↾}_{J} = {c ↾}_{(I ∖ \{Y\})}$
252	251	uneq1i	$⊢ ({c ↾}_{J}) \cup \{⟨Y, 0⟩\} = ({c ↾}_{(I ∖ \{Y\})}) \cup \{⟨Y, 0⟩\}$
253	252	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⟩\}$
254	25	elmaprd	$⊢ (φ \land c \in \{h \in ({ℕ_{0}}^{I}) \| ({finSupp}_{0} (h) \land h (Y) = 0)\}) \to c : I ⟶ ℕ_{0}$
255	254	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}$
256	255	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$
257	243	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$
258	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)$
259	258	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$
260		fresunsn	$⊢ (c Fn I \land Y \in I \land c (Y) = 0) \to ({c ↾}_{(I ∖ \{Y\})}) \cup \{⟨Y, 0⟩\} = c$
261	256 257 259 260	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$
262	250 253 261	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⟩\}$
263		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⟩\}$
264	263	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}$
265	179	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}$
266	265	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$
267	234	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$
268		fsnunres	$⊢ (b Fn J \land \neg Y \in J) \to {(b \cup \{⟨Y, 0⟩\}) ↾}_{J} = b$
269	266 267 268	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$
270	264 269	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}$
271	262 270	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⟩\})$
272	248 271	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}$
273	149 5 17 155 103 158 197 198 200 205 272	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))))$
274	101 148 273	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))))$
275	1 5	evlval	$⊢ Q = (I evalSub R) (B)$
276		eqid	$⊢ I mPoly (R ↾_{𝑠} B) = I mPoly (R ↾_{𝑠} B)$
277		eqid	$⊢ {Base}_{(I mPoly (R ↾_{𝑠} B))} = {Base}_{(I mPoly (R ↾_{𝑠} B))}$
278		eqid	$⊢ R ↾_{𝑠} B = R ↾_{𝑠} B$
279	5	subrgid	$⊢ R \in Ring \to B \in SubRing (R)$
280	102 279	syl	$⊢ φ \to B \in SubRing (R)$
281	5	ressid	$⊢ R \in CRing \to R ↾_{𝑠} B = R$
282	7 281	syl	$⊢ φ \to R ↾_{𝑠} B = R$
283	282	oveq2d	$⊢ φ \to I mPoly (R ↾_{𝑠} B) = I mPoly R$
284	283	fveq2d	$⊢ φ \to {Base}_{(I mPoly (R ↾_{𝑠} B))} = {Base}_{(I mPoly R)}$
285	138 284	eleqtrrd	$⊢ φ \to E (Y) (F) \in {Base}_{(I mPoly (R ↾_{𝑠} B))}$
286	5	fvexi	$⊢ B \in V$
287	286	a1i	$⊢ φ \to B \in V$
288	287 8 11	elmapdd	$⊢ φ \to A \in (B^{I})$
289	275 276 277 278 136 5 37 60 127 8 7 280 285 288	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))))$
290	2 5	evlval	$⊢ O = (J evalSub R) (B)$
291		eqid	$⊢ J mPoly (R ↾_{𝑠} B) = J mPoly (R ↾_{𝑠} B)$
292		eqid	$⊢ {Base}_{(J mPoly (R ↾_{𝑠} B))} = {Base}_{(J mPoly (R ↾_{𝑠} B))}$
293	10 4	eleqtrdi	$⊢ φ \to F \in {Base}_{(J mPoly R)}$
294	282	oveq2d	$⊢ φ \to J mPoly (R ↾_{𝑠} B) = J mPoly R$
295	294	fveq2d	$⊢ φ \to {Base}_{(J mPoly (R ↾_{𝑠} B))} = {Base}_{(J mPoly R)}$
296	293 295	eleqtrrd	$⊢ φ \to F \in {Base}_{(J mPoly (R ↾_{𝑠} B))}$
297	288 171	elmapssresd	$⊢ φ \to {A ↾}_{J} \in (B^{J})$
298	290 291 292 278 161 5 37 60 127 172 7 280 296 297	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))))$
299	274 289 298	3eqtr4d	$⊢ φ \to Q (E (Y) (F)) (A) = O (F) ({A ↾}_{J})$

Metamath Proof Explorer

Theorem evlextv

Proof