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 syl5ibr
 |-  ( ( 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 )