Step |
Hyp |
Ref |
Expression |
1 |
|
zarclsx.1 |
Could not format V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) : No typesetting found for |- V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) with typecode |- |
2 |
|
zarcls1.1 |
|
3 |
|
simplr |
|
4 |
|
sseq2 |
|
5 |
|
eqid |
|
6 |
5
|
mxidlprm |
Could not format ( ( R e. CRing /\ m e. ( MaxIdeal ` R ) ) -> m e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( R e. CRing /\ m e. ( MaxIdeal ` R ) ) -> m e. ( PrmIdeal ` R ) ) with typecode |- |
7 |
6
|
ad5ant14 |
Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. ( PrmIdeal ` R ) ) with typecode |- |
8 |
|
simpr |
Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> I C_ m ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> I C_ m ) with typecode |- |
9 |
4 7 8
|
elrabd |
Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. { j e. ( PrmIdeal ` R ) | I C_ j } ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. { j e. ( PrmIdeal ` R ) | I C_ j } ) with typecode |- |
10 |
1
|
a1i |
Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) with typecode |- |
11 |
|
sseq1 |
|
12 |
11
|
rabbidv |
Could not format ( i = I -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | I C_ j } ) : No typesetting found for |- ( i = I -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | I C_ j } ) with typecode |- |
13 |
12
|
adantl |
Could not format ( ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) /\ i = I ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | I C_ j } ) : No typesetting found for |- ( ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) /\ i = I ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | I C_ j } ) with typecode |- |
14 |
|
simp-4r |
Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> I e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> I e. ( LIdeal ` R ) ) with typecode |- |
15 |
|
fvex |
Could not format ( PrmIdeal ` R ) e. _V : No typesetting found for |- ( PrmIdeal ` R ) e. _V with typecode |- |
16 |
15
|
rabex |
Could not format { j e. ( PrmIdeal ` R ) | I C_ j } e. _V : No typesetting found for |- { j e. ( PrmIdeal ` R ) | I C_ j } e. _V with typecode |- |
17 |
16
|
a1i |
Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> { j e. ( PrmIdeal ` R ) | I C_ j } e. _V ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> { j e. ( PrmIdeal ` R ) | I C_ j } e. _V ) with typecode |- |
18 |
10 13 14 17
|
fvmptd |
Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> ( V ` I ) = { j e. ( PrmIdeal ` R ) | I C_ j } ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> ( V ` I ) = { j e. ( PrmIdeal ` R ) | I C_ j } ) with typecode |- |
19 |
9 18
|
eleqtrrd |
Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. ( V ` I ) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> m e. ( V ` I ) ) with typecode |- |
20 |
|
ne0i |
|
21 |
19 20
|
syl |
Could not format ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> ( V ` I ) =/= (/) ) : No typesetting found for |- ( ( ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) /\ m e. ( MaxIdeal ` R ) ) /\ I C_ m ) -> ( V ` I ) =/= (/) ) with typecode |- |
22 |
|
crngring |
|
23 |
2
|
ssmxidl |
Could not format ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) : No typesetting found for |- ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) with typecode |- |
24 |
23
|
3expa |
Could not format ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) : No typesetting found for |- ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) with typecode |- |
25 |
22 24
|
sylanl1 |
Could not format ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) : No typesetting found for |- ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) with typecode |- |
26 |
21 25
|
r19.29a |
|
27 |
26
|
adantlr |
|
28 |
27
|
neneqd |
|
29 |
3 28
|
pm2.65da |
|
30 |
|
nne |
|
31 |
29 30
|
sylib |
|
32 |
|
fveq2 |
|
33 |
32
|
adantl |
|
34 |
1
|
a1i |
Could not format ( R e. Ring -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) : No typesetting found for |- ( R e. Ring -> V = ( i e. ( LIdeal ` R ) |-> { j e. ( PrmIdeal ` R ) | i C_ j } ) ) with typecode |- |
35 |
|
sseq1 |
|
36 |
35
|
adantl |
|
37 |
36
|
rabbidv |
Could not format ( ( R e. Ring /\ i = B ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | B C_ j } ) : No typesetting found for |- ( ( R e. Ring /\ i = B ) -> { j e. ( PrmIdeal ` R ) | i C_ j } = { j e. ( PrmIdeal ` R ) | B C_ j } ) with typecode |- |
38 |
|
eqid |
|
39 |
38 2
|
lidl1 |
|
40 |
15
|
rabex |
Could not format { j e. ( PrmIdeal ` R ) | B C_ j } e. _V : No typesetting found for |- { j e. ( PrmIdeal ` R ) | B C_ j } e. _V with typecode |- |
41 |
40
|
a1i |
Could not format ( R e. Ring -> { j e. ( PrmIdeal ` R ) | B C_ j } e. _V ) : No typesetting found for |- ( R e. Ring -> { j e. ( PrmIdeal ` R ) | B C_ j } e. _V ) with typecode |- |
42 |
34 37 39 41
|
fvmptd |
Could not format ( R e. Ring -> ( V ` B ) = { j e. ( PrmIdeal ` R ) | B C_ j } ) : No typesetting found for |- ( R e. Ring -> ( V ` B ) = { j e. ( PrmIdeal ` R ) | B C_ j } ) with typecode |- |
43 |
|
prmidlidl |
Could not format ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j e. ( LIdeal ` R ) ) with typecode |- |
44 |
2 38
|
lidlss |
|
45 |
43 44
|
syl |
Could not format ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j C_ B ) : No typesetting found for |- ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j C_ B ) with typecode |- |
46 |
45
|
adantr |
Could not format ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j C_ B ) : No typesetting found for |- ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j C_ B ) with typecode |- |
47 |
|
simpr |
Could not format ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> B C_ j ) : No typesetting found for |- ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> B C_ j ) with typecode |- |
48 |
46 47
|
eqssd |
Could not format ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j = B ) : No typesetting found for |- ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j = B ) with typecode |- |
49 |
|
eqid |
|
50 |
2 49
|
prmidlnr |
Could not format ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j =/= B ) : No typesetting found for |- ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> j =/= B ) with typecode |- |
51 |
50
|
adantr |
Could not format ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j =/= B ) : No typesetting found for |- ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> j =/= B ) with typecode |- |
52 |
51
|
neneqd |
Could not format ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> -. j = B ) : No typesetting found for |- ( ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) /\ B C_ j ) -> -. j = B ) with typecode |- |
53 |
48 52
|
pm2.65da |
Could not format ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> -. B C_ j ) : No typesetting found for |- ( ( R e. Ring /\ j e. ( PrmIdeal ` R ) ) -> -. B C_ j ) with typecode |- |
54 |
53
|
ralrimiva |
Could not format ( R e. Ring -> A. j e. ( PrmIdeal ` R ) -. B C_ j ) : No typesetting found for |- ( R e. Ring -> A. j e. ( PrmIdeal ` R ) -. B C_ j ) with typecode |- |
55 |
|
rabeq0 |
Could not format ( { j e. ( PrmIdeal ` R ) | B C_ j } = (/) <-> A. j e. ( PrmIdeal ` R ) -. B C_ j ) : No typesetting found for |- ( { j e. ( PrmIdeal ` R ) | B C_ j } = (/) <-> A. j e. ( PrmIdeal ` R ) -. B C_ j ) with typecode |- |
56 |
54 55
|
sylibr |
Could not format ( R e. Ring -> { j e. ( PrmIdeal ` R ) | B C_ j } = (/) ) : No typesetting found for |- ( R e. Ring -> { j e. ( PrmIdeal ` R ) | B C_ j } = (/) ) with typecode |- |
57 |
42 56
|
eqtrd |
|
58 |
22 57
|
syl |
|
59 |
58
|
ad2antrr |
|
60 |
33 59
|
eqtrd |
|
61 |
31 60
|
impbida |
|