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 = {Poly}_{1} (R)$
	drnguc1p.b	$⊢ B = {Base}_{P}$
	drnguc1p.z	$⊢ \underset{˙}{0} = 0_{P}$
	drnguc1p.c	$⊢ C = {Unic}_{1p} (R)$
Assertion	drnguc1p	$⊢ (R \in DivRing \land F \in B \land F \neq \underset{˙}{0}) \to F \in C$

Proof

Step	Hyp	Ref	Expression
1		drnguc1p.p	$⊢ P = {Poly}_{1} (R)$
2		drnguc1p.b	$⊢ B = {Base}_{P}$
3		drnguc1p.z	$⊢ \underset{˙}{0} = 0_{P}$
4		drnguc1p.c	$⊢ C = {Unic}_{1p} (R)$
5		simp2	$⊢ (R \in DivRing \land F \in B \land F \neq \underset{˙}{0}) \to F \in B$
6		simp3	$⊢ (R \in DivRing \land F \in B \land F \neq \underset{˙}{0}) \to F \neq \underset{˙}{0}$
7		eqid	$⊢ {coe}_{1} (F) = {coe}_{1} (F)$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	7 2 1 8	coe1f	$⊢ F \in B \to {coe}_{1} (F) : ℕ_{0} ⟶ {Base}_{R}$
10	9	3ad2ant2	$⊢ (R \in DivRing \land F \in B \land F \neq \underset{˙}{0}) \to {coe}_{1} (F) : ℕ_{0} ⟶ {Base}_{R}$
11		drngring	$⊢ R \in DivRing \to R \in Ring$
12		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
13	12 1 3 2	deg1nn0cl	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to \deg_{1} (R) (F) \in ℕ_{0}$
14	11 13	syl3an1	$⊢ (R \in DivRing \land F \in B \land F \neq \underset{˙}{0}) \to \deg_{1} (R) (F) \in ℕ_{0}$
15	10 14	ffvelcdmd	$⊢ (R \in DivRing \land F \in B \land F \neq \underset{˙}{0}) \to {coe}_{1} (F) (\deg_{1} (R) (F)) \in {Base}_{R}$
16		eqid	$⊢ 0_{R} = 0_{R}$
17	12 1 3 2 16 7	deg1ldg	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to {coe}_{1} (F) (\deg_{1} (R) (F)) \neq 0_{R}$
18	11 17	syl3an1	$⊢ (R \in DivRing \land F \in B \land F \neq \underset{˙}{0}) \to {coe}_{1} (F) (\deg_{1} (R) (F)) \neq 0_{R}$
19		eqid	$⊢ Unit (R) = Unit (R)$
20	8 19 16	drngunit	$⊢ R \in DivRing \to ({coe}_{1} (F) (\deg_{1} (R) (F)) \in Unit (R) \leftrightarrow ({coe}_{1} (F) (\deg_{1} (R) (F)) \in {Base}_{R} \land {coe}_{1} (F) (\deg_{1} (R) (F)) \neq 0_{R}))$
21	20	3ad2ant1	$⊢ (R \in DivRing \land F \in B \land F \neq \underset{˙}{0}) \to ({coe}_{1} (F) (\deg_{1} (R) (F)) \in Unit (R) \leftrightarrow ({coe}_{1} (F) (\deg_{1} (R) (F)) \in {Base}_{R} \land {coe}_{1} (F) (\deg_{1} (R) (F)) \neq 0_{R}))$
22	15 18 21	mpbir2and	$⊢ (R \in DivRing \land F \in B \land F \neq \underset{˙}{0}) \to {coe}_{1} (F) (\deg_{1} (R) (F)) \in Unit (R)$
23	1 2 3 12 4 19	isuc1p	$⊢ F \in C \leftrightarrow (F \in B \land F \neq \underset{˙}{0} \land {coe}_{1} (F) (\deg_{1} (R) (F)) \in Unit (R))$
24	5 6 22 23	syl3anbrc	$⊢ (R \in DivRing \land F \in B \land F \neq \underset{˙}{0}) \to F \in C$

Metamath Proof Explorer

Theorem drnguc1p

Proof