Metamath Proof Explorer

Theorem lsssra

Description: A subring is a subspace of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses lsssra.w 
|- W = ( ( subringAlg ` R ) ` C )
lsssra.a 
|- A = ( Base ` R )
lsssra.s 
|- S = ( R |`s B )
lsssra.b 
|- ( ph -> B e. ( SubRing ` R ) )
lsssra.c 
|- ( ph -> C e. ( SubRing ` S ) )
Assertion lsssra 
|- ( ph -> B e. ( LSubSp ` W ) )

Proof

Step Hyp Ref Expression
1 lsssra.w 
 |-  W = ( ( subringAlg ` R ) ` C )
2 lsssra.a 
 |-  A = ( Base ` R )
3 lsssra.s 
 |-  S = ( R |`s B )
4 lsssra.b 
 |-  ( ph -> B e. ( SubRing ` R ) )
5 lsssra.c 
 |-  ( ph -> C e. ( SubRing ` S ) )
6 3 subsubrg 
 |-  ( B e. ( SubRing ` R ) -> ( C e. ( SubRing ` S ) <-> ( C e. ( SubRing ` R ) /\ C C_ B ) ) )
7 6 biimpa 
 |-  ( ( B e. ( SubRing ` R ) /\ C e. ( SubRing ` S ) ) -> ( C e. ( SubRing ` R ) /\ C C_ B ) )
8 4 5 7 syl2anc 
 |-  ( ph -> ( C e. ( SubRing ` R ) /\ C C_ B ) )
9 8 simpld 
 |-  ( ph -> C e. ( SubRing ` R ) )
10 1 sralmod 
 |-  ( C e. ( SubRing ` R ) -> W e. LMod )
11 9 10 syl 
 |-  ( ph -> W e. LMod )
12 2 subrgss 
 |-  ( B e. ( SubRing ` R ) -> B C_ A )
13 4 12 syl 
 |-  ( ph -> B C_ A )
14 1 a1i 
 |-  ( ph -> W = ( ( subringAlg ` R ) ` C ) )
15 8 simprd 
 |-  ( ph -> C C_ B )
16 15 13 sstrd 
 |-  ( ph -> C C_ A )
17 16 2 sseqtrdi 
 |-  ( ph -> C C_ ( Base ` R ) )
18 14 17 srabase 
 |-  ( ph -> ( Base ` R ) = ( Base ` W ) )
19 2 18 eqtrid 
 |-  ( ph -> A = ( Base ` W ) )
20 13 19 sseqtrd 
 |-  ( ph -> B C_ ( Base ` W ) )
21 4 elfvexd 
 |-  ( ph -> R e. _V )
22 2 3 13 15 21 resssra 
 |-  ( ph -> ( ( subringAlg ` S ) ` C ) = ( ( ( subringAlg ` R ) ` C ) |`s B ) )
23 1 oveq1i 
 |-  ( W |`s B ) = ( ( ( subringAlg ` R ) ` C ) |`s B )
24 22 23 eqtr4di 
 |-  ( ph -> ( ( subringAlg ` S ) ` C ) = ( W |`s B ) )
25 eqid 
 |-  ( ( subringAlg ` S ) ` C ) = ( ( subringAlg ` S ) ` C )
26 25 sralmod 
 |-  ( C e. ( SubRing ` S ) -> ( ( subringAlg ` S ) ` C ) e. LMod )
27 5 26 syl 
 |-  ( ph -> ( ( subringAlg ` S ) ` C ) e. LMod )
28 24 27 eqeltrrd 
 |-  ( ph -> ( W |`s B ) e. LMod )
29 eqid 
 |-  ( W |`s B ) = ( W |`s B )
30 eqid 
 |-  ( Base ` W ) = ( Base ` W )
31 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
32 29 30 31 islss3 
 |-  ( W e. LMod -> ( B e. ( LSubSp ` W ) <-> ( B C_ ( Base ` W ) /\ ( W |`s B ) e. LMod ) ) )
33 32 biimpar 
 |-  ( ( W e. LMod /\ ( B C_ ( Base ` W ) /\ ( W |`s B ) e. LMod ) ) -> B e. ( LSubSp ` W ) )
34 11 20 28 33 syl12anc 
 |-  ( ph -> B e. ( LSubSp ` W ) )