Metamath Proof Explorer

Theorem 1arithufdlem4

Description: Lemma for 1arithufd . Nonzero ring, non-field case. Those trivial cases are handled in the final proof. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses 1arithufd.b 
|- B = ( Base ` R )
1arithufd.0 
|- .0. = ( 0g ` R )
1arithufd.u 
|- U = ( Unit ` R )
1arithufd.p 
|- P = ( RPrime ` R )
1arithufd.m 
|- M = ( mulGrp ` R )
1arithufd.r 
|- ( ph -> R e. UFD )
1arithufdlem.2 
|- ( ph -> -. R e. DivRing )
1arithufdlem.s 
|- S = { x e. B | E. f e. Word P x = ( M gsum f ) }
1arithufdlem.3 
|- ( ph -> X e. B )
1arithufdlem.4 
|- ( ph -> -. X e. U )
1arithufdlem.5 
|- ( ph -> X =/= .0. )
Assertion 1arithufdlem4 
|- ( ph -> X e. S )

Proof

Step Hyp Ref Expression
1 1arithufd.b 
 |-  B = ( Base ` R )
2 1arithufd.0 
 |-  .0. = ( 0g ` R )
3 1arithufd.u 
 |-  U = ( Unit ` R )
4 1arithufd.p 
 |-  P = ( RPrime ` R )
5 1arithufd.m 
 |-  M = ( mulGrp ` R )
6 1arithufd.r 
 |-  ( ph -> R e. UFD )
7 1arithufdlem.2 
 |-  ( ph -> -. R e. DivRing )
8 1arithufdlem.s 
 |-  S = { x e. B | E. f e. Word P x = ( M gsum f ) }
9 1arithufdlem.3 
 |-  ( ph -> X e. B )
10 1arithufdlem.4 
 |-  ( ph -> -. X e. U )
11 1arithufdlem.5 
 |-  ( ph -> X =/= .0. )
12 eqeq1 
 |-  ( x = a -> ( x = ( M gsum f ) <-> a = ( M gsum f ) ) )
13 12 rexbidv 
 |-  ( x = a -> ( E. f e. Word P x = ( M gsum f ) <-> E. f e. Word P a = ( M gsum f ) ) )
14 eqcom 
 |-  ( a = ( M gsum f ) <-> ( M gsum f ) = a )
15 14 rexbii 
 |-  ( E. f e. Word P a = ( M gsum f ) <-> E. f e. Word P ( M gsum f ) = a )
16 13 15 bitrdi 
 |-  ( x = a -> ( E. f e. Word P x = ( M gsum f ) <-> E. f e. Word P ( M gsum f ) = a ) )
17 6 adantr 
 |-  ( ( ph /\ a e. P ) -> R e. UFD )
18 simpr 
 |-  ( ( ph /\ a e. P ) -> a e. P )
19 1 4 17 18 rprmcl 
 |-  ( ( ph /\ a e. P ) -> a e. B )
20 oveq2 
 |-  ( f = <" a "> -> ( M gsum f ) = ( M gsum <" a "> ) )
21 20 eqeq1d 
 |-  ( f = <" a "> -> ( ( M gsum f ) = a <-> ( M gsum <" a "> ) = a ) )
22 18 s1cld 
 |-  ( ( ph /\ a e. P ) -> <" a "> e. Word P )
23 5 1 mgpbas 
 |-  B = ( Base ` M )
24 23 gsumws1 
 |-  ( a e. B -> ( M gsum <" a "> ) = a )
25 19 24 syl 
 |-  ( ( ph /\ a e. P ) -> ( M gsum <" a "> ) = a )
26 21 22 25 rspcedvdw 
 |-  ( ( ph /\ a e. P ) -> E. f e. Word P ( M gsum f ) = a )
27 16 19 26 elrabd 
 |-  ( ( ph /\ a e. P ) -> a e. { x e. B | E. f e. Word P x = ( M gsum f ) } )
28 27 8 eleqtrrdi 
 |-  ( ( ph /\ a e. P ) -> a e. S )
29 28 ex 
 |-  ( ph -> ( a e. P -> a e. S ) )
30 29 ssrdv 
 |-  ( ph -> P C_ S )
31 30 adantr 
 |-  ( ( ph /\ -. X e. S ) -> P C_ S )
32 anass 
 |-  ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) <-> ( ( ph /\ -. X e. S ) /\ ( i e. ( LIdeal ` R ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) ) )
33 ineq2 
 |-  ( p = i -> ( S i^i p ) = ( S i^i i ) )
34 33 eqeq1d 
 |-  ( p = i -> ( ( S i^i p ) = (/) <-> ( S i^i i ) = (/) ) )
35 sseq2 
 |-  ( p = i -> ( ( ( RSpan ` R ) ` { X } ) C_ p <-> ( ( RSpan ` R ) ` { X } ) C_ i ) )
36 34 35 anbi12d 
 |-  ( p = i -> ( ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) <-> ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) )
37 36 elrab 
 |-  ( i e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } <-> ( i e. ( LIdeal ` R ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) )
38 37 anbi2i 
 |-  ( ( ( ph /\ -. X e. S ) /\ i e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } ) <-> ( ( ph /\ -. X e. S ) /\ ( i e. ( LIdeal ` R ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) ) )
39 32 38 bitr4i 
 |-  ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) <-> ( ( ph /\ -. X e. S ) /\ i e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } ) )
40 39 anbi1i 
 |-  ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) <-> ( ( ( ph /\ -. X e. S ) /\ i e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } ) /\ i e. ( PrmIdeal ` R ) ) )
41 incom 
 |-  ( i i^i S ) = ( S i^i i )
42 simpllr 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) )
43 42 simpld 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> ( S i^i i ) = (/) )
44 41 43 eqtrid 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> ( i i^i S ) = (/) )
45 6 ad5antr 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> R e. UFD )
46 simplr 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> i e. ( PrmIdeal ` R ) )
47 42 simprd 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> ( ( RSpan ` R ) ` { X } ) C_ i )
48 6 ufdidom 
 |-  ( ph -> R e. IDomn )
49 48 idomringd 
 |-  ( ph -> R e. Ring )
50 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
51 1 50 rspsnid 
 |-  ( ( R e. Ring /\ X e. B ) -> X e. ( ( RSpan ` R ) ` { X } ) )
52 49 9 51 syl2anc 
 |-  ( ph -> X e. ( ( RSpan ` R ) ` { X } ) )
53 52 ad5antr 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> X e. ( ( RSpan ` R ) ` { X } ) )
54 47 53 sseldd 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> X e. i )
55 nelsn 
 |-  ( X =/= .0. -> -. X e. { .0. } )
56 11 55 syl 
 |-  ( ph -> -. X e. { .0. } )
57 56 ad5antr 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> -. X e. { .0. } )
58 nelne1 
 |-  ( ( X e. i /\ -. X e. { .0. } ) -> i =/= { .0. } )
59 54 57 58 syl2anc 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> i =/= { .0. } )
60 46 59 eldifsnd 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) )
61 ineq1 
 |-  ( j = i -> ( j i^i P ) = ( i i^i P ) )
62 61 neeq1d 
 |-  ( j = i -> ( ( j i^i P ) =/= (/) <-> ( i i^i P ) =/= (/) ) )
63 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
64 63 4 2 isufd 
 |-  ( R e. UFD <-> ( R e. IDomn /\ A. j e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ( j i^i P ) =/= (/) ) )
65 64 simprbi 
 |-  ( R e. UFD -> A. j e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ( j i^i P ) =/= (/) )
66 65 adantr 
 |-  ( ( R e. UFD /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> A. j e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ( j i^i P ) =/= (/) )
67 simpr 
 |-  ( ( R e. UFD /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) )
68 62 66 67 rspcdva 
 |-  ( ( R e. UFD /\ i e. ( ( PrmIdeal ` R ) \ { { .0. } } ) ) -> ( i i^i P ) =/= (/) )
69 45 60 68 syl2anc 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> ( i i^i P ) =/= (/) )
70 sseq0 
 |-  ( ( ( i i^i P ) C_ ( i i^i S ) /\ ( i i^i S ) = (/) ) -> ( i i^i P ) = (/) )
71 70 expcom 
 |-  ( ( i i^i S ) = (/) -> ( ( i i^i P ) C_ ( i i^i S ) -> ( i i^i P ) = (/) ) )
72 71 necon3ad 
 |-  ( ( i i^i S ) = (/) -> ( ( i i^i P ) =/= (/) -> -. ( i i^i P ) C_ ( i i^i S ) ) )
73 sslin 
 |-  ( P C_ S -> ( i i^i P ) C_ ( i i^i S ) )
74 73 con3i 
 |-  ( -. ( i i^i P ) C_ ( i i^i S ) -> -. P C_ S )
75 72 74 syl6 
 |-  ( ( i i^i S ) = (/) -> ( ( i i^i P ) =/= (/) -> -. P C_ S ) )
76 44 69 75 sylc 
 |-  ( ( ( ( ( ( ph /\ -. X e. S ) /\ i e. ( LIdeal ` R ) ) /\ ( ( S i^i i ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ i ) ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> -. P C_ S )
77 40 76 sylanbr 
 |-  ( ( ( ( ( ph /\ -. X e. S ) /\ i e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } ) /\ i e. ( PrmIdeal ` R ) ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) -> -. P C_ S )
78 77 anasss 
 |-  ( ( ( ( ph /\ -. X e. S ) /\ i e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } ) /\ ( i e. ( PrmIdeal ` R ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) ) -> -. P C_ S )
79 48 idomcringd 
 |-  ( ph -> R e. CRing )
80 79 adantr 
 |-  ( ( ph /\ -. X e. S ) -> R e. CRing )
81 49 adantr 
 |-  ( ( ph /\ -. X e. S ) -> R e. Ring )
82 9 adantr 
 |-  ( ( ph /\ -. X e. S ) -> X e. B )
83 82 snssd 
 |-  ( ( ph /\ -. X e. S ) -> { X } C_ B )
84 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
85 50 1 84 rspcl 
 |-  ( ( R e. Ring /\ { X } C_ B ) -> ( ( RSpan ` R ) ` { X } ) e. ( LIdeal ` R ) )
86 81 83 85 syl2anc 
 |-  ( ( ph /\ -. X e. S ) -> ( ( RSpan ` R ) ` { X } ) e. ( LIdeal ` R ) )
87 5 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
88 49 87 syl 
 |-  ( ph -> M e. Mnd )
89 8 ssrab3 
 |-  S C_ B
90 89 a1i 
 |-  ( ph -> S C_ B )
91 eqeq1 
 |-  ( x = ( 1r ` R ) -> ( x = ( M gsum f ) <-> ( 1r ` R ) = ( M gsum f ) ) )
92 91 rexbidv 
 |-  ( x = ( 1r ` R ) -> ( E. f e. Word P x = ( M gsum f ) <-> E. f e. Word P ( 1r ` R ) = ( M gsum f ) ) )
93 eqcom 
 |-  ( ( 1r ` R ) = ( M gsum f ) <-> ( M gsum f ) = ( 1r ` R ) )
94 93 rexbii 
 |-  ( E. f e. Word P ( 1r ` R ) = ( M gsum f ) <-> E. f e. Word P ( M gsum f ) = ( 1r ` R ) )
95 92 94 bitrdi 
 |-  ( x = ( 1r ` R ) -> ( E. f e. Word P x = ( M gsum f ) <-> E. f e. Word P ( M gsum f ) = ( 1r ` R ) ) )
96 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
97 1 96 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
98 49 97 syl 
 |-  ( ph -> ( 1r ` R ) e. B )
99 oveq2 
 |-  ( f = (/) -> ( M gsum f ) = ( M gsum (/) ) )
100 99 eqeq1d 
 |-  ( f = (/) -> ( ( M gsum f ) = ( 1r ` R ) <-> ( M gsum (/) ) = ( 1r ` R ) ) )
101 wrd0 
 |-  (/) e. Word P
102 101 a1i 
 |-  ( ph -> (/) e. Word P )
103 5 96 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
104 103 gsum0 
 |-  ( M gsum (/) ) = ( 1r ` R )
105 104 a1i 
 |-  ( ph -> ( M gsum (/) ) = ( 1r ` R ) )
106 100 102 105 rspcedvdw 
 |-  ( ph -> E. f e. Word P ( M gsum f ) = ( 1r ` R ) )
107 95 98 106 elrabd 
 |-  ( ph -> ( 1r ` R ) e. { x e. B | E. f e. Word P x = ( M gsum f ) } )
108 107 8 eleqtrrdi 
 |-  ( ph -> ( 1r ` R ) e. S )
109 6 ad2antrr 
 |-  ( ( ( ph /\ a e. S ) /\ b e. S ) -> R e. UFD )
110 7 ad2antrr 
 |-  ( ( ( ph /\ a e. S ) /\ b e. S ) -> -. R e. DivRing )
111 eqid 
 |-  ( .r ` R ) = ( .r ` R )
112 simplr 
 |-  ( ( ( ph /\ a e. S ) /\ b e. S ) -> a e. S )
113 simpr 
 |-  ( ( ( ph /\ a e. S ) /\ b e. S ) -> b e. S )
114 1 2 3 4 5 109 110 8 111 112 113 1arithufdlem2 
 |-  ( ( ( ph /\ a e. S ) /\ b e. S ) -> ( a ( .r ` R ) b ) e. S )
115 114 anasss 
 |-  ( ( ph /\ ( a e. S /\ b e. S ) ) -> ( a ( .r ` R ) b ) e. S )
116 115 ralrimivva 
 |-  ( ph -> A. a e. S A. b e. S ( a ( .r ` R ) b ) e. S )
117 5 111 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
118 23 103 117 issubm 
 |-  ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> ( S C_ B /\ ( 1r ` R ) e. S /\ A. a e. S A. b e. S ( a ( .r ` R ) b ) e. S ) ) )
119 118 biimpar 
 |-  ( ( M e. Mnd /\ ( S C_ B /\ ( 1r ` R ) e. S /\ A. a e. S A. b e. S ( a ( .r ` R ) b ) e. S ) ) -> S e. ( SubMnd ` M ) )
120 88 90 108 116 119 syl13anc 
 |-  ( ph -> S e. ( SubMnd ` M ) )
121 120 adantr 
 |-  ( ( ph /\ -. X e. S ) -> S e. ( SubMnd ` M ) )
122 neq0 
 |-  ( -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) <-> E. u u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) )
123 122 biimpi 
 |-  ( -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) -> E. u u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) )
124 123 adantl 
 |-  ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) -> E. u u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) )
125 6 ad4antr 
 |-  ( ( ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) /\ y e. B ) /\ u = ( y ( .r ` R ) X ) ) -> R e. UFD )
126 7 ad4antr 
 |-  ( ( ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) /\ y e. B ) /\ u = ( y ( .r ` R ) X ) ) -> -. R e. DivRing )
127 9 ad4antr 
 |-  ( ( ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) /\ y e. B ) /\ u = ( y ( .r ` R ) X ) ) -> X e. B )
128 10 ad4antr 
 |-  ( ( ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) /\ y e. B ) /\ u = ( y ( .r ` R ) X ) ) -> -. X e. U )
129 11 ad4antr 
 |-  ( ( ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) /\ y e. B ) /\ u = ( y ( .r ` R ) X ) ) -> X =/= .0. )
130 simplr 
 |-  ( ( ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) /\ y e. B ) /\ u = ( y ( .r ` R ) X ) ) -> y e. B )
131 simpr 
 |-  ( ( ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) /\ y e. B ) /\ u = ( y ( .r ` R ) X ) ) -> u = ( y ( .r ` R ) X ) )
132 simpllr 
 |-  ( ( ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) /\ y e. B ) /\ u = ( y ( .r ` R ) X ) ) -> u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) )
133 132 elin1d 
 |-  ( ( ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) /\ y e. B ) /\ u = ( y ( .r ` R ) X ) ) -> u e. S )
134 131 133 eqeltrrd 
 |-  ( ( ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) /\ y e. B ) /\ u = ( y ( .r ` R ) X ) ) -> ( y ( .r ` R ) X ) e. S )
135 1 2 3 4 5 125 126 8 127 128 129 111 130 134 1arithufdlem3 
 |-  ( ( ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) /\ y e. B ) /\ u = ( y ( .r ` R ) X ) ) -> X e. S )
136 49 ad2antrr 
 |-  ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) -> R e. Ring )
137 9 ad2antrr 
 |-  ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) -> X e. B )
138 simpr 
 |-  ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) -> u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) )
139 138 elin2d 
 |-  ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) -> u e. ( ( RSpan ` R ) ` { X } ) )
140 1 111 50 elrspsn 
 |-  ( ( R e. Ring /\ X e. B ) -> ( u e. ( ( RSpan ` R ) ` { X } ) <-> E. y e. B u = ( y ( .r ` R ) X ) ) )
141 140 biimpa 
 |-  ( ( ( R e. Ring /\ X e. B ) /\ u e. ( ( RSpan ` R ) ` { X } ) ) -> E. y e. B u = ( y ( .r ` R ) X ) )
142 136 137 139 141 syl21anc 
 |-  ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) -> E. y e. B u = ( y ( .r ` R ) X ) )
143 135 142 r19.29a 
 |-  ( ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) /\ u e. ( S i^i ( ( RSpan ` R ) ` { X } ) ) ) -> X e. S )
144 124 143 exlimddv 
 |-  ( ( ph /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) -> X e. S )
145 144 adantlr 
 |-  ( ( ( ph /\ -. X e. S ) /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) -> X e. S )
146 simplr 
 |-  ( ( ( ph /\ -. X e. S ) /\ -. ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) ) -> -. X e. S )
147 145 146 condan 
 |-  ( ( ph /\ -. X e. S ) -> ( S i^i ( ( RSpan ` R ) ` { X } ) ) = (/) )
148 eqid 
 |-  { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } = { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) }
149 1 80 86 121 5 147 148 ssdifidlprm 
 |-  ( ( ph /\ -. X e. S ) -> E. i e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } ( i e. ( PrmIdeal ` R ) /\ A. j e. { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ ( ( RSpan ` R ) ` { X } ) C_ p ) } -. i C. j ) )
150 78 149 r19.29a 
 |-  ( ( ph /\ -. X e. S ) -> -. P C_ S )
151 31 150 condan 
 |-  ( ph -> X e. S )