| Step |
Hyp |
Ref |
Expression |
| 1 |
|
irngnminplynz.z |
|- Z = ( 0g ` ( Poly1 ` E ) ) |
| 2 |
|
irngnminplynz.e |
|- ( ph -> E e. Field ) |
| 3 |
|
irngnminplynz.f |
|- ( ph -> F e. ( SubDRing ` E ) ) |
| 4 |
|
irngnminplynz.m |
|- M = ( E minPoly F ) |
| 5 |
|
irngnminplynz.a |
|- ( ph -> A e. ( E IntgRing F ) ) |
| 6 |
|
minplym1p.1 |
|- U = ( Monic1p ` ( E |`s F ) ) |
| 7 |
|
eqid |
|- ( E evalSub1 F ) = ( E evalSub1 F ) |
| 8 |
|
eqid |
|- ( Poly1 ` ( E |`s F ) ) = ( Poly1 ` ( E |`s F ) ) |
| 9 |
|
eqid |
|- ( Base ` E ) = ( Base ` E ) |
| 10 |
|
eqid |
|- ( E |`s F ) = ( E |`s F ) |
| 11 |
|
eqid |
|- ( 0g ` E ) = ( 0g ` E ) |
| 12 |
2
|
fldcrngd |
|- ( ph -> E e. CRing ) |
| 13 |
|
sdrgsubrg |
|- ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) ) |
| 14 |
3 13
|
syl |
|- ( ph -> F e. ( SubRing ` E ) ) |
| 15 |
7 10 9 11 12 14
|
irngssv |
|- ( ph -> ( E IntgRing F ) C_ ( Base ` E ) ) |
| 16 |
15 5
|
sseldd |
|- ( ph -> A e. ( Base ` E ) ) |
| 17 |
|
eqid |
|- { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } = { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } |
| 18 |
|
eqid |
|- ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) = ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) |
| 19 |
|
eqid |
|- ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) ) |
| 20 |
7 8 9 2 3 16 11 17 18 19 4
|
minplyval |
|- ( ph -> ( M ` A ) = ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) ) |
| 21 |
10
|
sdrgdrng |
|- ( F e. ( SubDRing ` E ) -> ( E |`s F ) e. DivRing ) |
| 22 |
3 21
|
syl |
|- ( ph -> ( E |`s F ) e. DivRing ) |
| 23 |
7 8 9 12 14 16 11 17
|
ply1annidl |
|- ( ph -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } e. ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) ) |
| 24 |
20
|
sneqd |
|- ( ph -> { ( M ` A ) } = { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) } ) |
| 25 |
24
|
fveq2d |
|- ( ph -> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( M ` A ) } ) = ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) } ) ) |
| 26 |
7 8 9 2 3 16 11 17 18 19
|
ply1annig1p |
|- ( ph -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } = ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) } ) ) |
| 27 |
25 26
|
eqtr4d |
|- ( ph -> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( M ` A ) } ) = { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) |
| 28 |
22
|
drngringd |
|- ( ph -> ( E |`s F ) e. Ring ) |
| 29 |
8
|
ply1ring |
|- ( ( E |`s F ) e. Ring -> ( Poly1 ` ( E |`s F ) ) e. Ring ) |
| 30 |
28 29
|
syl |
|- ( ph -> ( Poly1 ` ( E |`s F ) ) e. Ring ) |
| 31 |
7 8 9 2 3 16 11 17 18 19 4
|
minplycl |
|- ( ph -> ( M ` A ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) ) |
| 32 |
1 2 3 4 5
|
irngnminplynz |
|- ( ph -> ( M ` A ) =/= Z ) |
| 33 |
|
eqid |
|- ( Poly1 ` E ) = ( Poly1 ` E ) |
| 34 |
|
eqid |
|- ( Base ` ( Poly1 ` ( E |`s F ) ) ) = ( Base ` ( Poly1 ` ( E |`s F ) ) ) |
| 35 |
33 10 8 34 14 1
|
ressply10g |
|- ( ph -> Z = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) ) |
| 36 |
32 35
|
neeqtrd |
|- ( ph -> ( M ` A ) =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) ) |
| 37 |
|
eqid |
|- ( 0g ` ( Poly1 ` ( E |`s F ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) |
| 38 |
34 37 18
|
pidlnz |
|- ( ( ( Poly1 ` ( E |`s F ) ) e. Ring /\ ( M ` A ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) /\ ( M ` A ) =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) ) -> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( M ` A ) } ) =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } ) |
| 39 |
30 31 36 38
|
syl3anc |
|- ( ph -> ( ( RSpan ` ( Poly1 ` ( E |`s F ) ) ) ` { ( M ` A ) } ) =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } ) |
| 40 |
27 39
|
eqnetrrd |
|- ( ph -> { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } ) |
| 41 |
|
eqid |
|- ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) = ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) |
| 42 |
|
eqid |
|- ( deg1 ` ( E |`s F ) ) = ( deg1 ` ( E |`s F ) ) |
| 43 |
8 19 37 41 42 6
|
ig1pval3 |
|- ( ( ( E |`s F ) e. DivRing /\ { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } e. ( LIdeal ` ( Poly1 ` ( E |`s F ) ) ) /\ { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } =/= { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } ) -> ( ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } /\ ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. U /\ ( ( deg1 ` ( E |`s F ) ) ` ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) ) = inf ( ( ( deg1 ` ( E |`s F ) ) " ( { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } \ { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } ) ) , RR , < ) ) ) |
| 44 |
22 23 40 43
|
syl3anc |
|- ( ph -> ( ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } /\ ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. U /\ ( ( deg1 ` ( E |`s F ) ) ` ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) ) = inf ( ( ( deg1 ` ( E |`s F ) ) " ( { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } \ { ( 0g ` ( Poly1 ` ( E |`s F ) ) ) } ) ) , RR , < ) ) ) |
| 45 |
44
|
simp2d |
|- ( ph -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom ( E evalSub1 F ) | ( ( ( E evalSub1 F ) ` q ) ` A ) = ( 0g ` E ) } ) e. U ) |
| 46 |
20 45
|
eqeltrd |
|- ( ph -> ( M ` A ) e. U ) |