# Metamath Proof Explorer

## Theorem issubassa

Description: The subalgebras of an associative algebra are exactly the subrings (under the ring multiplication) that are simultaneously subspaces (under the scalar multiplication from the vector space). (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses issubassa.s ${⊢}{S}={W}{↾}_{𝑠}{A}$
issubassa.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
issubassa.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
issubassa.o
Assertion issubassa

### Proof

Step Hyp Ref Expression
1 issubassa.s ${⊢}{S}={W}{↾}_{𝑠}{A}$
2 issubassa.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
3 issubassa.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
4 issubassa.o
5 simpl1
6 assaring ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{Ring}$
7 5 6 syl
8 assaring ${⊢}{S}\in \mathrm{AssAlg}\to {S}\in \mathrm{Ring}$
10 1 9 eqeltrrid
11 simpl3
12 simpl2
13 11 12 jca
14 3 4 issubrg
15 7 10 13 14 syl21anbrc
16 assalmod ${⊢}{S}\in \mathrm{AssAlg}\to {S}\in \mathrm{LMod}$
18 assalmod ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{LMod}$
19 1 3 2 islss3 ${⊢}{W}\in \mathrm{LMod}\to \left({A}\in {L}↔\left({A}\subseteq {V}\wedge {S}\in \mathrm{LMod}\right)\right)$
23 1 2 issubassa3 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({A}\in \mathrm{SubRing}\left({W}\right)\wedge {A}\in {L}\right)\right)\to {S}\in \mathrm{AssAlg}$