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

Metamath Proof Explorer

Theorem minplyirred

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

Ref Expression
Hypotheses ply1annig1p.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
ply1annig1p.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
ply1annig1p.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
ply1annig1p.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
ply1annig1p.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
ply1annig1p.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
minplyirred.1 ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
minplyirred.2 ⊢ 𝑍 = ( 0g ‘ 𝑃 )
minplyirred.3 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ 𝑍 )
Assertion minplyirred ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Irred ‘ 𝑃 ) )

Proof

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