Metamath Proof Explorer

Theorem irredminply

Description: An irreducible, monic, annihilating polynomial isthe minimal polynomial. (Contributed by Thierry Arnoux, 27-Apr-2025)

Ref Expression
Hypotheses irredminply.o ⊢ O = E evalSub 1 F
irredminply.p ⊢ P = Poly 1 ⁡ E ↾ 𝑠 F
irredminply.b ⊢ B = Base E
irredminply.e ⊢ φ → E ∈ Field
irredminply.f ⊢ φ → F ∈ SubDRing ⁡ E
irredminply.a ⊢ φ → A ∈ B
irredminply.0 ⊢ 0 ˙ = 0 E
irredminply.m ⊢ M = E minPoly F
irredminply.z ⊢ Z = 0 P
irredminply.1 ⊢ φ → O ⁡ G ⁡ A = 0 ˙
irredminply.2 ⊢ φ → G ∈ Irred ⁡ P
irredminply.3 ⊢ φ → G ∈ Monic 1p ⁡ E ↾ 𝑠 F
Assertion irredminply ⊢ φ → G = M ⁡ A

Proof

Step Hyp Ref Expression
1 irredminply.o ⊢ O = E evalSub 1 F
2 irredminply.p ⊢ P = Poly 1 ⁡ E ↾ 𝑠 F
3 irredminply.b ⊢ B = Base E
4 irredminply.e ⊢ φ → E ∈ Field
5 irredminply.f ⊢ φ → F ∈ SubDRing ⁡ E
6 irredminply.a ⊢ φ → A ∈ B
7 irredminply.0 ⊢ 0 ˙ = 0 E
8 irredminply.m ⊢ M = E minPoly F
9 irredminply.z ⊢ Z = 0 P
10 irredminply.1 ⊢ φ → O ⁡ G ⁡ A = 0 ˙
11 irredminply.2 ⊢ φ → G ∈ Irred ⁡ P
12 irredminply.3 ⊢ φ → G ∈ Monic 1p ⁡ E ↾ 𝑠 F
13 eqid ⊢ Monic 1p ⁡ E ↾ 𝑠 F = Monic 1p ⁡ E ↾ 𝑠 F
14 eqid ⊢ Unit ⁡ P = Unit ⁡ P
15 eqid ⊢ ⋅ P = ⋅ P
16 fldsdrgfld ⊢ E ∈ Field ∧ F ∈ SubDRing ⁡ E → E ↾ 𝑠 F ∈ Field
17 4 5 16 syl2anc ⊢ φ → E ↾ 𝑠 F ∈ Field
18 eqid ⊢ 0 Poly 1 ⁡ E = 0 Poly 1 ⁡ E
19 fveq2 ⊢ g = G → O ⁡ g = O ⁡ G
20 19 fveq1d ⊢ g = G → O ⁡ g ⁡ A = O ⁡ G ⁡ A
21 20 eqeq1d ⊢ g = G → O ⁡ g ⁡ A = 0 ˙ ↔ O ⁡ G ⁡ A = 0 ˙
22 21 12 10 rspcedvdw ⊢ φ → ∃ g ∈ Monic 1p ⁡ E ↾ 𝑠 F O ⁡ g ⁡ A = 0 ˙
23 eqid ⊢ E ↾ 𝑠 F = E ↾ 𝑠 F
24 4 fldcrngd ⊢ φ → E ∈ CRing
25 sdrgsubrg ⊢ F ∈ SubDRing ⁡ E → F ∈ SubRing ⁡ E
26 5 25 syl ⊢ φ → F ∈ SubRing ⁡ E
27 1 23 3 7 24 26 elirng ⊢ φ → A ∈ E IntgRing F ↔ A ∈ B ∧ ∃ g ∈ Monic 1p ⁡ E ↾ 𝑠 F O ⁡ g ⁡ A = 0 ˙
28 6 22 27 mpbir2and ⊢ φ → A ∈ E IntgRing F
29 18 4 5 8 28 13 minplym1p ⊢ φ → M ⁡ A ∈ Monic 1p ⁡ E ↾ 𝑠 F
30 23 sdrgdrng ⊢ F ∈ SubDRing ⁡ E → E ↾ 𝑠 F ∈ DivRing
31 5 30 syl ⊢ φ → E ↾ 𝑠 F ∈ DivRing
32 31 drngringd ⊢ φ → E ↾ 𝑠 F ∈ Ring
33 eqid ⊢ Irred ⁡ P = Irred ⁡ P
34 eqid ⊢ Base P = Base P
35 33 34 irredcl ⊢ G ∈ Irred ⁡ P → G ∈ Base P
36 11 35 syl ⊢ φ → G ∈ Base P
37 2 34 13 mon1pcl ⊢ M ⁡ A ∈ Monic 1p ⁡ E ↾ 𝑠 F → M ⁡ A ∈ Base P
38 29 37 syl ⊢ φ → M ⁡ A ∈ Base P
39 18 4 5 8 28 irngnminplynz ⊢ φ → M ⁡ A ≠ 0 Poly 1 ⁡ E
40 eqid ⊢ Poly 1 ⁡ E = Poly 1 ⁡ E
41 40 23 2 34 26 18 ressply10g ⊢ φ → 0 Poly 1 ⁡ E = 0 P
42 9 41 eqtr4id ⊢ φ → Z = 0 Poly 1 ⁡ E
43 39 42 neeqtrrd ⊢ φ → M ⁡ A ≠ Z
44 eqid ⊢ Unic 1p ⁡ E ↾ 𝑠 F = Unic 1p ⁡ E ↾ 𝑠 F
45 2 34 9 44 drnguc1p ⊢ E ↾ 𝑠 F ∈ DivRing ∧ M ⁡ A ∈ Base P ∧ M ⁡ A ≠ Z → M ⁡ A ∈ Unic 1p ⁡ E ↾ 𝑠 F
46 31 38 43 45 syl3anc ⊢ φ → M ⁡ A ∈ Unic 1p ⁡ E ↾ 𝑠 F
47 eqidd ⊢ φ → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A = G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A
48 eqid ⊢ quot 1p ⁡ E ↾ 𝑠 F = quot 1p ⁡ E ↾ 𝑠 F
49 eqid ⊢ deg 1 ⁡ E ↾ 𝑠 F = deg 1 ⁡ E ↾ 𝑠 F
50 eqid ⊢ - P = - P
51 48 2 34 49 50 15 44 q1peqb ⊢ E ↾ 𝑠 F ∈ Ring ∧ G ∈ Base P ∧ M ⁡ A ∈ Unic 1p ⁡ E ↾ 𝑠 F → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Base P ∧ deg 1 ⁡ E ↾ 𝑠 F ⁡ G - P G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A < deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A ↔ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A = G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A
52 51 biimpar ⊢ E ↾ 𝑠 F ∈ Ring ∧ G ∈ Base P ∧ M ⁡ A ∈ Unic 1p ⁡ E ↾ 𝑠 F ∧ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A = G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Base P ∧ deg 1 ⁡ E ↾ 𝑠 F ⁡ G - P G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A < deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A
53 32 36 46 47 52 syl31anc ⊢ φ → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Base P ∧ deg 1 ⁡ E ↾ 𝑠 F ⁡ G - P G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A < deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A
54 53 simpld ⊢ φ → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Base P
55 eqid ⊢ rem 1p ⁡ E ↾ 𝑠 F = rem 1p ⁡ E ↾ 𝑠 F
56 eqid ⊢ + P = + P
57 2 34 44 48 55 15 56 r1pid ⊢ E ↾ 𝑠 F ∈ Ring ∧ G ∈ Base P ∧ M ⁡ A ∈ Unic 1p ⁡ E ↾ 𝑠 F → G = G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A + P G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A
58 32 36 46 57 syl3anc ⊢ φ → G = G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A + P G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A
59 55 2 34 44 49 r1pdeglt ⊢ E ↾ 𝑠 F ∈ Ring ∧ G ∈ Base P ∧ M ⁡ A ∈ Unic 1p ⁡ E ↾ 𝑠 F → deg 1 ⁡ E ↾ 𝑠 F ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A < deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A
60 32 36 46 59 syl3anc ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A < deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A
61 60 adantr ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A < deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A
62 32 adantr ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → E ↾ 𝑠 F ∈ Ring
63 38 adantr ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → M ⁡ A ∈ Base P
64 43 adantr ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → M ⁡ A ≠ Z
65 49 2 9 34 deg1nn0cl ⊢ E ↾ 𝑠 F ∈ Ring ∧ M ⁡ A ∈ Base P ∧ M ⁡ A ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A ∈ ℕ 0
66 62 63 64 65 syl3anc ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A ∈ ℕ 0
67 66 nn0red ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A ∈ ℝ
68 55 2 34 44 r1pcl ⊢ E ↾ 𝑠 F ∈ Ring ∧ G ∈ Base P ∧ M ⁡ A ∈ Unic 1p ⁡ E ↾ 𝑠 F → G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Base P
69 32 36 46 68 syl3anc ⊢ φ → G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Base P
70 69 adantr ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Base P
71 simpr ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z
72 49 2 9 34 deg1nn0cl ⊢ E ↾ 𝑠 F ∈ Ring ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Base P ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ ℕ 0
73 62 70 71 72 syl3anc ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ ℕ 0
74 73 nn0red ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ ℝ
75 eqid ⊢ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙ = q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
76 eqid ⊢ RSpan ⁡ P = RSpan ⁡ P
77 eqid ⊢ idlGen 1p ⁡ E ↾ 𝑠 F = idlGen 1p ⁡ E ↾ 𝑠 F
78 1 2 3 4 5 6 7 75 76 77 8 minplyval ⊢ φ → M ⁡ A = idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
79 78 fveq2d ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A = deg 1 ⁡ E ↾ 𝑠 F ⁡ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
80 79 adantr ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A = deg 1 ⁡ E ↾ 𝑠 F ⁡ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
81 5 adantr ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → F ∈ SubDRing ⁡ E
82 81 30 syl ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → E ↾ 𝑠 F ∈ DivRing
83 1 2 3 24 26 6 7 75 ply1annidl ⊢ φ → q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙ ∈ LIdeal ⁡ P
84 83 adantr ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙ ∈ LIdeal ⁡ P
85 fveq2 ⊢ q = G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A → O ⁡ q = O ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A
86 85 fveq1d ⊢ q = G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A → O ⁡ q ⁡ A = O ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ⁡ A
87 86 eqeq1d ⊢ q = G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A → O ⁡ q ⁡ A = 0 ˙ ↔ O ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ⁡ A = 0 ˙
88 1 2 34 24 26 evls1dm ⊢ φ → dom ⁡ O = Base P
89 69 88 eleqtrrd ⊢ φ → G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ dom ⁡ O
90 55 2 34 48 15 50 r1pval ⊢ G ∈ Base P ∧ M ⁡ A ∈ Base P → G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A = G - P G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A
91 36 38 90 syl2anc ⊢ φ → G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A = G - P G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A
92 91 fveq2d ⊢ φ → O ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A = O ⁡ G - P G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A
93 92 fveq1d ⊢ φ → O ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ⁡ A = O ⁡ G - P G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ⁡ A
94 eqid ⊢ - E = - E
95 2 ply1ring ⊢ E ↾ 𝑠 F ∈ Ring → P ∈ Ring
96 32 95 syl ⊢ φ → P ∈ Ring
97 34 15 96 54 38 ringcld ⊢ φ → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ∈ Base P
98 1 3 2 23 34 50 94 24 26 36 97 6 evls1subd ⊢ φ → O ⁡ G - P G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ⁡ A = O ⁡ G ⁡ A - E O ⁡ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ⁡ A
99 eqid ⊢ ⋅ E = ⋅ E
100 1 3 2 23 34 15 99 24 26 54 38 6 evls1muld ⊢ φ → O ⁡ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ⁡ A = O ⁡ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⁡ A ⋅ E O ⁡ M ⁡ A ⁡ A
101 1 2 3 4 5 6 7 8 minplyann ⊢ φ → O ⁡ M ⁡ A ⁡ A = 0 ˙
102 101 oveq2d ⊢ φ → O ⁡ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⁡ A ⋅ E O ⁡ M ⁡ A ⁡ A = O ⁡ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⁡ A ⋅ E 0 ˙
103 24 crngringd ⊢ φ → E ∈ Ring
104 1 2 3 34 24 26 6 54 evls1fvcl ⊢ φ → O ⁡ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⁡ A ∈ B
105 3 99 7 103 104 ringrzd ⊢ φ → O ⁡ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⁡ A ⋅ E 0 ˙ = 0 ˙
106 100 102 105 3eqtrd ⊢ φ → O ⁡ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ⁡ A = 0 ˙
107 10 106 oveq12d ⊢ φ → O ⁡ G ⁡ A - E O ⁡ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ⁡ A = 0 ˙ - E 0 ˙
108 24 crnggrpd ⊢ φ → E ∈ Grp
109 3 7 grpidcl ⊢ E ∈ Grp → 0 ˙ ∈ B
110 3 7 94 grpsubid1 ⊢ E ∈ Grp ∧ 0 ˙ ∈ B → 0 ˙ - E 0 ˙ = 0 ˙
111 108 109 110 syl2anc2 ⊢ φ → 0 ˙ - E 0 ˙ = 0 ˙
112 98 107 111 3eqtrd ⊢ φ → O ⁡ G - P G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ⁡ A = 0 ˙
113 93 112 eqtrd ⊢ φ → O ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ⁡ A = 0 ˙
114 87 89 113 elrabd ⊢ φ → G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
115 114 adantr ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
116 2 77 34 82 84 49 9 115 71 ig1pmindeg ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙ ≤ deg 1 ⁡ E ↾ 𝑠 F ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A
117 80 116 eqbrtrd ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A ≤ deg 1 ⁡ E ↾ 𝑠 F ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A
118 67 74 117 lensymd ⊢ φ ∧ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z → ¬ deg 1 ⁡ E ↾ 𝑠 F ⁡ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A < deg 1 ⁡ E ↾ 𝑠 F ⁡ M ⁡ A
119 61 118 pm2.65da ⊢ φ → ¬ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z
120 nne ⊢ ¬ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A ≠ Z ↔ G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A = Z
121 119 120 sylib ⊢ φ → G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A = Z
122 121 oveq2d ⊢ φ → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A + P G rem 1p ⁡ E ↾ 𝑠 F M ⁡ A = G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A + P Z
123 96 ringgrpd ⊢ φ → P ∈ Grp
124 34 56 9 123 97 grpridd ⊢ φ → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A + P Z = G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A
125 58 122 124 3eqtrd ⊢ φ → G = G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A
126 125 11 eqeltrrd ⊢ φ → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ∈ Irred ⁡ P
127 1 2 3 4 5 6 8 9 43 minplyirred ⊢ φ → M ⁡ A ∈ Irred ⁡ P
128 33 14 irrednu ⊢ M ⁡ A ∈ Irred ⁡ P → ¬ M ⁡ A ∈ Unit ⁡ P
129 127 128 syl ⊢ φ → ¬ M ⁡ A ∈ Unit ⁡ P
130 33 34 14 15 irredmul ⊢ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Base P ∧ M ⁡ A ∈ Base P ∧ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ∈ Irred ⁡ P → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Unit ⁡ P ∨ M ⁡ A ∈ Unit ⁡ P
131 130 orcomd ⊢ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Base P ∧ M ⁡ A ∈ Base P ∧ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ∈ Irred ⁡ P → M ⁡ A ∈ Unit ⁡ P ∨ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Unit ⁡ P
132 131 orcanai ⊢ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Base P ∧ M ⁡ A ∈ Base P ∧ G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ⋅ P M ⁡ A ∈ Irred ⁡ P ∧ ¬ M ⁡ A ∈ Unit ⁡ P → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Unit ⁡ P
133 54 38 126 129 132 syl31anc ⊢ φ → G quot 1p ⁡ E ↾ 𝑠 F M ⁡ A ∈ Unit ⁡ P
134 2 13 14 15 17 12 29 133 125 m1pmeq ⊢ φ → G = M ⁡ A