Metamath Proof Explorer

Theorem evls1fldgencl

Description: Closure of the subring polynomial evaluation in the field extention. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses evls1fldgencl.1 
|- B = ( Base ` E )
evls1fldgencl.2 
|- O = ( E evalSub1 F )
evls1fldgencl.3 
|- P = ( Poly1 ` ( E |`s F ) )
evls1fldgencl.4 
|- U = ( Base ` P )
evls1fldgencl.5 
|- ( ph -> E e. Field )
evls1fldgencl.6 
|- ( ph -> F e. ( SubDRing ` E ) )
evls1fldgencl.7 
|- ( ph -> A e. B )
evls1fldgencl.8 
|- ( ph -> G e. U )
Assertion evls1fldgencl 
|- ( ph -> ( ( O ` G ) ` A ) e. ( E fldGen ( F u. { A } ) ) )

Proof

Step Hyp Ref Expression
1 evls1fldgencl.1 
 |-  B = ( Base ` E )
2 evls1fldgencl.2 
 |-  O = ( E evalSub1 F )
3 evls1fldgencl.3 
 |-  P = ( Poly1 ` ( E |`s F ) )
4 evls1fldgencl.4 
 |-  U = ( Base ` P )
5 evls1fldgencl.5 
 |-  ( ph -> E e. Field )
6 evls1fldgencl.6 
 |-  ( ph -> F e. ( SubDRing ` E ) )
7 evls1fldgencl.7 
 |-  ( ph -> A e. B )
8 evls1fldgencl.8 
 |-  ( ph -> G e. U )
9 eqid 
 |-  ( E |`s F ) = ( E |`s F )
10 5 fldcrngd 
 |-  ( ph -> E e. CRing )
11 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
12 6 11 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
13 eqid 
 |-  ( .r ` E ) = ( .r ` E )
14 eqid 
 |-  ( .g ` ( mulGrp ` E ) ) = ( .g ` ( mulGrp ` E ) )
15 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
16 2 1 3 9 4 10 12 8 13 14 15 evls1fpws 
 |-  ( ph -> ( O ` G ) = ( x e. B |-> ( E gsum ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) x ) ) ) ) ) )
17 oveq2 
 |-  ( x = A -> ( k ( .g ` ( mulGrp ` E ) ) x ) = ( k ( .g ` ( mulGrp ` E ) ) A ) )
18 17 oveq2d 
 |-  ( x = A -> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) x ) ) = ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) )
19 18 mpteq2dv 
 |-  ( x = A -> ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) x ) ) ) = ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) )
20 19 oveq2d 
 |-  ( x = A -> ( E gsum ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) x ) ) ) ) = ( E gsum ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) ) )
21 20 adantl 
 |-  ( ( ph /\ x = A ) -> ( E gsum ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) x ) ) ) ) = ( E gsum ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) ) )
22 ovexd 
 |-  ( ph -> ( E gsum ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) ) e. _V )
23 16 21 7 22 fvmptd 
 |-  ( ph -> ( ( O ` G ) ` A ) = ( E gsum ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) ) )
24 23 ad2antrr 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( ( O ` G ) ` A ) = ( E gsum ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) ) )
25 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
26 10 crngringd 
 |-  ( ph -> E e. Ring )
27 26 ringabld 
 |-  ( ph -> E e. Abel )
28 27 ad2antrr 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> E e. Abel )
29 nn0ex 
 |-  NN0 e. _V
30 29 a1i 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> NN0 e. _V )
31 simplr 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> a e. ( SubDRing ` E ) )
32 sdrgsubrg 
 |-  ( a e. ( SubDRing ` E ) -> a e. ( SubRing ` E ) )
33 subrgsubg 
 |-  ( a e. ( SubRing ` E ) -> a e. ( SubGrp ` E ) )
34 31 32 33 3syl 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> a e. ( SubGrp ` E ) )
35 32 ad3antlr 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> a e. ( SubRing ` E ) )
36 simplr 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> ( F u. { A } ) C_ a )
37 36 unssad 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> F C_ a )
38 8 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> G e. U )
39 simpr 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> k e. NN0 )
40 eqid 
 |-  ( Base ` ( E |`s F ) ) = ( Base ` ( E |`s F ) )
41 15 4 3 40 coe1fvalcl 
 |-  ( ( G e. U /\ k e. NN0 ) -> ( ( coe1 ` G ) ` k ) e. ( Base ` ( E |`s F ) ) )
42 38 39 41 syl2anc 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> ( ( coe1 ` G ) ` k ) e. ( Base ` ( E |`s F ) ) )
43 1 sdrgss 
 |-  ( F e. ( SubDRing ` E ) -> F C_ B )
44 6 43 syl 
 |-  ( ph -> F C_ B )
45 9 1 ressbas2 
 |-  ( F C_ B -> F = ( Base ` ( E |`s F ) ) )
46 44 45 syl 
 |-  ( ph -> F = ( Base ` ( E |`s F ) ) )
47 46 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> F = ( Base ` ( E |`s F ) ) )
48 42 47 eleqtrrd 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> ( ( coe1 ` G ) ` k ) e. F )
49 37 48 sseldd 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> ( ( coe1 ` G ) ` k ) e. a )
50 simpllr 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> a e. ( SubDRing ` E ) )
51 7 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> A e. B )
52 36 unssbd 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> { A } C_ a )
53 snssg 
 |-  ( A e. B -> ( A e. a <-> { A } C_ a ) )
54 53 biimpar 
 |-  ( ( A e. B /\ { A } C_ a ) -> A e. a )
55 51 52 54 syl2anc 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> A e. a )
56 eqid 
 |-  ( mulGrp ` E ) = ( mulGrp ` E )
57 56 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` E ) )
58 56 13 mgpplusg 
 |-  ( .r ` E ) = ( +g ` ( mulGrp ` E ) )
59 fvexd 
 |-  ( a e. ( SubDRing ` E ) -> ( mulGrp ` E ) e. _V )
60 1 sdrgss 
 |-  ( a e. ( SubDRing ` E ) -> a C_ B )
61 13 subrgmcl 
 |-  ( ( a e. ( SubRing ` E ) /\ x e. a /\ y e. a ) -> ( x ( .r ` E ) y ) e. a )
62 32 61 syl3an1 
 |-  ( ( a e. ( SubDRing ` E ) /\ x e. a /\ y e. a ) -> ( x ( .r ` E ) y ) e. a )
63 eqid 
 |-  ( 0g ` ( mulGrp ` E ) ) = ( 0g ` ( mulGrp ` E ) )
64 eqid 
 |-  ( 1r ` E ) = ( 1r ` E )
65 56 64 ringidval 
 |-  ( 1r ` E ) = ( 0g ` ( mulGrp ` E ) )
66 65 eqcomi 
 |-  ( 0g ` ( mulGrp ` E ) ) = ( 1r ` E )
67 66 subrg1cl 
 |-  ( a e. ( SubRing ` E ) -> ( 0g ` ( mulGrp ` E ) ) e. a )
68 32 67 syl 
 |-  ( a e. ( SubDRing ` E ) -> ( 0g ` ( mulGrp ` E ) ) e. a )
69 57 14 58 59 60 62 63 68 mulgnn0subcl 
 |-  ( ( a e. ( SubDRing ` E ) /\ k e. NN0 /\ A e. a ) -> ( k ( .g ` ( mulGrp ` E ) ) A ) e. a )
70 50 39 55 69 syl3anc 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> ( k ( .g ` ( mulGrp ` E ) ) A ) e. a )
71 13 subrgmcl 
 |-  ( ( a e. ( SubRing ` E ) /\ ( ( coe1 ` G ) ` k ) e. a /\ ( k ( .g ` ( mulGrp ` E ) ) A ) e. a ) -> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) e. a )
72 35 49 70 71 syl3anc 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ k e. NN0 ) -> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) e. a )
73 72 fmpttd 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) : NN0 --> a )
74 30 mptexd 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) e. _V )
75 73 ffund 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> Fun ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) )
76 fvexd 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( 0g ` E ) e. _V )
77 9 subrgring 
 |-  ( F e. ( SubRing ` E ) -> ( E |`s F ) e. Ring )
78 12 77 syl 
 |-  ( ph -> ( E |`s F ) e. Ring )
79 78 ad2antrr 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( E |`s F ) e. Ring )
80 8 ad2antrr 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> G e. U )
81 eqid 
 |-  ( 0g ` ( E |`s F ) ) = ( 0g ` ( E |`s F ) )
82 3 4 81 mptcoe1fsupp 
 |-  ( ( ( E |`s F ) e. Ring /\ G e. U ) -> ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) finSupp ( 0g ` ( E |`s F ) ) )
83 79 80 82 syl2anc 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) finSupp ( 0g ` ( E |`s F ) ) )
84 ringmnd 
 |-  ( E e. Ring -> E e. Mnd )
85 26 84 syl 
 |-  ( ph -> E e. Mnd )
86 subrgsubg 
 |-  ( F e. ( SubRing ` E ) -> F e. ( SubGrp ` E ) )
87 subgsubm 
 |-  ( F e. ( SubGrp ` E ) -> F e. ( SubMnd ` E ) )
88 25 subm0cl 
 |-  ( F e. ( SubMnd ` E ) -> ( 0g ` E ) e. F )
89 12 86 87 88 4syl 
 |-  ( ph -> ( 0g ` E ) e. F )
90 9 1 25 ress0g 
 |-  ( ( E e. Mnd /\ ( 0g ` E ) e. F /\ F C_ B ) -> ( 0g ` E ) = ( 0g ` ( E |`s F ) ) )
91 85 89 44 90 syl3anc 
 |-  ( ph -> ( 0g ` E ) = ( 0g ` ( E |`s F ) ) )
92 91 ad2antrr 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( 0g ` E ) = ( 0g ` ( E |`s F ) ) )
93 83 92 breqtrrd 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) finSupp ( 0g ` E ) )
94 93 fsuppimpd 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) supp ( 0g ` E ) ) e. Fin )
95 fveq2 
 |-  ( k = i -> ( ( coe1 ` G ) ` k ) = ( ( coe1 ` G ) ` i ) )
96 oveq1 
 |-  ( k = i -> ( k ( .g ` ( mulGrp ` E ) ) A ) = ( i ( .g ` ( mulGrp ` E ) ) A ) )
97 95 96 oveq12d 
 |-  ( k = i -> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) = ( ( ( coe1 ` G ) ` i ) ( .r ` E ) ( i ( .g ` ( mulGrp ` E ) ) A ) ) )
98 97 cbvmptv 
 |-  ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) = ( i e. NN0 |-> ( ( ( coe1 ` G ) ` i ) ( .r ` E ) ( i ( .g ` ( mulGrp ` E ) ) A ) ) )
99 nfv 
 |-  F/ k ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a )
100 eqid 
 |-  ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) = ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) )
101 99 42 100 fnmptd 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) Fn NN0 )
102 simplr 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> i e. NN0 )
103 fvexd 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> ( ( coe1 ` G ) ` i ) e. _V )
104 100 95 102 103 fvmptd3 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( ( coe1 ` G ) ` i ) )
105 simpr 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) )
106 104 105 eqtr3d 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> ( ( coe1 ` G ) ` i ) = ( 0g ` E ) )
107 106 oveq1d 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> ( ( ( coe1 ` G ) ` i ) ( .r ` E ) ( i ( .g ` ( mulGrp ` E ) ) A ) ) = ( ( 0g ` E ) ( .r ` E ) ( i ( .g ` ( mulGrp ` E ) ) A ) ) )
108 26 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> E e. Ring )
109 56 ringmgp 
 |-  ( E e. Ring -> ( mulGrp ` E ) e. Mnd )
110 26 109 syl 
 |-  ( ph -> ( mulGrp ` E ) e. Mnd )
111 110 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> ( mulGrp ` E ) e. Mnd )
112 7 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> A e. B )
113 57 14 111 102 112 mulgnn0cld 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> ( i ( .g ` ( mulGrp ` E ) ) A ) e. B )
114 1 13 25 108 113 ringlzd 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> ( ( 0g ` E ) ( .r ` E ) ( i ( .g ` ( mulGrp ` E ) ) A ) ) = ( 0g ` E ) )
115 107 114 eqtrd 
 |-  ( ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 ) /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> ( ( ( coe1 ` G ) ` i ) ( .r ` E ) ( i ( .g ` ( mulGrp ` E ) ) A ) ) = ( 0g ` E ) )
116 115 3impa 
 |-  ( ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) /\ i e. NN0 /\ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) ` i ) = ( 0g ` E ) ) -> ( ( ( coe1 ` G ) ` i ) ( .r ` E ) ( i ( .g ` ( mulGrp ` E ) ) A ) ) = ( 0g ` E ) )
117 98 30 76 101 116 suppss3 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) supp ( 0g ` E ) ) C_ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) supp ( 0g ` E ) ) )
118 suppssfifsupp 
 |-  ( ( ( ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) /\ ( 0g ` E ) e. _V ) /\ ( ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) supp ( 0g ` E ) ) e. Fin /\ ( ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) supp ( 0g ` E ) ) C_ ( ( k e. NN0 |-> ( ( coe1 ` G ) ` k ) ) supp ( 0g ` E ) ) ) ) -> ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) finSupp ( 0g ` E ) )
119 74 75 76 94 117 118 syl32anc 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) finSupp ( 0g ` E ) )
120 25 28 30 34 73 119 gsumsubgcl 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( E gsum ( k e. NN0 |-> ( ( ( coe1 ` G ) ` k ) ( .r ` E ) ( k ( .g ` ( mulGrp ` E ) ) A ) ) ) ) e. a )
121 24 120 eqeltrd 
 |-  ( ( ( ph /\ a e. ( SubDRing ` E ) ) /\ ( F u. { A } ) C_ a ) -> ( ( O ` G ) ` A ) e. a )
122 121 ex 
 |-  ( ( ph /\ a e. ( SubDRing ` E ) ) -> ( ( F u. { A } ) C_ a -> ( ( O ` G ) ` A ) e. a ) )
123 122 ralrimiva 
 |-  ( ph -> A. a e. ( SubDRing ` E ) ( ( F u. { A } ) C_ a -> ( ( O ` G ) ` A ) e. a ) )
124 fvex 
 |-  ( ( O ` G ) ` A ) e. _V
125 124 elintrab 
 |-  ( ( ( O ` G ) ` A ) e. |^| { a e. ( SubDRing ` E ) | ( F u. { A } ) C_ a } <-> A. a e. ( SubDRing ` E ) ( ( F u. { A } ) C_ a -> ( ( O ` G ) ` A ) e. a ) )
126 123 125 sylibr 
 |-  ( ph -> ( ( O ` G ) ` A ) e. |^| { a e. ( SubDRing ` E ) | ( F u. { A } ) C_ a } )
127 5 flddrngd 
 |-  ( ph -> E e. DivRing )
128 7 snssd 
 |-  ( ph -> { A } C_ B )
129 44 128 unssd 
 |-  ( ph -> ( F u. { A } ) C_ B )
130 1 127 129 fldgenval 
 |-  ( ph -> ( E fldGen ( F u. { A } ) ) = |^| { a e. ( SubDRing ` E ) | ( F u. { A } ) C_ a } )
131 126 130 eleqtrrd 
 |-  ( ph -> ( ( O ` G ) ` A ) e. ( E fldGen ( F u. { A } ) ) )