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		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
10	2 9 4	ply1bas	$⊢ B = {Base}_{(1_{𝑜} mPoly R)}$
11		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{c \in ({ℕ_{0}}^{1_{𝑜}}) \| c^{-1} [ℕ] \in Fin\}$
12		tdeglem2	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) = (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \sum_{ℂ_{fld}} a)$
13	8 2 3	ply1mpl0	$⊢ \underset{˙}{0} = 0_{(1_{𝑜} mPoly R)}$
14	7 8 10 5 11 12 13	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))$
15	6	fvcoe1	$⊢ (F \in B \land b \in ({ℕ_{0}}^{1_{𝑜}})) \to F (b) = A (b (\emptyset))$
16	15	3ad2antl2	$⊢ ((R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \land b \in ({ℕ_{0}}^{1_{𝑜}})) \to F (b) = A (b (\emptyset))$
17		fveq1	$⊢ a = b \to a (\emptyset) = b (\emptyset)$
18		eqid	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) = (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset))$
19		fvex	$⊢ b (\emptyset) \in V$
20	17 18 19	fvmpt	$⊢ b \in ({ℕ_{0}}^{1_{𝑜}}) \to (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = b (\emptyset)$
21	20	fveq2d	$⊢ b \in ({ℕ_{0}}^{1_{𝑜}}) \to A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) = A (b (\emptyset))$
22	21	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))$
23	16 22	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))$
24	23	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)$
25	24	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)))$
26	25	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))$
27	26	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))$
28		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
29		nn0ex	$⊢ ℕ_{0} \in V$
30		0ex	$⊢ \emptyset \in V$
31	28 29 30 18	mapsnf1o2	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) : {ℕ_{0}}^{1_{𝑜}} \underset{1-1 onto}{⟶} ℕ_{0}$
32		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}$
33		eqeq1	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = d \to ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = D (F) \leftrightarrow d = D (F))$
34		fveq2	$⊢ (a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b) = d \to A ((a \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ a (\emptyset)) (b)) = A (d)$
35	34	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)$
36	33 35	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))$
37	36	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))$
38	31 32 37	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)$
39	27 38	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))$
40	1 2 3 4	deg1nn0cl	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to D (F) \in ℕ_{0}$
41		fveq2	$⊢ d = D (F) \to A (d) = A (D (F))$
42	41	neeq1d	$⊢ d = D (F) \to (A (d) \neq Y \leftrightarrow A (D (F)) \neq Y)$
43	42	ceqsrexv	$⊢ D (F) \in ℕ_{0} \to (\exists d \in ℕ_{0} (d = D (F) \land A (d) \neq Y) \leftrightarrow A (D (F)) \neq Y)$
44	40 43	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)$
45	39 44	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)$
46	14 45	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