![]() |
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 21804 | . . 3 β’ (π β AssAlg β ((π β LMod β§ π β Ring) β§ βπ§ β (Baseβ(Scalarβπ))βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(((π§( Β·π βπ)π₯)(.rβπ)π¦) = (π§( Β·π βπ)(π₯(.rβπ)π¦)) β§ (π₯(.rβπ)(π§( Β·π βπ)π¦)) = (π§( Β·π βπ)(π₯(.rβπ)π¦))))) |
7 | 6 | simplbi 496 | . 2 β’ (π β AssAlg β (π β LMod β§ π β Ring)) |
8 | 7 | simpld 493 | 1 β’ (π β AssAlg β π β LMod) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 394 = wceq 1533 β wcel 2098 βwral 3058 βcfv 6553 (class class class)co 7426 Basecbs 17189 .rcmulr 17243 Scalarcsca 17245 Β·π cvsca 17246 Ringcrg 20187 LModclmod 20757 AssAlgcasa 21798 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 ax-nul 5310 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-ral 3059 df-rab 3431 df-v 3475 df-sbc 3779 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-br 5153 df-iota 6505 df-fv 6561 df-ov 7429 df-assa 21801 |
This theorem is referenced by: assasca 21810 assa2ass 21811 issubassa3 21813 issubassa 21814 assapropd 21819 aspval 21820 asplss 21821 ascldimul 21835 asclrhm 21837 rnascl 21838 issubassa2 21839 aspval2 21845 assamulgscmlem1 21846 assamulgscmlem2 21847 asclmulg 21849 mplmon2mul 22030 mplind 22031 matinv 22607 assaascl0 47544 assaascl1 47545 |
Copyright terms: Public domain | W3C validator |