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

Theorem rmodislmodlem 13534
Description: Lemma for rmodislmod 13535. This is the part of the proof of rmodislmod 13535 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 2551 . . . . . . . 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 2551 . . . . . . 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 2652 . . . . . . . . 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 1007 . . . . . . . . . . . 12  |-  R  e. 
Grp
7 rmodislmod.v . . . . . . . . . . . . . 14  |-  V  =  ( Base `  R
)
8 eqid 2187 . . . . . . . . . . . . . 14  |-  ( 0g
`  R )  =  ( 0g `  R
)
97, 8grpidcl 12925 . . . . . . . . . . . . 13  |-  ( R  e.  Grp  ->  ( 0g `  R )  e.  V )
10 elex2 2765 . . . . . . . . . . . . 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 3525 . . . . . . . . . . . 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 5895 . . . . . . . . . . . . . 14  |-  ( q  =  b  ->  (
q  .X.  r )  =  ( b  .X.  r ) )
1615oveq2d 5904 . . . . . . . . . . . . 13  |-  ( q  =  b  ->  (
w  .x.  ( q  .X.  r ) )  =  ( w  .x.  (
b  .X.  r )
) )
17 oveq2 5896 . . . . . . . . . . . . . 14  |-  ( q  =  b  ->  (
w  .x.  q )  =  ( w  .x.  b ) )
1817oveq1d 5903 . . . . . . . . . . . . 13  |-  ( q  =  b  ->  (
( w  .x.  q
)  .x.  r )  =  ( ( w 
.x.  b )  .x.  r ) )
1916, 18eqeq12d 2202 . . . . . . . . . . . 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 5896 . . . . . . . . . . . . . 14  |-  ( r  =  a  ->  (
b  .X.  r )  =  ( b  .X.  a ) )
2120oveq2d 5904 . . . . . . . . . . . . 13  |-  ( r  =  a  ->  (
w  .x.  ( b  .X.  r ) )  =  ( w  .x.  (
b  .X.  a )
) )
22 oveq2 5896 . . . . . . . . . . . . 13  |-  ( r  =  a  ->  (
( w  .x.  b
)  .x.  r )  =  ( ( w 
.x.  b )  .x.  a ) )
2321, 22eqeq12d 2202 . . . . . . . . . . . 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 5895 . . . . . . . . . . . . 13  |-  ( w  =  c  ->  (
w  .x.  ( b  .X.  a ) )  =  ( c  .x.  (
b  .X.  a )
) )
25 oveq1 5895 . . . . . . . . . . . . . 14  |-  ( w  =  c  ->  (
w  .x.  b )  =  ( c  .x.  b ) )
2625oveq1d 5903 . . . . . . . . . . . . 13  |-  ( w  =  c  ->  (
( w  .x.  b
)  .x.  a )  =  ( ( c 
.x.  b )  .x.  a ) )
2724, 26eqeq12d 2202 . . . . . . . . . . . 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 2869 . . . . . . . . . . 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 1208 . . . . . . . . . 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 2189 . . . . . . . 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 1021 . . . . 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 13261 . . . . . . . . 9  |-  ( ( F  e.  CRing  /\  b  e.  K  /\  a  e.  K )  ->  (
b  .X.  a )  =  ( a  .X.  b ) )
41403expb 1205 . . . . . . . 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 1018 . . . . 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 5904 . . 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 2220 . 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 5897 . . . . . . . 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 999 . . . . . 6  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  b  e.  K )
54 simp3 1000 . . . . . 6  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  c  e.  V )
55 vex 2752 . . . . . . . 8  |-  c  e. 
_V
56 rmodislmod.s . . . . . . . . 9  |-  .x.  =  ( .s `  R )
57 vscaslid 12635 . . . . . . . . . . 11  |-  ( .s  = Slot  ( .s `  ndx )  /\  ( .s `  ndx )  e.  NN )
5857slotex 12502 . . . . . . . . . 10  |-  ( R  e.  Grp  ->  ( .s `  R )  e. 
_V )
596, 58ax-mp 5 . . . . . . . . 9  |-  ( .s
`  R )  e. 
_V
6056, 59eqeltri 2260 . . . . . . . 8  |-  .x.  e.  _V
61 vex 2752 . . . . . . . 8  |-  b  e. 
_V
62 ovexg 5922 . . . . . . . 8  |-  ( ( c  e.  _V  /\  .x. 
e.  _V  /\  b  e.  _V )  ->  (
c  .x.  b )  e.  _V )
6355, 60, 61, 62mp3an 1347 . . . . . . 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 6015 . . . . 5  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( b  .*  c
)  =  ( c 
.x.  b ) )
6665oveq2d 5904 . . . 4  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( a  .*  (
b  .*  c ) )  =  ( a  .*  ( c  .x.  b ) ) )
67 oveq12 5897 . . . . . . 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 998 . . . . 5  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  a  e.  K )
71 simpl1 1001 . . . . . . . . . . 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 2551 . . . . . . . . . 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 2551 . . . . . . . . 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 1008 . . . . . . . . . . . 12  |-  F  e. 
Ring
75 ringgrp 13248 . . . . . . . . . . . 12  |-  ( F  e.  Ring  ->  F  e. 
Grp )
76 eqid 2187 . . . . . . . . . . . . 13  |-  ( 0g
`  F )  =  ( 0g `  F
)
7738, 76grpidcl 12925 . . . . . . . . . . . 12  |-  ( F  e.  Grp  ->  ( 0g `  F )  e.  K )
7874, 75, 77mp2b 8 . . . . . . . . . . 11  |-  ( 0g
`  F )  e.  K
79 elex2 2765 . . . . . . . . . . 11  |-  ( ( 0g `  F )  e.  K  ->  E. j 
j  e.  K )
80 r19.3rmv 3525 . . . . . . . . . . 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 2650 . . . . . . . . . 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 3525 . . . . . . . . . . . . 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 5896 . . . . . . . . . . . . 13  |-  ( r  =  b  ->  (
w  .x.  r )  =  ( w  .x.  b ) )
8887eleq1d 2256 . . . . . . . . . . . 12  |-  ( r  =  b  ->  (
( w  .x.  r
)  e.  V  <->  ( w  .x.  b )  e.  V
) )
8925eleq1d 2256 . . . . . . . . . . . 12  |-  ( w  =  c  ->  (
( w  .x.  b
)  e.  V  <->  ( c  .x.  b )  e.  V
) )
9088, 89rspc2v 2866 . . . . . . . . . . 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 1021 . . . . . . 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 1016 . . . . 5  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( c  .x.  b
)  e.  V )
97 vex 2752 . . . . . . 7  |-  a  e. 
_V
98 ovexg 5922 . . . . . . 7  |-  ( ( ( c  .x.  b
)  e.  _V  /\  .x. 
e.  _V  /\  a  e.  _V )  ->  (
( c  .x.  b
)  .x.  a )  e.  _V )
9963, 60, 97, 98mp3an 1347 . . . . . 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 6015 . . . 4  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( a  .*  (
c  .x.  b )
)  =  ( ( c  .x.  b ) 
.x.  a ) )
10266, 101eqtrd 2220 . . 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 5897 . . . . . 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 13260 . . . . . . . 8  |-  ( ( F  e.  Ring  /\  a  e.  K  /\  b  e.  K )  ->  (
a  .X.  b )  e.  K )
1081073expib 1207 . . . . . . 7  |-  ( F  e.  Ring  ->  ( ( a  e.  K  /\  b  e.  K )  ->  ( a  .X.  b
)  e.  K ) )
1091083ad2ant2 1020 . . . . . 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 1018 . . . 4  |-  ( ( a  e.  K  /\  b  e.  K  /\  c  e.  V )  ->  ( a  .X.  b
)  e.  K )
112 mulrslid 12604 . . . . . . . . . 10  |-  ( .r  = Slot  ( .r `  ndx )  /\  ( .r `  ndx )  e.  NN )
113112slotex 12502 . . . . . . . . 9  |-  ( F  e.  Ring  ->  ( .r
`  F )  e. 
_V )
11474, 113ax-mp 5 . . . . . . . 8  |-  ( .r
`  F )  e. 
_V
11539, 114eqeltri 2260 . . . . . . 7  |-  .X.  e.  _V
116 ovexg 5922 . . . . . . 7  |-  ( ( a  e.  _V  /\  .X. 
e.  _V  /\  b  e.  _V )  ->  (
a  .X.  b )  e.  _V )
11797, 115, 61, 116mp3an 1347 . . . . . 6  |-  ( a 
.X.  b )  e. 
_V
118 ovexg 5922 . . . . . 6  |-  ( ( c  e.  _V  /\  .x. 
e.  _V  /\  (
a  .X.  b )  e.  _V )  ->  (
c  .x.  ( a  .X.  b ) )  e. 
_V )
11955, 60, 117, 118mp3an 1347 . . . . 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 6015 . . 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 2231 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 979    = wceq 1363   E.wex 1502    e. wcel 2158   A.wral 2465   _Vcvv 2749   <.cop 3607   ` cfv 5228  (class class class)co 5888    e. cmpo 5890   ndxcnx 12472   sSet csts 12473   Basecbs 12475   +g cplusg 12550   .rcmulr 12551  Scalarcsca 12553   .scvsca 12554   0gc0g 12722   Grpcgrp 12898   1rcur 13206   Ringcrg 13243   CRingccrg 13244
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-addcom 7924  ax-addass 7926  ax-i2m1 7929  ax-0lt1 7930  ax-0id 7932  ax-rnegex 7933  ax-pre-ltirr 7936  ax-pre-ltadd 7940
This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-br 4016  df-opab 4077  df-mpt 4078  df-id 4305  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-iota 5190  df-fun 5230  df-fn 5231  df-fv 5236  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-pnf 8007  df-mnf 8008  df-ltxr 8010  df-inn 8933  df-2 8991  df-3 8992  df-4 8993  df-5 8994  df-6 8995  df-ndx 12478  df-slot 12479  df-base 12481  df-sets 12482  df-plusg 12563  df-mulr 12564  df-vsca 12567  df-0g 12724  df-mgm 12793  df-sgrp 12826  df-mnd 12839  df-grp 12901  df-cmn 13122  df-mgp 13171  df-ring 13245  df-cring 13246
This theorem is referenced by:  rmodislmod  13535
  Copyright terms: Public domain W3C validator