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 ↾ 𝑠 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 algextdeglem5 ⊢ φ → Z = RSpan ⁡ P ⁡ M ⁡ A

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 1 fveq2i ⊢ Poly 1 ⁡ K = Poly 1 ⁡ E ↾ 𝑠 F
17 9 16 eqtri ⊢ P = Poly 1 ⁡ E ↾ 𝑠 F
18 eqid ⊢ Base E = Base E
19 eqid ⊢ 0 E = 0 E
20 5 fldcrngd ⊢ φ → E ∈ CRing
21 issdrg ⊢ F ∈ SubDRing ⁡ E ↔ E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
22 6 21 sylib ⊢ φ → E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
23 22 simp2d ⊢ φ → F ∈ SubRing ⁡ E
24 8 1 18 19 20 23 irngssv ⊢ φ → E IntgRing F ⊆ Base E
25 24 7 sseldd ⊢ φ → A ∈ Base E
26 eqid ⊢ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E = q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E
27 eqid ⊢ RSpan ⁡ P = RSpan ⁡ P
28 eqid ⊢ idlGen 1p ⁡ E ↾ 𝑠 F = idlGen 1p ⁡ E ↾ 𝑠 F
29 8 17 18 5 6 25 19 26 27 28 ply1annig1p ⊢ φ → q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E = RSpan ⁡ P ⁡ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E
30 20 crnggrpd ⊢ φ → E ∈ Grp
31 30 grpmndd ⊢ φ → E ∈ Mnd
32 5 flddrngd ⊢ φ → E ∈ DivRing
33 subrgsubg ⊢ F ∈ SubRing ⁡ E → F ∈ SubGrp ⁡ E
34 18 subgss ⊢ F ∈ SubGrp ⁡ E → F ⊆ Base E
35 23 33 34 3syl ⊢ φ → F ⊆ Base E
36 25 snssd ⊢ φ → A ⊆ Base E
37 35 36 unssd ⊢ φ → F ∪ A ⊆ Base E
38 18 32 37 fldgensdrg ⊢ φ → E fldGen F ∪ A ∈ SubDRing ⁡ E
39 sdrgsubrg ⊢ E fldGen F ∪ A ∈ SubDRing ⁡ E → E fldGen F ∪ A ∈ SubRing ⁡ E
40 subrgsubg ⊢ E fldGen F ∪ A ∈ SubRing ⁡ E → E fldGen F ∪ A ∈ SubGrp ⁡ E
41 19 subg0cl ⊢ E fldGen F ∪ A ∈ SubGrp ⁡ E → 0 E ∈ E fldGen F ∪ A
42 38 39 40 41 4syl ⊢ φ → 0 E ∈ E fldGen F ∪ A
43 18 32 37 fldgenssv ⊢ φ → E fldGen F ∪ A ⊆ Base E
44 2 18 19 ress0g ⊢ E ∈ Mnd ∧ 0 E ∈ E fldGen F ∪ A ∧ E fldGen F ∪ A ⊆ Base E → 0 E = 0 L
45 31 42 43 44 syl3anc ⊢ φ → 0 E = 0 L
46 45 sneqd ⊢ φ → 0 E = 0 L
47 46 imaeq2d ⊢ φ → G -1 0 E = G -1 0 L
48 13 47 eqtr4id ⊢ φ → Z = G -1 0 E
49 10 mpteq1i ⊢ p ∈ U ⟼ O ⁡ p ⁡ A = p ∈ Base P ⟼ O ⁡ p ⁡ A
50 11 49 eqtri ⊢ G = p ∈ Base P ⟼ O ⁡ p ⁡ A
51 8 17 18 20 23 25 19 26 50 ply1annidllem ⊢ φ → q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E = G -1 0 E
52 48 51 eqtr4d ⊢ φ → Z = q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E
53 8 17 18 5 6 25 19 26 27 28 4 minplyval ⊢ φ → M ⁡ A = idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E
54 53 sneqd ⊢ φ → M ⁡ A = idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E
55 54 fveq2d ⊢ φ → RSpan ⁡ P ⁡ M ⁡ A = RSpan ⁡ P ⁡ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E
56 29 52 55 3eqtr4d ⊢ φ → Z = RSpan ⁡ P ⁡ M ⁡ A