Metamath Proof Explorer

Theorem deg1ldgdomn

Description: A nonzero univariate polynomial over a domain always has a nonzero-divisor leading coefficient. (Contributed by Stefan O'Rear, 28-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}$
		deg1ldgdomn.e	$⊢ E = RLReg (R)$
		deg1ldgdomn.a	$⊢ A = {coe}_{1} (F)$
	Assertion	deg1ldgdomn	$⊢ (R \in Domn \land F \in B \land F \neq \underset{˙}{0}) \to A (D (F)) \in E$

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		deg1ldgdomn.e	$⊢ E = RLReg (R)$
6		deg1ldgdomn.a	$⊢ A = {coe}_{1} (F)$
7		simp1	$⊢ (R \in Domn \land F \in B \land F \neq \underset{˙}{0}) \to R \in Domn$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	6 4 2 8	coe1f	$⊢ F \in B \to A : ℕ_{0} ⟶ {Base}_{R}$
10	9	3ad2ant2	$⊢ (R \in Domn \land F \in B \land F \neq \underset{˙}{0}) \to A : ℕ_{0} ⟶ {Base}_{R}$
11		domnring	$⊢ R \in Domn \to R \in Ring$
12	1 2 3 4	deg1nn0cl	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to D (F) \in ℕ_{0}$
13	11 12	syl3an1	$⊢ (R \in Domn \land F \in B \land F \neq \underset{˙}{0}) \to D (F) \in ℕ_{0}$
14	10 13	ffvelcdmd	$⊢ (R \in Domn \land F \in B \land F \neq \underset{˙}{0}) \to A (D (F)) \in {Base}_{R}$
15		eqid	$⊢ 0_{R} = 0_{R}$
16	1 2 3 4 15 6	deg1ldg	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to A (D (F)) \neq 0_{R}$
17	11 16	syl3an1	$⊢ (R \in Domn \land F \in B \land F \neq \underset{˙}{0}) \to A (D (F)) \neq 0_{R}$
18	8 5 15	domnrrg	$⊢ (R \in Domn \land A (D (F)) \in {Base}_{R} \land A (D (F)) \neq 0_{R}) \to A (D (F)) \in E$
19	7 14 17 18	syl3anc	$⊢ (R \in Domn \land F \in B \land F \neq \underset{˙}{0}) \to A (D (F)) \in E$