Theorem ply1scln0

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

	Ref	Expression
Hypotheses	ply1scl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1scl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	ply1scl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
	ply1scl0.y	⊢ 𝑌 = ( 0g ‘ 𝑃 )
	ply1scln0.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion	ply1scln0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( 𝐴 ‘ 𝑋 ) ≠ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1scl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
3		ply1scl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		ply1scl0.y	⊢ 𝑌 = ( 0g ‘ 𝑃 )
5		ply1scln0.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
6		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
7	1 2 5 6	ply1sclf1	⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐾 –1-1→ ( Base ‘ 𝑃 ) )
8	7	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → 𝐴 : 𝐾 –1-1→ ( Base ‘ 𝑃 ) )
9		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → 𝑋 ∈ 𝐾 )
10	5 3	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐾 )
11	10	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → 0 ∈ 𝐾 )
12		f1fveq	⊢ ( ( 𝐴 : 𝐾 –1-1→ ( Base ‘ 𝑃 ) ∧ ( 𝑋 ∈ 𝐾 ∧ 0 ∈ 𝐾 ) ) → ( ( 𝐴 ‘ 𝑋 ) = ( 𝐴 ‘ 0 ) ↔ 𝑋 = 0 ) )
13	8 9 11 12	syl12anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑋 ) = ( 𝐴 ‘ 0 ) ↔ 𝑋 = 0 ) )
14	13	biimpd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑋 ) = ( 𝐴 ‘ 0 ) → 𝑋 = 0 ) )
15	14	necon3d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 ≠ 0 → ( 𝐴 ‘ 𝑋 ) ≠ ( 𝐴 ‘ 0 ) ) )
16	15	3impia	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( 𝐴 ‘ 𝑋 ) ≠ ( 𝐴 ‘ 0 ) )
17	1 2 3 4	ply1scl0	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 0 ) = 𝑌 )
18	17	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( 𝐴 ‘ 0 ) = 𝑌 )
19	16 18	neeqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑋 ≠ 0 ) → ( 𝐴 ‘ 𝑋 ) ≠ 𝑌 )