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 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
lring.u ⊢ ( 𝜑 → 𝑈 = ( Unit ‘ 𝑅 ) )
lring.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
lring.l ⊢ ( 𝜑 → 𝑅 ∈ LRing )
lring.s ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑈 )
lring.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
lring.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion lringuplu ( 𝜑 → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) )

Proof

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