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 
|- O = ( E evalSub1 F )
irredminply.p 
|- P = ( Poly1 ` ( E |`s F ) )
irredminply.b 
|- B = ( Base ` E )
irredminply.e 
|- ( ph -> E e. Field )
irredminply.f 
|- ( ph -> F e. ( SubDRing ` E ) )
irredminply.a 
|- ( ph -> A e. B )
irredminply.0 
|- .0. = ( 0g ` E )
irredminply.m 
|- M = ( E minPoly F )
irredminply.z 
|- Z = ( 0g ` P )
irredminply.1 
|- ( ph -> ( ( O ` G ) ` A ) = .0. )
irredminply.2 
|- ( ph -> G e. ( Irred ` P ) )
irredminply.3 
|- ( ph -> G e. ( Monic1p ` ( E |`s F ) ) )
Assertion irredminply 
|- ( ph -> G = ( M ` A ) )

Proof

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