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 33877

Description: Lemma for extdgfialg 33878. (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 2739	. 2 ⊢ (𝐸 evalSub₁ 𝐹) = (𝐸 evalSub₁ 𝐹)
2		eqid 2739	. 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 2739	. . . 4 ⊢ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Base‘(Poly₁‘(𝐸 ↾_s 𝐹)))
8		eqid 2739	. . . 4 ⊢ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹)))
9		sdrgsubrg 20763	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
10	5, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
11		eqid 2739	. . . . . . . 8 ⊢ (𝐸 ↾_s 𝐹) = (𝐸 ↾_s 𝐹)
12	11	subrgring 20546	. . . . . . 7 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (𝐸 ↾_s 𝐹) ∈ Ring)
13	10, 12	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐸 ↾_s 𝐹) ∈ Ring)
14		eqid 2739	. . . . . . 7 ⊢ (Poly₁‘(𝐸 ↾_s 𝐹)) = (Poly₁‘(𝐸 ↾_s 𝐹))
15	14	ply1ring 22232	. . . . . 6 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring)
16	13, 15	syl 17	. . . . 5 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring)
17	16	ringcmnd 20256	. . . 4 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ CMnd)
18		fzfid 13926	. . . 4 ⊢ (𝜑 → (0...𝐷) ∈ Fin)
19		eqid 2739	. . . . . 6 ⊢ (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))
20		eqid 2739	. . . . . 6 ⊢ ( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹))) = ( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))
21		eqid 2739	. . . . . 6 ⊢ (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
22	14	ply1lmod 22236	. . . . . . . 8 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
23	13, 22	syl 17	. . . . . . 7 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
24	23	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
25		extdgfialglem2.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴:(0...𝐷)⟶𝐹)
26	25	ffvelcdmda 7025	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) ∈ 𝐹)
27	6	sdrgss 20765	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝐵)
28	5, 27	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
29	11, 6	ressbas2 17199	. . . . . . . . . 10 ⊢ (𝐹 ⊆ 𝐵 → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
31		ovex 7389	. . . . . . . . . . 11 ⊢ (𝐸 ↾_s 𝐹) ∈ V
32	14	ply1sca 22237	. . . . . . . . . . 11 ⊢ ((𝐸 ↾_s 𝐹) ∈ V → (𝐸 ↾_s 𝐹) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
33	31, 32	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐸 ↾_s 𝐹) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))
34	33	fveq2i 6830	. . . . . . . . 9 ⊢ (Base‘(𝐸 ↾_s 𝐹)) = (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
35	30, 34	eqtr2di 2791	. . . . . . . 8 ⊢ (𝜑 → (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = 𝐹)
36	35	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = 𝐹)
37	26, 36	eleqtrrd 2842	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) ∈ (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))))
38		eqid 2739	. . . . . . . 8 ⊢ (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹)))
39	38, 7	mgpbas 20117	. . . . . . 7 ⊢ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Base‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))
40		eqid 2739	. . . . . . 7 ⊢ (._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = (._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))
41	38	ringmgp 20211	. . . . . . . . 9 ⊢ ((Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
42	16, 41	syl 17	. . . . . . . 8 ⊢ (𝜑 → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
43	42	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
44		fz0ssnn0 13567	. . . . . . . . 9 ⊢ (0...𝐷) ⊆ ℕ₀
45	44	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (0...𝐷) ⊆ ℕ₀)
46	45	sselda 3915	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ₀)
47		eqid 2739	. . . . . . . . . 10 ⊢ (var₁‘(𝐸 ↾_s 𝐹)) = (var₁‘(𝐸 ↾_s 𝐹))
48	47, 14, 7	vr1cl 22202	. . . . . . . . 9 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
49	13, 48	syl 17	. . . . . . . 8 ⊢ (𝜑 → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
50	49	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
51	39, 40, 43, 46, 50	mulgnn0cld 19062	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
52	7, 19, 20, 21, 24, 37, 51	lmodvscld 20869	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
53	52	fmpttd 7056	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))):(0...𝐷)⟶(Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
54		eqid 2739	. . . . 5 ⊢ (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
55		fvexd 6842	. . . . 5 ⊢ (𝜑 → (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ V)
56	54, 18, 52, 55	fsuppmptdm 9279	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) finSupp (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
57	7, 8, 17, 18, 53, 56	gsumcl 19881	. . 3 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
58	4	fldcrngd 20714	. . . 4 ⊢ (𝜑 → 𝐸 ∈ CRing)
59	1, 14, 7, 58, 10	evls1dm 33644	. . 3 ⊢ (𝜑 → dom (𝐸 evalSub₁ 𝐹) = (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
60	57, 59	eleqtrrd 2842	. 2 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ∈ dom (𝐸 evalSub₁ 𝐹))
61		extdgfialglem2.4	. . 3 ⊢ (𝜑 → 𝐴 ≠ ((0...𝐷) × {𝑍}))
62		eqid 2739	. . . . . 6 ⊢ (Base‘(𝐸 ↾_s 𝐹)) = (Base‘(𝐸 ↾_s 𝐹))
63		eqid 2739	. . . . . 6 ⊢ (0_g‘(𝐸 ↾_s 𝐹)) = (0_g‘(𝐸 ↾_s 𝐹))
64	25	ffvelcdmda 7025	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ 𝐹)
65	64	adantlr 721	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ 𝐹)
66	30	ad2antrr 732	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
67	65, 66	eleqtrd 2841	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ (Base‘(𝐸 ↾_s 𝐹)))
68		subrgsubg 20549	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
69	10, 68	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
70	3	subg0cl 19101	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝑍 ∈ 𝐹)
71	69, 70	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝐹)
72	71, 30	eleqtrd 2841	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
73	72	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ ¬ 𝑚 ∈ (0...𝐷)) → 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
74	67, 73	ifclda 4490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) ∈ (Base‘(𝐸 ↾_s 𝐹)))
75	74	ralrimiva 3131	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) ∈ (Base‘(𝐸 ↾_s 𝐹)))
76		eqid 2739	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) = (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍))
77		nn0ex 12434	. . . . . . . . 9 ⊢ ℕ₀ ∈ V
78	77	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℕ₀ ∈ V)
79	76, 78, 18, 64, 71	mptiffisupp 32785	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) finSupp 𝑍)
80	58	crngringd 20218	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ Ring)
81	80	ringcmnd 20256	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ CMnd)
82	81	cmnmndd 19770	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Mnd)
83	11, 6, 3	ress0g 18721	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ 𝑍 ∈ 𝐹 ∧ 𝐹 ⊆ 𝐵) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
84	82, 71, 28, 83	syl3anc 1379	. . . . . . 7 ⊢ (𝜑 → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
85	79, 84	breqtrd 5098	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) finSupp (0_g‘(𝐸 ↾_s 𝐹)))
86	72	ralrimivw 3135	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ₀ 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
87		fconstmpt 5680	. . . . . . . 8 ⊢ (ℕ₀ × {𝑍}) = (𝑚 ∈ ℕ₀ ↦ 𝑍)
88	78, 71	fczfsuppd 9289	. . . . . . . 8 ⊢ (𝜑 → (ℕ₀ × {𝑍}) finSupp 𝑍)
89	87, 88	eqbrtrrid 5108	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ 𝑍) finSupp 𝑍)
90	89, 84	breqtrd 5098	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ 𝑍) finSupp (0_g‘(𝐸 ↾_s 𝐹)))
91		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑚 ∈ (ℕ₀ ∖ (0...𝐷)))
92	91	eldifbd 3896	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → ¬ 𝑚 ∈ (0...𝐷))
93	92	iffalsed 4465	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍)
94	84	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
95	93, 94	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = (0_g‘(𝐸 ↾_s 𝐹)))
96	95	oveq1d 7371	. . . . . . . . 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 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
98	42	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
99	91	eldifad 3895	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑚 ∈ ℕ₀)
100	49	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
101	39, 40, 98, 99, 100	mulgnn0cld 19062	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
102	7, 33, 20, 63, 8	lmod0vs 20885	. . . . . . . . . 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 590	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
104	96, 103	eqtrd 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
105	23	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
106	42	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
107		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → 𝑚 ∈ ℕ₀)
108	49	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
109	39, 40, 106, 107, 108	mulgnn0cld 19062	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
110	7, 33, 20, 62, 105, 74, 109	lmodvscld 20869	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
111	7, 8, 17, 78, 104, 18, 110, 45	gsummptres2 33134	. . . . . . 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 2822	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (0...𝐷) ↔ 𝑛 ∈ (0...𝐷)))
113		fveq2 6827	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝐴‘𝑚) = (𝐴‘𝑛))
114	112, 113	ifbieq1d 4479	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍))
115		oveq1 7363	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) = (𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))
116	114, 115	oveq12d 7374	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
117	116	cbvmptv 5176	. . . . . . . . 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 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ (0...𝐷))
119	118	iftrued 4462	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = (𝐴‘𝑛))
120	119	oveq1d 7371	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
121	120	mpteq2dva 5165	. . . . . . . . 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 2786	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ (0...𝐷) ↦ (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))))
123	122	oveq2d 7372	. . . . . . 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 2775	. . . . . 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 19770	. . . . . . . 8 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Mnd)
126	8	gsumz 18795	. . . . . . . 8 ⊢ (((Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Mnd ∧ ℕ₀ ∈ V) → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
127	125, 78, 126	syl2anc 590	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
128	84	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
129	128	oveq1d 7371	. . . . . . . . . 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 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
131	129, 130	eqtrd 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
132	131	mpteq2dva 5165	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹)))))
133	132	oveq2d 7372	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))))
134		eqid 2739	. . . . . . . 8 ⊢ (Poly₁‘𝐸) = (Poly₁‘𝐸)
135	134, 11, 14, 7, 10, 2	ressply10g 33650	. . . . . . 7 ⊢ (𝜑 → (0_g‘(Poly₁‘𝐸)) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
136	127, 133, 135	3eqtr4rd 2785	. . . . . 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 22295	. . . . 5 ⊢ (𝜑 → (((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (0_g‘(Poly₁‘𝐸)) ↔ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍))
138	25	ffnd 6656	. . . . . . . 8 ⊢ (𝜑 → 𝐴 Fn (0...𝐷))
139	138	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → 𝐴 Fn (0...𝐷))
140	119	adantlr 721	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = (𝐴‘𝑛))
141	114	eqeq1d 2741	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍 ↔ if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = 𝑍))
142		simplr 774	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍)
143	44	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → (0...𝐷) ⊆ ℕ₀)
144	143	sselda 3915	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ₀)
145	141, 142, 144	rspcdva 3561	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = 𝑍)
146	140, 145	eqtr3d 2776	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) = 𝑍)
147	139, 146	fconst7v 32712	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → 𝐴 = ((0...𝐷) × {𝑍}))
148	147	ex 413	. . . . 5 ⊢ (𝜑 → (∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍 → 𝐴 = ((0...𝐷) × {𝑍})))
149	137, 148	sylbid 241	. . . 4 ⊢ (𝜑 → (((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (0_g‘(Poly₁‘𝐸)) → 𝐴 = ((0...𝐷) × {𝑍})))
150	149	necon3d 2955	. . 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 2739	. . . . 5 ⊢ (𝐸 ↑_s 𝐵) = (𝐸 ↑_s 𝐵)
153	1, 6, 14, 8, 11, 152, 7, 58, 10, 52, 45, 56	evls1gsumadd 22310	. . . 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 6829	. . 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 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝐸 ∈ CRing)
156	10	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝐹 ∈ (SubRing‘𝐸))
157	1, 14, 7, 155, 156, 6, 52	evls1fvf 33645	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))):𝐵⟶𝐵)
158	157	feqmptd 6895	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)))
159	158	mpteq2dva 5165	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))))
160	159	oveq2d 7372	. . . . . 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 6829	. . . . 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 2739	. . . . . . 7 ⊢ (0_g‘(𝐸 ↑_s 𝐵)) = (0_g‘(𝐸 ↑_s 𝐵))
163	6	fvexi 6841	. . . . . . . 8 ⊢ 𝐵 ∈ V
164	163	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ V)
165	155	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝐸 ∈ CRing)
166	156	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝐹 ∈ (SubRing‘𝐸))
167		simpr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
168	52	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
169	1, 14, 6, 7, 165, 166, 167, 168	evls1fvcl 22361	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
170	169	an32s 658	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (0...𝐷)) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
171	170	anasss 467	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑛 ∈ (0...𝐷))) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
172		eqid 2739	. . . . . . . 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 7168	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)) ∈ V)
175		fvexd 6842	. . . . . . . 8 ⊢ (𝜑 → (0_g‘(𝐸 ↑_s 𝐵)) ∈ V)
176	172, 18, 174, 175	fsuppmptdm 9279	. . . . . . 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 19948	. . . . . 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 6829	. . . . 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 2774	. . . 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 6827	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) = (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))
181	180	mpteq2dv 5166	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)) = (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)))
182	181	oveq2d 7372	. . . . 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 2740	. . . . 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 7391	. . . . 5 ⊢ (𝜑 → (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))) ∈ V)
186	182, 183, 184, 185	fvmptd4 6960	. . . 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 2739	. . . . . . . 8 ⊢ (._g‘(mulGrp‘𝐸)) = (._g‘(mulGrp‘𝐸))
188		extdgfialglem1.3	. . . . . . . 8 ⊢ · = (._r‘𝐸)
189	184	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑋 ∈ 𝐵)
190	1, 6, 14, 11, 47, 40, 187, 20, 188, 155, 156, 26, 46, 189	evls1monply1 33662	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋) = ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋)))
191	190	mpteq2dva 5165	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋))))
192		nfv 1921	. . . . . . . 8 ⊢ Ⅎ𝑛𝜑
193		ovexd 7391	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V)
194		extdgfialglem1.r	. . . . . . . 8 ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
195	192, 193, 194	fnmptd 6626	. . . . . . 7 ⊢ (𝜑 → 𝐺 Fn (0...𝐷))
196		inidm 4155	. . . . . . 7 ⊢ ((0...𝐷) ∩ (0...𝐷)) = (0...𝐷)
197		eqidd 2740	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) = (𝐴‘𝑛))
198	194	fvmpt2 6947	. . . . . . . . 9 ⊢ ((𝑛 ∈ (0...𝐷) ∧ (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
199	118, 193, 198	syl2anc 590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
200		eqid 2739	. . . . . . . . . . 11 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
201	28, 6	sseqtrdi 3955	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
202	200, 80, 201	srapwov 33773	. . . . . . . . . 10 ⊢ (𝜑 → (._g‘(mulGrp‘𝐸)) = (._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹))))
203	202	oveqd 7373	. . . . . . . . 9 ⊢ (𝜑 → (𝑛(._g‘(mulGrp‘𝐸))𝑋) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
204	203	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘𝐸))𝑋) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
205	199, 204	eqtr4d 2777	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘𝐸))𝑋))
206	138, 195, 18, 18, 196, 197, 205	offval 7629	. . . . . 6 ⊢ (𝜑 → (𝐴 ∘_f · 𝐺) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋))))
207	191, 206	eqtr4d 2777	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)) = (𝐴 ∘_f · 𝐺))
208	207	oveq2d 7372	. . . 4 ⊢ (𝜑 → (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))) = (𝐸 Σ_g (𝐴 ∘_f · 𝐺)))
209	179, 186, 208	3eqtrd 2778	. . 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 2778	. 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 33874	1 ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∀wral 3053 Vcvv 3431 ∖ cdif 3880 ⊆ wss 3883 ifcif 4454 {csn 4555 class class class wbr 5072 ↦ cmpt 5153 × cxp 5616 dom cdm 5618 Fn wfn 6480 ⟶wf 6481 ‘cfv 6485 (class class class)co 7356 ∘_f cof 7618 Fincfn 8883 finSupp cfsupp 9264 0cc0 11029 ℕ₀cn0 12428 ...cfz 13452 Basecbs 17170 ↾_s cress 17191 ._rcmulr 17212 Scalarcsca 17214 ·_𝑠 cvsca 17215 0_gc0g 17393 Σ_g cgsu 17394 ↑_s cpws 17400 Mndcmnd 18693 ._gcmg 19034 SubGrpcsubg 19087 mulGrpcmgp 20112 Ringcrg 20205 CRingccrg 20206 SubRingcsubrg 20541 Fieldcfield 20702 SubDRingcsdrg 20758 LModclmod 20850 subringAlg csra 21161 var₁cv1 22161 Poly₁cpl1 22162 evalSub₁ ces1 22299 dimcldim 33783 IntgRing cirng 33867

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-addf 11108

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-iin 4924 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-se 5572 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-isom 6494 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-ofr 7621 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-tpos 8166 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-er 8633 df-map 8765 df-pm 8766 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9265 df-sup 9345 df-oi 9415 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-z 12516 df-dec 12636 df-uz 12780 df-fz 13453 df-fzo 13600 df-seq 13955 df-hash 14284 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-mulr 17225 df-starv 17226 df-sca 17227 df-vsca 17228 df-ip 17229 df-tset 17230 df-ple 17231 df-ds 17233 df-unif 17234 df-hom 17235 df-cco 17236 df-0g 17395 df-gsum 17396 df-prds 17401 df-pws 17403 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-mhm 18742 df-submnd 18743 df-grp 18903 df-minusg 18904 df-sbg 18905 df-mulg 19035 df-subg 19090 df-ghm 19179 df-cntz 19283 df-cmn 19748 df-abl 19749 df-mgp 20113 df-rng 20125 df-ur 20154 df-srg 20159 df-ring 20207 df-cring 20208 df-oppr 20308 df-dvdsr 20328 df-unit 20329 df-invr 20359 df-rhm 20443 df-subrng 20518 df-subrg 20542 df-rlreg 20666 df-drng 20703 df-field 20704 df-sdrg 20759 df-lmod 20852 df-lss 20922 df-lsp 20962 df-sra 21163 df-cnfld 21348 df-assa 21828 df-asp 21829 df-ascl 21830 df-psr 21884 df-mvr 21885 df-mpl 21886 df-opsr 21888 df-evls 22050 df-evl 22051 df-psr1 22165 df-vr1 22166 df-ply1 22167 df-coe1 22168 df-evls1 22301 df-evl1 22302 df-mdeg 26038 df-deg1 26039 df-mon1 26114 df-uc1p 26115 df-irng 33868

This theorem is referenced by: extdgfialg 33878

W3C validator