deg1ldg

Description: A nonzero univariate polynomial always has a nonzero leading coefficient. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1z.d	$⊢ D = \deg_{1} (R)$
	deg1z.p	$⊢ P = {Poly}_{1} (R)$
	deg1z.z	$⊢ \underset{˙}{0} = 0_{P}$
	deg1nn0cl.b	$⊢ B = {Base}_{P}$
	deg1ldg.y	$⊢ Y = 0_{R}$
	deg1ldg.a	$⊢ A = {coe}_{1} (F)$
Assertion	deg1ldg	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to A (D (F)) \neq Y$

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	$⊢ D = \deg_{1} (R)$
2		deg1z.p	$⊢ P = {Poly}_{1} (R)$
3		deg1z.z	$⊢ \underset{˙}{0} = 0_{P}$
4		deg1nn0cl.b	$⊢ B = {Base}_{P}$
5		deg1ldg.y	$⊢ Y = 0_{R}$
6		deg1ldg.a	$⊢ A = {coe}_{1} (F)$
7	1	deg1fval	$⊢ D = 1_{𝑜} mDeg R$
8		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
9	2 4	ply1bas	$⊢ B = {Base}_{(1_{𝑜} mPoly R)}$
10		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{c \in ({ℕ_{0}}^{1_{𝑜}}) \| c^{-1} [ℕ] \in Fin\}$
11		tdeglem2	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) = (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \sum_{ℂ_{fld}} a)$
12	8 2 3	ply1mpl0	$⊢ \underset{˙}{0} = 0_{(1_{𝑜} mPoly R)}$
13	7 8 9 5 10 11 12	mdegldg	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to \exists b \in ({ℕ_{0}}^{1_{𝑜}}) (F (b) \neq Y \land (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F))$
14	6	fvcoe1	$⊢ (F \in B \land b \in ({ℕ_{0}}^{1_{𝑜}})) \to F (b) = A (b (\emptyset))$
15	14	3ad2antl2	$⊢ ((R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \land b \in ({ℕ_{0}}^{1_{𝑜}})) \to F (b) = A (b (\emptyset))$
16		fveq1	$⊢ a = b \to a (\emptyset) = b (\emptyset)$
17		eqid	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) = (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset))$
18		fvex	$⊢ b (\emptyset) \in V$
19	16 17 18	fvmpt	$⊢ b \in ({ℕ_{0}}^{1_{𝑜}}) \to (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = b (\emptyset)$
20	19	fveq2d	$⊢ b \in ({ℕ_{0}}^{1_{𝑜}}) \to A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) = A (b (\emptyset))$
21	20	adantl	$⊢ ((R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \land b \in ({ℕ_{0}}^{1_{𝑜}})) \to A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) = A (b (\emptyset))$
22	15 21	eqtr4d	$⊢ ((R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \land b \in ({ℕ_{0}}^{1_{𝑜}})) \to F (b) = A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b))$
23	22	neeq1d	$⊢ ((R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \land b \in ({ℕ_{0}}^{1_{𝑜}})) \to (F (b) \neq Y \leftrightarrow A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) \neq Y)$
24	23	anbi1d	$⊢ ((R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \land b \in ({ℕ_{0}}^{1_{𝑜}})) \to ((F (b) \neq Y \land (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F)) \leftrightarrow (A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) \neq Y \land (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F)))$
25	24	biancomd	$⊢ ((R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \land b \in ({ℕ_{0}}^{1_{𝑜}})) \to ((F (b) \neq Y \land (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F)) \leftrightarrow ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F) \land A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) \neq Y))$
26	25	rexbidva	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to (\exists b \in ({ℕ_{0}}^{1_{𝑜}}) (F (b) \neq Y \land (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F)) \leftrightarrow \exists b \in ({ℕ_{0}}^{1_{𝑜}}) ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F) \land A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) \neq Y))$
27		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
28		nn0ex	$⊢ ℕ_{0} \in V$
29		0ex	$⊢ \emptyset \in V$
30	27 28 29 17	mapsnf1o2	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) : {ℕ_{0}}^{1_{𝑜}} \underset{1-1 onto}{⟶} ℕ_{0}$
31		f1ofo	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) : {ℕ_{0}}^{1_{𝑜}} \underset{1-1 onto}{⟶} ℕ_{0} \to (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) : {ℕ_{0}}^{1_{𝑜}} \underset{onto}{⟶} ℕ_{0}$
32		eqeq1	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = d \to ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F) \leftrightarrow d = D (F))$
33		fveq2	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = d \to A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) = A (d)$
34	33	neeq1d	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = d \to (A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) \neq Y \leftrightarrow A (d) \neq Y)$
35	32 34	anbi12d	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = d \to (((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F) \land A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) \neq Y) \leftrightarrow (d = D (F) \land A (d) \neq Y))$
36	35	cbvexfo	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) : {ℕ_{0}}^{1_{𝑜}} \underset{onto}{⟶} ℕ_{0} \to (\exists b \in ({ℕ_{0}}^{1_{𝑜}}) ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F) \land A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) \neq Y) \leftrightarrow \exists d \in ℕ_{0} (d = D (F) \land A (d) \neq Y))$
37	30 31 36	mp2b	$⊢ \exists b \in ({ℕ_{0}}^{1_{𝑜}}) ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F) \land A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) \neq Y) \leftrightarrow \exists d \in ℕ_{0} (d = D (F) \land A (d) \neq Y)$
38	26 37	bitrdi	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to (\exists b \in ({ℕ_{0}}^{1_{𝑜}}) (F (b) \neq Y \land (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F)) \leftrightarrow \exists d \in ℕ_{0} (d = D (F) \land A (d) \neq Y))$
39	1 2 3 4	deg1nn0cl	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to D (F) \in ℕ_{0}$
40		fveq2	$⊢ d = D (F) \to A (d) = A (D (F))$
41	40	neeq1d	$⊢ d = D (F) \to (A (d) \neq Y \leftrightarrow A (D (F)) \neq Y)$
42	41	ceqsrexv	$⊢ D (F) \in ℕ_{0} \to (\exists d \in ℕ_{0} (d = D (F) \land A (d) \neq Y) \leftrightarrow A (D (F)) \neq Y)$
43	39 42	syl	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to (\exists d \in ℕ_{0} (d = D (F) \land A (d) \neq Y) \leftrightarrow A (D (F)) \neq Y)$
44	38 43	bitrd	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to (\exists b \in ({ℕ_{0}}^{1_{𝑜}}) (F (b) \neq Y \land (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F)) \leftrightarrow A (D (F)) \neq Y)$
45	13 44	mpbid	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to A (D (F)) \neq Y$

Metamath Proof Explorer

Theorem deg1ldg

Proof