This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
irredminply.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
irredminply.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
irredminply.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
irredminply.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
irredminply.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
irredminply.0 ⊢ 0 = ( 0g ‘ 𝐸 )
irredminply.m ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
irredminply.z ⊢ 𝑍 = ( 0g ‘ 𝑃 )
irredminply.1 ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) = 0 )
irredminply.2 ⊢ ( 𝜑 → 𝐺 ∈ ( Irred ‘ 𝑃 ) )
irredminply.3 ⊢ ( 𝜑 → 𝐺 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) )
Assertion irredminply ( 𝜑 → 𝐺 = ( 𝑀 ‘ 𝐴 ) )

Proof

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