irredminply

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

	Ref	Expression
Hypotheses	irredminply.o	⊢ 𝑂 = ( 𝐸 evalSub₁ 𝐹 )
	irredminply.p	⊢ 𝑃 = ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) )
	irredminply.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
	irredminply.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
	irredminply.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	irredminply.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	irredminply.0	⊢ 0 = ( 0_g ‘ 𝐸 )
	irredminply.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
	irredminply.z	⊢ 𝑍 = ( 0_g ‘ 𝑃 )
	irredminply.1	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) = 0 )
	irredminply.2	⊢ ( 𝜑 → 𝐺 ∈ ( Irred ‘ 𝑃 ) )
	irredminply.3	⊢ ( 𝜑 → 𝐺 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) )
Assertion	irredminply	⊢ ( 𝜑 → 𝐺 = ( 𝑀 ‘ 𝐴 ) )

Proof

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

Metamath Proof Explorer

Theorem irredminply

Proof