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 ⊢ 𝑊 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝐶 )
lsssra.a ⊢ 𝐴 = ( Base ‘ 𝑅 )
lsssra.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐵 )
lsssra.b ⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
lsssra.c ⊢ ( 𝜑 → 𝐶 ∈ ( SubRing ‘ 𝑆 ) )
Assertion lsssra ( 𝜑 → 𝐵 ∈ ( LSubSp ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 lsssra.w ⊢ 𝑊 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝐶 )
2 lsssra.a ⊢ 𝐴 = ( Base ‘ 𝑅 )
3 lsssra.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐵 )
4 lsssra.b ⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
5 lsssra.c ⊢ ( 𝜑 → 𝐶 ∈ ( SubRing ‘ 𝑆 ) )
6 3 subsubrg ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) → ( 𝐶 ∈ ( SubRing ‘ 𝑆 ) ↔ ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐶 ⊆ 𝐵 ) ) )
7 6 biimpa ⊢ ( ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐶 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐶 ⊆ 𝐵 ) )
8 4 5 7 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐶 ⊆ 𝐵 ) )
9 8 simpld ⊢ ( 𝜑 → 𝐶 ∈ ( SubRing ‘ 𝑅 ) )
10 1 sralmod ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) → 𝑊 ∈ LMod )
11 9 10 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
12 2 subrgss ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) → 𝐵 ⊆ 𝐴 )
13 4 12 syl ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
14 1 a1i ⊢ ( 𝜑 → 𝑊 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝐶 ) )
15 8 simprd ⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
16 15 13 sstrd ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
17 16 2 sseqtrdi ⊢ ( 𝜑 → 𝐶 ⊆ ( Base ‘ 𝑅 ) )
18 14 17 srabase ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑊 ) )
19 2 18 eqtrid ⊢ ( 𝜑 → 𝐴 = ( Base ‘ 𝑊 ) )
20 13 19 sseqtrd ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝑊 ) )
21 4 elfvexd ⊢ ( 𝜑 → 𝑅 ∈ V )
22 2 3 13 15 21 resssra ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝑆 ) ‘ 𝐶 ) = ( ( ( subringAlg ‘ 𝑅 ) ‘ 𝐶 ) ↾s 𝐵 ) )
23 1 oveq1i ⊢ ( 𝑊 ↾s 𝐵 ) = ( ( ( subringAlg ‘ 𝑅 ) ‘ 𝐶 ) ↾s 𝐵 )
24 22 23 eqtr4di ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝑆 ) ‘ 𝐶 ) = ( 𝑊 ↾s 𝐵 ) )
25 eqid ⊢ ( ( subringAlg ‘ 𝑆 ) ‘ 𝐶 ) = ( ( subringAlg ‘ 𝑆 ) ‘ 𝐶 )
26 25 sralmod ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝑆 ) → ( ( subringAlg ‘ 𝑆 ) ‘ 𝐶 ) ∈ LMod )
27 5 26 syl ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝑆 ) ‘ 𝐶 ) ∈ LMod )
28 24 27 eqeltrrd ⊢ ( 𝜑 → ( 𝑊 ↾s 𝐵 ) ∈ LMod )
29 eqid ⊢ ( 𝑊 ↾s 𝐵 ) = ( 𝑊 ↾s 𝐵 )
30 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
31 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
32 29 30 31 islss3 ⊢ ( 𝑊 ∈ LMod → ( 𝐵 ∈ ( LSubSp ‘ 𝑊 ) ↔ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ( 𝑊 ↾s 𝐵 ) ∈ LMod ) ) )
33 32 biimpar ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ( 𝑊 ↾s 𝐵 ) ∈ LMod ) ) → 𝐵 ∈ ( LSubSp ‘ 𝑊 ) )
34 11 20 28 33 syl12anc ⊢ ( 𝜑 → 𝐵 ∈ ( LSubSp ‘ 𝑊 ) )