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 
|- B = ( Base ` R )
dflringlem2.u 
|- U = ( Unit ` R )
dflringlem2.1 
|- ( ph -> R e. CRing )
dflringlem2.2 
|- ( ph -> R e. LRing )
Assertion dflringlem2 
|- ( ph -> ( B \ U ) e. ( LIdeal ` R ) )

Proof

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