minplyirredlem

	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$
	minplyirredlem.1	$⊢ φ \to G \in {Base}_{P}$
	minplyirredlem.2	$⊢ φ \to H \in {Base}_{P}$
	minplyirredlem.3	$⊢ φ \to G \cdot_{P} H = M (A)$
	minplyirredlem.4	$⊢ φ \to O (G) (A) = 0_{E}$
	minplyirredlem.5	$⊢ φ \to G \neq Z$
	minplyirredlem.6	$⊢ φ \to H \neq Z$
Assertion	minplyirredlem	$⊢ φ \to H \in Unit (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		minplyirredlem.1	$⊢ φ \to G \in {Base}_{P}$
11		minplyirredlem.2	$⊢ φ \to H \in {Base}_{P}$
12		minplyirredlem.3	$⊢ φ \to G \cdot_{P} H = M (A)$
13		minplyirredlem.4	$⊢ φ \to O (G) (A) = 0_{E}$
14		minplyirredlem.5	$⊢ φ \to G \neq Z$
15		minplyirredlem.6	$⊢ φ \to H \neq Z$
16		eqid	$⊢ E ↾_{𝑠} F = E ↾_{𝑠} F$
17	16	sdrgdrng	$⊢ F \in SubDRing (E) \to E ↾_{𝑠} F \in DivRing$
18	5 17	syl	$⊢ φ \to E ↾_{𝑠} F \in DivRing$
19	18	drngringd	$⊢ φ \to E ↾_{𝑠} F \in Ring$
20		eqid	$⊢ \deg_{1} (E ↾_{𝑠} F) = \deg_{1} (E ↾_{𝑠} F)$
21		eqid	$⊢ {Base}_{P} = {Base}_{P}$
22	20 2 8 21	deg1nn0cl	$⊢ (E ↾_{𝑠} F \in Ring \land G \in {Base}_{P} \land G \neq Z) \to \deg_{1} (E ↾_{𝑠} F) (G) \in ℕ_{0}$
23	19 10 14 22	syl3anc	$⊢ φ \to \deg_{1} (E ↾_{𝑠} F) (G) \in ℕ_{0}$
24	23	nn0red	$⊢ φ \to \deg_{1} (E ↾_{𝑠} F) (G) \in ℝ$
25	20 2 8 21	deg1nn0cl	$⊢ (E ↾_{𝑠} F \in Ring \land H \in {Base}_{P} \land H \neq Z) \to \deg_{1} (E ↾_{𝑠} F) (H) \in ℕ_{0}$
26	19 11 15 25	syl3anc	$⊢ φ \to \deg_{1} (E ↾_{𝑠} F) (H) \in ℕ_{0}$
27	26	nn0red	$⊢ φ \to \deg_{1} (E ↾_{𝑠} F) (H) \in ℝ$
28		eqid	$⊢ RLReg (E ↾_{𝑠} F) = RLReg (E ↾_{𝑠} F)$
29		eqid	$⊢ \cdot_{P} = \cdot_{P}$
30		fldsdrgfld	$⊢ (E \in Field \land F \in SubDRing (E)) \to E ↾_{𝑠} F \in Field$
31	4 5 30	syl2anc	$⊢ φ \to E ↾_{𝑠} F \in Field$
32		fldidom	$⊢ E ↾_{𝑠} F \in Field \to E ↾_{𝑠} F \in IDomn$
33	31 32	syl	$⊢ φ \to E ↾_{𝑠} F \in IDomn$
34	33	idomdomd	$⊢ φ \to E ↾_{𝑠} F \in Domn$
35		eqid	$⊢ {coe}_{1} (G) = {coe}_{1} (G)$
36	20 2 8 21 28 35	deg1ldgdomn	$⊢ (E ↾_{𝑠} F \in Domn \land G \in {Base}_{P} \land G \neq Z) \to {coe}_{1} (G) (\deg_{1} (E ↾_{𝑠} F) (G)) \in RLReg (E ↾_{𝑠} F)$
37	34 10 14 36	syl3anc	$⊢ φ \to {coe}_{1} (G) (\deg_{1} (E ↾_{𝑠} F) (G)) \in RLReg (E ↾_{𝑠} F)$
38	20 2 28 21 29 8 19 10 14 37 11 15	deg1mul2	$⊢ φ \to \deg_{1} (E ↾_{𝑠} F) (G \cdot_{P} H) = \deg_{1} (E ↾_{𝑠} F) (G) + \deg_{1} (E ↾_{𝑠} F) (H)$
39		eqid	$⊢ 0_{E} = 0_{E}$
40		eqid	$⊢ \{q \in dom O \| O (q) (A) = 0_{E}\} = \{q \in dom O \| O (q) (A) = 0_{E}\}$
41		eqid	$⊢ RSpan (P) = RSpan (P)$
42		eqid	$⊢ {idlGen}_{1p} (E ↾_{𝑠} F) = {idlGen}_{1p} (E ↾_{𝑠} F)$
43	1 2 3 4 5 6 39 40 41 42 7	minplyval	$⊢ φ \to M (A) = {idlGen}_{1p} (E ↾_{𝑠} F) (\{q \in dom O \| O (q) (A) = 0_{E}\})$
44	12 43	eqtrd	$⊢ φ \to G \cdot_{P} H = {idlGen}_{1p} (E ↾_{𝑠} F) (\{q \in dom O \| O (q) (A) = 0_{E}\})$
45	44	fveq2d	$⊢ φ \to \deg_{1} (E ↾_{𝑠} F) (G \cdot_{P} H) = \deg_{1} (E ↾_{𝑠} F) ({idlGen}_{1p} (E ↾_{𝑠} F) (\{q \in dom O \| O (q) (A) = 0_{E}\}))$
46	4	fldcrngd	$⊢ φ \to E \in CRing$
47		sdrgsubrg	$⊢ F \in SubDRing (E) \to F \in SubRing (E)$
48	5 47	syl	$⊢ φ \to F \in SubRing (E)$
49	1 2 3 46 48 6 39 40	ply1annidl	$⊢ φ \to \{q \in dom O \| O (q) (A) = 0_{E}\} \in LIdeal (P)$
50		fveq2	$⊢ q = G \to O (q) = O (G)$
51	50	fveq1d	$⊢ q = G \to O (q) (A) = O (G) (A)$
52	51	eqeq1d	$⊢ q = G \to (O (q) (A) = 0_{E} \leftrightarrow O (G) (A) = 0_{E})$
53	1 2 21 46 48	evls1dm	$⊢ φ \to dom O = {Base}_{P}$
54	10 53	eleqtrrd	$⊢ φ \to G \in dom O$
55	52 54 13	elrabd	$⊢ φ \to G \in \{q \in dom O \| O (q) (A) = 0_{E}\}$
56	2 42 21 18 49 20 8 55 14	ig1pmindeg	$⊢ φ \to \deg_{1} (E ↾_{𝑠} F) ({idlGen}_{1p} (E ↾_{𝑠} F) (\{q \in dom O \| O (q) (A) = 0_{E}\})) \leq \deg_{1} (E ↾_{𝑠} F) (G)$
57	45 56	eqbrtrd	$⊢ φ \to \deg_{1} (E ↾_{𝑠} F) (G \cdot_{P} H) \leq \deg_{1} (E ↾_{𝑠} F) (G)$
58	38 57	eqbrtrrd	$⊢ φ \to \deg_{1} (E ↾_{𝑠} F) (G) + \deg_{1} (E ↾_{𝑠} F) (H) \leq \deg_{1} (E ↾_{𝑠} F) (G)$
59		leaddle0	$⊢ (\deg_{1} (E ↾_{𝑠} F) (G) \in ℝ \land \deg_{1} (E ↾_{𝑠} F) (H) \in ℝ) \to (\deg_{1} (E ↾_{𝑠} F) (G) + \deg_{1} (E ↾_{𝑠} F) (H) \leq \deg_{1} (E ↾_{𝑠} F) (G) \leftrightarrow \deg_{1} (E ↾_{𝑠} F) (H) \leq 0)$
60	59	biimpa	$⊢ ((\deg_{1} (E ↾_{𝑠} F) (G) \in ℝ \land \deg_{1} (E ↾_{𝑠} F) (H) \in ℝ) \land \deg_{1} (E ↾_{𝑠} F) (G) + \deg_{1} (E ↾_{𝑠} F) (H) \leq \deg_{1} (E ↾_{𝑠} F) (G)) \to \deg_{1} (E ↾_{𝑠} F) (H) \leq 0$
61	24 27 58 60	syl21anc	$⊢ φ \to \deg_{1} (E ↾_{𝑠} F) (H) \leq 0$
62		eqid	$⊢ algSc (P) = algSc (P)$
63	20 2 21 62	deg1le0	$⊢ (E ↾_{𝑠} F \in Ring \land H \in {Base}_{P}) \to (\deg_{1} (E ↾_{𝑠} F) (H) \leq 0 \leftrightarrow H = algSc (P) ({coe}_{1} (H) (0)))$
64	63	biimpa	$⊢ ((E ↾_{𝑠} F \in Ring \land H \in {Base}_{P}) \land \deg_{1} (E ↾_{𝑠} F) (H) \leq 0) \to H = algSc (P) ({coe}_{1} (H) (0))$
65	19 11 61 64	syl21anc	$⊢ φ \to H = algSc (P) ({coe}_{1} (H) (0))$
66		eqid	$⊢ {Base}_{(E ↾_{𝑠} F)} = {Base}_{(E ↾_{𝑠} F)}$
67		eqid	$⊢ 0_{(E ↾_{𝑠} F)} = 0_{(E ↾_{𝑠} F)}$
68		0nn0	$⊢ 0 \in ℕ_{0}$
69		eqid	$⊢ {coe}_{1} (H) = {coe}_{1} (H)$
70	69 21 2 66	coe1fvalcl	$⊢ (H \in {Base}_{P} \land 0 \in ℕ_{0}) \to {coe}_{1} (H) (0) \in {Base}_{(E ↾_{𝑠} F)}$
71	11 68 70	sylancl	$⊢ φ \to {coe}_{1} (H) (0) \in {Base}_{(E ↾_{𝑠} F)}$
72	20 2 67 21 8 19 11 61	deg1le0eq0	$⊢ φ \to (H = Z \leftrightarrow {coe}_{1} (H) (0) = 0_{(E ↾_{𝑠} F)})$
73	72	necon3bid	$⊢ φ \to (H \neq Z \leftrightarrow {coe}_{1} (H) (0) \neq 0_{(E ↾_{𝑠} F)})$
74	15 73	mpbid	$⊢ φ \to {coe}_{1} (H) (0) \neq 0_{(E ↾_{𝑠} F)}$
75	2 62 66 67 31 71 74	ply1asclunit	$⊢ φ \to algSc (P) ({coe}_{1} (H) (0)) \in Unit (P)$
76	65 75	eqeltrd	$⊢ φ \to H \in Unit (P)$

Metamath Proof Explorer

Theorem minplyirredlem

Proof