This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → ( 𝐴 ‘ 𝑋 ) ≠ 𝑌 )