Metamath Proof Explorer

Theorem minplyirredlem

Description: Lemma for minplyirred . (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses ply1annig1p.o 
|- O = ( E evalSub1 F )
ply1annig1p.p 
|- P = ( Poly1 ` ( E |`s F ) )
ply1annig1p.b 
|- B = ( Base ` E )
ply1annig1p.e 
|- ( ph -> E e. Field )
ply1annig1p.f 
|- ( ph -> F e. ( SubDRing ` E ) )
ply1annig1p.a 
|- ( ph -> A e. B )
minplyirred.1 
|- M = ( E minPoly F )
minplyirred.2 
|- Z = ( 0g ` P )
minplyirred.3 
|- ( ph -> ( M ` A ) =/= Z )
minplyirredlem.1 
|- ( ph -> G e. ( Base ` P ) )
minplyirredlem.2 
|- ( ph -> H e. ( Base ` P ) )
minplyirredlem.3 
|- ( ph -> ( G ( .r ` P ) H ) = ( M ` A ) )
minplyirredlem.4 
|- ( ph -> ( ( O ` G ) ` A ) = ( 0g ` E ) )
minplyirredlem.5 
|- ( ph -> G =/= Z )
minplyirredlem.6 
|- ( ph -> H =/= Z )
Assertion minplyirredlem 
|- ( ph -> H e. ( Unit ` P ) )

Proof

Step Hyp Ref Expression
1 ply1annig1p.o 
 |-  O = ( E evalSub1 F )
2 ply1annig1p.p 
 |-  P = ( Poly1 ` ( E |`s F ) )
3 ply1annig1p.b 
 |-  B = ( Base ` E )
4 ply1annig1p.e 
 |-  ( ph -> E e. Field )
5 ply1annig1p.f 
 |-  ( ph -> F e. ( SubDRing ` E ) )
6 ply1annig1p.a 
 |-  ( ph -> A e. B )
7 minplyirred.1 
 |-  M = ( E minPoly F )
8 minplyirred.2 
 |-  Z = ( 0g ` P )
9 minplyirred.3 
 |-  ( ph -> ( M ` A ) =/= Z )
10 minplyirredlem.1 
 |-  ( ph -> G e. ( Base ` P ) )
11 minplyirredlem.2 
 |-  ( ph -> H e. ( Base ` P ) )
12 minplyirredlem.3 
 |-  ( ph -> ( G ( .r ` P ) H ) = ( M ` A ) )
13 minplyirredlem.4 
 |-  ( ph -> ( ( O ` G ) ` A ) = ( 0g ` E ) )
14 minplyirredlem.5 
 |-  ( ph -> G =/= Z )
15 minplyirredlem.6 
 |-  ( ph -> H =/= Z )
16 eqid 
 |-  ( E |`s F ) = ( E |`s F )
17 16 sdrgdrng 
 |-  ( F e. ( SubDRing ` E ) -> ( E |`s F ) e. DivRing )
18 5 17 syl 
 |-  ( ph -> ( E |`s F ) e. DivRing )
19 18 drngringd 
 |-  ( ph -> ( E |`s F ) e. Ring )
20 eqid 
 |-  ( deg1 ` ( E |`s F ) ) = ( deg1 ` ( E |`s F ) )
21 eqid 
 |-  ( Base ` P ) = ( Base ` P )
22 20 2 8 21 deg1nn0cl 
 |-  ( ( ( E |`s F ) e. Ring /\ G e. ( Base ` P ) /\ G =/= Z ) -> ( ( deg1 ` ( E |`s F ) ) ` G ) e. NN0 )
23 19 10 14 22 syl3anc 
 |-  ( ph -> ( ( deg1 ` ( E |`s F ) ) ` G ) e. NN0 )
24 23 nn0red 
 |-  ( ph -> ( ( deg1 ` ( E |`s F ) ) ` G ) e. RR )
25 20 2 8 21 deg1nn0cl 
 |-  ( ( ( E |`s F ) e. Ring /\ H e. ( Base ` P ) /\ H =/= Z ) -> ( ( deg1 ` ( E |`s F ) ) ` H ) e. NN0 )
26 19 11 15 25 syl3anc 
 |-  ( ph -> ( ( deg1 ` ( E |`s F ) ) ` H ) e. NN0 )
27 26 nn0red 
 |-  ( ph -> ( ( deg1 ` ( E |`s F ) ) ` H ) e. RR )
28 eqid 
 |-  ( RLReg ` ( E |`s F ) ) = ( RLReg ` ( E |`s F ) )
29 eqid 
 |-  ( .r ` P ) = ( .r ` P )
30 fldsdrgfld 
 |-  ( ( E e. Field /\ F e. ( SubDRing ` E ) ) -> ( E |`s F ) e. Field )
31 4 5 30 syl2anc 
 |-  ( ph -> ( E |`s F ) e. Field )
32 fldidom 
 |-  ( ( E |`s F ) e. Field -> ( E |`s F ) e. IDomn )
33 31 32 syl 
 |-  ( ph -> ( E |`s F ) e. IDomn )
34 33 idomdomd 
 |-  ( ph -> ( E |`s F ) e. Domn )
35 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
36 20 2 8 21 28 35 deg1ldgdomn 
 |-  ( ( ( E |`s F ) e. Domn /\ G e. ( Base ` P ) /\ G =/= Z ) -> ( ( coe1 ` G ) ` ( ( deg1 ` ( E |`s F ) ) ` G ) ) e. ( RLReg ` ( E |`s F ) ) )
37 34 10 14 36 syl3anc 
 |-  ( ph -> ( ( coe1 ` G ) ` ( ( deg1 ` ( E |`s F ) ) ` G ) ) e. ( RLReg ` ( E |`s F ) ) )
38 20 2 28 21 29 8 19 10 14 37 11 15 deg1mul2 
 |-  ( ph -> ( ( deg1 ` ( E |`s F ) ) ` ( G ( .r ` P ) H ) ) = ( ( ( deg1 ` ( E |`s F ) ) ` G ) + ( ( deg1 ` ( E |`s F ) ) ` H ) ) )
39 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
40 eqid 
 |-  { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } = { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) }
41 eqid 
 |-  ( RSpan ` P ) = ( RSpan ` P )
42 eqid 
 |-  ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) )
43 1 2 3 4 5 6 39 40 41 42 7 minplyval 
 |-  ( ph -> ( M ` A ) = ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) )
44 12 43 eqtrd 
 |-  ( ph -> ( G ( .r ` P ) H ) = ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) )
45 44 fveq2d 
 |-  ( ph -> ( ( deg1 ` ( E |`s F ) ) ` ( G ( .r ` P ) H ) ) = ( ( deg1 ` ( E |`s F ) ) ` ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) ) )
46 4 fldcrngd 
 |-  ( ph -> E e. CRing )
47 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
48 5 47 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
49 1 2 3 46 48 6 39 40 ply1annidl 
 |-  ( ph -> { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } e. ( LIdeal ` P ) )
50 fveq2 
 |-  ( q = G -> ( O ` q ) = ( O ` G ) )
51 50 fveq1d 
 |-  ( q = G -> ( ( O ` q ) ` A ) = ( ( O ` G ) ` A ) )
52 51 eqeq1d 
 |-  ( q = G -> ( ( ( O ` q ) ` A ) = ( 0g ` E ) <-> ( ( O ` G ) ` A ) = ( 0g ` E ) ) )
53 1 2 21 46 48 evls1dm 
 |-  ( ph -> dom O = ( Base ` P ) )
54 10 53 eleqtrrd 
 |-  ( ph -> G e. dom O )
55 52 54 13 elrabd 
 |-  ( ph -> G e. { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } )
56 2 42 21 18 49 20 8 55 14 ig1pmindeg 
 |-  ( ph -> ( ( deg1 ` ( E |`s F ) ) ` ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) ) <_ ( ( deg1 ` ( E |`s F ) ) ` G ) )
57 45 56 eqbrtrd 
 |-  ( ph -> ( ( deg1 ` ( E |`s F ) ) ` ( G ( .r ` P ) H ) ) <_ ( ( deg1 ` ( E |`s F ) ) ` G ) )
58 38 57 eqbrtrrd 
 |-  ( ph -> ( ( ( deg1 ` ( E |`s F ) ) ` G ) + ( ( deg1 ` ( E |`s F ) ) ` H ) ) <_ ( ( deg1 ` ( E |`s F ) ) ` G ) )
59 leaddle0 
 |-  ( ( ( ( deg1 ` ( E |`s F ) ) ` G ) e. RR /\ ( ( deg1 ` ( E |`s F ) ) ` H ) e. RR ) -> ( ( ( ( deg1 ` ( E |`s F ) ) ` G ) + ( ( deg1 ` ( E |`s F ) ) ` H ) ) <_ ( ( deg1 ` ( E |`s F ) ) ` G ) <-> ( ( deg1 ` ( E |`s F ) ) ` H ) <_ 0 ) )
60 59 biimpa 
 |-  ( ( ( ( ( deg1 ` ( E |`s F ) ) ` G ) e. RR /\ ( ( deg1 ` ( E |`s F ) ) ` H ) e. RR ) /\ ( ( ( deg1 ` ( E |`s F ) ) ` G ) + ( ( deg1 ` ( E |`s F ) ) ` H ) ) <_ ( ( deg1 ` ( E |`s F ) ) ` G ) ) -> ( ( deg1 ` ( E |`s F ) ) ` H ) <_ 0 )
61 24 27 58 60 syl21anc 
 |-  ( ph -> ( ( deg1 ` ( E |`s F ) ) ` H ) <_ 0 )
62 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
63 20 2 21 62 deg1le0 
 |-  ( ( ( E |`s F ) e. Ring /\ H e. ( Base ` P ) ) -> ( ( ( deg1 ` ( E |`s F ) ) ` H ) <_ 0 <-> H = ( ( algSc ` P ) ` ( ( coe1 ` H ) ` 0 ) ) ) )
64 63 biimpa 
 |-  ( ( ( ( E |`s F ) e. Ring /\ H e. ( Base ` P ) ) /\ ( ( deg1 ` ( E |`s F ) ) ` H ) <_ 0 ) -> H = ( ( algSc ` P ) ` ( ( coe1 ` H ) ` 0 ) ) )
65 19 11 61 64 syl21anc 
 |-  ( ph -> H = ( ( algSc ` P ) ` ( ( coe1 ` H ) ` 0 ) ) )
66 eqid 
 |-  ( Base ` ( E |`s F ) ) = ( Base ` ( E |`s F ) )
67 eqid 
 |-  ( 0g ` ( E |`s F ) ) = ( 0g ` ( E |`s F ) )
68 0nn0 
 |-  0 e. NN0
69 eqid 
 |-  ( coe1 ` H ) = ( coe1 ` H )
70 69 21 2 66 coe1fvalcl 
 |-  ( ( H e. ( Base ` P ) /\ 0 e. NN0 ) -> ( ( coe1 ` H ) ` 0 ) e. ( Base ` ( E |`s F ) ) )
71 11 68 70 sylancl 
 |-  ( ph -> ( ( coe1 ` H ) ` 0 ) e. ( Base ` ( E |`s F ) ) )
72 20 2 67 21 8 19 11 61 deg1le0eq0 
 |-  ( ph -> ( H = Z <-> ( ( coe1 ` H ) ` 0 ) = ( 0g ` ( E |`s F ) ) ) )
73 72 necon3bid 
 |-  ( ph -> ( H =/= Z <-> ( ( coe1 ` H ) ` 0 ) =/= ( 0g ` ( E |`s F ) ) ) )
74 15 73 mpbid 
 |-  ( ph -> ( ( coe1 ` H ) ` 0 ) =/= ( 0g ` ( E |`s F ) ) )
75 2 62 66 67 31 71 74 ply1asclunit 
 |-  ( ph -> ( ( algSc ` P ) ` ( ( coe1 ` H ) ` 0 ) ) e. ( Unit ` P ) )
76 65 75 eqeltrd 
 |-  ( ph -> H e. ( Unit ` P ) )