Step |
Hyp |
Ref |
Expression |
1 |
|
rhmpreimacn.t |
Could not format T = ( Spec ` R ) : No typesetting found for |- T = ( Spec ` R ) with typecode |- |
2 |
|
rhmpreimacn.u |
Could not format U = ( Spec ` S ) : No typesetting found for |- U = ( Spec ` S ) with typecode |- |
3 |
|
rhmpreimacn.a |
Could not format A = ( PrmIdeal ` R ) : No typesetting found for |- A = ( PrmIdeal ` R ) with typecode |- |
4 |
|
rhmpreimacn.b |
Could not format B = ( PrmIdeal ` S ) : No typesetting found for |- B = ( PrmIdeal ` S ) with typecode |- |
5 |
|
rhmpreimacn.j |
|
6 |
|
rhmpreimacn.k |
|
7 |
|
rhmpreimacn.g |
|
8 |
|
rhmpreimacn.r |
|
9 |
|
rhmpreimacn.s |
|
10 |
|
rhmpreimacn.f |
|
11 |
|
rhmpreimacn.1 |
|
12 |
|
rhmpreimacnlem.1 |
|
13 |
|
rhmpreimacnlem.v |
|
14 |
|
rhmpreimacnlem.w |
|
15 |
|
imaeq2 |
|
16 |
|
simpr |
|
17 |
10
|
elexd |
|
18 |
|
cnvexg |
|
19 |
|
imaexg |
|
20 |
17 18 19
|
3syl |
|
21 |
20
|
adantr |
|
22 |
7 15 16 21
|
fvmptd3 |
|
23 |
22
|
eleq1d |
|
24 |
23
|
pm5.32da |
|
25 |
9
|
adantr |
|
26 |
10
|
adantr |
|
27 |
|
simpr |
|
28 |
27 4
|
eleqtrdi |
Could not format ( ( ph /\ i e. B ) -> i e. ( PrmIdeal ` S ) ) : No typesetting found for |- ( ( ph /\ i e. B ) -> i e. ( PrmIdeal ` S ) ) with typecode |- |
29 |
3
|
rhmpreimaprmidl |
Could not format ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ i e. ( PrmIdeal ` S ) ) -> ( `' F " i ) e. A ) : No typesetting found for |- ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ i e. ( PrmIdeal ` S ) ) -> ( `' F " i ) e. A ) with typecode |- |
30 |
25 26 28 29
|
syl21anc |
|
31 |
30 7
|
fmptd |
|
32 |
31
|
ffnd |
|
33 |
|
elpreima |
|
34 |
32 33
|
syl |
|
35 |
|
sseq1 |
|
36 |
35
|
rabbidv |
|
37 |
|
eqid |
|
38 |
|
eqid |
|
39 |
|
eqid |
|
40 |
37 38 39
|
rhmimaidl |
|
41 |
10 11 12 40
|
syl3anc |
|
42 |
4
|
fvexi |
|
43 |
42
|
rabex |
|
44 |
43
|
a1i |
|
45 |
14 36 41 44
|
fvmptd3 |
|
46 |
45
|
eleq2d |
|
47 |
|
sseq2 |
|
48 |
47
|
elrab |
|
49 |
46 48
|
bitrdi |
|
50 |
|
eqid |
|
51 |
50 37
|
rhmf |
|
52 |
10 51
|
syl |
|
53 |
52
|
ffund |
|
54 |
50 38
|
lidlss |
|
55 |
12 54
|
syl |
|
56 |
52
|
fdmd |
|
57 |
55 56
|
sseqtrrd |
|
58 |
|
funimass3 |
|
59 |
53 57 58
|
syl2anc |
|
60 |
59
|
anbi2d |
|
61 |
9
|
adantr |
|
62 |
10
|
adantr |
|
63 |
16 4
|
eleqtrdi |
Could not format ( ( ph /\ g e. B ) -> g e. ( PrmIdeal ` S ) ) : No typesetting found for |- ( ( ph /\ g e. B ) -> g e. ( PrmIdeal ` S ) ) with typecode |- |
64 |
3
|
rhmpreimaprmidl |
Could not format ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ g e. ( PrmIdeal ` S ) ) -> ( `' F " g ) e. A ) : No typesetting found for |- ( ( ( S e. CRing /\ F e. ( R RingHom S ) ) /\ g e. ( PrmIdeal ` S ) ) -> ( `' F " g ) e. A ) with typecode |- |
65 |
61 62 63 64
|
syl21anc |
|
66 |
65
|
biantrurd |
|
67 |
66
|
pm5.32da |
|
68 |
49 60 67
|
3bitrd |
|
69 |
|
sseq2 |
|
70 |
69
|
elrab |
|
71 |
70
|
anbi2i |
|
72 |
68 71
|
bitr4di |
|
73 |
|
sseq1 |
|
74 |
73
|
rabbidv |
|
75 |
3
|
fvexi |
|
76 |
75
|
rabex |
|
77 |
76
|
a1i |
|
78 |
13 74 12 77
|
fvmptd3 |
|
79 |
78
|
eleq2d |
|
80 |
79
|
anbi2d |
|
81 |
72 80
|
bitr4d |
|
82 |
24 34 81
|
3bitr4rd |
|
83 |
82
|
eqrdv |
|