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	|- B = ( Base ` R )
	isdrng2.z	|- .0. = ( 0g ` R )
	isdrng2.g	|- G = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
Assertion	drngprops	|- ( R e. DivRing -> ( R e. Ring /\ G e. Grp ) )

Proof

Step	Hyp	Ref	Expression
1		isdrng2.b	|- B = ( Base ` R )
2		isdrng2.z	|- .0. = ( 0g ` R )
3		isdrng2.g	|- G = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
4		eqid	|- ( Unit ` R ) = ( Unit ` R )
5	1 4 2	isdrng	|- ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) ) )
6		simpl	|- ( ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) ) -> R e. Ring )
7		oveq2	|- ( ( Unit ` R ) = ( B \ { .0. } ) -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) )
8	7	adantl	|- ( ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) ) -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) )
9	8 3	eqtr4di	|- ( ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) ) -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) = G )
10		eqid	|- ( ( mulGrp ` R ) |`s ( Unit ` R ) ) = ( ( mulGrp ` R ) |`s ( Unit ` R ) )
11	4 10	unitgrp	|- ( R e. Ring -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. Grp )
12	11	adantr	|- ( ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) ) -> ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. Grp )
13	9 12	eqeltrrd	|- ( ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) ) -> G e. Grp )
14	6 13	jca	|- ( ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) ) -> ( R e. Ring /\ G e. Grp ) )
15	5 14	sylbi	|- ( R e. DivRing -> ( R e. Ring /\ G e. Grp ) )