ply1scln0

Description: Nonzero scalars create nonzero polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	ply1scl.p	$⊢ P = {Poly}_{1} (R)$
	ply1scl.a	$⊢ A = algSc (P)$
	ply1scl0.z	$⊢ \underset{˙}{0} = 0_{R}$
	ply1scl0.y	$⊢ Y = 0_{P}$
	ply1scln0.k	$⊢ K = {Base}_{R}$
Assertion	ply1scln0	$⊢ (R \in Ring \land X \in K \land X \neq \underset{˙}{0}) \to A (X) \neq Y$

Step	Hyp	Ref	Expression
1		ply1scl.p	$⊢ P = {Poly}_{1} (R)$
2		ply1scl.a	$⊢ A = algSc (P)$
3		ply1scl0.z	$⊢ \underset{˙}{0} = 0_{R}$
4		ply1scl0.y	$⊢ Y = 0_{P}$
5		ply1scln0.k	$⊢ K = {Base}_{R}$
6		eqid	$⊢ {Base}_{P} = {Base}_{P}$
7	1 2 5 6	ply1sclf1	$⊢ R \in Ring \to A : K \underset{1-1}{⟶} {Base}_{P}$
8	7	adantr	$⊢ (R \in Ring \land X \in K) \to A : K \underset{1-1}{⟶} {Base}_{P}$
9		simpr	$⊢ (R \in Ring \land X \in K) \to X \in K$
10	5 3	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in K$
11	10	adantr	$⊢ (R \in Ring \land X \in K) \to \underset{˙}{0} \in K$
12		f1fveq	$⊢ (A : K \underset{1-1}{⟶} {Base}_{P} \land (X \in K \land \underset{˙}{0} \in K)) \to (A (X) = A (\underset{˙}{0}) \leftrightarrow X = \underset{˙}{0})$
13	8 9 11 12	syl12anc	$⊢ (R \in Ring \land X \in K) \to (A (X) = A (\underset{˙}{0}) \leftrightarrow X = \underset{˙}{0})$
14	13	biimpd	$⊢ (R \in Ring \land X \in K) \to (A (X) = A (\underset{˙}{0}) \to X = \underset{˙}{0})$
15	14	necon3d	$⊢ (R \in Ring \land X \in K) \to (X \neq \underset{˙}{0} \to A (X) \neq A (\underset{˙}{0}))$
16	15	3impia	$⊢ (R \in Ring \land X \in K \land X \neq \underset{˙}{0}) \to A (X) \neq A (\underset{˙}{0})$
17	1 2 3 4	ply1scl0	$⊢ R \in Ring \to A (\underset{˙}{0}) = Y$
18	17	3ad2ant1	$⊢ (R \in Ring \land X \in K \land X \neq \underset{˙}{0}) \to A (\underset{˙}{0}) = Y$
19	16 18	neeqtrd	$⊢ (R \in Ring \land X \in K \land X \neq \underset{˙}{0}) \to A (X) \neq Y$

Metamath Proof Explorer