This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem algextdeglem2

Description: Lemma for algextdeg . Both the ring of polynomials P and the field L generated by K and the algebraic element A can be considered as modules over the elements of F . Then, the evaluation map G , mapping polynomials to their evaluation at A , is a module homomorphism between those modules. (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 algextdeglem2 
|- ( ph -> G e. ( P LMHom ( ( subringAlg ` L ) ` F ) ) )

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 issdrg 
 |-  ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
17 6 16 sylib 
 |-  ( ph -> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
18 17 simp2d 
 |-  ( ph -> F e. ( SubRing ` E ) )
19 eqid 
 |-  ( ( subringAlg ` E ) ` F ) = ( ( subringAlg ` E ) ` F )
20 19 sralmod 
 |-  ( F e. ( SubRing ` E ) -> ( ( subringAlg ` E ) ` F ) e. LMod )
21 18 20 syl 
 |-  ( ph -> ( ( subringAlg ` E ) ` F ) e. LMod )
22 eqid 
 |-  ( Base ` E ) = ( Base ` E )
23 eqid 
 |-  ( E |`s ( E fldGen ( F u. { A } ) ) ) = ( E |`s ( E fldGen ( F u. { A } ) ) )
24 5 flddrngd 
 |-  ( ph -> E e. DivRing )
25 subrgsubg 
 |-  ( F e. ( SubRing ` E ) -> F e. ( SubGrp ` E ) )
26 22 subgss 
 |-  ( F e. ( SubGrp ` E ) -> F C_ ( Base ` E ) )
27 18 25 26 3syl 
 |-  ( ph -> F C_ ( Base ` E ) )
28 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
29 5 fldcrngd 
 |-  ( ph -> E e. CRing )
30 8 1 22 28 29 18 irngssv 
 |-  ( ph -> ( E IntgRing F ) C_ ( Base ` E ) )
31 30 7 sseldd 
 |-  ( ph -> A e. ( Base ` E ) )
32 31 snssd 
 |-  ( ph -> { A } C_ ( Base ` E ) )
33 27 32 unssd 
 |-  ( ph -> ( F u. { A } ) C_ ( Base ` E ) )
34 22 24 33 fldgensdrg 
 |-  ( ph -> ( E fldGen ( F u. { A } ) ) e. ( SubDRing ` E ) )
35 issdrg 
 |-  ( ( E fldGen ( F u. { A } ) ) e. ( SubDRing ` E ) <-> ( E e. DivRing /\ ( E fldGen ( F u. { A } ) ) e. ( SubRing ` E ) /\ ( E |`s ( E fldGen ( F u. { A } ) ) ) e. DivRing ) )
36 34 35 sylib 
 |-  ( ph -> ( E e. DivRing /\ ( E fldGen ( F u. { A } ) ) e. ( SubRing ` E ) /\ ( E |`s ( E fldGen ( F u. { A } ) ) ) e. DivRing ) )
37 36 simp2d 
 |-  ( ph -> ( E fldGen ( F u. { A } ) ) e. ( SubRing ` E ) )
38 22 24 33 fldgenssid 
 |-  ( ph -> ( F u. { A } ) C_ ( E fldGen ( F u. { A } ) ) )
39 38 unssad 
 |-  ( ph -> F C_ ( E fldGen ( F u. { A } ) ) )
40 23 subsubrg 
 |-  ( ( E fldGen ( F u. { A } ) ) e. ( SubRing ` E ) -> ( F e. ( SubRing ` ( E |`s ( E fldGen ( F u. { A } ) ) ) ) <-> ( F e. ( SubRing ` E ) /\ F C_ ( E fldGen ( F u. { A } ) ) ) ) )
41 40 biimpar 
 |-  ( ( ( E fldGen ( F u. { A } ) ) e. ( SubRing ` E ) /\ ( F e. ( SubRing ` E ) /\ F C_ ( E fldGen ( F u. { A } ) ) ) ) -> F e. ( SubRing ` ( E |`s ( E fldGen ( F u. { A } ) ) ) ) )
42 37 18 39 41 syl12anc 
 |-  ( ph -> F e. ( SubRing ` ( E |`s ( E fldGen ( F u. { A } ) ) ) ) )
43 19 22 23 37 42 lsssra 
 |-  ( ph -> ( E fldGen ( F u. { A } ) ) e. ( LSubSp ` ( ( subringAlg ` E ) ` F ) ) )
44 1 fveq2i 
 |-  ( Poly1 ` K ) = ( Poly1 ` ( E |`s F ) )
45 9 44 eqtri 
 |-  P = ( Poly1 ` ( E |`s F ) )
46 5 adantr 
 |-  ( ( ph /\ p e. U ) -> E e. Field )
47 6 adantr 
 |-  ( ( ph /\ p e. U ) -> F e. ( SubDRing ` E ) )
48 31 adantr 
 |-  ( ( ph /\ p e. U ) -> A e. ( Base ` E ) )
49 simpr 
 |-  ( ( ph /\ p e. U ) -> p e. U )
50 22 8 45 10 46 47 48 49 evls1fldgencl 
 |-  ( ( ph /\ p e. U ) -> ( ( O ` p ) ` A ) e. ( E fldGen ( F u. { A } ) ) )
51 50 ralrimiva 
 |-  ( ph -> A. p e. U ( ( O ` p ) ` A ) e. ( E fldGen ( F u. { A } ) ) )
52 11 rnmptss 
 |-  ( A. p e. U ( ( O ` p ) ` A ) e. ( E fldGen ( F u. { A } ) ) -> ran G C_ ( E fldGen ( F u. { A } ) ) )
53 51 52 syl 
 |-  ( ph -> ran G C_ ( E fldGen ( F u. { A } ) ) )
54 8 45 22 10 29 18 31 11 19 evls1maplmhm 
 |-  ( ph -> G e. ( P LMHom ( ( subringAlg ` E ) ` F ) ) )
55 eqid 
 |-  ( ( ( subringAlg ` E ) ` F ) |`s ( E fldGen ( F u. { A } ) ) ) = ( ( ( subringAlg ` E ) ` F ) |`s ( E fldGen ( F u. { A } ) ) )
56 eqid 
 |-  ( LSubSp ` ( ( subringAlg ` E ) ` F ) ) = ( LSubSp ` ( ( subringAlg ` E ) ` F ) )
57 55 56 reslmhm2b 
 |-  ( ( ( ( subringAlg ` E ) ` F ) e. LMod /\ ( E fldGen ( F u. { A } ) ) e. ( LSubSp ` ( ( subringAlg ` E ) ` F ) ) /\ ran G C_ ( E fldGen ( F u. { A } ) ) ) -> ( G e. ( P LMHom ( ( subringAlg ` E ) ` F ) ) <-> G e. ( P LMHom ( ( ( subringAlg ` E ) ` F ) |`s ( E fldGen ( F u. { A } ) ) ) ) ) )
58 57 biimpa 
 |-  ( ( ( ( ( subringAlg ` E ) ` F ) e. LMod /\ ( E fldGen ( F u. { A } ) ) e. ( LSubSp ` ( ( subringAlg ` E ) ` F ) ) /\ ran G C_ ( E fldGen ( F u. { A } ) ) ) /\ G e. ( P LMHom ( ( subringAlg ` E ) ` F ) ) ) -> G e. ( P LMHom ( ( ( subringAlg ` E ) ` F ) |`s ( E fldGen ( F u. { A } ) ) ) ) )
59 21 43 53 54 58 syl31anc 
 |-  ( ph -> G e. ( P LMHom ( ( ( subringAlg ` E ) ` F ) |`s ( E fldGen ( F u. { A } ) ) ) ) )
60 22 24 33 fldgenssv 
 |-  ( ph -> ( E fldGen ( F u. { A } ) ) C_ ( Base ` E ) )
61 22 2 60 39 5 resssra 
 |-  ( ph -> ( ( subringAlg ` L ) ` F ) = ( ( ( subringAlg ` E ) ` F ) |`s ( E fldGen ( F u. { A } ) ) ) )
62 61 oveq2d 
 |-  ( ph -> ( P LMHom ( ( subringAlg ` L ) ` F ) ) = ( P LMHom ( ( ( subringAlg ` E ) ` F ) |`s ( E fldGen ( F u. { A } ) ) ) ) )
63 59 62 eleqtrrd 
 |-  ( ph -> G e. ( P LMHom ( ( subringAlg ` L ) ` F ) ) )