Metamath Proof Explorer

Theorem ply1degltdimlem

Description: Lemma for ply1degltdim . (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses ply1degltdim.p 
|- P = ( Poly1 ` R )
ply1degltdim.d 
|- D = ( deg1 ` R )
ply1degltdim.s 
|- S = ( `' D " ( -oo [,) N ) )
ply1degltdim.n 
|- ( ph -> N e. NN0 )
ply1degltdim.r 
|- ( ph -> R e. DivRing )
ply1degltdim.e 
|- E = ( P |`s S )
ply1degltdimlem.f 
|- F = ( n e. ( 0 ..^ N ) |-> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
Assertion ply1degltdimlem 
|- ( ph -> ran F e. ( LBasis ` E ) )

Proof

Step Hyp Ref Expression
1 ply1degltdim.p 
 |-  P = ( Poly1 ` R )
2 ply1degltdim.d 
 |-  D = ( deg1 ` R )
3 ply1degltdim.s 
 |-  S = ( `' D " ( -oo [,) N ) )
4 ply1degltdim.n 
 |-  ( ph -> N e. NN0 )
5 ply1degltdim.r 
 |-  ( ph -> R e. DivRing )
6 ply1degltdim.e 
 |-  E = ( P |`s S )
7 ply1degltdimlem.f 
 |-  F = ( n e. ( 0 ..^ N ) |-> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 4 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> N e. NN0 )
10 5 drngringd 
 |-  ( ph -> R e. Ring )
11 10 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> R e. Ring )
12 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
13 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
14 elmapi 
 |-  ( a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) -> a : ( 0 ..^ N ) --> ( Base ` ( Scalar ` P ) ) )
15 14 adantl 
 |-  ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) -> a : ( 0 ..^ N ) --> ( Base ` ( Scalar ` P ) ) )
16 1 ply1sca 
 |-  ( R e. DivRing -> R = ( Scalar ` P ) )
17 5 16 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
18 17 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
19 18 adantr 
 |-  ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
20 19 feq3d 
 |-  ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) -> ( a : ( 0 ..^ N ) --> ( Base ` R ) <-> a : ( 0 ..^ N ) --> ( Base ` ( Scalar ` P ) ) ) )
21 15 20 mpbird 
 |-  ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) -> a : ( 0 ..^ N ) --> ( Base ` R ) )
22 21 ad2antrr 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a : ( 0 ..^ N ) --> ( Base ` R ) )
23 simpr 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) )
24 ovexd 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( 0 ..^ N ) e. _V )
25 1 5 ply1lvec 
 |-  ( ph -> P e. LVec )
26 25 lveclmodd 
 |-  ( ph -> P e. LMod )
27 1 2 3 4 10 ply1degltlss 
 |-  ( ph -> S e. ( LSubSp ` P ) )
28 eqid 
 |-  ( LSubSp ` P ) = ( LSubSp ` P )
29 28 lsssubg 
 |-  ( ( P e. LMod /\ S e. ( LSubSp ` P ) ) -> S e. ( SubGrp ` P ) )
30 26 27 29 syl2anc 
 |-  ( ph -> S e. ( SubGrp ` P ) )
31 subgsubm 
 |-  ( S e. ( SubGrp ` P ) -> S e. ( SubMnd ` P ) )
32 30 31 syl 
 |-  ( ph -> S e. ( SubMnd ` P ) )
33 32 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> S e. ( SubMnd ` P ) )
34 eqid 
 |-  ( Base ` P ) = ( Base ` P )
35 2 1 34 deg1xrf 
 |-  D : ( Base ` P ) --> RR*
36 ffn 
 |-  ( D : ( Base ` P ) --> RR* -> D Fn ( Base ` P ) )
37 35 36 mp1i 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> D Fn ( Base ` P ) )
38 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
39 eqid 
 |-  ( .s ` P ) = ( .s ` P )
40 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
41 26 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> P e. LMod )
42 simplr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> k e. ( Base ` ( Scalar ` P ) ) )
43 34 28 lssss 
 |-  ( S e. ( LSubSp ` P ) -> S C_ ( Base ` P ) )
44 27 43 syl 
 |-  ( ph -> S C_ ( Base ` P ) )
45 6 34 ressbas2 
 |-  ( S C_ ( Base ` P ) -> S = ( Base ` E ) )
46 44 45 syl 
 |-  ( ph -> S = ( Base ` E ) )
47 46 44 eqsstrrd 
 |-  ( ph -> ( Base ` E ) C_ ( Base ` P ) )
48 47 sselda 
 |-  ( ( ph /\ x e. ( Base ` E ) ) -> x e. ( Base ` P ) )
49 48 adantlr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> x e. ( Base ` P ) )
50 34 38 39 40 41 42 49 lmodvscld 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( k ( .s ` P ) x ) e. ( Base ` P ) )
51 mnfxr 
 |-  -oo e. RR*
52 51 a1i 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> -oo e. RR* )
53 4 nn0red 
 |-  ( ph -> N e. RR )
54 53 rexrd 
 |-  ( ph -> N e. RR* )
55 54 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> N e. RR* )
56 35 a1i 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> D : ( Base ` P ) --> RR* )
57 56 50 ffvelcdmd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` ( k ( .s ` P ) x ) ) e. RR* )
58 57 mnfled 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> -oo <_ ( D ` ( k ( .s ` P ) x ) ) )
59 56 49 ffvelcdmd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` x ) e. RR* )
60 10 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> R e. Ring )
61 18 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
62 42 61 eleqtrrd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> k e. ( Base ` R ) )
63 1 2 60 34 8 39 62 49 deg1vscale 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` ( k ( .s ` P ) x ) ) <_ ( D ` x ) )
64 simpll 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ph )
65 simpr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> x e. ( Base ` E ) )
66 46 ad2antrr 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> S = ( Base ` E ) )
67 65 66 eleqtrrd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> x e. S )
68 51 a1i 
 |-  ( ( ph /\ x e. S ) -> -oo e. RR* )
69 54 adantr 
 |-  ( ( ph /\ x e. S ) -> N e. RR* )
70 35 36 mp1i 
 |-  ( ( ph /\ x e. S ) -> D Fn ( Base ` P ) )
71 simpr 
 |-  ( ( ph /\ x e. S ) -> x e. S )
72 71 3 eleqtrdi 
 |-  ( ( ph /\ x e. S ) -> x e. ( `' D " ( -oo [,) N ) ) )
73 elpreima 
 |-  ( D Fn ( Base ` P ) -> ( x e. ( `' D " ( -oo [,) N ) ) <-> ( x e. ( Base ` P ) /\ ( D ` x ) e. ( -oo [,) N ) ) ) )
74 73 simplbda 
 |-  ( ( D Fn ( Base ` P ) /\ x e. ( `' D " ( -oo [,) N ) ) ) -> ( D ` x ) e. ( -oo [,) N ) )
75 70 72 74 syl2anc 
 |-  ( ( ph /\ x e. S ) -> ( D ` x ) e. ( -oo [,) N ) )
76 elico1 
 |-  ( ( -oo e. RR* /\ N e. RR* ) -> ( ( D ` x ) e. ( -oo [,) N ) <-> ( ( D ` x ) e. RR* /\ -oo <_ ( D ` x ) /\ ( D ` x ) < N ) ) )
77 76 biimpa 
 |-  ( ( ( -oo e. RR* /\ N e. RR* ) /\ ( D ` x ) e. ( -oo [,) N ) ) -> ( ( D ` x ) e. RR* /\ -oo <_ ( D ` x ) /\ ( D ` x ) < N ) )
78 77 simp3d 
 |-  ( ( ( -oo e. RR* /\ N e. RR* ) /\ ( D ` x ) e. ( -oo [,) N ) ) -> ( D ` x ) < N )
79 68 69 75 78 syl21anc 
 |-  ( ( ph /\ x e. S ) -> ( D ` x ) < N )
80 64 67 79 syl2anc 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` x ) < N )
81 57 59 55 63 80 xrlelttrd 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` ( k ( .s ` P ) x ) ) < N )
82 52 55 57 58 81 elicod 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( D ` ( k ( .s ` P ) x ) ) e. ( -oo [,) N ) )
83 37 50 82 elpreimad 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( k ( .s ` P ) x ) e. ( `' D " ( -oo [,) N ) ) )
84 83 3 eleqtrrdi 
 |-  ( ( ( ph /\ k e. ( Base ` ( Scalar ` P ) ) ) /\ x e. ( Base ` E ) ) -> ( k ( .s ` P ) x ) e. S )
85 84 anasss 
 |-  ( ( ph /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ x e. ( Base ` E ) ) ) -> ( k ( .s ` P ) x ) e. S )
86 85 ad5ant15 
 |-  ( ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) /\ ( k e. ( Base ` ( Scalar ` P ) ) /\ x e. ( Base ` E ) ) ) -> ( k ( .s ` P ) x ) e. S )
87 15 ad2antrr 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a : ( 0 ..^ N ) --> ( Base ` ( Scalar ` P ) ) )
88 35 36 mp1i 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> D Fn ( Base ` P ) )
89 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
90 89 34 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
91 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
92 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
93 89 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
94 10 92 93 3syl 
 |-  ( ph -> ( mulGrp ` P ) e. Mnd )
95 94 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( mulGrp ` P ) e. Mnd )
96 elfzonn0 
 |-  ( n e. ( 0 ..^ N ) -> n e. NN0 )
97 96 adantl 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> n e. NN0 )
98 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
99 98 1 34 vr1cl 
 |-  ( R e. Ring -> ( var1 ` R ) e. ( Base ` P ) )
100 10 99 syl 
 |-  ( ph -> ( var1 ` R ) e. ( Base ` P ) )
101 100 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( var1 ` R ) e. ( Base ` P ) )
102 90 91 95 97 101 mulgnn0cld 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) )
103 51 a1i 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> -oo e. RR* )
104 54 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> N e. RR* )
105 2 1 34 deg1xrcl 
 |-  ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. RR* )
106 102 105 syl 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. RR* )
107 106 mnfled 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> -oo <_ ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
108 96 nn0red 
 |-  ( n e. ( 0 ..^ N ) -> n e. RR )
109 108 rexrd 
 |-  ( n e. ( 0 ..^ N ) -> n e. RR* )
110 109 adantl 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> n e. RR* )
111 2 1 98 89 91 deg1pwle 
 |-  ( ( R e. Ring /\ n e. NN0 ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) <_ n )
112 10 96 111 syl2an 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) <_ n )
113 elfzolt2 
 |-  ( n e. ( 0 ..^ N ) -> n < N )
114 113 adantl 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> n < N )
115 106 110 104 112 114 xrlelttrd 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) < N )
116 103 104 106 107 115 elicod 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. ( -oo [,) N ) )
117 88 102 116 elpreimad 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( `' D " ( -oo [,) N ) ) )
118 117 3 eleqtrrdi 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. S )
119 46 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> S = ( Base ` E ) )
120 118 119 eleqtrd 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` E ) )
121 120 7 fmptd 
 |-  ( ph -> F : ( 0 ..^ N ) --> ( Base ` E ) )
122 121 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> F : ( 0 ..^ N ) --> ( Base ` E ) )
123 inidm 
 |-  ( ( 0 ..^ N ) i^i ( 0 ..^ N ) ) = ( 0 ..^ N )
124 86 87 122 24 24 123 off 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( a oF ( .s ` P ) F ) : ( 0 ..^ N ) --> S )
125 24 33 124 6 gsumsubm 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( P gsum ( a oF ( .s ` P ) F ) ) = ( E gsum ( a oF ( .s ` P ) F ) ) )
126 ringmnd 
 |-  ( P e. Ring -> P e. Mnd )
127 10 92 126 3syl 
 |-  ( ph -> P e. Mnd )
128 35 36 mp1i 
 |-  ( ph -> D Fn ( Base ` P ) )
129 34 13 mndidcl 
 |-  ( P e. Mnd -> ( 0g ` P ) e. ( Base ` P ) )
130 127 129 syl 
 |-  ( ph -> ( 0g ` P ) e. ( Base ` P ) )
131 51 a1i 
 |-  ( ph -> -oo e. RR* )
132 2 1 34 deg1xrcl 
 |-  ( ( 0g ` P ) e. ( Base ` P ) -> ( D ` ( 0g ` P ) ) e. RR* )
133 130 132 syl 
 |-  ( ph -> ( D ` ( 0g ` P ) ) e. RR* )
134 133 mnfled 
 |-  ( ph -> -oo <_ ( D ` ( 0g ` P ) ) )
135 2 1 13 deg1z 
 |-  ( R e. Ring -> ( D ` ( 0g ` P ) ) = -oo )
136 10 135 syl 
 |-  ( ph -> ( D ` ( 0g ` P ) ) = -oo )
137 53 mnfltd 
 |-  ( ph -> -oo < N )
138 136 137 eqbrtrd 
 |-  ( ph -> ( D ` ( 0g ` P ) ) < N )
139 131 54 133 134 138 elicod 
 |-  ( ph -> ( D ` ( 0g ` P ) ) e. ( -oo [,) N ) )
140 128 130 139 elpreimad 
 |-  ( ph -> ( 0g ` P ) e. ( `' D " ( -oo [,) N ) ) )
141 140 3 eleqtrrdi 
 |-  ( ph -> ( 0g ` P ) e. S )
142 6 34 13 ress0g 
 |-  ( ( P e. Mnd /\ ( 0g ` P ) e. S /\ S C_ ( Base ` P ) ) -> ( 0g ` P ) = ( 0g ` E ) )
143 127 141 44 142 syl3anc 
 |-  ( ph -> ( 0g ` P ) = ( 0g ` E ) )
144 143 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( 0g ` P ) = ( 0g ` E ) )
145 23 125 144 3eqtr4d 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( P gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` P ) )
146 1 8 9 11 7 12 13 22 145 ply1gsumz 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a = ( ( 0 ..^ N ) X. { ( 0g ` R ) } ) )
147 17 fveq2d 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
148 147 sneqd 
 |-  ( ph -> { ( 0g ` R ) } = { ( 0g ` ( Scalar ` P ) ) } )
149 148 xpeq2d 
 |-  ( ph -> ( ( 0 ..^ N ) X. { ( 0g ` R ) } ) = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) )
150 149 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> ( ( 0 ..^ N ) X. { ( 0g ` R ) } ) = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) )
151 146 150 eqtrd 
 |-  ( ( ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) /\ a finSupp ( 0g ` ( Scalar ` P ) ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) )
152 151 expl 
 |-  ( ( ph /\ a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ) -> ( ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) ) )
153 152 ralrimiva 
 |-  ( ph -> A. a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ( ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) ) )
154 118 7 fmptd 
 |-  ( ph -> F : ( 0 ..^ N ) --> S )
155 154 frnd 
 |-  ( ph -> ran F C_ S )
156 eqid 
 |-  ( LSpan ` P ) = ( LSpan ` P )
157 28 156 lspssp 
 |-  ( ( P e. LMod /\ S e. ( LSubSp ` P ) /\ ran F C_ S ) -> ( ( LSpan ` P ) ` ran F ) C_ S )
158 26 27 155 157 syl3anc 
 |-  ( ph -> ( ( LSpan ` P ) ` ran F ) C_ S )
159 breq1 
 |-  ( a = ( ( coe1 ` x ) |` ( 0 ..^ N ) ) -> ( a finSupp ( 0g ` ( Scalar ` P ) ) <-> ( ( coe1 ` x ) |` ( 0 ..^ N ) ) finSupp ( 0g ` ( Scalar ` P ) ) ) )
160 oveq1 
 |-  ( a = ( ( coe1 ` x ) |` ( 0 ..^ N ) ) -> ( a oF ( .s ` P ) F ) = ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) )
161 160 oveq2d 
 |-  ( a = ( ( coe1 ` x ) |` ( 0 ..^ N ) ) -> ( P gsum ( a oF ( .s ` P ) F ) ) = ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) )
162 161 eqeq2d 
 |-  ( a = ( ( coe1 ` x ) |` ( 0 ..^ N ) ) -> ( x = ( P gsum ( a oF ( .s ` P ) F ) ) <-> x = ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) ) )
163 159 162 anbi12d 
 |-  ( a = ( ( coe1 ` x ) |` ( 0 ..^ N ) ) -> ( ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( a oF ( .s ` P ) F ) ) ) <-> ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) ) ) )
164 fvexd 
 |-  ( ( ph /\ x e. S ) -> ( Base ` ( Scalar ` P ) ) e. _V )
165 ovexd 
 |-  ( ( ph /\ x e. S ) -> ( 0 ..^ N ) e. _V )
166 44 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. ( Base ` P ) )
167 eqid 
 |-  ( coe1 ` x ) = ( coe1 ` x )
168 167 34 1 8 coe1f 
 |-  ( x e. ( Base ` P ) -> ( coe1 ` x ) : NN0 --> ( Base ` R ) )
169 166 168 syl 
 |-  ( ( ph /\ x e. S ) -> ( coe1 ` x ) : NN0 --> ( Base ` R ) )
170 18 adantr 
 |-  ( ( ph /\ x e. S ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
171 170 feq3d 
 |-  ( ( ph /\ x e. S ) -> ( ( coe1 ` x ) : NN0 --> ( Base ` R ) <-> ( coe1 ` x ) : NN0 --> ( Base ` ( Scalar ` P ) ) ) )
172 169 171 mpbid 
 |-  ( ( ph /\ x e. S ) -> ( coe1 ` x ) : NN0 --> ( Base ` ( Scalar ` P ) ) )
173 fzo0ssnn0 
 |-  ( 0 ..^ N ) C_ NN0
174 173 a1i 
 |-  ( ( ph /\ x e. S ) -> ( 0 ..^ N ) C_ NN0 )
175 172 174 fssresd 
 |-  ( ( ph /\ x e. S ) -> ( ( coe1 ` x ) |` ( 0 ..^ N ) ) : ( 0 ..^ N ) --> ( Base ` ( Scalar ` P ) ) )
176 164 165 175 elmapdd 
 |-  ( ( ph /\ x e. S ) -> ( ( coe1 ` x ) |` ( 0 ..^ N ) ) e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) )
177 169 ffund 
 |-  ( ( ph /\ x e. S ) -> Fun ( coe1 ` x ) )
178 fzofi 
 |-  ( 0 ..^ N ) e. Fin
179 178 a1i 
 |-  ( ( ph /\ x e. S ) -> ( 0 ..^ N ) e. Fin )
180 fvexd 
 |-  ( ( ph /\ x e. S ) -> ( 0g ` ( Scalar ` P ) ) e. _V )
181 177 179 180 resfifsupp 
 |-  ( ( ph /\ x e. S ) -> ( ( coe1 ` x ) |` ( 0 ..^ N ) ) finSupp ( 0g ` ( Scalar ` P ) ) )
182 ringcmn 
 |-  ( P e. Ring -> P e. CMnd )
183 10 92 182 3syl 
 |-  ( ph -> P e. CMnd )
184 183 adantr 
 |-  ( ( ph /\ x e. S ) -> P e. CMnd )
185 nn0ex 
 |-  NN0 e. _V
186 185 a1i 
 |-  ( ( ph /\ x e. S ) -> NN0 e. _V )
187 26 ad2antrr 
 |-  ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> P e. LMod )
188 172 ffvelcdmda 
 |-  ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> ( ( coe1 ` x ) ` i ) e. ( Base ` ( Scalar ` P ) ) )
189 10 ad2antrr 
 |-  ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> R e. Ring )
190 189 92 93 3syl 
 |-  ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> ( mulGrp ` P ) e. Mnd )
191 simpr 
 |-  ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> i e. NN0 )
192 189 99 syl 
 |-  ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> ( var1 ` R ) e. ( Base ` P ) )
193 90 91 190 191 192 mulgnn0cld 
 |-  ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) )
194 34 38 39 40 187 188 193 lmodvscld 
 |-  ( ( ( ph /\ x e. S ) /\ i e. NN0 ) -> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. ( Base ` P ) )
195 eqid 
 |-  ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
196 194 195 fmptd 
 |-  ( ( ph /\ x e. S ) -> ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) : NN0 --> ( Base ` P ) )
197 nfv 
 |-  F/ i ( ph /\ x e. S )
198 197 194 195 fnmptd 
 |-  ( ( ph /\ x e. S ) -> ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) Fn NN0 )
199 fveq2 
 |-  ( i = j -> ( ( coe1 ` x ) ` i ) = ( ( coe1 ` x ) ` j ) )
200 oveq1 
 |-  ( i = j -> ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
201 199 200 oveq12d 
 |-  ( i = j -> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
202 simplr 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> j e. NN0 )
203 ovexd 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. _V )
204 195 201 202 203 fvmptd3 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) = ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
205 166 ad2antrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> x e. ( Base ` P ) )
206 icossxr 
 |-  ( -oo [,) N ) C_ RR*
207 206 75 sselid 
 |-  ( ( ph /\ x e. S ) -> ( D ` x ) e. RR* )
208 207 ad2antrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( D ` x ) e. RR* )
209 54 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> N e. RR* )
210 202 nn0red 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> j e. RR )
211 210 rexrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> j e. RR* )
212 79 ad2antrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( D ` x ) < N )
213 simpr 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> N <_ j )
214 208 209 211 212 213 xrltletrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( D ` x ) < j )
215 2 1 34 12 167 deg1lt 
 |-  ( ( x e. ( Base ` P ) /\ j e. NN0 /\ ( D ` x ) < j ) -> ( ( coe1 ` x ) ` j ) = ( 0g ` R ) )
216 205 202 214 215 syl3anc 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( coe1 ` x ) ` j ) = ( 0g ` R ) )
217 216 oveq1d 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( 0g ` R ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
218 147 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
219 218 oveq1d 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( 0g ` R ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
220 26 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> P e. LMod )
221 94 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( mulGrp ` P ) e. Mnd )
222 100 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( var1 ` R ) e. ( Base ` P ) )
223 90 91 221 202 222 mulgnn0cld 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) )
224 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
225 34 38 39 224 13 lmod0vs 
 |-  ( ( P e. LMod /\ ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) )
226 220 223 225 syl2anc 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) )
227 219 226 eqtrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( 0g ` R ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) )
228 204 217 227 3eqtrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ j e. NN0 ) /\ N <_ j ) -> ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) = ( 0g ` P ) )
229 4 nn0zd 
 |-  ( ph -> N e. ZZ )
230 229 adantr 
 |-  ( ( ph /\ x e. S ) -> N e. ZZ )
231 198 228 230 suppssnn0 
 |-  ( ( ph /\ x e. S ) -> ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) supp ( 0g ` P ) ) C_ ( 0 ..^ N ) )
232 186 mptexd 
 |-  ( ( ph /\ x e. S ) -> ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) e. _V )
233 198 fnfund 
 |-  ( ( ph /\ x e. S ) -> Fun ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
234 fvexd 
 |-  ( ( ph /\ x e. S ) -> ( 0g ` P ) e. _V )
235 suppssfifsupp 
 |-  ( ( ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) e. _V /\ Fun ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) /\ ( 0g ` P ) e. _V ) /\ ( ( 0 ..^ N ) e. Fin /\ ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) supp ( 0g ` P ) ) C_ ( 0 ..^ N ) ) ) -> ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) finSupp ( 0g ` P ) )
236 232 233 234 179 231 235 syl32anc 
 |-  ( ( ph /\ x e. S ) -> ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) finSupp ( 0g ` P ) )
237 34 13 184 186 196 231 236 gsumres 
 |-  ( ( ph /\ x e. S ) -> ( P gsum ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) ) = ( P gsum ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) )
238 fvexd 
 |-  ( ( ph /\ x e. S ) -> ( coe1 ` x ) e. _V )
239 ovexd 
 |-  ( ph -> ( 0 ..^ N ) e. _V )
240 154 239 fexd 
 |-  ( ph -> F e. _V )
241 240 adantr 
 |-  ( ( ph /\ x e. S ) -> F e. _V )
242 offres 
 |-  ( ( ( coe1 ` x ) e. _V /\ F e. _V ) -> ( ( ( coe1 ` x ) oF ( .s ` P ) F ) |` ( 0 ..^ N ) ) = ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) ( F |` ( 0 ..^ N ) ) ) )
243 238 241 242 syl2anc 
 |-  ( ( ph /\ x e. S ) -> ( ( ( coe1 ` x ) oF ( .s ` P ) F ) |` ( 0 ..^ N ) ) = ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) ( F |` ( 0 ..^ N ) ) ) )
244 169 ffnd 
 |-  ( ( ph /\ x e. S ) -> ( coe1 ` x ) Fn NN0 )
245 154 ffnd 
 |-  ( ph -> F Fn ( 0 ..^ N ) )
246 245 adantr 
 |-  ( ( ph /\ x e. S ) -> F Fn ( 0 ..^ N ) )
247 sseqin2 
 |-  ( ( 0 ..^ N ) C_ NN0 <-> ( NN0 i^i ( 0 ..^ N ) ) = ( 0 ..^ N ) )
248 173 247 mpbi 
 |-  ( NN0 i^i ( 0 ..^ N ) ) = ( 0 ..^ N )
249 eqidd 
 |-  ( ( ( ph /\ x e. S ) /\ j e. NN0 ) -> ( ( coe1 ` x ) ` j ) = ( ( coe1 ` x ) ` j ) )
250 oveq1 
 |-  ( n = j -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
251 simpr 
 |-  ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> j e. ( 0 ..^ N ) )
252 ovexd 
 |-  ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. _V )
253 7 250 251 252 fvmptd3 
 |-  ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( F ` j ) = ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
254 244 246 186 165 248 249 253 ofval 
 |-  ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( coe1 ` x ) oF ( .s ` P ) F ) ` j ) = ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
255 173 251 sselid 
 |-  ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> j e. NN0 )
256 ovexd 
 |-  ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. _V )
257 195 201 255 256 fvmptd3 
 |-  ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) = ( ( ( coe1 ` x ) ` j ) ( .s ` P ) ( j ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
258 254 257 eqtr4d 
 |-  ( ( ( ph /\ x e. S ) /\ j e. ( 0 ..^ N ) ) -> ( ( ( coe1 ` x ) oF ( .s ` P ) F ) ` j ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) )
259 258 ralrimiva 
 |-  ( ( ph /\ x e. S ) -> A. j e. ( 0 ..^ N ) ( ( ( coe1 ` x ) oF ( .s ` P ) F ) ` j ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) )
260 244 246 186 165 248 offn 
 |-  ( ( ph /\ x e. S ) -> ( ( coe1 ` x ) oF ( .s ` P ) F ) Fn ( 0 ..^ N ) )
261 ssidd 
 |-  ( ( ph /\ x e. S ) -> ( 0 ..^ N ) C_ ( 0 ..^ N ) )
262 fvreseq0 
 |-  ( ( ( ( ( coe1 ` x ) oF ( .s ` P ) F ) Fn ( 0 ..^ N ) /\ ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) Fn NN0 ) /\ ( ( 0 ..^ N ) C_ ( 0 ..^ N ) /\ ( 0 ..^ N ) C_ NN0 ) ) -> ( ( ( ( coe1 ` x ) oF ( .s ` P ) F ) |` ( 0 ..^ N ) ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) <-> A. j e. ( 0 ..^ N ) ( ( ( coe1 ` x ) oF ( .s ` P ) F ) ` j ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) ) )
263 260 198 261 174 262 syl22anc 
 |-  ( ( ph /\ x e. S ) -> ( ( ( ( coe1 ` x ) oF ( .s ` P ) F ) |` ( 0 ..^ N ) ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) <-> A. j e. ( 0 ..^ N ) ( ( ( coe1 ` x ) oF ( .s ` P ) F ) ` j ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ` j ) ) )
264 259 263 mpbird 
 |-  ( ( ph /\ x e. S ) -> ( ( ( coe1 ` x ) oF ( .s ` P ) F ) |` ( 0 ..^ N ) ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) )
265 fnresdm 
 |-  ( F Fn ( 0 ..^ N ) -> ( F |` ( 0 ..^ N ) ) = F )
266 245 265 syl 
 |-  ( ph -> ( F |` ( 0 ..^ N ) ) = F )
267 266 adantr 
 |-  ( ( ph /\ x e. S ) -> ( F |` ( 0 ..^ N ) ) = F )
268 267 oveq2d 
 |-  ( ( ph /\ x e. S ) -> ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) ( F |` ( 0 ..^ N ) ) ) = ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) )
269 243 264 268 3eqtr3rd 
 |-  ( ( ph /\ x e. S ) -> ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) = ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) )
270 269 oveq2d 
 |-  ( ( ph /\ x e. S ) -> ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) = ( P gsum ( ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |` ( 0 ..^ N ) ) ) )
271 10 adantr 
 |-  ( ( ph /\ x e. S ) -> R e. Ring )
272 1 98 34 39 89 91 167 ply1coe 
 |-  ( ( R e. Ring /\ x e. ( Base ` P ) ) -> x = ( P gsum ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) )
273 271 166 272 syl2anc 
 |-  ( ( ph /\ x e. S ) -> x = ( P gsum ( i e. NN0 |-> ( ( ( coe1 ` x ) ` i ) ( .s ` P ) ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) )
274 237 270 273 3eqtr4rd 
 |-  ( ( ph /\ x e. S ) -> x = ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) )
275 181 274 jca 
 |-  ( ( ph /\ x e. S ) -> ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( ( ( coe1 ` x ) |` ( 0 ..^ N ) ) oF ( .s ` P ) F ) ) ) )
276 163 176 275 rspcedvdw 
 |-  ( ( ph /\ x e. S ) -> E. a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( a oF ( .s ` P ) F ) ) ) )
277 102 7 fmptd 
 |-  ( ph -> F : ( 0 ..^ N ) --> ( Base ` P ) )
278 156 34 40 38 224 39 277 26 239 ellspd 
 |-  ( ph -> ( x e. ( ( LSpan ` P ) ` ( F " ( 0 ..^ N ) ) ) <-> E. a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( a oF ( .s ` P ) F ) ) ) ) )
279 278 adantr 
 |-  ( ( ph /\ x e. S ) -> ( x e. ( ( LSpan ` P ) ` ( F " ( 0 ..^ N ) ) ) <-> E. a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ x = ( P gsum ( a oF ( .s ` P ) F ) ) ) ) )
280 276 279 mpbird 
 |-  ( ( ph /\ x e. S ) -> x e. ( ( LSpan ` P ) ` ( F " ( 0 ..^ N ) ) ) )
281 imadmrn 
 |-  ( F " dom F ) = ran F
282 154 fdmd 
 |-  ( ph -> dom F = ( 0 ..^ N ) )
283 282 imaeq2d 
 |-  ( ph -> ( F " dom F ) = ( F " ( 0 ..^ N ) ) )
284 281 283 eqtr3id 
 |-  ( ph -> ran F = ( F " ( 0 ..^ N ) ) )
285 284 fveq2d 
 |-  ( ph -> ( ( LSpan ` P ) ` ran F ) = ( ( LSpan ` P ) ` ( F " ( 0 ..^ N ) ) ) )
286 285 adantr 
 |-  ( ( ph /\ x e. S ) -> ( ( LSpan ` P ) ` ran F ) = ( ( LSpan ` P ) ` ( F " ( 0 ..^ N ) ) ) )
287 280 286 eleqtrrd 
 |-  ( ( ph /\ x e. S ) -> x e. ( ( LSpan ` P ) ` ran F ) )
288 158 287 eqelssd 
 |-  ( ph -> ( ( LSpan ` P ) ` ran F ) = S )
289 eqid 
 |-  ( LSpan ` E ) = ( LSpan ` E )
290 6 156 289 28 lsslsp 
 |-  ( ( P e. LMod /\ S e. ( LSubSp ` P ) /\ ran F C_ S ) -> ( ( LSpan ` E ) ` ran F ) = ( ( LSpan ` P ) ` ran F ) )
291 290 eqcomd 
 |-  ( ( P e. LMod /\ S e. ( LSubSp ` P ) /\ ran F C_ S ) -> ( ( LSpan ` P ) ` ran F ) = ( ( LSpan ` E ) ` ran F ) )
292 26 27 155 291 syl3anc 
 |-  ( ph -> ( ( LSpan ` P ) ` ran F ) = ( ( LSpan ` E ) ` ran F ) )
293 288 292 46 3eqtr3d 
 |-  ( ph -> ( ( LSpan ` E ) ` ran F ) = ( Base ` E ) )
294 eqid 
 |-  ( Base ` E ) = ( Base ` E )
295 2 fvexi 
 |-  D e. _V
296 cnvexg 
 |-  ( D e. _V -> `' D e. _V )
297 imaexg 
 |-  ( `' D e. _V -> ( `' D " ( -oo [,) N ) ) e. _V )
298 295 296 297 mp2b 
 |-  ( `' D " ( -oo [,) N ) ) e. _V
299 3 298 eqeltri 
 |-  S e. _V
300 6 38 resssca 
 |-  ( S e. _V -> ( Scalar ` P ) = ( Scalar ` E ) )
301 299 300 ax-mp 
 |-  ( Scalar ` P ) = ( Scalar ` E )
302 301 fveq2i 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` E ) )
303 eqid 
 |-  ( Scalar ` E ) = ( Scalar ` E )
304 6 39 ressvsca 
 |-  ( S e. _V -> ( .s ` P ) = ( .s ` E ) )
305 299 304 ax-mp 
 |-  ( .s ` P ) = ( .s ` E )
306 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
307 301 fveq2i 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` E ) )
308 eqid 
 |-  ( LBasis ` E ) = ( LBasis ` E )
309 6 28 lsslvec 
 |-  ( ( P e. LVec /\ S e. ( LSubSp ` P ) ) -> E e. LVec )
310 25 27 309 syl2anc 
 |-  ( ph -> E e. LVec )
311 310 lveclmodd 
 |-  ( ph -> E e. LMod )
312 17 5 eqeltrrd 
 |-  ( ph -> ( Scalar ` P ) e. DivRing )
313 drngnzr 
 |-  ( ( Scalar ` P ) e. DivRing -> ( Scalar ` P ) e. NzRing )
314 312 313 syl 
 |-  ( ph -> ( Scalar ` P ) e. NzRing )
315 301 314 eqeltrrid 
 |-  ( ph -> ( Scalar ` E ) e. NzRing )
316 120 ralrimiva 
 |-  ( ph -> A. n e. ( 0 ..^ N ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` E ) )
317 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
318 5 317 syl 
 |-  ( ph -> R e. NzRing )
319 318 ad2antrr 
 |-  ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> R e. NzRing )
320 97 adantr 
 |-  ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> n e. NN0 )
321 elfzonn0 
 |-  ( i e. ( 0 ..^ N ) -> i e. NN0 )
322 321 adantl 
 |-  ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> i e. NN0 )
323 1 98 91 319 320 322 ply1moneq 
 |-  ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) <-> n = i ) )
324 323 biimpd 
 |-  ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) )
325 324 anasss 
 |-  ( ( ph /\ ( n e. ( 0 ..^ N ) /\ i e. ( 0 ..^ N ) ) ) -> ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) )
326 325 ralrimivva 
 |-  ( ph -> A. n e. ( 0 ..^ N ) A. i e. ( 0 ..^ N ) ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) )
327 oveq1 
 |-  ( n = i -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
328 7 327 f1mpt 
 |-  ( F : ( 0 ..^ N ) -1-1-> ( Base ` E ) <-> ( A. n e. ( 0 ..^ N ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` E ) /\ A. n e. ( 0 ..^ N ) A. i e. ( 0 ..^ N ) ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) ) )
329 316 326 328 sylanbrc 
 |-  ( ph -> F : ( 0 ..^ N ) -1-1-> ( Base ` E ) )
330 294 302 303 305 306 307 308 289 311 315 239 329 islbs5 
 |-  ( ph -> ( ran F e. ( LBasis ` E ) <-> ( A. a e. ( ( Base ` ( Scalar ` P ) ) ^m ( 0 ..^ N ) ) ( ( a finSupp ( 0g ` ( Scalar ` P ) ) /\ ( E gsum ( a oF ( .s ` P ) F ) ) = ( 0g ` E ) ) -> a = ( ( 0 ..^ N ) X. { ( 0g ` ( Scalar ` P ) ) } ) ) /\ ( ( LSpan ` E ) ` ran F ) = ( Base ` E ) ) ) )
331 153 293 330 mpbir2and 
 |-  ( ph -> ran F e. ( LBasis ` E ) )