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 ↾ 𝑠 F
algextdeg.l ⊢ L = E ↾ 𝑠 E fldGen F ∪ A
algextdeg.d ⊢ D = deg 1 ⁡ E
algextdeg.m ⊢ M = E minPoly F
algextdeg.f ⊢ φ → E ∈ Field
algextdeg.e ⊢ φ → F ∈ SubDRing ⁡ E
algextdeg.a ⊢ φ → A ∈ E IntgRing F
algextdeglem.o ⊢ O = E evalSub 1 F
algextdeglem.y ⊢ P = Poly 1 ⁡ K
algextdeglem.u ⊢ U = Base P
algextdeglem.g ⊢ G = p ∈ U ⟼ O ⁡ p ⁡ A
algextdeglem.n ⊢ N = x ∈ U ⟼ x P ~ QG Z
algextdeglem.z ⊢ Z = G -1 0 L
algextdeglem.q ⊢ Q = P / 𝑠 P ~ QG Z
algextdeglem.j ⊢ J = p ∈ Base Q ⟼ ⋃ G p
Assertion algextdeglem2 ⊢ φ → G ∈ P LMHom subringAlg ⁡ L ⁡ F

Proof

Step Hyp Ref Expression
1 algextdeg.k ⊢ K = E ↾ 𝑠 F
2 algextdeg.l ⊢ L = E ↾ 𝑠 E fldGen F ∪ A
3 algextdeg.d ⊢ D = deg 1 ⁡ E
4 algextdeg.m ⊢ M = E minPoly F
5 algextdeg.f ⊢ φ → E ∈ Field
6 algextdeg.e ⊢ φ → F ∈ SubDRing ⁡ E
7 algextdeg.a ⊢ φ → A ∈ E IntgRing F
8 algextdeglem.o ⊢ O = E evalSub 1 F
9 algextdeglem.y ⊢ P = Poly 1 ⁡ K
10 algextdeglem.u ⊢ U = Base P
11 algextdeglem.g ⊢ G = p ∈ U ⟼ O ⁡ p ⁡ A
12 algextdeglem.n ⊢ N = x ∈ U ⟼ x P ~ QG Z
13 algextdeglem.z ⊢ Z = G -1 0 L
14 algextdeglem.q ⊢ Q = P / 𝑠 P ~ QG Z
15 algextdeglem.j ⊢ J = p ∈ Base Q ⟼ ⋃ G p
16 issdrg ⊢ F ∈ SubDRing ⁡ E ↔ E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
17 6 16 sylib ⊢ φ → E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
18 17 simp2d ⊢ φ → F ∈ SubRing ⁡ E
19 eqid ⊢ subringAlg ⁡ E ⁡ F = subringAlg ⁡ E ⁡ F
20 19 sralmod ⊢ F ∈ SubRing ⁡ E → subringAlg ⁡ E ⁡ F ∈ LMod
21 18 20 syl ⊢ φ → subringAlg ⁡ E ⁡ F ∈ LMod
22 eqid ⊢ Base E = Base E
23 eqid ⊢ E ↾ 𝑠 E fldGen F ∪ A = E ↾ 𝑠 E fldGen F ∪ A
24 5 flddrngd ⊢ φ → E ∈ DivRing
25 subrgsubg ⊢ F ∈ SubRing ⁡ E → F ∈ SubGrp ⁡ E
26 22 subgss ⊢ F ∈ SubGrp ⁡ E → F ⊆ Base E
27 18 25 26 3syl ⊢ φ → F ⊆ Base E
28 eqid ⊢ 0 E = 0 E
29 5 fldcrngd ⊢ φ → E ∈ CRing
30 8 1 22 28 29 18 irngssv ⊢ φ → E IntgRing F ⊆ Base E
31 30 7 sseldd ⊢ φ → A ∈ Base E
32 31 snssd ⊢ φ → A ⊆ Base E
33 27 32 unssd ⊢ φ → F ∪ A ⊆ Base E
34 22 24 33 fldgensdrg ⊢ φ → E fldGen F ∪ A ∈ SubDRing ⁡ E
35 issdrg ⊢ E fldGen F ∪ A ∈ SubDRing ⁡ E ↔ E ∈ DivRing ∧ E fldGen F ∪ A ∈ SubRing ⁡ E ∧ E ↾ 𝑠 E fldGen F ∪ A ∈ DivRing
36 34 35 sylib ⊢ φ → E ∈ DivRing ∧ E fldGen F ∪ A ∈ SubRing ⁡ E ∧ E ↾ 𝑠 E fldGen F ∪ A ∈ DivRing
37 36 simp2d ⊢ φ → E fldGen F ∪ A ∈ SubRing ⁡ E
38 22 24 33 fldgenssid ⊢ φ → F ∪ A ⊆ E fldGen F ∪ A
39 38 unssad ⊢ φ → F ⊆ E fldGen F ∪ A
40 23 subsubrg ⊢ E fldGen F ∪ A ∈ SubRing ⁡ E → F ∈ SubRing ⁡ E ↾ 𝑠 E fldGen F ∪ A ↔ F ∈ SubRing ⁡ E ∧ F ⊆ E fldGen F ∪ A
41 40 biimpar ⊢ E fldGen F ∪ A ∈ SubRing ⁡ E ∧ F ∈ SubRing ⁡ E ∧ F ⊆ E fldGen F ∪ A → F ∈ SubRing ⁡ E ↾ 𝑠 E fldGen F ∪ A
42 37 18 39 41 syl12anc ⊢ φ → F ∈ SubRing ⁡ E ↾ 𝑠 E fldGen F ∪ A
43 19 22 23 37 42 lsssra ⊢ φ → E fldGen F ∪ A ∈ LSubSp ⁡ subringAlg ⁡ E ⁡ F
44 1 fveq2i ⊢ Poly 1 ⁡ K = Poly 1 ⁡ E ↾ 𝑠 F
45 9 44 eqtri ⊢ P = Poly 1 ⁡ E ↾ 𝑠 F
46 5 adantr ⊢ φ ∧ p ∈ U → E ∈ Field
47 6 adantr ⊢ φ ∧ p ∈ U → F ∈ SubDRing ⁡ E
48 31 adantr ⊢ φ ∧ p ∈ U → A ∈ Base E
49 simpr ⊢ φ ∧ p ∈ U → p ∈ U
50 22 8 45 10 46 47 48 49 evls1fldgencl ⊢ φ ∧ p ∈ U → O ⁡ p ⁡ A ∈ E fldGen F ∪ A
51 50 ralrimiva ⊢ φ → ∀ p ∈ U O ⁡ p ⁡ A ∈ E fldGen F ∪ A
52 11 rnmptss ⊢ ∀ p ∈ U O ⁡ p ⁡ A ∈ E fldGen F ∪ A → ran ⁡ G ⊆ E fldGen F ∪ A
53 51 52 syl ⊢ φ → ran ⁡ G ⊆ E fldGen F ∪ A
54 8 45 22 10 29 18 31 11 19 evls1maplmhm ⊢ φ → G ∈ P LMHom subringAlg ⁡ E ⁡ F
55 eqid ⊢ subringAlg ⁡ E ⁡ F ↾ 𝑠 E fldGen F ∪ A = subringAlg ⁡ E ⁡ F ↾ 𝑠 E fldGen F ∪ A
56 eqid ⊢ LSubSp ⁡ subringAlg ⁡ E ⁡ F = LSubSp ⁡ subringAlg ⁡ E ⁡ F
57 55 56 reslmhm2b ⊢ subringAlg ⁡ E ⁡ F ∈ LMod ∧ E fldGen F ∪ A ∈ LSubSp ⁡ subringAlg ⁡ E ⁡ F ∧ ran ⁡ G ⊆ E fldGen F ∪ A → G ∈ P LMHom subringAlg ⁡ E ⁡ F ↔ G ∈ P LMHom subringAlg ⁡ E ⁡ F ↾ 𝑠 E fldGen F ∪ A
58 57 biimpa ⊢ subringAlg ⁡ E ⁡ F ∈ LMod ∧ E fldGen F ∪ A ∈ LSubSp ⁡ subringAlg ⁡ E ⁡ F ∧ ran ⁡ G ⊆ E fldGen F ∪ A ∧ G ∈ P LMHom subringAlg ⁡ E ⁡ F → G ∈ P LMHom subringAlg ⁡ E ⁡ F ↾ 𝑠 E fldGen F ∪ A
59 21 43 53 54 58 syl31anc ⊢ φ → G ∈ P LMHom subringAlg ⁡ E ⁡ F ↾ 𝑠 E fldGen F ∪ A
60 22 24 33 fldgenssv ⊢ φ → E fldGen F ∪ A ⊆ Base E
61 22 2 60 39 5 resssra ⊢ φ → subringAlg ⁡ L ⁡ F = subringAlg ⁡ E ⁡ F ↾ 𝑠 E fldGen F ∪ A
62 61 oveq2d ⊢ φ → P LMHom subringAlg ⁡ L ⁡ F = P LMHom subringAlg ⁡ E ⁡ F ↾ 𝑠 E fldGen F ∪ A
63 59 62 eleqtrrd ⊢ φ → G ∈ P LMHom subringAlg ⁡ L ⁡ F