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

Definition df-lmod 18631
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 18629 . 2 class LMod
2 vf . . . . . . . . . . . . 13 setvar 𝑓
32cv 1473 . . . . . . . . . . . 12 class 𝑓
4 crg 18313 . . . . . . . . . . . 12 class Ring
53, 4wcel 1976 . . . . . . . . . . 11 wff 𝑓 ∈ Ring
6 vr . . . . . . . . . . . . . . . . . . . 20 setvar 𝑟
76cv 1473 . . . . . . . . . . . . . . . . . . 19 class 𝑟
8 vw . . . . . . . . . . . . . . . . . . . 20 setvar 𝑤
98cv 1473 . . . . . . . . . . . . . . . . . . 19 class 𝑤
10 vs . . . . . . . . . . . . . . . . . . . 20 setvar 𝑠
1110cv 1473 . . . . . . . . . . . . . . . . . . 19 class 𝑠
127, 9, 11co 6524 . . . . . . . . . . . . . . . . . 18 class (𝑟𝑠𝑤)
13 vv . . . . . . . . . . . . . . . . . . 19 setvar 𝑣
1413cv 1473 . . . . . . . . . . . . . . . . . 18 class 𝑣
1512, 14wcel 1976 . . . . . . . . . . . . . . . . 17 wff (𝑟𝑠𝑤) ∈ 𝑣
16 vx . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑥
1716cv 1473 . . . . . . . . . . . . . . . . . . . 20 class 𝑥
18 va . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑎
1918cv 1473 . . . . . . . . . . . . . . . . . . . 20 class 𝑎
209, 17, 19co 6524 . . . . . . . . . . . . . . . . . . 19 class (𝑤𝑎𝑥)
217, 20, 11co 6524 . . . . . . . . . . . . . . . . . 18 class (𝑟𝑠(𝑤𝑎𝑥))
227, 17, 11co 6524 . . . . . . . . . . . . . . . . . . 19 class (𝑟𝑠𝑥)
2312, 22, 19co 6524 . . . . . . . . . . . . . . . . . 18 class ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥))
2421, 23wceq 1474 . . . . . . . . . . . . . . . . 17 wff (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥))
25 vq . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑞
2625cv 1473 . . . . . . . . . . . . . . . . . . . 20 class 𝑞
27 vp . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑝
2827cv 1473 . . . . . . . . . . . . . . . . . . . 20 class 𝑝
2926, 7, 28co 6524 . . . . . . . . . . . . . . . . . . 19 class (𝑞𝑝𝑟)
3029, 9, 11co 6524 . . . . . . . . . . . . . . . . . 18 class ((𝑞𝑝𝑟)𝑠𝑤)
3126, 9, 11co 6524 . . . . . . . . . . . . . . . . . . 19 class (𝑞𝑠𝑤)
3231, 12, 19co 6524 . . . . . . . . . . . . . . . . . 18 class ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))
3330, 32wceq 1474 . . . . . . . . . . . . . . . . 17 wff ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))
3415, 24, 33w3a 1030 . . . . . . . . . . . . . . . 16 wff ((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤)))
35 vt . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑡
3635cv 1473 . . . . . . . . . . . . . . . . . . . 20 class 𝑡
3726, 7, 36co 6524 . . . . . . . . . . . . . . . . . . 19 class (𝑞𝑡𝑟)
3837, 9, 11co 6524 . . . . . . . . . . . . . . . . . 18 class ((𝑞𝑡𝑟)𝑠𝑤)
3926, 12, 11co 6524 . . . . . . . . . . . . . . . . . 18 class (𝑞𝑠(𝑟𝑠𝑤))
4038, 39wceq 1474 . . . . . . . . . . . . . . . . 17 wff ((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤))
41 cur 18267 . . . . . . . . . . . . . . . . . . . 20 class 1r
423, 41cfv 5787 . . . . . . . . . . . . . . . . . . 19 class (1r𝑓)
4342, 9, 11co 6524 . . . . . . . . . . . . . . . . . 18 class ((1r𝑓)𝑠𝑤)
4443, 9wceq 1474 . . . . . . . . . . . . . . . . 17 wff ((1r𝑓)𝑠𝑤) = 𝑤
4540, 44wa 382 . . . . . . . . . . . . . . . 16 wff (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)
4634, 45wa 382 . . . . . . . . . . . . . . 15 wff (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))
4746, 8, 14wral 2892 . . . . . . . . . . . . . 14 wff 𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))
4847, 16, 14wral 2892 . . . . . . . . . . . . 13 wff 𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))
49 vk . . . . . . . . . . . . . 14 setvar 𝑘
5049cv 1473 . . . . . . . . . . . . 13 class 𝑘
5148, 6, 50wral 2892 . . . . . . . . . . . 12 wff 𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))
5251, 25, 50wral 2892 . . . . . . . . . . 11 wff 𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤))
535, 52wa 382 . . . . . . . . . 10 wff (𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
54 cmulr 15712 . . . . . . . . . . 11 class .r
553, 54cfv 5787 . . . . . . . . . 10 class (.r𝑓)
5653, 35, 55wsbc 3398 . . . . . . . . 9 wff [(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
57 cplusg 15711 . . . . . . . . . 10 class +g
583, 57cfv 5787 . . . . . . . . 9 class (+g𝑓)
5956, 27, 58wsbc 3398 . . . . . . . 8 wff [(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
60 cbs 15638 . . . . . . . . 9 class Base
613, 60cfv 5787 . . . . . . . 8 class (Base‘𝑓)
6259, 49, 61wsbc 3398 . . . . . . 7 wff [(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
63 vg . . . . . . . . 9 setvar 𝑔
6463cv 1473 . . . . . . . 8 class 𝑔
65 cvsca 15715 . . . . . . . 8 class ·𝑠
6664, 65cfv 5787 . . . . . . 7 class ( ·𝑠𝑔)
6762, 10, 66wsbc 3398 . . . . . 6 wff [( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
68 csca 15714 . . . . . . 7 class Scalar
6964, 68cfv 5787 . . . . . 6 class (Scalar‘𝑔)
7067, 2, 69wsbc 3398 . . . . 5 wff [(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
7164, 57cfv 5787 . . . . 5 class (+g𝑔)
7270, 18, 71wsbc 3398 . . . 4 wff [(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
7364, 60cfv 5787 . . . 4 class (Base‘𝑔)
7472, 13, 73wsbc 3398 . . 3 wff [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))
75 cgrp 17188 . . 3 class Grp
7674, 63, 75crab 2896 . 2 class {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))}
771, 76wceq 1474 1 wff LMod = {𝑔 ∈ Grp ∣ [(Base‘𝑔) / 𝑣][(+g𝑔) / 𝑎][(Scalar‘𝑔) / 𝑓][( ·𝑠𝑔) / 𝑠][(Base‘𝑓) / 𝑘][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡](𝑓 ∈ Ring ∧ ∀𝑞𝑘𝑟𝑘𝑥𝑣𝑤𝑣 (((𝑟𝑠𝑤) ∈ 𝑣 ∧ (𝑟𝑠(𝑤𝑎𝑥)) = ((𝑟𝑠𝑤)𝑎(𝑟𝑠𝑥)) ∧ ((𝑞𝑝𝑟)𝑠𝑤) = ((𝑞𝑠𝑤)𝑎(𝑟𝑠𝑤))) ∧ (((𝑞𝑡𝑟)𝑠𝑤) = (𝑞𝑠(𝑟𝑠𝑤)) ∧ ((1r𝑓)𝑠𝑤) = 𝑤)))}
Colors of variables: wff setvar class
This definition is referenced by:  islmod  18633
  Copyright terms: Public domain W3C validator