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 )