Step |
Hyp |
Ref |
Expression |
1 |
|
ssmxidl.1 |
|- B = ( Base ` R ) |
2 |
|
ssmxidllem.1 |
|- P = { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } |
3 |
|
ssmxidllem.2 |
|- ( ph -> R e. Ring ) |
4 |
|
ssmxidllem.3 |
|- ( ph -> I e. ( LIdeal ` R ) ) |
5 |
|
ssmxidllem.4 |
|- ( ph -> I =/= B ) |
6 |
|
ssmxidllem2.1 |
|- ( ph -> Z C_ P ) |
7 |
|
ssmxidllem2.2 |
|- ( ph -> Z =/= (/) ) |
8 |
|
ssmxidllem2.3 |
|- ( ph -> [C.] Or Z ) |
9 |
|
neeq1 |
|- ( p = U. Z -> ( p =/= B <-> U. Z =/= B ) ) |
10 |
|
sseq2 |
|- ( p = U. Z -> ( I C_ p <-> I C_ U. Z ) ) |
11 |
9 10
|
anbi12d |
|- ( p = U. Z -> ( ( p =/= B /\ I C_ p ) <-> ( U. Z =/= B /\ I C_ U. Z ) ) ) |
12 |
2
|
ssrab3 |
|- P C_ ( LIdeal ` R ) |
13 |
6 12
|
sstrdi |
|- ( ph -> Z C_ ( LIdeal ` R ) ) |
14 |
13
|
sselda |
|- ( ( ph /\ j e. Z ) -> j e. ( LIdeal ` R ) ) |
15 |
|
eqid |
|- ( LIdeal ` R ) = ( LIdeal ` R ) |
16 |
1 15
|
lidlss |
|- ( j e. ( LIdeal ` R ) -> j C_ B ) |
17 |
14 16
|
syl |
|- ( ( ph /\ j e. Z ) -> j C_ B ) |
18 |
17
|
ralrimiva |
|- ( ph -> A. j e. Z j C_ B ) |
19 |
|
unissb |
|- ( U. Z C_ B <-> A. j e. Z j C_ B ) |
20 |
18 19
|
sylibr |
|- ( ph -> U. Z C_ B ) |
21 |
3
|
adantr |
|- ( ( ph /\ j e. Z ) -> R e. Ring ) |
22 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
23 |
15 22
|
lidl0cl |
|- ( ( R e. Ring /\ j e. ( LIdeal ` R ) ) -> ( 0g ` R ) e. j ) |
24 |
21 14 23
|
syl2anc |
|- ( ( ph /\ j e. Z ) -> ( 0g ` R ) e. j ) |
25 |
|
n0i |
|- ( ( 0g ` R ) e. j -> -. j = (/) ) |
26 |
24 25
|
syl |
|- ( ( ph /\ j e. Z ) -> -. j = (/) ) |
27 |
26
|
reximdva0 |
|- ( ( ph /\ Z =/= (/) ) -> E. j e. Z -. j = (/) ) |
28 |
7 27
|
mpdan |
|- ( ph -> E. j e. Z -. j = (/) ) |
29 |
|
rexnal |
|- ( E. j e. Z -. j = (/) <-> -. A. j e. Z j = (/) ) |
30 |
28 29
|
sylib |
|- ( ph -> -. A. j e. Z j = (/) ) |
31 |
|
uni0c |
|- ( U. Z = (/) <-> A. j e. Z j = (/) ) |
32 |
31
|
necon3abii |
|- ( U. Z =/= (/) <-> -. A. j e. Z j = (/) ) |
33 |
30 32
|
sylibr |
|- ( ph -> U. Z =/= (/) ) |
34 |
|
eluni2 |
|- ( a e. U. Z <-> E. i e. Z a e. i ) |
35 |
|
eluni2 |
|- ( b e. U. Z <-> E. j e. Z b e. j ) |
36 |
34 35
|
anbi12i |
|- ( ( a e. U. Z /\ b e. U. Z ) <-> ( E. i e. Z a e. i /\ E. j e. Z b e. j ) ) |
37 |
|
an32 |
|- ( ( ( ( ph /\ x e. B ) /\ E. i e. Z a e. i ) /\ j e. Z ) <-> ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ E. i e. Z a e. i ) ) |
38 |
3
|
ad6antr |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> R e. Ring ) |
39 |
13
|
ad5antr |
|- ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> Z C_ ( LIdeal ` R ) ) |
40 |
|
simp-4r |
|- ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> j e. Z ) |
41 |
39 40
|
sseldd |
|- ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> j e. ( LIdeal ` R ) ) |
42 |
41
|
adantr |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> j e. ( LIdeal ` R ) ) |
43 |
|
simp-6r |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> x e. B ) |
44 |
|
simpr |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> i C_ j ) |
45 |
|
simplr |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> a e. i ) |
46 |
44 45
|
sseldd |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> a e. j ) |
47 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
48 |
15 1 47
|
lidlmcl |
|- ( ( ( R e. Ring /\ j e. ( LIdeal ` R ) ) /\ ( x e. B /\ a e. j ) ) -> ( x ( .r ` R ) a ) e. j ) |
49 |
38 42 43 46 48
|
syl22anc |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> ( x ( .r ` R ) a ) e. j ) |
50 |
|
simp-4r |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> b e. j ) |
51 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
52 |
15 51
|
lidlacl |
|- ( ( ( R e. Ring /\ j e. ( LIdeal ` R ) ) /\ ( ( x ( .r ` R ) a ) e. j /\ b e. j ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. j ) |
53 |
38 42 49 50 52
|
syl22anc |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. j ) |
54 |
40
|
adantr |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> j e. Z ) |
55 |
|
elunii |
|- ( ( ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. j /\ j e. Z ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
56 |
53 54 55
|
syl2anc |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ i C_ j ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
57 |
3
|
ad6antr |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> R e. Ring ) |
58 |
39
|
adantr |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> Z C_ ( LIdeal ` R ) ) |
59 |
|
simplr |
|- ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> i e. Z ) |
60 |
59
|
adantr |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> i e. Z ) |
61 |
58 60
|
sseldd |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> i e. ( LIdeal ` R ) ) |
62 |
|
simp-6r |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> x e. B ) |
63 |
|
simplr |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> a e. i ) |
64 |
15 1 47
|
lidlmcl |
|- ( ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) /\ ( x e. B /\ a e. i ) ) -> ( x ( .r ` R ) a ) e. i ) |
65 |
57 61 62 63 64
|
syl22anc |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> ( x ( .r ` R ) a ) e. i ) |
66 |
|
simpr |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> j C_ i ) |
67 |
|
simp-4r |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> b e. j ) |
68 |
66 67
|
sseldd |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> b e. i ) |
69 |
15 51
|
lidlacl |
|- ( ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) /\ ( ( x ( .r ` R ) a ) e. i /\ b e. i ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i ) |
70 |
57 61 65 68 69
|
syl22anc |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i ) |
71 |
|
elunii |
|- ( ( ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i /\ i e. Z ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
72 |
70 60 71
|
syl2anc |
|- ( ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) /\ j C_ i ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
73 |
8
|
ad5antr |
|- ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> [C.] Or Z ) |
74 |
|
sorpssi |
|- ( ( [C.] Or Z /\ ( i e. Z /\ j e. Z ) ) -> ( i C_ j \/ j C_ i ) ) |
75 |
73 59 40 74
|
syl12anc |
|- ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> ( i C_ j \/ j C_ i ) ) |
76 |
56 72 75
|
mpjaodan |
|- ( ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ i e. Z ) /\ a e. i ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
77 |
76
|
r19.29an |
|- ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ b e. j ) /\ E. i e. Z a e. i ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
78 |
77
|
an32s |
|- ( ( ( ( ( ph /\ x e. B ) /\ j e. Z ) /\ E. i e. Z a e. i ) /\ b e. j ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
79 |
37 78
|
sylanb |
|- ( ( ( ( ( ph /\ x e. B ) /\ E. i e. Z a e. i ) /\ j e. Z ) /\ b e. j ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
80 |
79
|
r19.29an |
|- ( ( ( ( ph /\ x e. B ) /\ E. i e. Z a e. i ) /\ E. j e. Z b e. j ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
81 |
80
|
anasss |
|- ( ( ( ph /\ x e. B ) /\ ( E. i e. Z a e. i /\ E. j e. Z b e. j ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
82 |
36 81
|
sylan2b |
|- ( ( ( ph /\ x e. B ) /\ ( a e. U. Z /\ b e. U. Z ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
83 |
82
|
ralrimivva |
|- ( ( ph /\ x e. B ) -> A. a e. U. Z A. b e. U. Z ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
84 |
83
|
ralrimiva |
|- ( ph -> A. x e. B A. a e. U. Z A. b e. U. Z ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) |
85 |
15 1 51 47
|
islidl |
|- ( U. Z e. ( LIdeal ` R ) <-> ( U. Z C_ B /\ U. Z =/= (/) /\ A. x e. B A. a e. U. Z A. b e. U. Z ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. U. Z ) ) |
86 |
20 33 84 85
|
syl3anbrc |
|- ( ph -> U. Z e. ( LIdeal ` R ) ) |
87 |
6
|
sselda |
|- ( ( ph /\ j e. Z ) -> j e. P ) |
88 |
|
neeq1 |
|- ( p = j -> ( p =/= B <-> j =/= B ) ) |
89 |
|
sseq2 |
|- ( p = j -> ( I C_ p <-> I C_ j ) ) |
90 |
88 89
|
anbi12d |
|- ( p = j -> ( ( p =/= B /\ I C_ p ) <-> ( j =/= B /\ I C_ j ) ) ) |
91 |
90 2
|
elrab2 |
|- ( j e. P <-> ( j e. ( LIdeal ` R ) /\ ( j =/= B /\ I C_ j ) ) ) |
92 |
87 91
|
sylib |
|- ( ( ph /\ j e. Z ) -> ( j e. ( LIdeal ` R ) /\ ( j =/= B /\ I C_ j ) ) ) |
93 |
92
|
simprld |
|- ( ( ph /\ j e. Z ) -> j =/= B ) |
94 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
95 |
1 94
|
pridln1 |
|- ( ( R e. Ring /\ j e. ( LIdeal ` R ) /\ j =/= B ) -> -. ( 1r ` R ) e. j ) |
96 |
21 14 93 95
|
syl3anc |
|- ( ( ph /\ j e. Z ) -> -. ( 1r ` R ) e. j ) |
97 |
96
|
nrexdv |
|- ( ph -> -. E. j e. Z ( 1r ` R ) e. j ) |
98 |
|
eluni2 |
|- ( ( 1r ` R ) e. U. Z <-> E. j e. Z ( 1r ` R ) e. j ) |
99 |
97 98
|
sylnibr |
|- ( ph -> -. ( 1r ` R ) e. U. Z ) |
100 |
15 1 94
|
lidl1el |
|- ( ( R e. Ring /\ U. Z e. ( LIdeal ` R ) ) -> ( ( 1r ` R ) e. U. Z <-> U. Z = B ) ) |
101 |
3 86 100
|
syl2anc |
|- ( ph -> ( ( 1r ` R ) e. U. Z <-> U. Z = B ) ) |
102 |
101
|
necon3bbid |
|- ( ph -> ( -. ( 1r ` R ) e. U. Z <-> U. Z =/= B ) ) |
103 |
99 102
|
mpbid |
|- ( ph -> U. Z =/= B ) |
104 |
92
|
simprrd |
|- ( ( ph /\ j e. Z ) -> I C_ j ) |
105 |
104
|
ralrimiva |
|- ( ph -> A. j e. Z I C_ j ) |
106 |
|
ssint |
|- ( I C_ |^| Z <-> A. j e. Z I C_ j ) |
107 |
105 106
|
sylibr |
|- ( ph -> I C_ |^| Z ) |
108 |
|
intssuni |
|- ( Z =/= (/) -> |^| Z C_ U. Z ) |
109 |
7 108
|
syl |
|- ( ph -> |^| Z C_ U. Z ) |
110 |
107 109
|
sstrd |
|- ( ph -> I C_ U. Z ) |
111 |
103 110
|
jca |
|- ( ph -> ( U. Z =/= B /\ I C_ U. Z ) ) |
112 |
11 86 111
|
elrabd |
|- ( ph -> U. Z e. { p e. ( LIdeal ` R ) | ( p =/= B /\ I C_ p ) } ) |
113 |
112 2
|
eleqtrrdi |
|- ( ph -> U. Z e. P ) |