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 33837

Description: Lemma for extdgfialg 33838. (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 2736	. 2 ⊢ (𝐸 evalSub₁ 𝐹) = (𝐸 evalSub₁ 𝐹)
2		eqid 2736	. 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 2736	. . . 4 ⊢ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Base‘(Poly₁‘(𝐸 ↾_s 𝐹)))
8		eqid 2736	. . . 4 ⊢ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹)))
9		sdrgsubrg 20768	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
10	5, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
11		eqid 2736	. . . . . . . 8 ⊢ (𝐸 ↾_s 𝐹) = (𝐸 ↾_s 𝐹)
12	11	subrgring 20551	. . . . . . 7 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (𝐸 ↾_s 𝐹) ∈ Ring)
13	10, 12	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐸 ↾_s 𝐹) ∈ Ring)
14		eqid 2736	. . . . . . 7 ⊢ (Poly₁‘(𝐸 ↾_s 𝐹)) = (Poly₁‘(𝐸 ↾_s 𝐹))
15	14	ply1ring 22211	. . . . . 6 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring)
16	13, 15	syl 17	. . . . 5 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring)
17	16	ringcmnd 20265	. . . 4 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ CMnd)
18		fzfid 13935	. . . 4 ⊢ (𝜑 → (0...𝐷) ∈ Fin)
19		eqid 2736	. . . . . 6 ⊢ (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))
20		eqid 2736	. . . . . 6 ⊢ ( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹))) = ( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))
21		eqid 2736	. . . . . 6 ⊢ (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
22	14	ply1lmod 22215	. . . . . . . 8 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
23	13, 22	syl 17	. . . . . . 7 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
24	23	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
25		extdgfialglem2.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴:(0...𝐷)⟶𝐹)
26	25	ffvelcdmda 7036	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) ∈ 𝐹)
27	6	sdrgss 20770	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝐵)
28	5, 27	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
29	11, 6	ressbas2 17208	. . . . . . . . . 10 ⊢ (𝐹 ⊆ 𝐵 → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
31		ovex 7400	. . . . . . . . . . 11 ⊢ (𝐸 ↾_s 𝐹) ∈ V
32	14	ply1sca 22216	. . . . . . . . . . 11 ⊢ ((𝐸 ↾_s 𝐹) ∈ V → (𝐸 ↾_s 𝐹) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
33	31, 32	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐸 ↾_s 𝐹) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))
34	33	fveq2i 6843	. . . . . . . . 9 ⊢ (Base‘(𝐸 ↾_s 𝐹)) = (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
35	30, 34	eqtr2di 2788	. . . . . . . 8 ⊢ (𝜑 → (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = 𝐹)
36	35	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = 𝐹)
37	26, 36	eleqtrrd 2839	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) ∈ (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))))
38		eqid 2736	. . . . . . . 8 ⊢ (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹)))
39	38, 7	mgpbas 20126	. . . . . . 7 ⊢ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Base‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))
40		eqid 2736	. . . . . . 7 ⊢ (._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = (._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))
41	38	ringmgp 20220	. . . . . . . . 9 ⊢ ((Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
42	16, 41	syl 17	. . . . . . . 8 ⊢ (𝜑 → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
43	42	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
44		fz0ssnn0 13576	. . . . . . . . 9 ⊢ (0...𝐷) ⊆ ℕ₀
45	44	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (0...𝐷) ⊆ ℕ₀)
46	45	sselda 3921	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ₀)
47		eqid 2736	. . . . . . . . . 10 ⊢ (var₁‘(𝐸 ↾_s 𝐹)) = (var₁‘(𝐸 ↾_s 𝐹))
48	47, 14, 7	vr1cl 22181	. . . . . . . . 9 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
49	13, 48	syl 17	. . . . . . . 8 ⊢ (𝜑 → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
50	49	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
51	39, 40, 43, 46, 50	mulgnn0cld 19071	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
52	7, 19, 20, 21, 24, 37, 51	lmodvscld 20874	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
53	52	fmpttd 7067	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))):(0...𝐷)⟶(Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
54		eqid 2736	. . . . 5 ⊢ (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
55		fvexd 6855	. . . . 5 ⊢ (𝜑 → (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ V)
56	54, 18, 52, 55	fsuppmptdm 9289	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) finSupp (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
57	7, 8, 17, 18, 53, 56	gsumcl 19890	. . 3 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
58	4	fldcrngd 20719	. . . 4 ⊢ (𝜑 → 𝐸 ∈ CRing)
59	1, 14, 7, 58, 10	evls1dm 33621	. . 3 ⊢ (𝜑 → dom (𝐸 evalSub₁ 𝐹) = (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
60	57, 59	eleqtrrd 2839	. 2 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ∈ dom (𝐸 evalSub₁ 𝐹))
61		extdgfialglem2.4	. . 3 ⊢ (𝜑 → 𝐴 ≠ ((0...𝐷) × {𝑍}))
62		eqid 2736	. . . . . 6 ⊢ (Base‘(𝐸 ↾_s 𝐹)) = (Base‘(𝐸 ↾_s 𝐹))
63		eqid 2736	. . . . . 6 ⊢ (0_g‘(𝐸 ↾_s 𝐹)) = (0_g‘(𝐸 ↾_s 𝐹))
64	25	ffvelcdmda 7036	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ 𝐹)
65	64	adantlr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ 𝐹)
66	30	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
67	65, 66	eleqtrd 2838	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ (Base‘(𝐸 ↾_s 𝐹)))
68		subrgsubg 20554	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
69	10, 68	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
70	3	subg0cl 19110	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝑍 ∈ 𝐹)
71	69, 70	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝐹)
72	71, 30	eleqtrd 2838	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
73	72	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ ¬ 𝑚 ∈ (0...𝐷)) → 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
74	67, 73	ifclda 4502	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) ∈ (Base‘(𝐸 ↾_s 𝐹)))
75	74	ralrimiva 3129	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) ∈ (Base‘(𝐸 ↾_s 𝐹)))
76		eqid 2736	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) = (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍))
77		nn0ex 12443	. . . . . . . . 9 ⊢ ℕ₀ ∈ V
78	77	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℕ₀ ∈ V)
79	76, 78, 18, 64, 71	mptiffisupp 32766	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) finSupp 𝑍)
80	58	crngringd 20227	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ Ring)
81	80	ringcmnd 20265	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ CMnd)
82	81	cmnmndd 19779	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Mnd)
83	11, 6, 3	ress0g 18730	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ 𝑍 ∈ 𝐹 ∧ 𝐹 ⊆ 𝐵) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
84	82, 71, 28, 83	syl3anc 1374	. . . . . . 7 ⊢ (𝜑 → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
85	79, 84	breqtrd 5111	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) finSupp (0_g‘(𝐸 ↾_s 𝐹)))
86	72	ralrimivw 3133	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ₀ 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
87		fconstmpt 5693	. . . . . . . 8 ⊢ (ℕ₀ × {𝑍}) = (𝑚 ∈ ℕ₀ ↦ 𝑍)
88	78, 71	fczfsuppd 9299	. . . . . . . 8 ⊢ (𝜑 → (ℕ₀ × {𝑍}) finSupp 𝑍)
89	87, 88	eqbrtrrid 5121	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ 𝑍) finSupp 𝑍)
90	89, 84	breqtrd 5111	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ 𝑍) finSupp (0_g‘(𝐸 ↾_s 𝐹)))
91		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑚 ∈ (ℕ₀ ∖ (0...𝐷)))
92	91	eldifbd 3902	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → ¬ 𝑚 ∈ (0...𝐷))
93	92	iffalsed 4477	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍)
94	84	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
95	93, 94	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = (0_g‘(𝐸 ↾_s 𝐹)))
96	95	oveq1d 7382	. . . . . . . . 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 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
98	42	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
99	91	eldifad 3901	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑚 ∈ ℕ₀)
100	49	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
101	39, 40, 98, 99, 100	mulgnn0cld 19071	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
102	7, 33, 20, 63, 8	lmod0vs 20890	. . . . . . . . . 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 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
104	96, 103	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
105	23	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
106	42	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
107		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → 𝑚 ∈ ℕ₀)
108	49	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
109	39, 40, 106, 107, 108	mulgnn0cld 19071	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
110	7, 33, 20, 62, 105, 74, 109	lmodvscld 20874	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
111	7, 8, 17, 78, 104, 18, 110, 45	gsummptres2 33114	. . . . . . 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 2819	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (0...𝐷) ↔ 𝑛 ∈ (0...𝐷)))
113		fveq2 6840	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝐴‘𝑚) = (𝐴‘𝑛))
114	112, 113	ifbieq1d 4491	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍))
115		oveq1 7374	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) = (𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))
116	114, 115	oveq12d 7385	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
117	116	cbvmptv 5189	. . . . . . . . 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 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ (0...𝐷))
119	118	iftrued 4474	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = (𝐴‘𝑛))
120	119	oveq1d 7382	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
121	120	mpteq2dva 5178	. . . . . . . . 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 2783	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ (0...𝐷) ↦ (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))))
123	122	oveq2d 7383	. . . . . . 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 2772	. . . . . 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 19779	. . . . . . . 8 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Mnd)
126	8	gsumz 18804	. . . . . . . 8 ⊢ (((Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Mnd ∧ ℕ₀ ∈ V) → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
127	125, 78, 126	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
128	84	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
129	128	oveq1d 7382	. . . . . . . . . 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 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
131	129, 130	eqtrd 2771	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
132	131	mpteq2dva 5178	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹)))))
133	132	oveq2d 7383	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))))
134		eqid 2736	. . . . . . . 8 ⊢ (Poly₁‘𝐸) = (Poly₁‘𝐸)
135	134, 11, 14, 7, 10, 2	ressply10g 33627	. . . . . . 7 ⊢ (𝜑 → (0_g‘(Poly₁‘𝐸)) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
136	127, 133, 135	3eqtr4rd 2782	. . . . . 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 22274	. . . . 5 ⊢ (𝜑 → (((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (0_g‘(Poly₁‘𝐸)) ↔ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍))
138	25	ffnd 6669	. . . . . . . 8 ⊢ (𝜑 → 𝐴 Fn (0...𝐷))
139	138	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → 𝐴 Fn (0...𝐷))
140	119	adantlr 716	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = (𝐴‘𝑛))
141	114	eqeq1d 2738	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍 ↔ if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = 𝑍))
142		simplr 769	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍)
143	44	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → (0...𝐷) ⊆ ℕ₀)
144	143	sselda 3921	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ₀)
145	141, 142, 144	rspcdva 3565	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = 𝑍)
146	140, 145	eqtr3d 2773	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) = 𝑍)
147	139, 146	fconst7v 32693	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → 𝐴 = ((0...𝐷) × {𝑍}))
148	147	ex 412	. . . . 5 ⊢ (𝜑 → (∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍 → 𝐴 = ((0...𝐷) × {𝑍})))
149	137, 148	sylbid 240	. . . 4 ⊢ (𝜑 → (((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (0_g‘(Poly₁‘𝐸)) → 𝐴 = ((0...𝐷) × {𝑍})))
150	149	necon3d 2953	. . 3 ⊢ (𝜑 → (𝐴 ≠ ((0...𝐷) × {𝑍}) → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ≠ (0_g‘(Poly₁‘𝐸))))
151	61, 150	mpd 15	. 2 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ≠ (0_g‘(Poly₁‘𝐸)))
152		eqid 2736	. . . . 5 ⊢ (𝐸 ↑_s 𝐵) = (𝐸 ↑_s 𝐵)
153	1, 6, 14, 8, 11, 152, 7, 58, 10, 52, 45, 56	evls1gsumadd 22289	. . . 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 6842	. . 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 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝐸 ∈ CRing)
156	10	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝐹 ∈ (SubRing‘𝐸))
157	1, 14, 7, 155, 156, 6, 52	evls1fvf 33622	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))):𝐵⟶𝐵)
158	157	feqmptd 6908	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)))
159	158	mpteq2dva 5178	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))))
160	159	oveq2d 7383	. . . . . 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 6842	. . . . 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 2736	. . . . . . 7 ⊢ (0_g‘(𝐸 ↑_s 𝐵)) = (0_g‘(𝐸 ↑_s 𝐵))
163	6	fvexi 6854	. . . . . . . 8 ⊢ 𝐵 ∈ V
164	163	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ V)
165	155	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝐸 ∈ CRing)
166	156	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝐹 ∈ (SubRing‘𝐸))
167		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
168	52	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
169	1, 14, 6, 7, 165, 166, 167, 168	evls1fvcl 22340	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
170	169	an32s 653	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (0...𝐷)) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
171	170	anasss 466	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑛 ∈ (0...𝐷))) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
172		eqid 2736	. . . . . . . 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 7179	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)) ∈ V)
175		fvexd 6855	. . . . . . . 8 ⊢ (𝜑 → (0_g‘(𝐸 ↑_s 𝐵)) ∈ V)
176	172, 18, 174, 175	fsuppmptdm 9289	. . . . . . 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 19957	. . . . . 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 6842	. . . . 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 2771	. . . 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 6840	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) = (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))
181	180	mpteq2dv 5179	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)) = (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)))
182	181	oveq2d 7383	. . . . 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 2737	. . . . 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 7402	. . . . 5 ⊢ (𝜑 → (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))) ∈ V)
186	182, 183, 184, 185	fvmptd4 6972	. . . 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 2736	. . . . . . . 8 ⊢ (._g‘(mulGrp‘𝐸)) = (._g‘(mulGrp‘𝐸))
188		extdgfialglem1.3	. . . . . . . 8 ⊢ · = (._r‘𝐸)
189	184	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑋 ∈ 𝐵)
190	1, 6, 14, 11, 47, 40, 187, 20, 188, 155, 156, 26, 46, 189	evls1monply1 33639	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋) = ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋)))
191	190	mpteq2dva 5178	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋))))
192		nfv 1916	. . . . . . . 8 ⊢ Ⅎ𝑛𝜑
193		ovexd 7402	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V)
194		extdgfialglem1.r	. . . . . . . 8 ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
195	192, 193, 194	fnmptd 6639	. . . . . . 7 ⊢ (𝜑 → 𝐺 Fn (0...𝐷))
196		inidm 4167	. . . . . . 7 ⊢ ((0...𝐷) ∩ (0...𝐷)) = (0...𝐷)
197		eqidd 2737	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) = (𝐴‘𝑛))
198	194	fvmpt2 6959	. . . . . . . . 9 ⊢ ((𝑛 ∈ (0...𝐷) ∧ (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
199	118, 193, 198	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
200		eqid 2736	. . . . . . . . . . 11 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
201	28, 6	sseqtrdi 3962	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
202	200, 80, 201	srapwov 33733	. . . . . . . . . 10 ⊢ (𝜑 → (._g‘(mulGrp‘𝐸)) = (._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹))))
203	202	oveqd 7384	. . . . . . . . 9 ⊢ (𝜑 → (𝑛(._g‘(mulGrp‘𝐸))𝑋) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
204	203	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘𝐸))𝑋) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
205	199, 204	eqtr4d 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘𝐸))𝑋))
206	138, 195, 18, 18, 196, 197, 205	offval 7640	. . . . . 6 ⊢ (𝜑 → (𝐴 ∘_f · 𝐺) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋))))
207	191, 206	eqtr4d 2774	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)) = (𝐴 ∘_f · 𝐺))
208	207	oveq2d 7383	. . . 4 ⊢ (𝜑 → (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))) = (𝐸 Σ_g (𝐴 ∘_f · 𝐺)))
209	179, 186, 208	3eqtrd 2775	. . 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 2775	. 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 33834	1 ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 ∀wral 3051 Vcvv 3429 ∖ cdif 3886 ⊆ wss 3889 ifcif 4466 {csn 4567 class class class wbr 5085 ↦ cmpt 5166 × cxp 5629 dom cdm 5631 Fn wfn 6493 ⟶wf 6494 ‘cfv 6498 (class class class)co 7367 ∘_f cof 7629 Fincfn 8893 finSupp cfsupp 9274 0cc0 11038 ℕ₀cn0 12437 ...cfz 13461 Basecbs 17179 ↾_s cress 17200 ._rcmulr 17221 Scalarcsca 17223 ·_𝑠 cvsca 17224 0_gc0g 17402 Σ_g cgsu 17403 ↑_s cpws 17409 Mndcmnd 18702 ._gcmg 19043 SubGrpcsubg 19096 mulGrpcmgp 20121 Ringcrg 20214 CRingccrg 20215 SubRingcsubrg 20546 Fieldcfield 20707 SubDRingcsdrg 20763 LModclmod 20855 subringAlg csra 21166 var₁cv1 22139 Poly₁cpl1 22140 evalSub₁ ces1 22278 dimcldim 33743 IntgRing cirng 33827

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-addf 11117

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-iin 4936 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-ofr 7632 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-tpos 8176 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-er 8643 df-map 8775 df-pm 8776 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fsupp 9275 df-sup 9355 df-oi 9425 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-z 12525 df-dec 12645 df-uz 12789 df-fz 13462 df-fzo 13609 df-seq 13964 df-hash 14293 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-0g 17404 df-gsum 17405 df-prds 17410 df-pws 17412 df-mre 17548 df-mrc 17549 df-acs 17551 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-mhm 18751 df-submnd 18752 df-grp 18912 df-minusg 18913 df-sbg 18914 df-mulg 19044 df-subg 19099 df-ghm 19188 df-cntz 19292 df-cmn 19757 df-abl 19758 df-mgp 20122 df-rng 20134 df-ur 20163 df-srg 20168 df-ring 20216 df-cring 20217 df-oppr 20317 df-dvdsr 20337 df-unit 20338 df-invr 20368 df-rhm 20452 df-subrng 20523 df-subrg 20547 df-rlreg 20671 df-drng 20708 df-field 20709 df-sdrg 20764 df-lmod 20857 df-lss 20927 df-lsp 20967 df-sra 21168 df-cnfld 21353 df-assa 21833 df-asp 21834 df-ascl 21835 df-psr 21889 df-mvr 21890 df-mpl 21891 df-opsr 21893 df-evls 22052 df-evl 22053 df-psr1 22143 df-vr1 22144 df-ply1 22145 df-coe1 22146 df-evls1 22280 df-evl1 22281 df-mdeg 26020 df-deg1 26021 df-mon1 26096 df-uc1p 26097 df-irng 33828

This theorem is referenced by: extdgfialg 33838

W3C validator