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 |`s A )
issubassa.l 
|- L = ( LSubSp ` W )
issubassa.v 
|- V = ( Base ` W )
issubassa.o 
|- .1. = ( 1r ` W )
Assertion issubassa 
|- ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) -> ( S e. AssAlg <-> ( A e. ( SubRing ` W ) /\ A e. L ) ) )

Proof

Step Hyp Ref Expression
1 issubassa.s 
 |-  S = ( W |`s A )
2 issubassa.l 
 |-  L = ( LSubSp ` W )
3 issubassa.v 
 |-  V = ( Base ` W )
4 issubassa.o 
 |-  .1. = ( 1r ` W )
5 simpl1 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> W e. AssAlg )
6 assaring 
 |-  ( W e. AssAlg -> W e. Ring )
7 5 6 syl 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> W e. Ring )
8 assaring 
 |-  ( S e. AssAlg -> S e. Ring )
9 8 adantl 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> S e. Ring )
10 1 9 eqeltrrid 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> ( W |`s A ) e. Ring )
11 simpl3 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> A C_ V )
12 simpl2 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> .1. e. A )
13 11 12 jca 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> ( A C_ V /\ .1. e. A ) )
14 3 4 issubrg 
 |-  ( A e. ( SubRing ` W ) <-> ( ( W e. Ring /\ ( W |`s A ) e. Ring ) /\ ( A C_ V /\ .1. e. A ) ) )
15 7 10 13 14 syl21anbrc 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> A e. ( SubRing ` W ) )
16 assalmod 
 |-  ( S e. AssAlg -> S e. LMod )
17 16 adantl 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> S e. LMod )
18 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
19 1 3 2 islss3 
 |-  ( W e. LMod -> ( A e. L <-> ( A C_ V /\ S e. LMod ) ) )
20 5 18 19 3syl 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> ( A e. L <-> ( A C_ V /\ S e. LMod ) ) )
21 11 17 20 mpbir2and 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> A e. L )
22 15 21 jca 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ S e. AssAlg ) -> ( A e. ( SubRing ` W ) /\ A e. L ) )
23 1 2 issubassa3 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> S e. AssAlg )
24 23 3ad2antl1 
 |-  ( ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> S e. AssAlg )
25 22 24 impbida 
 |-  ( ( W e. AssAlg /\ .1. e. A /\ A C_ V ) -> ( S e. AssAlg <-> ( A e. ( SubRing ` W ) /\ A e. L ) ) )