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 33951

Description: Lemma for extdgfialg 33952. (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 2761	. 2 ⊢ (𝐸 evalSub₁ 𝐹) = (𝐸 evalSub₁ 𝐹)
2		eqid 2761	. 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 2761	. . . 4 ⊢ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Base‘(Poly₁‘(𝐸 ↾_s 𝐹)))
8		eqid 2761	. . . 4 ⊢ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹)))
9		sdrgsubrg 20828	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
10	5, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
11		eqid 2761	. . . . . . . 8 ⊢ (𝐸 ↾_s 𝐹) = (𝐸 ↾_s 𝐹)
12	11	subrgring 20611	. . . . . . 7 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (𝐸 ↾_s 𝐹) ∈ Ring)
13	10, 12	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐸 ↾_s 𝐹) ∈ Ring)
14		eqid 2761	. . . . . . 7 ⊢ (Poly₁‘(𝐸 ↾_s 𝐹)) = (Poly₁‘(𝐸 ↾_s 𝐹))
15	14	ply1ring 22297	. . . . . 6 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring)
16	13, 15	syl 17	. . . . 5 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring)
17	16	ringcmnd 20321	. . . 4 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ CMnd)
18		fzfid 13980	. . . 4 ⊢ (𝜑 → (0...𝐷) ∈ Fin)
19		eqid 2761	. . . . . 6 ⊢ (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))
20		eqid 2761	. . . . . 6 ⊢ ( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹))) = ( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))
21		eqid 2761	. . . . . 6 ⊢ (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
22	14	ply1lmod 22301	. . . . . . . 8 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
23	13, 22	syl 17	. . . . . . 7 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
24	23	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
25		extdgfialglem2.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴:(0...𝐷)⟶𝐹)
26	25	ffvelcdmda 7060	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) ∈ 𝐹)
27	6	sdrgss 20830	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝐵)
28	5, 27	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
29	11, 6	ressbas2 17265	. . . . . . . . . 10 ⊢ (𝐹 ⊆ 𝐵 → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
31		ovex 7424	. . . . . . . . . . 11 ⊢ (𝐸 ↾_s 𝐹) ∈ V
32	14	ply1sca 22302	. . . . . . . . . . 11 ⊢ ((𝐸 ↾_s 𝐹) ∈ V → (𝐸 ↾_s 𝐹) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
33	31, 32	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐸 ↾_s 𝐹) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))
34	33	fveq2i 6865	. . . . . . . . 9 ⊢ (Base‘(𝐸 ↾_s 𝐹)) = (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
35	30, 34	eqtr2di 2813	. . . . . . . 8 ⊢ (𝜑 → (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = 𝐹)
36	35	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = 𝐹)
37	26, 36	eleqtrrd 2864	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) ∈ (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))))
38		eqid 2761	. . . . . . . 8 ⊢ (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹)))
39	38, 7	mgpbas 20182	. . . . . . 7 ⊢ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Base‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))
40		eqid 2761	. . . . . . 7 ⊢ (._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = (._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))
41	38	ringmgp 20276	. . . . . . . . 9 ⊢ ((Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
42	16, 41	syl 17	. . . . . . . 8 ⊢ (𝜑 → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
43	42	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
44		fz0ssnn0 13621	. . . . . . . . 9 ⊢ (0...𝐷) ⊆ ℕ₀
45	44	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (0...𝐷) ⊆ ℕ₀)
46	45	sselda 3934	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ₀)
47		eqid 2761	. . . . . . . . . 10 ⊢ (var₁‘(𝐸 ↾_s 𝐹)) = (var₁‘(𝐸 ↾_s 𝐹))
48	47, 14, 7	vr1cl 22267	. . . . . . . . 9 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
49	13, 48	syl 17	. . . . . . . 8 ⊢ (𝜑 → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
50	49	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
51	39, 40, 43, 46, 50	mulgnn0cld 19128	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
52	7, 19, 20, 21, 24, 37, 51	lmodvscld 20934	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
53	52	fmpttd 7091	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))):(0...𝐷)⟶(Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
54		eqid 2761	. . . . 5 ⊢ (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
55		fvexd 6877	. . . . 5 ⊢ (𝜑 → (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ V)
56	54, 18, 52, 55	fsuppmptdm 9316	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) finSupp (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
57	7, 8, 17, 18, 53, 56	gsumcl 19946	. . 3 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
58	4	fldcrngd 20779	. . . 4 ⊢ (𝜑 → 𝐸 ∈ CRing)
59	1, 14, 7, 58, 10	evls1dm 33718	. . 3 ⊢ (𝜑 → dom (𝐸 evalSub₁ 𝐹) = (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
60	57, 59	eleqtrrd 2864	. 2 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ∈ dom (𝐸 evalSub₁ 𝐹))
61		extdgfialglem2.4	. . 3 ⊢ (𝜑 → 𝐴 ≠ ((0...𝐷) × {𝑍}))
62		eqid 2761	. . . . . 6 ⊢ (Base‘(𝐸 ↾_s 𝐹)) = (Base‘(𝐸 ↾_s 𝐹))
63		eqid 2761	. . . . . 6 ⊢ (0_g‘(𝐸 ↾_s 𝐹)) = (0_g‘(𝐸 ↾_s 𝐹))
64	25	ffvelcdmda 7060	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ 𝐹)
65	64	adantlr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ 𝐹)
66	30	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
67	65, 66	eleqtrd 2863	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ (Base‘(𝐸 ↾_s 𝐹)))
68		subrgsubg 20614	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
69	10, 68	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
70	3	subg0cl 19167	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝑍 ∈ 𝐹)
71	69, 70	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝐹)
72	71, 30	eleqtrd 2863	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
73	72	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ ¬ 𝑚 ∈ (0...𝐷)) → 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
74	67, 73	ifclda 4513	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) ∈ (Base‘(𝐸 ↾_s 𝐹)))
75	74	ralrimiva 3153	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) ∈ (Base‘(𝐸 ↾_s 𝐹)))
76		eqid 2761	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) = (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍))
77		nn0ex 12481	. . . . . . . . 9 ⊢ ℕ₀ ∈ V
78	77	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℕ₀ ∈ V)
79	76, 78, 18, 64, 71	mptiffisupp 32856	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) finSupp 𝑍)
80	58	crngringd 20283	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ Ring)
81	80	ringcmnd 20321	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ CMnd)
82	81	cmnmndd 19835	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Mnd)
83	11, 6, 3	ress0g 18787	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ 𝑍 ∈ 𝐹 ∧ 𝐹 ⊆ 𝐵) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
84	82, 71, 28, 83	syl3anc 1389	. . . . . . 7 ⊢ (𝜑 → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
85	79, 84	breqtrd 5123	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) finSupp (0_g‘(𝐸 ↾_s 𝐹)))
86	72	ralrimivw 3157	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ₀ 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
87		fconstmpt 5705	. . . . . . . 8 ⊢ (ℕ₀ × {𝑍}) = (𝑚 ∈ ℕ₀ ↦ 𝑍)
88	78, 71	fczfsuppd 9326	. . . . . . . 8 ⊢ (𝜑 → (ℕ₀ × {𝑍}) finSupp 𝑍)
89	87, 88	eqbrtrrid 5133	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ 𝑍) finSupp 𝑍)
90	89, 84	breqtrd 5123	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ 𝑍) finSupp (0_g‘(𝐸 ↾_s 𝐹)))
91		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑚 ∈ (ℕ₀ ∖ (0...𝐷)))
92	91	eldifbd 3915	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → ¬ 𝑚 ∈ (0...𝐷))
93	92	iffalsed 4488	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍)
94	84	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
95	93, 94	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = (0_g‘(𝐸 ↾_s 𝐹)))
96	95	oveq1d 7406	. . . . . . . . 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 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
98	42	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
99	91	eldifad 3914	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑚 ∈ ℕ₀)
100	49	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
101	39, 40, 98, 99, 100	mulgnn0cld 19128	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
102	7, 33, 20, 63, 8	lmod0vs 20950	. . . . . . . . . 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 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
104	96, 103	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
105	23	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ LMod)
106	42	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ Mnd)
107		simpr 488	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → 𝑚 ∈ ℕ₀)
108	49	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
109	39, 40, 106, 107, 108	mulgnn0cld 19128	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
110	7, 33, 20, 62, 105, 74, 109	lmodvscld 20934	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
111	7, 8, 17, 78, 104, 18, 110, 45	gsummptres2 33194	. . . . . . 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 2844	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (0...𝐷) ↔ 𝑛 ∈ (0...𝐷)))
113		fveq2 6862	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝐴‘𝑚) = (𝐴‘𝑛))
114	112, 113	ifbieq1d 4502	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍))
115		oveq1 7398	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) = (𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))
116	114, 115	oveq12d 7409	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
117	116	cbvmptv 5201	. . . . . . . . 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 488	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ (0...𝐷))
119	118	iftrued 4485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = (𝐴‘𝑛))
120	119	oveq1d 7406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
121	120	mpteq2dva 5190	. . . . . . . . 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 2808	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ (0...𝐷) ↦ (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))))
123	122	oveq2d 7407	. . . . . . 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 2797	. . . . . 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 19835	. . . . . . . 8 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Mnd)
126	8	gsumz 18861	. . . . . . . 8 ⊢ (((Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Mnd ∧ ℕ₀ ∈ V) → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
127	125, 78, 126	syl2anc 593	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
128	84	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
129	128	oveq1d 7406	. . . . . . . . . 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 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
131	129, 130	eqtrd 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
132	131	mpteq2dva 5190	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹)))))
133	132	oveq2d 7407	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))))
134		eqid 2761	. . . . . . . 8 ⊢ (Poly₁‘𝐸) = (Poly₁‘𝐸)
135	134, 11, 14, 7, 10, 2	ressply10g 33724	. . . . . . 7 ⊢ (𝜑 → (0_g‘(Poly₁‘𝐸)) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
136	127, 133, 135	3eqtr4rd 2807	. . . . . 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 22360	. . . . 5 ⊢ (𝜑 → (((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (0_g‘(Poly₁‘𝐸)) ↔ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍))
138	25	ffnd 6687	. . . . . . . 8 ⊢ (𝜑 → 𝐴 Fn (0...𝐷))
139	138	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → 𝐴 Fn (0...𝐷))
140	119	adantlr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = (𝐴‘𝑛))
141	114	eqeq1d 2763	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍 ↔ if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = 𝑍))
142		simplr 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍)
143	44	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → (0...𝐷) ⊆ ℕ₀)
144	143	sselda 3934	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ₀)
145	141, 142, 144	rspcdva 3581	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = 𝑍)
146	140, 145	eqtr3d 2798	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) = 𝑍)
147	139, 146	fconst7v 32783	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → 𝐴 = ((0...𝐷) × {𝑍}))
148	147	ex 416	. . . . 5 ⊢ (𝜑 → (∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍 → 𝐴 = ((0...𝐷) × {𝑍})))
149	137, 148	sylbid 242	. . . 4 ⊢ (𝜑 → (((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (0_g‘(Poly₁‘𝐸)) → 𝐴 = ((0...𝐷) × {𝑍})))
150	149	necon3d 2977	. . 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 2761	. . . . 5 ⊢ (𝐸 ↑_s 𝐵) = (𝐸 ↑_s 𝐵)
153	1, 6, 14, 8, 11, 152, 7, 58, 10, 52, 45, 56	evls1gsumadd 22375	. . . 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 6864	. . 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 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝐸 ∈ CRing)
156	10	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝐹 ∈ (SubRing‘𝐸))
157	1, 14, 7, 155, 156, 6, 52	evls1fvf 33719	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))):𝐵⟶𝐵)
158	157	feqmptd 6930	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)))
159	158	mpteq2dva 5190	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))))
160	159	oveq2d 7407	. . . . . 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 6864	. . . . 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 2761	. . . . . . 7 ⊢ (0_g‘(𝐸 ↑_s 𝐵)) = (0_g‘(𝐸 ↑_s 𝐵))
163	6	fvexi 6876	. . . . . . . 8 ⊢ 𝐵 ∈ V
164	163	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ V)
165	155	adantr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝐸 ∈ CRing)
166	156	adantr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝐹 ∈ (SubRing‘𝐸))
167		simpr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
168	52	adantr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
169	1, 14, 6, 7, 165, 166, 167, 168	evls1fvcl 22426	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
170	169	an32s 662	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑛 ∈ (0...𝐷)) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
171	170	anasss 470	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑛 ∈ (0...𝐷))) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
172		eqid 2761	. . . . . . . 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 7203	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)) ∈ V)
175		fvexd 6877	. . . . . . . 8 ⊢ (𝜑 → (0_g‘(𝐸 ↑_s 𝐵)) ∈ V)
176	172, 18, 174, 175	fsuppmptdm 9316	. . . . . . 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 20013	. . . . . 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 6864	. . . . 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 2796	. . . 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 6862	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) = (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))
181	180	mpteq2dv 5191	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)) = (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)))
182	181	oveq2d 7407	. . . . 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 2762	. . . . 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 7426	. . . . 5 ⊢ (𝜑 → (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))) ∈ V)
186	182, 183, 184, 185	fvmptd4 6995	. . . 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 2761	. . . . . . . 8 ⊢ (._g‘(mulGrp‘𝐸)) = (._g‘(mulGrp‘𝐸))
188		extdgfialglem1.3	. . . . . . . 8 ⊢ · = (._r‘𝐸)
189	184	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑋 ∈ 𝐵)
190	1, 6, 14, 11, 47, 40, 187, 20, 188, 155, 156, 26, 46, 189	evls1monply1 33736	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋) = ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋)))
191	190	mpteq2dva 5190	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋))))
192		nfv 1933	. . . . . . . 8 ⊢ Ⅎ𝑛𝜑
193		ovexd 7426	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V)
194		extdgfialglem1.r	. . . . . . . 8 ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
195	192, 193, 194	fnmptd 6657	. . . . . . 7 ⊢ (𝜑 → 𝐺 Fn (0...𝐷))
196		inidm 4176	. . . . . . 7 ⊢ ((0...𝐷) ∩ (0...𝐷)) = (0...𝐷)
197		eqidd 2762	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) = (𝐴‘𝑛))
198	194	fvmpt2 6982	. . . . . . . . 9 ⊢ ((𝑛 ∈ (0...𝐷) ∧ (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
199	118, 193, 198	syl2anc 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
200		eqid 2761	. . . . . . . . . . 11 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
201	28, 6	sseqtrdi 3974	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
202	200, 80, 201	srapwov 33847	. . . . . . . . . 10 ⊢ (𝜑 → (._g‘(mulGrp‘𝐸)) = (._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹))))
203	202	oveqd 7408	. . . . . . . . 9 ⊢ (𝜑 → (𝑛(._g‘(mulGrp‘𝐸))𝑋) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
204	203	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘𝐸))𝑋) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
205	199, 204	eqtr4d 2799	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘𝐸))𝑋))
206	138, 195, 18, 18, 196, 197, 205	offval 7664	. . . . . 6 ⊢ (𝜑 → (𝐴 ∘_f · 𝐺) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋))))
207	191, 206	eqtr4d 2799	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)) = (𝐴 ∘_f · 𝐺))
208	207	oveq2d 7407	. . . 4 ⊢ (𝜑 → (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))) = (𝐸 Σ_g (𝐴 ∘_f · 𝐺)))
209	179, 186, 208	3eqtrd 2800	. . 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 2800	. 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 33948	1 ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∀wral 3075 Vcvv 3453 ∖ cdif 3899 ⊆ wss 3902 ifcif 4477 {csn 4579 class class class wbr 5097 ↦ cmpt 5178 × cxp 5641 dom cdm 5643 Fn wfn 6511 ⟶wf 6512 ‘cfv 6516 (class class class)co 7391 ∘_f cof 7653 Fincfn 8921 finSupp cfsupp 9301 0cc0 11067 ℕ₀cn0 12475 ...cfz 13506 Basecbs 17236 ↾_s cress 17257 ._rcmulr 17278 Scalarcsca 17280 ·_𝑠 cvsca 17281 0_gc0g 17459 Σ_g cgsu 17460 ↑_s cpws 17466 Mndcmnd 18759 ._gcmg 19100 SubGrpcsubg 19153 mulGrpcmgp 20177 Ringcrg 20270 CRingccrg 20271 SubRingcsubrg 20606 Fieldcfield 20767 SubDRingcsdrg 20823 LModclmod 20915 subringAlg csra 21226 var₁cv1 22226 Poly₁cpl1 22227 evalSub₁ ces1 22364 dimcldim 33857 IntgRing cirng 33941

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-addf 11146

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-se 5597 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-isom 6525 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-of 7655 df-ofr 7656 df-om 7842 df-1st 7965 df-2nd 7966 df-supp 8135 df-tpos 8200 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-2o 8432 df-er 8672 df-map 8804 df-pm 8805 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9302 df-sup 9382 df-oi 9452 df-card 9891 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-7 12279 df-8 12280 df-9 12281 df-n0 12476 df-z 12563 df-dec 12683 df-uz 12834 df-fz 13507 df-fzo 13654 df-seq 14009 df-hash 14338 df-struct 17174 df-sets 17191 df-slot 17209 df-ndx 17221 df-base 17237 df-ress 17258 df-plusg 17290 df-mulr 17291 df-starv 17292 df-sca 17293 df-vsca 17294 df-ip 17295 df-tset 17296 df-ple 17297 df-ds 17299 df-unif 17300 df-hom 17301 df-cco 17302 df-0g 17461 df-gsum 17462 df-prds 17467 df-pws 17469 df-mre 17605 df-mrc 17606 df-acs 17608 df-mgm 18665 df-sgrp 18744 df-mnd 18760 df-mhm 18808 df-submnd 18809 df-grp 18969 df-minusg 18970 df-sbg 18971 df-mulg 19101 df-subg 19156 df-ghm 19245 df-cntz 19348 df-cmn 19813 df-abl 19814 df-mgp 20178 df-rng 20190 df-ur 20219 df-srg 20224 df-ring 20272 df-cring 20273 df-oppr 20373 df-dvdsr 20393 df-unit 20394 df-invr 20424 df-rhm 20508 df-subrng 20583 df-subrg 20607 df-rlreg 20731 df-drng 20768 df-field 20769 df-sdrg 20824 df-lmod 20917 df-lss 20987 df-lsp 21027 df-sra 21228 df-cnfld 21413 df-assa 21893 df-asp 21894 df-ascl 21895 df-psr 21949 df-mvr 21950 df-mpl 21951 df-opsr 21953 df-evls 22115 df-evl 22116 df-psr1 22230 df-vr1 22231 df-ply1 22232 df-coe1 22233 df-evls1 22366 df-evl1 22367 df-mdeg 26103 df-deg1 26104 df-mon1 26179 df-uc1p 26180 df-irng 33942

This theorem is referenced by: extdgfialg 33952

W3C validator