Metamath Proof Explorer

Theorem isdrngrd

Description: Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element x should have a right-inverse I ( x ) . See isdrngd for the characterization using left-inverses. (Contributed by NM, 10-Aug-2013) Remove hypothesis. (Revised by SN, 19-Feb-2025)

Ref Expression
Hypotheses isdrngd.b 
|- ( ph -> B = ( Base ` R ) )
isdrngd.t 
|- ( ph -> .x. = ( .r ` R ) )
isdrngd.z 
|- ( ph -> .0. = ( 0g ` R ) )
isdrngd.u 
|- ( ph -> .1. = ( 1r ` R ) )
isdrngd.r 
|- ( ph -> R e. Ring )
isdrngd.n 
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) =/= .0. )
isdrngd.o 
|- ( ph -> .1. =/= .0. )
isdrngd.i 
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> I e. B )
isdrngrd.k 
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( x .x. I ) = .1. )
Assertion isdrngrd 
|- ( ph -> R e. DivRing )

Proof

Step Hyp Ref Expression
1 isdrngd.b 
 |-  ( ph -> B = ( Base ` R ) )
2 isdrngd.t 
 |-  ( ph -> .x. = ( .r ` R ) )
3 isdrngd.z 
 |-  ( ph -> .0. = ( 0g ` R ) )
4 isdrngd.u 
 |-  ( ph -> .1. = ( 1r ` R ) )
5 isdrngd.r 
 |-  ( ph -> R e. Ring )
6 isdrngd.n 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) =/= .0. )
7 isdrngd.o 
 |-  ( ph -> .1. =/= .0. )
8 isdrngd.i 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> I e. B )
9 isdrngrd.k 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( x .x. I ) = .1. )
10 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 10 11 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` R ) )
13 1 12 eqtrdi 
 |-  ( ph -> B = ( Base ` ( oppR ` R ) ) )
14 eqidd 
 |-  ( ph -> ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) ) )
15 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
16 10 15 oppr0 
 |-  ( 0g ` R ) = ( 0g ` ( oppR ` R ) )
17 3 16 eqtrdi 
 |-  ( ph -> .0. = ( 0g ` ( oppR ` R ) ) )
18 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
19 10 18 oppr1 
 |-  ( 1r ` R ) = ( 1r ` ( oppR ` R ) )
20 4 19 eqtrdi 
 |-  ( ph -> .1. = ( 1r ` ( oppR ` R ) ) )
21 10 opprring 
 |-  ( R e. Ring -> ( oppR ` R ) e. Ring )
22 5 21 syl 
 |-  ( ph -> ( oppR ` R ) e. Ring )
23 eleq1w 
 |-  ( y = x -> ( y e. B <-> x e. B ) )
24 neeq1 
 |-  ( y = x -> ( y =/= .0. <-> x =/= .0. ) )
25 23 24 anbi12d 
 |-  ( y = x -> ( ( y e. B /\ y =/= .0. ) <-> ( x e. B /\ x =/= .0. ) ) )
26 25 3anbi2d 
 |-  ( y = x -> ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) <-> ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) ) )
27 oveq1 
 |-  ( y = x -> ( y ( .r ` ( oppR ` R ) ) z ) = ( x ( .r ` ( oppR ` R ) ) z ) )
28 27 neeq1d 
 |-  ( y = x -> ( ( y ( .r ` ( oppR ` R ) ) z ) =/= .0. <-> ( x ( .r ` ( oppR ` R ) ) z ) =/= .0. ) )
29 26 28 imbi12d 
 |-  ( y = x -> ( ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) z ) =/= .0. ) <-> ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( x ( .r ` ( oppR ` R ) ) z ) =/= .0. ) ) )
30 eleq1w 
 |-  ( x = z -> ( x e. B <-> z e. B ) )
31 neeq1 
 |-  ( x = z -> ( x =/= .0. <-> z =/= .0. ) )
32 30 31 anbi12d 
 |-  ( x = z -> ( ( x e. B /\ x =/= .0. ) <-> ( z e. B /\ z =/= .0. ) ) )
33 32 3anbi3d 
 |-  ( x = z -> ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( x e. B /\ x =/= .0. ) ) <-> ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) ) )
34 oveq2 
 |-  ( x = z -> ( y ( .r ` ( oppR ` R ) ) x ) = ( y ( .r ` ( oppR ` R ) ) z ) )
35 34 neeq1d 
 |-  ( x = z -> ( ( y ( .r ` ( oppR ` R ) ) x ) =/= .0. <-> ( y ( .r ` ( oppR ` R ) ) z ) =/= .0. ) )
36 33 35 imbi12d 
 |-  ( x = z -> ( ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( x e. B /\ x =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) x ) =/= .0. ) <-> ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) z ) =/= .0. ) ) )
37 2 3ad2ant1 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> .x. = ( .r ` R ) )
38 37 oveqd 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) = ( x ( .r ` R ) y ) )
39 eqid 
 |-  ( .r ` R ) = ( .r ` R )
40 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
41 11 39 10 40 opprmul 
 |-  ( y ( .r ` ( oppR ` R ) ) x ) = ( x ( .r ` R ) y )
42 38 41 eqtr4di 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) = ( y ( .r ` ( oppR ` R ) ) x ) )
43 42 6 eqnetrrd 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) x ) =/= .0. )
44 43 3com23 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( x e. B /\ x =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) x ) =/= .0. )
45 36 44 chvarvv 
 |-  ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) z ) =/= .0. )
46 29 45 chvarvv 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( x ( .r ` ( oppR ` R ) ) z ) =/= .0. )
47 11 39 10 40 opprmul 
 |-  ( I ( .r ` ( oppR ` R ) ) x ) = ( x ( .r ` R ) I )
48 2 adantr 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> .x. = ( .r ` R ) )
49 48 oveqd 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( x .x. I ) = ( x ( .r ` R ) I ) )
50 49 9 eqtr3d 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( x ( .r ` R ) I ) = .1. )
51 47 50 eqtrid 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( I ( .r ` ( oppR ` R ) ) x ) = .1. )
52 13 14 17 20 22 46 7 8 51 isdrngd 
 |-  ( ph -> ( oppR ` R ) e. DivRing )
53 10 opprdrng 
 |-  ( R e. DivRing <-> ( oppR ` R ) e. DivRing )
54 52 53 sylibr 
 |-  ( ph -> R e. DivRing )