Metamath Proof Explorer

Theorem extdgfialglem1

Description: Lemma for extdgfialg . (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses extdgfialg.b 
|- B = ( Base ` E )
extdgfialg.d 
|- D = ( dim ` ( ( subringAlg ` E ) ` F ) )
extdgfialg.e 
|- ( ph -> E e. Field )
extdgfialg.f 
|- ( ph -> F e. ( SubDRing ` E ) )
extdgfialg.1 
|- ( ph -> D e. NN0 )
extdgfialglem1.2 
|- Z = ( 0g ` E )
extdgfialglem1.3 
|- .x. = ( .r ` E )
extdgfialglem1.r 
|- G = ( n e. ( 0 ... D ) |-> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) )
extdgfialglem1.4 
|- ( ph -> X e. B )
Assertion extdgfialglem1 
|- ( ph -> E. a e. ( F ^m ( 0 ... D ) ) ( a finSupp Z /\ ( ( E gsum ( a oF .x. G ) ) = Z /\ a =/= ( ( 0 ... D ) X. { Z } ) ) ) )

Proof

Step Hyp Ref Expression
1 extdgfialg.b 
 |-  B = ( Base ` E )
2 extdgfialg.d 
 |-  D = ( dim ` ( ( subringAlg ` E ) ` F ) )
3 extdgfialg.e 
 |-  ( ph -> E e. Field )
4 extdgfialg.f 
 |-  ( ph -> F e. ( SubDRing ` E ) )
5 extdgfialg.1 
 |-  ( ph -> D e. NN0 )
6 extdgfialglem1.2 
 |-  Z = ( 0g ` E )
7 extdgfialglem1.3 
 |-  .x. = ( .r ` E )
8 extdgfialglem1.r 
 |-  G = ( n e. ( 0 ... D ) |-> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) )
9 extdgfialglem1.4 
 |-  ( ph -> X e. B )
10 simplr 
 |-  ( ( ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) /\ b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ) /\ ran G C_ b ) -> b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) )
11 3 flddrngd 
 |-  ( ph -> E e. DivRing )
12 eqid 
 |-  ( E |`s F ) = ( E |`s F )
13 12 sdrgdrng 
 |-  ( F e. ( SubDRing ` E ) -> ( E |`s F ) e. DivRing )
14 4 13 syl 
 |-  ( ph -> ( E |`s F ) e. DivRing )
15 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
16 4 15 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
17 eqid 
 |-  ( ( subringAlg ` E ) ` F ) = ( ( subringAlg ` E ) ` F )
18 17 12 sralvec 
 |-  ( ( E e. DivRing /\ ( E |`s F ) e. DivRing /\ F e. ( SubRing ` E ) ) -> ( ( subringAlg ` E ) ` F ) e. LVec )
19 11 14 16 18 syl3anc 
 |-  ( ph -> ( ( subringAlg ` E ) ` F ) e. LVec )
20 19 ad2antrr 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> ( ( subringAlg ` E ) ` F ) e. LVec )
21 20 ad2antrr 
 |-  ( ( ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) /\ b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ) /\ ran G C_ b ) -> ( ( subringAlg ` E ) ` F ) e. LVec )
22 eqid 
 |-  ( LBasis ` ( ( subringAlg ` E ) ` F ) ) = ( LBasis ` ( ( subringAlg ` E ) ` F ) )
23 22 dimval 
 |-  ( ( ( ( subringAlg ` E ) ` F ) e. LVec /\ b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ) -> ( dim ` ( ( subringAlg ` E ) ` F ) ) = ( # ` b ) )
24 2 23 eqtrid 
 |-  ( ( ( ( subringAlg ` E ) ` F ) e. LVec /\ b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ) -> D = ( # ` b ) )
25 21 10 24 syl2anc 
 |-  ( ( ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) /\ b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ) /\ ran G C_ b ) -> D = ( # ` b ) )
26 5 ad4antr 
 |-  ( ( ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) /\ b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ) /\ ran G C_ b ) -> D e. NN0 )
27 25 26 eqeltrrd 
 |-  ( ( ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) /\ b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ) /\ ran G C_ b ) -> ( # ` b ) e. NN0 )
28 hashclb 
 |-  ( b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) -> ( b e. Fin <-> ( # ` b ) e. NN0 ) )
29 28 biimpar 
 |-  ( ( b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) /\ ( # ` b ) e. NN0 ) -> b e. Fin )
30 10 27 29 syl2anc 
 |-  ( ( ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) /\ b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ) /\ ran G C_ b ) -> b e. Fin )
31 hashss 
 |-  ( ( b e. Fin /\ ran G C_ b ) -> ( # ` ran G ) <_ ( # ` b ) )
32 30 31 sylancom 
 |-  ( ( ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) /\ b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ) /\ ran G C_ b ) -> ( # ` ran G ) <_ ( # ` b ) )
33 8 dmeqi 
 |-  dom G = dom ( n e. ( 0 ... D ) |-> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) )
34 eqid 
 |-  ( n e. ( 0 ... D ) |-> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) ) = ( n e. ( 0 ... D ) |-> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) )
35 ovexd 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ n e. ( 0 ... D ) ) -> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) e. _V )
36 34 35 dmmptd 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> dom ( n e. ( 0 ... D ) |-> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) ) = ( 0 ... D ) )
37 ovexd 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> ( 0 ... D ) e. _V )
38 36 37 eqeltrd 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> dom ( n e. ( 0 ... D ) |-> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) ) e. _V )
39 33 38 eqeltrid 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> dom G e. _V )
40 hashf1rn 
 |-  ( ( dom G e. _V /\ G : dom G -1-1-> _V ) -> ( # ` G ) = ( # ` ran G ) )
41 39 40 sylancom 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> ( # ` G ) = ( # ` ran G ) )
42 41 ad3antrrr 
 |-  ( ( ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) /\ b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ) /\ ran G C_ b ) -> ( # ` G ) = ( # ` ran G ) )
43 32 42 25 3brtr4d 
 |-  ( ( ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) /\ b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ) /\ ran G C_ b ) -> ( # ` G ) <_ D )
44 22 islinds4 
 |-  ( ( ( subringAlg ` E ) ` F ) e. LVec -> ( ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) <-> E. b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ran G C_ b ) )
45 44 biimpa 
 |-  ( ( ( ( subringAlg ` E ) ` F ) e. LVec /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> E. b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ran G C_ b )
46 20 45 sylancom 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> E. b e. ( LBasis ` ( ( subringAlg ` E ) ` F ) ) ran G C_ b )
47 43 46 r19.29a 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> ( # ` G ) <_ D )
48 5 nn0red 
 |-  ( ph -> D e. RR )
49 48 ad2antrr 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> D e. RR )
50 49 ltp1d 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> D < ( D + 1 ) )
51 fzfid 
 |-  ( ph -> ( 0 ... D ) e. Fin )
52 51 mptexd 
 |-  ( ph -> ( n e. ( 0 ... D ) |-> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) ) e. _V )
53 8 52 eqeltrid 
 |-  ( ph -> G e. _V )
54 53 adantr 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> G e. _V )
55 f1f 
 |-  ( G : dom G -1-1-> _V -> G : dom G --> _V )
56 55 adantl 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> G : dom G --> _V )
57 56 ffund 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> Fun G )
58 hashfundm 
 |-  ( ( G e. _V /\ Fun G ) -> ( # ` G ) = ( # ` dom G ) )
59 54 57 58 syl2anc 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> ( # ` G ) = ( # ` dom G ) )
60 8 35 dmmptd 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> dom G = ( 0 ... D ) )
61 60 fveq2d 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> ( # ` dom G ) = ( # ` ( 0 ... D ) ) )
62 hashfz0 
 |-  ( D e. NN0 -> ( # ` ( 0 ... D ) ) = ( D + 1 ) )
63 5 62 syl 
 |-  ( ph -> ( # ` ( 0 ... D ) ) = ( D + 1 ) )
64 63 adantr 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> ( # ` ( 0 ... D ) ) = ( D + 1 ) )
65 59 61 64 3eqtrd 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> ( # ` G ) = ( D + 1 ) )
66 65 adantr 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> ( # ` G ) = ( D + 1 ) )
67 50 66 breqtrrd 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> D < ( # ` G ) )
68 49 rexrd 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> D e. RR* )
69 54 adantr 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> G e. _V )
70 hashxrcl 
 |-  ( G e. _V -> ( # ` G ) e. RR* )
71 69 70 syl 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> ( # ` G ) e. RR* )
72 68 71 xrltnled 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> ( D < ( # ` G ) <-> -. ( # ` G ) <_ D ) )
73 67 72 mpbid 
 |-  ( ( ( ph /\ G : dom G -1-1-> _V ) /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) -> -. ( # ` G ) <_ D )
74 47 73 pm2.65da 
 |-  ( ( ph /\ G : dom G -1-1-> _V ) -> -. ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) )
75 74 ex 
 |-  ( ph -> ( G : dom G -1-1-> _V -> -. ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) )
76 imnan 
 |-  ( ( G : dom G -1-1-> _V -> -. ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) <-> -. ( G : dom G -1-1-> _V /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) )
77 75 76 sylib 
 |-  ( ph -> -. ( G : dom G -1-1-> _V /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) )
78 19 lveclmodd 
 |-  ( ph -> ( ( subringAlg ` E ) ` F ) e. LMod )
79 eqidd 
 |-  ( ph -> ( ( subringAlg ` E ) ` F ) = ( ( subringAlg ` E ) ` F ) )
80 1 sdrgss 
 |-  ( F e. ( SubDRing ` E ) -> F C_ B )
81 4 80 syl 
 |-  ( ph -> F C_ B )
82 81 1 sseqtrdi 
 |-  ( ph -> F C_ ( Base ` E ) )
83 79 82 srasca 
 |-  ( ph -> ( E |`s F ) = ( Scalar ` ( ( subringAlg ` E ) ` F ) ) )
84 drngnzr 
 |-  ( ( E |`s F ) e. DivRing -> ( E |`s F ) e. NzRing )
85 14 84 syl 
 |-  ( ph -> ( E |`s F ) e. NzRing )
86 83 85 eqeltrrd 
 |-  ( ph -> ( Scalar ` ( ( subringAlg ` E ) ` F ) ) e. NzRing )
87 eqid 
 |-  ( Scalar ` ( ( subringAlg ` E ) ` F ) ) = ( Scalar ` ( ( subringAlg ` E ) ` F ) )
88 87 islindf3 
 |-  ( ( ( ( subringAlg ` E ) ` F ) e. LMod /\ ( Scalar ` ( ( subringAlg ` E ) ` F ) ) e. NzRing ) -> ( G LIndF ( ( subringAlg ` E ) ` F ) <-> ( G : dom G -1-1-> _V /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) ) )
89 78 86 88 syl2anc 
 |-  ( ph -> ( G LIndF ( ( subringAlg ` E ) ` F ) <-> ( G : dom G -1-1-> _V /\ ran G e. ( LIndS ` ( ( subringAlg ` E ) ` F ) ) ) ) )
90 77 89 mtbird 
 |-  ( ph -> -. G LIndF ( ( subringAlg ` E ) ` F ) )
91 ovexd 
 |-  ( ph -> ( 0 ... D ) e. _V )
92 eqid 
 |-  ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) = ( mulGrp ` ( ( subringAlg ` E ) ` F ) )
93 eqid 
 |-  ( Base ` ( ( subringAlg ` E ) ` F ) ) = ( Base ` ( ( subringAlg ` E ) ` F ) )
94 92 93 mgpbas 
 |-  ( Base ` ( ( subringAlg ` E ) ` F ) ) = ( Base ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) )
95 eqid 
 |-  ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) = ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) )
96 3 fldcrngd 
 |-  ( ph -> E e. CRing )
97 96 crngringd 
 |-  ( ph -> E e. Ring )
98 17 1 sraring 
 |-  ( ( E e. Ring /\ F C_ B ) -> ( ( subringAlg ` E ) ` F ) e. Ring )
99 97 81 98 syl2anc 
 |-  ( ph -> ( ( subringAlg ` E ) ` F ) e. Ring )
100 92 ringmgp 
 |-  ( ( ( subringAlg ` E ) ` F ) e. Ring -> ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) e. Mnd )
101 99 100 syl 
 |-  ( ph -> ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) e. Mnd )
102 101 adantr 
 |-  ( ( ph /\ n e. ( 0 ... D ) ) -> ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) e. Mnd )
103 fz0ssnn0 
 |-  ( 0 ... D ) C_ NN0
104 103 a1i 
 |-  ( ph -> ( 0 ... D ) C_ NN0 )
105 104 sselda 
 |-  ( ( ph /\ n e. ( 0 ... D ) ) -> n e. NN0 )
106 79 82 srabase 
 |-  ( ph -> ( Base ` E ) = ( Base ` ( ( subringAlg ` E ) ` F ) ) )
107 1 106 eqtr2id 
 |-  ( ph -> ( Base ` ( ( subringAlg ` E ) ` F ) ) = B )
108 9 107 eleqtrrd 
 |-  ( ph -> X e. ( Base ` ( ( subringAlg ` E ) ` F ) ) )
109 108 adantr 
 |-  ( ( ph /\ n e. ( 0 ... D ) ) -> X e. ( Base ` ( ( subringAlg ` E ) ` F ) ) )
110 94 95 102 105 109 mulgnn0cld 
 |-  ( ( ph /\ n e. ( 0 ... D ) ) -> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) X ) e. ( Base ` ( ( subringAlg ` E ) ` F ) ) )
111 110 8 fmptd 
 |-  ( ph -> G : ( 0 ... D ) --> ( Base ` ( ( subringAlg ` E ) ` F ) ) )
112 eqid 
 |-  ( .s ` ( ( subringAlg ` E ) ` F ) ) = ( .s ` ( ( subringAlg ` E ) ` F ) )
113 eqid 
 |-  ( 0g ` ( ( subringAlg ` E ) ` F ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) )
114 eqid 
 |-  ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) = ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) )
115 eqid 
 |-  ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) = ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) )
116 93 87 112 113 114 115 islindf4 
 |-  ( ( ( ( subringAlg ` E ) ` F ) e. LMod /\ ( 0 ... D ) e. _V /\ G : ( 0 ... D ) --> ( Base ` ( ( subringAlg ` E ) ` F ) ) ) -> ( G LIndF ( ( subringAlg ` E ) ` F ) <-> A. a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) -> a = ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) )
117 78 91 111 116 syl3anc 
 |-  ( ph -> ( G LIndF ( ( subringAlg ` E ) ` F ) <-> A. a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) -> a = ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) )
118 90 117 mtbid 
 |-  ( ph -> -. A. a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) -> a = ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) )
119 rexanali 
 |-  ( E. a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ -. a = ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) <-> -. A. a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) -> a = ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) )
120 118 119 sylibr 
 |-  ( ph -> E. a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ -. a = ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) )
121 fvex 
 |-  ( Scalar ` ( ( subringAlg ` E ) ` F ) ) e. _V
122 ovex 
 |-  ( 0 ... D ) e. _V
123 eqid 
 |-  ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) = ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) )
124 eqid 
 |-  ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) = ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) )
125 123 124 114 115 frlmelbas 
 |-  ( ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) e. _V /\ ( 0 ... D ) e. _V ) -> ( a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) <-> ( a e. ( ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ^m ( 0 ... D ) ) /\ a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ) ) )
126 121 122 125 mp2an 
 |-  ( a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) <-> ( a e. ( ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ^m ( 0 ... D ) ) /\ a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ) )
127 126 anbi1i 
 |-  ( ( a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) <-> ( ( a e. ( ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ^m ( 0 ... D ) ) /\ a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) )
128 df-ne 
 |-  ( a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) <-> -. a = ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) )
129 128 anbi2i 
 |-  ( ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) <-> ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ -. a = ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) )
130 129 anbi2i 
 |-  ( ( a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) <-> ( a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ -. a = ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) )
131 anass 
 |-  ( ( ( a e. ( ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ^m ( 0 ... D ) ) /\ a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) <-> ( a e. ( ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ^m ( 0 ... D ) ) /\ ( a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) ) )
132 127 130 131 3bitr3i 
 |-  ( ( a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ -. a = ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) <-> ( a e. ( ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ^m ( 0 ... D ) ) /\ ( a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) ) )
133 132 rexbii2 
 |-  ( E. a e. ( Base ` ( ( Scalar ` ( ( subringAlg ` E ) ` F ) ) freeLMod ( 0 ... D ) ) ) ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ -. a = ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) <-> E. a e. ( ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ^m ( 0 ... D ) ) ( a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) )
134 120 133 sylib 
 |-  ( ph -> E. a e. ( ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ^m ( 0 ... D ) ) ( a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) )
135 12 1 ressbas2 
 |-  ( F C_ B -> F = ( Base ` ( E |`s F ) ) )
136 81 135 syl 
 |-  ( ph -> F = ( Base ` ( E |`s F ) ) )
137 83 fveq2d 
 |-  ( ph -> ( Base ` ( E |`s F ) ) = ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) )
138 136 137 eqtr2d 
 |-  ( ph -> ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) = F )
139 138 oveq1d 
 |-  ( ph -> ( ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ^m ( 0 ... D ) ) = ( F ^m ( 0 ... D ) ) )
140 96 crnggrpd 
 |-  ( ph -> E e. Grp )
141 140 grpmndd 
 |-  ( ph -> E e. Mnd )
142 subrgsubg 
 |-  ( F e. ( SubRing ` E ) -> F e. ( SubGrp ` E ) )
143 16 142 syl 
 |-  ( ph -> F e. ( SubGrp ` E ) )
144 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
145 144 subg0cl 
 |-  ( F e. ( SubGrp ` E ) -> ( 0g ` E ) e. F )
146 143 145 syl 
 |-  ( ph -> ( 0g ` E ) e. F )
147 12 1 144 ress0g 
 |-  ( ( E e. Mnd /\ ( 0g ` E ) e. F /\ F C_ B ) -> ( 0g ` E ) = ( 0g ` ( E |`s F ) ) )
148 141 146 81 147 syl3anc 
 |-  ( ph -> ( 0g ` E ) = ( 0g ` ( E |`s F ) ) )
149 83 fveq2d 
 |-  ( ph -> ( 0g ` ( E |`s F ) ) = ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) )
150 148 149 eqtr2d 
 |-  ( ph -> ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) = ( 0g ` E ) )
151 150 6 eqtr4di 
 |-  ( ph -> ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) = Z )
152 151 breq2d 
 |-  ( ph -> ( a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) <-> a finSupp Z ) )
153 79 82 sravsca 
 |-  ( ph -> ( .r ` E ) = ( .s ` ( ( subringAlg ` E ) ` F ) ) )
154 7 153 eqtr2id 
 |-  ( ph -> ( .s ` ( ( subringAlg ` E ) ` F ) ) = .x. )
155 154 ofeqd 
 |-  ( ph -> oF ( .s ` ( ( subringAlg ` E ) ` F ) ) = oF .x. )
156 155 oveqd 
 |-  ( ph -> ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) = ( a oF .x. G ) )
157 156 oveq2d 
 |-  ( ph -> ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( ( ( subringAlg ` E ) ` F ) gsum ( a oF .x. G ) ) )
158 ovexd 
 |-  ( ph -> ( a oF .x. G ) e. _V )
159 17 158 3 19 82 gsumsra 
 |-  ( ph -> ( E gsum ( a oF .x. G ) ) = ( ( ( subringAlg ` E ) ` F ) gsum ( a oF .x. G ) ) )
160 157 159 eqtr4d 
 |-  ( ph -> ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( E gsum ( a oF .x. G ) ) )
161 6 a1i 
 |-  ( ph -> Z = ( 0g ` E ) )
162 79 161 82 sralmod0 
 |-  ( ph -> Z = ( 0g ` ( ( subringAlg ` E ) ` F ) ) )
163 162 eqcomd 
 |-  ( ph -> ( 0g ` ( ( subringAlg ` E ) ` F ) ) = Z )
164 160 163 eqeq12d 
 |-  ( ph -> ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) <-> ( E gsum ( a oF .x. G ) ) = Z ) )
165 151 sneqd 
 |-  ( ph -> { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } = { Z } )
166 165 xpeq2d 
 |-  ( ph -> ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) = ( ( 0 ... D ) X. { Z } ) )
167 166 neeq2d 
 |-  ( ph -> ( a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) <-> a =/= ( ( 0 ... D ) X. { Z } ) ) )
168 164 167 anbi12d 
 |-  ( ph -> ( ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) <-> ( ( E gsum ( a oF .x. G ) ) = Z /\ a =/= ( ( 0 ... D ) X. { Z } ) ) ) )
169 152 168 anbi12d 
 |-  ( ph -> ( ( a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) <-> ( a finSupp Z /\ ( ( E gsum ( a oF .x. G ) ) = Z /\ a =/= ( ( 0 ... D ) X. { Z } ) ) ) ) )
170 139 169 rexeqbidv 
 |-  ( ph -> ( E. a e. ( ( Base ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) ^m ( 0 ... D ) ) ( a finSupp ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) /\ ( ( ( ( subringAlg ` E ) ` F ) gsum ( a oF ( .s ` ( ( subringAlg ` E ) ` F ) ) G ) ) = ( 0g ` ( ( subringAlg ` E ) ` F ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` ( Scalar ` ( ( subringAlg ` E ) ` F ) ) ) } ) ) ) <-> E. a e. ( F ^m ( 0 ... D ) ) ( a finSupp Z /\ ( ( E gsum ( a oF .x. G ) ) = Z /\ a =/= ( ( 0 ... D ) X. { Z } ) ) ) ) )
171 134 170 mpbid 
 |-  ( ph -> E. a e. ( F ^m ( 0 ... D ) ) ( a finSupp Z /\ ( ( E gsum ( a oF .x. G ) ) = Z /\ a =/= ( ( 0 ... D ) X. { Z } ) ) ) )