mon1puc1p

Description: Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015)

Step	Hyp	Ref	Expression
1		mon1puc1p.c	$⊢ C = {Unic}_{1p} (R)$
2		mon1puc1p.m	$⊢ M = {Monic}_{1p} (R)$
3		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
4		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
5	3 4 2	mon1pcl	$⊢ X \in M \to X \in {Base}_{{Poly}_{1} (R)}$
6	5	adantl	$⊢ (R \in Ring \land X \in M) \to X \in {Base}_{{Poly}_{1} (R)}$
7		eqid	$⊢ 0_{{Poly}_{1} (R)} = 0_{{Poly}_{1} (R)}$
8	3 7 2	mon1pn0	$⊢ X \in M \to X \neq 0_{{Poly}_{1} (R)}$
9	8	adantl	$⊢ (R \in Ring \land X \in M) \to X \neq 0_{{Poly}_{1} (R)}$
10		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
11		eqid	$⊢ 1_{R} = 1_{R}$
12	10 11 2	mon1pldg	$⊢ X \in M \to {coe}_{1} (X) (\deg_{1} (R) (X)) = 1_{R}$
13	12	adantl	$⊢ (R \in Ring \land X \in M) \to {coe}_{1} (X) (\deg_{1} (R) (X)) = 1_{R}$
14		eqid	$⊢ Unit (R) = Unit (R)$
15	14 11	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
16	15	adantr	$⊢ (R \in Ring \land X \in M) \to 1_{R} \in Unit (R)$
17	13 16	eqeltrd	$⊢ (R \in Ring \land X \in M) \to {coe}_{1} (X) (\deg_{1} (R) (X)) \in Unit (R)$
18	3 4 7 10 1 14	isuc1p	$⊢ X \in C \leftrightarrow (X \in {Base}_{{Poly}_{1} (R)} \land X \neq 0_{{Poly}_{1} (R)} \land {coe}_{1} (X) (\deg_{1} (R) (X)) \in Unit (R))$
19	6 9 17 18	syl3anbrc	$⊢ (R \in Ring \land X \in M) \to X \in C$

Metamath Proof Explorer