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

Theorem islmodd 15946
Description: Properties that determine a left module. See note in isgrpd2 14818 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 2510 . 2  |-  ( ph  ->  (Scalar `  W )  e.  Ring )
5 islmodd.w . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  B  /\  y  e.  V
)  ->  ( x  .x.  y )  e.  V
)
653expb 1154 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  V ) )  -> 
( x  .x.  y
)  e.  V )
76ralrimivva 2790 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  B  A. y  e.  V  ( x  .x.  y )  e.  V )
8 oveq1 6080 . . . . . . . . . . . 12  |-  ( x  =  r  ->  (
x  .x.  y )  =  ( r  .x.  y ) )
98eleq1d 2501 . . . . . . . . . . 11  |-  ( x  =  r  ->  (
( x  .x.  y
)  e.  V  <->  ( r  .x.  y )  e.  V
) )
10 oveq2 6081 . . . . . . . . . . . 12  |-  ( y  =  w  ->  (
r  .x.  y )  =  ( r  .x.  w ) )
1110eleq1d 2501 . . . . . . . . . . 11  |-  ( y  =  w  ->  (
( r  .x.  y
)  e.  V  <->  ( r  .x.  w )  e.  V
) )
129, 11rspc2v 3050 . . . . . . . . . 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 727 . . . . . . . . 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 456 . . . . . . . 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 2791 . . . . . . . . 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 6080 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  (
x  .x.  ( y  .+  z ) )  =  ( r  .x.  (
y  .+  z )
) )
18 oveq1 6080 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  (
x  .x.  z )  =  ( r  .x.  z ) )
198, 18oveq12d 6091 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  (
( x  .x.  y
)  .+  ( x  .x.  z ) )  =  ( ( r  .x.  y )  .+  (
r  .x.  z )
) )
2017, 19eqeq12d 2449 . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . 15  |-  ( y  =  w  ->  (
y  .+  z )  =  ( w  .+  z ) )
2221oveq2d 6089 . . . . . . . . . . . . . 14  |-  ( y  =  w  ->  (
r  .x.  ( y  .+  z ) )  =  ( r  .x.  (
w  .+  z )
) )
2310oveq1d 6088 . . . . . . . . . . . . . 14  |-  ( y  =  w  ->  (
( r  .x.  y
)  .+  ( r  .x.  z ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  z )
) )
2422, 23eqeq12d 2449 . . . . . . . . . . . . 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 6081 . . . . . . . . . . . . . . 15  |-  ( z  =  u  ->  (
w  .+  z )  =  ( w  .+  u ) )
2625oveq2d 6089 . . . . . . . . . . . . . 14  |-  ( z  =  u  ->  (
r  .x.  ( w  .+  z ) )  =  ( r  .x.  (
w  .+  u )
) )
27 oveq2 6081 . . . . . . . . . . . . . . 15  |-  ( z  =  u  ->  (
r  .x.  z )  =  ( r  .x.  u ) )
2827oveq2d 6089 . . . . . . . . . . . . . 14  |-  ( z  =  u  ->  (
( r  .x.  w
)  .+  ( r  .x.  z ) )  =  ( ( r  .x.  w )  .+  (
r  .x.  u )
) )
2926, 28eqeq12d 2449 . . . . . . . . . . . . 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 3053 . . . . . . . . . . . 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 1159 . . . . . . . . . . 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 1154 . . . . . . . . . 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 695 . . . . . . . . 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 456 . . . . . . . 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 731 . . . . . . . . . 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 1171 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  B  ->  ( y  e.  B  ->  ( z  e.  V  ->  ( ( x  .+^  y )  .x.  z
)  =  ( ( x  .x.  z ) 
.+  ( y  .x.  z ) ) ) ) ) )
3837imp43 579 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  B )  /\  (
y  e.  B  /\  z  e.  V )
)  ->  ( (
x  .+^  y )  .x.  z )  =  ( ( x  .x.  z
)  .+  ( y  .x.  z ) ) )
3938ralrimivva 2790 . . . . . . . . . 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 461 . . . . . . . . 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 740 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
r  e.  B )
42 simprrr 742 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  ->  w  e.  V )
43 oveq2 6081 . . . . . . . . . . . . 13  |-  ( y  =  r  ->  (
x  .+^  y )  =  ( x  .+^  r ) )
4443oveq1d 6088 . . . . . . . . . . . 12  |-  ( y  =  r  ->  (
( x  .+^  y ) 
.x.  z )  =  ( ( x  .+^  r )  .x.  z
) )
45 oveq1 6080 . . . . . . . . . . . . 13  |-  ( y  =  r  ->  (
y  .x.  z )  =  ( r  .x.  z ) )
4645oveq2d 6089 . . . . . . . . . . . 12  |-  ( y  =  r  ->  (
( x  .x.  z
)  .+  ( y  .x.  z ) )  =  ( ( x  .x.  z )  .+  (
r  .x.  z )
) )
4744, 46eqeq12d 2449 . . . . . . . . . . 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 6081 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
( x  .+^  r ) 
.x.  z )  =  ( ( x  .+^  r )  .x.  w
) )
49 oveq2 6081 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
x  .x.  z )  =  ( x  .x.  w ) )
50 oveq2 6081 . . . . . . . . . . . . 13  |-  ( z  =  w  ->  (
r  .x.  z )  =  ( r  .x.  w ) )
5149, 50oveq12d 6091 . . . . . . . . . . . 12  |-  ( z  =  w  ->  (
( x  .x.  z
)  .+  ( r  .x.  z ) )  =  ( ( x  .x.  w )  .+  (
r  .x.  w )
) )
5248, 51eqeq12d 2449 . . . . . . . . . . 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 3050 . . . . . . . . . 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 643 . . . . . . . . 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 1134 . . . . . . 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 1171 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  B  ->  ( y  e.  B  ->  ( z  e.  V  ->  ( ( x  .X.  y )  .x.  z
)  =  ( x 
.x.  ( y  .x.  z ) ) ) ) ) )
5958imp43 579 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  B )  /\  (
y  e.  B  /\  z  e.  V )
)  ->  ( (
x  .X.  y )  .x.  z )  =  ( x  .x.  ( y 
.x.  z ) ) )
6059ralrimivva 2790 . . . . . . . . 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 461 . . . . . . . 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 6081 . . . . . . . . . . . 12  |-  ( y  =  r  ->  (
x  .X.  y )  =  ( x  .X.  r ) )
6362oveq1d 6088 . . . . . . . . . . 11  |-  ( y  =  r  ->  (
( x  .X.  y
)  .x.  z )  =  ( ( x 
.X.  r )  .x.  z ) )
6445oveq2d 6089 . . . . . . . . . . 11  |-  ( y  =  r  ->  (
x  .x.  ( y  .x.  z ) )  =  ( x  .x.  (
r  .x.  z )
) )
6563, 64eqeq12d 2449 . . . . . . . . . 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 6081 . . . . . . . . . . 11  |-  ( z  =  w  ->  (
( x  .X.  r
)  .x.  z )  =  ( ( x 
.X.  r )  .x.  w ) )
6750oveq2d 6089 . . . . . . . . . . 11  |-  ( z  =  w  ->  (
x  .x.  ( r  .x.  z ) )  =  ( x  .x.  (
r  .x.  w )
) )
6866, 67eqeq12d 2449 . . . . . . . . . 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 3050 . . . . . . . . 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 643 . . . . . . . 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 2781 . . . . . . . 8  |-  ( ph  ->  A. x  e.  V  (  .1.  .x.  x )  =  x )
74 oveq2 6081 . . . . . . . . . . 11  |-  ( x  =  w  ->  (  .1.  .x.  x )  =  (  .1.  .x.  w
) )
75 id 20 . . . . . . . . . . 11  |-  ( x  =  w  ->  x  =  w )
7674, 75eqeq12d 2449 . . . . . . . . . 10  |-  ( x  =  w  ->  (
(  .1.  .x.  x
)  =  x  <->  (  .1.  .x.  w )  =  w ) )
7776rspcv 3040 . . . . . . . . 9  |-  ( w  e.  V  ->  ( A. x  e.  V  (  .1.  .x.  x )  =  x  ->  (  .1. 
.x.  w )  =  w ) )
7877ad2antll 710 . . . . . . . 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 456 . . . . . . 7  |-  ( (
ph  /\  ( (
x  e.  B  /\  r  e.  B )  /\  ( u  e.  V  /\  w  e.  V
) ) )  -> 
(  .1.  .x.  w
)  =  w )
8056, 71, 79jca32 522 . . . . . 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 630 . . . . 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 2790 . . . 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 2790 . . 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 5724 . . . . 5  |-  ( ph  ->  ( Base `  F
)  =  ( Base `  (Scalar `  W )
) )
8684, 85eqtrd 2467 . . . 4  |-  ( ph  ->  B  =  ( Base `  (Scalar `  W )
) )
87 islmodd.v . . . . . 6  |-  ( ph  ->  V  =  ( Base `  W ) )
88 islmodd.s . . . . . . . . . . 11  |-  ( ph  ->  .x.  =  ( .s
`  W ) )
8988oveqd 6090 . . . . . . . . . 10  |-  ( ph  ->  ( r  .x.  w
)  =  ( r ( .s `  W
) w ) )
9089, 87eleq12d 2503 . . . . . . . . 9  |-  ( ph  ->  ( ( r  .x.  w )  e.  V  <->  ( r ( .s `  W ) w )  e.  ( Base `  W
) ) )
91 eqidd 2436 . . . . . . . . . . 11  |-  ( ph  ->  r  =  r )
92 islmodd.a . . . . . . . . . . . 12  |-  ( ph  ->  .+  =  ( +g  `  W ) )
9392oveqd 6090 . . . . . . . . . . 11  |-  ( ph  ->  ( w  .+  u
)  =  ( w ( +g  `  W
) u ) )
9488, 91, 93oveq123d 6094 . . . . . . . . . 10  |-  ( ph  ->  ( r  .x.  (
w  .+  u )
)  =  ( r ( .s `  W
) ( w ( +g  `  W ) u ) ) )
9588oveqd 6090 . . . . . . . . . . 11  |-  ( ph  ->  ( r  .x.  u
)  =  ( r ( .s `  W
) u ) )
9692, 89, 95oveq123d 6094 . . . . . . . . . 10  |-  ( ph  ->  ( ( r  .x.  w )  .+  (
r  .x.  u )
)  =  ( ( r ( .s `  W ) w ) ( +g  `  W
) ( r ( .s `  W ) u ) ) )
9794, 96eqeq12d 2449 . . . . . . . . 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 5724 . . . . . . . . . . . . 13  |-  ( ph  ->  ( +g  `  F
)  =  ( +g  `  (Scalar `  W )
) )
10098, 99eqtrd 2467 . . . . . . . . . . . 12  |-  ( ph  -> 
.+^  =  ( +g  `  (Scalar `  W )
) )
101100oveqd 6090 . . . . . . . . . . 11  |-  ( ph  ->  ( x  .+^  r )  =  ( x ( +g  `  (Scalar `  W ) ) r ) )
102 eqidd 2436 . . . . . . . . . . 11  |-  ( ph  ->  w  =  w )
10388, 101, 102oveq123d 6094 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  .+^  r )  .x.  w
)  =  ( ( x ( +g  `  (Scalar `  W ) ) r ) ( .s `  W ) w ) )
10488oveqd 6090 . . . . . . . . . . 11  |-  ( ph  ->  ( x  .x.  w
)  =  ( x ( .s `  W
) w ) )
10592, 104, 89oveq123d 6094 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  .x.  w )  .+  (
r  .x.  w )
)  =  ( ( x ( .s `  W ) w ) ( +g  `  W
) ( r ( .s `  W ) w ) ) )
106103, 105eqeq12d 2449 . . . . . . . . 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 1254 . . . . . . . 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 5724 . . . . . . . . . . . . 13  |-  ( ph  ->  ( .r `  F
)  =  ( .r
`  (Scalar `  W )
) )
110108, 109eqtrd 2467 . . . . . . . . . . . 12  |-  ( ph  ->  .X.  =  ( .r
`  (Scalar `  W )
) )
111110oveqd 6090 . . . . . . . . . . 11  |-  ( ph  ->  ( x  .X.  r
)  =  ( x ( .r `  (Scalar `  W ) ) r ) )
11288, 111, 102oveq123d 6094 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  .X.  r )  .x.  w
)  =  ( ( x ( .r `  (Scalar `  W ) ) r ) ( .s
`  W ) w ) )
113 eqidd 2436 . . . . . . . . . . 11  |-  ( ph  ->  x  =  x )
11488, 113, 89oveq123d 6094 . . . . . . . . . 10  |-  ( ph  ->  ( x  .x.  (
r  .x.  w )
)  =  ( x ( .s `  W
) ( r ( .s `  W ) w ) ) )
115112, 114eqeq12d 2449 . . . . . . . . 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 5724 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1r `  F
)  =  ( 1r
`  (Scalar `  W )
) )
118116, 117eqtrd 2467 . . . . . . . . . . 11  |-  ( ph  ->  .1.  =  ( 1r
`  (Scalar `  W )
) )
11988, 118, 102oveq123d 6094 . . . . . . . . . 10  |-  ( ph  ->  (  .1.  .x.  w
)  =  ( ( 1r `  (Scalar `  W ) ) ( .s `  W ) w ) )
120119eqeq1d 2443 . . . . . . . . 9  |-  ( ph  ->  ( (  .1.  .x.  w )  =  w  <-> 
( ( 1r `  (Scalar `  W ) ) ( .s `  W
) w )  =  w ) )
121115, 120anbi12d 692 . . . . . . . 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 692 . . . . . . 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 2908 . . . . . 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 2908 . . . . 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 2908 . . . 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 2908 . . 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 202 . 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 2435 . . 3  |-  ( Base `  W )  =  (
Base `  W )
129 eqid 2435 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
130 eqid 2435 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
131 eqid 2435 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
132 eqid 2435 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
133 eqid 2435 . . 3  |-  ( +g  `  (Scalar `  W )
)  =  ( +g  `  (Scalar `  W )
)
134 eqid 2435 . . 3  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
135 eqid 2435 . . 3  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
136128, 129, 130, 131, 132, 133, 134, 135islmod 15944 . 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 1138 1  |-  ( ph  ->  W  e.  LMod )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936    = wceq 1652    e. wcel 1725   A.wral 2697   ` cfv 5446  (class class class)co 6073   Basecbs 13459   +g cplusg 13519   .rcmulr 13520  Scalarcsca 13522   .scvsca 13523   Grpcgrp 14675   Ringcrg 15650   1rcur 15652   LModclmod 15940
This theorem is referenced by:  islss3  16025  prdslmodd  16035  sralmod  16248  psrlmod  16455  zlmlmod  16794  mendlmod  27433  lduallmodlem  29851  dvalveclem  31724  dvhlveclem  31807
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-nul 4330
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-lmod 15942
  Copyright terms: Public domain W3C validator