Theorem drngprops

Description: Properties of a division ring. (Contributed by NM, 4-Apr-2009) (Revised by AV, 26-Aug-2026)

	Ref	Expression
Hypotheses	isdrng2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isdrng2.z	⊢ 0 = ( 0g ‘ 𝑅 )
	isdrng2.g	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
Assertion	drngprops	⊢ ( 𝑅 ∈ DivRing → ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) )

Proof

Step	Hyp	Ref	Expression
1		isdrng2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isdrng2.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		isdrng2.g	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
4		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
5	1 4 2	isdrng	⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) ) )
6		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) ) → 𝑅 ∈ Ring )
7		oveq2	⊢ ( ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
8	7	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
9	8 3	eqtr4di	⊢ ( ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) = 𝐺 )
10		eqid	⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
11	4 10	unitgrp	⊢ ( 𝑅 ∈ Ring → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ Grp )
12	11	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ Grp )
13	9 12	eqeltrrd	⊢ ( ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) ) → 𝐺 ∈ Grp )
14	6 13	jca	⊢ ( ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) ) → ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) )
15	5 14	sylbi	⊢ ( 𝑅 ∈ DivRing → ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) )