Theorem sdrgid

Description: Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		sdrgid.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		id	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ DivRing )
3		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
4	1	subrgid	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
5	3 4	syl	⊢ ( 𝑅 ∈ DivRing → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
6	1	ressid	⊢ ( 𝑅 ∈ DivRing → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
7	6 2	eqeltrd	⊢ ( 𝑅 ∈ DivRing → ( 𝑅 ↾s 𝐵 ) ∈ DivRing )
8		issdrg	⊢ ( 𝐵 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝐵 ) ∈ DivRing ) )
9	2 5 7 8	syl3anbrc	⊢ ( 𝑅 ∈ DivRing → 𝐵 ∈ ( SubDRing ‘ 𝑅 ) )