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

Definition df-lmod 15631
Description: Define the class of all left modules, which are generalizations of left vector spaces. A left module over a ring is an (Abelian) group (vectors) together with a ring (scalars) and a left scalar product connecting them. (Contributed by NM, 4-Nov-2013.)
Assertion
Ref Expression
df-lmod  |-  LMod  =  { g  e.  Grp  | 
[. ( Base `  g
)  /  v ]. [. ( +g  `  g
)  /  a ]. [. (Scalar `  g )  /  f ]. [. ( .s `  g )  / 
s ]. [. ( Base `  f )  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e.  Ring  /\ 
A. q  e.  k 
A. r  e.  k 
A. x  e.  v 
A. w  e.  v  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  (
( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) ) ) }
Distinct variable group:    f, a, g, k, p, q, r, s, t, v, w, x

Detailed syntax breakdown of Definition df-lmod
StepHypRef Expression
1 clmod 15629 . 2  class  LMod
2 vf . . . . . . . . . . . . 13  set  f
32cv 1624 . . . . . . . . . . . 12  class  f
4 crg 15339 . . . . . . . . . . . 12  class  Ring
53, 4wcel 1686 . . . . . . . . . . 11  wff  f  e. 
Ring
6 vr . . . . . . . . . . . . . . . . . . . 20  set  r
76cv 1624 . . . . . . . . . . . . . . . . . . 19  class  r
8 vw . . . . . . . . . . . . . . . . . . . 20  set  w
98cv 1624 . . . . . . . . . . . . . . . . . . 19  class  w
10 vs . . . . . . . . . . . . . . . . . . . 20  set  s
1110cv 1624 . . . . . . . . . . . . . . . . . . 19  class  s
127, 9, 11co 5860 . . . . . . . . . . . . . . . . . 18  class  ( r s w )
13 vv . . . . . . . . . . . . . . . . . . 19  set  v
1413cv 1624 . . . . . . . . . . . . . . . . . 18  class  v
1512, 14wcel 1686 . . . . . . . . . . . . . . . . 17  wff  ( r s w )  e.  v
16 vx . . . . . . . . . . . . . . . . . . . . 21  set  x
1716cv 1624 . . . . . . . . . . . . . . . . . . . 20  class  x
18 va . . . . . . . . . . . . . . . . . . . . 21  set  a
1918cv 1624 . . . . . . . . . . . . . . . . . . . 20  class  a
209, 17, 19co 5860 . . . . . . . . . . . . . . . . . . 19  class  ( w a x )
217, 20, 11co 5860 . . . . . . . . . . . . . . . . . 18  class  ( r s ( w a x ) )
227, 17, 11co 5860 . . . . . . . . . . . . . . . . . . 19  class  ( r s x )
2312, 22, 19co 5860 . . . . . . . . . . . . . . . . . 18  class  ( ( r s w ) a ( r s x ) )
2421, 23wceq 1625 . . . . . . . . . . . . . . . . 17  wff  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )
25 vq . . . . . . . . . . . . . . . . . . . . 21  set  q
2625cv 1624 . . . . . . . . . . . . . . . . . . . 20  class  q
27 vp . . . . . . . . . . . . . . . . . . . . 21  set  p
2827cv 1624 . . . . . . . . . . . . . . . . . . . 20  class  p
2926, 7, 28co 5860 . . . . . . . . . . . . . . . . . . 19  class  ( q p r )
3029, 9, 11co 5860 . . . . . . . . . . . . . . . . . 18  class  ( ( q p r ) s w )
3126, 9, 11co 5860 . . . . . . . . . . . . . . . . . . 19  class  ( q s w )
3231, 12, 19co 5860 . . . . . . . . . . . . . . . . . 18  class  ( ( q s w ) a ( r s w ) )
3330, 32wceq 1625 . . . . . . . . . . . . . . . . 17  wff  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) )
3415, 24, 33w3a 934 . . . . . . . . . . . . . . . 16  wff  ( ( r s w )  e.  v  /\  (
r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  (
( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )
35 vt . . . . . . . . . . . . . . . . . . . . 21  set  t
3635cv 1624 . . . . . . . . . . . . . . . . . . . 20  class  t
3726, 7, 36co 5860 . . . . . . . . . . . . . . . . . . 19  class  ( q t r )
3837, 9, 11co 5860 . . . . . . . . . . . . . . . . . 18  class  ( ( q t r ) s w )
3926, 12, 11co 5860 . . . . . . . . . . . . . . . . . 18  class  ( q s ( r s w ) )
4038, 39wceq 1625 . . . . . . . . . . . . . . . . 17  wff  ( ( q t r ) s w )  =  ( q s ( r s w ) )
41 cur 15341 . . . . . . . . . . . . . . . . . . . 20  class  1r
423, 41cfv 5257 . . . . . . . . . . . . . . . . . . 19  class  ( 1r
`  f )
4342, 9, 11co 5860 . . . . . . . . . . . . . . . . . 18  class  ( ( 1r `  f ) s w )
4443, 9wceq 1625 . . . . . . . . . . . . . . . . 17  wff  ( ( 1r `  f ) s w )  =  w
4540, 44wa 358 . . . . . . . . . . . . . . . 16  wff  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  (
( 1r `  f
) s w )  =  w )
4634, 45wa 358 . . . . . . . . . . . . . . 15  wff  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) )
4746, 8, 14wral 2545 . . . . . . . . . . . . . 14  wff  A. w  e.  v  ( (
( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) )
4847, 16, 14wral 2545 . . . . . . . . . . . . 13  wff  A. x  e.  v  A. w  e.  v  ( (
( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) )
49 vk . . . . . . . . . . . . . 14  set  k
5049cv 1624 . . . . . . . . . . . . 13  class  k
5148, 6, 50wral 2545 . . . . . . . . . . . 12  wff  A. r  e.  k  A. x  e.  v  A. w  e.  v  ( (
( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) )
5251, 25, 50wral 2545 . . . . . . . . . . 11  wff  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  ( (
( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) )
535, 52wa 358 . . . . . . . . . 10  wff  ( f  e.  Ring  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  ( (
( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) ) )
54 cmulr 13211 . . . . . . . . . . 11  class  .r
553, 54cfv 5257 . . . . . . . . . 10  class  ( .r
`  f )
5653, 35, 55wsbc 2993 . . . . . . . . 9  wff  [. ( .r `  f )  / 
t ]. ( f  e. 
Ring  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  ( ( ( r s w )  e.  v  /\  (
r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  (
( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r
`  f ) s w )  =  w ) ) )
57 cplusg 13210 . . . . . . . . . 10  class  +g
583, 57cfv 5257 . . . . . . . . 9  class  ( +g  `  f )
5956, 27, 58wsbc 2993 . . . . . . . 8  wff  [. ( +g  `  f )  /  p ]. [. ( .r
`  f )  / 
t ]. ( f  e. 
Ring  /\  A. q  e.  k  A. r  e.  k  A. x  e.  v  A. w  e.  v  ( ( ( r s w )  e.  v  /\  (
r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  (
( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  ( ( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r
`  f ) s w )  =  w ) ) )
60 cbs 13150 . . . . . . . . 9  class  Base
613, 60cfv 5257 . . . . . . . 8  class  ( Base `  f )
6259, 49, 61wsbc 2993 . . . . . . 7  wff  [. ( Base `  f )  / 
k ]. [. ( +g  `  f )  /  p ]. [. ( .r `  f )  /  t ]. ( f  e.  Ring  /\ 
A. q  e.  k 
A. r  e.  k 
A. x  e.  v 
A. w  e.  v  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  (
( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) ) )
63 vg . . . . . . . . 9  set  g
6463cv 1624 . . . . . . . 8  class  g
65 cvsca 13214 . . . . . . . 8  class  .s
6664, 65cfv 5257 . . . . . . 7  class  ( .s
`  g )
6762, 10, 66wsbc 2993 . . . . . 6  wff  [. ( .s `  g )  / 
s ]. [. ( Base `  f )  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e.  Ring  /\ 
A. q  e.  k 
A. r  e.  k 
A. x  e.  v 
A. w  e.  v  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  (
( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) ) )
68 csca 13213 . . . . . . 7  class Scalar
6964, 68cfv 5257 . . . . . 6  class  (Scalar `  g )
7067, 2, 69wsbc 2993 . . . . 5  wff  [. (Scalar `  g )  /  f ]. [. ( .s `  g )  /  s ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e.  Ring  /\ 
A. q  e.  k 
A. r  e.  k 
A. x  e.  v 
A. w  e.  v  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  (
( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) ) )
7164, 57cfv 5257 . . . . 5  class  ( +g  `  g )
7270, 18, 71wsbc 2993 . . . 4  wff  [. ( +g  `  g )  / 
a ]. [. (Scalar `  g )  /  f ]. [. ( .s `  g )  /  s ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e.  Ring  /\ 
A. q  e.  k 
A. r  e.  k 
A. x  e.  v 
A. w  e.  v  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  (
( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) ) )
7364, 60cfv 5257 . . . 4  class  ( Base `  g )
7472, 13, 73wsbc 2993 . . 3  wff  [. ( Base `  g )  / 
v ]. [. ( +g  `  g )  /  a ]. [. (Scalar `  g
)  /  f ]. [. ( .s `  g
)  /  s ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e.  Ring  /\ 
A. q  e.  k 
A. r  e.  k 
A. x  e.  v 
A. w  e.  v  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  (
( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) ) )
75 cgrp 14364 . . 3  class  Grp
7674, 63, 75crab 2549 . 2  class  { g  e.  Grp  |  [. ( Base `  g )  /  v ]. [. ( +g  `  g )  / 
a ]. [. (Scalar `  g )  /  f ]. [. ( .s `  g )  /  s ]. [. ( Base `  f
)  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e.  Ring  /\ 
A. q  e.  k 
A. r  e.  k 
A. x  e.  v 
A. w  e.  v  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  (
( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) ) ) }
771, 76wceq 1625 1  wff  LMod  =  { g  e.  Grp  | 
[. ( Base `  g
)  /  v ]. [. ( +g  `  g
)  /  a ]. [. (Scalar `  g )  /  f ]. [. ( .s `  g )  / 
s ]. [. ( Base `  f )  /  k ]. [. ( +g  `  f
)  /  p ]. [. ( .r `  f
)  /  t ]. ( f  e.  Ring  /\ 
A. q  e.  k 
A. r  e.  k 
A. x  e.  v 
A. w  e.  v  ( ( ( r s w )  e.  v  /\  ( r s ( w a x ) )  =  ( ( r s w ) a ( r s x ) )  /\  ( ( q p r ) s w )  =  ( ( q s w ) a ( r s w ) ) )  /\  (
( ( q t r ) s w )  =  ( q s ( r s w ) )  /\  ( ( 1r `  f ) s w )  =  w ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  islmod  15633
  Copyright terms: Public domain W3C validator