evlextv - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > evlextv		Structured version Visualization version GIF version

Theorem evlextv 34285

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.)

**Hypotheses**
Ref	Expression
evlextv.q	⊢ 𝑄 = (𝐼 eval 𝑅)
evlextv.o	⊢ 𝑂 = (𝐽 eval 𝑅)
evlextv.j	⊢ 𝐽 = (𝐼 ∖ {𝑌})
evlextv.m	⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))
evlextv.b	⊢ 𝐵 = (Base‘𝑅)
evlextv.e	⊢ 𝐸 = (𝐼extendVars𝑅)
evlextv.r	⊢ (𝜑 → 𝑅 ∈ CRing)
evlextv.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
evlextv.y	⊢ (𝜑 → 𝑌 ∈ 𝐼)
evlextv.f	⊢ (𝜑 → 𝐹 ∈ 𝑀)
evlextv.a	⊢ (𝜑 → 𝐴:𝐼⟶𝐵)

**Assertion**
Ref	Expression
evlextv	⊢ (𝜑 → ((𝑄‘((𝐸‘𝑌)‘𝐹))‘𝐴) = ((𝑂‘𝐹)‘(𝐴 ↾ 𝐽)))

Proof of Theorem evlextv Dummy variables 𝑏 𝑐 𝑖 𝑥 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evlextv.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐼extendVars𝑅)
2	1	fveq1i 6917	. . . . . . . . . 10 ⊢ (𝐸‘𝑌) = ((𝐼extendVars𝑅)‘𝑌)
3	2	fveq1i 6917	. . . . . . . . 9 ⊢ ((𝐸‘𝑌)‘𝐹) = (((𝐼extendVars𝑅)‘𝑌)‘𝐹)
4	3	fveq1i 6917	. . . . . . . 8 ⊢ (((𝐸‘𝑌)‘𝐹)‘𝑐) = ((((𝐼extendVars𝑅)‘𝑌)‘𝐹)‘𝑐)
5	4	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (((𝐸‘𝑌)‘𝐹)‘𝑐) = ((((𝐼extendVars𝑅)‘𝑌)‘𝐹)‘𝑐))
6		eqid 2763	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
7		eqid 2763	. . . . . . . 8 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
8		evlextv.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
9	8	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝐼 ∈ 𝑉)
10		evlextv.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ CRing)
11	10	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑅 ∈ CRing)
12		evlextv.y	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ 𝐼)
13	12	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑌 ∈ 𝐼)
14		evlextv.j	. . . . . . . 8 ⊢ 𝐽 = (𝐼 ∖ {𝑌})
15		evlextv.m	. . . . . . . 8 ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))
16		evlextv.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ 𝑀)
17	16	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝐹 ∈ 𝑀)
18		breq1 5111	. . . . . . . . 9 ⊢ (ℎ = 𝑐 → (ℎ finSupp 0 ↔ 𝑐 finSupp 0))
19		ssrab2 4008	. . . . . . . . . . 11 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ⊆ (ℕ₀ ↑_m 𝐼)
20	19	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ⊆ (ℕ₀ ↑_m 𝐼))
21	20	sselda 3913	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑐 ∈ (ℕ₀ ↑_m 𝐼))
22		fveq1 6915	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑐 → (ℎ‘𝑌) = (𝑐‘𝑌))
23	22	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑐 → ((ℎ‘𝑌) = 0 ↔ (𝑐‘𝑌) = 0))
24	18, 23	anbi12d 644	. . . . . . . . . . 11 ⊢ (ℎ = 𝑐 → ((ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0) ↔ (𝑐 finSupp 0 ∧ (𝑐‘𝑌) = 0)))
25		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})
26	24, 25	elrabrd 3651	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑐 finSupp 0 ∧ (𝑐‘𝑌) = 0))
27	26	simpld 500	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑐 finSupp 0)
28	18, 21, 27	elrabd 3650	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
29	6, 7, 9, 11, 13, 14, 15, 17, 28	extvfvv 34277	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → ((((𝐼extendVars𝑅)‘𝑌)‘𝐹)‘𝑐) = if((𝑐‘𝑌) = 0, (𝐹‘(𝑐 ↾ 𝐽)), (0_g‘𝑅)))
30	26	simprd 501	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑐‘𝑌) = 0)
31	30	iftrued 4493	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → if((𝑐‘𝑌) = 0, (𝐹‘(𝑐 ↾ 𝐽)), (0_g‘𝑅)) = (𝐹‘(𝑐 ↾ 𝐽)))
32	5, 29, 31	3eqtrd 2802	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (((𝐸‘𝑌)‘𝐹)‘𝑐) = (𝐹‘(𝑐 ↾ 𝐽)))
33		eqid 2763	. . . . . . . . 9 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
34		evlextv.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝑅)
35	33, 34	mgpbas 20416	. . . . . . . 8 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
36		eqid 2763	. . . . . . . . 9 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
37	33, 36	ringidval 20460	. . . . . . . 8 ⊢ (1_r‘𝑅) = (0_g‘(mulGrp‘𝑅))
38	33	crngmgp 20518	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
39	11, 38	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (mulGrp‘𝑅) ∈ CMnd)
40		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → 𝑖 ∈ (𝐼 ∖ 𝐽))
41	14	difeq2i 4063	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∖ 𝐽) = (𝐼 ∖ (𝐼 ∖ {𝑌}))
42	12	snssd 4749	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {𝑌} ⊆ 𝐼)
43		dfss4 4217	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑌} ⊆ 𝐼 ↔ (𝐼 ∖ (𝐼 ∖ {𝑌})) = {𝑌})
44	42, 43	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 ∖ (𝐼 ∖ {𝑌})) = {𝑌})
45	41, 44	eqtrid 2810	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 ∖ 𝐽) = {𝑌})
46	45	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (𝐼 ∖ 𝐽) = {𝑌})
47	40, 46	eleqtrd 2866	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → 𝑖 ∈ {𝑌})
48	47	elsnd 4602	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → 𝑖 = 𝑌)
49	48	fveq2d 6920	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (𝑐‘𝑖) = (𝑐‘𝑌))
50	30	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (𝑐‘𝑌) = 0)
51	49, 50	eqtrd 2798	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (𝑐‘𝑖) = 0)
52	51	oveq1d 7466	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)) = (0(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)))
53		evlextv.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴:𝐼⟶𝐵)
54	53	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → 𝐴:𝐼⟶𝐵)
55		difssd 4076	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝐼 ∖ 𝐽) ⊆ 𝐼)
56	55	sselda 3913	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → 𝑖 ∈ 𝐼)
57	54, 56	ffvelcdmd 7117	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (𝐴‘𝑖) ∈ 𝐵)
58		eqid 2763	. . . . . . . . . . 11 ⊢ (._g‘(mulGrp‘𝑅)) = (._g‘(mulGrp‘𝑅))
59	35, 37, 58	mulg0 19334	. . . . . . . . . 10 ⊢ ((𝐴‘𝑖) ∈ 𝐵 → (0(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)) = (1_r‘𝑅))
60	57, 59	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (0(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)) = (1_r‘𝑅))
61	52, 60	eqtrd 2798	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)) = (1_r‘𝑅))
62		fvexd 6931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (1_r‘𝑅) ∈ V)
63		0nn0 12661	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
64	63	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 0 ∈ ℕ₀)
65	8	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
66		ssidd 3936	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ⊆ 𝐼)
67	53	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝐴:𝐼⟶𝐵)
68	67	ffvelcdmda 7116	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐼) → (𝐴‘𝑖) ∈ 𝐵)
69		ssrab2 4008	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ₀ ↑_m 𝐼)
70	69	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ₀ ↑_m 𝐼))
71	70	sselda 3913	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑐 ∈ (ℕ₀ ↑_m 𝐼))
72	71	elmaprd 8908	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑐:𝐼⟶ℕ₀)
73		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
74	18, 73	elrabrd 3651	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑐 finSupp 0)
75	35, 37, 58	mulg0 19334	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → (0(._g‘(mulGrp‘𝑅))𝑥) = (1_r‘𝑅))
76	75	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 ∈ 𝐵) → (0(._g‘(mulGrp‘𝑅))𝑥) = (1_r‘𝑅))
77	62, 64, 65, 66, 68, 72, 74, 76	fisuppov1 33373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))) finSupp (1_r‘𝑅))
78	28, 77	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))) finSupp (1_r‘𝑅))
79	10, 38	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
80	79	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (mulGrp‘𝑅) ∈ CMnd)
81	80	cmnmndd 20069	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (mulGrp‘𝑅) ∈ Mnd)
82	81	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐼) → (mulGrp‘𝑅) ∈ Mnd)
83	72	ffvelcdmda 7116	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐼) → (𝑐‘𝑖) ∈ ℕ₀)
84	35, 58, 82, 83, 68	mulgnn0cld 19355	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐼) → ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)) ∈ 𝐵)
85	28, 84	syldanl 614	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ 𝐼) → ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)) ∈ 𝐵)
86		difss 4075	. . . . . . . . . 10 ⊢ (𝐼 ∖ {𝑌}) ⊆ 𝐼
87	14, 86	eqsstri 3959	. . . . . . . . 9 ⊢ 𝐽 ⊆ 𝐼
88	87	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝐽 ⊆ 𝐼)
89	35, 37, 39, 9, 61, 78, 85, 88	gsummptfsres 33714	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → ((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)))) = ((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)))))
90		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ 𝐽) → 𝑖 ∈ 𝐽)
91	90	fvresd 6936	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ 𝐽) → ((𝑐 ↾ 𝐽)‘𝑖) = (𝑐‘𝑖))
92	90	fvresd 6936	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ 𝐽) → ((𝐴 ↾ 𝐽)‘𝑖) = (𝐴‘𝑖))
93	91, 92	oveq12d 7469	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ 𝐽) → (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)) = ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)))
94	93	mpteq2dva 5204	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))) = (𝑖 ∈ 𝐽 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))
95	94	oveq2d 7467	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → ((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))) = ((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)))))
96	89, 95	eqtr4d 2801	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → ((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)))) = ((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))))
97	32, 96	oveq12d 7469	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → ((((𝐸‘𝑌)‘𝐹)‘𝑐)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))) = ((𝐹‘(𝑐 ↾ 𝐽))(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))
98	97	mpteq2dva 5204	. . . 4 ⊢ (𝜑 → (𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)))))) = (𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((𝐹‘(𝑐 ↾ 𝐽))(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))))))
99	98	oveq2d 7467	. . 3 ⊢ (𝜑 → (𝑅 Σ_g (𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))) = (𝑅 Σ_g (𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((𝐹‘(𝑐 ↾ 𝐽))(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))))
100	10	crngringd 20524	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
101	100	ringcmnd 20564	. . . 4 ⊢ (𝜑 → 𝑅 ∈ CMnd)
102		ovex 7484	. . . . . 6 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
103	102	rabex 5307	. . . . 5 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V
104	103	a1i 11	. . . 4 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∈ V)
105	4	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → (((𝐸‘𝑌)‘𝐹)‘𝑐) = ((((𝐼extendVars𝑅)‘𝑌)‘𝐹)‘𝑐))
106	8	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝐼 ∈ 𝑉)
107	10	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝑅 ∈ CRing)
108	12	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝑌 ∈ 𝐼)
109	16	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝐹 ∈ 𝑀)
110		difssd 4076	. . . . . . . . 9 ⊢ (𝜑 → ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ⊆ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
111	110	sselda 3913	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
112	6, 7, 106, 107, 108, 14, 15, 109, 111	extvfvv 34277	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ((((𝐼extendVars𝑅)‘𝑌)‘𝐹)‘𝑐) = if((𝑐‘𝑌) = 0, (𝐹‘(𝑐 ↾ 𝐽)), (0_g‘𝑅)))
113	111	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
114	69, 113	sselid 3911	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → 𝑐 ∈ (ℕ₀ ↑_m 𝐼))
115	18, 113	elrabrd 3651	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → 𝑐 finSupp 0)
116		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → (𝑐‘𝑌) = 0)
117	115, 116	jca 521	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → (𝑐 finSupp 0 ∧ (𝑐‘𝑌) = 0))
118	24, 114, 117	elrabd 3650	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})
119		simplr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}))
120	119	eldifbd 4055	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → ¬ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})
121	118, 120	pm2.65da 829	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ¬ (𝑐‘𝑌) = 0)
122	121	iffalsed 4496	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → if((𝑐‘𝑌) = 0, (𝐹‘(𝑐 ↾ 𝐽)), (0_g‘𝑅)) = (0_g‘𝑅))
123	105, 112, 122	3eqtrd 2802	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → (((𝐸‘𝑌)‘𝐹)‘𝑐) = (0_g‘𝑅))
124	123	oveq1d 7466	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ((((𝐸‘𝑌)‘𝐹)‘𝑐)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))) = ((0_g‘𝑅)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))
125		eqid 2763	. . . . . 6 ⊢ (._r‘𝑅) = (._r‘𝑅)
126	100	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝑅 ∈ Ring)
127	84	fmpttd 7147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))):𝐼⟶𝐵)
128	35, 37, 80, 65, 127, 77	gsumcl 20180	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → ((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)))) ∈ 𝐵)
129	111, 128	syldan 603	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)))) ∈ 𝐵)
130	34, 125, 7, 126, 129	ringlzd 20577	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ((0_g‘𝑅)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))) = (0_g‘𝑅))
131	124, 130	eqtrd 2798	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ((((𝐸‘𝑌)‘𝐹)‘𝑐)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))) = (0_g‘𝑅))
132		eqid 2763	. . . . . 6 ⊢ (𝐼 mPoly 𝑅) = (𝐼 mPoly 𝑅)
133		eqid 2763	. . . . . 6 ⊢ (Base‘(𝐼 mPoly 𝑅)) = (Base‘(𝐼 mPoly 𝑅))
134	6	psrbasfsupp 34254	. . . . . 6 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡ℎ “ ℕ) ∈ Fin}
135	6, 7, 8, 100, 34, 14, 15, 12, 16, 133	extvfvcl 34279	. . . . . . 7 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝑌)‘𝐹) ∈ (Base‘(𝐼 mPoly 𝑅)))
136	3, 135	eqeltrid 2868	. . . . . 6 ⊢ (𝜑 → ((𝐸‘𝑌)‘𝐹) ∈ (Base‘(𝐼 mPoly 𝑅)))
137	132, 34, 133, 134, 136	mplelf 22360	. . . . 5 ⊢ (𝜑 → ((𝐸‘𝑌)‘𝐹):{ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}⟶𝐵)
138	132, 133, 7, 136	mplelsfi 22357	. . . . 5 ⊢ (𝜑 → ((𝐸‘𝑌)‘𝐹) finSupp (0_g‘𝑅))
139	34, 100, 104, 128, 137, 138	rmfsupp2 33897	. . . 4 ⊢ (𝜑 → (𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖)))))) finSupp (0_g‘𝑅))
140	100	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → 𝑅 ∈ Ring)
141	137	ffvelcdmda 7116	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → (((𝐸‘𝑌)‘𝐹)‘𝑐) ∈ 𝐵)
142	34, 125, 140, 141, 128	ringcld 20535	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}) → ((((𝐸‘𝑌)‘𝐹)‘𝑐)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))) ∈ 𝐵)
143		simpl 488	. . . . . 6 ⊢ ((ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0) → ℎ finSupp 0)
144	143	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ (ℕ₀ ↑_m 𝐼)) → ((ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0) → ℎ finSupp 0))
145	144	ss2rabdv 4003	. . . 4 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ⊆ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0})
146	34, 7, 101, 104, 131, 139, 142, 145	gsummptfsres 33714	. . 3 ⊢ (𝜑 → (𝑅 Σ_g (𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))) = (𝑅 Σ_g (𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))))
147		nfcv 2926	. . . 4 ⊢ Ⅎ𝑏((𝐹‘(𝑐 ↾ 𝐽))(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))))
148		fveq2 6916	. . . . 5 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → (𝐹‘𝑏) = (𝐹‘(𝑐 ↾ 𝐽)))
149		fveq1 6915	. . . . . . . 8 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → (𝑏‘𝑖) = ((𝑐 ↾ 𝐽)‘𝑖))
150	149	oveq1d 7466	. . . . . . 7 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)) = (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))
151	150	mpteq2dv 5205	. . . . . 6 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))) = (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))
152	151	oveq2d 7467	. . . . 5 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → ((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))) = ((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))))
153	148, 152	oveq12d 7469	. . . 4 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → ((𝐹‘𝑏)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))) = ((𝐹‘(𝑐 ↾ 𝐽))(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))
154		ovex 7484	. . . . . 6 ⊢ (ℕ₀ ↑_m 𝐽) ∈ V
155	154	rabex 5307	. . . . 5 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} ∈ V
156	155	a1i 11	. . . 4 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} ∈ V)
157		eqid 2763	. . . . . . . 8 ⊢ (𝐽 mPoly 𝑅) = (𝐽 mPoly 𝑅)
158		eqid 2763	. . . . . . . . 9 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}
159	158	psrbasfsupp 34254	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ (^◡ℎ “ ℕ) ∈ Fin}
160	157, 34, 15, 159, 16	mplelf 22360	. . . . . . 7 ⊢ (𝜑 → 𝐹:{ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}⟶𝐵)
161	160	feqmptd 6984	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} ↦ (𝐹‘𝑏)))
162	157, 15, 7, 16	mplelsfi 22357	. . . . . 6 ⊢ (𝜑 → 𝐹 finSupp (0_g‘𝑅))
163	161, 162	eqbrtrrd 5135	. . . . 5 ⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} ↦ (𝐹‘𝑏)) finSupp (0_g‘𝑅))
164	100	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ Ring)
165		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
166	34, 125, 7, 164, 165	ringlzd 20577	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((0_g‘𝑅)(._r‘𝑅)𝑥) = (0_g‘𝑅))
167	160	ffvelcdmda 7116	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝐹‘𝑏) ∈ 𝐵)
168	79	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (mulGrp‘𝑅) ∈ CMnd)
169	87	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ⊆ 𝐼)
170	8, 169	ssexd 5293	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ V)
171	170	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝐽 ∈ V)
172	168	cmnmndd 20069	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (mulGrp‘𝑅) ∈ Mnd)
173	172	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐽) → (mulGrp‘𝑅) ∈ Mnd)
174		ssrab2 4008	. . . . . . . . . . . 12 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} ⊆ (ℕ₀ ↑_m 𝐽)
175	174	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} ⊆ (ℕ₀ ↑_m 𝐽))
176	175	sselda 3913	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝑏 ∈ (ℕ₀ ↑_m 𝐽))
177	176	elmaprd 8908	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝑏:𝐽⟶ℕ₀)
178	177	ffvelcdmda 7116	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐽) → (𝑏‘𝑖) ∈ ℕ₀)
179	53	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝐴:𝐼⟶𝐵)
180	87	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝐽 ⊆ 𝐼)
181	179, 180	fssresd 6779	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝐴 ↾ 𝐽):𝐽⟶𝐵)
182	181	ffvelcdmda 7116	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐽) → ((𝐴 ↾ 𝐽)‘𝑖) ∈ 𝐵)
183	35, 58, 173, 178, 182	mulgnn0cld 19355	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐽) → ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)) ∈ 𝐵)
184	183	fmpttd 7147	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))):𝐽⟶𝐵)
185	177	feqmptd 6984	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝑏 = (𝑖 ∈ 𝐽 ↦ (𝑏‘𝑖)))
186		breq1 5111	. . . . . . . . 9 ⊢ (ℎ = 𝑏 → (ℎ finSupp 0 ↔ 𝑏 finSupp 0))
187		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0})
188	186, 187	elrabrd 3651	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝑏 finSupp 0)
189	185, 188	eqbrtrrd 5135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝑖 ∈ 𝐽 ↦ (𝑏‘𝑖)) finSupp 0)
190	75	adantl 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑥 ∈ 𝐵) → (0(._g‘(mulGrp‘𝑅))𝑥) = (1_r‘𝑅))
191		fvexd 6931	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (1_r‘𝑅) ∈ V)
192	189, 190, 178, 182, 191	fsuppssov1 9413	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))) finSupp (1_r‘𝑅))
193	35, 37, 168, 171, 184, 192	gsumcl 20180	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → ((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))) ∈ 𝐵)
194		fvexd 6931	. . . . 5 ⊢ (𝜑 → (0_g‘𝑅) ∈ V)
195	163, 166, 167, 193, 194	fsuppssov1 9413	. . . 4 ⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} ↦ ((𝐹‘𝑏)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))))) finSupp (0_g‘𝑅))
196		ssidd 3936	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ 𝐵)
197	100	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝑅 ∈ Ring)
198	34, 125, 197, 167, 193	ringcld 20535	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → ((𝐹‘𝑏)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))) ∈ 𝐵)
199		breq1 5111	. . . . 5 ⊢ (ℎ = (𝑐 ↾ 𝐽) → (ℎ finSupp 0 ↔ (𝑐 ↾ 𝐽) finSupp 0))
200	21, 88	elmapssresd 8933	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑐 ↾ 𝐽) ∈ (ℕ₀ ↑_m 𝐽))
201	63	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 0 ∈ ℕ₀)
202	27, 201	fsuppres 9422	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑐 ↾ 𝐽) finSupp 0)
203	199, 200, 202	elrabd 3650	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑐 ↾ 𝐽) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0})
204		breq1 5111	. . . . . . 7 ⊢ (ℎ = (𝑏 ∪ {⟨𝑌, 0⟩}) → (ℎ finSupp 0 ↔ (𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0))
205		fveq1 6915	. . . . . . . 8 ⊢ (ℎ = (𝑏 ∪ {⟨𝑌, 0⟩}) → (ℎ‘𝑌) = ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌))
206	205	eqeq1d 2765	. . . . . . 7 ⊢ (ℎ = (𝑏 ∪ {⟨𝑌, 0⟩}) → ((ℎ‘𝑌) = 0 ↔ ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌) = 0))
207	204, 206	anbi12d 644	. . . . . 6 ⊢ (ℎ = (𝑏 ∪ {⟨𝑌, 0⟩}) → ((ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0) ↔ ((𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0 ∧ ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌) = 0)))
208		nn0ex 12652	. . . . . . . 8 ⊢ ℕ₀ ∈ V
209	208	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → ℕ₀ ∈ V)
210	8	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
211	14	uneq1i 4166	. . . . . . . . . 10 ⊢ (𝐽 ∪ {𝑌}) = ((𝐼 ∖ {𝑌}) ∪ {𝑌})
212		undifr 4442	. . . . . . . . . . 11 ⊢ ({𝑌} ⊆ 𝐼 ↔ ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
213	42, 212	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
214	211, 213	eqtrid 2810	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ∪ {𝑌}) = 𝐼)
215	214	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝐽 ∪ {𝑌}) = 𝐼)
216	63	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℕ₀)
217	12, 216	fsnd 6900	. . . . . . . . . 10 ⊢ (𝜑 → {⟨𝑌, 0⟩}:{𝑌}⟶ℕ₀)
218	217	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → {⟨𝑌, 0⟩}:{𝑌}⟶ℕ₀)
219	14	ineq1i 4116	. . . . . . . . . . 11 ⊢ (𝐽 ∩ {𝑌}) = ((𝐼 ∖ {𝑌}) ∩ {𝑌})
220		disjdifr 4430	. . . . . . . . . . 11 ⊢ ((𝐼 ∖ {𝑌}) ∩ {𝑌}) = ∅
221	219, 220	eqtri 2786	. . . . . . . . . 10 ⊢ (𝐽 ∩ {𝑌}) = ∅
222	221	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝐽 ∩ {𝑌}) = ∅)
223	177, 218, 222	fun2d 6776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝑏 ∪ {⟨𝑌, 0⟩}):(𝐽 ∪ {𝑌})⟶ℕ₀)
224	215, 223	feq2dd 6725	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝑏 ∪ {⟨𝑌, 0⟩}):𝐼⟶ℕ₀)
225	209, 210, 224	elmapdd 8899	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝑏 ∪ {⟨𝑌, 0⟩}) ∈ (ℕ₀ ↑_m 𝐼))
226	12, 63	jctir 530	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ₀))
227	226	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ₀))
228	177	ffund 6744	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → Fun 𝑏)
229		neldifsnd 4758	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝐼 ∖ {𝑌}))
230	14	eleq2i 2856	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ 𝐽 ↔ 𝑌 ∈ (𝐼 ∖ {𝑌}))
231	229, 230	sylnibr 332	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑌 ∈ 𝐽)
232	231	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → ¬ 𝑌 ∈ 𝐽)
233	177	fdmd 6750	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → dom 𝑏 = 𝐽)
234	232, 233	neleqtrrd 2887	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → ¬ 𝑌 ∈ dom 𝑏)
235		df-nel 3066	. . . . . . . . . 10 ⊢ (𝑌 ∉ dom 𝑏 ↔ ¬ 𝑌 ∈ dom 𝑏)
236	234, 235	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝑌 ∉ dom 𝑏)
237	228, 236	jca 521	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (Fun 𝑏 ∧ 𝑌 ∉ dom 𝑏))
238		funsnfsupp 9421	. . . . . . . . 9 ⊢ (((𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ₀) ∧ (Fun 𝑏 ∧ 𝑌 ∉ dom 𝑏)) → ((𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0 ↔ 𝑏 finSupp 0))
239	238	biimpar 483	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ₀) ∧ (Fun 𝑏 ∧ 𝑌 ∉ dom 𝑏)) ∧ 𝑏 finSupp 0) → (𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0)
240	227, 237, 188, 239	syl21anc 851	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0)
241	12	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 𝑌 ∈ 𝐼)
242	63	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → 0 ∈ ℕ₀)
243		fsnunfv 7223	. . . . . . . 8 ⊢ ((𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ₀ ∧ ¬ 𝑌 ∈ dom 𝑏) → ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌) = 0)
244	241, 242, 234, 243	syl3anc 1399	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌) = 0)
245	240, 244	jca 521	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → ((𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0 ∧ ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌) = 0))
246	207, 225, 245	elrabd 3650	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → (𝑏 ∪ {⟨𝑌, 0⟩}) ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})
247		simpr 490	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → 𝑏 = (𝑐 ↾ 𝐽))
248	247	uneq1d 4169	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → (𝑏 ∪ {⟨𝑌, 0⟩}) = ((𝑐 ↾ 𝐽) ∪ {⟨𝑌, 0⟩}))
249	14	reseq2i 5983	. . . . . . . . 9 ⊢ (𝑐 ↾ 𝐽) = (𝑐 ↾ (𝐼 ∖ {𝑌}))
250	249	uneq1i 4166	. . . . . . . 8 ⊢ ((𝑐 ↾ 𝐽) ∪ {⟨𝑌, 0⟩}) = ((𝑐 ↾ (𝐼 ∖ {𝑌})) ∪ {⟨𝑌, 0⟩})
251	250	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → ((𝑐 ↾ 𝐽) ∪ {⟨𝑌, 0⟩}) = ((𝑐 ↾ (𝐼 ∖ {𝑌})) ∪ {⟨𝑌, 0⟩}))
252	21	elmaprd 8908	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑐:𝐼⟶ℕ₀)
253	252	ad4ant13 764	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → 𝑐:𝐼⟶ℕ₀)
254	253	ffnd 6740	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → 𝑐 Fn 𝐼)
255	241	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → 𝑌 ∈ 𝐼)
256	26	ad4ant13 764	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → (𝑐 finSupp 0 ∧ (𝑐‘𝑌) = 0))
257	256	simprd 501	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → (𝑐‘𝑌) = 0)
258		fresunsn 33317	. . . . . . . 8 ⊢ ((𝑐 Fn 𝐼 ∧ 𝑌 ∈ 𝐼 ∧ (𝑐‘𝑌) = 0) → ((𝑐 ↾ (𝐼 ∖ {𝑌})) ∪ {⟨𝑌, 0⟩}) = 𝑐)
259	254, 255, 257, 258	syl3anc 1399	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → ((𝑐 ↾ (𝐼 ∖ {𝑌})) ∪ {⟨𝑌, 0⟩}) = 𝑐)
260	248, 251, 259	3eqtrrd 2803	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩}))
261		simpr 490	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩}))
262	261	reseq1d 5985	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → (𝑐 ↾ 𝐽) = ((𝑏 ∪ {⟨𝑌, 0⟩}) ↾ 𝐽))
263	177	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → 𝑏:𝐽⟶ℕ₀)
264	263	ffnd 6740	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → 𝑏 Fn 𝐽)
265	232	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → ¬ 𝑌 ∈ 𝐽)
266		fsnunres 7224	. . . . . . . 8 ⊢ ((𝑏 Fn 𝐽 ∧ ¬ 𝑌 ∈ 𝐽) → ((𝑏 ∪ {⟨𝑌, 0⟩}) ↾ 𝐽) = 𝑏)
267	264, 265, 266	syl2anc 596	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → ((𝑏 ∪ {⟨𝑌, 0⟩}) ↾ 𝐽) = 𝑏)
268	262, 267	eqtr2d 2799	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → 𝑏 = (𝑐 ↾ 𝐽))
269	260, 268	impbida 813	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑏 = (𝑐 ↾ 𝐽) ↔ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})))
270	246, 269	reu6dv 33168	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}) → ∃!𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}𝑏 = (𝑐 ↾ 𝐽))
271	147, 34, 7, 153, 101, 156, 195, 196, 198, 203, 270	gsummptfsf1o 33720	. . 3 ⊢ (𝜑 → (𝑅 Σ_g (𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} ↦ ((𝐹‘𝑏)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))) = (𝑅 Σ_g (𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((𝐹‘(𝑐 ↾ 𝐽))(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))))
272	99, 146, 271	3eqtr4d 2808	. 2 ⊢ (𝜑 → (𝑅 Σ_g (𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))) = (𝑅 Σ_g (𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} ↦ ((𝐹‘𝑏)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))))
273		evlextv.q	. . . 4 ⊢ 𝑄 = (𝐼 eval 𝑅)
274	273, 34	evlval 22464	. . 3 ⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝐵)
275		eqid 2763	. . 3 ⊢ (𝐼 mPoly (𝑅 ↾_s 𝐵)) = (𝐼 mPoly (𝑅 ↾_s 𝐵))
276		eqid 2763	. . 3 ⊢ (Base‘(𝐼 mPoly (𝑅 ↾_s 𝐵))) = (Base‘(𝐼 mPoly (𝑅 ↾_s 𝐵)))
277		eqid 2763	. . 3 ⊢ (𝑅 ↾_s 𝐵) = (𝑅 ↾_s 𝐵)
278	34	subrgid 20876	. . . 4 ⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅))
279	100, 278	syl 18	. . 3 ⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅))
280	34	ressid 17466	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (𝑅 ↾_s 𝐵) = 𝑅)
281	10, 280	syl 18	. . . . . 6 ⊢ (𝜑 → (𝑅 ↾_s 𝐵) = 𝑅)
282	281	oveq2d 7467	. . . . 5 ⊢ (𝜑 → (𝐼 mPoly (𝑅 ↾_s 𝐵)) = (𝐼 mPoly 𝑅))
283	282	fveq2d 6920	. . . 4 ⊢ (𝜑 → (Base‘(𝐼 mPoly (𝑅 ↾_s 𝐵))) = (Base‘(𝐼 mPoly 𝑅)))
284	136, 283	eleqtrrd 2867	. . 3 ⊢ (𝜑 → ((𝐸‘𝑌)‘𝐹) ∈ (Base‘(𝐼 mPoly (𝑅 ↾_s 𝐵))))
285	34	fvexi 6930	. . . . 5 ⊢ 𝐵 ∈ V
286	285	a1i 11	. . . 4 ⊢ (𝜑 → 𝐵 ∈ V)
287	286, 8, 53	elmapdd 8899	. . 3 ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑_m 𝐼))
288	274, 275, 276, 277, 134, 34, 33, 58, 125, 8, 10, 279, 284, 287	evlsvvval 22457	. 2 ⊢ (𝜑 → ((𝑄‘((𝐸‘𝑌)‘𝐹))‘𝐴) = (𝑅 Σ_g (𝑐 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(._g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))))
289		evlextv.o	. . . 4 ⊢ 𝑂 = (𝐽 eval 𝑅)
290	289, 34	evlval 22464	. . 3 ⊢ 𝑂 = ((𝐽 evalSub 𝑅)‘𝐵)
291		eqid 2763	. . 3 ⊢ (𝐽 mPoly (𝑅 ↾_s 𝐵)) = (𝐽 mPoly (𝑅 ↾_s 𝐵))
292		eqid 2763	. . 3 ⊢ (Base‘(𝐽 mPoly (𝑅 ↾_s 𝐵))) = (Base‘(𝐽 mPoly (𝑅 ↾_s 𝐵)))
293	16, 15	eleqtrdi 2874	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (Base‘(𝐽 mPoly 𝑅)))
294	281	oveq2d 7467	. . . . 5 ⊢ (𝜑 → (𝐽 mPoly (𝑅 ↾_s 𝐵)) = (𝐽 mPoly 𝑅))
295	294	fveq2d 6920	. . . 4 ⊢ (𝜑 → (Base‘(𝐽 mPoly (𝑅 ↾_s 𝐵))) = (Base‘(𝐽 mPoly 𝑅)))
296	293, 295	eleqtrrd 2867	. . 3 ⊢ (𝜑 → 𝐹 ∈ (Base‘(𝐽 mPoly (𝑅 ↾_s 𝐵))))
297	287, 169	elmapssresd 8933	. . 3 ⊢ (𝜑 → (𝐴 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
298	290, 291, 292, 277, 159, 34, 33, 58, 125, 170, 10, 279, 296, 297	evlsvvval 22457	. 2 ⊢ (𝜑 → ((𝑂‘𝐹)‘(𝐴 ↾ 𝐽)) = (𝑅 Σ_g (𝑏 ∈ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} ↦ ((𝐹‘𝑏)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(._g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))))
299	272, 288, 298	3eqtr4d 2808	1 ⊢ (𝜑 → ((𝑄‘((𝐸‘𝑌)‘𝐹))‘𝐴) = ((𝑂‘𝐹)‘(𝐴 ↾ 𝐽)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ∉ wnel 3065 {crab 3416 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 ∪ cun 4152 ∅c0 4281 ifcif 4485 {csn 4588 ⟨cop 4840 class class class wbr 5108 ↦ cmpt 5192 dom cdm 5658 ↾ cres 5660 Fun wfun 6560 Fn wfn 6561 ⟶wf 6562 ‘cfv 6566 (class class class)co 7451 ↑_m cmap 8885 finSupp cfsupp 9391 0cc0 11239 ℕ₀cn0 12646 Basecbs 17431 ↾_s cress 17452 ._rcmulr 17473 0_gc0g 17660 Σ_g cgsu 17661 Mndcmnd 18973 ._gcmg 19327 CMndccmn 20045 mulGrpcmgp 20411 1_rcur 20458 Ringcrg 20510 CRingccrg 20511 SubRingcsubrg 20872 mPoly cmpl 22269 eval cevl 22437 extendVarscextv 34272

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-of 7725 df-ofr 7726 df-om 7912 df-1st 8035 df-2nd 8036 df-supp 8215 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-er 8755 df-map 8887 df-pm 8888 df-ixp 8964 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-fsupp 9392 df-sup 9471 df-oi 9541 df-card 10057 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-z 12734 df-dec 12855 df-uz 13006 df-fz 13680 df-fzo 13829 df-seq 14185 df-hash 14516 df-struct 17369 df-sets 17386 df-slot 17404 df-ndx 17416 df-base 17432 df-ress 17453 df-plusg 17486 df-mulr 17487 df-sca 17489 df-vsca 17490 df-ip 17491 df-tset 17492 df-ple 17493 df-ds 17495 df-hom 17497 df-cco 17498 df-0g 17662 df-gsum 17663 df-prds 17668 df-pws 17670 df-mre 17806 df-mrc 17807 df-acs 17809 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-mhm 19028 df-submnd 19029 df-grp 19197 df-minusg 19198 df-sbg 19199 df-mulg 19328 df-subg 19383 df-ghm 19478 df-cntz 19582 df-cmn 20047 df-abl 20048 df-mgp 20412 df-rng 20426 df-ur 20459 df-srg 20464 df-ring 20512 df-cring 20513 df-rhm 20753 df-subrng 20849 df-subrg 20873 df-lmod 21188 df-lss 21258 df-lsp 21298 df-assa 22216 df-asp 22217 df-ascl 22218 df-psr 22272 df-mvr 22273 df-mpl 22274 df-evls 22438 df-evl 22439 df-extv 34273

This theorem is used by: esplyindfv 34319

W3C validator