Theorem evl1vard

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

	Ref	Expression
Hypotheses	evl1var.q	|- O = ( eval1 ` R )
	evl1var.v	|- X = ( var1 ` R )
	evl1var.b	|- B = ( Base ` R )
	evl1vard.p	|- P = ( Poly1 ` R )
	evl1vard.u	|- U = ( Base ` P )
	evl1vard.1	|- ( ph -> R e. CRing )
	evl1vard.2	|- ( ph -> Y e. B )
Assertion	evl1vard	|- ( ph -> ( X e. U /\ ( ( O ` X ) ` Y ) = Y ) )

Proof

Step	Hyp	Ref	Expression
1		evl1var.q	|- O = ( eval1 ` R )
2		evl1var.v	|- X = ( var1 ` R )
3		evl1var.b	|- B = ( Base ` R )
4		evl1vard.p	|- P = ( Poly1 ` R )
5		evl1vard.u	|- U = ( Base ` P )
6		evl1vard.1	|- ( ph -> R e. CRing )
7		evl1vard.2	|- ( ph -> Y e. B )
8		crngring	|- ( R e. CRing -> R e. Ring )
9	2 4 5	vr1cl	|- ( R e. Ring -> X e. U )
10	6 8 9	3syl	|- ( ph -> X e. U )
11	1 2 3	evl1var	|- ( R e. CRing -> ( O ` X ) = ( _I |` B ) )
12	6 11	syl	|- ( ph -> ( O ` X ) = ( _I |` B ) )
13	12	fveq1d	|- ( ph -> ( ( O ` X ) ` Y ) = ( ( _I |` B ) ` Y ) )
14		fvresi	|- ( Y e. B -> ( ( _I |` B ) ` Y ) = Y )
15	7 14	syl	|- ( ph -> ( ( _I |` B ) ` Y ) = Y )
16	13 15	eqtrd	|- ( ph -> ( ( O ` X ) ` Y ) = Y )
17	10 16	jca	|- ( ph -> ( X e. U /\ ( ( O ` X ) ` Y ) = Y ) )