Step |
Hyp |
Ref |
Expression |
1 |
|
0ringprmidl.1 |
|
2 |
|
prmidlssidl |
Could not format ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) : No typesetting found for |- ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) with typecode |- |
3 |
2
|
adantr |
Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) with typecode |- |
4 |
|
eqid |
|
5 |
1 4
|
0ringidl |
|
6 |
3 5
|
sseqtrd |
Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) C_ { { ( 0g ` R ) } } ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) C_ { { ( 0g ` R ) } } ) with typecode |- |
7 |
6
|
sselda |
Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i e. { { ( 0g ` R ) } } ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i e. { { ( 0g ` R ) } } ) with typecode |- |
8 |
|
elsni |
|
9 |
7 8
|
syl |
Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i = { ( 0g ` R ) } ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i = { ( 0g ` R ) } ) with typecode |- |
10 |
|
eqid |
|
11 |
1 10
|
prmidlnr |
Could not format ( ( R e. Ring /\ i e. ( PrmIdeal ` R ) ) -> i =/= B ) : No typesetting found for |- ( ( R e. Ring /\ i e. ( PrmIdeal ` R ) ) -> i =/= B ) with typecode |- |
12 |
11
|
adantlr |
Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i =/= B ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i =/= B ) with typecode |- |
13 |
1 4
|
0ring |
|
14 |
13
|
adantr |
Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> B = { ( 0g ` R ) } ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> B = { ( 0g ` R ) } ) with typecode |- |
15 |
12 14
|
neeqtrd |
Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i =/= { ( 0g ` R ) } ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> i =/= { ( 0g ` R ) } ) with typecode |- |
16 |
15
|
neneqd |
Could not format ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> -. i = { ( 0g ` R ) } ) : No typesetting found for |- ( ( ( R e. Ring /\ ( # ` B ) = 1 ) /\ i e. ( PrmIdeal ` R ) ) -> -. i = { ( 0g ` R ) } ) with typecode |- |
17 |
9 16
|
pm2.65da |
Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> -. i e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> -. i e. ( PrmIdeal ` R ) ) with typecode |- |
18 |
17
|
eq0rdv |
Could not format ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) = (/) ) : No typesetting found for |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( PrmIdeal ` R ) = (/) ) with typecode |- |