ply1nz

Description: Univariate polynomials over a nonzero ring are a nonzero ring. (Contributed by Stefan O'Rear, 29-Mar-2015)

		Ref	Expression
	Hypothesis	ply1domn.p	$⊢ P = {Poly}_{1} (R)$
	Assertion	ply1nz	$⊢ R \in NzRing \to P \in NzRing$

Step	Hyp	Ref	Expression
1		ply1domn.p	$⊢ P = {Poly}_{1} (R)$
2		nzrring	$⊢ R \in NzRing \to R \in Ring$
3	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
4	2 3	syl	$⊢ R \in NzRing \to P \in Ring$
5		eqid	$⊢ algSc (P) = algSc (P)$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ {Base}_{P} = {Base}_{P}$
8	1 5 6 7	ply1sclf	$⊢ R \in Ring \to algSc (P) : {Base}_{R} ⟶ {Base}_{P}$
9	2 8	syl	$⊢ R \in NzRing \to algSc (P) : {Base}_{R} ⟶ {Base}_{P}$
10		eqid	$⊢ 1_{R} = 1_{R}$
11	6 10	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
12	2 11	syl	$⊢ R \in NzRing \to 1_{R} \in {Base}_{R}$
13	9 12	ffvelrnd	$⊢ R \in NzRing \to algSc (P) (1_{R}) \in {Base}_{P}$
14		eqid	$⊢ 0_{R} = 0_{R}$
15	10 14	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
16		eqid	$⊢ 0_{P} = 0_{P}$
17	1 5 14 16 6	ply1scln0	$⊢ (R \in Ring \land 1_{R} \in {Base}_{R} \land 1_{R} \neq 0_{R}) \to algSc (P) (1_{R}) \neq 0_{P}$
18	2 12 15 17	syl3anc	$⊢ R \in NzRing \to algSc (P) (1_{R}) \neq 0_{P}$
19		eldifsn	$⊢ algSc (P) (1_{R}) \in ({Base}_{P} ∖ \{0_{P}\}) \leftrightarrow (algSc (P) (1_{R}) \in {Base}_{P} \land algSc (P) (1_{R}) \neq 0_{P})$
20	13 18 19	sylanbrc	$⊢ R \in NzRing \to algSc (P) (1_{R}) \in ({Base}_{P} ∖ \{0_{P}\})$
21	16 7	ringelnzr	$⊢ (P \in Ring \land algSc (P) (1_{R}) \in ({Base}_{P} ∖ \{0_{P}\})) \to P \in NzRing$
22	4 20 21	syl2anc	$⊢ R \in NzRing \to P \in NzRing$

Metamath Proof Explorer