Metamath Proof Explorer

Theorem minplyirredlem

Description: Lemma for minplyirred . (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses ply1annig1p.o ⊢ O = E evalSub 1 F
ply1annig1p.p ⊢ P = Poly 1 ⁡ E ↾ 𝑠 F
ply1annig1p.b ⊢ B = Base E
ply1annig1p.e ⊢ φ → E ∈ Field
ply1annig1p.f ⊢ φ → F ∈ SubDRing ⁡ E
ply1annig1p.a ⊢ φ → A ∈ B
minplyirred.1 ⊢ M = E minPoly F
minplyirred.2 ⊢ Z = 0 P
minplyirred.3 ⊢ φ → M ⁡ A ≠ Z
minplyirredlem.1 ⊢ φ → G ∈ Base P
minplyirredlem.2 ⊢ φ → H ∈ Base P
minplyirredlem.3 ⊢ φ → G ⋅ P H = M ⁡ A
minplyirredlem.4 ⊢ φ → O ⁡ G ⁡ A = 0 E
minplyirredlem.5 ⊢ φ → G ≠ Z
minplyirredlem.6 ⊢ φ → H ≠ Z
Assertion minplyirredlem ⊢ φ → H ∈ Unit ⁡ P

Proof

Step Hyp Ref Expression
1 ply1annig1p.o ⊢ O = E evalSub 1 F
2 ply1annig1p.p ⊢ P = Poly 1 ⁡ E ↾ 𝑠 F
3 ply1annig1p.b ⊢ B = Base E
4 ply1annig1p.e ⊢ φ → E ∈ Field
5 ply1annig1p.f ⊢ φ → F ∈ SubDRing ⁡ E
6 ply1annig1p.a ⊢ φ → A ∈ B
7 minplyirred.1 ⊢ M = E minPoly F
8 minplyirred.2 ⊢ Z = 0 P
9 minplyirred.3 ⊢ φ → M ⁡ A ≠ Z
10 minplyirredlem.1 ⊢ φ → G ∈ Base P
11 minplyirredlem.2 ⊢ φ → H ∈ Base P
12 minplyirredlem.3 ⊢ φ → G ⋅ P H = M ⁡ A
13 minplyirredlem.4 ⊢ φ → O ⁡ G ⁡ A = 0 E
14 minplyirredlem.5 ⊢ φ → G ≠ Z
15 minplyirredlem.6 ⊢ φ → H ≠ Z
16 eqid ⊢ E ↾ 𝑠 F = E ↾ 𝑠 F
17 16 sdrgdrng ⊢ F ∈ SubDRing ⁡ E → E ↾ 𝑠 F ∈ DivRing
18 5 17 syl ⊢ φ → E ↾ 𝑠 F ∈ DivRing
19 18 drngringd ⊢ φ → E ↾ 𝑠 F ∈ Ring
20 eqid ⊢ deg 1 ⁡ E ↾ 𝑠 F = deg 1 ⁡ E ↾ 𝑠 F
21 eqid ⊢ Base P = Base P
22 20 2 8 21 deg1nn0cl ⊢ E ↾ 𝑠 F ∈ Ring ∧ G ∈ Base P ∧ G ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ G ∈ ℕ 0
23 19 10 14 22 syl3anc ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ G ∈ ℕ 0
24 23 nn0red ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ G ∈ ℝ
25 20 2 8 21 deg1nn0cl ⊢ E ↾ 𝑠 F ∈ Ring ∧ H ∈ Base P ∧ H ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ H ∈ ℕ 0
26 19 11 15 25 syl3anc ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ H ∈ ℕ 0
27 26 nn0red ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ H ∈ ℝ
28 eqid ⊢ RLReg ⁡ E ↾ 𝑠 F = RLReg ⁡ E ↾ 𝑠 F
29 eqid ⊢ ⋅ P = ⋅ P
30 fldsdrgfld ⊢ E ∈ Field ∧ F ∈ SubDRing ⁡ E → E ↾ 𝑠 F ∈ Field
31 4 5 30 syl2anc ⊢ φ → E ↾ 𝑠 F ∈ Field
32 fldidom ⊢ E ↾ 𝑠 F ∈ Field → E ↾ 𝑠 F ∈ IDomn
33 31 32 syl ⊢ φ → E ↾ 𝑠 F ∈ IDomn
34 33 idomdomd ⊢ φ → E ↾ 𝑠 F ∈ Domn
35 eqid ⊢ coe 1 ⁡ G = coe 1 ⁡ G
36 20 2 8 21 28 35 deg1ldgdomn ⊢ E ↾ 𝑠 F ∈ Domn ∧ G ∈ Base P ∧ G ≠ Z → coe 1 ⁡ G ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ G ∈ RLReg ⁡ E ↾ 𝑠 F
37 34 10 14 36 syl3anc ⊢ φ → coe 1 ⁡ G ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ G ∈ RLReg ⁡ E ↾ 𝑠 F
38 20 2 28 21 29 8 19 10 14 37 11 15 deg1mul2 ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ G ⋅ P H = deg 1 ⁡ E ↾ 𝑠 F ⁡ G + deg 1 ⁡ E ↾ 𝑠 F ⁡ H
39 eqid ⊢ 0 E = 0 E
40 eqid ⊢ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E = q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E
41 eqid ⊢ RSpan ⁡ P = RSpan ⁡ P
42 eqid ⊢ idlGen 1p ⁡ E ↾ 𝑠 F = idlGen 1p ⁡ E ↾ 𝑠 F
43 1 2 3 4 5 6 39 40 41 42 7 minplyval ⊢ φ → M ⁡ A = idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E
44 12 43 eqtrd ⊢ φ → G ⋅ P H = idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E
45 44 fveq2d ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ G ⋅ P H = deg 1 ⁡ E ↾ 𝑠 F ⁡ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E
46 4 fldcrngd ⊢ φ → E ∈ CRing
47 sdrgsubrg ⊢ F ∈ SubDRing ⁡ E → F ∈ SubRing ⁡ E
48 5 47 syl ⊢ φ → F ∈ SubRing ⁡ E
49 1 2 3 46 48 6 39 40 ply1annidl ⊢ φ → q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E ∈ LIdeal ⁡ P
50 fveq2 ⊢ q = G → O ⁡ q = O ⁡ G
51 50 fveq1d ⊢ q = G → O ⁡ q ⁡ A = O ⁡ G ⁡ A
52 51 eqeq1d ⊢ q = G → O ⁡ q ⁡ A = 0 E ↔ O ⁡ G ⁡ A = 0 E
53 1 2 21 46 48 evls1dm ⊢ φ → dom ⁡ O = Base P
54 10 53 eleqtrrd ⊢ φ → G ∈ dom ⁡ O
55 52 54 13 elrabd ⊢ φ → G ∈ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E
56 2 42 21 18 49 20 8 55 14 ig1pmindeg ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 E ≤ deg 1 ⁡ E ↾ 𝑠 F ⁡ G
57 45 56 eqbrtrd ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ G ⋅ P H ≤ deg 1 ⁡ E ↾ 𝑠 F ⁡ G
58 38 57 eqbrtrrd ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ G + deg 1 ⁡ E ↾ 𝑠 F ⁡ H ≤ deg 1 ⁡ E ↾ 𝑠 F ⁡ G
59 leaddle0 ⊢ deg 1 ⁡ E ↾ 𝑠 F ⁡ G ∈ ℝ ∧ deg 1 ⁡ E ↾ 𝑠 F ⁡ H ∈ ℝ → deg 1 ⁡ E ↾ 𝑠 F ⁡ G + deg 1 ⁡ E ↾ 𝑠 F ⁡ H ≤ deg 1 ⁡ E ↾ 𝑠 F ⁡ G ↔ deg 1 ⁡ E ↾ 𝑠 F ⁡ H ≤ 0
60 59 biimpa ⊢ deg 1 ⁡ E ↾ 𝑠 F ⁡ G ∈ ℝ ∧ deg 1 ⁡ E ↾ 𝑠 F ⁡ H ∈ ℝ ∧ deg 1 ⁡ E ↾ 𝑠 F ⁡ G + deg 1 ⁡ E ↾ 𝑠 F ⁡ H ≤ deg 1 ⁡ E ↾ 𝑠 F ⁡ G → deg 1 ⁡ E ↾ 𝑠 F ⁡ H ≤ 0
61 24 27 58 60 syl21anc ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ H ≤ 0
62 eqid ⊢ algSc ⁡ P = algSc ⁡ P
63 20 2 21 62 deg1le0 ⊢ E ↾ 𝑠 F ∈ Ring ∧ H ∈ Base P → deg 1 ⁡ E ↾ 𝑠 F ⁡ H ≤ 0 ↔ H = algSc ⁡ P ⁡ coe 1 ⁡ H ⁡ 0
64 63 biimpa ⊢ E ↾ 𝑠 F ∈ Ring ∧ H ∈ Base P ∧ deg 1 ⁡ E ↾ 𝑠 F ⁡ H ≤ 0 → H = algSc ⁡ P ⁡ coe 1 ⁡ H ⁡ 0
65 19 11 61 64 syl21anc ⊢ φ → H = algSc ⁡ P ⁡ coe 1 ⁡ H ⁡ 0
66 eqid ⊢ Base E ↾ 𝑠 F = Base E ↾ 𝑠 F
67 eqid ⊢ 0 E ↾ 𝑠 F = 0 E ↾ 𝑠 F
68 0nn0 ⊢ 0 ∈ ℕ 0
69 eqid ⊢ coe 1 ⁡ H = coe 1 ⁡ H
70 69 21 2 66 coe1fvalcl ⊢ H ∈ Base P ∧ 0 ∈ ℕ 0 → coe 1 ⁡ H ⁡ 0 ∈ Base E ↾ 𝑠 F
71 11 68 70 sylancl ⊢ φ → coe 1 ⁡ H ⁡ 0 ∈ Base E ↾ 𝑠 F
72 20 2 67 21 8 19 11 61 deg1le0eq0 ⊢ φ → H = Z ↔ coe 1 ⁡ H ⁡ 0 = 0 E ↾ 𝑠 F
73 72 necon3bid ⊢ φ → H ≠ Z ↔ coe 1 ⁡ H ⁡ 0 ≠ 0 E ↾ 𝑠 F
74 15 73 mpbid ⊢ φ → coe 1 ⁡ H ⁡ 0 ≠ 0 E ↾ 𝑠 F
75 2 62 66 67 31 71 74 ply1asclunit ⊢ φ → algSc ⁡ P ⁡ coe 1 ⁡ H ⁡ 0 ∈ Unit ⁡ P
76 65 75 eqeltrd ⊢ φ → H ∈ Unit ⁡ P