Metamath Proof Explorer

Theorem issubassa3

Description: A subring that is also a subspace is a subalgebra. The key theorem is islss3 . (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses issubassa.s 
|- S = ( W |`s A )
issubassa.l 
|- L = ( LSubSp ` W )
Assertion issubassa3 
|- ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> S e. AssAlg )

Proof

Step Hyp Ref Expression
1 issubassa.s 
 |-  S = ( W |`s A )
2 issubassa.l 
 |-  L = ( LSubSp ` W )
3 1 subrgbas 
 |-  ( A e. ( SubRing ` W ) -> A = ( Base ` S ) )
4 3 ad2antrl 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> A = ( Base ` S ) )
5 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
6 1 5 resssca 
 |-  ( A e. ( SubRing ` W ) -> ( Scalar ` W ) = ( Scalar ` S ) )
7 6 ad2antrl 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> ( Scalar ` W ) = ( Scalar ` S ) )
8 eqidd 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) )
9 eqid 
 |-  ( .s ` W ) = ( .s ` W )
10 1 9 ressvsca 
 |-  ( A e. ( SubRing ` W ) -> ( .s ` W ) = ( .s ` S ) )
11 10 ad2antrl 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> ( .s ` W ) = ( .s ` S ) )
12 eqid 
 |-  ( .r ` W ) = ( .r ` W )
13 1 12 ressmulr 
 |-  ( A e. ( SubRing ` W ) -> ( .r ` W ) = ( .r ` S ) )
14 13 ad2antrl 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> ( .r ` W ) = ( .r ` S ) )
15 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
16 simpr 
 |-  ( ( A e. ( SubRing ` W ) /\ A e. L ) -> A e. L )
17 1 2 lsslmod 
 |-  ( ( W e. LMod /\ A e. L ) -> S e. LMod )
18 15 16 17 syl2an 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> S e. LMod )
19 1 subrgring 
 |-  ( A e. ( SubRing ` W ) -> S e. Ring )
20 19 ad2antrl 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> S e. Ring )
21 5 assasca 
 |-  ( W e. AssAlg -> ( Scalar ` W ) e. CRing )
22 21 adantr 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> ( Scalar ` W ) e. CRing )
23 idd 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> ( x e. ( Base ` ( Scalar ` W ) ) -> x e. ( Base ` ( Scalar ` W ) ) ) )
24 eqid 
 |-  ( Base ` W ) = ( Base ` W )
25 24 subrgss 
 |-  ( A e. ( SubRing ` W ) -> A C_ ( Base ` W ) )
26 25 ad2antrl 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> A C_ ( Base ` W ) )
27 26 sseld 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> ( y e. A -> y e. ( Base ` W ) ) )
28 26 sseld 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> ( z e. A -> z e. ( Base ` W ) ) )
29 23 27 28 3anim123d 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> ( ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. A /\ z e. A ) -> ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) )
30 29 imp 
 |-  ( ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. A /\ z e. A ) ) -> ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) )
31 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
32 24 5 31 9 12 assaass 
 |-  ( ( W e. AssAlg /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( x ( .s ` W ) y ) ( .r ` W ) z ) = ( x ( .s ` W ) ( y ( .r ` W ) z ) ) )
33 32 adantlr 
 |-  ( ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( x ( .s ` W ) y ) ( .r ` W ) z ) = ( x ( .s ` W ) ( y ( .r ` W ) z ) ) )
34 30 33 syldan 
 |-  ( ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. A /\ z e. A ) ) -> ( ( x ( .s ` W ) y ) ( .r ` W ) z ) = ( x ( .s ` W ) ( y ( .r ` W ) z ) ) )
35 24 5 31 9 12 assaassr 
 |-  ( ( W e. AssAlg /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( y ( .r ` W ) ( x ( .s ` W ) z ) ) = ( x ( .s ` W ) ( y ( .r ` W ) z ) ) )
36 35 adantlr 
 |-  ( ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( y ( .r ` W ) ( x ( .s ` W ) z ) ) = ( x ( .s ` W ) ( y ( .r ` W ) z ) ) )
37 30 36 syldan 
 |-  ( ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. A /\ z e. A ) ) -> ( y ( .r ` W ) ( x ( .s ` W ) z ) ) = ( x ( .s ` W ) ( y ( .r ` W ) z ) ) )
38 4 7 8 11 14 18 20 22 34 37 isassad 
 |-  ( ( W e. AssAlg /\ ( A e. ( SubRing ` W ) /\ A e. L ) ) -> S e. AssAlg )