MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islmodd Unicode version

Theorem islmodd 15633
Description: Properties that determine a left module. See note in isgrpd2 14505 regarding the  ph on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014.)
Hypotheses
Ref Expression
islmodd.v  |-  ( ph  ->  V  =  ( Base `  W ) )
islmodd.a  |-  ( ph  ->  .+  =  ( +g  `  W ) )
islmodd.f  |-  ( ph  ->  F  =  (Scalar `  W ) )
islmodd.s  |-  ( ph  ->  .x.  =  ( .s
`  W ) )
islmodd.b  |-  ( ph  ->  B  =  ( Base `  F ) )
islmodd.p  |-  ( ph  -> 
.+^  =  ( +g  `  F ) )
islmodd.t  |-  ( ph  ->  .X.  =  ( .r
`  F ) )
islmodd.u  |-  ( ph  ->  .1.  =  ( 1r
`  F ) )
islmodd.r  |-  ( ph  ->  F  e.  Ring )
islmodd.l  |-  ( ph  ->  W  e.  Grp )
islmodd.w  |-  ( (
ph  /\  x  e.  B  /\  y  e.  V
)  ->  ( x  .x.  y )  e.  V
)
islmodd.c  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  V  /\  z  e.  V ) )  -> 
( x  .x.  (
y  .+  z )
)  =  ( ( x  .x.  y ) 
.+  ( x  .x.  z ) ) )
islmodd.d  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  V ) )  -> 
( ( x  .+^  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )
islmodd.e  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  V ) )  -> 
( ( x  .X.  y )  .x.  z
)  =  ( x 
.x.  ( y  .x.  z ) ) )
islmodd.g  |-  ( (
ph  /\  x  e.  V )  ->  (  .1.  .x.  x )  =  x )
Assertion
Ref Expression
islmodd  |-  ( ph  ->  W  e.  LMod )
Distinct variable groups:    y, z,  .+^    x, y, z, B    ph, x, y, z    x, V, y, z    x,  .+ , y, z   
x, W    x,  .x. , y, z    y,  .X. , z    x,  .1.
Allowed substitution hints:    .+^ ( x)    .X. ( x)    .1. ( y, z)    F( x, y, z)    W( y, z)

Proof of Theorem islmodd
Dummy variables  u  r  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 islmodd.l . 2  |-  ( ph  ->  W  e.  Grp )
2 islmodd.f . . 3  |-  ( ph  ->  F  =  (Scalar `  W ) )
3 islmodd.r . . 3  |-  ( ph  ->  F  e.  Ring )
42, 3eqeltrrd 2358 . 2  |-  ( ph  ->  (Scalar `  W )  e.  Ring )
5 islmodd.w . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  B  /\  y  e.  V
)  ->  ( x  .x.  y )  e.  V
)
653expb 1152 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  V ) )  -> 
( x  .x.  y
)  e.  V )
76ralrimivva 2635 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  B  A. y  e.  V  ( x  .x.  y )  e.  V )
8 oveq1 5865 . . . . . . . . . . . 12  |-  ( x  =  r  ->  (
x  .x.  y )  =  ( r  .x.  y ) )
98eleq1d 2349 . . . . . . . . . . 11  |-  ( x  =  r  ->  (
( x  .x.  y
)  e.  V  <->  ( r  .x.  y )  e.  V
) )
10 oveq2 5866 . . . . . . . . . . . 12  |-  ( y  =  w  ->  (
r  .x.  y )  =  ( r  .x.  w ) )
1110eleq1d 2349 . . . . . . . . . . 11  |-  ( y  =  w  ->  (
( r  .x.  y
)  e.  V  <->  ( r  .x.  w )  e.  V
) )
129, 11rspc2v 2890 . . . . . . . . . 10  |-  ( ( r  e.  B  /\  w  e.  V )  ->  ( A. x  e.  B  A. y  e.  V  ( x  .x.  y )  e.  V  ->  ( r  .x.  w
)  e.  V ) )
1312ad2ant2l 726 . . . . . . . . 9  |-  ( ( ( x  e.  B  /\  r  e.  B
)  /\  ( u  e.  V  /\  w  e.  V ) )  -> 
( A. x  e.  B  A. y  e.  V  ( x  .x.  y )  e.  V  ->  ( r  .x.  w
)  e.  V ) )
147, 13mpan9 455 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
( r  .x.  w
)  e.  V )
15 islmodd.c . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  V  /\  z  e.  V ) )  -> 
( x  .x.  (
y  .+  z )
)  =  ( ( x  .x.  y ) 
.+  ( x  .x.  z ) ) )
1615ralrimivvva 2636 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  B  A. y  e.  V  A. z  e.  V  ( x  .x.  ( y 
.+  z ) )  =  ( ( x 
.x.  y )  .+  ( x  .x.  z ) ) )
17 oveq1 5865 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  (
x  .x.  ( y  .+  z ) )  =  ( r  .x.  (
y  .+  z )
) )
18 oveq1 5865 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  (
x  .x.  z )  =  ( r  .x.  z ) )
198, 18oveq12d 5876 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  (
( x  .x.  y
)  .+  ( x  .x.  z ) )  =  ( ( r  .x.  y )  .+  (
r  .x.  z )
) )
2017, 19eqeq12d 2297 . . . . . . . . . . . . 13  |-  ( x  =  r  ->  (
( x  .x.  (
y  .+  z )
)  =  ( ( x  .x.  y ) 
.+  ( x  .x.  z ) )  <->  ( r  .x.  ( y  .+  z
) )  =  ( ( r  .x.  y
)  .+  ( r  .x.  z ) ) ) )
21 oveq1 5865 . . . . . . . . . . . . . . 15  |-  ( y  =  w  ->  (
y  .+  z )  =  ( w  .+  z ) )
2221oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( y  =  w  ->  (
r  .x.  ( y  .+  z ) )  =  ( r  .x.  (
w  .+  z )
) )
2310oveq1d 5873 . . . . . . . . . . . . . 14  |-  ( y  =  w  ->  (
( r  .x.  y
)  .+  ( r  .x.  z ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  z )
) )
2422, 23eqeq12d 2297 . . . . . . . . . . . . 13  |-  ( y  =  w  ->  (
( r  .x.  (
y  .+  z )
)  =  ( ( r  .x.  y ) 
.+  ( r  .x.  z ) )  <->  ( r  .x.  ( w  .+  z
) )  =  ( ( r  .x.  w
)  .+  ( r  .x.  z ) ) ) )
25 oveq2 5866 . . . . . . . . . . . . . . 15  |-  ( z  =  u  ->  (
w  .+  z )  =  ( w  .+  u ) )
2625oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( z  =  u  ->  (
r  .x.  ( w  .+  z ) )  =  ( r  .x.  (
w  .+  u )
) )
27 oveq2 5866 . . . . . . . . . . . . . . 15  |-  ( z  =  u  ->  (
r  .x.  z )  =  ( r  .x.  u ) )
2827oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( z  =  u  ->  (
( r  .x.  w
)  .+  ( r  .x.  z ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
) )
2926, 28eqeq12d 2297 . . . . . . . . . . . . 13  |-  ( z  =  u  ->  (
( r  .x.  (
w  .+  z )
)  =  ( ( r  .x.  w ) 
.+  ( r  .x.  z ) )  <->  ( r  .x.  ( w  .+  u
) )  =  ( ( r  .x.  w
)  .+  ( r  .x.  u ) ) ) )
3020, 24, 29rspc3v 2893 . . . . . . . . . . . 12  |-  ( ( r  e.  B  /\  w  e.  V  /\  u  e.  V )  ->  ( A. x  e.  B  A. y  e.  V  A. z  e.  V  ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  -> 
( r  .x.  (
w  .+  u )
)  =  ( ( r  .x.  w ) 
.+  ( r  .x.  u ) ) ) )
31303com23 1157 . . . . . . . . . . 11  |-  ( ( r  e.  B  /\  u  e.  V  /\  w  e.  V )  ->  ( A. x  e.  B  A. y  e.  V  A. z  e.  V  ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  -> 
( r  .x.  (
w  .+  u )
)  =  ( ( r  .x.  w ) 
.+  ( r  .x.  u ) ) ) )
32313expb 1152 . . . . . . . . . 10  |-  ( ( r  e.  B  /\  ( u  e.  V  /\  w  e.  V
) )  ->  ( A. x  e.  B  A. y  e.  V  A. z  e.  V  ( x  .x.  ( y 
.+  z ) )  =  ( ( x 
.x.  y )  .+  ( x  .x.  z ) )  ->  ( r  .x.  ( w  .+  u
) )  =  ( ( r  .x.  w
)  .+  ( r  .x.  u ) ) ) )
3332adantll 694 . . . . . . . . 9  |-  ( ( ( x  e.  B  /\  r  e.  B
)  /\  ( u  e.  V  /\  w  e.  V ) )  -> 
( A. x  e.  B  A. y  e.  V  A. z  e.  V  ( x  .x.  ( y  .+  z
) )  =  ( ( x  .x.  y
)  .+  ( x  .x.  z ) )  -> 
( r  .x.  (
w  .+  u )
)  =  ( ( r  .x.  w ) 
.+  ( r  .x.  u ) ) ) )
3416, 33mpan9 455 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
( r  .x.  (
w  .+  u )
)  =  ( ( r  .x.  w ) 
.+  ( r  .x.  u ) ) )
35 simpll 730 . . . . . . . . . 10  |-  ( ( ( x  e.  B  /\  r  e.  B
)  /\  ( u  e.  V  /\  w  e.  V ) )  ->  x  e.  B )
36 islmodd.d . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  V ) )  -> 
( ( x  .+^  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )
37363exp2 1169 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  B  ->  ( y  e.  B  ->  ( z  e.  V  ->  ( ( x  .+^  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) ) ) ) )
3837imp43 578 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  B )  /\  (
y  e.  B  /\  z  e.  V )
)  ->  ( (
x  .+^  y )  .x.  z )  =  ( ( x  .x.  z
)  .+  ( y  .x.  z ) ) )
3938ralrimivva 2635 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  B )  ->  A. y  e.  B  A. z  e.  V  ( (
x  .+^  y )  .x.  z )  =  ( ( x  .x.  z
)  .+  ( y  .x.  z ) ) )
4035, 39sylan2 460 . . . . . . . . 9  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  ->  A. y  e.  B  A. z  e.  V  ( ( x  .+^  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) )
41 simprlr 739 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
r  e.  B )
42 simprrr 741 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  ->  w  e.  V )
43 oveq2 5866 . . . . . . . . . . . . 13  |-  ( y  =  r  ->  (
x  .+^  y )  =  ( x  .+^  r ) )
4443oveq1d 5873 . . . . . . . . . . . 12  |-  ( y  =  r  ->  (
( x  .+^  y ) 
.x.  z )  =  ( ( x  .+^  r )  .x.  z
) )
45 oveq1 5865 . . . . . . . . . . . . 13  |-  ( y  =  r  ->  (
y  .x.  z )  =  ( r  .x.  z ) )
4645oveq2d 5874 . . . . . . . . . . . 12  |-  ( y  =  r  ->  (
( x  .x.  z
)  .+  ( y  .x.  z ) )  =  ( ( x  .x.  z )  .+  (
r  .x.  z )
) )
4744, 46eqeq12d 2297 . . . . . . . . . . 11  |-  ( y  =  r  ->  (
( ( x  .+^  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) )  <->  ( (
x  .+^  r )  .x.  z )  =  ( ( x  .x.  z
)  .+  ( r  .x.  z ) ) ) )
48 oveq2 5866 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
( x  .+^  r ) 
.x.  z )  =  ( ( x  .+^  r )  .x.  w
) )
49 oveq2 5866 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
x  .x.  z )  =  ( x  .x.  w ) )
50 oveq2 5866 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
r  .x.  z )  =  ( r  .x.  w ) )
5149, 50oveq12d 5876 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
( x  .x.  z
)  .+  ( r  .x.  z ) )  =  ( ( x  .x.  w )  .+  (
r  .x.  w )
) )
5248, 51eqeq12d 2297 . . . . . . . . . . 11  |-  ( z  =  w  ->  (
( ( x  .+^  r )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( r  .x.  z ) )  <->  ( (
x  .+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) ) ) )
5347, 52rspc2v 2890 . . . . . . . . . 10  |-  ( ( r  e.  B  /\  w  e.  V )  ->  ( A. y  e.  B  A. z  e.  V  ( ( x 
.+^  y )  .x.  z )  =  ( ( x  .x.  z
)  .+  ( y  .x.  z ) )  -> 
( ( x  .+^  r )  .x.  w
)  =  ( ( x  .x.  w ) 
.+  ( r  .x.  w ) ) ) )
5441, 42, 53syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
( A. y  e.  B  A. z  e.  V  ( ( x 
.+^  y )  .x.  z )  =  ( ( x  .x.  z
)  .+  ( y  .x.  z ) )  -> 
( ( x  .+^  r )  .x.  w
)  =  ( ( x  .x.  w ) 
.+  ( r  .x.  w ) ) ) )
5540, 54mpd 14 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
( ( x  .+^  r )  .x.  w
)  =  ( ( x  .x.  w ) 
.+  ( r  .x.  w ) ) )
5614, 34, 553jca 1132 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
( ( r  .x.  w )  e.  V  /\  ( r  .x.  (
w  .+  u )
)  =  ( ( r  .x.  w ) 
.+  ( r  .x.  u ) )  /\  ( ( x  .+^  r )  .x.  w
)  =  ( ( x  .x.  w ) 
.+  ( r  .x.  w ) ) ) )
57 islmodd.e . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  V ) )  -> 
( ( x  .X.  y )  .x.  z
)  =  ( x 
.x.  ( y  .x.  z ) ) )
58573exp2 1169 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  B  ->  ( y  e.  B  ->  ( z  e.  V  ->  ( ( x  .X.  y )  .x.  z
)  =  ( x 
.x.  ( y  .x.  z ) ) ) ) ) )
5958imp43 578 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  B )  /\  (
y  e.  B  /\  z  e.  V )
)  ->  ( (
x  .X.  y )  .x.  z )  =  ( x  .x.  ( y 
.x.  z ) ) )
6059ralrimivva 2635 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  B )  ->  A. y  e.  B  A. z  e.  V  ( (
x  .X.  y )  .x.  z )  =  ( x  .x.  ( y 
.x.  z ) ) )
6135, 60sylan2 460 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  ->  A. y  e.  B  A. z  e.  V  ( ( x  .X.  y )  .x.  z
)  =  ( x 
.x.  ( y  .x.  z ) ) )
62 oveq2 5866 . . . . . . . . . . . 12  |-  ( y  =  r  ->  (
x  .X.  y )  =  ( x  .X.  r ) )
6362oveq1d 5873 . . . . . . . . . . 11  |-  ( y  =  r  ->  (
( x  .X.  y
)  .x.  z )  =  ( ( x 
.X.  r )  .x.  z ) )
6445oveq2d 5874 . . . . . . . . . . 11  |-  ( y  =  r  ->  (
x  .x.  ( y  .x.  z ) )  =  ( x  .x.  (
r  .x.  z )
) )
6563, 64eqeq12d 2297 . . . . . . . . . 10  |-  ( y  =  r  ->  (
( ( x  .X.  y )  .x.  z
)  =  ( x 
.x.  ( y  .x.  z ) )  <->  ( (
x  .X.  r )  .x.  z )  =  ( x  .x.  ( r 
.x.  z ) ) ) )
66 oveq2 5866 . . . . . . . . . . 11  |-  ( z  =  w  ->  (
( x  .X.  r
)  .x.  z )  =  ( ( x 
.X.  r )  .x.  w ) )
6750oveq2d 5874 . . . . . . . . . . 11  |-  ( z  =  w  ->  (
x  .x.  ( r  .x.  z ) )  =  ( x  .x.  (
r  .x.  w )
) )
6866, 67eqeq12d 2297 . . . . . . . . . 10  |-  ( z  =  w  ->  (
( ( x  .X.  r )  .x.  z
)  =  ( x 
.x.  ( r  .x.  z ) )  <->  ( (
x  .X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) ) ) )
6965, 68rspc2v 2890 . . . . . . . . 9  |-  ( ( r  e.  B  /\  w  e.  V )  ->  ( A. y  e.  B  A. z  e.  V  ( ( x 
.X.  y )  .x.  z )  =  ( x  .x.  ( y 
.x.  z ) )  ->  ( ( x 
.X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) ) ) )
7041, 42, 69syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
( A. y  e.  B  A. z  e.  V  ( ( x 
.X.  y )  .x.  z )  =  ( x  .x.  ( y 
.x.  z ) )  ->  ( ( x 
.X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) ) ) )
7161, 70mpd 14 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
( ( x  .X.  r )  .x.  w
)  =  ( x 
.x.  ( r  .x.  w ) ) )
72 islmodd.g . . . . . . . . 9  |-  ( (
ph  /\  x  e.  V )  ->  (  .1.  .x.  x )  =  x )
7372ralrimiva 2626 . . . . . . . 8  |-  ( ph  ->  A. x  e.  V  (  .1.  .x.  x )  =  x )
74 oveq2 5866 . . . . . . . . . . 11  |-  ( x  =  w  ->  (  .1.  .x.  x )  =  (  .1.  .x.  w
) )
75 id 19 . . . . . . . . . . 11  |-  ( x  =  w  ->  x  =  w )
7674, 75eqeq12d 2297 . . . . . . . . . 10  |-  ( x  =  w  ->  (
(  .1.  .x.  x
)  =  x  <->  (  .1.  .x.  w )  =  w ) )
7776rspcv 2880 . . . . . . . . 9  |-  ( w  e.  V  ->  ( A. x  e.  V  (  .1.  .x.  x )  =  x  ->  (  .1. 
.x.  w )  =  w ) )
7877ad2antll 709 . . . . . . . 8  |-  ( ( ( x  e.  B  /\  r  e.  B
)  /\  ( u  e.  V  /\  w  e.  V ) )  -> 
( A. x  e.  V  (  .1.  .x.  x )  =  x  ->  (  .1.  .x.  w )  =  w ) )
7973, 78mpan9 455 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
(  .1.  .x.  w
)  =  w )
8056, 71, 79jca32 521 . . . . . 6  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
( ( ( r 
.x.  w )  e.  V  /\  ( r 
.x.  ( w  .+  u ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  /\  ( (
x  .+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) ) )  /\  ( ( ( x  .X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) )  /\  (  .1.  .x.  w )  =  w ) ) )
8180anassrs 629 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  B  /\  r  e.  B )
)  /\  ( u  e.  V  /\  w  e.  V ) )  -> 
( ( ( r 
.x.  w )  e.  V  /\  ( r 
.x.  ( w  .+  u ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  /\  ( (
x  .+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) ) )  /\  ( ( ( x  .X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) )  /\  (  .1.  .x.  w )  =  w ) ) )
8281ralrimivva 2635 . . . 4  |-  ( (
ph  /\  ( x  e.  B  /\  r  e.  B ) )  ->  A. u  e.  V  A. w  e.  V  ( ( ( r 
.x.  w )  e.  V  /\  ( r 
.x.  ( w  .+  u ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  /\  ( (
x  .+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) ) )  /\  ( ( ( x  .X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) )  /\  (  .1.  .x.  w )  =  w ) ) )
8382ralrimivva 2635 . . 3  |-  ( ph  ->  A. x  e.  B  A. r  e.  B  A. u  e.  V  A. w  e.  V  ( ( ( r 
.x.  w )  e.  V  /\  ( r 
.x.  ( w  .+  u ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  /\  ( (
x  .+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) ) )  /\  ( ( ( x  .X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) )  /\  (  .1.  .x.  w )  =  w ) ) )
84 islmodd.b . . . . 5  |-  ( ph  ->  B  =  ( Base `  F ) )
852fveq2d 5529 . . . . 5  |-  ( ph  ->  ( Base `  F
)  =  ( Base `  (Scalar `  W )
) )
8684, 85eqtrd 2315 . . . 4  |-  ( ph  ->  B  =  ( Base `  (Scalar `  W )
) )
87 islmodd.v . . . . . 6  |-  ( ph  ->  V  =  ( Base `  W ) )
88 islmodd.s . . . . . . . . . . 11  |-  ( ph  ->  .x.  =  ( .s
`  W ) )
8988oveqd 5875 . . . . . . . . . 10  |-  ( ph  ->  ( r  .x.  w
)  =  ( r ( .s `  W
) w ) )
9089, 87eleq12d 2351 . . . . . . . . 9  |-  ( ph  ->  ( ( r  .x.  w )  e.  V  <->  ( r ( .s `  W ) w )  e.  ( Base `  W
) ) )
91 eqidd 2284 . . . . . . . . . . 11  |-  ( ph  ->  r  =  r )
92 islmodd.a . . . . . . . . . . . 12  |-  ( ph  ->  .+  =  ( +g  `  W ) )
9392oveqd 5875 . . . . . . . . . . 11  |-  ( ph  ->  ( w  .+  u
)  =  ( w ( +g  `  W
) u ) )
9488, 91, 93oveq123d 5879 . . . . . . . . . 10  |-  ( ph  ->  ( r  .x.  (
w  .+  u )
)  =  ( r ( .s `  W
) ( w ( +g  `  W ) u ) ) )
9588oveqd 5875 . . . . . . . . . . 11  |-  ( ph  ->  ( r  .x.  u
)  =  ( r ( .s `  W
) u ) )
9692, 89, 95oveq123d 5879 . . . . . . . . . 10  |-  ( ph  ->  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  =  ( ( r ( .s `  W ) w ) ( +g  `  W
) ( r ( .s `  W ) u ) ) )
9794, 96eqeq12d 2297 . . . . . . . . 9  |-  ( ph  ->  ( ( r  .x.  ( w  .+  u ) )  =  ( ( r  .x.  w ) 
.+  ( r  .x.  u ) )  <->  ( r
( .s `  W
) ( w ( +g  `  W ) u ) )  =  ( ( r ( .s `  W ) w ) ( +g  `  W ) ( r ( .s `  W
) u ) ) ) )
98 islmodd.p . . . . . . . . . . . . 13  |-  ( ph  -> 
.+^  =  ( +g  `  F ) )
992fveq2d 5529 . . . . . . . . . . . . 13  |-  ( ph  ->  ( +g  `  F
)  =  ( +g  `  (Scalar `  W )
) )
10098, 99eqtrd 2315 . . . . . . . . . . . 12  |-  ( ph  -> 
.+^  =  ( +g  `  (Scalar `  W )
) )
101100oveqd 5875 . . . . . . . . . . 11  |-  ( ph  ->  ( x  .+^  r )  =  ( x ( +g  `  (Scalar `  W ) ) r ) )
102 eqidd 2284 . . . . . . . . . . 11  |-  ( ph  ->  w  =  w )
10388, 101, 102oveq123d 5879 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  .+^  r )  .x.  w
)  =  ( ( x ( +g  `  (Scalar `  W ) ) r ) ( .s `  W ) w ) )
10488oveqd 5875 . . . . . . . . . . 11  |-  ( ph  ->  ( x  .x.  w
)  =  ( x ( .s `  W
) w ) )
10592, 104, 89oveq123d 5879 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  .x.  w )  .+  (
r  .x.  w )
)  =  ( ( x ( .s `  W ) w ) ( +g  `  W
) ( r ( .s `  W ) w ) ) )
106103, 105eqeq12d 2297 . . . . . . . . 9  |-  ( ph  ->  ( ( ( x 
.+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) )  <->  ( (
x ( +g  `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( ( x ( .s `  W
) w ) ( +g  `  W ) ( r ( .s
`  W ) w ) ) ) )
10790, 97, 1063anbi123d 1252 . . . . . . . 8  |-  ( ph  ->  ( ( ( r 
.x.  w )  e.  V  /\  ( r 
.x.  ( w  .+  u ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  /\  ( (
x  .+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) ) )  <-> 
( ( r ( .s `  W ) w )  e.  (
Base `  W )  /\  ( r ( .s
`  W ) ( w ( +g  `  W
) u ) )  =  ( ( r ( .s `  W
) w ) ( +g  `  W ) ( r ( .s
`  W ) u ) )  /\  (
( x ( +g  `  (Scalar `  W )
) r ) ( .s `  W ) w )  =  ( ( x ( .s
`  W ) w ) ( +g  `  W
) ( r ( .s `  W ) w ) ) ) ) )
108 islmodd.t . . . . . . . . . . . . 13  |-  ( ph  ->  .X.  =  ( .r
`  F ) )
1092fveq2d 5529 . . . . . . . . . . . . 13  |-  ( ph  ->  ( .r `  F
)  =  ( .r
`  (Scalar `  W )
) )
110108, 109eqtrd 2315 . . . . . . . . . . . 12  |-  ( ph  ->  .X.  =  ( .r
`  (Scalar `  W )
) )
111110oveqd 5875 . . . . . . . . . . 11  |-  ( ph  ->  ( x  .X.  r
)  =  ( x ( .r `  (Scalar `  W ) ) r ) )
11288, 111, 102oveq123d 5879 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  .X.  r )  .x.  w
)  =  ( ( x ( .r `  (Scalar `  W ) ) r ) ( .s
`  W ) w ) )
113 eqidd 2284 . . . . . . . . . . 11  |-  ( ph  ->  x  =  x )
11488, 113, 89oveq123d 5879 . . . . . . . . . 10  |-  ( ph  ->  ( x  .x.  (
r  .x.  w )
)  =  ( x ( .s `  W
) ( r ( .s `  W ) w ) ) )
115112, 114eqeq12d 2297 . . . . . . . . 9  |-  ( ph  ->  ( ( ( x 
.X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) )  <-> 
( ( x ( .r `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( x ( .s `  W ) ( r ( .s
`  W ) w ) ) ) )
116 islmodd.u . . . . . . . . . . . 12  |-  ( ph  ->  .1.  =  ( 1r
`  F ) )
1172fveq2d 5529 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1r `  F
)  =  ( 1r
`  (Scalar `  W )
) )
118116, 117eqtrd 2315 . . . . . . . . . . 11  |-  ( ph  ->  .1.  =  ( 1r
`  (Scalar `  W )
) )
11988, 118, 102oveq123d 5879 . . . . . . . . . 10  |-  ( ph  ->  (  .1.  .x.  w
)  =  ( ( 1r `  (Scalar `  W ) ) ( .s `  W ) w ) )
120119eqeq1d 2291 . . . . . . . . 9  |-  ( ph  ->  ( (  .1.  .x.  w )  =  w  <-> 
( ( 1r `  (Scalar `  W ) ) ( .s `  W
) w )  =  w ) )
121115, 120anbi12d 691 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( x  .X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) )  /\  (  .1.  .x.  w )  =  w )  <->  ( ( ( x ( .r `  (Scalar `  W ) ) r ) ( .s
`  W ) w )  =  ( x ( .s `  W
) ( r ( .s `  W ) w ) )  /\  ( ( 1r `  (Scalar `  W ) ) ( .s `  W
) w )  =  w ) ) )
122107, 121anbi12d 691 . . . . . . 7  |-  ( ph  ->  ( ( ( ( r  .x.  w )  e.  V  /\  (
r  .x.  ( w  .+  u ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  /\  ( (
x  .+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) ) )  /\  ( ( ( x  .X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) )  /\  (  .1.  .x.  w )  =  w ) )  <->  ( (
( r ( .s
`  W ) w )  e.  ( Base `  W )  /\  (
r ( .s `  W ) ( w ( +g  `  W
) u ) )  =  ( ( r ( .s `  W
) w ) ( +g  `  W ) ( r ( .s
`  W ) u ) )  /\  (
( x ( +g  `  (Scalar `  W )
) r ) ( .s `  W ) w )  =  ( ( x ( .s
`  W ) w ) ( +g  `  W
) ( r ( .s `  W ) w ) ) )  /\  ( ( ( x ( .r `  (Scalar `  W ) ) r ) ( .s
`  W ) w )  =  ( x ( .s `  W
) ( r ( .s `  W ) w ) )  /\  ( ( 1r `  (Scalar `  W ) ) ( .s `  W
) w )  =  w ) ) ) )
12387, 122raleqbidv 2748 . . . . . 6  |-  ( ph  ->  ( A. w  e.  V  ( ( ( r  .x.  w )  e.  V  /\  (
r  .x.  ( w  .+  u ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  /\  ( (
x  .+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) ) )  /\  ( ( ( x  .X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) )  /\  (  .1.  .x.  w )  =  w ) )  <->  A. w  e.  ( Base `  W
) ( ( ( r ( .s `  W ) w )  e.  ( Base `  W
)  /\  ( r
( .s `  W
) ( w ( +g  `  W ) u ) )  =  ( ( r ( .s `  W ) w ) ( +g  `  W ) ( r ( .s `  W
) u ) )  /\  ( ( x ( +g  `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( ( x ( .s `  W
) w ) ( +g  `  W ) ( r ( .s
`  W ) w ) ) )  /\  ( ( ( x ( .r `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( x ( .s `  W ) ( r ( .s
`  W ) w ) )  /\  (
( 1r `  (Scalar `  W ) ) ( .s `  W ) w )  =  w ) ) ) )
12487, 123raleqbidv 2748 . . . . 5  |-  ( ph  ->  ( A. u  e.  V  A. w  e.  V  ( ( ( r  .x.  w )  e.  V  /\  (
r  .x.  ( w  .+  u ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  /\  ( (
x  .+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) ) )  /\  ( ( ( x  .X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) )  /\  (  .1.  .x.  w )  =  w ) )  <->  A. u  e.  ( Base `  W
) A. w  e.  ( Base `  W
) ( ( ( r ( .s `  W ) w )  e.  ( Base `  W
)  /\  ( r
( .s `  W
) ( w ( +g  `  W ) u ) )  =  ( ( r ( .s `  W ) w ) ( +g  `  W ) ( r ( .s `  W
) u ) )  /\  ( ( x ( +g  `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( ( x ( .s `  W
) w ) ( +g  `  W ) ( r ( .s
`  W ) w ) ) )  /\  ( ( ( x ( .r `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( x ( .s `  W ) ( r ( .s
`  W ) w ) )  /\  (
( 1r `  (Scalar `  W ) ) ( .s `  W ) w )  =  w ) ) ) )
12586, 124raleqbidv 2748 . . . 4  |-  ( ph  ->  ( A. r  e.  B  A. u  e.  V  A. w  e.  V  ( ( ( r  .x.  w )  e.  V  /\  (
r  .x.  ( w  .+  u ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  /\  ( (
x  .+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) ) )  /\  ( ( ( x  .X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) )  /\  (  .1.  .x.  w )  =  w ) )  <->  A. r  e.  ( Base `  (Scalar `  W ) ) A. u  e.  ( Base `  W ) A. w  e.  ( Base `  W
) ( ( ( r ( .s `  W ) w )  e.  ( Base `  W
)  /\  ( r
( .s `  W
) ( w ( +g  `  W ) u ) )  =  ( ( r ( .s `  W ) w ) ( +g  `  W ) ( r ( .s `  W
) u ) )  /\  ( ( x ( +g  `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( ( x ( .s `  W
) w ) ( +g  `  W ) ( r ( .s
`  W ) w ) ) )  /\  ( ( ( x ( .r `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( x ( .s `  W ) ( r ( .s
`  W ) w ) )  /\  (
( 1r `  (Scalar `  W ) ) ( .s `  W ) w )  =  w ) ) ) )
12686, 125raleqbidv 2748 . . 3  |-  ( ph  ->  ( A. x  e.  B  A. r  e.  B  A. u  e.  V  A. w  e.  V  ( ( ( r  .x.  w )  e.  V  /\  (
r  .x.  ( w  .+  u ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  /\  ( (
x  .+^  r )  .x.  w )  =  ( ( x  .x.  w
)  .+  ( r  .x.  w ) ) )  /\  ( ( ( x  .X.  r )  .x.  w )  =  ( x  .x.  ( r 
.x.  w ) )  /\  (  .1.  .x.  w )  =  w ) )  <->  A. x  e.  ( Base `  (Scalar `  W ) ) A. r  e.  ( Base `  (Scalar `  W )
) A. u  e.  ( Base `  W
) A. w  e.  ( Base `  W
) ( ( ( r ( .s `  W ) w )  e.  ( Base `  W
)  /\  ( r
( .s `  W
) ( w ( +g  `  W ) u ) )  =  ( ( r ( .s `  W ) w ) ( +g  `  W ) ( r ( .s `  W
) u ) )  /\  ( ( x ( +g  `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( ( x ( .s `  W
) w ) ( +g  `  W ) ( r ( .s
`  W ) w ) ) )  /\  ( ( ( x ( .r `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( x ( .s `  W ) ( r ( .s
`  W ) w ) )  /\  (
( 1r `  (Scalar `  W ) ) ( .s `  W ) w )  =  w ) ) ) )
12783, 126mpbid 201 . 2  |-  ( ph  ->  A. x  e.  (
Base `  (Scalar `  W
) ) A. r  e.  ( Base `  (Scalar `  W ) ) A. u  e.  ( Base `  W ) A. w  e.  ( Base `  W
) ( ( ( r ( .s `  W ) w )  e.  ( Base `  W
)  /\  ( r
( .s `  W
) ( w ( +g  `  W ) u ) )  =  ( ( r ( .s `  W ) w ) ( +g  `  W ) ( r ( .s `  W
) u ) )  /\  ( ( x ( +g  `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( ( x ( .s `  W
) w ) ( +g  `  W ) ( r ( .s
`  W ) w ) ) )  /\  ( ( ( x ( .r `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( x ( .s `  W ) ( r ( .s
`  W ) w ) )  /\  (
( 1r `  (Scalar `  W ) ) ( .s `  W ) w )  =  w ) ) )
128 eqid 2283 . . 3  |-  ( Base `  W )  =  (
Base `  W )
129 eqid 2283 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
130 eqid 2283 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
131 eqid 2283 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
132 eqid 2283 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
133 eqid 2283 . . 3  |-  ( +g  `  (Scalar `  W )
)  =  ( +g  `  (Scalar `  W )
)
134 eqid 2283 . . 3  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
135 eqid 2283 . . 3  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
136128, 129, 130, 131, 132, 133, 134, 135islmod 15631 . 2  |-  ( W  e.  LMod  <->  ( W  e. 
Grp  /\  (Scalar `  W
)  e.  Ring  /\  A. x  e.  ( Base `  (Scalar `  W )
) A. r  e.  ( Base `  (Scalar `  W ) ) A. u  e.  ( Base `  W ) A. w  e.  ( Base `  W
) ( ( ( r ( .s `  W ) w )  e.  ( Base `  W
)  /\  ( r
( .s `  W
) ( w ( +g  `  W ) u ) )  =  ( ( r ( .s `  W ) w ) ( +g  `  W ) ( r ( .s `  W
) u ) )  /\  ( ( x ( +g  `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( ( x ( .s `  W
) w ) ( +g  `  W ) ( r ( .s
`  W ) w ) ) )  /\  ( ( ( x ( .r `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( x ( .s `  W ) ( r ( .s
`  W ) w ) )  /\  (
( 1r `  (Scalar `  W ) ) ( .s `  W ) w )  =  w ) ) ) )
1371, 4, 127, 136syl3anbrc 1136 1  |-  ( ph  ->  W  e.  LMod )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   A.wral 2543   ` cfv 5255  (class class class)co 5858   Basecbs 13148   +g cplusg 13208   .rcmulr 13209  Scalarcsca 13211   .scvsca 13212   Grpcgrp 14362   Ringcrg 15337   1rcur 15339   LModclmod 15627
This theorem is referenced by:  islss3  15716  prdslmodd  15726  sralmod  15939  psrlmod  16146  zlmlmod  16477  mendlmod  27501  lduallmodlem  29342  dvalveclem  31215  dvhlveclem  31298
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-lmod 15629
  Copyright terms: Public domain W3C validator