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=BaseR
lsssra.s ⊢S=R↾𝑠B
lsssra.b ⊢φ→B∈SubRing⁡R
lsssra.c ⊢φ→C∈SubRing⁡S
Assertion lsssra ⊢φ→B∈LSubSp⁡W

Proof

Step Hyp Ref Expression
1 lsssra.w ⊢W=subringAlg⁡R⁡C
2 lsssra.a ⊢A=BaseR
3 lsssra.s ⊢S=R↾𝑠B
4 lsssra.b ⊢φ→B∈SubRing⁡R
5 lsssra.c ⊢φ→C∈SubRing⁡S
6 3 subsubrg ⊢B∈SubRing⁡R→C∈SubRing⁡S↔C∈SubRing⁡R∧C⊆B
7 6 biimpa ⊢B∈SubRing⁡R∧C∈SubRing⁡S→C∈SubRing⁡R∧C⊆B
8 4 5 7 syl2anc ⊢φ→C∈SubRing⁡R∧C⊆B
9 8 simpld ⊢φ→C∈SubRing⁡R
10 1 sralmod ⊢C∈SubRing⁡R→W∈LMod
11 9 10 syl ⊢φ→W∈LMod
12 2 subrgss ⊢B∈SubRing⁡R→B⊆A
13 4 12 syl ⊢φ→B⊆A
14 1 a1i ⊢φ→W=subringAlg⁡R⁡C
15 8 simprd ⊢φ→C⊆B
16 15 13 sstrd ⊢φ→C⊆A
17 16 2 sseqtrdi ⊢φ→C⊆BaseR
18 14 17 srabase ⊢φ→BaseR=BaseW
19 2 18 eqtrid ⊢φ→A=BaseW
20 13 19 sseqtrd ⊢φ→B⊆BaseW
21 4 elfvexd ⊢φ→R∈V
22 2 3 13 15 21 resssra ⊢φ→subringAlg⁡S⁡C=subringAlg⁡R⁡C↾𝑠B
23 1 oveq1i ⊢W↾𝑠B=subringAlg⁡R⁡C↾𝑠B
24 22 23 eqtr4di ⊢φ→subringAlg⁡S⁡C=W↾𝑠B
25 eqid ⊢subringAlg⁡S⁡C=subringAlg⁡S⁡C
26 25 sralmod ⊢C∈SubRing⁡S→subringAlg⁡S⁡C∈LMod
27 5 26 syl ⊢φ→subringAlg⁡S⁡C∈LMod
28 24 27 eqeltrrd ⊢φ→W↾𝑠B∈LMod
29 eqid ⊢W↾𝑠B=W↾𝑠B
30 eqid ⊢BaseW=BaseW
31 eqid ⊢LSubSp⁡W=LSubSp⁡W
32 29 30 31 islss3 ⊢W∈LMod→B∈LSubSp⁡W↔B⊆BaseW∧W↾𝑠B∈LMod
33 32 biimpar ⊢W∈LMod∧B⊆BaseW∧W↾𝑠B∈LMod→B∈LSubSp⁡W
34 11 20 28 33 syl12anc ⊢φ→B∈LSubSp⁡W