This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )