Metamath Proof Explorer

Theorem mplbas2

Description: An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses mplbas2.p 
|- P = ( I mPoly R )
mplbas2.s 
|- S = ( I mPwSer R )
mplbas2.v 
|- V = ( I mVar R )
mplbas2.a 
|- A = ( AlgSpan ` S )
mplbas2.i 
|- ( ph -> I e. W )
mplbas2.r 
|- ( ph -> R e. CRing )
Assertion mplbas2 
|- ( ph -> ( A ` ran V ) = ( Base ` P ) )

Proof

Step Hyp Ref Expression
1 mplbas2.p 
 |-  P = ( I mPoly R )
2 mplbas2.s 
 |-  S = ( I mPwSer R )
3 mplbas2.v 
 |-  V = ( I mVar R )
4 mplbas2.a 
 |-  A = ( AlgSpan ` S )
5 mplbas2.i 
 |-  ( ph -> I e. W )
6 mplbas2.r 
 |-  ( ph -> R e. CRing )
7 2 5 6 psrassa 
 |-  ( ph -> S e. AssAlg )
8 eqid 
 |-  ( Base ` P ) = ( Base ` P )
9 eqid 
 |-  ( Base ` S ) = ( Base ` S )
10 1 2 8 9 mplbasss 
 |-  ( Base ` P ) C_ ( Base ` S )
11 10 a1i 
 |-  ( ph -> ( Base ` P ) C_ ( Base ` S ) )
12 crngring 
 |-  ( R e. CRing -> R e. Ring )
13 6 12 syl 
 |-  ( ph -> R e. Ring )
14 2 3 9 5 13 mvrf 
 |-  ( ph -> V : I --> ( Base ` S ) )
15 14 ffnd 
 |-  ( ph -> V Fn I )
16 5 adantr 
 |-  ( ( ph /\ x e. I ) -> I e. W )
17 13 adantr 
 |-  ( ( ph /\ x e. I ) -> R e. Ring )
18 simpr 
 |-  ( ( ph /\ x e. I ) -> x e. I )
19 1 3 8 16 17 18 mvrcl 
 |-  ( ( ph /\ x e. I ) -> ( V ` x ) e. ( Base ` P ) )
20 19 ralrimiva 
 |-  ( ph -> A. x e. I ( V ` x ) e. ( Base ` P ) )
21 ffnfv 
 |-  ( V : I --> ( Base ` P ) <-> ( V Fn I /\ A. x e. I ( V ` x ) e. ( Base ` P ) ) )
22 15 20 21 sylanbrc 
 |-  ( ph -> V : I --> ( Base ` P ) )
23 22 frnd 
 |-  ( ph -> ran V C_ ( Base ` P ) )
24 4 9 aspss 
 |-  ( ( S e. AssAlg /\ ( Base ` P ) C_ ( Base ` S ) /\ ran V C_ ( Base ` P ) ) -> ( A ` ran V ) C_ ( A ` ( Base ` P ) ) )
25 7 11 23 24 syl3anc 
 |-  ( ph -> ( A ` ran V ) C_ ( A ` ( Base ` P ) ) )
26 2 1 8 5 13 mplsubrg 
 |-  ( ph -> ( Base ` P ) e. ( SubRing ` S ) )
27 2 1 8 5 13 mpllss 
 |-  ( ph -> ( Base ` P ) e. ( LSubSp ` S ) )
28 eqid 
 |-  ( LSubSp ` S ) = ( LSubSp ` S )
29 4 9 28 aspid 
 |-  ( ( S e. AssAlg /\ ( Base ` P ) e. ( SubRing ` S ) /\ ( Base ` P ) e. ( LSubSp ` S ) ) -> ( A ` ( Base ` P ) ) = ( Base ` P ) )
30 7 26 27 29 syl3anc 
 |-  ( ph -> ( A ` ( Base ` P ) ) = ( Base ` P ) )
31 25 30 sseqtrd 
 |-  ( ph -> ( A ` ran V ) C_ ( Base ` P ) )
32 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
33 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
34 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
35 5 adantr 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> I e. W )
36 eqid 
 |-  ( .s ` P ) = ( .s ` P )
37 13 adantr 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> R e. Ring )
38 simpr 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> x e. ( Base ` P ) )
39 1 32 33 34 35 8 36 37 38 mplcoe1 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> x = ( P gsum ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) ) )
40 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
41 1 mplring 
 |-  ( ( I e. W /\ R e. Ring ) -> P e. Ring )
42 5 13 41 syl2anc 
 |-  ( ph -> P e. Ring )
43 ringabl 
 |-  ( P e. Ring -> P e. Abel )
44 42 43 syl 
 |-  ( ph -> P e. Abel )
45 44 adantr 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> P e. Abel )
46 ovex 
 |-  ( NN0 ^m I ) e. _V
47 46 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
48 47 a1i 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
49 14 frnd 
 |-  ( ph -> ran V C_ ( Base ` S ) )
50 4 9 aspsubrg 
 |-  ( ( S e. AssAlg /\ ran V C_ ( Base ` S ) ) -> ( A ` ran V ) e. ( SubRing ` S ) )
51 7 49 50 syl2anc 
 |-  ( ph -> ( A ` ran V ) e. ( SubRing ` S ) )
52 1 2 8 mplval2 
 |-  P = ( S |`s ( Base ` P ) )
53 52 subsubrg 
 |-  ( ( Base ` P ) e. ( SubRing ` S ) -> ( ( A ` ran V ) e. ( SubRing ` P ) <-> ( ( A ` ran V ) e. ( SubRing ` S ) /\ ( A ` ran V ) C_ ( Base ` P ) ) ) )
54 26 53 syl 
 |-  ( ph -> ( ( A ` ran V ) e. ( SubRing ` P ) <-> ( ( A ` ran V ) e. ( SubRing ` S ) /\ ( A ` ran V ) C_ ( Base ` P ) ) ) )
55 51 31 54 mpbir2and 
 |-  ( ph -> ( A ` ran V ) e. ( SubRing ` P ) )
56 subrgsubg 
 |-  ( ( A ` ran V ) e. ( SubRing ` P ) -> ( A ` ran V ) e. ( SubGrp ` P ) )
57 55 56 syl 
 |-  ( ph -> ( A ` ran V ) e. ( SubGrp ` P ) )
58 57 adantr 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( A ` ran V ) e. ( SubGrp ` P ) )
59 1 mpllmod 
 |-  ( ( I e. W /\ R e. Ring ) -> P e. LMod )
60 5 13 59 syl2anc 
 |-  ( ph -> P e. LMod )
61 60 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> P e. LMod )
62 4 9 28 asplss 
 |-  ( ( S e. AssAlg /\ ran V C_ ( Base ` S ) ) -> ( A ` ran V ) e. ( LSubSp ` S ) )
63 7 49 62 syl2anc 
 |-  ( ph -> ( A ` ran V ) e. ( LSubSp ` S ) )
64 2 5 13 psrlmod 
 |-  ( ph -> S e. LMod )
65 eqid 
 |-  ( LSubSp ` P ) = ( LSubSp ` P )
66 52 28 65 lsslss 
 |-  ( ( S e. LMod /\ ( Base ` P ) e. ( LSubSp ` S ) ) -> ( ( A ` ran V ) e. ( LSubSp ` P ) <-> ( ( A ` ran V ) e. ( LSubSp ` S ) /\ ( A ` ran V ) C_ ( Base ` P ) ) ) )
67 64 27 66 syl2anc 
 |-  ( ph -> ( ( A ` ran V ) e. ( LSubSp ` P ) <-> ( ( A ` ran V ) e. ( LSubSp ` S ) /\ ( A ` ran V ) C_ ( Base ` P ) ) ) )
68 63 31 67 mpbir2and 
 |-  ( ph -> ( A ` ran V ) e. ( LSubSp ` P ) )
69 68 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( A ` ran V ) e. ( LSubSp ` P ) )
70 eqid 
 |-  ( Base ` R ) = ( Base ` R )
71 1 70 8 32 38 mplelf 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> x : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
72 71 ffvelrnda 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( x ` k ) e. ( Base ` R ) )
73 1 35 37 mplsca 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> R = ( Scalar ` P ) )
74 73 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> R = ( Scalar ` P ) )
75 74 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
76 72 75 eleqtrd 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( x ` k ) e. ( Base ` ( Scalar ` P ) ) )
77 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> I e. W )
78 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
79 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
80 6 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> R e. CRing )
81 simpr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
82 1 32 33 34 77 78 79 3 80 81 mplcoe2 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) = ( ( mulGrp ` P ) gsum ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) ) )
83 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
84 78 83 ringidval 
 |-  ( 1r ` P ) = ( 0g ` ( mulGrp ` P ) )
85 1 mplcrng 
 |-  ( ( I e. W /\ R e. CRing ) -> P e. CRing )
86 5 6 85 syl2anc 
 |-  ( ph -> P e. CRing )
87 78 crngmgp 
 |-  ( P e. CRing -> ( mulGrp ` P ) e. CMnd )
88 86 87 syl 
 |-  ( ph -> ( mulGrp ` P ) e. CMnd )
89 88 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( mulGrp ` P ) e. CMnd )
90 55 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( A ` ran V ) e. ( SubRing ` P ) )
91 78 subrgsubm 
 |-  ( ( A ` ran V ) e. ( SubRing ` P ) -> ( A ` ran V ) e. ( SubMnd ` ( mulGrp ` P ) ) )
92 90 91 syl 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( A ` ran V ) e. ( SubMnd ` ( mulGrp ` P ) ) )
93 simplll 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. I ) -> ph )
94 32 psrbag 
 |-  ( I e. W -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } <-> ( k : I --> NN0 /\ ( `' k " NN ) e. Fin ) ) )
95 35 94 syl 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } <-> ( k : I --> NN0 /\ ( `' k " NN ) e. Fin ) ) )
96 95 biimpa 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( k : I --> NN0 /\ ( `' k " NN ) e. Fin ) )
97 96 simpld 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> k : I --> NN0 )
98 97 ffvelrnda 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. I ) -> ( k ` z ) e. NN0 )
99 4 9 aspssid 
 |-  ( ( S e. AssAlg /\ ran V C_ ( Base ` S ) ) -> ran V C_ ( A ` ran V ) )
100 7 49 99 syl2anc 
 |-  ( ph -> ran V C_ ( A ` ran V ) )
101 100 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. I ) -> ran V C_ ( A ` ran V ) )
102 15 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> V Fn I )
103 fnfvelrn 
 |-  ( ( V Fn I /\ z e. I ) -> ( V ` z ) e. ran V )
104 102 103 sylan 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. I ) -> ( V ` z ) e. ran V )
105 101 104 sseldd 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. I ) -> ( V ` z ) e. ( A ` ran V ) )
106 78 8 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
107 eqid 
 |-  ( .r ` P ) = ( .r ` P )
108 78 107 mgpplusg 
 |-  ( .r ` P ) = ( +g ` ( mulGrp ` P ) )
109 107 subrgmcl 
 |-  ( ( ( A ` ran V ) e. ( SubRing ` P ) /\ u e. ( A ` ran V ) /\ v e. ( A ` ran V ) ) -> ( u ( .r ` P ) v ) e. ( A ` ran V ) )
110 55 109 syl3an1 
 |-  ( ( ph /\ u e. ( A ` ran V ) /\ v e. ( A ` ran V ) ) -> ( u ( .r ` P ) v ) e. ( A ` ran V ) )
111 83 subrg1cl 
 |-  ( ( A ` ran V ) e. ( SubRing ` P ) -> ( 1r ` P ) e. ( A ` ran V ) )
112 55 111 syl 
 |-  ( ph -> ( 1r ` P ) e. ( A ` ran V ) )
113 106 79 108 88 31 110 84 112 mulgnn0subcl 
 |-  ( ( ph /\ ( k ` z ) e. NN0 /\ ( V ` z ) e. ( A ` ran V ) ) -> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) e. ( A ` ran V ) )
114 93 98 105 113 syl3anc 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. I ) -> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) e. ( A ` ran V ) )
115 114 fmpttd 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) : I --> ( A ` ran V ) )
116 5 mptexd 
 |-  ( ph -> ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) e. _V )
117 116 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) e. _V )
118 funmpt 
 |-  Fun ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) )
119 118 a1i 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> Fun ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) )
120 fvexd 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( 1r ` P ) e. _V )
121 96 simprd 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( `' k " NN ) e. Fin )
122 elrabi 
 |-  ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } -> k e. ( NN0 ^m I ) )
123 elmapi 
 |-  ( k e. ( NN0 ^m I ) -> k : I --> NN0 )
124 123 adantl 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) -> k : I --> NN0 )
125 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) -> I e. W )
126 frnnn0supp 
 |-  ( ( I e. W /\ k : I --> NN0 ) -> ( k supp 0 ) = ( `' k " NN ) )
127 125 124 126 syl2anc 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) -> ( k supp 0 ) = ( `' k " NN ) )
128 eqimss 
 |-  ( ( k supp 0 ) = ( `' k " NN ) -> ( k supp 0 ) C_ ( `' k " NN ) )
129 127 128 syl 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) -> ( k supp 0 ) C_ ( `' k " NN ) )
130 c0ex 
 |-  0 e. _V
131 130 a1i 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) -> 0 e. _V )
132 124 129 125 131 suppssr 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) /\ z e. ( I \ ( `' k " NN ) ) ) -> ( k ` z ) = 0 )
133 122 132 sylanl2 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. ( I \ ( `' k " NN ) ) ) -> ( k ` z ) = 0 )
134 133 oveq1d 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. ( I \ ( `' k " NN ) ) ) -> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) = ( 0 ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) )
135 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. ( I \ ( `' k " NN ) ) ) -> I e. W )
136 13 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. ( I \ ( `' k " NN ) ) ) -> R e. Ring )
137 eldifi 
 |-  ( z e. ( I \ ( `' k " NN ) ) -> z e. I )
138 137 adantl 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. ( I \ ( `' k " NN ) ) ) -> z e. I )
139 1 3 8 135 136 138 mvrcl 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. ( I \ ( `' k " NN ) ) ) -> ( V ` z ) e. ( Base ` P ) )
140 106 84 79 mulg0 
 |-  ( ( V ` z ) e. ( Base ` P ) -> ( 0 ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) = ( 1r ` P ) )
141 139 140 syl 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. ( I \ ( `' k " NN ) ) ) -> ( 0 ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) = ( 1r ` P ) )
142 134 141 eqtrd 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. ( I \ ( `' k " NN ) ) ) -> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) = ( 1r ` P ) )
143 142 77 suppss2 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) supp ( 1r ` P ) ) C_ ( `' k " NN ) )
144 suppssfifsupp 
 |-  ( ( ( ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) e. _V /\ Fun ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) /\ ( 1r ` P ) e. _V ) /\ ( ( `' k " NN ) e. Fin /\ ( ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) supp ( 1r ` P ) ) C_ ( `' k " NN ) ) ) -> ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) finSupp ( 1r ` P ) )
145 117 119 120 121 143 144 syl32anc 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) finSupp ( 1r ` P ) )
146 84 89 77 92 115 145 gsumsubmcl 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( ( mulGrp ` P ) gsum ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) ) e. ( A ` ran V ) )
147 82 146 eqeltrd 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( A ` ran V ) )
148 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
149 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
150 148 36 149 65 lssvscl 
 |-  ( ( ( P e. LMod /\ ( A ` ran V ) e. ( LSubSp ` P ) ) /\ ( ( x ` k ) e. ( Base ` ( Scalar ` P ) ) /\ ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( A ` ran V ) ) ) -> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) e. ( A ` ran V ) )
151 61 69 76 147 150 syl22anc 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) e. ( A ` ran V ) )
152 151 fmpttd 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( A ` ran V ) )
153 46 mptrabex 
 |-  ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) e. _V
154 funmpt 
 |-  Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
155 fvex 
 |-  ( 0g ` P ) e. _V
156 153 154 155 3pm3.2i 
 |-  ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) e. _V /\ Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) /\ ( 0g ` P ) e. _V )
157 156 a1i 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) e. _V /\ Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) /\ ( 0g ` P ) e. _V ) )
158 1 2 9 33 8 mplelbas 
 |-  ( x e. ( Base ` P ) <-> ( x e. ( Base ` S ) /\ x finSupp ( 0g ` R ) ) )
159 158 simprbi 
 |-  ( x e. ( Base ` P ) -> x finSupp ( 0g ` R ) )
160 159 adantl 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> x finSupp ( 0g ` R ) )
161 160 fsuppimpd 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( x supp ( 0g ` R ) ) e. Fin )
162 ssidd 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( x supp ( 0g ` R ) ) C_ ( x supp ( 0g ` R ) ) )
163 fvexd 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( 0g ` R ) e. _V )
164 71 162 48 163 suppssr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ ( x supp ( 0g ` R ) ) ) ) -> ( x ` k ) = ( 0g ` R ) )
165 73 fveq2d 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
166 165 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ ( x supp ( 0g ` R ) ) ) ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
167 164 166 eqtrd 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ ( x supp ( 0g ` R ) ) ) ) -> ( x ` k ) = ( 0g ` ( Scalar ` P ) ) )
168 167 oveq1d 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ ( x supp ( 0g ` R ) ) ) ) -> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
169 eldifi 
 |-  ( k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ ( x supp ( 0g ` R ) ) ) -> k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
170 13 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> R e. Ring )
171 1 8 33 34 32 77 170 81 mplmon 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( Base ` P ) )
172 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
173 8 148 36 172 40 lmod0vs 
 |-  ( ( P e. LMod /\ ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( Base ` P ) ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( 0g ` P ) )
174 61 171 173 syl2anc 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( 0g ` P ) )
175 169 174 sylan2 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ ( x supp ( 0g ` R ) ) ) ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( 0g ` P ) )
176 168 175 eqtrd 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ ( x supp ( 0g ` R ) ) ) ) -> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( 0g ` P ) )
177 176 48 suppss2 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) supp ( 0g ` P ) ) C_ ( x supp ( 0g ` R ) ) )
178 suppssfifsupp 
 |-  ( ( ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) e. _V /\ Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) /\ ( 0g ` P ) e. _V ) /\ ( ( x supp ( 0g ` R ) ) e. Fin /\ ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) supp ( 0g ` P ) ) C_ ( x supp ( 0g ` R ) ) ) ) -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) finSupp ( 0g ` P ) )
179 157 161 177 178 syl12anc 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) finSupp ( 0g ` P ) )
180 40 45 48 58 152 179 gsumsubgcl 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( P gsum ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( ( x ` k ) ( .s ` P ) ( y e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( y = k , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) ) e. ( A ` ran V ) )
181 39 180 eqeltrd 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> x e. ( A ` ran V ) )
182 31 181 eqelssd 
 |-  ( ph -> ( A ` ran V ) = ( Base ` P ) )