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

Metamath Proof Explorer

Theorem ply1sclf1

Description: The polynomial scalar function is injective. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses ply1scl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1scl.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
ply1sclid.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
ply1sclf1.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion ply1sclf1 ( 𝑅 ∈ Ring → 𝐴 : 𝐾 –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 ply1scl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1scl.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
3 ply1sclid.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 ply1sclf1.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
5 1 2 3 4 ply1sclf ⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐾 ⟶ 𝐵 )
6 fveq2 ⊢ ( ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) → ( coe1 ‘ ( 𝐴 ‘ 𝑥 ) ) = ( coe1 ‘ ( 𝐴 ‘ 𝑦 ) ) )
7 6 fveq1d ⊢ ( ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) → ( ( coe1 ‘ ( 𝐴 ‘ 𝑥 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝑦 ) ) ‘ 0 ) )
8 1 2 3 ply1sclid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐾 ) → 𝑥 = ( ( coe1 ‘ ( 𝐴 ‘ 𝑥 ) ) ‘ 0 ) )
9 8 adantrr ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑥 = ( ( coe1 ‘ ( 𝐴 ‘ 𝑥 ) ) ‘ 0 ) )
10 1 2 3 ply1sclid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ) → 𝑦 = ( ( coe1 ‘ ( 𝐴 ‘ 𝑦 ) ) ‘ 0 ) )
11 10 adantrl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑦 = ( ( coe1 ‘ ( 𝐴 ‘ 𝑦 ) ) ‘ 0 ) )
12 9 11 eqeq12d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 = 𝑦 ↔ ( ( coe1 ‘ ( 𝐴 ‘ 𝑥 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝑦 ) ) ‘ 0 ) ) )
13 7 12 imbitrrid ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
14 13 ralrimivva ⊢ ( 𝑅 ∈ Ring → ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
15 dff13 ⊢ ( 𝐴 : 𝐾 –1-1→ 𝐵 ↔ ( 𝐴 : 𝐾 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
16 5 14 15 sylanbrc ⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐾 –1-1→ 𝐵 )