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 5 13 mplringd 
 |-  ( ph -> P e. Ring )
42 ringabl 
 |-  ( P e. Ring -> P e. Abel )
43 41 42 syl 
 |-  ( ph -> P e. Abel )
44 43 adantr 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> P e. Abel )
45 ovex 
 |-  ( NN0 ^m I ) e. _V
46 45 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
47 46 a1i 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
48 14 frnd 
 |-  ( ph -> ran V C_ ( Base ` S ) )
49 4 9 aspsubrg 
 |-  ( ( S e. AssAlg /\ ran V C_ ( Base ` S ) ) -> ( A ` ran V ) e. ( SubRing ` S ) )
50 7 48 49 syl2anc 
 |-  ( ph -> ( A ` ran V ) e. ( SubRing ` S ) )
51 1 2 8 mplval2 
 |-  P = ( S |`s ( Base ` P ) )
52 51 subsubrg 
 |-  ( ( Base ` P ) e. ( SubRing ` S ) -> ( ( A ` ran V ) e. ( SubRing ` P ) <-> ( ( A ` ran V ) e. ( SubRing ` S ) /\ ( A ` ran V ) C_ ( Base ` P ) ) ) )
53 26 52 syl 
 |-  ( ph -> ( ( A ` ran V ) e. ( SubRing ` P ) <-> ( ( A ` ran V ) e. ( SubRing ` S ) /\ ( A ` ran V ) C_ ( Base ` P ) ) ) )
54 50 31 53 mpbir2and 
 |-  ( ph -> ( A ` ran V ) e. ( SubRing ` P ) )
55 subrgsubg 
 |-  ( ( A ` ran V ) e. ( SubRing ` P ) -> ( A ` ran V ) e. ( SubGrp ` P ) )
56 54 55 syl 
 |-  ( ph -> ( A ` ran V ) e. ( SubGrp ` P ) )
57 56 adantr 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( A ` ran V ) e. ( SubGrp ` P ) )
58 1 5 13 mpllmodd 
 |-  ( ph -> P e. LMod )
59 58 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> P e. LMod )
60 4 9 28 asplss 
 |-  ( ( S e. AssAlg /\ ran V C_ ( Base ` S ) ) -> ( A ` ran V ) e. ( LSubSp ` S ) )
61 7 48 60 syl2anc 
 |-  ( ph -> ( A ` ran V ) e. ( LSubSp ` S ) )
62 2 5 13 psrlmod 
 |-  ( ph -> S e. LMod )
63 eqid 
 |-  ( LSubSp ` P ) = ( LSubSp ` P )
64 51 28 63 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 ) ) ) )
65 62 27 64 syl2anc 
 |-  ( ph -> ( ( A ` ran V ) e. ( LSubSp ` P ) <-> ( ( A ` ran V ) e. ( LSubSp ` S ) /\ ( A ` ran V ) C_ ( Base ` P ) ) ) )
66 61 31 65 mpbir2and 
 |-  ( ph -> ( A ` ran V ) e. ( LSubSp ` P ) )
67 66 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( A ` ran V ) e. ( LSubSp ` P ) )
68 eqid 
 |-  ( Base ` R ) = ( Base ` R )
69 1 68 8 32 38 mplelf 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> x : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
70 69 ffvelcdmda 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( x ` k ) e. ( Base ` R ) )
71 1 35 37 mplsca 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> R = ( Scalar ` P ) )
72 71 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> R = ( Scalar ` P ) )
73 72 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
74 70 73 eleqtrd 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( x ` k ) e. ( Base ` ( Scalar ` P ) ) )
75 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> I e. W )
76 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
77 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
78 6 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> R e. CRing )
79 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 } )
80 1 32 33 34 75 76 77 3 78 79 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 ) ) ) ) )
81 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
82 76 81 ringidval 
 |-  ( 1r ` P ) = ( 0g ` ( mulGrp ` P ) )
83 1 mplcrng 
 |-  ( ( I e. W /\ R e. CRing ) -> P e. CRing )
84 5 6 83 syl2anc 
 |-  ( ph -> P e. CRing )
85 76 crngmgp 
 |-  ( P e. CRing -> ( mulGrp ` P ) e. CMnd )
86 84 85 syl 
 |-  ( ph -> ( mulGrp ` P ) e. CMnd )
87 86 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( mulGrp ` P ) e. CMnd )
88 54 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( A ` ran V ) e. ( SubRing ` P ) )
89 76 subrgsubm 
 |-  ( ( A ` ran V ) e. ( SubRing ` P ) -> ( A ` ran V ) e. ( SubMnd ` ( mulGrp ` P ) ) )
90 88 89 syl 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( A ` ran V ) e. ( SubMnd ` ( mulGrp ` P ) ) )
91 simplll 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. I ) -> ph )
92 32 psrbag 
 |-  ( I e. W -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } <-> ( k : I --> NN0 /\ ( `' k " NN ) e. Fin ) ) )
93 35 92 syl 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } <-> ( k : I --> NN0 /\ ( `' k " NN ) e. Fin ) ) )
94 93 biimpa 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( k : I --> NN0 /\ ( `' k " NN ) e. Fin ) )
95 94 simpld 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> k : I --> NN0 )
96 95 ffvelcdmda 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ z e. I ) -> ( k ` z ) e. NN0 )
97 4 9 aspssid 
 |-  ( ( S e. AssAlg /\ ran V C_ ( Base ` S ) ) -> ran V C_ ( A ` ran V ) )
98 7 48 97 syl2anc 
 |-  ( ph -> ran V C_ ( A ` ran V ) )
99 98 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 ) )
100 15 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> V Fn I )
101 fnfvelrn 
 |-  ( ( V Fn I /\ z e. I ) -> ( V ` z ) e. ran V )
102 100 101 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 )
103 99 102 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 ) )
104 76 8 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
105 eqid 
 |-  ( .r ` P ) = ( .r ` P )
106 76 105 mgpplusg 
 |-  ( .r ` P ) = ( +g ` ( mulGrp ` P ) )
107 105 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 ) )
108 54 107 syl3an1 
 |-  ( ( ph /\ u e. ( A ` ran V ) /\ v e. ( A ` ran V ) ) -> ( u ( .r ` P ) v ) e. ( A ` ran V ) )
109 81 subrg1cl 
 |-  ( ( A ` ran V ) e. ( SubRing ` P ) -> ( 1r ` P ) e. ( A ` ran V ) )
110 54 109 syl 
 |-  ( ph -> ( 1r ` P ) e. ( A ` ran V ) )
111 104 77 106 86 31 108 82 110 mulgnn0subcl 
 |-  ( ( ph /\ ( k ` z ) e. NN0 /\ ( V ` z ) e. ( A ` ran V ) ) -> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) e. ( A ` ran V ) )
112 91 96 103 111 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 ) )
113 112 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 ) )
114 5 mptexd 
 |-  ( ph -> ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) ) e. _V )
115 114 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 )
116 funmpt 
 |-  Fun ( z e. I |-> ( ( k ` z ) ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) )
117 116 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 ) ) ) )
118 fvexd 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( 1r ` P ) e. _V )
119 94 simprd 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( `' k " NN ) e. Fin )
120 elrabi 
 |-  ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } -> k e. ( NN0 ^m I ) )
121 elmapi 
 |-  ( k e. ( NN0 ^m I ) -> k : I --> NN0 )
122 121 adantl 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) -> k : I --> NN0 )
123 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) -> I e. W )
124 fcdmnn0supp 
 |-  ( ( I e. W /\ k : I --> NN0 ) -> ( k supp 0 ) = ( `' k " NN ) )
125 123 122 124 syl2anc 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) -> ( k supp 0 ) = ( `' k " NN ) )
126 eqimss 
 |-  ( ( k supp 0 ) = ( `' k " NN ) -> ( k supp 0 ) C_ ( `' k " NN ) )
127 125 126 syl 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) -> ( k supp 0 ) C_ ( `' k " NN ) )
128 c0ex 
 |-  0 e. _V
129 128 a1i 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) -> 0 e. _V )
130 122 127 123 129 suppssr 
 |-  ( ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. ( NN0 ^m I ) ) /\ z e. ( I \ ( `' k " NN ) ) ) -> ( k ` z ) = 0 )
131 120 130 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 )
132 131 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 ) ) )
133 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 )
134 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 )
135 eldifi 
 |-  ( z e. ( I \ ( `' k " NN ) ) -> z e. I )
136 135 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 )
137 1 3 8 133 134 136 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 ) )
138 104 82 77 mulg0 
 |-  ( ( V ` z ) e. ( Base ` P ) -> ( 0 ( .g ` ( mulGrp ` P ) ) ( V ` z ) ) = ( 1r ` P ) )
139 137 138 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 ) )
140 132 139 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 ) )
141 140 75 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 ) )
142 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 ) )
143 115 117 118 119 141 142 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 ) )
144 82 87 75 90 113 143 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 ) )
145 80 144 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 ) )
146 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
147 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
148 146 36 147 63 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 ) )
149 59 67 74 145 148 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 ) )
150 149 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 ) )
151 45 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
152 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 ) ) ) ) )
153 fvex 
 |-  ( 0g ` P ) e. _V
154 151 152 153 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 )
155 154 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 ) )
156 1 2 9 33 8 mplelbas 
 |-  ( x e. ( Base ` P ) <-> ( x e. ( Base ` S ) /\ x finSupp ( 0g ` R ) ) )
157 156 simprbi 
 |-  ( x e. ( Base ` P ) -> x finSupp ( 0g ` R ) )
158 157 adantl 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> x finSupp ( 0g ` R ) )
159 158 fsuppimpd 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( x supp ( 0g ` R ) ) e. Fin )
160 ssidd 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( x supp ( 0g ` R ) ) C_ ( x supp ( 0g ` R ) ) )
161 fvexd 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( 0g ` R ) e. _V )
162 69 160 47 161 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 ) )
163 71 fveq2d 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
164 163 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 ) ) )
165 162 164 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 ) ) )
166 165 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 ) ) ) ) )
167 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 } )
168 13 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` P ) ) /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> R e. Ring )
169 1 8 33 34 32 75 168 79 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 ) )
170 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
171 8 146 36 170 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 ) )
172 59 169 171 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 ) )
173 167 172 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 ) )
174 166 173 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 ) )
175 174 47 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 ) ) )
176 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 ) )
177 155 159 175 176 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 ) )
178 40 44 47 57 150 177 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 ) )
179 39 178 eqeltrd 
 |-  ( ( ph /\ x e. ( Base ` P ) ) -> x e. ( A ` ran V ) )
180 31 179 eqelssd 
 |-  ( ph -> ( A ` ran V ) = ( Base ` P ) )