![]() |
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 2740 | . . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
2 | eqid 2740 | . . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
3 | eqid 2740 | . . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
4 | eqid 2740 | . . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
5 | eqid 2740 | . . . 4 ⊢ (.r‘𝑊) = (.r‘𝑊) | |
6 | 1, 2, 3, 4, 5 | isassa 21899 | . . 3 ⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑧( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑧( ·𝑠 ‘𝑊)𝑦)) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦))))) |
7 | 6 | simplbi 497 | . 2 ⊢ (𝑊 ∈ AssAlg → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring)) |
8 | 7 | simprd 495 | 1 ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2108 ∀wral 3067 ‘cfv 6573 (class class class)co 7448 Basecbs 17258 .rcmulr 17312 Scalarcsca 17314 ·𝑠 cvsca 17315 Ringcrg 20260 LModclmod 20880 AssAlgcasa 21893 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711 ax-nul 5324 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-ne 2947 df-ral 3068 df-rab 3444 df-v 3490 df-sbc 3805 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-iota 6525 df-fv 6581 df-ov 7451 df-assa 21896 |
This theorem is referenced by: issubassa 21910 assapropd 21915 aspval 21916 asclmul1 21929 asclmul2 21930 ascldimul 21931 asclrhm 21933 rnascl 21934 aspval2 21941 assamulgscmlem1 21942 assamulgscmlem2 21943 asclmulg 21945 zlmassa 21946 mplind 22117 evlseu 22130 pf1subrg 22373 matinv 22704 lactlmhm 33647 assalactf1o 33648 assarrginv 33649 irngnzply1lem 33690 assaascl0 48109 assaascl1 48110 |
Copyright terms: Public domain | W3C validator |