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 = ( algSc ` W )
issubassa2.l 
|- L = ( LSubSp ` W )
Assertion issubassa2 
|- ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) -> ( S e. L <-> ran A C_ S ) )

Proof

Step Hyp Ref Expression
1 issubassa2.a 
 |-  A = ( algSc ` W )
2 issubassa2.l 
 |-  L = ( LSubSp ` W )
3 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
4 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
5 1 3 4 rnascl 
 |-  ( W e. AssAlg -> ran A = ( ( LSpan ` W ) ` { ( 1r ` W ) } ) )
6 5 ad2antrr 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ S e. L ) -> ran A = ( ( LSpan ` W ) ` { ( 1r ` W ) } ) )
7 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
8 7 ad2antrr 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ S e. L ) -> W e. LMod )
9 simpr 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ S e. L ) -> S e. L )
10 3 subrg1cl 
 |-  ( S e. ( SubRing ` W ) -> ( 1r ` W ) e. S )
11 10 ad2antlr 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ S e. L ) -> ( 1r ` W ) e. S )
12 2 4 8 9 11 lspsnel5a 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ S e. L ) -> ( ( LSpan ` W ) ` { ( 1r ` W ) } ) C_ S )
13 6 12 eqsstrd 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ S e. L ) -> ran A C_ S )
14 subrgsubg 
 |-  ( S e. ( SubRing ` W ) -> S e. ( SubGrp ` W ) )
15 14 ad2antlr 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) -> S e. ( SubGrp ` W ) )
16 simplll 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. S ) ) -> W e. AssAlg )
17 simprl 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. S ) ) -> x e. ( Base ` ( Scalar ` W ) ) )
18 eqid 
 |-  ( Base ` W ) = ( Base ` W )
19 18 subrgss 
 |-  ( S e. ( SubRing ` W ) -> S C_ ( Base ` W ) )
20 19 ad2antlr 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) -> S C_ ( Base ` W ) )
21 20 sselda 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ y e. S ) -> y e. ( Base ` W ) )
22 21 adantrl 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. S ) ) -> y e. ( Base ` W ) )
23 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
24 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
25 eqid 
 |-  ( .r ` W ) = ( .r ` W )
26 eqid 
 |-  ( .s ` W ) = ( .s ` W )
27 1 23 24 18 25 26 asclmul1 
 |-  ( ( W e. AssAlg /\ x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) ) -> ( ( A ` x ) ( .r ` W ) y ) = ( x ( .s ` W ) y ) )
28 16 17 22 27 syl3anc 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. S ) ) -> ( ( A ` x ) ( .r ` W ) y ) = ( x ( .s ` W ) y ) )
29 simpllr 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. S ) ) -> S e. ( SubRing ` W ) )
30 simplr 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ x e. ( Base ` ( Scalar ` W ) ) ) -> ran A C_ S )
31 1 23 24 asclfn 
 |-  A Fn ( Base ` ( Scalar ` W ) )
32 31 a1i 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) -> A Fn ( Base ` ( Scalar ` W ) ) )
33 fnfvelrn 
 |-  ( ( A Fn ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` ( Scalar ` W ) ) ) -> ( A ` x ) e. ran A )
34 32 33 sylan 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ x e. ( Base ` ( Scalar ` W ) ) ) -> ( A ` x ) e. ran A )
35 30 34 sseldd 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ x e. ( Base ` ( Scalar ` W ) ) ) -> ( A ` x ) e. S )
36 35 adantrr 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. S ) ) -> ( A ` x ) e. S )
37 simprr 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. S ) ) -> y e. S )
38 25 subrgmcl 
 |-  ( ( S e. ( SubRing ` W ) /\ ( A ` x ) e. S /\ y e. S ) -> ( ( A ` x ) ( .r ` W ) y ) e. S )
39 29 36 37 38 syl3anc 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. S ) ) -> ( ( A ` x ) ( .r ` W ) y ) e. S )
40 28 39 eqeltrrd 
 |-  ( ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. S ) ) -> ( x ( .s ` W ) y ) e. S )
41 40 ralrimivva 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) -> A. x e. ( Base ` ( Scalar ` W ) ) A. y e. S ( x ( .s ` W ) y ) e. S )
42 23 24 18 26 2 islss4 
 |-  ( W e. LMod -> ( S e. L <-> ( S e. ( SubGrp ` W ) /\ A. x e. ( Base ` ( Scalar ` W ) ) A. y e. S ( x ( .s ` W ) y ) e. S ) ) )
43 7 42 syl 
 |-  ( W e. AssAlg -> ( S e. L <-> ( S e. ( SubGrp ` W ) /\ A. x e. ( Base ` ( Scalar ` W ) ) A. y e. S ( x ( .s ` W ) y ) e. S ) ) )
44 43 ad2antrr 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) -> ( S e. L <-> ( S e. ( SubGrp ` W ) /\ A. x e. ( Base ` ( Scalar ` W ) ) A. y e. S ( x ( .s ` W ) y ) e. S ) ) )
45 15 41 44 mpbir2and 
 |-  ( ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) /\ ran A C_ S ) -> S e. L )
46 13 45 impbida 
 |-  ( ( W e. AssAlg /\ S e. ( SubRing ` W ) ) -> ( S e. L <-> ran A C_ S ) )