mpaaeu

Description: An algebraic number has exactly one monic polynomial of the least degree. (Contributed by Stefan O'Rear, 25-Nov-2014)

		Ref	Expression
	Assertion	mpaaeu	$⊢ A \in 𝔸 \to \exists! p \in Poly (ℚ) (\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1)$

Proof

Step	Hyp	Ref	Expression
1		qsscn	$⊢ ℚ \subseteq ℂ$
2		eldifi	$⊢ a \in (Poly (ℚ) ∖ \{0_{𝑝}\}) \to a \in Poly (ℚ)$
3	2	ad2antlr	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to a \in Poly (ℚ)$
4		zssq	$⊢ ℤ \subseteq ℚ$
5		0z	$⊢ 0 \in ℤ$
6	4 5	sselii	$⊢ 0 \in ℚ$
7		eqid	$⊢ coeff (a) = coeff (a)$
8	7	coef2	$⊢ (a \in Poly (ℚ) \land 0 \in ℚ) \to coeff (a) : ℕ_{0} ⟶ ℚ$
9	3 6 8	sylancl	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to coeff (a) : ℕ_{0} ⟶ ℚ$
10		dgrcl	$⊢ a \in Poly (ℚ) \to \deg (a) \in ℕ_{0}$
11	3 10	syl	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to \deg (a) \in ℕ_{0}$
12	9 11	ffvelrnd	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to coeff (a) (\deg (a)) \in ℚ$
13		eldifsni	$⊢ a \in (Poly (ℚ) ∖ \{0_{𝑝}\}) \to a \neq 0_{𝑝}$
14	13	ad2antlr	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to a \neq 0_{𝑝}$
15		eqid	$⊢ \deg (a) = \deg (a)$
16	15 7	dgreq0	$⊢ a \in Poly (ℚ) \to (a = 0_{𝑝} \leftrightarrow coeff (a) (\deg (a)) = 0)$
17	16	necon3bid	$⊢ a \in Poly (ℚ) \to (a \neq 0_{𝑝} \leftrightarrow coeff (a) (\deg (a)) \neq 0)$
18	3 17	syl	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to (a \neq 0_{𝑝} \leftrightarrow coeff (a) (\deg (a)) \neq 0)$
19	14 18	mpbid	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to coeff (a) (\deg (a)) \neq 0$
20		qreccl	$⊢ (coeff (a) (\deg (a)) \in ℚ \land coeff (a) (\deg (a)) \neq 0) \to \frac{1}{coeff (a) (\deg (a))} \in ℚ$
21	12 19 20	syl2anc	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to \frac{1}{coeff (a) (\deg (a))} \in ℚ$
22		plyconst	$⊢ (ℚ \subseteq ℂ \land \frac{1}{coeff (a) (\deg (a))} \in ℚ) \to ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\} \in Poly (ℚ)$
23	1 21 22	sylancr	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\} \in Poly (ℚ)$
24		simpl	$⊢ (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\} \in Poly (ℚ) \land a \in Poly (ℚ)) \to ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\} \in Poly (ℚ)$
25		simpr	$⊢ (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\} \in Poly (ℚ) \land a \in Poly (ℚ)) \to a \in Poly (ℚ)$
26		qaddcl	$⊢ (b \in ℚ \land c \in ℚ) \to b + c \in ℚ$
27	26	adantl	$⊢ ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\} \in Poly (ℚ) \land a \in Poly (ℚ)) \land (b \in ℚ \land c \in ℚ)) \to b + c \in ℚ$
28		qmulcl	$⊢ (b \in ℚ \land c \in ℚ) \to b c \in ℚ$
29	28	adantl	$⊢ ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\} \in Poly (ℚ) \land a \in Poly (ℚ)) \land (b \in ℚ \land c \in ℚ)) \to b c \in ℚ$
30	24 25 27 29	plymul	$⊢ (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\} \in Poly (ℚ) \land a \in Poly (ℚ)) \to (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a \in Poly (ℚ)$
31	23 3 30	syl2anc	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a \in Poly (ℚ)$
32	7	coef3	$⊢ a \in Poly (ℚ) \to coeff (a) : ℕ_{0} ⟶ ℂ$
33	3 32	syl	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to coeff (a) : ℕ_{0} ⟶ ℂ$
34	33 11	ffvelrnd	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to coeff (a) (\deg (a)) \in ℂ$
35	34 19	reccld	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to \frac{1}{coeff (a) (\deg (a))} \in ℂ$
36	34 19	recne0d	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to \frac{1}{coeff (a) (\deg (a))} \neq 0$
37		dgrmulc	$⊢ (\frac{1}{coeff (a) (\deg (a))} \in ℂ \land \frac{1}{coeff (a) (\deg (a))} \neq 0 \land a \in Poly (ℚ)) \to \deg ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) = \deg (a)$
38	35 36 3 37	syl3anc	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to \deg ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) = \deg (a)$
39		simprl	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to \deg (a) = \deg_{𝔸} (A)$
40	38 39	eqtrd	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to \deg ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) = \deg_{𝔸} (A)$
41		aacn	$⊢ A \in 𝔸 \to A \in ℂ$
42	41	ad2antrr	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to A \in ℂ$
43		ovex	$⊢ \frac{1}{coeff (a) (\deg (a))} \in V$
44		fnconstg	$⊢ \frac{1}{coeff (a) (\deg (a))} \in V \to (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) Fn ℂ$
45	43 44	mp1i	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) Fn ℂ$
46		plyf	$⊢ a \in Poly (ℚ) \to a : ℂ ⟶ ℂ$
47		ffn	$⊢ a : ℂ ⟶ ℂ \to a Fn ℂ$
48	3 46 47	3syl	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to a Fn ℂ$
49		cnex	$⊢ ℂ \in V$
50	49	a1i	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to ℂ \in V$
51		inidm	$⊢ ℂ \cap ℂ = ℂ$
52	43	fvconst2	$⊢ A \in ℂ \to (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) (A) = \frac{1}{coeff (a) (\deg (a))}$
53	52	adantl	$⊢ (((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \land A \in ℂ) \to (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) (A) = \frac{1}{coeff (a) (\deg (a))}$
54		simplrr	$⊢ (((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \land A \in ℂ) \to a (A) = 0$
55	45 48 50 50 51 53 54	ofval	$⊢ (((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \land A \in ℂ) \to ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (A) = (\frac{1}{coeff (a) (\deg (a))}) \cdot 0$
56	42 55	mpdan	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (A) = (\frac{1}{coeff (a) (\deg (a))}) \cdot 0$
57	35	mul01d	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to (\frac{1}{coeff (a) (\deg (a))}) \cdot 0 = 0$
58	56 57	eqtrd	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (A) = 0$
59		coemulc	$⊢ (\frac{1}{coeff (a) (\deg (a))} \in ℂ \land a \in Poly (ℚ)) \to coeff ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) = (ℕ_{0} \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} coeff (a)$
60	35 3 59	syl2anc	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to coeff ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) = (ℕ_{0} \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} coeff (a)$
61	60	fveq1d	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to coeff ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (\deg_{𝔸} (A)) = ((ℕ_{0} \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} coeff (a)) (\deg_{𝔸} (A))$
62		dgraacl	$⊢ A \in 𝔸 \to \deg_{𝔸} (A) \in ℕ$
63	62	ad2antrr	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to \deg_{𝔸} (A) \in ℕ$
64	63	nnnn0d	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to \deg_{𝔸} (A) \in ℕ_{0}$
65		fnconstg	$⊢ \frac{1}{coeff (a) (\deg (a))} \in V \to (ℕ_{0} \times \{\frac{1}{coeff (a) (\deg (a))}\}) Fn ℕ_{0}$
66	43 65	mp1i	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to (ℕ_{0} \times \{\frac{1}{coeff (a) (\deg (a))}\}) Fn ℕ_{0}$
67	33	ffnd	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to coeff (a) Fn ℕ_{0}$
68		nn0ex	$⊢ ℕ_{0} \in V$
69	68	a1i	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to ℕ_{0} \in V$
70		inidm	$⊢ ℕ_{0} \cap ℕ_{0} = ℕ_{0}$
71	43	fvconst2	$⊢ \deg_{𝔸} (A) \in ℕ_{0} \to (ℕ_{0} \times \{\frac{1}{coeff (a) (\deg (a))}\}) (\deg_{𝔸} (A)) = \frac{1}{coeff (a) (\deg (a))}$
72	71	adantl	$⊢ (((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \land \deg_{𝔸} (A) \in ℕ_{0}) \to (ℕ_{0} \times \{\frac{1}{coeff (a) (\deg (a))}\}) (\deg_{𝔸} (A)) = \frac{1}{coeff (a) (\deg (a))}$
73		simplrl	$⊢ (((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \land \deg_{𝔸} (A) \in ℕ_{0}) \to \deg (a) = \deg_{𝔸} (A)$
74	73	eqcomd	$⊢ (((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \land \deg_{𝔸} (A) \in ℕ_{0}) \to \deg_{𝔸} (A) = \deg (a)$
75	74	fveq2d	$⊢ (((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \land \deg_{𝔸} (A) \in ℕ_{0}) \to coeff (a) (\deg_{𝔸} (A)) = coeff (a) (\deg (a))$
76	66 67 69 69 70 72 75	ofval	$⊢ (((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \land \deg_{𝔸} (A) \in ℕ_{0}) \to ((ℕ_{0} \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} coeff (a)) (\deg_{𝔸} (A)) = (\frac{1}{coeff (a) (\deg (a))}) coeff (a) (\deg (a))$
77	64 76	mpdan	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to ((ℕ_{0} \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} coeff (a)) (\deg_{𝔸} (A)) = (\frac{1}{coeff (a) (\deg (a))}) coeff (a) (\deg (a))$
78	34 19	recid2d	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to (\frac{1}{coeff (a) (\deg (a))}) coeff (a) (\deg (a)) = 1$
79	61 77 78	3eqtrd	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to coeff ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (\deg_{𝔸} (A)) = 1$
80		fveqeq2	$⊢ p = (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a \to (\deg (p) = \deg_{𝔸} (A) \leftrightarrow \deg ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) = \deg_{𝔸} (A))$
81		fveq1	$⊢ p = (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a \to p (A) = ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (A)$
82	81	eqeq1d	$⊢ p = (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a \to (p (A) = 0 \leftrightarrow ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (A) = 0)$
83		fveq2	$⊢ p = (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a \to coeff (p) = coeff ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a)$
84	83	fveq1d	$⊢ p = (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a \to coeff (p) (\deg_{𝔸} (A)) = coeff ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (\deg_{𝔸} (A))$
85	84	eqeq1d	$⊢ p = (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a \to (coeff (p) (\deg_{𝔸} (A)) = 1 \leftrightarrow coeff ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (\deg_{𝔸} (A)) = 1)$
86	80 82 85	3anbi123d	$⊢ p = (ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a \to ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \leftrightarrow (\deg ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) = \deg_{𝔸} (A) \land ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (A) = 0 \land coeff ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (\deg_{𝔸} (A)) = 1))$
87	86	rspcev	$⊢ ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a \in Poly (ℚ) \land (\deg ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) = \deg_{𝔸} (A) \land ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (A) = 0 \land coeff ((ℂ \times \{\frac{1}{coeff (a) (\deg (a))}\}) \times_{f} a) (\deg_{𝔸} (A)) = 1)) \to \exists p \in Poly (ℚ) (\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1)$
88	31 40 58 79 87	syl13anc	$⊢ ((A \in 𝔸 \land a \in (Poly (ℚ) ∖ \{0_{𝑝}\})) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)) \to \exists p \in Poly (ℚ) (\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1)$
89		dgraalem	$⊢ A \in 𝔸 \to (\deg_{𝔸} (A) \in ℕ \land \exists a \in (Poly (ℚ) ∖ \{0_{𝑝}\}) (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0))$
90	89	simprd	$⊢ A \in 𝔸 \to \exists a \in (Poly (ℚ) ∖ \{0_{𝑝}\}) (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0)$
91	88 90	r19.29a	$⊢ A \in 𝔸 \to \exists p \in Poly (ℚ) (\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1)$
92		simp2	$⊢ (\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \to p (A) = 0$
93		simp2	$⊢ (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1) \to a (A) = 0$
94	92 93	anim12i	$⊢ ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1)) \to (p (A) = 0 \land a (A) = 0)$
95		plyf	$⊢ p \in Poly (ℚ) \to p : ℂ ⟶ ℂ$
96	95	ffnd	$⊢ p \in Poly (ℚ) \to p Fn ℂ$
97	96	ad2antrr	$⊢ ((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (p (A) = 0 \land a (A) = 0)) \to p Fn ℂ$
98	46	ffnd	$⊢ a \in Poly (ℚ) \to a Fn ℂ$
99	98	ad2antlr	$⊢ ((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (p (A) = 0 \land a (A) = 0)) \to a Fn ℂ$
100	49	a1i	$⊢ ((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (p (A) = 0 \land a (A) = 0)) \to ℂ \in V$
101		simplrl	$⊢ (((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (p (A) = 0 \land a (A) = 0)) \land A \in ℂ) \to p (A) = 0$
102		simplrr	$⊢ (((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (p (A) = 0 \land a (A) = 0)) \land A \in ℂ) \to a (A) = 0$
103	97 99 100 100 51 101 102	ofval	$⊢ (((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (p (A) = 0 \land a (A) = 0)) \land A \in ℂ) \to (p -_{f} a) (A) = 0 - 0$
104	41 103	sylan2	$⊢ (((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (p (A) = 0 \land a (A) = 0)) \land A \in 𝔸) \to (p -_{f} a) (A) = 0 - 0$
105		0m0e0	$⊢ 0 - 0 = 0$
106	104 105	eqtrdi	$⊢ (((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (p (A) = 0 \land a (A) = 0)) \land A \in 𝔸) \to (p -_{f} a) (A) = 0$
107	106	ex	$⊢ ((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (p (A) = 0 \land a (A) = 0)) \to (A \in 𝔸 \to (p -_{f} a) (A) = 0)$
108	94 107	sylan2	$⊢ ((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to (A \in 𝔸 \to (p -_{f} a) (A) = 0)$
109	108	com12	$⊢ A \in 𝔸 \to (((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to (p -_{f} a) (A) = 0)$
110	109	impl	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to (p -_{f} a) (A) = 0$
111		simpll	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to A \in 𝔸$
112		simpl	$⊢ (p \in Poly (ℚ) \land a \in Poly (ℚ)) \to p \in Poly (ℚ)$
113		simpr	$⊢ (p \in Poly (ℚ) \land a \in Poly (ℚ)) \to a \in Poly (ℚ)$
114	26	adantl	$⊢ ((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (b \in ℚ \land c \in ℚ)) \to b + c \in ℚ$
115	28	adantl	$⊢ ((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (b \in ℚ \land c \in ℚ)) \to b c \in ℚ$
116		1z	$⊢ 1 \in ℤ$
117		zq	$⊢ 1 \in ℤ \to 1 \in ℚ$
118		qnegcl	$⊢ 1 \in ℚ \to - 1 \in ℚ$
119	116 117 118	mp2b	$⊢ - 1 \in ℚ$
120	119	a1i	$⊢ (p \in Poly (ℚ) \land a \in Poly (ℚ)) \to - 1 \in ℚ$
121	112 113 114 115 120	plysub	$⊢ (p \in Poly (ℚ) \land a \in Poly (ℚ)) \to p -_{f} a \in Poly (ℚ)$
122	121	ad2antlr	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to p -_{f} a \in Poly (ℚ)$
123		simplrl	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to p \in Poly (ℚ)$
124		simplrr	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to a \in Poly (ℚ)$
125		simprr1	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to \deg (a) = \deg_{𝔸} (A)$
126		simprl1	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to \deg (p) = \deg_{𝔸} (A)$
127	125 126	eqtr4d	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to \deg (a) = \deg (p)$
128	62	ad2antrr	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to \deg_{𝔸} (A) \in ℕ$
129	126 128	eqeltrd	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to \deg (p) \in ℕ$
130		simprl3	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to coeff (p) (\deg_{𝔸} (A)) = 1$
131	126	fveq2d	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to coeff (p) (\deg (p)) = coeff (p) (\deg_{𝔸} (A))$
132	126	fveq2d	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to coeff (a) (\deg (p)) = coeff (a) (\deg_{𝔸} (A))$
133		simprr3	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to coeff (a) (\deg_{𝔸} (A)) = 1$
134	132 133	eqtrd	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to coeff (a) (\deg (p)) = 1$
135	130 131 134	3eqtr4d	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to coeff (p) (\deg (p)) = coeff (a) (\deg (p))$
136		eqid	$⊢ \deg (p) = \deg (p)$
137	136	dgrsub2	$⊢ ((p \in Poly (ℚ) \land a \in Poly (ℚ)) \land (\deg (a) = \deg (p) \land \deg (p) \in ℕ \land coeff (p) (\deg (p)) = coeff (a) (\deg (p)))) \to \deg (p -_{f} a) < \deg (p)$
138	123 124 127 129 135 137	syl23anc	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to \deg (p -_{f} a) < \deg (p)$
139	138 126	breqtrd	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to \deg (p -_{f} a) < \deg_{𝔸} (A)$
140		dgraa0p	$⊢ (A \in 𝔸 \land p -_{f} a \in Poly (ℚ) \land \deg (p -_{f} a) < \deg_{𝔸} (A)) \to ((p -_{f} a) (A) = 0 \leftrightarrow p -_{f} a = 0_{𝑝})$
141	111 122 139 140	syl3anc	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to ((p -_{f} a) (A) = 0 \leftrightarrow p -_{f} a = 0_{𝑝})$
142	110 141	mpbid	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to p -_{f} a = 0_{𝑝}$
143		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
144	142 143	eqtrdi	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to p -_{f} a = ℂ \times \{0\}$
145		ofsubeq0	$⊢ (ℂ \in V \land p : ℂ ⟶ ℂ \land a : ℂ ⟶ ℂ) \to (p -_{f} a = ℂ \times \{0\} \leftrightarrow p = a)$
146	49 145	mp3an1	$⊢ (p : ℂ ⟶ ℂ \land a : ℂ ⟶ ℂ) \to (p -_{f} a = ℂ \times \{0\} \leftrightarrow p = a)$
147	95 46 146	syl2an	$⊢ (p \in Poly (ℚ) \land a \in Poly (ℚ)) \to (p -_{f} a = ℂ \times \{0\} \leftrightarrow p = a)$
148	147	ad2antlr	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to (p -_{f} a = ℂ \times \{0\} \leftrightarrow p = a)$
149	144 148	mpbid	$⊢ ((A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \land ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))) \to p = a$
150	149	ex	$⊢ (A \in 𝔸 \land (p \in Poly (ℚ) \land a \in Poly (ℚ))) \to (((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1)) \to p = a)$
151	150	ralrimivva	$⊢ A \in 𝔸 \to \forall p \in Poly (ℚ) \forall a \in Poly (ℚ) (((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1)) \to p = a)$
152		fveqeq2	$⊢ p = a \to (\deg (p) = \deg_{𝔸} (A) \leftrightarrow \deg (a) = \deg_{𝔸} (A))$
153		fveq1	$⊢ p = a \to p (A) = a (A)$
154	153	eqeq1d	$⊢ p = a \to (p (A) = 0 \leftrightarrow a (A) = 0)$
155		fveq2	$⊢ p = a \to coeff (p) = coeff (a)$
156	155	fveq1d	$⊢ p = a \to coeff (p) (\deg_{𝔸} (A)) = coeff (a) (\deg_{𝔸} (A))$
157	156	eqeq1d	$⊢ p = a \to (coeff (p) (\deg_{𝔸} (A)) = 1 \leftrightarrow coeff (a) (\deg_{𝔸} (A)) = 1)$
158	152 154 157	3anbi123d	$⊢ p = a \to ((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \leftrightarrow (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1))$
159	158	reu4	$⊢ \exists! p \in Poly (ℚ) (\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \leftrightarrow (\exists p \in Poly (ℚ) (\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land \forall p \in Poly (ℚ) \forall a \in Poly (ℚ) (((\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1) \land (\deg (a) = \deg_{𝔸} (A) \land a (A) = 0 \land coeff (a) (\deg_{𝔸} (A)) = 1)) \to p = a))$
160	91 151 159	sylanbrc	$⊢ A \in 𝔸 \to \exists! p \in Poly (ℚ) (\deg (p) = \deg_{𝔸} (A) \land p (A) = 0 \land coeff (p) (\deg_{𝔸} (A)) = 1)$

Metamath Proof Explorer

Theorem mpaaeu

Proof