Theorem evlextv 34052

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 6879	. . . . . . . . . 10 ⊢ (𝐸‘𝑌) = ((𝐼extendVars𝑅)‘𝑌)
3	2	fveq1i 6879	. . . . . . . . 9 ⊢ ((𝐸‘𝑌)‘𝐹) = (((𝐼extendVars𝑅)‘𝑌)‘𝐹)
4	3	fveq1i 6879	. . . . . . . 8 ⊢ (((𝐸‘𝑌)‘𝐹)‘𝑐) = ((((𝐼extendVars𝑅)‘𝑌)‘𝐹)‘𝑐)
5	4	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (((𝐸‘𝑌)‘𝐹)‘𝑐) = ((((𝐼extendVars𝑅)‘𝑌)‘𝐹)‘𝑐))
6		eqid 2760	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
7		eqid 2760	. . . . . . . 8 ⊢ (0g‘𝑅) = (0g‘𝑅)
8		evlextv.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
9	8	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝐼 ∈ 𝑉)
10		evlextv.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ CRing)
11	10	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑅 ∈ CRing)
12		evlextv.y	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ 𝐼)
13	12	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑌 ∈ 𝐼)
14		evlextv.j	. . . . . . . 8 ⊢ 𝐽 = (𝐼 ∖ {𝑌})
15		evlextv.m	. . . . . . . 8 ⊢ 𝑀 = (Base‘(𝐽 mPoly 𝑅))
16		evlextv.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ 𝑀)
17	16	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝐹 ∈ 𝑀)
18		breq1 5106	. . . . . . . . 9 ⊢ (ℎ = 𝑐 → (ℎ finSupp 0 ↔ 𝑐 finSupp 0))
19		ssrab2 4028	. . . . . . . . . . 11 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ⊆ (ℕ0 ↑m 𝐼)
20	19	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ⊆ (ℕ0 ↑m 𝐼))
21	20	sselda 3931	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑐 ∈ (ℕ0 ↑m 𝐼))
22		fveq1 6877	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑐 → (ℎ‘𝑌) = (𝑐‘𝑌))
23	22	eqeq1d 2762	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑐 → ((ℎ‘𝑌) = 0 ↔ (𝑐‘𝑌) = 0))
24	18, 23	anbi12d 644	. . . . . . . . . . 11 ⊢ (ℎ = 𝑐 → ((ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0) ↔ (𝑐 finSupp 0 ∧ (𝑐‘𝑌) = 0)))
25		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})
26	24, 25	elrabrd 3648	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑐 finSupp 0 ∧ (𝑐‘𝑌) = 0))
27	26	simpld 500	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑐 finSupp 0)
28	18, 21, 27	elrabd 3647	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
29	6, 7, 9, 11, 13, 14, 15, 17, 28	extvfvv 34044	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → ((((𝐼extendVars𝑅)‘𝑌)‘𝐹)‘𝑐) = if((𝑐‘𝑌) = 0, (𝐹‘(𝑐 ↾ 𝐽)), (0g‘𝑅)))
30	26	simprd 501	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑐‘𝑌) = 0)
31	30	iftrued 4490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → if((𝑐‘𝑌) = 0, (𝐹‘(𝑐 ↾ 𝐽)), (0g‘𝑅)) = (𝐹‘(𝑐 ↾ 𝐽)))
32	5, 29, 31	3eqtrd 2799	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (((𝐸‘𝑌)‘𝐹)‘𝑐) = (𝐹‘(𝑐 ↾ 𝐽)))
33		eqid 2760	. . . . . . . . 9 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
34		evlextv.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝑅)
35	33, 34	mgpbas 20278	. . . . . . . 8 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
36		eqid 2760	. . . . . . . . 9 ⊢ (1r‘𝑅) = (1r‘𝑅)
37	33, 36	ringidval 20322	. . . . . . . 8 ⊢ (1r‘𝑅) = (0g‘(mulGrp‘𝑅))
38	33	crngmgp 20380	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
39	11, 38	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (mulGrp‘𝑅) ∈ CMnd)
40		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → 𝑖 ∈ (𝐼 ∖ 𝐽))
41	14	difeq2i 4071	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∖ 𝐽) = (𝐼 ∖ (𝐼 ∖ {𝑌}))
42	12	snssd 4747	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {𝑌} ⊆ 𝐼)
43		dfss4 4215	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑌} ⊆ 𝐼 ↔ (𝐼 ∖ (𝐼 ∖ {𝑌})) = {𝑌})
44	42, 43	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐼 ∖ (𝐼 ∖ {𝑌})) = {𝑌})
45	41, 44	eqtrid 2807	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐼 ∖ 𝐽) = {𝑌})
46	45	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (𝐼 ∖ 𝐽) = {𝑌})
47	40, 46	eleqtrd 2862	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → 𝑖 ∈ {𝑌})
48	47	elsnd 4602	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → 𝑖 = 𝑌)
49	48	fveq2d 6882	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (𝑐‘𝑖) = (𝑐‘𝑌))
50	30	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (𝑐‘𝑌) = 0)
51	49, 50	eqtrd 2795	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (𝑐‘𝑖) = 0)
52	51	oveq1d 7428	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)) = (0(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)))
53		evlextv.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴:𝐼⟶𝐵)
54	53	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → 𝐴:𝐼⟶𝐵)
55		difssd 4084	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝐼 ∖ 𝐽) ⊆ 𝐼)
56	55	sselda 3931	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → 𝑖 ∈ 𝐼)
57	54, 56	ffvelcdmd 7078	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (𝐴‘𝑖) ∈ 𝐵)
58		eqid 2760	. . . . . . . . . . 11 ⊢ (.g‘(mulGrp‘𝑅)) = (.g‘(mulGrp‘𝑅))
59	35, 37, 58	mulg0 19197	. . . . . . . . . 10 ⊢ ((𝐴‘𝑖) ∈ 𝐵 → (0(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)) = (1r‘𝑅))
60	57, 59	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → (0(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)) = (1r‘𝑅))
61	52, 60	eqtrd 2795	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ (𝐼 ∖ 𝐽)) → ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)) = (1r‘𝑅))
62		fvexd 6893	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (1r‘𝑅) ∈ V)
63		0nn0 12543	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
64	63	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 0 ∈ ℕ0)
65	8	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
66		ssidd 3954	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ⊆ 𝐼)
67	53	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐴:𝐼⟶𝐵)
68	67	ffvelcdmda 7077	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐼) → (𝐴‘𝑖) ∈ 𝐵)
69		ssrab2 4028	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼)
70	69	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼))
71	70	sselda 3931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑐 ∈ (ℕ0 ↑m 𝐼))
72	71	elmaprd 8849	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑐:𝐼⟶ℕ0)
73		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
74	18, 73	elrabrd 3648	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑐 finSupp 0)
75	35, 37, 58	mulg0 19197	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → (0(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅))
76	75	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑥 ∈ 𝐵) → (0(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅))
77	62, 64, 65, 66, 68, 72, 74, 76	fisuppov1 33155	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))) finSupp (1r‘𝑅))
78	28, 77	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))) finSupp (1r‘𝑅))
79	10, 38	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
80	79	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (mulGrp‘𝑅) ∈ CMnd)
81	80	cmnmndd 19931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (mulGrp‘𝑅) ∈ Mnd)
82	81	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐼) → (mulGrp‘𝑅) ∈ Mnd)
83	72	ffvelcdmda 7077	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐼) → (𝑐‘𝑖) ∈ ℕ0)
84	35, 58, 82, 83, 68	mulgnn0cld 19218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐼) → ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)) ∈ 𝐵)
85	28, 84	syldanl 614	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ 𝐼) → ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)) ∈ 𝐵)
86		difss 4083	. . . . . . . . . 10 ⊢ (𝐼 ∖ {𝑌}) ⊆ 𝐼
87	14, 86	eqsstri 3977	. . . . . . . . 9 ⊢ 𝐽 ⊆ 𝐼
88	87	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝐽 ⊆ 𝐼)
89	35, 37, 39, 9, 61, 78, 85, 88	gsummptfsres 33494	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → ((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)))) = ((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)))))
90		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ 𝐽) → 𝑖 ∈ 𝐽)
91	90	fvresd 6898	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ 𝐽) → ((𝑐 ↾ 𝐽)‘𝑖) = (𝑐‘𝑖))
92	90	fvresd 6898	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ 𝐽) → ((𝐴 ↾ 𝐽)‘𝑖) = (𝐴‘𝑖))
93	91, 92	oveq12d 7431	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑖 ∈ 𝐽) → (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)) = ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)))
94	93	mpteq2dva 5198	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))) = (𝑖 ∈ 𝐽 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))
95	94	oveq2d 7429	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → ((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))) = ((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)))))
96	89, 95	eqtr4d 2798	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → ((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)))) = ((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))))
97	32, 96	oveq12d 7431	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → ((((𝐸‘𝑌)‘𝐹)‘𝑐)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))) = ((𝐹‘(𝑐 ↾ 𝐽))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))
98	97	mpteq2dva 5198	. . . 4 ⊢ (𝜑 → (𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)))))) = (𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((𝐹‘(𝑐 ↾ 𝐽))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))))))
99	98	oveq2d 7429	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))) = (𝑅 Σg (𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((𝐹‘(𝑐 ↾ 𝐽))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))))
100	10	crngringd 20385	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
101	100	ringcmnd 20425	. . . 4 ⊢ (𝜑 → 𝑅 ∈ CMnd)
102		ovex 7446	. . . . . 6 ⊢ (ℕ0 ↑m 𝐼) ∈ V
103	102	rabex 5303	. . . . 5 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V
104	103	a1i 11	. . . 4 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V)
105	4	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → (((𝐸‘𝑌)‘𝐹)‘𝑐) = ((((𝐼extendVars𝑅)‘𝑌)‘𝐹)‘𝑐))
106	8	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝐼 ∈ 𝑉)
107	10	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝑅 ∈ CRing)
108	12	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝑌 ∈ 𝐼)
109	16	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝐹 ∈ 𝑀)
110		difssd 4084	. . . . . . . . 9 ⊢ (𝜑 → ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ⊆ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
111	110	sselda 3931	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
112	6, 7, 106, 107, 108, 14, 15, 109, 111	extvfvv 34044	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ((((𝐼extendVars𝑅)‘𝑌)‘𝐹)‘𝑐) = if((𝑐‘𝑌) = 0, (𝐹‘(𝑐 ↾ 𝐽)), (0g‘𝑅)))
113	111	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
114	69, 113	sselid 3929	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → 𝑐 ∈ (ℕ0 ↑m 𝐼))
115	18, 113	elrabrd 3648	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → 𝑐 finSupp 0)
116		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → (𝑐‘𝑌) = 0)
117	115, 116	jca 521	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → (𝑐 finSupp 0 ∧ (𝑐‘𝑌) = 0))
118	24, 114, 117	elrabd 3647	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})
119		simplr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}))
120	119	eldifbd 3912	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) ∧ (𝑐‘𝑌) = 0) → ¬ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})
121	118, 120	pm2.65da 829	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ¬ (𝑐‘𝑌) = 0)
122	121	iffalsed 4493	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → if((𝑐‘𝑌) = 0, (𝐹‘(𝑐 ↾ 𝐽)), (0g‘𝑅)) = (0g‘𝑅))
123	105, 112, 122	3eqtrd 2799	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → (((𝐸‘𝑌)‘𝐹)‘𝑐) = (0g‘𝑅))
124	123	oveq1d 7428	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ((((𝐸‘𝑌)‘𝐹)‘𝑐)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))) = ((0g‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))
125		eqid 2760	. . . . . 6 ⊢ (.r‘𝑅) = (.r‘𝑅)
126	100	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → 𝑅 ∈ Ring)
127	84	fmpttd 7108	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))):𝐼⟶𝐵)
128	35, 37, 80, 65, 127, 77	gsumcl 20042	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)))) ∈ 𝐵)
129	111, 128	syldan 603	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)))) ∈ 𝐵)
130	34, 125, 7, 126, 129	ringlzd 20437	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ((0g‘𝑅)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))) = (0g‘𝑅))
131	124, 130	eqtrd 2795	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∖ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})) → ((((𝐸‘𝑌)‘𝐹)‘𝑐)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))) = (0g‘𝑅))
132		eqid 2760	. . . . . 6 ⊢ (𝐼 mPoly 𝑅) = (𝐼 mPoly 𝑅)
133		eqid 2760	. . . . . 6 ⊢ (Base‘(𝐼 mPoly 𝑅)) = (Base‘(𝐼 mPoly 𝑅))
134	6	psrbasfsupp 34021	. . . . . 6 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
135	6, 7, 8, 100, 34, 14, 15, 12, 16, 133	extvfvcl 34046	. . . . . . 7 ⊢ (𝜑 → (((𝐼extendVars𝑅)‘𝑌)‘𝐹) ∈ (Base‘(𝐼 mPoly 𝑅)))
136	3, 135	eqeltrid 2864	. . . . . 6 ⊢ (𝜑 → ((𝐸‘𝑌)‘𝐹) ∈ (Base‘(𝐼 mPoly 𝑅)))
137	132, 34, 133, 134, 136	mplelf 22212	. . . . 5 ⊢ (𝜑 → ((𝐸‘𝑌)‘𝐹):{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶𝐵)
138	132, 133, 7, 136	mplelsfi 22209	. . . . 5 ⊢ (𝜑 → ((𝐸‘𝑌)‘𝐹) finSupp (0g‘𝑅))
139	34, 100, 104, 128, 137, 138	rmfsupp2 33677	. . . 4 ⊢ (𝜑 → (𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖)))))) finSupp (0g‘𝑅))
140	100	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑅 ∈ Ring)
141	137	ffvelcdmda 7077	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (((𝐸‘𝑌)‘𝐹)‘𝑐) ∈ 𝐵)
142	34, 125, 140, 141, 128	ringcld 20396	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ((((𝐸‘𝑌)‘𝐹)‘𝑐)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))) ∈ 𝐵)
143		simpl 488	. . . . . 6 ⊢ ((ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0) → ℎ finSupp 0)
144	143	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ (ℕ0 ↑m 𝐼)) → ((ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0) → ℎ finSupp 0))
145	144	ss2rabdv 4023	. . . 4 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ⊆ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
146	34, 7, 101, 104, 131, 139, 142, 145	gsummptfsres 33494	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))) = (𝑅 Σg (𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))))
147		nfcv 2922	. . . 4 ⊢ Ⅎ𝑏((𝐹‘(𝑐 ↾ 𝐽))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))))
148		fveq2 6878	. . . . 5 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → (𝐹‘𝑏) = (𝐹‘(𝑐 ↾ 𝐽)))
149		fveq1 6877	. . . . . . . 8 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → (𝑏‘𝑖) = ((𝑐 ↾ 𝐽)‘𝑖))
150	149	oveq1d 7428	. . . . . . 7 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)) = (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))
151	150	mpteq2dv 5199	. . . . . 6 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))) = (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))
152	151	oveq2d 7429	. . . . 5 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → ((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))) = ((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))))
153	148, 152	oveq12d 7431	. . . 4 ⊢ (𝑏 = (𝑐 ↾ 𝐽) → ((𝐹‘𝑏)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))) = ((𝐹‘(𝑐 ↾ 𝐽))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))
154		ovex 7446	. . . . . 6 ⊢ (ℕ0 ↑m 𝐽) ∈ V
155	154	rabex 5303	. . . . 5 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} ∈ V
156	155	a1i 11	. . . 4 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} ∈ V)
157		eqid 2760	. . . . . . . 8 ⊢ (𝐽 mPoly 𝑅) = (𝐽 mPoly 𝑅)
158		eqid 2760	. . . . . . . . 9 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}
159	158	psrbasfsupp 34021	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ (◡ℎ “ ℕ) ∈ Fin}
160	157, 34, 15, 159, 16	mplelf 22212	. . . . . . 7 ⊢ (𝜑 → 𝐹:{ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}⟶𝐵)
161	160	feqmptd 6946	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} ↦ (𝐹‘𝑏)))
162	157, 15, 7, 16	mplelsfi 22209	. . . . . 6 ⊢ (𝜑 → 𝐹 finSupp (0g‘𝑅))
163	161, 162	eqbrtrrd 5129	. . . . 5 ⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} ↦ (𝐹‘𝑏)) finSupp (0g‘𝑅))
164	100	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ Ring)
165		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
166	34, 125, 7, 164, 165	ringlzd 20437	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((0g‘𝑅)(.r‘𝑅)𝑥) = (0g‘𝑅))
167	160	ffvelcdmda 7077	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝐹‘𝑏) ∈ 𝐵)
168	79	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (mulGrp‘𝑅) ∈ CMnd)
169	87	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ⊆ 𝐼)
170	8, 169	ssexd 5289	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ V)
171	170	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝐽 ∈ V)
172	168	cmnmndd 19931	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (mulGrp‘𝑅) ∈ Mnd)
173	172	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐽) → (mulGrp‘𝑅) ∈ Mnd)
174		ssrab2 4028	. . . . . . . . . . . 12 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐽)
175	174	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐽))
176	175	sselda 3931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝑏 ∈ (ℕ0 ↑m 𝐽))
177	176	elmaprd 8849	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝑏:𝐽⟶ℕ0)
178	177	ffvelcdmda 7077	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐽) → (𝑏‘𝑖) ∈ ℕ0)
179	53	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝐴:𝐼⟶𝐵)
180	87	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝐽 ⊆ 𝐼)
181	179, 180	fssresd 6742	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝐴 ↾ 𝐽):𝐽⟶𝐵)
182	181	ffvelcdmda 7077	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐽) → ((𝐴 ↾ 𝐽)‘𝑖) ∈ 𝐵)
183	35, 58, 173, 178, 182	mulgnn0cld 19218	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑖 ∈ 𝐽) → ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)) ∈ 𝐵)
184	183	fmpttd 7108	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))):𝐽⟶𝐵)
185	177	feqmptd 6946	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝑏 = (𝑖 ∈ 𝐽 ↦ (𝑏‘𝑖)))
186		breq1 5106	. . . . . . . . 9 ⊢ (ℎ = 𝑏 → (ℎ finSupp 0 ↔ 𝑏 finSupp 0))
187		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0})
188	186, 187	elrabrd 3648	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝑏 finSupp 0)
189	185, 188	eqbrtrrd 5129	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝑖 ∈ 𝐽 ↦ (𝑏‘𝑖)) finSupp 0)
190	75	adantl 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑥 ∈ 𝐵) → (0(.g‘(mulGrp‘𝑅))𝑥) = (1r‘𝑅))
191		fvexd 6893	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (1r‘𝑅) ∈ V)
192	189, 190, 178, 182, 191	fsuppssov1 9354	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))) finSupp (1r‘𝑅))
193	35, 37, 168, 171, 184, 192	gsumcl 20042	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → ((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))) ∈ 𝐵)
194		fvexd 6893	. . . . 5 ⊢ (𝜑 → (0g‘𝑅) ∈ V)
195	163, 166, 167, 193, 194	fsuppssov1 9354	. . . 4 ⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} ↦ ((𝐹‘𝑏)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖)))))) finSupp (0g‘𝑅))
196		ssidd 3954	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ 𝐵)
197	100	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝑅 ∈ Ring)
198	34, 125, 197, 167, 193	ringcld 20396	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → ((𝐹‘𝑏)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))) ∈ 𝐵)
199		breq1 5106	. . . . 5 ⊢ (ℎ = (𝑐 ↾ 𝐽) → (ℎ finSupp 0 ↔ (𝑐 ↾ 𝐽) finSupp 0))
200	21, 88	elmapssresd 8874	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑐 ↾ 𝐽) ∈ (ℕ0 ↑m 𝐽))
201	63	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 0 ∈ ℕ0)
202	27, 201	fsuppres 9363	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑐 ↾ 𝐽) finSupp 0)
203	199, 200, 202	elrabd 3647	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑐 ↾ 𝐽) ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0})
204		breq1 5106	. . . . . . 7 ⊢ (ℎ = (𝑏 ∪ {⟨𝑌, 0⟩}) → (ℎ finSupp 0 ↔ (𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0))
205		fveq1 6877	. . . . . . . 8 ⊢ (ℎ = (𝑏 ∪ {⟨𝑌, 0⟩}) → (ℎ‘𝑌) = ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌))
206	205	eqeq1d 2762	. . . . . . 7 ⊢ (ℎ = (𝑏 ∪ {⟨𝑌, 0⟩}) → ((ℎ‘𝑌) = 0 ↔ ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌) = 0))
207	204, 206	anbi12d 644	. . . . . 6 ⊢ (ℎ = (𝑏 ∪ {⟨𝑌, 0⟩}) → ((ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0) ↔ ((𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0 ∧ ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌) = 0)))
208		nn0ex 12534	. . . . . . . 8 ⊢ ℕ0 ∈ V
209	208	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → ℕ0 ∈ V)
210	8	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
211	14	uneq1i 4111	. . . . . . . . . 10 ⊢ (𝐽 ∪ {𝑌}) = ((𝐼 ∖ {𝑌}) ∪ {𝑌})
212		undifr 4439	. . . . . . . . . . 11 ⊢ ({𝑌} ⊆ 𝐼 ↔ ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
213	42, 212	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
214	211, 213	eqtrid 2807	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ∪ {𝑌}) = 𝐼)
215	214	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝐽 ∪ {𝑌}) = 𝐼)
216	63	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ ℕ0)
217	12, 216	fsnd 6862	. . . . . . . . . 10 ⊢ (𝜑 → {⟨𝑌, 0⟩}:{𝑌}⟶ℕ0)
218	217	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → {⟨𝑌, 0⟩}:{𝑌}⟶ℕ0)
219	14	ineq1i 4162	. . . . . . . . . . 11 ⊢ (𝐽 ∩ {𝑌}) = ((𝐼 ∖ {𝑌}) ∩ {𝑌})
220		disjdifr 4427	. . . . . . . . . . 11 ⊢ ((𝐼 ∖ {𝑌}) ∩ {𝑌}) = ∅
221	219, 220	eqtri 2783	. . . . . . . . . 10 ⊢ (𝐽 ∩ {𝑌}) = ∅
222	221	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝐽 ∩ {𝑌}) = ∅)
223	177, 218, 222	fun2d 6739	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝑏 ∪ {⟨𝑌, 0⟩}):(𝐽 ∪ {𝑌})⟶ℕ0)
224	215, 223	feq2dd 6688	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝑏 ∪ {⟨𝑌, 0⟩}):𝐼⟶ℕ0)
225	209, 210, 224	elmapdd 8840	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝑏 ∪ {⟨𝑌, 0⟩}) ∈ (ℕ0 ↑m 𝐼))
226	12, 63	jctir 530	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ0))
227	226	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ0))
228	177	ffund 6707	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → Fun 𝑏)
229		neldifsnd 4756	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝐼 ∖ {𝑌}))
230	14	eleq2i 2852	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ 𝐽 ↔ 𝑌 ∈ (𝐼 ∖ {𝑌}))
231	229, 230	sylnibr 332	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑌 ∈ 𝐽)
232	231	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → ¬ 𝑌 ∈ 𝐽)
233	177	fdmd 6713	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → dom 𝑏 = 𝐽)
234	232, 233	neleqtrrd 2883	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → ¬ 𝑌 ∈ dom 𝑏)
235		df-nel 3062	. . . . . . . . . 10 ⊢ (𝑌 ∉ dom 𝑏 ↔ ¬ 𝑌 ∈ dom 𝑏)
236	234, 235	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝑌 ∉ dom 𝑏)
237	228, 236	jca 521	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (Fun 𝑏 ∧ 𝑌 ∉ dom 𝑏))
238		funsnfsupp 9362	. . . . . . . . 9 ⊢ (((𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ0) ∧ (Fun 𝑏 ∧ 𝑌 ∉ dom 𝑏)) → ((𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0 ↔ 𝑏 finSupp 0))
239	238	biimpar 483	. . . . . . . 8 ⊢ ((((𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ0) ∧ (Fun 𝑏 ∧ 𝑌 ∉ dom 𝑏)) ∧ 𝑏 finSupp 0) → (𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0)
240	227, 237, 188, 239	syl21anc 851	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0)
241	12	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 𝑌 ∈ 𝐼)
242	63	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → 0 ∈ ℕ0)
243		fsnunfv 7185	. . . . . . . 8 ⊢ ((𝑌 ∈ 𝐼 ∧ 0 ∈ ℕ0 ∧ ¬ 𝑌 ∈ dom 𝑏) → ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌) = 0)
244	241, 242, 234, 243	syl3anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌) = 0)
245	240, 244	jca 521	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → ((𝑏 ∪ {⟨𝑌, 0⟩}) finSupp 0 ∧ ((𝑏 ∪ {⟨𝑌, 0⟩})‘𝑌) = 0))
246	207, 225, 245	elrabd 3647	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → (𝑏 ∪ {⟨𝑌, 0⟩}) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)})
247		simpr 490	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → 𝑏 = (𝑐 ↾ 𝐽))
248	247	uneq1d 4114	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → (𝑏 ∪ {⟨𝑌, 0⟩}) = ((𝑐 ↾ 𝐽) ∪ {⟨𝑌, 0⟩}))
249	14	reseq2i 5969	. . . . . . . . 9 ⊢ (𝑐 ↾ 𝐽) = (𝑐 ↾ (𝐼 ∖ {𝑌}))
250	249	uneq1i 4111	. . . . . . . 8 ⊢ ((𝑐 ↾ 𝐽) ∪ {⟨𝑌, 0⟩}) = ((𝑐 ↾ (𝐼 ∖ {𝑌})) ∪ {⟨𝑌, 0⟩})
251	250	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → ((𝑐 ↾ 𝐽) ∪ {⟨𝑌, 0⟩}) = ((𝑐 ↾ (𝐼 ∖ {𝑌})) ∪ {⟨𝑌, 0⟩}))
252	21	elmaprd 8849	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → 𝑐:𝐼⟶ℕ0)
253	252	ad4ant13 764	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → 𝑐:𝐼⟶ℕ0)
254	253	ffnd 6703	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → 𝑐 Fn 𝐼)
255	241	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → 𝑌 ∈ 𝐼)
256	26	ad4ant13 764	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → (𝑐 finSupp 0 ∧ (𝑐‘𝑌) = 0))
257	256	simprd 501	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → (𝑐‘𝑌) = 0)
258		fresunsn 33098	. . . . . . . 8 ⊢ ((𝑐 Fn 𝐼 ∧ 𝑌 ∈ 𝐼 ∧ (𝑐‘𝑌) = 0) → ((𝑐 ↾ (𝐼 ∖ {𝑌})) ∪ {⟨𝑌, 0⟩}) = 𝑐)
259	254, 255, 257, 258	syl3anc 1398	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → ((𝑐 ↾ (𝐼 ∖ {𝑌})) ∪ {⟨𝑌, 0⟩}) = 𝑐)
260	248, 251, 259	3eqtrrd 2800	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑏 = (𝑐 ↾ 𝐽)) → 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩}))
261		simpr 490	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩}))
262	261	reseq1d 5971	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → (𝑐 ↾ 𝐽) = ((𝑏 ∪ {⟨𝑌, 0⟩}) ↾ 𝐽))
263	177	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → 𝑏:𝐽⟶ℕ0)
264	263	ffnd 6703	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → 𝑏 Fn 𝐽)
265	232	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → ¬ 𝑌 ∈ 𝐽)
266		fsnunres 7186	. . . . . . . 8 ⊢ ((𝑏 Fn 𝐽 ∧ ¬ 𝑌 ∈ 𝐽) → ((𝑏 ∪ {⟨𝑌, 0⟩}) ↾ 𝐽) = 𝑏)
267	264, 265, 266	syl2anc 596	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → ((𝑏 ∪ {⟨𝑌, 0⟩}) ↾ 𝐽) = 𝑏)
268	262, 267	eqtr2d 2796	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) ∧ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})) → 𝑏 = (𝑐 ↾ 𝐽))
269	260, 268	impbida 813	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) ∧ 𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}) → (𝑏 = (𝑐 ↾ 𝐽) ↔ 𝑐 = (𝑏 ∪ {⟨𝑌, 0⟩})))
270	246, 269	reu6dv 32948	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0}) → ∃!𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)}𝑏 = (𝑐 ↾ 𝐽))
271	147, 34, 7, 153, 101, 156, 195, 196, 198, 203, 270	gsummptfsf1o 33500	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} ↦ ((𝐹‘𝑏)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))) = (𝑅 Σg (𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (ℎ finSupp 0 ∧ (ℎ‘𝑌) = 0)} ↦ ((𝐹‘(𝑐 ↾ 𝐽))(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ (((𝑐 ↾ 𝐽)‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))))
272	99, 146, 271	3eqtr4d 2805	. 2 ⊢ (𝜑 → (𝑅 Σg (𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))) = (𝑅 Σg (𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} ↦ ((𝐹‘𝑏)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))))
273		evlextv.q	. . . 4 ⊢ 𝑄 = (𝐼 eval 𝑅)
274	273, 34	evlval 22316	. . 3 ⊢ 𝑄 = ((𝐼 evalSub 𝑅)‘𝐵)
275		eqid 2760	. . 3 ⊢ (𝐼 mPoly (𝑅 ↾s 𝐵)) = (𝐼 mPoly (𝑅 ↾s 𝐵))
276		eqid 2760	. . 3 ⊢ (Base‘(𝐼 mPoly (𝑅 ↾s 𝐵))) = (Base‘(𝐼 mPoly (𝑅 ↾s 𝐵)))
277		eqid 2760	. . 3 ⊢ (𝑅 ↾s 𝐵) = (𝑅 ↾s 𝐵)
278	34	subrgid 20735	. . . 4 ⊢ (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅))
279	100, 278	syl 18	. . 3 ⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅))
280	34	ressid 17336	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (𝑅 ↾s 𝐵) = 𝑅)
281	10, 280	syl 18	. . . . . 6 ⊢ (𝜑 → (𝑅 ↾s 𝐵) = 𝑅)
282	281	oveq2d 7429	. . . . 5 ⊢ (𝜑 → (𝐼 mPoly (𝑅 ↾s 𝐵)) = (𝐼 mPoly 𝑅))
283	282	fveq2d 6882	. . . 4 ⊢ (𝜑 → (Base‘(𝐼 mPoly (𝑅 ↾s 𝐵))) = (Base‘(𝐼 mPoly 𝑅)))
284	136, 283	eleqtrrd 2863	. . 3 ⊢ (𝜑 → ((𝐸‘𝑌)‘𝐹) ∈ (Base‘(𝐼 mPoly (𝑅 ↾s 𝐵))))
285	34	fvexi 6892	. . . . 5 ⊢ 𝐵 ∈ V
286	285	a1i 11	. . . 4 ⊢ (𝜑 → 𝐵 ∈ V)
287	286, 8, 53	elmapdd 8840	. . 3 ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m 𝐼))
288	274, 275, 276, 277, 134, 34, 33, 58, 125, 8, 10, 279, 284, 287	evlsvvval 22309	. 2 ⊢ (𝜑 → ((𝑄‘((𝐸‘𝑌)‘𝐹))‘𝐴) = (𝑅 Σg (𝑐 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((((𝐸‘𝑌)‘𝐹)‘𝑐)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐼 ↦ ((𝑐‘𝑖)(.g‘(mulGrp‘𝑅))(𝐴‘𝑖))))))))
289		evlextv.o	. . . 4 ⊢ 𝑂 = (𝐽 eval 𝑅)
290	289, 34	evlval 22316	. . 3 ⊢ 𝑂 = ((𝐽 evalSub 𝑅)‘𝐵)
291		eqid 2760	. . 3 ⊢ (𝐽 mPoly (𝑅 ↾s 𝐵)) = (𝐽 mPoly (𝑅 ↾s 𝐵))
292		eqid 2760	. . 3 ⊢ (Base‘(𝐽 mPoly (𝑅 ↾s 𝐵))) = (Base‘(𝐽 mPoly (𝑅 ↾s 𝐵)))
293	16, 15	eleqtrdi 2870	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (Base‘(𝐽 mPoly 𝑅)))
294	281	oveq2d 7429	. . . . 5 ⊢ (𝜑 → (𝐽 mPoly (𝑅 ↾s 𝐵)) = (𝐽 mPoly 𝑅))
295	294	fveq2d 6882	. . . 4 ⊢ (𝜑 → (Base‘(𝐽 mPoly (𝑅 ↾s 𝐵))) = (Base‘(𝐽 mPoly 𝑅)))
296	293, 295	eleqtrrd 2863	. . 3 ⊢ (𝜑 → 𝐹 ∈ (Base‘(𝐽 mPoly (𝑅 ↾s 𝐵))))
297	287, 169	elmapssresd 8874	. . 3 ⊢ (𝜑 → (𝐴 ↾ 𝐽) ∈ (𝐵 ↑m 𝐽))
298	290, 291, 292, 277, 159, 34, 33, 58, 125, 170, 10, 279, 296, 297	evlsvvval 22309	. 2 ⊢ (𝜑 → ((𝑂‘𝐹)‘(𝐴 ↾ 𝐽)) = (𝑅 Σg (𝑏 ∈ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ ℎ finSupp 0} ↦ ((𝐹‘𝑏)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑖 ∈ 𝐽 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘𝑅))((𝐴 ↾ 𝐽)‘𝑖))))))))
299	272, 288, 298	3eqtr4d 2805	1 ⊢ (𝜑 → ((𝑄‘((𝐸‘𝑌)‘𝐹))‘𝐴) = ((𝑂‘𝐹)‘(𝐴 ↾ 𝐽)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ∉ wnel 3061  {crab 3412  Vcvv 3450   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  ifcif 4482  {csn 4584  ⟨cop 4590   class class class wbr 5103   ↦ cmpt 5186  dom cdm 5655   ↾ cres 5657  Fun wfun 6527   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533  (class class class)co 7413   ↑_m cmap 8826   finSupp cfsupp 9331  0cc0 11124  ℕ₀cn0 12528  Basecbs 17301   ↾_s cress 17322  ._rcmulr 17343  0_gc0g 17524   Σ_g cgsu 17525  Mndcmnd 18836  ._gcmg 19190  CMndccmn 19907  mulGrpcmgp 20273  1_rcur 20320  Ringcrg 20372  CRingccrg 20373  SubRingcsubrg 20731   mPoly cmpl 22121   eval cevl 22289  extendVarscextv 34039

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7678  df-ofr 7679  df-om 7863  df-1st 7986  df-2nd 7987  df-supp 8159  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-er 8696  df-map 8828  df-pm 8829  df-ixp 8905  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-fsupp 9332  df-sup 9412  df-oi 9482  df-card 9944  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-nn 12258  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12529  df-z 12616  df-dec 12737  df-uz 12888  df-fz 13562  df-fzo 13710  df-seq 14066  df-hash 14395  df-struct 17239  df-sets 17256  df-slot 17274  df-ndx 17286  df-base 17302  df-ress 17323  df-plusg 17355  df-mulr 17356  df-sca 17358  df-vsca 17359  df-ip 17360  df-tset 17361  df-ple 17362  df-ds 17364  df-hom 17366  df-cco 17367  df-0g 17526  df-gsum 17527  df-prds 17532  df-pws 17534  df-mre 17670  df-mrc 17671  df-acs 17673  df-mgm 18730  df-sgrp 18821  df-mnd 18837  df-mhm 18891  df-submnd 18892  df-grp 19060  df-minusg 19061  df-sbg 19062  df-mulg 19191  df-subg 19246  df-ghm 19341  df-cntz 19444  df-cmn 19909  df-abl 19910  df-mgp 20274  df-rng 20288  df-ur 20321  df-srg 20326  df-ring 20374  df-cring 20375  df-rhm 20613  df-subrng 20708  df-subrg 20732  df-lmod 21046  df-lss 21116  df-lsp 21156  df-assa 22068  df-asp 22069  df-ascl 22070  df-psr 22124  df-mvr 22125  df-mpl 22126  df-evls 22290  df-evl 22291  df-extv 34040

This theorem is used by:  esplyindfv  34086