![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > assalmod | Structured version Visualization version GIF version |
Description: An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.) |
Ref | Expression |
---|---|
assalmod | ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2728 | . . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
2 | eqid 2728 | . . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
3 | eqid 2728 | . . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
4 | eqid 2728 | . . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
5 | eqid 2728 | . . . 4 ⊢ (.r‘𝑊) = (.r‘𝑊) | |
6 | 1, 2, 3, 4, 5 | isassa 21790 | . . 3 ⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑧( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑧( ·𝑠 ‘𝑊)𝑦)) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦))))) |
7 | 6 | simplbi 497 | . 2 ⊢ (𝑊 ∈ AssAlg → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring)) |
8 | 7 | simpld 494 | 1 ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1534 ∈ wcel 2099 ∀wral 3058 ‘cfv 6548 (class class class)co 7420 Basecbs 17180 .rcmulr 17234 Scalarcsca 17236 ·𝑠 cvsca 17237 Ringcrg 20173 LModclmod 20743 AssAlgcasa 21784 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-nul 5306 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-ral 3059 df-rab 3430 df-v 3473 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-iota 6500 df-fv 6556 df-ov 7423 df-assa 21787 |
This theorem is referenced by: assasca 21796 assa2ass 21797 issubassa3 21799 issubassa 21800 assapropd 21805 aspval 21806 asplss 21807 ascldimul 21821 asclrhm 21823 rnascl 21824 issubassa2 21825 aspval2 21831 assamulgscmlem1 21832 assamulgscmlem2 21833 asclmulg 21835 mplmon2mul 22013 mplind 22014 matinv 22592 assaascl0 47448 assaascl1 47449 |
Copyright terms: Public domain | W3C validator |