Theorem isdrng3

Description: A division ring is a ring in which 1 =/= 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by AV, 22-Jul-2026)

	Ref	Expression
Hypotheses	isdrng3.b	|- B = ( Base ` R )
	isdrng3.0	|- .0. = ( 0g ` R )
	isdrng3.1	|- .1. = ( 1r ` R )
	isdrng3.t	|- .x. = ( .r ` R )
Assertion	isdrng3	|- ( R e. DivRing <-> ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) )

Proof

Step	Hyp	Ref	Expression
1		isdrng3.b	|- B = ( Base ` R )
2		isdrng3.0	|- .0. = ( 0g ` R )
3		isdrng3.1	|- .1. = ( 1r ` R )
4		isdrng3.t	|- .x. = ( .r ` R )
5		eqid	|- ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
6	1 2 5	isdrng2	|- ( R e. DivRing <-> ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) )
7	2 3	drngunz	|- ( R e. DivRing -> .1. =/= .0. )
8	6 7	sylbir	|- ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) -> .1. =/= .0. )
9	1 2 3 4	isdrng3lem1	|- ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) -> A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. )
10	8 9	jca	|- ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) -> ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) )
11		3anass	|- ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) <-> ( R e. Ring /\ ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) ) )
12	1 2 3 4	isdrng3lem2	|- ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) -> ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp )
13	11 12	sylbir	|- ( ( R e. Ring /\ ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) ) -> ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp )
14	10 13	impbida	|- ( R e. Ring -> ( ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp <-> ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) ) )
15	14	pm5.32i	|- ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) <-> ( R e. Ring /\ ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) ) )
16	15 6 11	3bitr4i	|- ( R e. DivRing <-> ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) )