| 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 2733 | . . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
| 2 | eqid 2733 | . . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
| 3 | eqid 2733 | . . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
| 4 | eqid 2733 | . . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
| 5 | eqid 2733 | . . . 4 ⊢ (.r‘𝑊) = (.r‘𝑊) | |
| 6 | 1, 2, 3, 4, 5 | isassa 21803 | . . 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 1541 ∈ wcel 2113 ∀wral 3049 ‘cfv 6489 (class class class)co 7355 Basecbs 17130 .rcmulr 17172 Scalarcsca 17174 ·𝑠 cvsca 17175 Ringcrg 20161 LModclmod 20803 AssAlgcasa 21797 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2705 ax-nul 5248 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2712 df-cleq 2725 df-clel 2808 df-ne 2931 df-ral 3050 df-rab 3398 df-v 3440 df-sbc 3739 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4285 df-if 4477 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-br 5096 df-iota 6445 df-fv 6497 df-ov 7358 df-assa 21800 |
| This theorem is referenced by: issubassa 21814 assapropd 21819 aspval 21820 asclmul1 21833 asclmul2 21834 ascldimul 21835 asclrhm 21837 rnascl 21838 aspval2 21845 assamulgscmlem1 21846 assamulgscmlem2 21847 asclmulg 21849 zlmassa 21850 mplind 22015 evlseu 22028 pf1subrg 22273 matinv 22602 lactlmhm 33658 assalactf1o 33659 assarrginv 33660 irngnzply1lem 33714 assaascl0 48495 assaascl1 48496 asclelbas 49120 asclelbasALT 49121 |
| Copyright terms: Public domain | W3C validator |