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 2736 | . . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
2 | eqid 2736 | . . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
3 | eqid 2736 | . . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
4 | eqid 2736 | . . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
5 | eqid 2736 | . . . 4 ⊢ (.r‘𝑊) = (.r‘𝑊) | |
6 | 1, 2, 3, 4, 5 | isassa 20772 | . . 3 ⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ (Scalar‘𝑊) ∈ CRing) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑧( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑧( ·𝑠 ‘𝑊)𝑦)) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦))))) |
7 | 6 | simplbi 501 | . 2 ⊢ (𝑊 ∈ AssAlg → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ (Scalar‘𝑊) ∈ CRing)) |
8 | 7 | simp2d 1145 | 1 ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2112 ∀wral 3051 ‘cfv 6358 (class class class)co 7191 Basecbs 16666 .rcmulr 16750 Scalarcsca 16752 ·𝑠 cvsca 16753 Ringcrg 19516 CRingccrg 19517 LModclmod 19853 AssAlgcasa 20766 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-nul 5184 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-sbc 3684 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-br 5040 df-iota 6316 df-fv 6366 df-ov 7194 df-assa 20769 |
This theorem is referenced by: issubassa 20782 assapropd 20785 aspval 20786 asclmul1 20799 asclmul2 20800 ascldimul 20801 ascldimulOLD 20802 asclrhm 20804 rnascl 20805 aspval2 20812 assamulgscmlem1 20813 assamulgscmlem2 20814 zlmassa 20816 mplind 20982 evlseu 20997 pf1subrg 21218 matinv 21528 asclmulg 31334 selvval2lem4 39882 assaascl0 45336 assaascl1 45337 |
Copyright terms: Public domain | W3C validator |