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 33679

Description: Lemma for extdgfialg 33680. (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 2729	. 2 ⊢ (𝐸 evalSub₁ 𝐹) = (𝐸 evalSub₁ 𝐹)
2		eqid 2729	. 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 2729	. . . 4 ⊢ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Base‘(Poly₁‘(𝐸 ↾_s 𝐹)))
8		eqid 2729	. . . 4 ⊢ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹)))
9		sdrgsubrg 20695	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
10	5, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
11		eqid 2729	. . . . . . . 8 ⊢ (𝐸 ↾_s 𝐹) = (𝐸 ↾_s 𝐹)
12	11	subrgring 20478	. . . . . . 7 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (𝐸 ↾_s 𝐹) ∈ Ring)
13	10, 12	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐸 ↾_s 𝐹) ∈ Ring)
14		eqid 2729	. . . . . . 7 ⊢ (Poly₁‘(𝐸 ↾_s 𝐹)) = (Poly₁‘(𝐸 ↾_s 𝐹))
15	14	ply1ring 22149	. . . . . 6 ⊢ ((𝐸 ↾_s 𝐹) ∈ Ring → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring)
16	13, 15	syl 17	. . . . 5 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Ring)
17	16	ringcmnd 20188	. . . 4 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ CMnd)
18		fzfid 13899	. . . 4 ⊢ (𝜑 → (0...𝐷) ∈ Fin)
19		eqid 2729	. . . . . 6 ⊢ (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))
20		eqid 2729	. . . . . 6 ⊢ ( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹))) = ( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))
21		eqid 2729	. . . . . 6 ⊢ (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
22	14	ply1lmod 22153	. . . . . . . 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 7022	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) ∈ 𝐹)
27	6	sdrgss 20697	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝐵)
28	5, 27	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝐵)
29	11, 6	ressbas2 17168	. . . . . . . . . 10 ⊢ (𝐹 ⊆ 𝐵 → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
31		ovex 7386	. . . . . . . . . . 11 ⊢ (𝐸 ↾_s 𝐹) ∈ V
32	14	ply1sca 22154	. . . . . . . . . . 11 ⊢ ((𝐸 ↾_s 𝐹) ∈ V → (𝐸 ↾_s 𝐹) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
33	31, 32	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐸 ↾_s 𝐹) = (Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))
34	33	fveq2i 6829	. . . . . . . . 9 ⊢ (Base‘(𝐸 ↾_s 𝐹)) = (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹))))
35	30, 34	eqtr2di 2781	. . . . . . . 8 ⊢ (𝜑 → (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = 𝐹)
36	35	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = 𝐹)
37	26, 36	eleqtrrd 2831	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) ∈ (Base‘(Scalar‘(Poly₁‘(𝐸 ↾_s 𝐹)))))
38		eqid 2729	. . . . . . . 8 ⊢ (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹)))
39	38, 7	mgpbas 20049	. . . . . . 7 ⊢ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))) = (Base‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))
40		eqid 2729	. . . . . . 7 ⊢ (._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹)))) = (._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))
41	38	ringmgp 20143	. . . . . . . . 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 13544	. . . . . . . . 9 ⊢ (0...𝐷) ⊆ ℕ₀
45	44	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (0...𝐷) ⊆ ℕ₀)
46	45	sselda 3937	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ₀)
47		eqid 2729	. . . . . . . . . 10 ⊢ (var₁‘(𝐸 ↾_s 𝐹)) = (var₁‘(𝐸 ↾_s 𝐹))
48	47, 14, 7	vr1cl 22119	. . . . . . . . 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 18993	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
52	7, 19, 20, 21, 24, 37, 51	lmodvscld 20801	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
53	52	fmpttd 7053	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))):(0...𝐷)⟶(Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
54		eqid 2729	. . . . 5 ⊢ (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
55		fvexd 6841	. . . . 5 ⊢ (𝜑 → (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))) ∈ V)
56	54, 18, 52, 55	fsuppmptdm 9285	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) finSupp (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
57	7, 8, 17, 18, 53, 56	gsumcl 19813	. . 3 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
58	4	fldcrngd 20646	. . . 4 ⊢ (𝜑 → 𝐸 ∈ CRing)
59	1, 14, 7, 58, 10	evls1dm 33515	. . 3 ⊢ (𝜑 → dom (𝐸 evalSub₁ 𝐹) = (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
60	57, 59	eleqtrrd 2831	. 2 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) ∈ dom (𝐸 evalSub₁ 𝐹))
61		extdgfialglem2.4	. . 3 ⊢ (𝜑 → 𝐴 ≠ ((0...𝐷) × {𝑍}))
62		eqid 2729	. . . . . 6 ⊢ (Base‘(𝐸 ↾_s 𝐹)) = (Base‘(𝐸 ↾_s 𝐹))
63		eqid 2729	. . . . . 6 ⊢ (0_g‘(𝐸 ↾_s 𝐹)) = (0_g‘(𝐸 ↾_s 𝐹))
64	25	ffvelcdmda 7022	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ 𝐹)
65	64	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ 𝐹)
66	30	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → 𝐹 = (Base‘(𝐸 ↾_s 𝐹)))
67	65, 66	eleqtrd 2830	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ 𝑚 ∈ (0...𝐷)) → (𝐴‘𝑚) ∈ (Base‘(𝐸 ↾_s 𝐹)))
68		subrgsubg 20481	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
69	10, 68	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
70	3	subg0cl 19032	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝑍 ∈ 𝐹)
71	69, 70	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝐹)
72	71, 30	eleqtrd 2830	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
73	72	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ₀) ∧ ¬ 𝑚 ∈ (0...𝐷)) → 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
74	67, 73	ifclda 4514	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) ∈ (Base‘(𝐸 ↾_s 𝐹)))
75	74	ralrimiva 3121	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) ∈ (Base‘(𝐸 ↾_s 𝐹)))
76		eqid 2729	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) = (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍))
77		nn0ex 12409	. . . . . . . . 9 ⊢ ℕ₀ ∈ V
78	77	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℕ₀ ∈ V)
79	76, 78, 18, 64, 71	mptiffisupp 32654	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) finSupp 𝑍)
80	58	crngringd 20150	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ Ring)
81	80	ringcmnd 20188	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ CMnd)
82	81	cmnmndd 19702	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Mnd)
83	11, 6, 3	ress0g 18655	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ 𝑍 ∈ 𝐹 ∧ 𝐹 ⊆ 𝐵) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
84	82, 71, 28, 83	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
85	79, 84	breqtrd 5121	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)) finSupp (0_g‘(𝐸 ↾_s 𝐹)))
86	72	ralrimivw 3125	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ₀ 𝑍 ∈ (Base‘(𝐸 ↾_s 𝐹)))
87		fconstmpt 5685	. . . . . . . 8 ⊢ (ℕ₀ × {𝑍}) = (𝑚 ∈ ℕ₀ ↦ 𝑍)
88	78, 71	fczfsuppd 9295	. . . . . . . 8 ⊢ (𝜑 → (ℕ₀ × {𝑍}) finSupp 𝑍)
89	87, 88	eqbrtrrid 5131	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ 𝑍) finSupp 𝑍)
90	89, 84	breqtrd 5121	. . . . . 6 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ 𝑍) finSupp (0_g‘(𝐸 ↾_s 𝐹)))
91		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑚 ∈ (ℕ₀ ∖ (0...𝐷)))
92	91	eldifbd 3918	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → ¬ 𝑚 ∈ (0...𝐷))
93	92	iffalsed 4489	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍)
94	84	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
95	93, 94	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = (0_g‘(𝐸 ↾_s 𝐹)))
96	95	oveq1d 7368	. . . . . . . . 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 3917	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → 𝑚 ∈ ℕ₀)
100	49	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (var₁‘(𝐸 ↾_s 𝐹)) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
101	39, 40, 98, 99, 100	mulgnn0cld 18993	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
102	7, 33, 20, 63, 8	lmod0vs 20817	. . . . . . . . . 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 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℕ₀ ∖ (0...𝐷))) → ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
104	96, 103	eqtrd 2764	. . . . . . . 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 18993	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
110	7, 33, 20, 62, 105, 74, 109	lmodvscld 20801	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) ∈ (Base‘(Poly₁‘(𝐸 ↾_s 𝐹))))
111	7, 8, 17, 78, 104, 18, 110, 45	gsummptres2 33025	. . . . . . 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 2811	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ (0...𝐷) ↔ 𝑛 ∈ (0...𝐷)))
113		fveq2 6826	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝐴‘𝑚) = (𝐴‘𝑛))
114	112, 113	ifbieq1d 4503	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍))
115		oveq1 7360	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))) = (𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))
116	114, 115	oveq12d 7371	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
117	116	cbvmptv 5199	. . . . . . . . 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 4486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = (𝐴‘𝑛))
120	119	oveq1d 7368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))
121	120	mpteq2dva 5188	. . . . . . . . 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 2776	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ (0...𝐷) ↦ (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))))
123	122	oveq2d 7369	. . . . . . 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 2765	. . . . . 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 19702	. . . . . . . 8 ⊢ (𝜑 → (Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Mnd)
126	8	gsumz 18729	. . . . . . . 8 ⊢ (((Poly₁‘(𝐸 ↾_s 𝐹)) ∈ Mnd ∧ ℕ₀ ∈ V) → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
127	125, 78, 126	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
128	84	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → 𝑍 = (0_g‘(𝐸 ↾_s 𝐹)))
129	128	oveq1d 7368	. . . . . . . . . 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 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → ((0_g‘(𝐸 ↾_s 𝐹))( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
131	129, 130	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ₀) → (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
132	131	mpteq2dva 5188	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ ℕ₀ ↦ (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹))))) = (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹)))))
133	132	oveq2d 7369	. . . . . . 7 ⊢ (𝜑 → ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (𝑍( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑚(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = ((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑚 ∈ ℕ₀ ↦ (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))))
134		eqid 2729	. . . . . . . 8 ⊢ (Poly₁‘𝐸) = (Poly₁‘𝐸)
135	134, 11, 14, 7, 10, 2	ressply10g 33521	. . . . . . 7 ⊢ (𝜑 → (0_g‘(Poly₁‘𝐸)) = (0_g‘(Poly₁‘(𝐸 ↾_s 𝐹))))
136	127, 133, 135	3eqtr4rd 2775	. . . . . 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 22213	. . . . 5 ⊢ (𝜑 → (((Poly₁‘(𝐸 ↾_s 𝐹)) Σ_g (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (0_g‘(Poly₁‘𝐸)) ↔ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍))
138	25	ffnd 6657	. . . . . . . 8 ⊢ (𝜑 → 𝐴 Fn (0...𝐷))
139	138	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → 𝐴 Fn (0...𝐷))
140	119	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = (𝐴‘𝑛))
141	114	eqeq1d 2731	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍 ↔ if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = 𝑍))
142		simplr 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍)
143	44	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) → (0...𝐷) ⊆ ℕ₀)
144	143	sselda 3937	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → 𝑛 ∈ ℕ₀)
145	141, 142, 144	rspcdva 3580	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → if(𝑛 ∈ (0...𝐷), (𝐴‘𝑛), 𝑍) = 𝑍)
146	140, 145	eqtr3d 2766	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ₀ if(𝑚 ∈ (0...𝐷), (𝐴‘𝑚), 𝑍) = 𝑍) ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) = 𝑍)
147	139, 146	fconst7v 32584	. . . . . 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 2946	. . 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 2729	. . . . 5 ⊢ (𝐸 ↑_s 𝐵) = (𝐸 ↑_s 𝐵)
153	1, 6, 14, 8, 11, 152, 7, 58, 10, 52, 45, 56	evls1gsumadd 22228	. . . 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 6828	. . 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 33516	. . . . . . . . 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 5188	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ ((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))) = (𝑛 ∈ (0...𝐷) ↦ (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥))))
160	159	oveq2d 7369	. . . . . 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 6828	. . . . 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 2729	. . . . . . 7 ⊢ (0_g‘(𝐸 ↑_s 𝐵)) = (0_g‘(𝐸 ↑_s 𝐵))
163	6	fvexi 6840	. . . . . . . 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 22279	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...𝐷)) ∧ 𝑥 ∈ 𝐵) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) ∈ 𝐵)
170	169	an32s 652	. . . . . . . 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 2729	. . . . . . . 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 7164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑥 ∈ 𝐵 ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)) ∈ V)
175		fvexd 6841	. . . . . . . 8 ⊢ (𝜑 → (0_g‘(𝐸 ↑_s 𝐵)) ∈ V)
176	172, 18, 174, 175	fsuppmptdm 9285	. . . . . . 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 19880	. . . . . 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 6828	. . . . 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 2764	. . . 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 6826	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥) = (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))
181	180	mpteq2dv 5189	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑥)) = (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)))
182	181	oveq2d 7369	. . . . 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 2730	. . . . 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 7388	. . . . 5 ⊢ (𝜑 → (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))) ∈ V)
186	182, 183, 184, 185	fvmptd4 6958	. . . 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 2729	. . . . . . . 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 33533	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋) = ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋)))
191	190	mpteq2dva 5188	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋))))
192		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑛𝜑
193		ovexd 7388	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V)
194		extdgfialglem1.r	. . . . . . . 8 ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
195	192, 193, 194	fnmptd 6627	. . . . . . 7 ⊢ (𝜑 → 𝐺 Fn (0...𝐷))
196		inidm 4180	. . . . . . 7 ⊢ ((0...𝐷) ∩ (0...𝐷)) = (0...𝐷)
197		eqidd 2730	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐴‘𝑛) = (𝐴‘𝑛))
198	194	fvmpt2 6945	. . . . . . . . 9 ⊢ ((𝑛 ∈ (0...𝐷) ∧ (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋) ∈ V) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
199	118, 193, 198	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
200		eqid 2729	. . . . . . . . . . 11 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
201	28, 6	sseqtrdi 3978	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
202	200, 80, 201	srapwov 33574	. . . . . . . . . 10 ⊢ (𝜑 → (._g‘(mulGrp‘𝐸)) = (._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹))))
203	202	oveqd 7370	. . . . . . . . 9 ⊢ (𝜑 → (𝑛(._g‘(mulGrp‘𝐸))𝑋) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
204	203	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝑛(._g‘(mulGrp‘𝐸))𝑋) = (𝑛(._g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋))
205	199, 204	eqtr4d 2767	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝐷)) → (𝐺‘𝑛) = (𝑛(._g‘(mulGrp‘𝐸))𝑋))
206	138, 195, 18, 18, 196, 197, 205	offval 7626	. . . . . 6 ⊢ (𝜑 → (𝐴 ∘_f · 𝐺) = (𝑛 ∈ (0...𝐷) ↦ ((𝐴‘𝑛) · (𝑛(._g‘(mulGrp‘𝐸))𝑋))))
207	191, 206	eqtr4d 2767	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋)) = (𝐴 ∘_f · 𝐺))
208	207	oveq2d 7369	. . . 4 ⊢ (𝜑 → (𝐸 Σ_g (𝑛 ∈ (0...𝐷) ↦ (((𝐸 evalSub₁ 𝐹)‘((𝐴‘𝑛)( ·_𝑠 ‘(Poly₁‘(𝐸 ↾_s 𝐹)))(𝑛(._g‘(mulGrp‘(Poly₁‘(𝐸 ↾_s 𝐹))))(var₁‘(𝐸 ↾_s 𝐹)))))‘𝑋))) = (𝐸 Σ_g (𝐴 ∘_f · 𝐺)))
209	179, 186, 208	3eqtrd 2768	. . 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 2768	. 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 33676	1 ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 Vcvv 3438 ∖ cdif 3902 ⊆ wss 3905 ifcif 4478 {csn 4579 class class class wbr 5095 ↦ cmpt 5176 × cxp 5621 dom cdm 5623 Fn wfn 6481 ⟶wf 6482 ‘cfv 6486 (class class class)co 7353 ∘_f cof 7615 Fincfn 8879 finSupp cfsupp 9270 0cc0 11028 ℕ₀cn0 12403 ...cfz 13429 Basecbs 17139 ↾_s cress 17160 ._rcmulr 17181 Scalarcsca 17183 ·_𝑠 cvsca 17184 0_gc0g 17362 Σ_g cgsu 17363 ↑_s cpws 17369 Mndcmnd 18627 ._gcmg 18965 SubGrpcsubg 19018 mulGrpcmgp 20044 Ringcrg 20137 CRingccrg 20138 SubRingcsubrg 20473 Fieldcfield 20634 SubDRingcsdrg 20690 LModclmod 20782 subringAlg csra 21094 var₁cv1 22077 Poly₁cpl1 22078 evalSub₁ ces1 22217 dimcldim 33584 IntgRing cirng 33669

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-addf 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-ofr 7618 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 8632 df-map 8762 df-pm 8763 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9271 df-sup 9351 df-oi 9421 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-nn 12148 df-2 12210 df-3 12211 df-4 12212 df-5 12213 df-6 12214 df-7 12215 df-8 12216 df-9 12217 df-n0 12404 df-z 12491 df-dec 12611 df-uz 12755 df-fz 13430 df-fzo 13577 df-seq 13928 df-hash 14257 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17140 df-ress 17161 df-plusg 17193 df-mulr 17194 df-starv 17195 df-sca 17196 df-vsca 17197 df-ip 17198 df-tset 17199 df-ple 17200 df-ds 17202 df-unif 17203 df-hom 17204 df-cco 17205 df-0g 17364 df-gsum 17365 df-prds 17370 df-pws 17372 df-mre 17507 df-mrc 17508 df-acs 17510 df-mgm 18533 df-sgrp 18612 df-mnd 18628 df-mhm 18676 df-submnd 18677 df-grp 18834 df-minusg 18835 df-sbg 18836 df-mulg 18966 df-subg 19021 df-ghm 19111 df-cntz 19215 df-cmn 19680 df-abl 19681 df-mgp 20045 df-rng 20057 df-ur 20086 df-srg 20091 df-ring 20139 df-cring 20140 df-oppr 20241 df-dvdsr 20261 df-unit 20262 df-invr 20292 df-rhm 20376 df-subrng 20450 df-subrg 20474 df-rlreg 20598 df-drng 20635 df-field 20636 df-sdrg 20691 df-lmod 20784 df-lss 20854 df-lsp 20894 df-sra 21096 df-cnfld 21281 df-assa 21779 df-asp 21780 df-ascl 21781 df-psr 21835 df-mvr 21836 df-mpl 21837 df-opsr 21839 df-evls 21998 df-evl 21999 df-psr1 22081 df-vr1 22082 df-ply1 22083 df-coe1 22084 df-evls1 22219 df-evl1 22220 df-mdeg 25977 df-deg1 25978 df-mon1 26053 df-uc1p 26054 df-irng 33670

This theorem is referenced by: extdgfialg 33680

W3C validator