Metamath Proof Explorer

Theorem lmod1

Description: The (smallest) structure representing azero module over an arbitrary ring. (Contributed by AV, 29-Apr-2019)

Ref Expression
Hypothesis lmod1.m 
|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )
Assertion lmod1 
|- ( ( I e. V /\ R e. Ring ) -> M e. LMod )

Proof

Step Hyp Ref Expression
1 lmod1.m 
 |-  M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )
2 eqid 
 |-  { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
3 2 grp1 
 |-  ( I e. V -> { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } e. Grp )
4 fvex 
 |-  ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) e. _V
5 snex 
 |-  { I } e. _V
6 2 grpbase 
 |-  ( { I } e. _V -> { I } = ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) )
7 5 6 ax-mp 
 |-  { I } = ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } )
8 7 opeq2i 
 |-  <. ( Base ` ndx ) , { I } >. = <. ( Base ` ndx ) , ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >.
9 tpeq1 
 |-  ( <. ( Base ` ndx ) , { I } >. = <. ( Base ` ndx ) , ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >. -> { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } = { <. ( Base ` ndx ) , ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } )
10 8 9 ax-mp 
 |-  { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } = { <. ( Base ` ndx ) , ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. }
11 10 uneq1i 
 |-  ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } ) = ( { <. ( Base ` ndx ) , ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )
12 1 11 eqtri 
 |-  M = ( { <. ( Base ` ndx ) , ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )
13 12 lmodbase 
 |-  ( ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) e. _V -> ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) = ( Base ` M ) )
14 4 13 ax-mp 
 |-  ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) = ( Base ` M )
15 14 eqcomi 
 |-  ( Base ` M ) = ( Base ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } )
16 fvex 
 |-  ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) e. _V
17 snex 
 |-  { <. <. I , I >. , I >. } e. _V
18 2 grpplusg 
 |-  ( { <. <. I , I >. , I >. } e. _V -> { <. <. I , I >. , I >. } = ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) )
19 17 18 ax-mp 
 |-  { <. <. I , I >. , I >. } = ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } )
20 19 opeq2i 
 |-  <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. = <. ( +g ` ndx ) , ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >.
21 tpeq2 
 |-  ( <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. = <. ( +g ` ndx ) , ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >. -> { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >. , <. ( Scalar ` ndx ) , R >. } )
22 20 21 ax-mp 
 |-  { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >. , <. ( Scalar ` ndx ) , R >. }
23 22 uneq1i 
 |-  ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } ) = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )
24 1 23 eqtri 
 |-  M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } )
25 24 lmodplusg 
 |-  ( ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) e. _V -> ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) = ( +g ` M ) )
26 16 25 ax-mp 
 |-  ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } ) = ( +g ` M )
27 26 eqcomi 
 |-  ( +g ` M ) = ( +g ` { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } )
28 15 27 grpprop 
 |-  ( M e. Grp <-> { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. } e. Grp )
29 3 28 sylibr 
 |-  ( I e. V -> M e. Grp )
30 29 adantr 
 |-  ( ( I e. V /\ R e. Ring ) -> M e. Grp )
31 1 lmodsca 
 |-  ( R e. Ring -> R = ( Scalar ` M ) )
32 31 eqcomd 
 |-  ( R e. Ring -> ( Scalar ` M ) = R )
33 32 adantl 
 |-  ( ( I e. V /\ R e. Ring ) -> ( Scalar ` M ) = R )
34 simpr 
 |-  ( ( I e. V /\ R e. Ring ) -> R e. Ring )
35 33 34 eqeltrd 
 |-  ( ( I e. V /\ R e. Ring ) -> ( Scalar ` M ) e. Ring )
36 33 fveq2d 
 |-  ( ( I e. V /\ R e. Ring ) -> ( Base ` ( Scalar ` M ) ) = ( Base ` R ) )
37 36 eleq2d 
 |-  ( ( I e. V /\ R e. Ring ) -> ( q e. ( Base ` ( Scalar ` M ) ) <-> q e. ( Base ` R ) ) )
38 36 eleq2d 
 |-  ( ( I e. V /\ R e. Ring ) -> ( r e. ( Base ` ( Scalar ` M ) ) <-> r e. ( Base ` R ) ) )
39 37 38 anbi12d 
 |-  ( ( I e. V /\ R e. Ring ) -> ( ( q e. ( Base ` ( Scalar ` M ) ) /\ r e. ( Base ` ( Scalar ` M ) ) ) <-> ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) )
40 simpll 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> I e. V )
41 simplr 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> R e. Ring )
42 simprr 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> r e. ( Base ` R ) )
43 40 41 42 3jca 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) )
44 1 lmod1lem1 
 |-  ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( r ( .s ` M ) I ) e. { I } )
45 43 44 syl 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( r ( .s ` M ) I ) e. { I } )
46 1 lmod1lem2 
 |-  ( ( I e. V /\ R e. Ring /\ r e. ( Base ` R ) ) -> ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) )
47 43 46 syl 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) )
48 1 lmod1lem3 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) )
49 45 47 48 3jca 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( r ( .s ` M ) I ) e. { I } /\ ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) )
50 1 lmod1lem4 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) )
51 1 lmod1lem5 
 |-  ( ( I e. V /\ R e. Ring ) -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I )
52 51 adantr 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I )
53 49 50 52 jca32 
 |-  ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( ( r ( .s ` M ) I ) e. { I } /\ ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I ) ) )
54 53 ex 
 |-  ( ( I e. V /\ R e. Ring ) -> ( ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) -> ( ( ( r ( .s ` M ) I ) e. { I } /\ ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I ) ) ) )
55 39 54 sylbid 
 |-  ( ( I e. V /\ R e. Ring ) -> ( ( q e. ( Base ` ( Scalar ` M ) ) /\ r e. ( Base ` ( Scalar ` M ) ) ) -> ( ( ( r ( .s ` M ) I ) e. { I } /\ ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I ) ) ) )
56 55 ralrimivv 
 |-  ( ( I e. V /\ R e. Ring ) -> A. q e. ( Base ` ( Scalar ` M ) ) A. r e. ( Base ` ( Scalar ` M ) ) ( ( ( r ( .s ` M ) I ) e. { I } /\ ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I ) ) )
57 oveq2 
 |-  ( x = I -> ( w ( +g ` M ) x ) = ( w ( +g ` M ) I ) )
58 57 oveq2d 
 |-  ( x = I -> ( r ( .s ` M ) ( w ( +g ` M ) x ) ) = ( r ( .s ` M ) ( w ( +g ` M ) I ) ) )
59 oveq2 
 |-  ( x = I -> ( r ( .s ` M ) x ) = ( r ( .s ` M ) I ) )
60 59 oveq2d 
 |-  ( x = I -> ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) x ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) )
61 58 60 eqeq12d 
 |-  ( x = I -> ( ( r ( .s ` M ) ( w ( +g ` M ) x ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) x ) ) <-> ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) )
62 61 3anbi2d 
 |-  ( x = I -> ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) x ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) x ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) <-> ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) ) )
63 62 anbi1d 
 |-  ( x = I -> ( ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) x ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) x ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) <-> ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) ) )
64 63 ralbidv 
 |-  ( x = I -> ( A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) x ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) x ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) <-> A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) ) )
65 64 ralsng 
 |-  ( I e. V -> ( A. x e. { I } A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) x ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) x ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) <-> A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) ) )
66 65 adantr 
 |-  ( ( I e. V /\ R e. Ring ) -> ( A. x e. { I } A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) x ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) x ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) <-> A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) ) )
67 oveq2 
 |-  ( w = I -> ( r ( .s ` M ) w ) = ( r ( .s ` M ) I ) )
68 67 eleq1d 
 |-  ( w = I -> ( ( r ( .s ` M ) w ) e. { I } <-> ( r ( .s ` M ) I ) e. { I } ) )
69 oveq1 
 |-  ( w = I -> ( w ( +g ` M ) I ) = ( I ( +g ` M ) I ) )
70 69 oveq2d 
 |-  ( w = I -> ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( r ( .s ` M ) ( I ( +g ` M ) I ) ) )
71 67 oveq1d 
 |-  ( w = I -> ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) )
72 70 71 eqeq12d 
 |-  ( w = I -> ( ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) <-> ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) )
73 oveq2 
 |-  ( w = I -> ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) )
74 oveq2 
 |-  ( w = I -> ( q ( .s ` M ) w ) = ( q ( .s ` M ) I ) )
75 74 67 oveq12d 
 |-  ( w = I -> ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) )
76 73 75 eqeq12d 
 |-  ( w = I -> ( ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) <-> ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) )
77 68 72 76 3anbi123d 
 |-  ( w = I -> ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) <-> ( ( r ( .s ` M ) I ) e. { I } /\ ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) ) )
78 oveq2 
 |-  ( w = I -> ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) )
79 67 oveq2d 
 |-  ( w = I -> ( q ( .s ` M ) ( r ( .s ` M ) w ) ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) )
80 78 79 eqeq12d 
 |-  ( w = I -> ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) <-> ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) ) )
81 oveq2 
 |-  ( w = I -> ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) )
82 id 
 |-  ( w = I -> w = I )
83 81 82 eqeq12d 
 |-  ( w = I -> ( ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w <-> ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I ) )
84 80 83 anbi12d 
 |-  ( w = I -> ( ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) <-> ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I ) ) )
85 77 84 anbi12d 
 |-  ( w = I -> ( ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) <-> ( ( ( r ( .s ` M ) I ) e. { I } /\ ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I ) ) ) )
86 85 ralsng 
 |-  ( I e. V -> ( A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) <-> ( ( ( r ( .s ` M ) I ) e. { I } /\ ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I ) ) ) )
87 86 adantr 
 |-  ( ( I e. V /\ R e. Ring ) -> ( A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) I ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) <-> ( ( ( r ( .s ` M ) I ) e. { I } /\ ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I ) ) ) )
88 66 87 bitrd 
 |-  ( ( I e. V /\ R e. Ring ) -> ( A. x e. { I } A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) x ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) x ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) <-> ( ( ( r ( .s ` M ) I ) e. { I } /\ ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I ) ) ) )
89 88 2ralbidv 
 |-  ( ( I e. V /\ R e. Ring ) -> ( A. q e. ( Base ` ( Scalar ` M ) ) A. r e. ( Base ` ( Scalar ` M ) ) A. x e. { I } A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) x ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) x ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) <-> A. q e. ( Base ` ( Scalar ` M ) ) A. r e. ( Base ` ( Scalar ` M ) ) ( ( ( r ( .s ` M ) I ) e. { I } /\ ( r ( .s ` M ) ( I ( +g ` M ) I ) ) = ( ( r ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( ( q ( .s ` M ) I ) ( +g ` M ) ( r ( .s ` M ) I ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) I ) = I ) ) ) )
90 56 89 mpbird 
 |-  ( ( I e. V /\ R e. Ring ) -> A. q e. ( Base ` ( Scalar ` M ) ) A. r e. ( Base ` ( Scalar ` M ) ) A. x e. { I } A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) x ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) x ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) )
91 1 lmodbase 
 |-  ( { I } e. _V -> { I } = ( Base ` M ) )
92 5 91 ax-mp 
 |-  { I } = ( Base ` M )
93 eqid 
 |-  ( +g ` M ) = ( +g ` M )
94 eqid 
 |-  ( .s ` M ) = ( .s ` M )
95 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
96 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
97 eqid 
 |-  ( +g ` ( Scalar ` M ) ) = ( +g ` ( Scalar ` M ) )
98 eqid 
 |-  ( .r ` ( Scalar ` M ) ) = ( .r ` ( Scalar ` M ) )
99 eqid 
 |-  ( 1r ` ( Scalar ` M ) ) = ( 1r ` ( Scalar ` M ) )
100 92 93 94 95 96 97 98 99 islmod 
 |-  ( M e. LMod <-> ( M e. Grp /\ ( Scalar ` M ) e. Ring /\ A. q e. ( Base ` ( Scalar ` M ) ) A. r e. ( Base ` ( Scalar ` M ) ) A. x e. { I } A. w e. { I } ( ( ( r ( .s ` M ) w ) e. { I } /\ ( r ( .s ` M ) ( w ( +g ` M ) x ) ) = ( ( r ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) x ) ) /\ ( ( q ( +g ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( ( q ( .s ` M ) w ) ( +g ` M ) ( r ( .s ` M ) w ) ) ) /\ ( ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) w ) = ( q ( .s ` M ) ( r ( .s ` M ) w ) ) /\ ( ( 1r ` ( Scalar ` M ) ) ( .s ` M ) w ) = w ) ) ) )
101 30 35 90 100 syl3anbrc 
 |-  ( ( I e. V /\ R e. Ring ) -> M e. LMod )