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 
|- P = ( Poly1 ` R )
ply1scl.a 
|- A = ( algSc ` P )
ply1sclid.k 
|- K = ( Base ` R )
ply1sclf1.b 
|- B = ( Base ` P )
Assertion ply1sclf1 
|- ( R e. Ring -> A : K -1-1-> B )

Proof

Step Hyp Ref Expression
1 ply1scl.p 
 |-  P = ( Poly1 ` R )
2 ply1scl.a 
 |-  A = ( algSc ` P )
3 ply1sclid.k 
 |-  K = ( Base ` R )
4 ply1sclf1.b 
 |-  B = ( Base ` P )
5 1 2 3 4 ply1sclf 
 |-  ( R e. Ring -> A : K --> B )
6 fveq2 
 |-  ( ( A ` x ) = ( A ` y ) -> ( coe1 ` ( A ` x ) ) = ( coe1 ` ( A ` y ) ) )
7 6 fveq1d 
 |-  ( ( A ` x ) = ( A ` y ) -> ( ( coe1 ` ( A ` x ) ) ` 0 ) = ( ( coe1 ` ( A ` y ) ) ` 0 ) )
8 1 2 3 ply1sclid 
 |-  ( ( R e. Ring /\ x e. K ) -> x = ( ( coe1 ` ( A ` x ) ) ` 0 ) )
9 8 adantrr 
 |-  ( ( R e. Ring /\ ( x e. K /\ y e. K ) ) -> x = ( ( coe1 ` ( A ` x ) ) ` 0 ) )
10 1 2 3 ply1sclid 
 |-  ( ( R e. Ring /\ y e. K ) -> y = ( ( coe1 ` ( A ` y ) ) ` 0 ) )
11 10 adantrl 
 |-  ( ( R e. Ring /\ ( x e. K /\ y e. K ) ) -> y = ( ( coe1 ` ( A ` y ) ) ` 0 ) )
12 9 11 eqeq12d 
 |-  ( ( R e. Ring /\ ( x e. K /\ y e. K ) ) -> ( x = y <-> ( ( coe1 ` ( A ` x ) ) ` 0 ) = ( ( coe1 ` ( A ` y ) ) ` 0 ) ) )
13 7 12 imbitrrid 
 |-  ( ( R e. Ring /\ ( x e. K /\ y e. K ) ) -> ( ( A ` x ) = ( A ` y ) -> x = y ) )
14 13 ralrimivva 
 |-  ( R e. Ring -> A. x e. K A. y e. K ( ( A ` x ) = ( A ` y ) -> x = y ) )
15 dff13 
 |-  ( A : K -1-1-> B <-> ( A : K --> B /\ A. x e. K A. y e. K ( ( A ` x ) = ( A ` y ) -> x = y ) ) )
16 5 14 15 sylanbrc 
 |-  ( R e. Ring -> A : K -1-1-> B )