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 ↾ 𝑠 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 = Base R
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 ⊆ Base R
18 14 17 srabase ⊢ φ → Base R = Base W
19 2 18 eqtrid ⊢ φ → A = Base W
20 13 19 sseqtrd ⊢ φ → B ⊆ Base W
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 ⊢ Base W = Base W
31 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
32 29 30 31 islss3 ⊢ W ∈ LMod → B ∈ LSubSp ⁡ W ↔ B ⊆ Base W ∧ W ↾ 𝑠 B ∈ LMod
33 32 biimpar ⊢ W ∈ LMod ∧ B ⊆ Base W ∧ W ↾ 𝑠 B ∈ LMod → B ∈ LSubSp ⁡ W
34 11 20 28 33 syl12anc ⊢ φ → B ∈ LSubSp ⁡ W