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)

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