Metamath Proof Explorer

Theorem isdrng5

Description: A division ring is a ring in which 1 =/= 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by AV, 23-Jul-2026)

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

Proof

Step Hyp Ref Expression
1 isdrng3.b 
 |-  B = ( Base ` R )
2 isdrng3.0 
 |-  .0. = ( 0g ` R )
3 isdrng3.1 
 |-  .1. = ( 1r ` R )
4 isdrng3.t 
 |-  .x. = ( .r ` R )
5 1 2 3 4 isdrng3 
 |-  ( R e. DivRing <-> ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) )
6 eldifi 
 |-  ( x e. ( B \ { .0. } ) -> x e. B )
7 difss 
 |-  ( B \ { .0. } ) C_ B
8 ssrexv 
 |-  ( ( B \ { .0. } ) C_ B -> ( E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. -> E. y e. B ( y .x. x ) = .1. ) )
9 7 8 ax-mp 
 |-  ( E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. -> E. y e. B ( y .x. x ) = .1. )
10 1 4 2 ringlz 
 |-  ( ( R e. Ring /\ x e. B ) -> ( .0. .x. x ) = .0. )
11 oveq1 
 |-  ( y = .0. -> ( y .x. x ) = ( .0. .x. x ) )
12 11 eqeq1d 
 |-  ( y = .0. -> ( ( y .x. x ) = .0. <-> ( .0. .x. x ) = .0. ) )
13 10 12 syl5ibrcom 
 |-  ( ( R e. Ring /\ x e. B ) -> ( y = .0. -> ( y .x. x ) = .0. ) )
14 13 necon3d 
 |-  ( ( R e. Ring /\ x e. B ) -> ( ( y .x. x ) =/= .0. -> y =/= .0. ) )
15 neeq1 
 |-  ( ( y .x. x ) = .1. -> ( ( y .x. x ) =/= .0. <-> .1. =/= .0. ) )
16 15 biimparc 
 |-  ( ( .1. =/= .0. /\ ( y .x. x ) = .1. ) -> ( y .x. x ) =/= .0. )
17 14 16 impel 
 |-  ( ( ( R e. Ring /\ x e. B ) /\ ( .1. =/= .0. /\ ( y .x. x ) = .1. ) ) -> y =/= .0. )
18 17 an4s 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. ) /\ ( x e. B /\ ( y .x. x ) = .1. ) ) -> y =/= .0. )
19 18 anassrs 
 |-  ( ( ( ( R e. Ring /\ .1. =/= .0. ) /\ x e. B ) /\ ( y .x. x ) = .1. ) -> y =/= .0. )
20 pm3.2 
 |-  ( y e. B -> ( y =/= .0. -> ( y e. B /\ y =/= .0. ) ) )
21 19 20 syl5com 
 |-  ( ( ( ( R e. Ring /\ .1. =/= .0. ) /\ x e. B ) /\ ( y .x. x ) = .1. ) -> ( y e. B -> ( y e. B /\ y =/= .0. ) ) )
22 eldifsn 
 |-  ( y e. ( B \ { .0. } ) <-> ( y e. B /\ y =/= .0. ) )
23 21 22 imbitrrdi 
 |-  ( ( ( ( R e. Ring /\ .1. =/= .0. ) /\ x e. B ) /\ ( y .x. x ) = .1. ) -> ( y e. B -> y e. ( B \ { .0. } ) ) )
24 23 imdistanda 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. ) /\ x e. B ) -> ( ( ( y .x. x ) = .1. /\ y e. B ) -> ( ( y .x. x ) = .1. /\ y e. ( B \ { .0. } ) ) ) )
25 ancom 
 |-  ( ( y e. B /\ ( y .x. x ) = .1. ) <-> ( ( y .x. x ) = .1. /\ y e. B ) )
26 ancom 
 |-  ( ( y e. ( B \ { .0. } ) /\ ( y .x. x ) = .1. ) <-> ( ( y .x. x ) = .1. /\ y e. ( B \ { .0. } ) ) )
27 24 25 26 3imtr4g 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. ) /\ x e. B ) -> ( ( y e. B /\ ( y .x. x ) = .1. ) -> ( y e. ( B \ { .0. } ) /\ ( y .x. x ) = .1. ) ) )
28 27 reximdv2 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. ) /\ x e. B ) -> ( E. y e. B ( y .x. x ) = .1. -> E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) )
29 9 28 impbid2 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. ) /\ x e. B ) -> ( E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. <-> E. y e. B ( y .x. x ) = .1. ) )
30 6 29 sylan2 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. ) /\ x e. ( B \ { .0. } ) ) -> ( E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. <-> E. y e. B ( y .x. x ) = .1. ) )
31 30 ralbidva 
 |-  ( ( R e. Ring /\ .1. =/= .0. ) -> ( A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. <-> A. x e. ( B \ { .0. } ) E. y e. B ( y .x. x ) = .1. ) )
32 31 pm5.32i 
 |-  ( ( ( R e. Ring /\ .1. =/= .0. ) /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) <-> ( ( R e. Ring /\ .1. =/= .0. ) /\ A. x e. ( B \ { .0. } ) E. y e. B ( y .x. x ) = .1. ) )
33 df-3an 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) <-> ( ( R e. Ring /\ .1. =/= .0. ) /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) )
34 df-3an 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( y .x. x ) = .1. ) <-> ( ( R e. Ring /\ .1. =/= .0. ) /\ A. x e. ( B \ { .0. } ) E. y e. B ( y .x. x ) = .1. ) )
35 32 33 34 3bitr4i 
 |-  ( ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. ( B \ { .0. } ) ( y .x. x ) = .1. ) <-> ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( y .x. x ) = .1. ) )
36 5 35 bitri 
 |-  ( R e. DivRing <-> ( R e. Ring /\ .1. =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( y .x. x ) = .1. ) )