Metamath Proof Explorer

Theorem algextdeglem5

Description: Lemma for algextdeg . The subspace Z of annihilators of A is a principal ideal generated by the minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses algextdeg.k 
|- K = ( E |`s F )
algextdeg.l 
|- L = ( E |`s ( E fldGen ( F u. { A } ) ) )
algextdeg.d 
|- D = ( deg1 ` E )
algextdeg.m 
|- M = ( E minPoly F )
algextdeg.f 
|- ( ph -> E e. Field )
algextdeg.e 
|- ( ph -> F e. ( SubDRing ` E ) )
algextdeg.a 
|- ( ph -> A e. ( E IntgRing F ) )
algextdeglem.o 
|- O = ( E evalSub1 F )
algextdeglem.y 
|- P = ( Poly1 ` K )
algextdeglem.u 
|- U = ( Base ` P )
algextdeglem.g 
|- G = ( p e. U |-> ( ( O ` p ) ` A ) )
algextdeglem.n 
|- N = ( x e. U |-> [ x ] ( P ~QG Z ) )
algextdeglem.z 
|- Z = ( `' G " { ( 0g ` L ) } )
algextdeglem.q 
|- Q = ( P /s ( P ~QG Z ) )
algextdeglem.j 
|- J = ( p e. ( Base ` Q ) |-> U. ( G " p ) )
Assertion algextdeglem5 
|- ( ph -> Z = ( ( RSpan ` P ) ` { ( M ` A ) } ) )

Proof

Step Hyp Ref Expression
1 algextdeg.k 
 |-  K = ( E |`s F )
2 algextdeg.l 
 |-  L = ( E |`s ( E fldGen ( F u. { A } ) ) )
3 algextdeg.d 
 |-  D = ( deg1 ` E )
4 algextdeg.m 
 |-  M = ( E minPoly F )
5 algextdeg.f 
 |-  ( ph -> E e. Field )
6 algextdeg.e 
 |-  ( ph -> F e. ( SubDRing ` E ) )
7 algextdeg.a 
 |-  ( ph -> A e. ( E IntgRing F ) )
8 algextdeglem.o 
 |-  O = ( E evalSub1 F )
9 algextdeglem.y 
 |-  P = ( Poly1 ` K )
10 algextdeglem.u 
 |-  U = ( Base ` P )
11 algextdeglem.g 
 |-  G = ( p e. U |-> ( ( O ` p ) ` A ) )
12 algextdeglem.n 
 |-  N = ( x e. U |-> [ x ] ( P ~QG Z ) )
13 algextdeglem.z 
 |-  Z = ( `' G " { ( 0g ` L ) } )
14 algextdeglem.q 
 |-  Q = ( P /s ( P ~QG Z ) )
15 algextdeglem.j 
 |-  J = ( p e. ( Base ` Q ) |-> U. ( G " p ) )
16 1 fveq2i 
 |-  ( Poly1 ` K ) = ( Poly1 ` ( E |`s F ) )
17 9 16 eqtri 
 |-  P = ( Poly1 ` ( E |`s F ) )
18 eqid 
 |-  ( Base ` E ) = ( Base ` E )
19 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
20 5 fldcrngd 
 |-  ( ph -> E e. CRing )
21 issdrg 
 |-  ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
22 6 21 sylib 
 |-  ( ph -> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
23 22 simp2d 
 |-  ( ph -> F e. ( SubRing ` E ) )
24 8 1 18 19 20 23 irngssv 
 |-  ( ph -> ( E IntgRing F ) C_ ( Base ` E ) )
25 24 7 sseldd 
 |-  ( ph -> A e. ( Base ` E ) )
26 eqid 
 |-  { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } = { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) }
27 eqid 
 |-  ( RSpan ` P ) = ( RSpan ` P )
28 eqid 
 |-  ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) )
29 8 17 18 5 6 25 19 26 27 28 ply1annig1p 
 |-  ( ph -> { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } = ( ( RSpan ` P ) ` { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) } ) )
30 20 crnggrpd 
 |-  ( ph -> E e. Grp )
31 30 grpmndd 
 |-  ( ph -> E e. Mnd )
32 5 flddrngd 
 |-  ( ph -> E e. DivRing )
33 subrgsubg 
 |-  ( F e. ( SubRing ` E ) -> F e. ( SubGrp ` E ) )
34 18 subgss 
 |-  ( F e. ( SubGrp ` E ) -> F C_ ( Base ` E ) )
35 23 33 34 3syl 
 |-  ( ph -> F C_ ( Base ` E ) )
36 25 snssd 
 |-  ( ph -> { A } C_ ( Base ` E ) )
37 35 36 unssd 
 |-  ( ph -> ( F u. { A } ) C_ ( Base ` E ) )
38 18 32 37 fldgensdrg 
 |-  ( ph -> ( E fldGen ( F u. { A } ) ) e. ( SubDRing ` E ) )
39 sdrgsubrg 
 |-  ( ( E fldGen ( F u. { A } ) ) e. ( SubDRing ` E ) -> ( E fldGen ( F u. { A } ) ) e. ( SubRing ` E ) )
40 subrgsubg 
 |-  ( ( E fldGen ( F u. { A } ) ) e. ( SubRing ` E ) -> ( E fldGen ( F u. { A } ) ) e. ( SubGrp ` E ) )
41 19 subg0cl 
 |-  ( ( E fldGen ( F u. { A } ) ) e. ( SubGrp ` E ) -> ( 0g ` E ) e. ( E fldGen ( F u. { A } ) ) )
42 38 39 40 41 4syl 
 |-  ( ph -> ( 0g ` E ) e. ( E fldGen ( F u. { A } ) ) )
43 18 32 37 fldgenssv 
 |-  ( ph -> ( E fldGen ( F u. { A } ) ) C_ ( Base ` E ) )
44 2 18 19 ress0g 
 |-  ( ( E e. Mnd /\ ( 0g ` E ) e. ( E fldGen ( F u. { A } ) ) /\ ( E fldGen ( F u. { A } ) ) C_ ( Base ` E ) ) -> ( 0g ` E ) = ( 0g ` L ) )
45 31 42 43 44 syl3anc 
 |-  ( ph -> ( 0g ` E ) = ( 0g ` L ) )
46 45 sneqd 
 |-  ( ph -> { ( 0g ` E ) } = { ( 0g ` L ) } )
47 46 imaeq2d 
 |-  ( ph -> ( `' G " { ( 0g ` E ) } ) = ( `' G " { ( 0g ` L ) } ) )
48 13 47 eqtr4id 
 |-  ( ph -> Z = ( `' G " { ( 0g ` E ) } ) )
49 10 mpteq1i 
 |-  ( p e. U |-> ( ( O ` p ) ` A ) ) = ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) )
50 11 49 eqtri 
 |-  G = ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) )
51 8 17 18 20 23 25 19 26 50 ply1annidllem 
 |-  ( ph -> { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } = ( `' G " { ( 0g ` E ) } ) )
52 48 51 eqtr4d 
 |-  ( ph -> Z = { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } )
53 8 17 18 5 6 25 19 26 27 28 4 minplyval 
 |-  ( ph -> ( M ` A ) = ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) )
54 53 sneqd 
 |-  ( ph -> { ( M ` A ) } = { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) } )
55 54 fveq2d 
 |-  ( ph -> ( ( RSpan ` P ) ` { ( M ` A ) } ) = ( ( RSpan ` P ) ` { ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) } ) )
56 29 52 55 3eqtr4d 
 |-  ( ph -> Z = ( ( RSpan ` P ) ` { ( M ` A ) } ) )