Metamath Proof Explorer

Theorem lringuplu

Description: If the sum of two elements of a local ring is invertible, then at least one of the summands must be invertible. (Contributed by Jim Kingdon, 18-Feb-2025) (Revised by SN, 23-Feb-2025)

Ref Expression
Hypotheses lring.b 
|- ( ph -> B = ( Base ` R ) )
lring.u 
|- ( ph -> U = ( Unit ` R ) )
lring.p 
|- ( ph -> .+ = ( +g ` R ) )
lring.l 
|- ( ph -> R e. LRing )
lring.s 
|- ( ph -> ( X .+ Y ) e. U )
lring.x 
|- ( ph -> X e. B )
lring.y 
|- ( ph -> Y e. B )
Assertion lringuplu 
|- ( ph -> ( X e. U \/ Y e. U ) )

Proof

Step Hyp Ref Expression
1 lring.b 
 |-  ( ph -> B = ( Base ` R ) )
2 lring.u 
 |-  ( ph -> U = ( Unit ` R ) )
3 lring.p 
 |-  ( ph -> .+ = ( +g ` R ) )
4 lring.l 
 |-  ( ph -> R e. LRing )
5 lring.s 
 |-  ( ph -> ( X .+ Y ) e. U )
6 lring.x 
 |-  ( ph -> X e. B )
7 lring.y 
 |-  ( ph -> Y e. B )
8 lringring 
 |-  ( R e. LRing -> R e. Ring )
9 4 8 syl 
 |-  ( ph -> R e. Ring )
10 6 1 eleqtrd 
 |-  ( ph -> X e. ( Base ` R ) )
11 5 2 eleqtrd 
 |-  ( ph -> ( X .+ Y ) e. ( Unit ` R ) )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
14 eqid 
 |-  ( /r ` R ) = ( /r ` R )
15 eqid 
 |-  ( .r ` R ) = ( .r ` R )
16 12 13 14 15 dvrcan1 
 |-  ( ( R e. Ring /\ X e. ( Base ` R ) /\ ( X .+ Y ) e. ( Unit ` R ) ) -> ( ( X ( /r ` R ) ( X .+ Y ) ) ( .r ` R ) ( X .+ Y ) ) = X )
17 9 10 11 16 syl3anc 
 |-  ( ph -> ( ( X ( /r ` R ) ( X .+ Y ) ) ( .r ` R ) ( X .+ Y ) ) = X )
18 17 adantr 
 |-  ( ( ph /\ ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> ( ( X ( /r ` R ) ( X .+ Y ) ) ( .r ` R ) ( X .+ Y ) ) = X )
19 9 adantr 
 |-  ( ( ph /\ ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> R e. Ring )
20 simpr 
 |-  ( ( ph /\ ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) )
21 11 adantr 
 |-  ( ( ph /\ ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> ( X .+ Y ) e. ( Unit ` R ) )
22 13 15 unitmulcl 
 |-  ( ( R e. Ring /\ ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) /\ ( X .+ Y ) e. ( Unit ` R ) ) -> ( ( X ( /r ` R ) ( X .+ Y ) ) ( .r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) )
23 19 20 21 22 syl3anc 
 |-  ( ( ph /\ ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> ( ( X ( /r ` R ) ( X .+ Y ) ) ( .r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) )
24 18 23 eqeltrrd 
 |-  ( ( ph /\ ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> X e. ( Unit ` R ) )
25 2 adantr 
 |-  ( ( ph /\ ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> U = ( Unit ` R ) )
26 24 25 eleqtrrd 
 |-  ( ( ph /\ ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> X e. U )
27 26 orcd 
 |-  ( ( ph /\ ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> ( X e. U \/ Y e. U ) )
28 7 1 eleqtrd 
 |-  ( ph -> Y e. ( Base ` R ) )
29 12 13 14 15 dvrcan1 
 |-  ( ( R e. Ring /\ Y e. ( Base ` R ) /\ ( X .+ Y ) e. ( Unit ` R ) ) -> ( ( Y ( /r ` R ) ( X .+ Y ) ) ( .r ` R ) ( X .+ Y ) ) = Y )
30 9 28 11 29 syl3anc 
 |-  ( ph -> ( ( Y ( /r ` R ) ( X .+ Y ) ) ( .r ` R ) ( X .+ Y ) ) = Y )
31 30 adantr 
 |-  ( ( ph /\ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> ( ( Y ( /r ` R ) ( X .+ Y ) ) ( .r ` R ) ( X .+ Y ) ) = Y )
32 9 adantr 
 |-  ( ( ph /\ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> R e. Ring )
33 simpr 
 |-  ( ( ph /\ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) )
34 11 adantr 
 |-  ( ( ph /\ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> ( X .+ Y ) e. ( Unit ` R ) )
35 13 15 unitmulcl 
 |-  ( ( R e. Ring /\ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) /\ ( X .+ Y ) e. ( Unit ` R ) ) -> ( ( Y ( /r ` R ) ( X .+ Y ) ) ( .r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) )
36 32 33 34 35 syl3anc 
 |-  ( ( ph /\ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> ( ( Y ( /r ` R ) ( X .+ Y ) ) ( .r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) )
37 31 36 eqeltrrd 
 |-  ( ( ph /\ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> Y e. ( Unit ` R ) )
38 2 adantr 
 |-  ( ( ph /\ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> U = ( Unit ` R ) )
39 37 38 eleqtrrd 
 |-  ( ( ph /\ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> Y e. U )
40 39 olcd 
 |-  ( ( ph /\ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) -> ( X e. U \/ Y e. U ) )
41 eqid 
 |-  ( +g ` R ) = ( +g ` R )
42 12 13 41 14 dvrdir 
 |-  ( ( R e. Ring /\ ( X e. ( Base ` R ) /\ Y e. ( Base ` R ) /\ ( X .+ Y ) e. ( Unit ` R ) ) ) -> ( ( X ( +g ` R ) Y ) ( /r ` R ) ( X .+ Y ) ) = ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) ( Y ( /r ` R ) ( X .+ Y ) ) ) )
43 9 10 28 11 42 syl13anc 
 |-  ( ph -> ( ( X ( +g ` R ) Y ) ( /r ` R ) ( X .+ Y ) ) = ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) ( Y ( /r ` R ) ( X .+ Y ) ) ) )
44 3 eqcomd 
 |-  ( ph -> ( +g ` R ) = .+ )
45 44 oveqd 
 |-  ( ph -> ( X ( +g ` R ) Y ) = ( X .+ Y ) )
46 9 ringgrpd 
 |-  ( ph -> R e. Grp )
47 12 41 46 10 28 grpcld 
 |-  ( ph -> ( X ( +g ` R ) Y ) e. ( Base ` R ) )
48 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
49 12 13 14 48 dvreq1 
 |-  ( ( R e. Ring /\ ( X ( +g ` R ) Y ) e. ( Base ` R ) /\ ( X .+ Y ) e. ( Unit ` R ) ) -> ( ( ( X ( +g ` R ) Y ) ( /r ` R ) ( X .+ Y ) ) = ( 1r ` R ) <-> ( X ( +g ` R ) Y ) = ( X .+ Y ) ) )
50 9 47 11 49 syl3anc 
 |-  ( ph -> ( ( ( X ( +g ` R ) Y ) ( /r ` R ) ( X .+ Y ) ) = ( 1r ` R ) <-> ( X ( +g ` R ) Y ) = ( X .+ Y ) ) )
51 45 50 mpbird 
 |-  ( ph -> ( ( X ( +g ` R ) Y ) ( /r ` R ) ( X .+ Y ) ) = ( 1r ` R ) )
52 43 51 eqtr3d 
 |-  ( ph -> ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) ( Y ( /r ` R ) ( X .+ Y ) ) ) = ( 1r ` R ) )
53 oveq2 
 |-  ( v = ( Y ( /r ` R ) ( X .+ Y ) ) -> ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) v ) = ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) ( Y ( /r ` R ) ( X .+ Y ) ) ) )
54 53 eqeq1d 
 |-  ( v = ( Y ( /r ` R ) ( X .+ Y ) ) -> ( ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) v ) = ( 1r ` R ) <-> ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) ( Y ( /r ` R ) ( X .+ Y ) ) ) = ( 1r ` R ) ) )
55 eleq1 
 |-  ( v = ( Y ( /r ` R ) ( X .+ Y ) ) -> ( v e. ( Unit ` R ) <-> ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) )
56 55 orbi2d 
 |-  ( v = ( Y ( /r ` R ) ( X .+ Y ) ) -> ( ( ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) <-> ( ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) \/ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) ) )
57 54 56 imbi12d 
 |-  ( v = ( Y ( /r ` R ) ( X .+ Y ) ) -> ( ( ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) v ) = ( 1r ` R ) -> ( ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) <-> ( ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) ( Y ( /r ` R ) ( X .+ Y ) ) ) = ( 1r ` R ) -> ( ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) \/ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) ) ) )
58 oveq1 
 |-  ( u = ( X ( /r ` R ) ( X .+ Y ) ) -> ( u ( +g ` R ) v ) = ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) v ) )
59 58 eqeq1d 
 |-  ( u = ( X ( /r ` R ) ( X .+ Y ) ) -> ( ( u ( +g ` R ) v ) = ( 1r ` R ) <-> ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) v ) = ( 1r ` R ) ) )
60 eleq1 
 |-  ( u = ( X ( /r ` R ) ( X .+ Y ) ) -> ( u e. ( Unit ` R ) <-> ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) )
61 60 orbi1d 
 |-  ( u = ( X ( /r ` R ) ( X .+ Y ) ) -> ( ( u e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) <-> ( ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) )
62 59 61 imbi12d 
 |-  ( u = ( X ( /r ` R ) ( X .+ Y ) ) -> ( ( ( u ( +g ` R ) v ) = ( 1r ` R ) -> ( u e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) <-> ( ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) v ) = ( 1r ` R ) -> ( ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) ) )
63 62 ralbidv 
 |-  ( u = ( X ( /r ` R ) ( X .+ Y ) ) -> ( A. v e. ( Base ` R ) ( ( u ( +g ` R ) v ) = ( 1r ` R ) -> ( u e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) <-> A. v e. ( Base ` R ) ( ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) v ) = ( 1r ` R ) -> ( ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) ) )
64 12 41 48 13 islring 
 |-  ( R e. LRing <-> ( R e. NzRing /\ A. u e. ( Base ` R ) A. v e. ( Base ` R ) ( ( u ( +g ` R ) v ) = ( 1r ` R ) -> ( u e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) ) )
65 4 64 sylib 
 |-  ( ph -> ( R e. NzRing /\ A. u e. ( Base ` R ) A. v e. ( Base ` R ) ( ( u ( +g ` R ) v ) = ( 1r ` R ) -> ( u e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) ) )
66 65 simprd 
 |-  ( ph -> A. u e. ( Base ` R ) A. v e. ( Base ` R ) ( ( u ( +g ` R ) v ) = ( 1r ` R ) -> ( u e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) )
67 12 13 14 dvrcl 
 |-  ( ( R e. Ring /\ X e. ( Base ` R ) /\ ( X .+ Y ) e. ( Unit ` R ) ) -> ( X ( /r ` R ) ( X .+ Y ) ) e. ( Base ` R ) )
68 9 10 11 67 syl3anc 
 |-  ( ph -> ( X ( /r ` R ) ( X .+ Y ) ) e. ( Base ` R ) )
69 63 66 68 rspcdva 
 |-  ( ph -> A. v e. ( Base ` R ) ( ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) v ) = ( 1r ` R ) -> ( ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) \/ v e. ( Unit ` R ) ) ) )
70 12 13 14 dvrcl 
 |-  ( ( R e. Ring /\ Y e. ( Base ` R ) /\ ( X .+ Y ) e. ( Unit ` R ) ) -> ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Base ` R ) )
71 9 28 11 70 syl3anc 
 |-  ( ph -> ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Base ` R ) )
72 57 69 71 rspcdva 
 |-  ( ph -> ( ( ( X ( /r ` R ) ( X .+ Y ) ) ( +g ` R ) ( Y ( /r ` R ) ( X .+ Y ) ) ) = ( 1r ` R ) -> ( ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) \/ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) ) )
73 52 72 mpd 
 |-  ( ph -> ( ( X ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) \/ ( Y ( /r ` R ) ( X .+ Y ) ) e. ( Unit ` R ) ) )
74 27 40 73 mpjaodan 
 |-  ( ph -> ( X e. U \/ Y e. U ) )