Theorem sdrgss

Description: A division subring is a subset of the base set. (Contributed by Thierry Arnoux, 21-Aug-2023)

	Ref	Expression
Hypothesis	sdrgid.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	sdrgss	⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sdrgid.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		issdrg	⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) )
3	1	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )
4	3	3ad2ant2	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) → 𝑆 ⊆ 𝐵 )
5	2 4	sylbi	⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )