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