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

Theorem islmodd 18175
Description: Properties that determine a left module. See note in isgrpd2 16767 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 2550 . 2  |-  ( ph  ->  (Scalar `  W )  e.  Ring )
5 islmodd.w . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  B  /\  y  e.  V
)  ->  ( x  .x.  y )  e.  V
)
653expb 1232 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  V ) )  -> 
( x  .x.  y
)  e.  V )
76ralrimivva 2814 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  B  A. y  e.  V  ( x  .x.  y )  e.  V )
8 oveq1 6315 . . . . . . . . . . . 12  |-  ( x  =  r  ->  (
x  .x.  y )  =  ( r  .x.  y ) )
98eleq1d 2533 . . . . . . . . . . 11  |-  ( x  =  r  ->  (
( x  .x.  y
)  e.  V  <->  ( r  .x.  y )  e.  V
) )
10 oveq2 6316 . . . . . . . . . . . 12  |-  ( y  =  w  ->  (
r  .x.  y )  =  ( r  .x.  w ) )
1110eleq1d 2533 . . . . . . . . . . 11  |-  ( y  =  w  ->  (
( r  .x.  y
)  e.  V  <->  ( r  .x.  w )  e.  V
) )
129, 11rspc2v 3147 . . . . . . . . . 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 760 . . . . . . . . 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 477 . . . . . . . 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 2815 . . . . . . . . 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 6315 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  (
x  .x.  ( y  .+  z ) )  =  ( r  .x.  (
y  .+  z )
) )
18 oveq1 6315 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  (
x  .x.  z )  =  ( r  .x.  z ) )
198, 18oveq12d 6326 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  (
( x  .x.  y
)  .+  ( x  .x.  z ) )  =  ( ( r  .x.  y )  .+  (
r  .x.  z )
) )
2017, 19eqeq12d 2486 . . . . . . . . . . . . 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 6315 . . . . . . . . . . . . . . 15  |-  ( y  =  w  ->  (
y  .+  z )  =  ( w  .+  z ) )
2221oveq2d 6324 . . . . . . . . . . . . . 14  |-  ( y  =  w  ->  (
r  .x.  ( y  .+  z ) )  =  ( r  .x.  (
w  .+  z )
) )
2310oveq1d 6323 . . . . . . . . . . . . . 14  |-  ( y  =  w  ->  (
( r  .x.  y
)  .+  ( r  .x.  z ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  z )
) )
2422, 23eqeq12d 2486 . . . . . . . . . . . . 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 6316 . . . . . . . . . . . . . . 15  |-  ( z  =  u  ->  (
w  .+  z )  =  ( w  .+  u ) )
2625oveq2d 6324 . . . . . . . . . . . . . 14  |-  ( z  =  u  ->  (
r  .x.  ( w  .+  z ) )  =  ( r  .x.  (
w  .+  u )
) )
27 oveq2 6316 . . . . . . . . . . . . . . 15  |-  ( z  =  u  ->  (
r  .x.  z )  =  ( r  .x.  u ) )
2827oveq2d 6324 . . . . . . . . . . . . . 14  |-  ( z  =  u  ->  (
( r  .x.  w
)  .+  ( r  .x.  z ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
) )
2926, 28eqeq12d 2486 . . . . . . . . . . . . 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 3150 . . . . . . . . . . . 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 1237 . . . . . . . . . . 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 1232 . . . . . . . . . 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 728 . . . . . . . . 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 477 . . . . . . . 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 768 . . . . . . . . . 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 1251 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  B  ->  ( y  e.  B  ->  ( z  e.  V  ->  ( ( x  .+^  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) ) ) ) )
3837imp43 606 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  B )  /\  (
y  e.  B  /\  z  e.  V )
)  ->  ( (
x  .+^  y )  .x.  z )  =  ( ( x  .x.  z
)  .+  ( y  .x.  z ) ) )
3938ralrimivva 2814 . . . . . . . . . 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 482 . . . . . . . . 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 781 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
r  e.  B )
42 simprrr 783 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  ->  w  e.  V )
43 oveq2 6316 . . . . . . . . . . . . 13  |-  ( y  =  r  ->  (
x  .+^  y )  =  ( x  .+^  r ) )
4443oveq1d 6323 . . . . . . . . . . . 12  |-  ( y  =  r  ->  (
( x  .+^  y ) 
.x.  z )  =  ( ( x  .+^  r )  .x.  z
) )
45 oveq1 6315 . . . . . . . . . . . . 13  |-  ( y  =  r  ->  (
y  .x.  z )  =  ( r  .x.  z ) )
4645oveq2d 6324 . . . . . . . . . . . 12  |-  ( y  =  r  ->  (
( x  .x.  z
)  .+  ( y  .x.  z ) )  =  ( ( x  .x.  z )  .+  (
r  .x.  z )
) )
4744, 46eqeq12d 2486 . . . . . . . . . . 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 6316 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
( x  .+^  r ) 
.x.  z )  =  ( ( x  .+^  r )  .x.  w
) )
49 oveq2 6316 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
x  .x.  z )  =  ( x  .x.  w ) )
50 oveq2 6316 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
r  .x.  z )  =  ( r  .x.  w ) )
5149, 50oveq12d 6326 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
( x  .x.  z
)  .+  ( r  .x.  z ) )  =  ( ( x  .x.  w )  .+  (
r  .x.  w )
) )
5248, 51eqeq12d 2486 . . . . . . . . . . 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 3147 . . . . . . . . . 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 673 . . . . . . . . 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 15 . . . . . . . 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 1210 . . . . . . 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 1251 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  B  ->  ( y  e.  B  ->  ( z  e.  V  ->  ( ( x  .X.  y )  .x.  z
)  =  ( x 
.x.  ( y  .x.  z ) ) ) ) ) )
5958imp43 606 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  B )  /\  (
y  e.  B  /\  z  e.  V )
)  ->  ( (
x  .X.  y )  .x.  z )  =  ( x  .x.  ( y 
.x.  z ) ) )
6059ralrimivva 2814 . . . . . . . . 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 482 . . . . . . . 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 6316 . . . . . . . . . . . 12  |-  ( y  =  r  ->  (
x  .X.  y )  =  ( x  .X.  r ) )
6362oveq1d 6323 . . . . . . . . . . 11  |-  ( y  =  r  ->  (
( x  .X.  y
)  .x.  z )  =  ( ( x 
.X.  r )  .x.  z ) )
6445oveq2d 6324 . . . . . . . . . . 11  |-  ( y  =  r  ->  (
x  .x.  ( y  .x.  z ) )  =  ( x  .x.  (
r  .x.  z )
) )
6563, 64eqeq12d 2486 . . . . . . . . . 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 6316 . . . . . . . . . . 11  |-  ( z  =  w  ->  (
( x  .X.  r
)  .x.  z )  =  ( ( x 
.X.  r )  .x.  w ) )
6750oveq2d 6324 . . . . . . . . . . 11  |-  ( z  =  w  ->  (
x  .x.  ( r  .x.  z ) )  =  ( x  .x.  (
r  .x.  w )
) )
6866, 67eqeq12d 2486 . . . . . . . . . 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 3147 . . . . . . . . 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 673 . . . . . . . 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 15 . . . . . . 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 2809 . . . . . . . 8  |-  ( ph  ->  A. x  e.  V  (  .1.  .x.  x )  =  x )
74 oveq2 6316 . . . . . . . . . . 11  |-  ( x  =  w  ->  (  .1.  .x.  x )  =  (  .1.  .x.  w
) )
75 id 22 . . . . . . . . . . 11  |-  ( x  =  w  ->  x  =  w )
7674, 75eqeq12d 2486 . . . . . . . . . 10  |-  ( x  =  w  ->  (
(  .1.  .x.  x
)  =  x  <->  (  .1.  .x.  w )  =  w ) )
7776rspcv 3132 . . . . . . . . 9  |-  ( w  e.  V  ->  ( A. x  e.  V  (  .1.  .x.  x )  =  x  ->  (  .1. 
.x.  w )  =  w ) )
7877ad2antll 743 . . . . . . . 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 477 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
(  .1.  .x.  w
)  =  w )
8056, 71, 79jca32 544 . . . . . 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 660 . . . . 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 2814 . . . 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 2814 . . 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 5883 . . . . 5  |-  ( ph  ->  ( Base `  F
)  =  ( Base `  (Scalar `  W )
) )
8684, 85eqtrd 2505 . . . 4  |-  ( ph  ->  B  =  ( Base `  (Scalar `  W )
) )
87 islmodd.v . . . . . 6  |-  ( ph  ->  V  =  ( Base `  W ) )
88 islmodd.s . . . . . . . . . . 11  |-  ( ph  ->  .x.  =  ( .s
`  W ) )
8988oveqd 6325 . . . . . . . . . 10  |-  ( ph  ->  ( r  .x.  w
)  =  ( r ( .s `  W
) w ) )
9089, 87eleq12d 2543 . . . . . . . . 9  |-  ( ph  ->  ( ( r  .x.  w )  e.  V  <->  ( r ( .s `  W ) w )  e.  ( Base `  W
) ) )
91 eqidd 2472 . . . . . . . . . . 11  |-  ( ph  ->  r  =  r )
92 islmodd.a . . . . . . . . . . . 12  |-  ( ph  ->  .+  =  ( +g  `  W ) )
9392oveqd 6325 . . . . . . . . . . 11  |-  ( ph  ->  ( w  .+  u
)  =  ( w ( +g  `  W
) u ) )
9488, 91, 93oveq123d 6329 . . . . . . . . . 10  |-  ( ph  ->  ( r  .x.  (
w  .+  u )
)  =  ( r ( .s `  W
) ( w ( +g  `  W ) u ) ) )
9588oveqd 6325 . . . . . . . . . . 11  |-  ( ph  ->  ( r  .x.  u
)  =  ( r ( .s `  W
) u ) )
9692, 89, 95oveq123d 6329 . . . . . . . . . 10  |-  ( ph  ->  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  =  ( ( r ( .s `  W ) w ) ( +g  `  W
) ( r ( .s `  W ) u ) ) )
9794, 96eqeq12d 2486 . . . . . . . . 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 5883 . . . . . . . . . . . . 13  |-  ( ph  ->  ( +g  `  F
)  =  ( +g  `  (Scalar `  W )
) )
10098, 99eqtrd 2505 . . . . . . . . . . . 12  |-  ( ph  -> 
.+^  =  ( +g  `  (Scalar `  W )
) )
101100oveqd 6325 . . . . . . . . . . 11  |-  ( ph  ->  ( x  .+^  r )  =  ( x ( +g  `  (Scalar `  W ) ) r ) )
102 eqidd 2472 . . . . . . . . . . 11  |-  ( ph  ->  w  =  w )
10388, 101, 102oveq123d 6329 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  .+^  r )  .x.  w
)  =  ( ( x ( +g  `  (Scalar `  W ) ) r ) ( .s `  W ) w ) )
10488oveqd 6325 . . . . . . . . . . 11  |-  ( ph  ->  ( x  .x.  w
)  =  ( x ( .s `  W
) w ) )
10592, 104, 89oveq123d 6329 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  .x.  w )  .+  (
r  .x.  w )
)  =  ( ( x ( .s `  W ) w ) ( +g  `  W
) ( r ( .s `  W ) w ) ) )
106103, 105eqeq12d 2486 . . . . . . . . 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 1365 . . . . . . . 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 5883 . . . . . . . . . . . . 13  |-  ( ph  ->  ( .r `  F
)  =  ( .r
`  (Scalar `  W )
) )
110108, 109eqtrd 2505 . . . . . . . . . . . 12  |-  ( ph  ->  .X.  =  ( .r
`  (Scalar `  W )
) )
111110oveqd 6325 . . . . . . . . . . 11  |-  ( ph  ->  ( x  .X.  r
)  =  ( x ( .r `  (Scalar `  W ) ) r ) )
11288, 111, 102oveq123d 6329 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  .X.  r )  .x.  w
)  =  ( ( x ( .r `  (Scalar `  W ) ) r ) ( .s
`  W ) w ) )
113 eqidd 2472 . . . . . . . . . . 11  |-  ( ph  ->  x  =  x )
11488, 113, 89oveq123d 6329 . . . . . . . . . 10  |-  ( ph  ->  ( x  .x.  (
r  .x.  w )
)  =  ( x ( .s `  W
) ( r ( .s `  W ) w ) ) )
115112, 114eqeq12d 2486 . . . . . . . . 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 5883 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1r `  F
)  =  ( 1r
`  (Scalar `  W )
) )
118116, 117eqtrd 2505 . . . . . . . . . . 11  |-  ( ph  ->  .1.  =  ( 1r
`  (Scalar `  W )
) )
11988, 118, 102oveq123d 6329 . . . . . . . . . 10  |-  ( ph  ->  (  .1.  .x.  w
)  =  ( ( 1r `  (Scalar `  W ) ) ( .s `  W ) w ) )
120119eqeq1d 2473 . . . . . . . . 9  |-  ( ph  ->  ( (  .1.  .x.  w )  =  w  <-> 
( ( 1r `  (Scalar `  W ) ) ( .s `  W
) w )  =  w ) )
121115, 120anbi12d 725 . . . . . . . 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 725 . . . . . . 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 2987 . . . . . 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 2987 . . . . 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 2987 . . . 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 2987 . . 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 215 . 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 2471 . . 3  |-  ( Base `  W )  =  (
Base `  W )
129 eqid 2471 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
130 eqid 2471 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
131 eqid 2471 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
132 eqid 2471 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
133 eqid 2471 . . 3  |-  ( +g  `  (Scalar `  W )
)  =  ( +g  `  (Scalar `  W )
)
134 eqid 2471 . . 3  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
135 eqid 2471 . . 3  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
136128, 129, 130, 131, 132, 133, 134, 135islmod 18173 . 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 1214 1  |-  ( ph  ->  W  e.  LMod )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007    = wceq 1452    e. wcel 1904   A.wral 2756   ` cfv 5589  (class class class)co 6308   Basecbs 15199   +g cplusg 15268   .rcmulr 15269  Scalarcsca 15271   .scvsca 15272   Grpcgrp 16747   1rcur 17813   Ringcrg 17858   LModclmod 18169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-nul 4527
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-iota 5553  df-fv 5597  df-ov 6311  df-lmod 18171
This theorem is referenced by:  islss3  18260  prdslmodd  18270  sralmod  18488  psrlmod  18702  zlmlmod  19171  lduallmodlem  32789  dvalveclem  34664  dvhlveclem  34747  mendlmod  36130
  Copyright terms: Public domain W3C validator