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 eqtrid
 |-  ( ( 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 )