Metamath Proof Explorer


Theorem isdrngd

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 left-inverse I ( x ) . See isdrngd for the characterization using right-inverses. (Contributed by NM, 2-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. )
isdrngd.k
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( I .x. x ) = .1. )
Assertion isdrngd
|- ( 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 isdrngd.k
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( I .x. x ) = .1. )
11 difss
 |-  ( B \ { .0. } ) C_ B
12 11 1 sseqtrid
 |-  ( ph -> ( B \ { .0. } ) C_ ( Base ` R ) )
13 eqid
 |-  ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
14 eqid
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
15 eqid
 |-  ( Base ` R ) = ( Base ` R )
16 14 15 mgpbas
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
17 13 16 ressbas2
 |-  ( ( B \ { .0. } ) C_ ( Base ` R ) -> ( B \ { .0. } ) = ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
18 12 17 syl
 |-  ( ph -> ( B \ { .0. } ) = ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
19 fvex
 |-  ( Base ` R ) e. _V
20 1 19 eqeltrdi
 |-  ( ph -> B e. _V )
21 difexg
 |-  ( B e. _V -> ( B \ { .0. } ) e. _V )
22 eqid
 |-  ( .r ` R ) = ( .r ` R )
23 14 22 mgpplusg
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
24 13 23 ressplusg
 |-  ( ( B \ { .0. } ) e. _V -> ( .r ` R ) = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
25 20 21 24 3syl
 |-  ( ph -> ( .r ` R ) = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
26 2 25 eqtrd
 |-  ( ph -> .x. = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) )
27 eldifsn
 |-  ( x e. ( B \ { .0. } ) <-> ( x e. B /\ x =/= .0. ) )
28 eldifsn
 |-  ( y e. ( B \ { .0. } ) <-> ( y e. B /\ y =/= .0. ) )
29 15 22 ringcl
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) )
30 5 29 syl3an1
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) )
31 30 3expib
 |-  ( ph -> ( ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) ) )
32 1 eleq2d
 |-  ( ph -> ( x e. B <-> x e. ( Base ` R ) ) )
33 1 eleq2d
 |-  ( ph -> ( y e. B <-> y e. ( Base ` R ) ) )
34 32 33 anbi12d
 |-  ( ph -> ( ( x e. B /\ y e. B ) <-> ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) )
35 2 oveqd
 |-  ( ph -> ( x .x. y ) = ( x ( .r ` R ) y ) )
36 35 1 eleq12d
 |-  ( ph -> ( ( x .x. y ) e. B <-> ( x ( .r ` R ) y ) e. ( Base ` R ) ) )
37 31 34 36 3imtr4d
 |-  ( ph -> ( ( x e. B /\ y e. B ) -> ( x .x. y ) e. B ) )
38 37 3impib
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) e. B )
39 38 3adant2r
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ y e. B ) -> ( x .x. y ) e. B )
40 39 3adant3r
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) e. B )
41 eldifsn
 |-  ( ( x .x. y ) e. ( B \ { .0. } ) <-> ( ( x .x. y ) e. B /\ ( x .x. y ) =/= .0. ) )
42 40 6 41 sylanbrc
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) e. ( B \ { .0. } ) )
43 28 42 syl3an3b
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ y e. ( B \ { .0. } ) ) -> ( x .x. y ) e. ( B \ { .0. } ) )
44 27 43 syl3an2b
 |-  ( ( ph /\ x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) -> ( x .x. y ) e. ( B \ { .0. } ) )
45 15 22 ringass
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) )
46 45 ex
 |-  ( R e. Ring -> ( ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) ) )
47 5 46 syl
 |-  ( ph -> ( ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) ) )
48 1 eleq2d
 |-  ( ph -> ( z e. B <-> z e. ( Base ` R ) ) )
49 32 33 48 3anbi123d
 |-  ( ph -> ( ( x e. B /\ y e. B /\ z e. B ) <-> ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) )
50 eqidd
 |-  ( ph -> z = z )
51 2 35 50 oveq123d
 |-  ( ph -> ( ( x .x. y ) .x. z ) = ( ( x ( .r ` R ) y ) ( .r ` R ) z ) )
52 eqidd
 |-  ( ph -> x = x )
53 2 oveqd
 |-  ( ph -> ( y .x. z ) = ( y ( .r ` R ) z ) )
54 2 52 53 oveq123d
 |-  ( ph -> ( x .x. ( y .x. z ) ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) )
55 51 54 eqeq12d
 |-  ( ph -> ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) <-> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) ) )
56 47 49 55 3imtr4d
 |-  ( ph -> ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) )
57 eldifi
 |-  ( x e. ( B \ { .0. } ) -> x e. B )
58 eldifi
 |-  ( y e. ( B \ { .0. } ) -> y e. B )
59 eldifi
 |-  ( z e. ( B \ { .0. } ) -> z e. B )
60 57 58 59 3anim123i
 |-  ( ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) /\ z e. ( B \ { .0. } ) ) -> ( x e. B /\ y e. B /\ z e. B ) )
61 56 60 impel
 |-  ( ( ph /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) /\ z e. ( B \ { .0. } ) ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) )
62 eqid
 |-  ( 1r ` R ) = ( 1r ` R )
63 15 62 ringidcl
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
64 5 63 syl
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
65 64 4 1 3eltr4d
 |-  ( ph -> .1. e. B )
66 eldifsn
 |-  ( .1. e. ( B \ { .0. } ) <-> ( .1. e. B /\ .1. =/= .0. ) )
67 65 7 66 sylanbrc
 |-  ( ph -> .1. e. ( B \ { .0. } ) )
68 15 22 62 ringlidm
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x )
69 68 ex
 |-  ( R e. Ring -> ( x e. ( Base ` R ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x ) )
70 5 69 syl
 |-  ( ph -> ( x e. ( Base ` R ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x ) )
71 2 4 52 oveq123d
 |-  ( ph -> ( .1. .x. x ) = ( ( 1r ` R ) ( .r ` R ) x ) )
72 71 eqeq1d
 |-  ( ph -> ( ( .1. .x. x ) = x <-> ( ( 1r ` R ) ( .r ` R ) x ) = x ) )
73 70 32 72 3imtr4d
 |-  ( ph -> ( x e. B -> ( .1. .x. x ) = x ) )
74 73 imp
 |-  ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x )
75 74 adantrr
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( .1. .x. x ) = x )
76 27 75 sylan2b
 |-  ( ( ph /\ x e. ( B \ { .0. } ) ) -> ( .1. .x. x ) = x )
77 eldifsn
 |-  ( I e. ( B \ { .0. } ) <-> ( I e. B /\ I =/= .0. ) )
78 8 9 77 sylanbrc
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> I e. ( B \ { .0. } ) )
79 27 78 sylan2b
 |-  ( ( ph /\ x e. ( B \ { .0. } ) ) -> I e. ( B \ { .0. } ) )
80 27 10 sylan2b
 |-  ( ( ph /\ x e. ( B \ { .0. } ) ) -> ( I .x. x ) = .1. )
81 18 26 44 61 67 76 79 80 isgrpd
 |-  ( ph -> ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp )
82 3 sneqd
 |-  ( ph -> { .0. } = { ( 0g ` R ) } )
83 1 82 difeq12d
 |-  ( ph -> ( B \ { .0. } ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) )
84 83 oveq2d
 |-  ( ph -> ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) = ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) )
85 84 eleq1d
 |-  ( ph -> ( ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp <-> ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) e. Grp ) )
86 85 anbi2d
 |-  ( ph -> ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) <-> ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) e. Grp ) ) )
87 5 81 86 mpbi2and
 |-  ( ph -> ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) e. Grp ) )
88 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
89 eqid
 |-  ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) = ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) )
90 15 88 89 isdrng2
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) e. Grp ) )
91 87 90 sylibr
 |-  ( ph -> R e. DivRing )