Metamath Proof Explorer

Theorem drnglring

Description: A division ring is a local ring. (Contributed by Thierry Arnoux, 2-Jun-2026)

Ref Expression
Hypothesis drnglring.1 
|- ( ph -> F e. DivRing )
Assertion drnglring 
|- ( ph -> F e. LRing )

Proof

Step Hyp Ref Expression
1 drnglring.1 
 |-  ( ph -> F e. DivRing )
2 drngnzr 
 |-  ( F e. DivRing -> F e. NzRing )
3 1 2 syl 
 |-  ( ph -> F e. NzRing )
4 1 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) /\ -. x = ( 0g ` F ) ) -> F e. DivRing )
5 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) /\ -. x = ( 0g ` F ) ) -> x e. ( Base ` F ) )
6 neqne 
 |-  ( -. x = ( 0g ` F ) -> x =/= ( 0g ` F ) )
7 6 adantl 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) /\ -. x = ( 0g ` F ) ) -> x =/= ( 0g ` F ) )
8 eqid 
 |-  ( Base ` F ) = ( Base ` F )
9 eqid 
 |-  ( Unit ` F ) = ( Unit ` F )
10 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
11 8 9 10 drngunit 
 |-  ( F e. DivRing -> ( x e. ( Unit ` F ) <-> ( x e. ( Base ` F ) /\ x =/= ( 0g ` F ) ) ) )
12 11 biimpar 
 |-  ( ( F e. DivRing /\ ( x e. ( Base ` F ) /\ x =/= ( 0g ` F ) ) ) -> x e. ( Unit ` F ) )
13 4 5 7 12 syl12anc 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) /\ -. x = ( 0g ` F ) ) -> x e. ( Unit ` F ) )
14 1 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) /\ -. y = ( 0g ` F ) ) -> F e. DivRing )
15 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) /\ -. y = ( 0g ` F ) ) -> y e. ( Base ` F ) )
16 neqne 
 |-  ( -. y = ( 0g ` F ) -> y =/= ( 0g ` F ) )
17 16 adantl 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) /\ -. y = ( 0g ` F ) ) -> y =/= ( 0g ` F ) )
18 8 9 10 drngunit 
 |-  ( F e. DivRing -> ( y e. ( Unit ` F ) <-> ( y e. ( Base ` F ) /\ y =/= ( 0g ` F ) ) ) )
19 18 biimpar 
 |-  ( ( F e. DivRing /\ ( y e. ( Base ` F ) /\ y =/= ( 0g ` F ) ) ) -> y e. ( Unit ` F ) )
20 14 15 17 19 syl12anc 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) /\ -. y = ( 0g ` F ) ) -> y e. ( Unit ` F ) )
21 simplll 
 |-  ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) -> ph )
22 simpr 
 |-  ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) -> ( x ( +g ` F ) y ) = ( 1r ` F ) )
23 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
24 23 10 nzrnz 
 |-  ( F e. NzRing -> ( 1r ` F ) =/= ( 0g ` F ) )
25 3 24 syl 
 |-  ( ph -> ( 1r ` F ) =/= ( 0g ` F ) )
26 25 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) -> ( 1r ` F ) =/= ( 0g ` F ) )
27 22 26 eqnetrd 
 |-  ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) -> ( x ( +g ` F ) y ) =/= ( 0g ` F ) )
28 27 neneqd 
 |-  ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) -> -. ( x ( +g ` F ) y ) = ( 0g ` F ) )
29 oveq12 
 |-  ( ( x = ( 0g ` F ) /\ y = ( 0g ` F ) ) -> ( x ( +g ` F ) y ) = ( ( 0g ` F ) ( +g ` F ) ( 0g ` F ) ) )
30 29 adantl 
 |-  ( ( ph /\ ( x = ( 0g ` F ) /\ y = ( 0g ` F ) ) ) -> ( x ( +g ` F ) y ) = ( ( 0g ` F ) ( +g ` F ) ( 0g ` F ) ) )
31 eqid 
 |-  ( +g ` F ) = ( +g ` F )
32 1 drnggrpd 
 |-  ( ph -> F e. Grp )
33 32 adantr 
 |-  ( ( ph /\ ( x = ( 0g ` F ) /\ y = ( 0g ` F ) ) ) -> F e. Grp )
34 8 10 33 grpidcld 
 |-  ( ( ph /\ ( x = ( 0g ` F ) /\ y = ( 0g ` F ) ) ) -> ( 0g ` F ) e. ( Base ` F ) )
35 8 31 10 33 34 grplidd 
 |-  ( ( ph /\ ( x = ( 0g ` F ) /\ y = ( 0g ` F ) ) ) -> ( ( 0g ` F ) ( +g ` F ) ( 0g ` F ) ) = ( 0g ` F ) )
36 30 35 eqtrd 
 |-  ( ( ph /\ ( x = ( 0g ` F ) /\ y = ( 0g ` F ) ) ) -> ( x ( +g ` F ) y ) = ( 0g ` F ) )
37 36 stoic1a 
 |-  ( ( ph /\ -. ( x ( +g ` F ) y ) = ( 0g ` F ) ) -> -. ( x = ( 0g ` F ) /\ y = ( 0g ` F ) ) )
38 21 28 37 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) -> -. ( x = ( 0g ` F ) /\ y = ( 0g ` F ) ) )
39 ianor 
 |-  ( -. ( x = ( 0g ` F ) /\ y = ( 0g ` F ) ) <-> ( -. x = ( 0g ` F ) \/ -. y = ( 0g ` F ) ) )
40 38 39 sylib 
 |-  ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) -> ( -. x = ( 0g ` F ) \/ -. y = ( 0g ` F ) ) )
41 13 20 40 orim12da 
 |-  ( ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) /\ ( x ( +g ` F ) y ) = ( 1r ` F ) ) -> ( x e. ( Unit ` F ) \/ y e. ( Unit ` F ) ) )
42 41 ex 
 |-  ( ( ( ph /\ x e. ( Base ` F ) ) /\ y e. ( Base ` F ) ) -> ( ( x ( +g ` F ) y ) = ( 1r ` F ) -> ( x e. ( Unit ` F ) \/ y e. ( Unit ` F ) ) ) )
43 42 anasss 
 |-  ( ( ph /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> ( ( x ( +g ` F ) y ) = ( 1r ` F ) -> ( x e. ( Unit ` F ) \/ y e. ( Unit ` F ) ) ) )
44 43 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` F ) A. y e. ( Base ` F ) ( ( x ( +g ` F ) y ) = ( 1r ` F ) -> ( x e. ( Unit ` F ) \/ y e. ( Unit ` F ) ) ) )
45 8 31 23 9 islring 
 |-  ( F e. LRing <-> ( F e. NzRing /\ A. x e. ( Base ` F ) A. y e. ( Base ` F ) ( ( x ( +g ` F ) y ) = ( 1r ` F ) -> ( x e. ( Unit ` F ) \/ y e. ( Unit ` F ) ) ) ) )
46 3 44 45 sylanbrc 
 |-  ( ph -> F e. LRing )