![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > assaring | Structured version Visualization version GIF version |
Description: An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.) |
Ref | Expression |
---|---|
assaring | β’ (π β AssAlg β π β Ring) |
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 21797 | . . 3 β’ (π β AssAlg β ((π β LMod β§ π β Ring) β§ βπ§ β (Baseβ(Scalarβπ))βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(((π§( Β·π βπ)π₯)(.rβπ)π¦) = (π§( Β·π βπ)(π₯(.rβπ)π¦)) β§ (π₯(.rβπ)(π§( Β·π βπ)π¦)) = (π§( Β·π βπ)(π₯(.rβπ)π¦))))) |
7 | 6 | simplbi 496 | . 2 β’ (π β AssAlg β (π β LMod β§ π β Ring)) |
8 | 7 | simprd 494 | 1 β’ (π β AssAlg β π β Ring) |
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 17187 .rcmulr 17241 Scalarcsca 17243 Β·π cvsca 17244 Ringcrg 20180 LModclmod 20750 AssAlgcasa 21791 |
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 21794 |
This theorem is referenced by: issubassa 21807 assapropd 21812 aspval 21813 asclmul1 21826 asclmul2 21827 ascldimul 21828 asclrhm 21830 rnascl 21831 aspval2 21838 assamulgscmlem1 21839 assamulgscmlem2 21840 asclmulg 21842 zlmassa 21843 mplind 22021 evlseu 22036 pf1subrg 22274 matinv 22599 irngnzply1lem 33401 assaascl0 47526 assaascl1 47527 |
Copyright terms: Public domain | W3C validator |