Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > assalmod | Structured version Visualization version GIF version |
Description: An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.) |
Ref | Expression |
---|---|
assalmod | ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
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 21074 | . . 3 ⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ (Scalar‘𝑊) ∈ CRing) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑧( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑧( ·𝑠 ‘𝑊)𝑦)) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦))))) |
7 | 6 | simplbi 498 | . 2 ⊢ (𝑊 ∈ AssAlg → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ (Scalar‘𝑊) ∈ CRing)) |
8 | 7 | simp1d 1141 | 1 ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1542 ∈ wcel 2110 ∀wral 3066 ‘cfv 6432 (class class class)co 7272 Basecbs 16923 .rcmulr 16974 Scalarcsca 16976 ·𝑠 cvsca 16977 Ringcrg 19794 CRingccrg 19795 LModclmod 20134 AssAlgcasa 21068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2711 ax-nul 5234 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2072 df-mo 2542 df-eu 2571 df-clab 2718 df-cleq 2732 df-clel 2818 df-ral 3071 df-rex 3072 df-rab 3075 df-v 3433 df-sbc 3721 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4846 df-br 5080 df-iota 6390 df-fv 6440 df-ov 7275 df-assa 21071 |
This theorem is referenced by: assa2ass 21081 issubassa3 21083 issubassa 21084 assapropd 21087 aspval 21088 asplss 21089 ascldimul 21103 asclrhm 21105 rnascl 21106 issubassa2 21107 aspval2 21113 assamulgscmlem1 21114 assamulgscmlem2 21115 mplmon2mul 21288 mplind 21289 matinv 21837 asclmulg 31675 selvval2lem4 40237 assaascl0 45699 assaascl1 45700 |
Copyright terms: Public domain | W3C validator |