extdgfialglem2 - Mathbox for Thierry Arnoux

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

Theorem extdgfialglem2 34372

Description: Lemma for extdgfialg 34373. (Contributed by Thierry Arnoux, 10-Jan-2026.)

**Hypotheses**
Ref	Expression
extdgfialg.b	⊢ 𝐵 = (Base‘𝐸)
extdgfialg.d	⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹))
extdgfialg.e	⊢ (𝜑 → 𝐸 ∈ Field)
extdgfialg.f	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
extdgfialg.1	⊢ (𝜑 → 𝐷 ∈ ℕ₀)
extdgfialglem1.2	⊢ 𝑍 = (0_g‘𝐸)
extdgfialglem1.3	⊢ · = (._r‘𝐸)
extdgfialglem1.r	⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
extdgfialglem1.4	⊢ (𝜑 → 𝑋 ∈ 𝐵)
extdgfialglem2.1	⊢ (𝜑 → 𝐴:(0...𝐷)⟶𝐹)
extdgfialglem2.2	⊢ (𝜑 → 𝐴 finSupp 𝑍)
extdgfialglem2.3	⊢ (𝜑 → (𝐸 Σ_g (𝐴 ∘_f · 𝐺)) = 𝑍)
extdgfialglem2.4	⊢ (𝜑 → 𝐴 ≠ ((0...𝐷) × {𝑍}))

**Assertion**
Ref	Expression
extdgfialglem2	⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))

Distinct variable groups: · ,𝑛 𝐴,𝑛 𝐵,𝑛 𝐷,𝑛 𝑛,𝐸 𝑛,𝐹 𝑛,𝐺 𝑛,𝑋 𝑛,𝑍 𝜑,𝑛

Proof of Theorem extdgfialglem2 Dummy variables 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2760	. 2 ⊢ (𝐸 evalSub₁ 𝐹) = (𝐸 evalSub₁ 𝐹)
2		eqid 2760	. 2 ⊢ (0_g‘(Poly₁‘𝐸)) = (0_g‘(Poly₁‘𝐸))
3		extdgfialglem1.2	. 2 ⊢ 𝑍 = (0_g‘𝐸)
4		extdgfialg.e	. 2 ⊢ (𝜑 → 𝐸 ∈ Field)
5		extdgfialg.f	. 2 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
6		extdgfialg.b	. 2 ⊢ 𝐵 = (Base‘𝐸)
7		eqid 2760	. . . 4 ⊢ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Base‘(Poly₁‘(𝐸 ↾_s 𝐹)))
8		eqid 2760	. . . 4 ⊢ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹)))
9		sdrgsubrg 21054	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
10	5, 9	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
11		eqid 2760	. . . . . . . 8 ⊢ (𝐸 ↾_s 𝐹) = (𝐸 ↾_s 𝐹)
12	11	subrgring 20832	. . . . . . 7 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (𝐸 ↾_s 𝐹) ∈ Ring)
13	10, 12	syl 18	. . . . . 6 ⊢ (𝜑 → (𝐸 ↾_s 𝐹) ∈ Ring)
14		eqid 2760	. . . . . . 7 ⊢ (Poly₁‘(𝐸 ↾_s 𝐹)) = (Poly₁‘(𝐸 ↾_s 𝐹))
15	14	ply1ring 22571	. . . . . 6 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring)
16	13, 15	syl 18	. . . . 5 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring)
17	16	ringcmnd 20519	. . . 4 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ CMnd)
18		fzfid 14120	. . . 4 ⊢ (𝜑 → (0...𝐷) ∈ Fin)
19		eqid 2760	. . . . . 6 ⊢ (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))
20		eqid 2760	. . . . . 6 ⊢ ( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹))) = ( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))
21		eqid 2760	. . . . . 6 ⊢ (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
22	14	ply1lmod 22575	. . . . . . . 8 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
23	13, 22	syl 18	. . . . . . 7 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
24	23	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
25		extdgfialglem2.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴:(0...𝐷)⟶𝐹)
26	25	ffvelcdmda 7085	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) ∈ 𝐹)
27	6	sdrgss 21056	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝐵)
28	5, 27	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
29	11, 6	ressbas2 17422	. . . . . . . . . 10 ⊢ (𝐹 ⊆ 𝐵 → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
30	28, 29	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
31		ovex 7454	. . . . . . . . . . 11 ⊢ (𝐸 ↾_s 𝐹) ∈ V
32	14	ply1sca 22576	. . . . . . . . . . 11 ⊢ ((𝐸 ↾_s 𝐹) ∈ V → (𝐸 ↾_s 𝐹) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
33	31, 32	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐸 ↾_s 𝐹) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))
34	33	fveq2i 6889	. . . . . . . . 9 ⊢ (Base‘(𝐸 ↾_s 𝐹)) = (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
35	30, 34	eqtr2di 2812	. . . . . . . 8 ⊢ (𝜑 → (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = 𝐹)
36	35	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = 𝐹)
37	26, 36	eleqtrrd 2863	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) ∈ (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))))
38		eqid 2760	. . . . . . . 8 ⊢ (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹)))
39	38, 7	mgpbas 20371	. . . . . . 7 ⊢ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Base‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))
40		eqid 2760	. . . . . . 7 ⊢ (._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = (._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))
41	38	ringmgp 20471	. . . . . . . . 9 ⊢ ((Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
42	16, 41	syl 18	. . . . . . . 8 ⊢ (𝜑 → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
43	42	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
44		fz0ssnn0 13760	. . . . . . . . 9 ⊢ (0...𝐷) ⊆ ℕ₀
45	44	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (0...𝐷) ⊆ ℕ₀)
46	45	sselda 3908	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ₀)
47		eqid 2760	. . . . . . . . . 10 ⊢ (var₁‘(𝐸 ↾_s 𝐹)) = (var₁‘(𝐸 ↾_s 𝐹))
48	47, 14, 7	vr1cl 22541	. . . . . . . . 9 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
49	13, 48	syl 18	. . . . . . . 8 ⊢ (𝜑 → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
50	49	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
51	39, 40, 43, 46, 50	mulgnn0cld 19311	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
52	7, 19, 20, 21, 24, 37, 51	lmodvscld 21160	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
53	52	fmpttd 7116	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))):(0...𝐷)⟶(Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
54		eqid 2760	. . . . 5 ⊢ (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
55		fvexd 6901	. . . . 5 ⊢ (𝜑 → (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ V)
56	54, 18, 52, 55	fsuppmptdm 9372	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) finSupp (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
57	7, 8, 17, 18, 53, 56	gsumcl 20135	. . 3 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
58	4	fldcrngd 21001	. . . 4 ⊢ (𝜑 → 𝐸 ∈ CRing)
59	1, 14, 7, 58, 10	evls1dm 34140	. . 3 ⊢ (𝜑 → dom (𝐸 evalSub₁ 𝐹) = (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
60	57, 59	eleqtrrd 2863	. 2 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ∈ dom (𝐸 evalSub₁ 𝐹))
61		extdgfialglem2.4	. . 3 ⊢ (𝜑 → 𝐴 ≠ ((0...𝐷) × {𝑍}))
62		eqid 2760	. . . . . 6 ⊢ (Base‘(𝐸 ↾_s 𝐹)) = (Base‘(𝐸 ↾_s 𝐹))
63		eqid 2760	. . . . . 6 ⊢ (0_g‘(𝐸 ↾_s 𝐹)) = (0_g‘(𝐸 ↾_s 𝐹))
64	25	ffvelcdmda 7085	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ 𝐹)
65	64	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ 𝐹)
66	30	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
67	65, 66	eleqtrd 2862	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ (Base‘(𝐸 ↾_s 𝐹)))
68		subrgsubg 20835	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
69	10, 68	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
70	3	subg0cl 19350	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝑍 ∈ 𝐹)
71	69, 70	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝐹)
72	71, 30	eleqtrd 2862	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
73	72	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ ¬ 𝑚 ∈ (0...𝐷)) → 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
74	67, 73	ifclda 4517	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) ∈ (Base‘(𝐸 ↾_s 𝐹)))
75	74	ralrimiva 3154	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) ∈ (Base‘(𝐸 ↾_s 𝐹)))
76		eqid 2760	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) = (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍))
77		nn0ex 12616	. . . . . . . . 9 ⊢ ℕ₀ ∈ V
78	77	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℕ₀ ∈ V)
79	76, 78, 18, 64, 71	mptiffisupp 33334	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) finSupp 𝑍)
80	58	crngringd 20479	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ Ring)
81	80	ringcmnd 20519	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ CMnd)
82	81	cmnmndd 20024	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Mnd)
83	11, 6, 3	ress0g 18960	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ 𝑍 ∈ 𝐹 ∧ 𝐹 ⊆ 𝐵) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
84	82, 71, 28, 83	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
85	79, 84	breqtrd 5130	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) finSupp (0_g‘(𝐸 ↾_s 𝐹)))
86	72	ralrimivw 3158	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ₀ 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
87		fconstmpt 5712	. . . . . . . 8 ⊢ (ℕ₀ × {𝑍}) = (𝑚 ∈ ℕ₀ ↦ 𝑍)
88	78, 71	fczfsuppd 9382	. . . . . . . 8 ⊢ (𝜑 → (ℕ₀ × {𝑍}) finSupp 𝑍)
89	87, 88	eqbrtrrid 5140	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ 𝑍) finSupp 𝑍)
90	89, 84	breqtrd 5130	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ 𝑍) finSupp (0_g‘(𝐸 ↾_s 𝐹)))
91		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑚 ∈ (ℕ₀ ∖ (0...𝐷)))
92	91	eldifbd 4052	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → ¬ 𝑚 ∈ (0...𝐷))
93	92	iffalsed 4492	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍)
94	84	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
95	93, 94	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = (0_g‘(𝐸 ↾_s 𝐹)))
96	95	oveq1d 7436	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
97	23	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
98	42	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
99	91	eldifad 4051	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑚 ∈ ℕ₀)
100	49	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
101	39, 40, 98, 99, 100	mulgnn0cld 19311	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
102	7, 33, 20, 63, 8	lmod0vs 21176	. . . . . . . . . 10 ⊢ (((Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod ∧ (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹)))) → ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
103	97, 101, 102	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
104	96, 103	eqtrd 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
105	23	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
106	42	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
107		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → 𝑚 ∈ ℕ₀)
108	49	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
109	39, 40, 106, 107, 108	mulgnn0cld 19311	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
110	7, 33, 20, 62, 105, 74, 109	lmodvscld 21160	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
111	7, 8, 17, 78, 104, 18, 110, 45	gsummptres2 33661	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ (0...𝐷) ↦ (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))))
112		eleq1w 2843	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (0...𝐷) ↔ 𝑛 ∈ (0...𝐷)))
113		fveq2 6886	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝐴‘𝑚) = (𝐴‘𝑛))
114	112, 113	ifbieq1d 4506	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍))
115		oveq1 7428	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) = (𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))
116	114, 115	oveq12d 7439	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
117	116	cbvmptv 5208	. . . . . . . . 9 ⊢ (𝑚 ∈ (0...𝐷) ↦ (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
118		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ (0...𝐷))
119	118	iftrued 4489	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = (𝐴‘𝑛))
120	119	oveq1d 7436	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
121	120	mpteq2dva 5197	. . . . . . . . 9 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))))
122	117, 121	eqtrid 2807	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ (0...𝐷) ↦ (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))))
123	122	oveq2d 7437	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ (0...𝐷) ↦ (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))))
124	111, 123	eqtr2d 2796	. . . . . 6 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))))
125	17	cmnmndd 20024	. . . . . . . 8 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Mnd)
126	8	gsumz 19038	. . . . . . . 8 ⊢ (((Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Mnd ∧ ℕ₀ ∈ V) → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
127	125, 78, 126	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
128	84	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
129	128	oveq1d 7436	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
130	105, 109, 102	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
131	129, 130	eqtrd 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
132	131	mpteq2dva 5197	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹)))))
133	132	oveq2d 7437	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))))
134		eqid 2760	. . . . . . . 8 ⊢ (Poly₁‘𝐸) = (Poly₁‘𝐸)
135	134, 11, 14, 7, 10, 2	ressply10g 34146	. . . . . . 7 ⊢ (𝜑 → (0_g‘(Poly₁‘𝐸)) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
136	127, 133, 135	3eqtr4rd 2806	. . . . . 6 ⊢ (𝜑 → (0_g‘(Poly₁‘𝐸)) = ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))))
137	14, 47, 40, 13, 62, 20, 63, 75, 85, 86, 90, 124, 136	gsumply1eq 22633	. . . . 5 ⊢ (𝜑 → (((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (0_g‘(Poly₁‘𝐸)) ↔ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍))
138	25	ffnd 6711	. . . . . . . 8 ⊢ (𝜑 → 𝐴 Fn (0...𝐷))
139	138	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → 𝐴 Fn (0...𝐷))
140	119	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = (𝐴‘𝑛))
141	114	eqeq1d 2762	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍 ↔ if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = 𝑍))
142		simplr 781	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍)
143	44	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → (0...𝐷) ⊆ ℕ₀)
144	143	sselda 3908	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ₀)
145	141, 142, 144	rspcdva 3577	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = 𝑍)
146	140, 145	eqtr3d 2797	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) = 𝑍)
147	139, 146	fconst7v 33262	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → 𝐴 = ((0...𝐷) × {𝑍}))
148	147	ex 418	. . . . 5 ⊢ (𝜑 → (∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍 → 𝐴 = ((0...𝐷) × {𝑍})))
149	137, 148	sylbid 243	. . . 4 ⊢ (𝜑 → (((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (0_g‘(Poly₁‘𝐸)) → 𝐴 = ((0...𝐷) × {𝑍})))
150	149	necon3d 2976	. . 3 ⊢ (𝜑 → (𝐴 ≠ ((0...𝐷) × {𝑍}) → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ≠ (0_g‘(Poly₁‘𝐸))))
151	61, 150	mpd 16	. 2 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ≠ (0_g‘(Poly₁‘𝐸)))
152		eqid 2760	. . . . 5 ⊢ (𝐸 ↑_s 𝐵) = (𝐸 ↑_s 𝐵)
153	1, 6, 14, 8, 11, 152, 7, 58, 10, 52, 45, 56	evls1gsumadd 22648	. . . 4 ⊢ (𝜑 → ((𝐸 evalSub₁ 𝐹)‘((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))))) = ((𝐸 ↑_s 𝐵) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))))))
154	153	fveq1d 6888	. . 3 ⊢ (𝜑 → (((𝐸 evalSub₁ 𝐹)‘((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))))‘𝑋) = (((𝐸 ↑_s 𝐵) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))))‘𝑋))
155	58	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝐸 ∈ CRing)
156	10	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝐹 ∈ (SubRing‘𝐸))
157	1, 14, 7, 155, 156, 6, 52	evls1fvf 34141	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))):𝐵⟶𝐵)
158	157	feqmptd 6954	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)))
159	158	mpteq2dva 5197	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))))
160	159	oveq2d 7437	. . . . . 6 ⊢ (𝜑 → ((𝐸 ↑_s 𝐵) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))))) = ((𝐸 ↑_s 𝐵) Σ_g (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)))))
161	160	fveq1d 6888	. . . . 5 ⊢ (𝜑 → (((𝐸 ↑_s 𝐵) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))))‘𝑋) = (((𝐸 ↑_s 𝐵) Σ_g (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))))‘𝑋))
162		eqid 2760	. . . . . . 7 ⊢ (0_g‘(𝐸 ↑_s 𝐵)) = (0_g‘(𝐸 ↑_s 𝐵))
163	6	fvexi 6900	. . . . . . . 8 ⊢ 𝐵 ∈ V
164	163	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ V)
165	155	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝐸 ∈ CRing)
166	156	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝐹 ∈ (SubRing‘𝐸))
167		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
168	52	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
169	1, 14, 6, 7, 165, 166, 167, 168	evls1fvcl 22699	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
170	169	an32s 665	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (0...𝐷)) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
171	170	anasss 472	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑛 ∈ (0...𝐷))) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
172		eqid 2760	. . . . . . . 8 ⊢ (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))) = (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)))
173	163	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝐵 ∈ V)
174	173	mptexd 7231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)) ∈ V)
175		fvexd 6901	. . . . . . . 8 ⊢ (𝜑 → (0_g‘(𝐸 ↑_s 𝐵)) ∈ V)
176	172, 18, 174, 175	fsuppmptdm 9372	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))) finSupp (0_g‘(𝐸 ↑_s 𝐵)))
177	152, 6, 162, 164, 18, 81, 171, 176	pwsgsum 20202	. . . . . 6 ⊢ (𝜑 → ((𝐸 ↑_s 𝐵) Σ_g (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)))) = (𝑥 ∈ 𝐵 ↦ (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)))))
178	177	fveq1d 6888	. . . . 5 ⊢ (𝜑 → (((𝐸 ↑_s 𝐵) Σ_g (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))))‘𝑋) = ((𝑥 ∈ 𝐵 ↦ (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))))‘𝑋))
179	161, 178	eqtrd 2795	. . . 4 ⊢ (𝜑 → (((𝐸 ↑_s 𝐵) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))))‘𝑋) = ((𝑥 ∈ 𝐵 ↦ (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))))‘𝑋))
180		fveq2 6886	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) = (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))
181	180	mpteq2dv 5198	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)) = (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)))
182	181	oveq2d 7437	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))) = (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))))
183		eqidd 2761	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)))) = (𝑥 ∈ 𝐵 ↦ (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)))))
184		extdgfialglem1.4	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
185		ovexd 7456	. . . . 5 ⊢ (𝜑 → (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))) ∈ V)
186	182, 183, 184, 185	fvmptd4 7019	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))))‘𝑋) = (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))))
187		eqid 2760	. . . . . . . 8 ⊢ (._g‘(mulGrp‘𝐸)) = (._g‘(mulGrp‘𝐸))
188		extdgfialglem1.3	. . . . . . . 8 ⊢ · = (._r‘𝐸)
189	184	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑋 ∈ 𝐵)
190	1, 6, 14, 11, 47, 40, 187, 20, 188, 155, 156, 26, 46, 189	evls1monply1 34158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋) = ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋)))
191	190	mpteq2dva 5197	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋))))
192		nfv 1946	. . . . . . . 8 ⊢ Ⅎ𝑛𝜑
193		ovexd 7456	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V)
194		extdgfialglem1.r	. . . . . . . 8 ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
195	192, 193, 194	fnmptd 6681	. . . . . . 7 ⊢ (𝜑 → 𝐺 Fn (0...𝐷))
196		inidm 4123	. . . . . . 7 ⊢ ((0...𝐷) ∩ (0...𝐷)) = (0...𝐷)
197		eqidd 2761	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) = (𝐴‘𝑛))
198	194	fvmpt2 7006	. . . . . . . . 9 ⊢ ((𝑛 ∈ (0...𝐷) ∧ (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
199	118, 193, 198	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
200		eqid 2760	. . . . . . . . . . 11 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
201	28, 6	sseqtrdi 3948	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
202	200, 80, 201	srapwov 34268	. . . . . . . . . 10 ⊢ (𝜑 → (._g‘(mulGrp‘𝐸)) = (._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹))))
203	202	oveqd 7438	. . . . . . . . 9 ⊢ (𝜑 → (𝑛(._g‘(mulGrp‘𝐸))𝑋) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
204	203	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘𝐸))𝑋) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
205	199, 204	eqtr4d 2798	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘𝐸))𝑋))
206	138, 195, 18, 18, 196, 197, 205	offval 7703	. . . . . 6 ⊢ (𝜑 → (𝐴 ∘_f · 𝐺) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋))))
207	191, 206	eqtr4d 2798	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)) = (𝐴 ∘_f · 𝐺))
208	207	oveq2d 7437	. . . 4 ⊢ (𝜑 → (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))) = (𝐸 Σ_g (𝐴 ∘_f · 𝐺)))
209	179, 186, 208	3eqtrd 2799	. . 3 ⊢ (𝜑 → (((𝐸 ↑_s 𝐵) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))))‘𝑋) = (𝐸 Σ_g (𝐴 ∘_f · 𝐺)))
210		extdgfialglem2.3	. . 3 ⊢ (𝜑 → (𝐸 Σ_g (𝐴 ∘_f · 𝐺)) = 𝑍)
211	154, 209, 210	3eqtrd 2799	. 2 ⊢ (𝜑 → (((𝐸 evalSub₁ 𝐹)‘((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))))‘𝑋) = 𝑍)
212	1, 2, 3, 4, 5, 6, 60, 151, 211, 184	irngnzply1lem 34369	1 ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 Vcvv 3450 ⊆ wss 3895 ∖ cdif 4045 ifcif 4481 {csn 4584 class class class wbr 5102 ↦ cmpt 5185 × cxp 5648 dom cdm 5650 Fn wfn 6534 ⟶wf 6535 ‘cfv 6539 (class class class)co 7421 ∘_f cof 7692 Fincfn 8977 finSupp cfsupp 9357 0cc0 11204 ℕ₀cn0 12610 ...cfz 13643 Basecbs 17393 ↾_s cress 17414 ._rcmulr 17435 Scalarcsca 17437 ·_𝑠 cvsca 17438 0_gc0g 17616 Σ_g cgsu 17617 ↑_s cpws 17623 Mndcmnd 18929 ._gcmg 19283 SubGrpcsubg 19336 mulGrpcmgp 20366 Ringcrg 20465 CRingccrg 20466 SubRingcsubrg 20827 Fieldcfield 20987 SubDRingcsdrg 21049 LModclmod 21141 subringAlg csra 21452 var₁cv1 22500 Poly₁cpl1 22501 evalSub₁ ces1 22637 dimcldim 34278 IntgRing cirng 34362

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-addf 11283

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 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 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-of 7694 df-ofr 7695 df-om 7879 df-1st 8002 df-2nd 8003 df-supp 8181 df-tpos 8247 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-2o 8481 df-er 8721 df-map 8853 df-pm 8854 df-ixp 8930 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-fsupp 9358 df-sup 9438 df-oi 9508 df-card 10024 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-nn 12340 df-2 12409 df-3 12410 df-4 12411 df-5 12412 df-6 12413 df-7 12414 df-8 12415 df-9 12416 df-n0 12611 df-z 12698 df-dec 12819 df-uz 12970 df-fz 13644 df-fzo 13793 df-seq 14149 df-hash 14479 df-struct 17331 df-sets 17348 df-slot 17366 df-ndx 17378 df-base 17394 df-ress 17415 df-plusg 17447 df-mulr 17448 df-starv 17449 df-sca 17450 df-vsca 17451 df-ip 17452 df-tset 17453 df-ple 17454 df-ds 17456 df-unif 17457 df-hom 17458 df-cco 17459 df-0g 17618 df-gsum 17619 df-prds 17624 df-pws 17626 df-mre 17762 df-mrc 17763 df-acs 17765 df-mgm 18822 df-sgrp 18914 df-mnd 18930 df-mhm 18984 df-submnd 18985 df-grp 19153 df-minusg 19154 df-sbg 19155 df-mulg 19284 df-subg 19339 df-ghm 19434 df-cntz 19537 df-cmn 20002 df-abl 20003 df-mgp 20367 df-rng 20381 df-ur 20414 df-srg 20419 df-ring 20467 df-cring 20468 df-oppr 20573 df-dvdsr 20593 df-unit 20594 df-invr 20624 df-rhm 20708 df-subrng 20804 df-subrg 20828 df-rlreg 20952 df-drng 20988 df-field 20989 df-sdrg 21050 df-lmod 21143 df-lss 21213 df-lsp 21253 df-sra 21454 df-cnfld 21685 df-assa 22167 df-asp 22168 df-ascl 22169 df-psr 22223 df-mvr 22224 df-mpl 22225 df-opsr 22227 df-evls 22389 df-evl 22390 df-psr1 22504 df-vr1 22505 df-ply1 22506 df-coe1 22507 df-evls1 22639 df-evl1 22640 df-mdeg 26379 df-deg1 26380 df-mon1 26455 df-uc1p 26456 df-irng 34363

This theorem is used by: extdgfialg 34373

W3C validator