minplyirred

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

	Ref	Expression
Hypotheses	ply1annig1p.o	$⊢ O = E {evalSub}_{1} F$
	ply1annig1p.p	$⊢ P = {Poly}_{1} (E ↾_{𝑠} F)$
	ply1annig1p.b	$⊢ B = {Base}_{E}$
	ply1annig1p.e	$⊢ φ \to E \in Field$
	ply1annig1p.f	$⊢ φ \to F \in SubDRing (E)$
	ply1annig1p.a	$⊢ φ \to A \in B$
	minplyirred.1	No typesetting found for \|- M = ( E minPoly F ) with typecode \|-
	minplyirred.2	$⊢ Z = 0_{P}$
	minplyirred.3	$⊢ φ \to M (A) \neq Z$
Assertion	minplyirred	$⊢ φ \to M (A) \in Irred (P)$

Proof

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

Metamath Proof Explorer

Theorem minplyirred

Proof