Metamath Proof Explorer

Definition df-lmod

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)

Ref Expression
Assertion 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 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmod 
 |-  LMod
1 vg 
 |-  g
2 cgrp 
 |-  Grp
3 cbs 
 |-  Base
4 1 cv 
 |-  g
5 4 3 cfv 
 |-  ( Base ` g )
6 vv 
 |-  v
7 cplusg 
 |-  +g
8 4 7 cfv 
 |-  ( +g ` g )
9 va 
 |-  a
10 csca 
 |-  Scalar
11 4 10 cfv 
 |-  ( Scalar ` g )
12 vf 
 |-  f
13 cvsca 
 |-  .s
14 4 13 cfv 
 |-  ( .s ` g )
15 vs 
 |-  s
16 12 cv 
 |-  f
17 16 3 cfv 
 |-  ( Base ` f )
18 vk 
 |-  k
19 16 7 cfv 
 |-  ( +g ` f )
20 vp 
 |-  p
21 cmulr 
 |-  .r
22 16 21 cfv 
 |-  ( .r ` f )
23 vt 
 |-  t
24 crg 
 |-  Ring
25 16 24 wcel 
 |-  f e. Ring
26 vq 
 |-  q
27 18 cv 
 |-  k
28 vr 
 |-  r
29 vx 
 |-  x
30 6 cv 
 |-  v
31 vw 
 |-  w
32 28 cv 
 |-  r
33 15 cv 
 |-  s
34 31 cv 
 |-  w
35 32 34 33 co 
 |-  ( r s w )
36 35 30 wcel 
 |-  ( r s w ) e. v
37 9 cv 
 |-  a
38 29 cv 
 |-  x
39 34 38 37 co 
 |-  ( w a x )
40 32 39 33 co 
 |-  ( r s ( w a x ) )
41 32 38 33 co 
 |-  ( r s x )
42 35 41 37 co 
 |-  ( ( r s w ) a ( r s x ) )
43 40 42 wceq 
 |-  ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) )
44 26 cv 
 |-  q
45 20 cv 
 |-  p
46 44 32 45 co 
 |-  ( q p r )
47 46 34 33 co 
 |-  ( ( q p r ) s w )
48 44 34 33 co 
 |-  ( q s w )
49 48 35 37 co 
 |-  ( ( q s w ) a ( r s w ) )
50 47 49 wceq 
 |-  ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) )
51 36 43 50 w3a 
 |-  ( ( 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 ) ) )
52 23 cv 
 |-  t
53 44 32 52 co 
 |-  ( q t r )
54 53 34 33 co 
 |-  ( ( q t r ) s w )
55 44 35 33 co 
 |-  ( q s ( r s w ) )
56 54 55 wceq 
 |-  ( ( q t r ) s w ) = ( q s ( r s w ) )
57 cur 
 |-  1r
58 16 57 cfv 
 |-  ( 1r ` f )
59 58 34 33 co 
 |-  ( ( 1r ` f ) s w )
60 59 34 wceq 
 |-  ( ( 1r ` f ) s w ) = w
61 56 60 wa 
 |-  ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w )
62 51 61 wa 
 |-  ( ( ( 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 62 31 30 wral 
 |-  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 ) )
64 63 29 30 wral 
 |-  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 ) )
65 64 28 27 wral 
 |-  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 ) )
66 65 26 27 wral 
 |-  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 ) )
67 25 66 wa 
 |-  ( 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 67 23 22 wsbc 
 |-  [. ( .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 ) ) )
69 68 20 19 wsbc 
 |-  [. ( +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 ) ) )
70 69 18 17 wsbc 
 |-  [. ( 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 ) ) )
71 70 15 14 wsbc 
 |-  [. ( .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 ) ) )
72 71 12 11 wsbc 
 |-  [. ( 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 ) ) )
73 72 9 8 wsbc 
 |-  [. ( +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 ) ) )
74 73 6 5 wsbc 
 |-  [. ( 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 74 1 2 crab 
 |-  { 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 ) ) ) }
76 0 75 wceq 
 |-  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 ) ) ) }