| 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 2765 | . . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
| 2 | eqid 2765 | . . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
| 3 | eqid 2765 | . . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
| 4 | eqid 2765 | . . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
| 5 | eqid 2765 | . . . 4 ⊢ (.r‘𝑊) = (.r‘𝑊) | |
| 6 | 1, 2, 3, 4, 5 | isassa 21963 | . . 3 ⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑧( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑧( ·𝑠 ‘𝑊)𝑦)) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦))))) |
| 7 | 6 | simplbi 501 | . 2 ⊢ (𝑊 ∈ AssAlg → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring)) |
| 8 | 7 | simprd 500 | 1 ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 = wceq 1563 ∈ wcel 2145 ∀wral 3079 ‘cfv 6525 (class class class)co 7400 Basecbs 17257 .rcmulr 17299 Scalarcsca 17301 ·𝑠 cvsca 17302 Ringcrg 20303 LModclmod 20947 AssAlgcasa 21957 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 ax-nul 5260 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-ne 2961 df-ral 3080 df-rab 3418 df-v 3459 df-sbc 3748 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-iota 6481 df-fv 6533 df-ov 7403 df-assa 21960 |
| This theorem is referenced by: issubassa 21974 assapropd 21978 aspval 21979 asclelbas 21990 asclmul1 21993 asclmul2 21994 ascldimul 21995 asclrhm 21997 rnascl 21998 aspval2 22005 assamulgscmlem1 22006 assamulgscmlem2 22007 asclmulg 22009 zlmassa 22010 mplind 22178 evlseu 22191 pf1subrg 22465 matinv 22791 lactlmhm 33936 assalactf1o 33937 assarrginv 33938 irngnzply1lem 33992 assaascl0 49013 assaascl1 49014 asclelbasALT 49636 |
| Copyright terms: Public domain | W3C validator |