![]() |
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 2726 | . . . 4 β’ (Baseβπ) = (Baseβπ) | |
2 | eqid 2726 | . . . 4 β’ (Scalarβπ) = (Scalarβπ) | |
3 | eqid 2726 | . . . 4 β’ (Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) | |
4 | eqid 2726 | . . . 4 β’ ( Β·π βπ) = ( Β·π βπ) | |
5 | eqid 2726 | . . . 4 β’ (.rβπ) = (.rβπ) | |
6 | 1, 2, 3, 4, 5 | isassa 21751 | . . 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 1533 β wcel 2098 βwral 3055 βcfv 6537 (class class class)co 7405 Basecbs 17153 .rcmulr 17207 Scalarcsca 17209 Β·π cvsca 17210 Ringcrg 20138 LModclmod 20706 AssAlgcasa 21745 |
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 2697 ax-nul 5299 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2704 df-cleq 2718 df-clel 2804 df-ne 2935 df-ral 3056 df-rab 3427 df-v 3470 df-sbc 3773 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-br 5142 df-iota 6489 df-fv 6545 df-ov 7408 df-assa 21748 |
This theorem is referenced by: assasca 21757 assa2ass 21758 issubassa3 21760 issubassa 21761 assapropd 21766 aspval 21767 asplss 21768 ascldimul 21782 asclrhm 21784 rnascl 21785 issubassa2 21786 aspval2 21792 assamulgscmlem1 21793 assamulgscmlem2 21794 asclmulg 21796 mplmon2mul 21972 mplind 21973 matinv 22534 assaascl0 47336 assaascl1 47337 |
Copyright terms: Public domain | W3C validator |