Theorem drnguc1p

Description: Over a division ring, all nonzero polynomials are unitic. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	drnguc1p.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	drnguc1p.b	$$⊢B={\mathrm{Base}}_P$$
	drnguc1p.z	$$⊢\underset{\dot{}}{0}=0_P$$
	drnguc1p.c	$$⊢C={Unic}_{\mathrm{1p}}\left(R\right)$$
Assertion	drnguc1p	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to F\in C$$

Proof

Step	Hyp	Ref	Expression
1		drnguc1p.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		drnguc1p.b	$$⊢B={\mathrm{Base}}_P$$
3		drnguc1p.z	$$⊢\underset{\dot{}}{0}=0_P$$
4		drnguc1p.c	$$⊢C={Unic}_{\mathrm{1p}}\left(R\right)$$
5		simp2	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to F\in B$$
6		simp3	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to F\ne \underset{\dot{}}{0}$$
7		eqid	$$⊢{\mathrm{coe}}_1\left(F\right)={\mathrm{coe}}_1\left(F\right)$$
8		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
9	7 2 1 8	coe1f	$$⊢F\in B\to {\mathrm{coe}}_1\left(F\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
10	9	3ad2ant2	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to {\mathrm{coe}}_1\left(F\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
11		drngring	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Ring}$$
12		eqid	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(R\right)$$
13	12 1 3 2	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to {\mathrm{deg}}_1\left(R\right)\left(F\right)\in {\mathbb{N}}_0$$
14	11 13	syl3an1	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to {\mathrm{deg}}_1\left(R\right)\left(F\right)\in {\mathbb{N}}_0$$
15	10 14	ffvelrnd	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to {\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\in {\mathrm{Base}}_R$$
16		eqid	$$⊢0_R=0_R$$
17	12 1 3 2 16 7	deg1ldg	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to {\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\ne 0_R$$
18	11 17	syl3an1	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to {\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\ne 0_R$$
19		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
20	8 19 16	drngunit	$$⊢R\in \mathrm{DivRing}\to \left({\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\in \mathrm{Unit}\left(R\right)\leftrightarrow \left({\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\in {\mathrm{Base}}_R\wedge {\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\ne 0_R\right)\right)$$
21	20	3ad2ant1	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to \left({\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\in \mathrm{Unit}\left(R\right)\leftrightarrow \left({\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\in {\mathrm{Base}}_R\wedge {\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\ne 0_R\right)\right)$$
22	15 18 21	mpbir2and	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to {\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\in \mathrm{Unit}\left(R\right)$$
23	1 2 3 12 4 19	isuc1p	$$⊢F\in C\leftrightarrow \left(F\in B\wedge F\ne \underset{\dot{}}{0}\wedge {\mathrm{coe}}_1\left(F\right)\left({\mathrm{deg}}_1\left(R\right)\left(F\right)\right)\in \mathrm{Unit}\left(R\right)\right)$$
24	5 6 22 23	syl3anbrc	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to F\in C$$