ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rmodislmodlem Unicode version

Theorem rmodislmodlem 13634
Description: Lemma for rmodislmod 13635. This is the part of the proof of rmodislmod 13635 which requires the scalar ring to be commutative. (Contributed by AV, 3-Dec-2021.)
Hypotheses
Ref Expression
rmodislmod.v  |-  V  =  ( Base `  R
)
rmodislmod.a  |-  .+  =  ( +g  `  R )
rmodislmod.s  |-  .x.  =  ( .s `  R )
rmodislmod.f  |-  F  =  (Scalar `  R )
rmodislmod.k  |-  K  =  ( Base `  F
)
rmodislmod.p  |-  .+^  =  ( +g  `  F )
rmodislmod.t  |-  .X.  =  ( .r `  F )
rmodislmod.u  |-  .1.  =  ( 1r `  F )
rmodislmod.r  |-  ( R  e.  Grp  /\  F  e.  Ring  /\  A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  ( (
( w  .x.  r
)  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) ) )
rmodislmod.m  |-  .*  =  ( s  e.  K ,  v  e.  V  |->  ( v  .x.  s
) )
rmodislmod.l  |-  L  =  ( R sSet  <. ( .s `  ndx ) ,  .*  >. )
Assertion
Ref Expression
rmodislmodlem  |-  ( ( F  e.  CRing  /\  (
a  e.  K  /\  b  e.  K  /\  c  e.  V )
)  ->  ( (
a  .X.  b )  .*  c )  =  ( a  .*  ( b  .*  c ) ) )
Distinct variable groups:    .X. , q, r, w, x    .X. , s, v    .x. , q, r, w, x    .x. , s, v    K, q, r, x    K, s, v    V, q, r, w, x    V, s, v    r,
a, w    s, a,
v    q, b, r, w   
s, b, v    s,
c, v    w, c
Allowed substitution hints:    .+ ( x, w, v, s, r, q, a, b, c)    .+^ ( x, w, v, s, r, q, a, b, c)    R( x, w, v, s, r, q, a, b, c)    .x. ( a, b, c)    .X. ( a,
b, c)    .1. ( x, w, v, s, r, q, a, b, c)    F( x, w, v, s, r, q, a, b, c)    .* ( x, w, v, s, r, q, a, b, c)    K( w, a, b, c)    L( x, w, v, s, r, q, a, b, c)    V( a, b, c)

Proof of Theorem rmodislmodlem
Dummy variable  j is distinct from all other variables.
StepHypRef Expression
1 rmodislmod.r . . . . 5  |-  ( R  e.  Grp  /\  F  e.  Ring  /\  A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  ( (
( w  .x.  r
)  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) ) )
2 simprl 529 . . . . . . . . 9  |-  ( ( ( ( w  .x.  r )  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) )  -> 
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r ) )
322ralimi 2554 . . . . . . . 8  |-  ( A. x  e.  V  A. w  e.  V  (
( ( w  .x.  r )  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) )  ->  A. x  e.  V  A. w  e.  V  ( w  .x.  ( q 
.X.  r ) )  =  ( ( w 
.x.  q )  .x.  r ) )
432ralimi 2554 . . . . . . 7  |-  ( A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
( ( w  .x.  r )  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) )  ->  A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  ( w  .x.  ( q 
.X.  r ) )  =  ( ( w 
.x.  q )  .x.  r ) )
5 ralrot3 2655 . . . . . . . . 9  |-  ( A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
w  .x.  ( q  .X.  r ) )  =  ( ( w  .x.  q )  .x.  r
)  <->  A. x  e.  V  A. q  e.  K  A. r  e.  K  A. w  e.  V  ( w  .x.  ( q 
.X.  r ) )  =  ( ( w 
.x.  q )  .x.  r ) )
61simp1i 1008 . . . . . . . . . . . 12  |-  R  e. 
Grp
7 rmodislmod.v . . . . . . . . . . . . . 14  |-  V  =  ( Base `  R
)
8 eqid 2189 . . . . . . . . . . . . . 14  |-  ( 0g
`  R )  =  ( 0g `  R
)
97, 8grpidcl 12946 . . . . . . . . . . . . 13  |-  ( R  e.  Grp  ->  ( 0g `  R )  e.  V )
10 elex2 2768 . . . . . . . . . . . . 13  |-  ( ( 0g `  R )  e.  V  ->  E. j 
j  e.  V )
119, 10syl 14 . . . . . . . . . . . 12  |-  ( R  e.  Grp  ->  E. j 
j  e.  V )
12 r19.3rmv 3528 . . . . . . . . . . . 12  |-  ( E. j  j  e.  V  ->  ( A. q  e.  K  A. r  e.  K  A. w  e.  V  ( w  .x.  ( q  .X.  r
) )  =  ( ( w  .x.  q
)  .x.  r )  <->  A. x  e.  V  A. q  e.  K  A. r  e.  K  A. w  e.  V  (
w  .x.  ( q  .X.  r ) )  =  ( ( w  .x.  q )  .x.  r
) ) )
136, 11, 12mp2b 8 . . . . . . . . . . 11  |-  ( A. q  e.  K  A. r  e.  K  A. w  e.  V  (
w  .x.  ( q  .X.  r ) )  =  ( ( w  .x.  q )  .x.  r
)  <->  A. x  e.  V  A. q  e.  K  A. r  e.  K  A. w  e.  V  ( w  .x.  ( q 
.X.  r ) )  =  ( ( w 
.x.  q )  .x.  r ) )
1413biimpri 133 . . . . . . . . . 10  |-  ( A. x  e.  V  A. q  e.  K  A. r  e.  K  A. w  e.  V  (
w  .x.  ( q  .X.  r ) )  =  ( ( w  .x.  q )  .x.  r
)  ->  A. q  e.  K  A. r  e.  K  A. w  e.  V  ( w  .x.  ( q  .X.  r
) )  =  ( ( w  .x.  q
)  .x.  r )
)
15 oveq1 5899 . . . . . . . . . . . . . 14  |-  ( q  =  b  ->  (
q  .X.  r )  =  ( b  .X.  r ) )
1615oveq2d 5908 . . . . . . . . . . . . 13  |-  ( q  =  b  ->  (
w  .x.  ( q  .X.  r ) )  =  ( w  .x.  (
b  .X.  r )
) )
17 oveq2 5900 . . . . . . . . . . . . . 14  |-  ( q  =  b  ->  (
w  .x.  q )  =  ( w  .x.  b ) )
1817oveq1d 5907 . . . . . . . . . . . . 13  |-  ( q  =  b  ->  (
( w  .x.  q
)  .x.  r )  =  ( ( w 
.x.  b )  .x.  r ) )
1916, 18eqeq12d 2204 . . . . . . . . . . . 12  |-  ( q  =  b  ->  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  <->  ( w  .x.  ( b  .X.  r
) )  =  ( ( w  .x.  b
)  .x.  r )
) )
20 oveq2 5900 . . . . . . . . . . . . . 14  |-  ( r  =  a  ->  (
b  .X.  r )  =  ( b  .X.  a ) )
2120oveq2d 5908 . . . . . . . . . . . . 13  |-  ( r  =  a  ->  (
w  .x.  ( b  .X.  r ) )  =  ( w  .x.  (
b  .X.  a )
) )
22 oveq2 5900 . . . . . . . . . . . . 13  |-  ( r  =  a  ->  (
( w  .x.  b
)  .x.  r )  =  ( ( w 
.x.  b )  .x.  a ) )
2321, 22eqeq12d 2204 . . . . . . . . . . . 12  |-  ( r  =  a  ->  (
( w  .x.  (
b  .X.  r )
)  =  ( ( w  .x.  b ) 
.x.  r )  <->  ( w  .x.  ( b  .X.  a
) )  =  ( ( w  .x.  b
)  .x.  a )
) )
24 oveq1 5899 . . . . . . . . . . . . 13  |-  ( w  =  c  ->  (
w  .x.  ( b  .X.  a ) )  =  ( c  .x.  (
b  .X.  a )
) )
25 oveq1 5899 . . . . . . . . . . . . . 14  |-  ( w  =  c  ->  (
w  .x.  b )  =  ( c  .x.  b ) )
2625oveq1d 5907 . . . . . . . . . . . . 13  |-  ( w  =  c  ->  (
( w  .x.  b
)  .x.  a )  =  ( ( c 
.x.  b )  .x.  a ) )
2724, 26eqeq12d 2204 . . . . . . . . . . . 12  |-  ( w  =  c  ->  (
( w  .x.  (
b  .X.  a )
)  =  ( ( w  .x.  b ) 
.x.  a )  <->  ( c  .x.  ( b  .X.  a
) )  =  ( ( c  .x.  b
)  .x.  a )
) )
2819, 23, 27rspc3v 2872 . . . . . . . . . . 11  |-  ( ( b  e.  K  /\  a  e.  K  /\  c  e.  V )  ->  ( A. q  e.  K  A. r  e.  K  A. w  e.  V  ( w  .x.  ( q  .X.  r
) )  =  ( ( w  .x.  q
)  .x.  r )  ->  ( c  .x.  (
b  .X.  a )
)  =  ( ( c  .x.  b ) 
.x.  a ) ) )
29283com12 1209 . . . . . . . . . 10  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( A. q  e.  K  A. r  e.  K  A. w  e.  V  ( w  .x.  ( q  .X.  r
) )  =  ( ( w  .x.  q
)  .x.  r )  ->  ( c  .x.  (
b  .X.  a )
)  =  ( ( c  .x.  b ) 
.x.  a ) ) )
3014, 29syl5com 29 . . . . . . . . 9  |-  ( A. x  e.  V  A. q  e.  K  A. r  e.  K  A. w  e.  V  (
w  .x.  ( q  .X.  r ) )  =  ( ( w  .x.  q )  .x.  r
)  ->  ( (
a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( c  .x.  (
b  .X.  a )
)  =  ( ( c  .x.  b ) 
.x.  a ) ) )
315, 30sylbi 121 . . . . . . . 8  |-  ( A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
w  .x.  ( q  .X.  r ) )  =  ( ( w  .x.  q )  .x.  r
)  ->  ( (
a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( c  .x.  (
b  .X.  a )
)  =  ( ( c  .x.  b ) 
.x.  a ) ) )
32 eqcom 2191 . . . . . . . 8  |-  ( ( ( c  .x.  b
)  .x.  a )  =  ( c  .x.  ( b  .X.  a
) )  <->  ( c  .x.  ( b  .X.  a
) )  =  ( ( c  .x.  b
)  .x.  a )
)
3331, 32imbitrrdi 162 . . . . . . 7  |-  ( A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
w  .x.  ( q  .X.  r ) )  =  ( ( w  .x.  q )  .x.  r
)  ->  ( (
a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( ( c  .x.  b )  .x.  a
)  =  ( c 
.x.  ( b  .X.  a ) ) ) )
344, 33syl 14 . . . . . 6  |-  ( A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
( ( w  .x.  r )  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) )  -> 
( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  (
( c  .x.  b
)  .x.  a )  =  ( c  .x.  ( b  .X.  a
) ) ) )
35343ad2ant3 1022 . . . . 5  |-  ( ( R  e.  Grp  /\  F  e.  Ring  /\  A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
( ( w  .x.  r )  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) ) )  ->  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  (
( c  .x.  b
)  .x.  a )  =  ( c  .x.  ( b  .X.  a
) ) ) )
361, 35ax-mp 5 . . . 4  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( ( c  .x.  b )  .x.  a
)  =  ( c 
.x.  ( b  .X.  a ) ) )
3736adantl 277 . . 3  |-  ( ( F  e.  CRing  /\  (
a  e.  K  /\  b  e.  K  /\  c  e.  V )
)  ->  ( (
c  .x.  b )  .x.  a )  =  ( c  .x.  ( b 
.X.  a ) ) )
38 rmodislmod.k . . . . . . . . . 10  |-  K  =  ( Base `  F
)
39 rmodislmod.t . . . . . . . . . 10  |-  .X.  =  ( .r `  F )
4038, 39crngcom 13336 . . . . . . . . 9  |-  ( ( F  e.  CRing  /\  b  e.  K  /\  a  e.  K )  ->  (
b  .X.  a )  =  ( a  .X.  b ) )
41403expb 1206 . . . . . . . 8  |-  ( ( F  e.  CRing  /\  (
b  e.  K  /\  a  e.  K )
)  ->  ( b  .X.  a )  =  ( a  .X.  b )
)
4241expcom 116 . . . . . . 7  |-  ( ( b  e.  K  /\  a  e.  K )  ->  ( F  e.  CRing  -> 
( b  .X.  a
)  =  ( a 
.X.  b ) ) )
4342ancoms 268 . . . . . 6  |-  ( ( a  e.  K  /\  b  e.  K )  ->  ( F  e.  CRing  -> 
( b  .X.  a
)  =  ( a 
.X.  b ) ) )
44433adant3 1019 . . . . 5  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( F  e.  CRing  -> 
( b  .X.  a
)  =  ( a 
.X.  b ) ) )
4544impcom 125 . . . 4  |-  ( ( F  e.  CRing  /\  (
a  e.  K  /\  b  e.  K  /\  c  e.  V )
)  ->  ( b  .X.  a )  =  ( a  .X.  b )
)
4645oveq2d 5908 . . 3  |-  ( ( F  e.  CRing  /\  (
a  e.  K  /\  b  e.  K  /\  c  e.  V )
)  ->  ( c  .x.  ( b  .X.  a
) )  =  ( c  .x.  ( a 
.X.  b ) ) )
4737, 46eqtrd 2222 . 2  |-  ( ( F  e.  CRing  /\  (
a  e.  K  /\  b  e.  K  /\  c  e.  V )
)  ->  ( (
c  .x.  b )  .x.  a )  =  ( c  .x.  ( a 
.X.  b ) ) )
48 rmodislmod.m . . . . . . 7  |-  .*  =  ( s  e.  K ,  v  e.  V  |->  ( v  .x.  s
) )
4948a1i 9 . . . . . 6  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  .*  =  ( s  e.  K ,  v  e.  V  |->  ( v 
.x.  s ) ) )
50 oveq12 5901 . . . . . . . 8  |-  ( ( v  =  c  /\  s  =  b )  ->  ( v  .x.  s
)  =  ( c 
.x.  b ) )
5150ancoms 268 . . . . . . 7  |-  ( ( s  =  b  /\  v  =  c )  ->  ( v  .x.  s
)  =  ( c 
.x.  b ) )
5251adantl 277 . . . . . 6  |-  ( ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V
)  /\  ( s  =  b  /\  v  =  c ) )  ->  ( v  .x.  s )  =  ( c  .x.  b ) )
53 simp2 1000 . . . . . 6  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  b  e.  K )
54 simp3 1001 . . . . . 6  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  c  e.  V )
55 vex 2755 . . . . . . . 8  |-  c  e. 
_V
56 rmodislmod.s . . . . . . . . 9  |-  .x.  =  ( .s `  R )
57 vscaslid 12647 . . . . . . . . . . 11  |-  ( .s  = Slot  ( .s `  ndx )  /\  ( .s `  ndx )  e.  NN )
5857slotex 12514 . . . . . . . . . 10  |-  ( R  e.  Grp  ->  ( .s `  R )  e. 
_V )
596, 58ax-mp 5 . . . . . . . . 9  |-  ( .s
`  R )  e. 
_V
6056, 59eqeltri 2262 . . . . . . . 8  |-  .x.  e.  _V
61 vex 2755 . . . . . . . 8  |-  b  e. 
_V
62 ovexg 5926 . . . . . . . 8  |-  ( ( c  e.  _V  /\  .x. 
e.  _V  /\  b  e.  _V )  ->  (
c  .x.  b )  e.  _V )
6355, 60, 61, 62mp3an 1348 . . . . . . 7  |-  ( c 
.x.  b )  e. 
_V
6463a1i 9 . . . . . 6  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( c  .x.  b
)  e.  _V )
6549, 52, 53, 54, 64ovmpod 6020 . . . . 5  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( b  .*  c
)  =  ( c 
.x.  b ) )
6665oveq2d 5908 . . . 4  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( a  .*  (
b  .*  c ) )  =  ( a  .*  ( c  .x.  b ) ) )
67 oveq12 5901 . . . . . . 7  |-  ( ( v  =  ( c 
.x.  b )  /\  s  =  a )  ->  ( v  .x.  s
)  =  ( ( c  .x.  b ) 
.x.  a ) )
6867ancoms 268 . . . . . 6  |-  ( ( s  =  a  /\  v  =  ( c  .x.  b ) )  -> 
( v  .x.  s
)  =  ( ( c  .x.  b ) 
.x.  a ) )
6968adantl 277 . . . . 5  |-  ( ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V
)  /\  ( s  =  a  /\  v  =  ( c  .x.  b ) ) )  ->  ( v  .x.  s )  =  ( ( c  .x.  b
)  .x.  a )
)
70 simp1 999 . . . . 5  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  a  e.  K )
71 simpl1 1002 . . . . . . . . . . 11  |-  ( ( ( ( w  .x.  r )  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) )  -> 
( w  .x.  r
)  e.  V )
72712ralimi 2554 . . . . . . . . . 10  |-  ( A. x  e.  V  A. w  e.  V  (
( ( w  .x.  r )  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) )  ->  A. x  e.  V  A. w  e.  V  ( w  .x.  r )  e.  V )
73722ralimi 2554 . . . . . . . . 9  |-  ( A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
( ( w  .x.  r )  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) )  ->  A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  ( w  .x.  r )  e.  V )
741simp2i 1009 . . . . . . . . . . . 12  |-  F  e. 
Ring
75 ringgrp 13323 . . . . . . . . . . . 12  |-  ( F  e.  Ring  ->  F  e. 
Grp )
76 eqid 2189 . . . . . . . . . . . . 13  |-  ( 0g
`  F )  =  ( 0g `  F
)
7738, 76grpidcl 12946 . . . . . . . . . . . 12  |-  ( F  e.  Grp  ->  ( 0g `  F )  e.  K )
7874, 75, 77mp2b 8 . . . . . . . . . . 11  |-  ( 0g
`  F )  e.  K
79 elex2 2768 . . . . . . . . . . 11  |-  ( ( 0g `  F )  e.  K  ->  E. j 
j  e.  K )
80 r19.3rmv 3528 . . . . . . . . . . 11  |-  ( E. j  j  e.  K  ->  ( A. r  e.  K  A. x  e.  V  A. w  e.  V  ( w  .x.  r )  e.  V  <->  A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
w  .x.  r )  e.  V ) )
8178, 79, 80mp2b 8 . . . . . . . . . 10  |-  ( A. r  e.  K  A. x  e.  V  A. w  e.  V  (
w  .x.  r )  e.  V  <->  A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  ( w  .x.  r )  e.  V )
8281biimpri 133 . . . . . . . . 9  |-  ( A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
w  .x.  r )  e.  V  ->  A. r  e.  K  A. x  e.  V  A. w  e.  V  ( w  .x.  r )  e.  V
)
83 ralcom 2653 . . . . . . . . . 10  |-  ( A. r  e.  K  A. x  e.  V  A. w  e.  V  (
w  .x.  r )  e.  V  <->  A. x  e.  V  A. r  e.  K  A. w  e.  V  ( w  .x.  r )  e.  V )
84 r19.3rmv 3528 . . . . . . . . . . . . 13  |-  ( E. j  j  e.  V  ->  ( A. r  e.  K  A. w  e.  V  ( w  .x.  r )  e.  V  <->  A. x  e.  V  A. r  e.  K  A. w  e.  V  (
w  .x.  r )  e.  V ) )
856, 11, 84mp2b 8 . . . . . . . . . . . 12  |-  ( A. r  e.  K  A. w  e.  V  (
w  .x.  r )  e.  V  <->  A. x  e.  V  A. r  e.  K  A. w  e.  V  ( w  .x.  r )  e.  V )
8685biimpri 133 . . . . . . . . . . 11  |-  ( A. x  e.  V  A. r  e.  K  A. w  e.  V  (
w  .x.  r )  e.  V  ->  A. r  e.  K  A. w  e.  V  ( w  .x.  r )  e.  V
)
87 oveq2 5900 . . . . . . . . . . . . 13  |-  ( r  =  b  ->  (
w  .x.  r )  =  ( w  .x.  b ) )
8887eleq1d 2258 . . . . . . . . . . . 12  |-  ( r  =  b  ->  (
( w  .x.  r
)  e.  V  <->  ( w  .x.  b )  e.  V
) )
8925eleq1d 2258 . . . . . . . . . . . 12  |-  ( w  =  c  ->  (
( w  .x.  b
)  e.  V  <->  ( c  .x.  b )  e.  V
) )
9088, 89rspc2v 2869 . . . . . . . . . . 11  |-  ( ( b  e.  K  /\  c  e.  V )  ->  ( A. r  e.  K  A. w  e.  V  ( w  .x.  r )  e.  V  ->  ( c  .x.  b
)  e.  V ) )
9186, 90syl5com 29 . . . . . . . . . 10  |-  ( A. x  e.  V  A. r  e.  K  A. w  e.  V  (
w  .x.  r )  e.  V  ->  ( ( b  e.  K  /\  c  e.  V )  ->  ( c  .x.  b
)  e.  V ) )
9283, 91sylbi 121 . . . . . . . . 9  |-  ( A. r  e.  K  A. x  e.  V  A. w  e.  V  (
w  .x.  r )  e.  V  ->  ( ( b  e.  K  /\  c  e.  V )  ->  ( c  .x.  b
)  e.  V ) )
9373, 82, 923syl 17 . . . . . . . 8  |-  ( A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
( ( w  .x.  r )  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) )  -> 
( ( b  e.  K  /\  c  e.  V )  ->  (
c  .x.  b )  e.  V ) )
94933ad2ant3 1022 . . . . . . 7  |-  ( ( R  e.  Grp  /\  F  e.  Ring  /\  A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
( ( w  .x.  r )  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) ) )  ->  ( ( b  e.  K  /\  c  e.  V )  ->  (
c  .x.  b )  e.  V ) )
951, 94ax-mp 5 . . . . . 6  |-  ( ( b  e.  K  /\  c  e.  V )  ->  ( c  .x.  b
)  e.  V )
96953adant1 1017 . . . . 5  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( c  .x.  b
)  e.  V )
97 vex 2755 . . . . . . 7  |-  a  e. 
_V
98 ovexg 5926 . . . . . . 7  |-  ( ( ( c  .x.  b
)  e.  _V  /\  .x. 
e.  _V  /\  a  e.  _V )  ->  (
( c  .x.  b
)  .x.  a )  e.  _V )
9963, 60, 97, 98mp3an 1348 . . . . . 6  |-  ( ( c  .x.  b ) 
.x.  a )  e. 
_V
10099a1i 9 . . . . 5  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( ( c  .x.  b )  .x.  a
)  e.  _V )
10149, 69, 70, 96, 100ovmpod 6020 . . . 4  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( a  .*  (
c  .x.  b )
)  =  ( ( c  .x.  b ) 
.x.  a ) )
10266, 101eqtrd 2222 . . 3  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( a  .*  (
b  .*  c ) )  =  ( ( c  .x.  b ) 
.x.  a ) )
103102adantl 277 . 2  |-  ( ( F  e.  CRing  /\  (
a  e.  K  /\  b  e.  K  /\  c  e.  V )
)  ->  ( a  .*  ( b  .*  c
) )  =  ( ( c  .x.  b
)  .x.  a )
)
104 oveq12 5901 . . . . . 6  |-  ( ( v  =  c  /\  s  =  ( a  .X.  b ) )  -> 
( v  .x.  s
)  =  ( c 
.x.  ( a  .X.  b ) ) )
105104ancoms 268 . . . . 5  |-  ( ( s  =  ( a 
.X.  b )  /\  v  =  c )  ->  ( v  .x.  s
)  =  ( c 
.x.  ( a  .X.  b ) ) )
106105adantl 277 . . . 4  |-  ( ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V
)  /\  ( s  =  ( a  .X.  b )  /\  v  =  c ) )  ->  ( v  .x.  s )  =  ( c  .x.  ( a 
.X.  b ) ) )
10738, 39ringcl 13335 . . . . . . . 8  |-  ( ( F  e.  Ring  /\  a  e.  K  /\  b  e.  K )  ->  (
a  .X.  b )  e.  K )
1081073expib 1208 . . . . . . 7  |-  ( F  e.  Ring  ->  ( ( a  e.  K  /\  b  e.  K )  ->  ( a  .X.  b
)  e.  K ) )
1091083ad2ant2 1021 . . . . . 6  |-  ( ( R  e.  Grp  /\  F  e.  Ring  /\  A. q  e.  K  A. r  e.  K  A. x  e.  V  A. w  e.  V  (
( ( w  .x.  r )  e.  V  /\  ( ( w  .+  x )  .x.  r
)  =  ( ( w  .x.  r ) 
.+  ( x  .x.  r ) )  /\  ( w  .x.  ( q 
.+^  r ) )  =  ( ( w 
.x.  q )  .+  ( w  .x.  r ) ) )  /\  (
( w  .x.  (
q  .X.  r )
)  =  ( ( w  .x.  q ) 
.x.  r )  /\  ( w  .x.  .1.  )  =  w ) ) )  ->  ( ( a  e.  K  /\  b  e.  K )  ->  (
a  .X.  b )  e.  K ) )
1101, 109ax-mp 5 . . . . 5  |-  ( ( a  e.  K  /\  b  e.  K )  ->  ( a  .X.  b
)  e.  K )
1111103adant3 1019 . . . 4  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( a  .X.  b
)  e.  K )
112 mulrslid 12616 . . . . . . . . . 10  |-  ( .r  = Slot  ( .r `  ndx )  /\  ( .r `  ndx )  e.  NN )
113112slotex 12514 . . . . . . . . 9  |-  ( F  e.  Ring  ->  ( .r
`  F )  e. 
_V )
11474, 113ax-mp 5 . . . . . . . 8  |-  ( .r
`  F )  e. 
_V
11539, 114eqeltri 2262 . . . . . . 7  |-  .X.  e.  _V
116 ovexg 5926 . . . . . . 7  |-  ( ( a  e.  _V  /\  .X. 
e.  _V  /\  b  e.  _V )  ->  (
a  .X.  b )  e.  _V )
11797, 115, 61, 116mp3an 1348 . . . . . 6  |-  ( a 
.X.  b )  e. 
_V
118 ovexg 5926 . . . . . 6  |-  ( ( c  e.  _V  /\  .x. 
e.  _V  /\  (
a  .X.  b )  e.  _V )  ->  (
c  .x.  ( a  .X.  b ) )  e. 
_V )
11955, 60, 117, 118mp3an 1348 . . . . 5  |-  ( c 
.x.  ( a  .X.  b ) )  e. 
_V
120119a1i 9 . . . 4  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( c  .x.  (
a  .X.  b )
)  e.  _V )
12149, 106, 111, 54, 120ovmpod 6020 . . 3  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( ( a  .X.  b )  .*  c
)  =  ( c 
.x.  ( a  .X.  b ) ) )
122121adantl 277 . 2  |-  ( ( F  e.  CRing  /\  (
a  e.  K  /\  b  e.  K  /\  c  e.  V )
)  ->  ( (
a  .X.  b )  .*  c )  =  ( c  .x.  ( a 
.X.  b ) ) )
12347, 103, 1223eqtr4rd 2233 1  |-  ( ( F  e.  CRing  /\  (
a  e.  K  /\  b  e.  K  /\  c  e.  V )
)  ->  ( (
a  .X.  b )  .*  c )  =  ( a  .*  ( b  .*  c ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    /\ w3a 980    = wceq 1364   E.wex 1503    e. wcel 2160   A.wral 2468   _Vcvv 2752   <.cop 3610   ` cfv 5232  (class class class)co 5892    e. cmpo 5894   ndxcnx 12484   sSet csts 12485   Basecbs 12487   +g cplusg 12562   .rcmulr 12563  Scalarcsca 12565   .scvsca 12566   0gc0g 12734   Grpcgrp 12918   1rcur 13281   Ringcrg 13318   CRingccrg 13319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-cnex 7922  ax-resscn 7923  ax-1cn 7924  ax-1re 7925  ax-icn 7926  ax-addcl 7927  ax-addrcl 7928  ax-mulcl 7929  ax-addcom 7931  ax-addass 7933  ax-i2m1 7936  ax-0lt1 7937  ax-0id 7939  ax-rnegex 7940  ax-pre-ltirr 7943  ax-pre-ltadd 7947
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4308  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-iota 5193  df-fun 5234  df-fn 5235  df-fv 5240  df-riota 5848  df-ov 5895  df-oprab 5896  df-mpo 5897  df-pnf 8014  df-mnf 8015  df-ltxr 8017  df-inn 8940  df-2 8998  df-3 8999  df-4 9000  df-5 9001  df-6 9002  df-ndx 12490  df-slot 12491  df-base 12493  df-sets 12494  df-plusg 12575  df-mulr 12576  df-vsca 12579  df-0g 12736  df-mgm 12805  df-sgrp 12838  df-mnd 12851  df-grp 12921  df-cmn 13193  df-mgp 13243  df-ring 13320  df-cring 13321
This theorem is referenced by:  rmodislmod  13635
  Copyright terms: Public domain W3C validator