Metamath Proof Explorer


Theorem issubassa2

Description: A subring of a unital algebra is a subspace and thus a subalgebra iff it contains all scalar multiples of the identity. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses issubassa2.a A=algScW
issubassa2.l L=LSubSpW
Assertion issubassa2 WAssAlgSSubRingWSLranAS

Proof

Step Hyp Ref Expression
1 issubassa2.a A=algScW
2 issubassa2.l L=LSubSpW
3 eqid 1W=1W
4 eqid LSpanW=LSpanW
5 1 3 4 rnascl WAssAlgranA=LSpanW1W
6 5 ad2antrr WAssAlgSSubRingWSLranA=LSpanW1W
7 assalmod WAssAlgWLMod
8 7 ad2antrr WAssAlgSSubRingWSLWLMod
9 simpr WAssAlgSSubRingWSLSL
10 3 subrg1cl SSubRingW1WS
11 10 ad2antlr WAssAlgSSubRingWSL1WS
12 2 4 8 9 11 lspsnel5a WAssAlgSSubRingWSLLSpanW1WS
13 6 12 eqsstrd WAssAlgSSubRingWSLranAS
14 subrgsubg SSubRingWSSubGrpW
15 14 ad2antlr WAssAlgSSubRingWranASSSubGrpW
16 simplll WAssAlgSSubRingWranASxBaseScalarWySWAssAlg
17 simprl WAssAlgSSubRingWranASxBaseScalarWySxBaseScalarW
18 eqid BaseW=BaseW
19 18 subrgss SSubRingWSBaseW
20 19 ad2antlr WAssAlgSSubRingWranASSBaseW
21 20 sselda WAssAlgSSubRingWranASySyBaseW
22 21 adantrl WAssAlgSSubRingWranASxBaseScalarWySyBaseW
23 eqid ScalarW=ScalarW
24 eqid BaseScalarW=BaseScalarW
25 eqid W=W
26 eqid W=W
27 1 23 24 18 25 26 asclmul1 WAssAlgxBaseScalarWyBaseWAxWy=xWy
28 16 17 22 27 syl3anc WAssAlgSSubRingWranASxBaseScalarWySAxWy=xWy
29 simpllr WAssAlgSSubRingWranASxBaseScalarWySSSubRingW
30 simplr WAssAlgSSubRingWranASxBaseScalarWranAS
31 1 23 24 asclfn AFnBaseScalarW
32 31 a1i WAssAlgSSubRingWranASAFnBaseScalarW
33 fnfvelrn AFnBaseScalarWxBaseScalarWAxranA
34 32 33 sylan WAssAlgSSubRingWranASxBaseScalarWAxranA
35 30 34 sseldd WAssAlgSSubRingWranASxBaseScalarWAxS
36 35 adantrr WAssAlgSSubRingWranASxBaseScalarWySAxS
37 simprr WAssAlgSSubRingWranASxBaseScalarWySyS
38 25 subrgmcl SSubRingWAxSySAxWyS
39 29 36 37 38 syl3anc WAssAlgSSubRingWranASxBaseScalarWySAxWyS
40 28 39 eqeltrrd WAssAlgSSubRingWranASxBaseScalarWySxWyS
41 40 ralrimivva WAssAlgSSubRingWranASxBaseScalarWySxWyS
42 23 24 18 26 2 islss4 WLModSLSSubGrpWxBaseScalarWySxWyS
43 7 42 syl WAssAlgSLSSubGrpWxBaseScalarWySxWyS
44 43 ad2antrr WAssAlgSSubRingWranASSLSSubGrpWxBaseScalarWySxWyS
45 15 41 44 mpbir2and WAssAlgSSubRingWranASSL
46 13 45 impbida WAssAlgSSubRingWSLranAS