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 )