Theorem evl1scad

Description: Polynomial evaluation builder for scalars. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	evl1sca.o	|- O = ( eval1 ` R )
	evl1sca.p	|- P = ( Poly1 ` R )
	evl1sca.b	|- B = ( Base ` R )
	evl1sca.a	|- A = ( algSc ` P )
	evl1scad.u	|- U = ( Base ` P )
	evl1scad.1	|- ( ph -> R e. CRing )
	evl1scad.2	|- ( ph -> X e. B )
	evl1scad.3	|- ( ph -> Y e. B )
Assertion	evl1scad	|- ( ph -> ( ( A ` X ) e. U /\ ( ( O ` ( A ` X ) ) ` Y ) = X ) )

Proof

Step	Hyp	Ref	Expression
1		evl1sca.o	|- O = ( eval1 ` R )
2		evl1sca.p	|- P = ( Poly1 ` R )
3		evl1sca.b	|- B = ( Base ` R )
4		evl1sca.a	|- A = ( algSc ` P )
5		evl1scad.u	|- U = ( Base ` P )
6		evl1scad.1	|- ( ph -> R e. CRing )
7		evl1scad.2	|- ( ph -> X e. B )
8		evl1scad.3	|- ( ph -> Y e. B )
9		crngring	|- ( R e. CRing -> R e. Ring )
10	2 4 3 5	ply1sclf	|- ( R e. Ring -> A : B --> U )
11	6 9 10	3syl	|- ( ph -> A : B --> U )
12	11 7	ffvelrnd	|- ( ph -> ( A ` X ) e. U )
13	1 2 3 4	evl1sca	|- ( ( R e. CRing /\ X e. B ) -> ( O ` ( A ` X ) ) = ( B X. { X } ) )
14	6 7 13	syl2anc	|- ( ph -> ( O ` ( A ` X ) ) = ( B X. { X } ) )
15	14	fveq1d	|- ( ph -> ( ( O ` ( A ` X ) ) ` Y ) = ( ( B X. { X } ) ` Y ) )
16		fvconst2g	|- ( ( X e. B /\ Y e. B ) -> ( ( B X. { X } ) ` Y ) = X )
17	7 8 16	syl2anc	|- ( ph -> ( ( B X. { X } ) ` Y ) = X )
18	15 17	eqtrd	|- ( ph -> ( ( O ` ( A ` X ) ) ` Y ) = X )
19	12 18	jca	|- ( ph -> ( ( A ` X ) e. U /\ ( ( O ` ( A ` X ) ) ` Y ) = X ) )