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 ⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
algextdeg.l ⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
algextdeg.d ⊢ 𝐷 = ( deg1 ‘ 𝐸 )
algextdeg.m ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
algextdeg.f ⊢ ( 𝜑 → 𝐸 ∈ Field )
algextdeg.e ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
algextdeg.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
algextdeglem.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
algextdeglem.y ⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
algextdeglem.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
algextdeglem.g ⊢ 𝐺 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
algextdeglem.n ⊢ 𝑁 = ( 𝑥 ∈ 𝑈 ↦ [ 𝑥 ] ( 𝑃 ~QG 𝑍 ) )
algextdeglem.z ⊢ 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } )
algextdeglem.q ⊢ 𝑄 = ( 𝑃 /s ( 𝑃 ~QG 𝑍 ) )
algextdeglem.j ⊢ 𝐽 = ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐺 “ 𝑝 ) )
Assertion algextdeglem2 ( 𝜑 → 𝐺 ∈ ( 𝑃 LMHom ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 algextdeg.k ⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
2 algextdeg.l ⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
3 algextdeg.d ⊢ 𝐷 = ( deg1 ‘ 𝐸 )
4 algextdeg.m ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
5 algextdeg.f ⊢ ( 𝜑 → 𝐸 ∈ Field )
6 algextdeg.e ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
7 algextdeg.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
8 algextdeglem.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
9 algextdeglem.y ⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
10 algextdeglem.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
11 algextdeglem.g ⊢ 𝐺 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
12 algextdeglem.n ⊢ 𝑁 = ( 𝑥 ∈ 𝑈 ↦ [ 𝑥 ] ( 𝑃 ~QG 𝑍 ) )
13 algextdeglem.z ⊢ 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } )
14 algextdeglem.q ⊢ 𝑄 = ( 𝑃 /s ( 𝑃 ~QG 𝑍 ) )
15 algextdeglem.j ⊢ 𝐽 = ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐺 “ 𝑝 ) )
16 issdrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
17 6 16 sylib ⊢ ( 𝜑 → ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
18 17 simp2d ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
19 eqid ⊢ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) = ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 )
20 19 sralmod ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LMod )
21 18 20 syl ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LMod )
22 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
23 eqid ⊢ ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
24 5 flddrngd ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
25 subrgsubg ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → 𝐹 ∈ ( SubGrp ‘ 𝐸 ) )
26 22 subgss ⊢ ( 𝐹 ∈ ( SubGrp ‘ 𝐸 ) → 𝐹 ⊆ ( Base ‘ 𝐸 ) )
27 18 25 26 3syl ⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐸 ) )
28 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
29 5 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
30 8 1 22 28 29 18 irngssv ⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
31 30 7 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐸 ) )
32 31 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ ( Base ‘ 𝐸 ) )
33 27 32 unssd ⊢ ( 𝜑 → ( 𝐹 ∪ { 𝐴 } ) ⊆ ( Base ‘ 𝐸 ) )
34 22 24 33 fldgensdrg ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ 𝐸 ) )
35 issdrg ⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ∈ DivRing ) )
36 34 35 sylib ⊢ ( 𝜑 → ( 𝐸 ∈ DivRing ∧ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ∈ DivRing ) )
37 36 simp2d ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) )
38 22 24 33 fldgenssid ⊢ ( 𝜑 → ( 𝐹 ∪ { 𝐴 } ) ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
39 38 unssad ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
40 23 subsubrg ⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) → ( 𝐹 ∈ ( SubRing ‘ ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ) ↔ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝐹 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ) )
41 40 biimpar ⊢ ( ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝐹 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ) → 𝐹 ∈ ( SubRing ‘ ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ) )
42 37 18 39 41 syl12anc ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ) )
43 19 22 23 37 42 lsssra ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( LSubSp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) )
44 1 fveq2i ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
45 9 44 eqtri ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
46 5 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝐸 ∈ Field )
47 6 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
48 31 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝐴 ∈ ( Base ‘ 𝐸 ) )
49 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑝 ∈ 𝑈 )
50 22 8 45 10 46 47 48 49 evls1fldgencl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
51 50 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑈 ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
52 11 rnmptss ⊢ ( ∀ 𝑝 ∈ 𝑈 ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) → ran 𝐺 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
53 51 52 syl ⊢ ( 𝜑 → ran 𝐺 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
54 8 45 22 10 29 18 31 11 19 evls1maplmhm ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 LMHom ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) )
55 eqid ⊢ ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
56 eqid ⊢ ( LSubSp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) = ( LSubSp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) )
57 55 56 reslmhm2b ⊢ ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LMod ∧ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( LSubSp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ ran 𝐺 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) → ( 𝐺 ∈ ( 𝑃 LMHom ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ↔ 𝐺 ∈ ( 𝑃 LMHom ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ) ) )
58 57 biimpa ⊢ ( ( ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ∈ LMod ∧ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( LSubSp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ∧ ran 𝐺 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ∧ 𝐺 ∈ ( 𝑃 LMHom ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) → 𝐺 ∈ ( 𝑃 LMHom ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ) )
59 21 43 53 54 58 syl31anc ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 LMHom ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ) )
60 22 24 33 fldgenssv ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ⊆ ( Base ‘ 𝐸 ) )
61 22 2 60 39 5 resssra ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) = ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) )
62 61 oveq2d ⊢ ( 𝜑 → ( 𝑃 LMHom ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) = ( 𝑃 LMHom ( ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ) )
63 59 62 eleqtrrd ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 LMHom ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )