Theorem extdgfialglem2

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

	Ref	Expression
Hypotheses	extdgfialg.b	|- B = ( Base ` E )
	extdgfialg.d	|- D = ( dim ` ( ( subringAlg ` E ) ` F ) )
	extdgfialg.e	|- ( ph -> E e. Field )
	extdgfialg.f	|- ( ph -> F e. ( SubDRing ` E ) )
	extdgfialg.1	|- ( ph -> D e. NN0 )
	extdgfialglem1.2	|- Z = ( 0g ` E )
	extdgfialglem1.3	|- .x. = ( .r ` E )
	extdgfialglem1.r	|- G = ( n e. ( 0 ... D ) |-> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) )
	extdgfialglem1.4	|- ( ph -> X e. B )
	extdgfialglem2.1	|- ( ph -> A : ( 0 ... D ) --> F )
	extdgfialglem2.2	|- ( ph -> A finSupp Z )
	extdgfialglem2.3	|- ( ph -> ( E gsum ( A oF .x. G ) ) = Z )
	extdgfialglem2.4	|- ( ph -> A =/= ( ( 0 ... D ) X. { Z } ) )
Assertion	extdgfialglem2	|- ( ph -> X e. ( E IntgRing F ) )

Proof

Step	Hyp	Ref	Expression
1		extdgfialg.b	|- B = ( Base ` E )
2		extdgfialg.d	|- D = ( dim ` ( ( subringAlg ` E ) ` F ) )
3		extdgfialg.e	|- ( ph -> E e. Field )
4		extdgfialg.f	|- ( ph -> F e. ( SubDRing ` E ) )
5		extdgfialg.1	|- ( ph -> D e. NN0 )
6		extdgfialglem1.2	|- Z = ( 0g ` E )
7		extdgfialglem1.3	|- .x. = ( .r ` E )
8		extdgfialglem1.r	|- G = ( n e. ( 0 ... D ) |-> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) )
9		extdgfialglem1.4	|- ( ph -> X e. B )
10		extdgfialglem2.1	|- ( ph -> A : ( 0 ... D ) --> F )
11		extdgfialglem2.2	|- ( ph -> A finSupp Z )
12		extdgfialglem2.3	|- ( ph -> ( E gsum ( A oF .x. G ) ) = Z )
13		extdgfialglem2.4	|- ( ph -> A =/= ( ( 0 ... D ) X. { Z } ) )
14		eqid	|- ( E evalSub1 F ) = ( E evalSub1 F )
15		eqid	|- ( 0g ` ( Poly1 ` E ) ) = ( 0g ` ( Poly1 ` E ) )
16		eqid	|- ( Base ` ( Poly1 ` ( E |`s F ) ) ) = ( Base ` ( Poly1 ` ( E |`s F ) ) )
17		eqid	|- ( 0g ` ( Poly1 ` ( E |`s F ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) )
18		sdrgsubrg	|- ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
19	4 18	syl	|- ( ph -> F e. ( SubRing ` E ) )
20		eqid	|- ( E |`s F ) = ( E |`s F )
21	20	subrgring	|- ( F e. ( SubRing ` E ) -> ( E |`s F ) e. Ring )
22	19 21	syl	|- ( ph -> ( E |`s F ) e. Ring )
23		eqid	|- ( Poly1 ` ( E |`s F ) ) = ( Poly1 ` ( E |`s F ) )
24	23	ply1ring	|- ( ( E |`s F ) e. Ring -> ( Poly1 ` ( E |`s F ) ) e. Ring )
25	22 24	syl	|- ( ph -> ( Poly1 ` ( E |`s F ) ) e. Ring )
26	25	ringcmnd	|- ( ph -> ( Poly1 ` ( E |`s F ) ) e. CMnd )
27		fzfid	|- ( ph -> ( 0 ... D ) e. Fin )
28		eqid	|- ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) = ( Scalar ` ( Poly1 ` ( E |`s F ) ) )
29		eqid	|- ( .s ` ( Poly1 ` ( E |`s F ) ) ) = ( .s ` ( Poly1 ` ( E |`s F ) ) )
30		eqid	|- ( Base ` ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) ) = ( Base ` ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) )
31	23	ply1lmod	|- ( ( E |`s F ) e. Ring -> ( Poly1 ` ( E |`s F ) ) e. LMod )
32	22 31	syl	|- ( ph -> ( Poly1 ` ( E |`s F ) ) e. LMod )
33	32	adantr	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( Poly1 ` ( E |`s F ) ) e. LMod )
34	10	ffvelcdmda	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( A ` n ) e. F )
35	1	sdrgss	|- ( F e. ( SubDRing ` E ) -> F C_ B )
36	4 35	syl	|- ( ph -> F C_ B )
37	20 1	ressbas2	|- ( F C_ B -> F = ( Base ` ( E |`s F ) ) )
38	36 37	syl	|- ( ph -> F = ( Base ` ( E |`s F ) ) )
39		ovex	|- ( E |`s F ) e. _V
40	23	ply1sca	|- ( ( E |`s F ) e. _V -> ( E |`s F ) = ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) )
41	39 40	ax-mp	|- ( E |`s F ) = ( Scalar ` ( Poly1 ` ( E |`s F ) ) )
42	41	fveq2i	|- ( Base ` ( E |`s F ) ) = ( Base ` ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) )
43	38 42	eqtr2di	|- ( ph -> ( Base ` ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) ) = F )
44	43	adantr	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( Base ` ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) ) = F )
45	34 44	eleqtrrd	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( A ` n ) e. ( Base ` ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) ) )
46		eqid	|- ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) = ( mulGrp ` ( Poly1 ` ( E |`s F ) ) )
47	46 16	mgpbas	|- ( Base ` ( Poly1 ` ( E |`s F ) ) ) = ( Base ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) )
48		eqid	|- ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) )
49	46	ringmgp	|- ( ( Poly1 ` ( E |`s F ) ) e. Ring -> ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) e. Mnd )
50	25 49	syl	|- ( ph -> ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) e. Mnd )
51	50	adantr	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) e. Mnd )
52		fz0ssnn0	|- ( 0 ... D ) C_ NN0
53	52	a1i	|- ( ph -> ( 0 ... D ) C_ NN0 )
54	53	sselda	|- ( ( ph /\ n e. ( 0 ... D ) ) -> n e. NN0 )
55		eqid	|- ( var1 ` ( E |`s F ) ) = ( var1 ` ( E |`s F ) )
56	55 23 16	vr1cl	|- ( ( E |`s F ) e. Ring -> ( var1 ` ( E |`s F ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
57	22 56	syl	|- ( ph -> ( var1 ` ( E |`s F ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
58	57	adantr	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( var1 ` ( E |`s F ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
59	47 48 51 54 58	mulgnn0cld	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
60	16 28 29 30 33 45 59	lmodvscld	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
61	60	fmpttd	|- ( ph -> ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) : ( 0 ... D ) --> ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
62		eqid	|- ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) = ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) )
63		fvexd	|- ( ph -> ( 0g ` ( Poly1 ` ( E |`s F ) ) ) e. _V )
64	62 27 60 63	fsuppmptdm	|- ( ph -> ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) finSupp ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
65	16 17 26 27 61 64	gsumcl	|- ( ph -> ( ( Poly1 ` ( E |`s F ) ) gsum ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
66	3	fldcrngd	|- ( ph -> E e. CRing )
67	14 23 16 66 19	evls1dm	|- ( ph -> dom ( E evalSub1 F ) = ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
68	65 67	eleqtrrd	|- ( ph -> ( ( Poly1 ` ( E |`s F ) ) gsum ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) e. dom ( E evalSub1 F ) )
69		eqid	|- ( Base ` ( E |`s F ) ) = ( Base ` ( E |`s F ) )
70		eqid	|- ( 0g ` ( E |`s F ) ) = ( 0g ` ( E |`s F ) )
71	10	ffvelcdmda	|- ( ( ph /\ m e. ( 0 ... D ) ) -> ( A ` m ) e. F )
72	71	adantlr	|- ( ( ( ph /\ m e. NN0 ) /\ m e. ( 0 ... D ) ) -> ( A ` m ) e. F )
73	38	ad2antrr	|- ( ( ( ph /\ m e. NN0 ) /\ m e. ( 0 ... D ) ) -> F = ( Base ` ( E |`s F ) ) )
74	72 73	eleqtrd	|- ( ( ( ph /\ m e. NN0 ) /\ m e. ( 0 ... D ) ) -> ( A ` m ) e. ( Base ` ( E |`s F ) ) )
75		subrgsubg	|- ( F e. ( SubRing ` E ) -> F e. ( SubGrp ` E ) )
76	19 75	syl	|- ( ph -> F e. ( SubGrp ` E ) )
77	6	subg0cl	|- ( F e. ( SubGrp ` E ) -> Z e. F )
78	76 77	syl	|- ( ph -> Z e. F )
79	78 38	eleqtrd	|- ( ph -> Z e. ( Base ` ( E |`s F ) ) )
80	79	ad2antrr	|- ( ( ( ph /\ m e. NN0 ) /\ -. m e. ( 0 ... D ) ) -> Z e. ( Base ` ( E |`s F ) ) )
81	74 80	ifclda	|- ( ( ph /\ m e. NN0 ) -> if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) e. ( Base ` ( E |`s F ) ) )
82	81	ralrimiva	|- ( ph -> A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) e. ( Base ` ( E |`s F ) ) )
83		eqid	|- ( m e. NN0 |-> if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ) = ( m e. NN0 |-> if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) )
84		nn0ex	|- NN0 e. _V
85	84	a1i	|- ( ph -> NN0 e. _V )
86	83 85 27 71 78	mptiffisupp	|- ( ph -> ( m e. NN0 |-> if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ) finSupp Z )
87	66	crngringd	|- ( ph -> E e. Ring )
88	87	ringcmnd	|- ( ph -> E e. CMnd )
89	88	cmnmndd	|- ( ph -> E e. Mnd )
90	20 1 6	ress0g	|- ( ( E e. Mnd /\ Z e. F /\ F C_ B ) -> Z = ( 0g ` ( E |`s F ) ) )
91	89 78 36 90	syl3anc	|- ( ph -> Z = ( 0g ` ( E |`s F ) ) )
92	86 91	breqtrd	|- ( ph -> ( m e. NN0 |-> if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ) finSupp ( 0g ` ( E |`s F ) ) )
93	79	ralrimivw	|- ( ph -> A. m e. NN0 Z e. ( Base ` ( E |`s F ) ) )
94		fconstmpt	|- ( NN0 X. { Z } ) = ( m e. NN0 |-> Z )
95	85 78	fczfsuppd	|- ( ph -> ( NN0 X. { Z } ) finSupp Z )
96	94 95	eqbrtrrid	|- ( ph -> ( m e. NN0 |-> Z ) finSupp Z )
97	96 91	breqtrd	|- ( ph -> ( m e. NN0 |-> Z ) finSupp ( 0g ` ( E |`s F ) ) )
98		simpr	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> m e. ( NN0 \ ( 0 ... D ) ) )
99	98	eldifbd	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> -. m e. ( 0 ... D ) )
100	99	iffalsed	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z )
101	91	adantr	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> Z = ( 0g ` ( E |`s F ) ) )
102	100 101	eqtrd	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = ( 0g ` ( E |`s F ) ) )
103	102	oveq1d	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> ( if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) = ( ( 0g ` ( E |`s F ) ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) )
104	32	adantr	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> ( Poly1 ` ( E |`s F ) ) e. LMod )
105	50	adantr	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) e. Mnd )
106	98	eldifad	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> m e. NN0 )
107	57	adantr	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> ( var1 ` ( E |`s F ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
108	47 48 105 106 107	mulgnn0cld	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
109	16 41 29 70 17	lmod0vs	|- ( ( ( Poly1 ` ( E |`s F ) ) e. LMod /\ ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) ) -> ( ( 0g ` ( E |`s F ) ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
110	104 108 109	syl2anc	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> ( ( 0g ` ( E |`s F ) ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
111	103 110	eqtrd	|- ( ( ph /\ m e. ( NN0 \ ( 0 ... D ) ) ) -> ( if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
112	32	adantr	|- ( ( ph /\ m e. NN0 ) -> ( Poly1 ` ( E |`s F ) ) e. LMod )
113	50	adantr	|- ( ( ph /\ m e. NN0 ) -> ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) e. Mnd )
114		simpr	|- ( ( ph /\ m e. NN0 ) -> m e. NN0 )
115	57	adantr	|- ( ( ph /\ m e. NN0 ) -> ( var1 ` ( E |`s F ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
116	47 48 113 114 115	mulgnn0cld	|- ( ( ph /\ m e. NN0 ) -> ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
117	16 41 29 69 112 81 116	lmodvscld	|- ( ( ph /\ m e. NN0 ) -> ( if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
118	16 17 26 85 111 27 117 53	gsummptres2	|- ( ph -> ( ( Poly1 ` ( E |`s F ) ) gsum ( m e. NN0 |-> ( if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) = ( ( Poly1 ` ( E |`s F ) ) gsum ( m e. ( 0 ... D ) |-> ( if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) )
119		eleq1w	|- ( m = n -> ( m e. ( 0 ... D ) <-> n e. ( 0 ... D ) ) )
120		fveq2	|- ( m = n -> ( A ` m ) = ( A ` n ) )
121	119 120	ifbieq1d	|- ( m = n -> if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = if ( n e. ( 0 ... D ) , ( A ` n ) , Z ) )
122		oveq1	|- ( m = n -> ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) = ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) )
123	121 122	oveq12d	|- ( m = n -> ( if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) = ( if ( n e. ( 0 ... D ) , ( A ` n ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) )
124	123	cbvmptv	|- ( m e. ( 0 ... D ) |-> ( if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) = ( n e. ( 0 ... D ) |-> ( if ( n e. ( 0 ... D ) , ( A ` n ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) )
125		simpr	|- ( ( ph /\ n e. ( 0 ... D ) ) -> n e. ( 0 ... D ) )
126	125	iftrued	|- ( ( ph /\ n e. ( 0 ... D ) ) -> if ( n e. ( 0 ... D ) , ( A ` n ) , Z ) = ( A ` n ) )
127	126	oveq1d	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( if ( n e. ( 0 ... D ) , ( A ` n ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) = ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) )
128	127	mpteq2dva	|- ( ph -> ( n e. ( 0 ... D ) |-> ( if ( n e. ( 0 ... D ) , ( A ` n ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) = ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) )
129	124 128	eqtrid	|- ( ph -> ( m e. ( 0 ... D ) |-> ( if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) = ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) )
130	129	oveq2d	|- ( ph -> ( ( Poly1 ` ( E |`s F ) ) gsum ( m e. ( 0 ... D ) |-> ( if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) = ( ( Poly1 ` ( E |`s F ) ) gsum ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) )
131	118 130	eqtr2d	|- ( ph -> ( ( Poly1 ` ( E |`s F ) ) gsum ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) = ( ( Poly1 ` ( E |`s F ) ) gsum ( m e. NN0 |-> ( if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) )
132	26	cmnmndd	|- ( ph -> ( Poly1 ` ( E |`s F ) ) e. Mnd )
133	17	gsumz	|- ( ( ( Poly1 ` ( E |`s F ) ) e. Mnd /\ NN0 e. _V ) -> ( ( Poly1 ` ( E |`s F ) ) gsum ( m e. NN0 |-> ( 0g ` ( Poly1 ` ( E |`s F ) ) ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
134	132 85 133	syl2anc	|- ( ph -> ( ( Poly1 ` ( E |`s F ) ) gsum ( m e. NN0 |-> ( 0g ` ( Poly1 ` ( E |`s F ) ) ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
135	91	adantr	|- ( ( ph /\ m e. NN0 ) -> Z = ( 0g ` ( E |`s F ) ) )
136	135	oveq1d	|- ( ( ph /\ m e. NN0 ) -> ( Z ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) = ( ( 0g ` ( E |`s F ) ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) )
137	112 116 109	syl2anc	|- ( ( ph /\ m e. NN0 ) -> ( ( 0g ` ( E |`s F ) ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
138	136 137	eqtrd	|- ( ( ph /\ m e. NN0 ) -> ( Z ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
139	138	mpteq2dva	|- ( ph -> ( m e. NN0 |-> ( Z ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) = ( m e. NN0 |-> ( 0g ` ( Poly1 ` ( E |`s F ) ) ) ) )
140	139	oveq2d	|- ( ph -> ( ( Poly1 ` ( E |`s F ) ) gsum ( m e. NN0 |-> ( Z ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) = ( ( Poly1 ` ( E |`s F ) ) gsum ( m e. NN0 |-> ( 0g ` ( Poly1 ` ( E |`s F ) ) ) ) ) )
141		eqid	|- ( Poly1 ` E ) = ( Poly1 ` E )
142	141 20 23 16 19 15	ressply10g	|- ( ph -> ( 0g ` ( Poly1 ` E ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
143	134 140 142	3eqtr4rd	|- ( ph -> ( 0g ` ( Poly1 ` E ) ) = ( ( Poly1 ` ( E |`s F ) ) gsum ( m e. NN0 |-> ( Z ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( m ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) )
144	23 55 48 22 69 29 70 82 92 93 97 131 143	gsumply1eq	|- ( ph -> ( ( ( Poly1 ` ( E |`s F ) ) gsum ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) = ( 0g ` ( Poly1 ` E ) ) <-> A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z ) )
145	10	ffnd	|- ( ph -> A Fn ( 0 ... D ) )
146	145	adantr	|- ( ( ph /\ A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z ) -> A Fn ( 0 ... D ) )
147	126	adantlr	|- ( ( ( ph /\ A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z ) /\ n e. ( 0 ... D ) ) -> if ( n e. ( 0 ... D ) , ( A ` n ) , Z ) = ( A ` n ) )
148	121	eqeq1d	|- ( m = n -> ( if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z <-> if ( n e. ( 0 ... D ) , ( A ` n ) , Z ) = Z ) )
149		simplr	|- ( ( ( ph /\ A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z ) /\ n e. ( 0 ... D ) ) -> A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z )
150	52	a1i	|- ( ( ph /\ A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z ) -> ( 0 ... D ) C_ NN0 )
151	150	sselda	|- ( ( ( ph /\ A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z ) /\ n e. ( 0 ... D ) ) -> n e. NN0 )
152	148 149 151	rspcdva	|- ( ( ( ph /\ A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z ) /\ n e. ( 0 ... D ) ) -> if ( n e. ( 0 ... D ) , ( A ` n ) , Z ) = Z )
153	147 152	eqtr3d	|- ( ( ( ph /\ A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z ) /\ n e. ( 0 ... D ) ) -> ( A ` n ) = Z )
154	146 153	fconst7v	|- ( ( ph /\ A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z ) -> A = ( ( 0 ... D ) X. { Z } ) )
155	154	ex	|- ( ph -> ( A. m e. NN0 if ( m e. ( 0 ... D ) , ( A ` m ) , Z ) = Z -> A = ( ( 0 ... D ) X. { Z } ) ) )
156	144 155	sylbid	|- ( ph -> ( ( ( Poly1 ` ( E |`s F ) ) gsum ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) = ( 0g ` ( Poly1 ` E ) ) -> A = ( ( 0 ... D ) X. { Z } ) ) )
157	156	necon3d	|- ( ph -> ( A =/= ( ( 0 ... D ) X. { Z } ) -> ( ( Poly1 ` ( E |`s F ) ) gsum ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) =/= ( 0g ` ( Poly1 ` E ) ) ) )
158	13 157	mpd	|- ( ph -> ( ( Poly1 ` ( E |`s F ) ) gsum ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) =/= ( 0g ` ( Poly1 ` E ) ) )
159		eqid	|- ( E ^s B ) = ( E ^s B )
160	14 1 23 17 20 159 16 66 19 60 53 64	evls1gsumadd	|- ( ph -> ( ( E evalSub1 F ) ` ( ( Poly1 ` ( E |`s F ) ) gsum ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) ) = ( ( E ^s B ) gsum ( n e. ( 0 ... D ) |-> ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) ) )
161	160	fveq1d	|- ( ph -> ( ( ( E evalSub1 F ) ` ( ( Poly1 ` ( E |`s F ) ) gsum ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) ) ` X ) = ( ( ( E ^s B ) gsum ( n e. ( 0 ... D ) |-> ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) ) ` X ) )
162	66	adantr	|- ( ( ph /\ n e. ( 0 ... D ) ) -> E e. CRing )
163	19	adantr	|- ( ( ph /\ n e. ( 0 ... D ) ) -> F e. ( SubRing ` E ) )
164	14 23 16 162 163 1 60	evls1fvf	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) : B --> B )
165	164	feqmptd	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) = ( x e. B |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) )
166	165	mpteq2dva	|- ( ph -> ( n e. ( 0 ... D ) |-> ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) = ( n e. ( 0 ... D ) |-> ( x e. B |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) )
167	166	oveq2d	|- ( ph -> ( ( E ^s B ) gsum ( n e. ( 0 ... D ) |-> ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) ) = ( ( E ^s B ) gsum ( n e. ( 0 ... D ) |-> ( x e. B |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) ) )
168	167	fveq1d	|- ( ph -> ( ( ( E ^s B ) gsum ( n e. ( 0 ... D ) |-> ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) ) ` X ) = ( ( ( E ^s B ) gsum ( n e. ( 0 ... D ) |-> ( x e. B |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) ) ` X ) )
169		eqid	|- ( 0g ` ( E ^s B ) ) = ( 0g ` ( E ^s B ) )
170	1	fvexi	|- B e. _V
171	170	a1i	|- ( ph -> B e. _V )
172	162	adantr	|- ( ( ( ph /\ n e. ( 0 ... D ) ) /\ x e. B ) -> E e. CRing )
173	163	adantr	|- ( ( ( ph /\ n e. ( 0 ... D ) ) /\ x e. B ) -> F e. ( SubRing ` E ) )
174		simpr	|- ( ( ( ph /\ n e. ( 0 ... D ) ) /\ x e. B ) -> x e. B )
175	60	adantr	|- ( ( ( ph /\ n e. ( 0 ... D ) ) /\ x e. B ) -> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
176	14 23 1 16 172 173 174 175	evls1fvcl	|- ( ( ( ph /\ n e. ( 0 ... D ) ) /\ x e. B ) -> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) e. B )
177	176	an32s	|- ( ( ( ph /\ x e. B ) /\ n e. ( 0 ... D ) ) -> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) e. B )
178	177	anasss	|- ( ( ph /\ ( x e. B /\ n e. ( 0 ... D ) ) ) -> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) e. B )
179		eqid	|- ( n e. ( 0 ... D ) |-> ( x e. B |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) = ( n e. ( 0 ... D ) |-> ( x e. B |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) )
180	170	a1i	|- ( ( ph /\ n e. ( 0 ... D ) ) -> B e. _V )
181	180	mptexd	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( x e. B |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) e. _V )
182		fvexd	|- ( ph -> ( 0g ` ( E ^s B ) ) e. _V )
183	179 27 181 182	fsuppmptdm	|- ( ph -> ( n e. ( 0 ... D ) |-> ( x e. B |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) finSupp ( 0g ` ( E ^s B ) ) )
184	159 1 169 171 27 88 178 183	pwsgsum	|- ( ph -> ( ( E ^s B ) gsum ( n e. ( 0 ... D ) |-> ( x e. B |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) ) = ( x e. B |-> ( E gsum ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) ) )
185	184	fveq1d	|- ( ph -> ( ( ( E ^s B ) gsum ( n e. ( 0 ... D ) |-> ( x e. B |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) ) ` X ) = ( ( x e. B |-> ( E gsum ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) ) ` X ) )
186	168 185	eqtrd	|- ( ph -> ( ( ( E ^s B ) gsum ( n e. ( 0 ... D ) |-> ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) ) ` X ) = ( ( x e. B |-> ( E gsum ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) ) ` X ) )
187		fveq2	|- ( x = X -> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) = ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` X ) )
188	187	mpteq2dv	|- ( x = X -> ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) = ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` X ) ) )
189	188	oveq2d	|- ( x = X -> ( E gsum ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) = ( E gsum ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` X ) ) ) )
190		eqidd	|- ( ph -> ( x e. B |-> ( E gsum ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) ) = ( x e. B |-> ( E gsum ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) ) )
191		ovexd	|- ( ph -> ( E gsum ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` X ) ) ) e. _V )
192	189 190 9 191	fvmptd4	|- ( ph -> ( ( x e. B |-> ( E gsum ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` x ) ) ) ) ` X ) = ( E gsum ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` X ) ) ) )
193		eqid	|- ( .g ` ( mulGrp ` E ) ) = ( .g ` ( mulGrp ` E ) )
194	9	adantr	|- ( ( ph /\ n e. ( 0 ... D ) ) -> X e. B )
195	14 1 23 20 55 48 193 29 7 162 163 34 54 194	evls1monply1	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` X ) = ( ( A ` n ) .x. ( n ( .g ` ( mulGrp ` E ) ) X ) ) )
196	195	mpteq2dva	|- ( ph -> ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` X ) ) = ( n e. ( 0 ... D ) |-> ( ( A ` n ) .x. ( n ( .g ` ( mulGrp ` E ) ) X ) ) ) )
197		nfv	|- F/ n ph
198		ovexd	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) e. _V )
199	197 198 8	fnmptd	|- ( ph -> G Fn ( 0 ... D ) )
200		inidm	|- ( ( 0 ... D ) i^i ( 0 ... D ) ) = ( 0 ... D )
201		eqidd	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( A ` n ) = ( A ` n ) )
202	8	fvmpt2	|- ( ( n e. ( 0 ... D ) /\ ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) e. _V ) -> ( G ` n ) = ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) )
203	125 198 202	syl2anc	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( G ` n ) = ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) )
204		eqid	|- ( ( subringAlg ` E ) ` F ) = ( ( subringAlg ` E ) ` F )
205	36 1	sseqtrdi	|- ( ph -> F C_ ( Base ` E ) )
206	204 87 205	srapwov	|- ( ph -> ( .g ` ( mulGrp ` E ) ) = ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) )
207	206	oveqd	|- ( ph -> ( n ( .g ` ( mulGrp ` E ) ) X ) = ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) )
208	207	adantr	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( n ( .g ` ( mulGrp ` E ) ) X ) = ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) )
209	203 208	eqtr4d	|- ( ( ph /\ n e. ( 0 ... D ) ) -> ( G ` n ) = ( n ( .g ` ( mulGrp ` E ) ) X ) )
210	145 199 27 27 200 201 209	offval	|- ( ph -> ( A oF .x. G ) = ( n e. ( 0 ... D ) |-> ( ( A ` n ) .x. ( n ( .g ` ( mulGrp ` E ) ) X ) ) ) )
211	196 210	eqtr4d	|- ( ph -> ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` X ) ) = ( A oF .x. G ) )
212	211	oveq2d	|- ( ph -> ( E gsum ( n e. ( 0 ... D ) |-> ( ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ` X ) ) ) = ( E gsum ( A oF .x. G ) ) )
213	186 192 212	3eqtrd	|- ( ph -> ( ( ( E ^s B ) gsum ( n e. ( 0 ... D ) |-> ( ( E evalSub1 F ) ` ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) ) ` X ) = ( E gsum ( A oF .x. G ) ) )
214	161 213 12	3eqtrd	|- ( ph -> ( ( ( E evalSub1 F ) ` ( ( Poly1 ` ( E |`s F ) ) gsum ( n e. ( 0 ... D ) |-> ( ( A ` n ) ( .s ` ( Poly1 ` ( E |`s F ) ) ) ( n ( .g ` ( mulGrp ` ( Poly1 ` ( E |`s F ) ) ) ) ( var1 ` ( E |`s F ) ) ) ) ) ) ) ` X ) = Z )
215	14 15 6 3 4 1 68 158 214 9	irngnzply1lem	|- ( ph -> X e. ( E IntgRing F ) )