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

Definition df-lmod 19697
 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 = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))}
Distinct variable group:   𝑓,𝑎,𝑔,𝑘,𝑝,𝑞,𝑟,𝑠,𝑡,𝑣,𝑤,𝑥

Detailed syntax breakdown of Definition df-lmod
StepHypRef Expression
1 clmod 19695 . 2 class LMod
2 vf . . . . . . . . . . . . 13 setvar 𝑓
32cv 1538 . . . . . . . . . . . 12 class 𝑓
4 crg 19358 . . . . . . . . . . . 12 class Ring
53, 4wcel 2112 . . . . . . . . . . 11 wff 𝑓 ∈ Ring
6 vr . . . . . . . . . . . . . . . . . . . 20 setvar 𝑟
76cv 1538 . . . . . . . . . . . . . . . . . . 19 class 𝑟
8 vw . . . . . . . . . . . . . . . . . . . 20 setvar 𝑤
98cv 1538 . . . . . . . . . . . . . . . . . . 19 class 𝑤
10 vs . . . . . . . . . . . . . . . . . . . 20 setvar 𝑠
1110cv 1538 . . . . . . . . . . . . . . . . . . 19 class 𝑠
127, 9, 11co 7151 . . . . . . . . . . . . . . . . . 18 class (𝑟𝑠𝑤)
13 vv . . . . . . . . . . . . . . . . . . 19 setvar 𝑣
1413cv 1538 . . . . . . . . . . . . . . . . . 18 class 𝑣
1512, 14wcel 2112 . . . . . . . . . . . . . . . . 17 wff (𝑟𝑠𝑤) ∈ 𝑣
16 vx . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑥
1716cv 1538 . . . . . . . . . . . . . . . . . . . 20 class 𝑥
18 va . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑎
1918cv 1538 . . . . . . . . . . . . . . . . . . . 20 class 𝑎
209, 17, 19co 7151 . . . . . . . . . . . . . . . . . . 19 class (𝑤𝑎𝑥)
217, 20, 11co 7151 . . . . . . . . . . . . . . . . . 18 class (𝑟𝑠(𝑤𝑎𝑥))
227, 17, 11co 7151 . . . . . . . . . . . . . . . . . . 19 class (𝑟𝑠𝑥)
2312, 22, 19co 7151 . . . . . . . . . . . . . . . . . 18 class ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥))
2421, 23wceq 1539 . . . . . . . . . . . . . . . . 17 wff (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥))
25 vq . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑞
2625cv 1538 . . . . . . . . . . . . . . . . . . . 20 class 𝑞
27 vp . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑝
2827cv 1538 . . . . . . . . . . . . . . . . . . . 20 class 𝑝
2926, 7, 28co 7151 . . . . . . . . . . . . . . . . . . 19 class (𝑞𝑝𝑟)
3029, 9, 11co 7151 . . . . . . . . . . . . . . . . . 18 class ((𝑞𝑝𝑟)𝑠𝑤)
3126, 9, 11co 7151 . . . . . . . . . . . . . . . . . . 19 class (𝑞𝑠𝑤)
3231, 12, 19co 7151 . . . . . . . . . . . . . . . . . 18 class ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))
3330, 32wceq 1539 . . . . . . . . . . . . . . . . 17 wff ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))
3415, 24, 33w3a 1085 . . . . . . . . . . . . . . . 16 wff ((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)))
35 vt . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑡
3635cv 1538 . . . . . . . . . . . . . . . . . . . 20 class 𝑡
3726, 7, 36co 7151 . . . . . . . . . . . . . . . . . . 19 class (𝑞𝑡𝑟)
3837, 9, 11co 7151 . . . . . . . . . . . . . . . . . 18 class ((𝑞𝑡𝑟)𝑠𝑤)
3926, 12, 11co 7151 . . . . . . . . . . . . . . . . . 18 class (𝑞𝑠(𝑟𝑠𝑤))
4038, 39wceq 1539 . . . . . . . . . . . . . . . . 17 wff ((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤))
41 cur 19312 . . . . . . . . . . . . . . . . . . . 20 class 1r
423, 41cfv 6336 . . . . . . . . . . . . . . . . . . 19 class (1r𝑓)
4342, 9, 11co 7151 . . . . . . . . . . . . . . . . . 18 class ((1r𝑓)𝑠𝑤)
4443, 9wceq 1539 . . . . . . . . . . . . . . . . 17 wff ((1r𝑓)𝑠𝑤) = 𝑤
4540, 44wa 400 . . . . . . . . . . . . . . . 16 wff (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)
4634, 45wa 400 . . . . . . . . . . . . . . 15 wff (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))
4746, 8, 14wral 3071 . . . . . . . . . . . . . 14 wff 𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))
4847, 16, 14wral 3071 . . . . . . . . . . . . 13 wff 𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))
49 vk . . . . . . . . . . . . . 14 setvar 𝑘
5049cv 1538 . . . . . . . . . . . . 13 class 𝑘
5148, 6, 50wral 3071 . . . . . . . . . . . 12 wff 𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))
5251, 25, 50wral 3071 . . . . . . . . . . 11 wff 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))
535, 52wa 400 . . . . . . . . . 10 wff (𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
54 cmulr 16617 . . . . . . . . . . 11 class .r
553, 54cfv 6336 . . . . . . . . . 10 class (.r𝑓)
5653, 35, 55wsbc 3697 . . . . . . . . 9 wff [(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
57 cplusg 16616 . . . . . . . . . 10 class +g
583, 57cfv 6336 . . . . . . . . 9 class (+g𝑓)
5956, 27, 58wsbc 3697 . . . . . . . 8 wff [(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
60 cbs 16534 . . . . . . . . 9 class Base
613, 60cfv 6336 . . . . . . . 8 class (Base‘𝑓)
6259, 49, 61wsbc 3697 . . . . . . 7 wff [(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
63 vg . . . . . . . . 9 setvar 𝑔
6463cv 1538 . . . . . . . 8 class 𝑔
65 cvsca 16620 . . . . . . . 8 class ·𝑠
6664, 65cfv 6336 . . . . . . 7 class ( ·𝑠𝑔)
6762, 10, 66wsbc 3697 . . . . . 6 wff [( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
68 csca 16619 . . . . . . 7 class Scalar
6964, 68cfv 6336 . . . . . 6 class (Scalar‘𝑔)
7067, 2, 69wsbc 3697 . . . . 5 wff [(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
7164, 57cfv 6336 . . . . 5 class (+g𝑔)
7270, 18, 71wsbc 3697 . . . 4 wff [(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
7364, 60cfv 6336 . . . 4 class (Base‘𝑔)
7472, 13, 73wsbc 3697 . . 3 wff [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
75 cgrp 18162 . . 3 class Grp
7674, 63, 75crab 3075 . 2 class {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))}
771, 76wceq 1539 1 wff LMod = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))}
 Colors of variables: wff setvar class This definition is referenced by:  islmod  19699
 Copyright terms: Public domain W3C validator