Metamath Proof Explorer

Theorem minplyirred

Description: A nonzero minimal polynomial is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses ply1annig1p.o 
|- O = ( E evalSub1 F )
ply1annig1p.p 
|- P = ( Poly1 ` ( E |`s F ) )
ply1annig1p.b 
|- B = ( Base ` E )
ply1annig1p.e 
|- ( ph -> E e. Field )
ply1annig1p.f 
|- ( ph -> F e. ( SubDRing ` E ) )
ply1annig1p.a 
|- ( ph -> A e. B )
minplyirred.1 
|- M = ( E minPoly F )
minplyirred.2 
|- Z = ( 0g ` P )
minplyirred.3 
|- ( ph -> ( M ` A ) =/= Z )
Assertion minplyirred 
|- ( ph -> ( M ` A ) e. ( Irred ` P ) )

Proof

Step Hyp Ref Expression
1 ply1annig1p.o 
 |-  O = ( E evalSub1 F )
2 ply1annig1p.p 
 |-  P = ( Poly1 ` ( E |`s F ) )
3 ply1annig1p.b 
 |-  B = ( Base ` E )
4 ply1annig1p.e 
 |-  ( ph -> E e. Field )
5 ply1annig1p.f 
 |-  ( ph -> F e. ( SubDRing ` E ) )
6 ply1annig1p.a 
 |-  ( ph -> A e. B )
7 minplyirred.1 
 |-  M = ( E minPoly F )
8 minplyirred.2 
 |-  Z = ( 0g ` P )
9 minplyirred.3 
 |-  ( ph -> ( M ` A ) =/= Z )
10 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
11 eqid 
 |-  { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } = { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) }
12 eqid 
 |-  ( RSpan ` P ) = ( RSpan ` P )
13 eqid 
 |-  ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) )
14 1 2 3 4 5 6 10 11 12 13 7 minplycl 
 |-  ( ph -> ( M ` A ) e. ( Base ` P ) )
15 1 2 3 4 5 6 10 11 12 13 7 minplyval 
 |-  ( ph -> ( M ` A ) = ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) )
16 eqid 
 |-  ( Base ` P ) = ( Base ` P )
17 eqid 
 |-  ( E |`s F ) = ( E |`s F )
18 17 sdrgdrng 
 |-  ( F e. ( SubDRing ` E ) -> ( E |`s F ) e. DivRing )
19 5 18 syl 
 |-  ( ph -> ( E |`s F ) e. DivRing )
20 4 fldcrngd 
 |-  ( ph -> E e. CRing )
21 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
22 5 21 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
23 1 2 3 20 22 6 10 11 ply1annidl 
 |-  ( ph -> { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } e. ( LIdeal ` P ) )
24 4 flddrngd 
 |-  ( ph -> E e. DivRing )
25 drngnzr 
 |-  ( E e. DivRing -> E e. NzRing )
26 24 25 syl 
 |-  ( ph -> E e. NzRing )
27 1 2 3 20 22 6 10 11 16 26 ply1annnr 
 |-  ( ph -> { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } =/= ( Base ` P ) )
28 2 13 16 19 23 27 ig1pnunit 
 |-  ( ph -> -. ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) e. ( Unit ` P ) )
29 15 28 eqneltrd 
 |-  ( ph -> -. ( M ` A ) e. ( Unit ` P ) )
30 fldidom 
 |-  ( E e. Field -> E e. IDomn )
31 4 30 syl 
 |-  ( ph -> E e. IDomn )
32 31 idomdomd 
 |-  ( ph -> E e. Domn )
33 32 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> E e. Domn )
34 20 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> E e. CRing )
35 22 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> F e. ( SubRing ` E ) )
36 6 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> A e. B )
37 simpllr 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> f e. ( Base ` P ) )
38 1 2 3 16 34 35 36 37 evls1fvcl 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( ( O ` f ) ` A ) e. B )
39 simplr 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> g e. ( Base ` P ) )
40 1 2 3 16 34 35 36 39 evls1fvcl 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( ( O ` g ) ` A ) e. B )
41 simpr 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( f ( .r ` P ) g ) = ( M ` A ) )
42 41 fveq2d 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( O ` ( f ( .r ` P ) g ) ) = ( O ` ( M ` A ) ) )
43 42 fveq1d 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( ( O ` ( f ( .r ` P ) g ) ) ` A ) = ( ( O ` ( M ` A ) ) ` A ) )
44 eqid 
 |-  ( .r ` P ) = ( .r ` P )
45 eqid 
 |-  ( .r ` E ) = ( .r ` E )
46 1 3 2 17 16 44 45 34 35 37 39 36 evls1muld 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( ( O ` ( f ( .r ` P ) g ) ) ` A ) = ( ( ( O ` f ) ` A ) ( .r ` E ) ( ( O ` g ) ` A ) ) )
47 eqid 
 |-  ( LIdeal ` P ) = ( LIdeal ` P )
48 2 13 47 ig1pcl 
 |-  ( ( ( E |`s F ) e. DivRing /\ { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } e. ( LIdeal ` P ) ) -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) e. { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } )
49 19 23 48 syl2anc 
 |-  ( ph -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } ) e. { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } )
50 15 49 eqeltrd 
 |-  ( ph -> ( M ` A ) e. { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } )
51 fveq2 
 |-  ( q = ( M ` A ) -> ( O ` q ) = ( O ` ( M ` A ) ) )
52 51 fveq1d 
 |-  ( q = ( M ` A ) -> ( ( O ` q ) ` A ) = ( ( O ` ( M ` A ) ) ` A ) )
53 52 eqeq1d 
 |-  ( q = ( M ` A ) -> ( ( ( O ` q ) ` A ) = ( 0g ` E ) <-> ( ( O ` ( M ` A ) ) ` A ) = ( 0g ` E ) ) )
54 53 elrab 
 |-  ( ( M ` A ) e. { q e. dom O | ( ( O ` q ) ` A ) = ( 0g ` E ) } <-> ( ( M ` A ) e. dom O /\ ( ( O ` ( M ` A ) ) ` A ) = ( 0g ` E ) ) )
55 50 54 sylib 
 |-  ( ph -> ( ( M ` A ) e. dom O /\ ( ( O ` ( M ` A ) ) ` A ) = ( 0g ` E ) ) )
56 55 simprd 
 |-  ( ph -> ( ( O ` ( M ` A ) ) ` A ) = ( 0g ` E ) )
57 56 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( ( O ` ( M ` A ) ) ` A ) = ( 0g ` E ) )
58 43 46 57 3eqtr3d 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( ( ( O ` f ) ` A ) ( .r ` E ) ( ( O ` g ) ` A ) ) = ( 0g ` E ) )
59 3 45 10 domneq0 
 |-  ( ( E e. Domn /\ ( ( O ` f ) ` A ) e. B /\ ( ( O ` g ) ` A ) e. B ) -> ( ( ( ( O ` f ) ` A ) ( .r ` E ) ( ( O ` g ) ` A ) ) = ( 0g ` E ) <-> ( ( ( O ` f ) ` A ) = ( 0g ` E ) \/ ( ( O ` g ) ` A ) = ( 0g ` E ) ) ) )
60 59 biimpa 
 |-  ( ( ( E e. Domn /\ ( ( O ` f ) ` A ) e. B /\ ( ( O ` g ) ` A ) e. B ) /\ ( ( ( O ` f ) ` A ) ( .r ` E ) ( ( O ` g ) ` A ) ) = ( 0g ` E ) ) -> ( ( ( O ` f ) ` A ) = ( 0g ` E ) \/ ( ( O ` g ) ` A ) = ( 0g ` E ) ) )
61 33 38 40 58 60 syl31anc 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( ( ( O ` f ) ` A ) = ( 0g ` E ) \/ ( ( O ` g ) ` A ) = ( 0g ` E ) ) )
62 4 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` f ) ` A ) = ( 0g ` E ) ) -> E e. Field )
63 5 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` f ) ` A ) = ( 0g ` E ) ) -> F e. ( SubDRing ` E ) )
64 36 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` f ) ` A ) = ( 0g ` E ) ) -> A e. B )
65 9 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( M ` A ) =/= Z )
66 65 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` f ) ` A ) = ( 0g ` E ) ) -> ( M ` A ) =/= Z )
67 37 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` f ) ` A ) = ( 0g ` E ) ) -> f e. ( Base ` P ) )
68 simpllr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` f ) ` A ) = ( 0g ` E ) ) -> g e. ( Base ` P ) )
69 simplr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` f ) ` A ) = ( 0g ` E ) ) -> ( f ( .r ` P ) g ) = ( M ` A ) )
70 simpr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` f ) ` A ) = ( 0g ` E ) ) -> ( ( O ` f ) ` A ) = ( 0g ` E ) )
71 fldsdrgfld 
 |-  ( ( E e. Field /\ F e. ( SubDRing ` E ) ) -> ( E |`s F ) e. Field )
72 4 5 71 syl2anc 
 |-  ( ph -> ( E |`s F ) e. Field )
73 fldidom 
 |-  ( ( E |`s F ) e. Field -> ( E |`s F ) e. IDomn )
74 72 73 syl 
 |-  ( ph -> ( E |`s F ) e. IDomn )
75 74 idomdomd 
 |-  ( ph -> ( E |`s F ) e. Domn )
76 2 ply1domn 
 |-  ( ( E |`s F ) e. Domn -> P e. Domn )
77 75 76 syl 
 |-  ( ph -> P e. Domn )
78 77 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> P e. Domn )
79 41 65 eqnetrd 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( f ( .r ` P ) g ) =/= Z )
80 16 44 8 domneq0 
 |-  ( ( P e. Domn /\ f e. ( Base ` P ) /\ g e. ( Base ` P ) ) -> ( ( f ( .r ` P ) g ) = Z <-> ( f = Z \/ g = Z ) ) )
81 80 necon3abid 
 |-  ( ( P e. Domn /\ f e. ( Base ` P ) /\ g e. ( Base ` P ) ) -> ( ( f ( .r ` P ) g ) =/= Z <-> -. ( f = Z \/ g = Z ) ) )
82 81 biimpa 
 |-  ( ( ( P e. Domn /\ f e. ( Base ` P ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) =/= Z ) -> -. ( f = Z \/ g = Z ) )
83 78 37 39 79 82 syl31anc 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> -. ( f = Z \/ g = Z ) )
84 neanior 
 |-  ( ( f =/= Z /\ g =/= Z ) <-> -. ( f = Z \/ g = Z ) )
85 83 84 sylibr 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( f =/= Z /\ g =/= Z ) )
86 85 simpld 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> f =/= Z )
87 86 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` f ) ` A ) = ( 0g ` E ) ) -> f =/= Z )
88 85 simprd 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> g =/= Z )
89 88 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` f ) ` A ) = ( 0g ` E ) ) -> g =/= Z )
90 1 2 3 62 63 64 7 8 66 67 68 69 70 87 89 minplyirredlem 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` f ) ` A ) = ( 0g ` E ) ) -> g e. ( Unit ` P ) )
91 90 ex 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( ( ( O ` f ) ` A ) = ( 0g ` E ) -> g e. ( Unit ` P ) ) )
92 4 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> E e. Field )
93 5 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> F e. ( SubDRing ` E ) )
94 36 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> A e. B )
95 65 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> ( M ` A ) =/= Z )
96 simpllr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> g e. ( Base ` P ) )
97 37 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> f e. ( Base ` P ) )
98 72 fldcrngd 
 |-  ( ph -> ( E |`s F ) e. CRing )
99 2 ply1crng 
 |-  ( ( E |`s F ) e. CRing -> P e. CRing )
100 98 99 syl 
 |-  ( ph -> P e. CRing )
101 100 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> P e. CRing )
102 16 44 crngcom 
 |-  ( ( P e. CRing /\ g e. ( Base ` P ) /\ f e. ( Base ` P ) ) -> ( g ( .r ` P ) f ) = ( f ( .r ` P ) g ) )
103 101 96 97 102 syl3anc 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> ( g ( .r ` P ) f ) = ( f ( .r ` P ) g ) )
104 simplr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> ( f ( .r ` P ) g ) = ( M ` A ) )
105 103 104 eqtrd 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> ( g ( .r ` P ) f ) = ( M ` A ) )
106 simpr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> ( ( O ` g ) ` A ) = ( 0g ` E ) )
107 88 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> g =/= Z )
108 86 adantr 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> f =/= Z )
109 1 2 3 92 93 94 7 8 95 96 97 105 106 107 108 minplyirredlem 
 |-  ( ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) /\ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> f e. ( Unit ` P ) )
110 109 ex 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( ( ( O ` g ) ` A ) = ( 0g ` E ) -> f e. ( Unit ` P ) ) )
111 91 110 orim12d 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( ( ( ( O ` f ) ` A ) = ( 0g ` E ) \/ ( ( O ` g ) ` A ) = ( 0g ` E ) ) -> ( g e. ( Unit ` P ) \/ f e. ( Unit ` P ) ) ) )
112 61 111 mpd 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( g e. ( Unit ` P ) \/ f e. ( Unit ` P ) ) )
113 112 orcomd 
 |-  ( ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) /\ ( f ( .r ` P ) g ) = ( M ` A ) ) -> ( f e. ( Unit ` P ) \/ g e. ( Unit ` P ) ) )
114 113 ex 
 |-  ( ( ( ph /\ f e. ( Base ` P ) ) /\ g e. ( Base ` P ) ) -> ( ( f ( .r ` P ) g ) = ( M ` A ) -> ( f e. ( Unit ` P ) \/ g e. ( Unit ` P ) ) ) )
115 114 anasss 
 |-  ( ( ph /\ ( f e. ( Base ` P ) /\ g e. ( Base ` P ) ) ) -> ( ( f ( .r ` P ) g ) = ( M ` A ) -> ( f e. ( Unit ` P ) \/ g e. ( Unit ` P ) ) ) )
116 115 ralrimivva 
 |-  ( ph -> A. f e. ( Base ` P ) A. g e. ( Base ` P ) ( ( f ( .r ` P ) g ) = ( M ` A ) -> ( f e. ( Unit ` P ) \/ g e. ( Unit ` P ) ) ) )
117 eqid 
 |-  ( Unit ` P ) = ( Unit ` P )
118 eqid 
 |-  ( Irred ` P ) = ( Irred ` P )
119 16 117 118 44 isirred2 
 |-  ( ( M ` A ) e. ( Irred ` P ) <-> ( ( M ` A ) e. ( Base ` P ) /\ -. ( M ` A ) e. ( Unit ` P ) /\ A. f e. ( Base ` P ) A. g e. ( Base ` P ) ( ( f ( .r ` P ) g ) = ( M ` A ) -> ( f e. ( Unit ` P ) \/ g e. ( Unit ` P ) ) ) ) )
120 14 29 116 119 syl3anbrc 
 |-  ( ph -> ( M ` A ) e. ( Irred ` P ) )