Step |
Hyp |
Ref |
Expression |
1 |
|
nzrring |
|
2 |
|
eqid |
|
3 |
|
eqid |
|
4 |
2 3
|
lidl0 |
|
5 |
1 4
|
syl |
|
6 |
|
fvex |
|
7 |
|
hashsng |
|
8 |
6 7
|
ax-mp |
|
9 |
|
simpr |
|
10 |
9
|
fveq2d |
|
11 |
8 10
|
eqtr3id |
|
12 |
|
1red |
|
13 |
|
eqid |
|
14 |
13
|
isnzr2hash |
|
15 |
14
|
simprbi |
|
16 |
15
|
adantr |
|
17 |
12 16
|
ltned |
|
18 |
17
|
neneqd |
|
19 |
11 18
|
pm2.65da |
|
20 |
19
|
neqned |
|
21 |
13
|
ssmxidl |
Could not format ( ( R e. Ring /\ { ( 0g ` R ) } e. ( LIdeal ` R ) /\ { ( 0g ` R ) } =/= ( Base ` R ) ) -> E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m ) : No typesetting found for |- ( ( R e. Ring /\ { ( 0g ` R ) } e. ( LIdeal ` R ) /\ { ( 0g ` R ) } =/= ( Base ` R ) ) -> E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m ) with typecode |- |
22 |
1 5 20 21
|
syl3anc |
Could not format ( R e. NzRing -> E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m ) : No typesetting found for |- ( R e. NzRing -> E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m ) with typecode |- |
23 |
|
df-rex |
Could not format ( E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m <-> E. m ( m e. ( MaxIdeal ` R ) /\ { ( 0g ` R ) } C_ m ) ) : No typesetting found for |- ( E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m <-> E. m ( m e. ( MaxIdeal ` R ) /\ { ( 0g ` R ) } C_ m ) ) with typecode |- |
24 |
|
exsimpl |
Could not format ( E. m ( m e. ( MaxIdeal ` R ) /\ { ( 0g ` R ) } C_ m ) -> E. m m e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( E. m ( m e. ( MaxIdeal ` R ) /\ { ( 0g ` R ) } C_ m ) -> E. m m e. ( MaxIdeal ` R ) ) with typecode |- |
25 |
23 24
|
sylbi |
Could not format ( E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m -> E. m m e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m -> E. m m e. ( MaxIdeal ` R ) ) with typecode |- |
26 |
22 25
|
syl |
Could not format ( R e. NzRing -> E. m m e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( R e. NzRing -> E. m m e. ( MaxIdeal ` R ) ) with typecode |- |