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