This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isdrng4

Description: A division ring is a ring in which 1 =/= 0 and every nonzero element has a left and right inverse. (Contributed by Thierry Arnoux, 2-Mar-2025)

Ref Expression
Hypotheses isdrng4.b 
|- B = ( Base ` R )
isdrng4.0 
|- .0. = ( 0g ` R )
isdrng4.1 
|- .1. = ( 1r ` R )
isdrng4.x 
|- .x. = ( .r ` R )
isdrng4.u 
|- U = ( Unit ` R )
isdrng4.r 
|- ( ph -> R e. Ring )
Assertion isdrng4 
|- ( ph -> ( R e. DivRing <-> ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) ) )

Proof

Step Hyp Ref Expression
1 isdrng4.b 
 |-  B = ( Base ` R )
2 isdrng4.0 
 |-  .0. = ( 0g ` R )
3 isdrng4.1 
 |-  .1. = ( 1r ` R )
4 isdrng4.x 
 |-  .x. = ( .r ` R )
5 isdrng4.u 
 |-  U = ( Unit ` R )
6 isdrng4.r 
 |-  ( ph -> R e. Ring )
7 1 5 2 isdrng 
 |-  ( R e. DivRing <-> ( R e. Ring /\ U = ( B \ { .0. } ) ) )
8 6 biantrurd 
 |-  ( ph -> ( U = ( B \ { .0. } ) <-> ( R e. Ring /\ U = ( B \ { .0. } ) ) ) )
9 7 8 bitr4id 
 |-  ( ph -> ( R e. DivRing <-> U = ( B \ { .0. } ) ) )
10 5 3 1unit 
 |-  ( R e. Ring -> .1. e. U )
11 6 10 syl 
 |-  ( ph -> .1. e. U )
12 11 adantr 
 |-  ( ( ph /\ U = ( B \ { .0. } ) ) -> .1. e. U )
13 simpr 
 |-  ( ( ph /\ U = ( B \ { .0. } ) ) -> U = ( B \ { .0. } ) )
14 12 13 eleqtrd 
 |-  ( ( ph /\ U = ( B \ { .0. } ) ) -> .1. e. ( B \ { .0. } ) )
15 eldifsni 
 |-  ( .1. e. ( B \ { .0. } ) -> .1. =/= .0. )
16 14 15 syl 
 |-  ( ( ph /\ U = ( B \ { .0. } ) ) -> .1. =/= .0. )
17 simpll 
 |-  ( ( ( ph /\ U = ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) -> ph )
18 13 eleq2d 
 |-  ( ( ph /\ U = ( B \ { .0. } ) ) -> ( x e. U <-> x e. ( B \ { .0. } ) ) )
19 18 biimpar 
 |-  ( ( ( ph /\ U = ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) -> x e. U )
20 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) /\ z e. B ) /\ ( x .x. z ) = .1. ) -> R e. Ring )
21 1 5 unitcl 
 |-  ( x e. U -> x e. B )
22 21 ad5antlr 
 |-  ( ( ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) /\ z e. B ) /\ ( x .x. z ) = .1. ) -> x e. B )
23 simp-4r 
 |-  ( ( ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) /\ z e. B ) /\ ( x .x. z ) = .1. ) -> y e. B )
24 simplr 
 |-  ( ( ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) /\ z e. B ) /\ ( x .x. z ) = .1. ) -> z e. B )
25 simpllr 
 |-  ( ( ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) /\ z e. B ) /\ ( x .x. z ) = .1. ) -> ( y .x. x ) = .1. )
26 simpr 
 |-  ( ( ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) /\ z e. B ) /\ ( x .x. z ) = .1. ) -> ( x .x. z ) = .1. )
27 1 2 3 4 5 20 22 23 24 25 26 ringinveu 
 |-  ( ( ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) /\ z e. B ) /\ ( x .x. z ) = .1. ) -> z = y )
28 27 oveq2d 
 |-  ( ( ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) /\ z e. B ) /\ ( x .x. z ) = .1. ) -> ( x .x. z ) = ( x .x. y ) )
29 28 26 eqtr3d 
 |-  ( ( ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) /\ z e. B ) /\ ( x .x. z ) = .1. ) -> ( x .x. y ) = .1. )
30 21 ad3antlr 
 |-  ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) -> x e. B )
31 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
32 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
33 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
34 5 3 31 32 33 isunit 
 |-  ( x e. U <-> ( x ( ||r ` R ) .1. /\ x ( ||r ` ( oppR ` R ) ) .1. ) )
35 34 simprbi 
 |-  ( x e. U -> x ( ||r ` ( oppR ` R ) ) .1. )
36 35 ad3antlr 
 |-  ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) -> x ( ||r ` ( oppR ` R ) ) .1. )
37 32 1 opprbas 
 |-  B = ( Base ` ( oppR ` R ) )
38 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
39 37 33 38 dvdsr2 
 |-  ( x e. B -> ( x ( ||r ` ( oppR ` R ) ) .1. <-> E. y e. B ( y ( .r ` ( oppR ` R ) ) x ) = .1. ) )
40 39 biimpa 
 |-  ( ( x e. B /\ x ( ||r ` ( oppR ` R ) ) .1. ) -> E. y e. B ( y ( .r ` ( oppR ` R ) ) x ) = .1. )
41 1 4 32 38 opprmul 
 |-  ( y ( .r ` ( oppR ` R ) ) x ) = ( x .x. y )
42 41 eqeq1i 
 |-  ( ( y ( .r ` ( oppR ` R ) ) x ) = .1. <-> ( x .x. y ) = .1. )
43 42 rexbii 
 |-  ( E. y e. B ( y ( .r ` ( oppR ` R ) ) x ) = .1. <-> E. y e. B ( x .x. y ) = .1. )
44 40 43 sylib 
 |-  ( ( x e. B /\ x ( ||r ` ( oppR ` R ) ) .1. ) -> E. y e. B ( x .x. y ) = .1. )
45 oveq2 
 |-  ( y = z -> ( x .x. y ) = ( x .x. z ) )
46 45 eqeq1d 
 |-  ( y = z -> ( ( x .x. y ) = .1. <-> ( x .x. z ) = .1. ) )
47 46 cbvrexvw 
 |-  ( E. y e. B ( x .x. y ) = .1. <-> E. z e. B ( x .x. z ) = .1. )
48 44 47 sylib 
 |-  ( ( x e. B /\ x ( ||r ` ( oppR ` R ) ) .1. ) -> E. z e. B ( x .x. z ) = .1. )
49 30 36 48 syl2anc 
 |-  ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) -> E. z e. B ( x .x. z ) = .1. )
50 29 49 r19.29a 
 |-  ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) -> ( x .x. y ) = .1. )
51 simpr 
 |-  ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) -> ( y .x. x ) = .1. )
52 50 51 jca 
 |-  ( ( ( ( ph /\ x e. U ) /\ y e. B ) /\ ( y .x. x ) = .1. ) -> ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) )
53 52 anasss 
 |-  ( ( ( ph /\ x e. U ) /\ ( y e. B /\ ( y .x. x ) = .1. ) ) -> ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) )
54 21 adantl 
 |-  ( ( ph /\ x e. U ) -> x e. B )
55 34 simplbi 
 |-  ( x e. U -> x ( ||r ` R ) .1. )
56 55 adantl 
 |-  ( ( ph /\ x e. U ) -> x ( ||r ` R ) .1. )
57 1 31 4 dvdsr2 
 |-  ( x e. B -> ( x ( ||r ` R ) .1. <-> E. y e. B ( y .x. x ) = .1. ) )
58 57 biimpa 
 |-  ( ( x e. B /\ x ( ||r ` R ) .1. ) -> E. y e. B ( y .x. x ) = .1. )
59 54 56 58 syl2anc 
 |-  ( ( ph /\ x e. U ) -> E. y e. B ( y .x. x ) = .1. )
60 53 59 reximddv 
 |-  ( ( ph /\ x e. U ) -> E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) )
61 17 19 60 syl2anc 
 |-  ( ( ( ph /\ U = ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) -> E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) )
62 61 ralrimiva 
 |-  ( ( ph /\ U = ( B \ { .0. } ) ) -> A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) )
63 16 62 jca 
 |-  ( ( ph /\ U = ( B \ { .0. } ) ) -> ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) )
64 1 5 unitss 
 |-  U C_ B
65 64 a1i 
 |-  ( ( ph /\ ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) ) -> U C_ B )
66 6 adantr 
 |-  ( ( ph /\ ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) ) -> R e. Ring )
67 simprl 
 |-  ( ( ph /\ ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) ) -> .1. =/= .0. )
68 5 2 3 0unit 
 |-  ( R e. Ring -> ( .0. e. U <-> .1. = .0. ) )
69 68 necon3bbid 
 |-  ( R e. Ring -> ( -. .0. e. U <-> .1. =/= .0. ) )
70 69 biimpar 
 |-  ( ( R e. Ring /\ .1. =/= .0. ) -> -. .0. e. U )
71 66 67 70 syl2anc 
 |-  ( ( ph /\ ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) ) -> -. .0. e. U )
72 ssdifsn 
 |-  ( U C_ ( B \ { .0. } ) <-> ( U C_ B /\ -. .0. e. U ) )
73 65 71 72 sylanbrc 
 |-  ( ( ph /\ ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) ) -> U C_ ( B \ { .0. } ) )
74 simplr 
 |-  ( ( ( ( ph /\ .1. =/= .0. ) /\ x e. ( B \ { .0. } ) ) /\ E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) -> x e. ( B \ { .0. } ) )
75 74 eldifad 
 |-  ( ( ( ( ph /\ .1. =/= .0. ) /\ x e. ( B \ { .0. } ) ) /\ E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) -> x e. B )
76 simpr 
 |-  ( ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) -> ( y .x. x ) = .1. )
77 76 reximi 
 |-  ( E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) -> E. y e. B ( y .x. x ) = .1. )
78 77 adantl 
 |-  ( ( ( ( ph /\ .1. =/= .0. ) /\ x e. ( B \ { .0. } ) ) /\ E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) -> E. y e. B ( y .x. x ) = .1. )
79 57 biimpar 
 |-  ( ( x e. B /\ E. y e. B ( y .x. x ) = .1. ) -> x ( ||r ` R ) .1. )
80 75 78 79 syl2anc 
 |-  ( ( ( ( ph /\ .1. =/= .0. ) /\ x e. ( B \ { .0. } ) ) /\ E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) -> x ( ||r ` R ) .1. )
81 simpl 
 |-  ( ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) -> ( x .x. y ) = .1. )
82 81 reximi 
 |-  ( E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) -> E. y e. B ( x .x. y ) = .1. )
83 82 adantl 
 |-  ( ( ( ( ph /\ .1. =/= .0. ) /\ x e. ( B \ { .0. } ) ) /\ E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) -> E. y e. B ( x .x. y ) = .1. )
84 83 43 sylibr 
 |-  ( ( ( ( ph /\ .1. =/= .0. ) /\ x e. ( B \ { .0. } ) ) /\ E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) -> E. y e. B ( y ( .r ` ( oppR ` R ) ) x ) = .1. )
85 39 biimpar 
 |-  ( ( x e. B /\ E. y e. B ( y ( .r ` ( oppR ` R ) ) x ) = .1. ) -> x ( ||r ` ( oppR ` R ) ) .1. )
86 75 84 85 syl2anc 
 |-  ( ( ( ( ph /\ .1. =/= .0. ) /\ x e. ( B \ { .0. } ) ) /\ E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) -> x ( ||r ` ( oppR ` R ) ) .1. )
87 80 86 34 sylanbrc 
 |-  ( ( ( ( ph /\ .1. =/= .0. ) /\ x e. ( B \ { .0. } ) ) /\ E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) -> x e. U )
88 87 ex 
 |-  ( ( ( ph /\ .1. =/= .0. ) /\ x e. ( B \ { .0. } ) ) -> ( E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) -> x e. U ) )
89 88 ralimdva 
 |-  ( ( ph /\ .1. =/= .0. ) -> ( A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) -> A. x e. ( B \ { .0. } ) x e. U ) )
90 89 impr 
 |-  ( ( ph /\ ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) ) -> A. x e. ( B \ { .0. } ) x e. U )
91 dfss3 
 |-  ( ( B \ { .0. } ) C_ U <-> A. x e. ( B \ { .0. } ) x e. U )
92 90 91 sylibr 
 |-  ( ( ph /\ ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) ) -> ( B \ { .0. } ) C_ U )
93 73 92 eqssd 
 |-  ( ( ph /\ ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) ) -> U = ( B \ { .0. } ) )
94 63 93 impbida 
 |-  ( ph -> ( U = ( B \ { .0. } ) <-> ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) ) )
95 9 94 bitrd 
 |-  ( ph -> ( R e. DivRing <-> ( .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x .x. y ) = .1. /\ ( y .x. x ) = .1. ) ) ) )