Metamath Proof Explorer

Theorem dflringlem2

Description: Lemma for dflring3 . In a commutative local ring R , the set ( B \ U ) of non-units is an ideal. (Contributed by Thierry Arnoux, 2-Jun-2026)

Ref Expression
Hypotheses dflringlem2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
dflringlem2.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dflringlem2.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
dflringlem2.2 ⊢ ( 𝜑 → 𝑅 ∈ LRing )
Assertion dflringlem2 ( 𝜑 → ( 𝐵 ∖ 𝑈 ) ∈ ( LIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 dflringlem2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dflringlem2.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 dflringlem2.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
4 dflringlem2.2 ⊢ ( 𝜑 → 𝑅 ∈ LRing )
5 difssd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑈 ) ⊆ 𝐵 )
6 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7 3 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
8 1 6 7 grpidcld ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
9 lringnzr ⊢ ( 𝑅 ∈ LRing → 𝑅 ∈ NzRing )
10 4 9 syl ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑅 ∈ NzRing )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
13 2 6 11 12 unitnz ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ≠ ( 0g ‘ 𝑅 ) )
14 13 nelrdva ⊢ ( 𝜑 → ¬ ( 0g ‘ 𝑅 ) ∈ 𝑈 )
15 8 14 eldifd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( 𝐵 ∖ 𝑈 ) )
16 15 ne0d ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑈 ) ≠ ∅ )
17 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
18 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → 𝑅 ∈ Grp )
19 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
20 3 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
21 20 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → 𝑅 ∈ Ring )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → 𝑥 ∈ 𝐵 )
23 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) )
24 23 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → 𝑎 ∈ 𝐵 )
25 1 19 21 22 24 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐵 )
26 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) )
27 26 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → 𝑏 ∈ 𝐵 )
28 1 17 18 25 27 grpcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
29 23 eldifbd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → ¬ 𝑎 ∈ 𝑈 )
30 26 eldifbd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → ¬ 𝑏 ∈ 𝑈 )
31 ioran ⊢ ( ¬ ( 𝑎 ∈ 𝑈 ∨ 𝑏 ∈ 𝑈 ) ↔ ( ¬ 𝑎 ∈ 𝑈 ∧ ¬ 𝑏 ∈ 𝑈 ) )
32 29 30 31 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → ¬ ( 𝑎 ∈ 𝑈 ∨ 𝑏 ∈ 𝑈 ) )
33 3 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → 𝑅 ∈ CRing )
34 33 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → 𝑅 ∈ CRing )
35 22 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → 𝑥 ∈ 𝐵 )
36 24 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → 𝑎 ∈ 𝐵 )
37 25 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐵 )
38 37 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐵 )
39 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → 𝑢 ∈ 𝐵 )
40 39 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → 𝑢 ∈ 𝐵 )
41 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 )
42 2 19 1 unitmulclb ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝑈 ∧ 𝑢 ∈ 𝑈 ) ) )
43 42 simprbda ⊢ ( ( ( 𝑅 ∈ CRing ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝑈 )
44 34 38 40 41 43 syl31anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝑈 )
45 2 19 1 unitmulclb ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝑈 ↔ ( 𝑥 ∈ 𝑈 ∧ 𝑎 ∈ 𝑈 ) ) )
46 45 simplbda ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝑈 ) → 𝑎 ∈ 𝑈 )
47 34 35 36 44 46 syl31anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → 𝑎 ∈ 𝑈 )
48 33 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → 𝑅 ∈ CRing )
49 27 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → 𝑏 ∈ 𝐵 )
50 49 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → 𝑏 ∈ 𝐵 )
51 39 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → 𝑢 ∈ 𝐵 )
52 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 )
53 2 19 1 unitmulclb ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑏 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ↔ ( 𝑏 ∈ 𝑈 ∧ 𝑢 ∈ 𝑈 ) ) )
54 53 simprbda ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑏 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → 𝑏 ∈ 𝑈 )
55 48 50 51 52 54 syl31anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) ∧ ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) → 𝑏 ∈ 𝑈 )
56 1 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → 𝐵 = ( Base ‘ 𝑅 ) )
57 2 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → 𝑈 = ( Unit ‘ 𝑅 ) )
58 17 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) )
59 4 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → 𝑅 ∈ LRing )
60 21 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
61 1 17 19 60 37 49 39 ringdird ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ) )
62 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) )
63 61 62 eqtr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ) = ( 1r ‘ 𝑅 ) )
64 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
65 2 64 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
66 20 65 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
67 66 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝑈 )
68 63 67 eqeltrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ( +g ‘ 𝑅 ) ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ) ∈ 𝑈 )
69 1 19 60 37 39 ringcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝐵 )
70 1 19 60 49 39 ringcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝐵 )
71 56 57 58 59 68 69 70 lringuplu ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ∨ ( 𝑏 ( .r ‘ 𝑅 ) 𝑢 ) ∈ 𝑈 ) )
72 47 55 71 orim12da ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ) → ( 𝑎 ∈ 𝑈 ∨ 𝑏 ∈ 𝑈 ) )
73 1 2 19 64 28 21 isunit3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ↔ ∃ 𝑢 ∈ 𝐵 ( ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ) = ( 1r ‘ 𝑅 ) ) ) )
74 73 biimpa ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) → ∃ 𝑢 ∈ 𝐵 ( ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ) = ( 1r ‘ 𝑅 ) ) )
75 simpl ⊢ ( ( ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ) = ( 1r ‘ 𝑅 ) ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) )
76 75 reximi ⊢ ( ∃ 𝑢 ∈ 𝐵 ( ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑢 ( .r ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ) = ( 1r ‘ 𝑅 ) ) → ∃ 𝑢 ∈ 𝐵 ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) )
77 74 76 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) → ∃ 𝑢 ∈ 𝐵 ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑢 ) = ( 1r ‘ 𝑅 ) )
78 72 77 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 ) → ( 𝑎 ∈ 𝑈 ∨ 𝑏 ∈ 𝑈 ) )
79 32 78 mtand ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → ¬ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑈 )
80 28 79 eldifd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ∧ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( 𝐵 ∖ 𝑈 ) )
81 80 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) → ∀ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( 𝐵 ∖ 𝑈 ) )
82 81 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ) ) → ∀ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( 𝐵 ∖ 𝑈 ) )
83 82 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ∀ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( 𝐵 ∖ 𝑈 ) )
84 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
85 84 1 17 19 islidl ⊢ ( ( 𝐵 ∖ 𝑈 ) ∈ ( LIdeal ‘ 𝑅 ) ↔ ( ( 𝐵 ∖ 𝑈 ) ⊆ 𝐵 ∧ ( 𝐵 ∖ 𝑈 ) ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑎 ∈ ( 𝐵 ∖ 𝑈 ) ∀ 𝑏 ∈ ( 𝐵 ∖ 𝑈 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( 𝐵 ∖ 𝑈 ) ) )
86 5 16 83 85 syl3anbrc ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑈 ) ∈ ( LIdeal ‘ 𝑅 ) )