evls1varsrng

Description: The evaluation of the variable of univariate polynomials over subring yields the same result as evaluated as variable of the polynomials over the ring itself. (Contributed by AV, 12-Sep-2019)

	Ref	Expression
Hypotheses	evls1varsrng.q	\|- Q = ( S evalSub1 R )
	evls1varsrng.o	\|- O = ( eval1 ` S )
	evls1varsrng.v	\|- V = ( var1 ` U )
	evls1varsrng.u	\|- U = ( S \|`s R )
	evls1varsrng.b	\|- B = ( Base ` S )
	evls1varsrng.s	\|- ( ph -> S e. CRing )
	evls1varsrng.r	\|- ( ph -> R e. ( SubRing ` S ) )
Assertion	evls1varsrng	\|- ( ph -> ( Q ` V ) = ( O ` V ) )

Proof

Step	Hyp	Ref	Expression
1		evls1varsrng.q	\|- Q = ( S evalSub1 R )
2		evls1varsrng.o	\|- O = ( eval1 ` S )
3		evls1varsrng.v	\|- V = ( var1 ` U )
4		evls1varsrng.u	\|- U = ( S \|`s R )
5		evls1varsrng.b	\|- B = ( Base ` S )
6		evls1varsrng.s	\|- ( ph -> S e. CRing )
7		evls1varsrng.r	\|- ( ph -> R e. ( SubRing ` S ) )
8	1 3 4 5 6 7	evls1var	\|- ( ph -> ( Q ` V ) = ( _I \|` B ) )
9	2 5	evl1fval1	\|- O = ( S evalSub1 B )
10	9	a1i	\|- ( ph -> O = ( S evalSub1 B ) )
11	10	fveq1d	\|- ( ph -> ( O ` V ) = ( ( S evalSub1 B ) ` V ) )
12	3	a1i	\|- ( ph -> V = ( var1 ` U ) )
13		eqid	\|- ( var1 ` S ) = ( var1 ` S )
14	13 7 4	subrgvr1	\|- ( ph -> ( var1 ` S ) = ( var1 ` U ) )
15	5	ressid	\|- ( S e. CRing -> ( S \|`s B ) = S )
16	6 15	syl	\|- ( ph -> ( S \|`s B ) = S )
17	16	eqcomd	\|- ( ph -> S = ( S \|`s B ) )
18	17	fveq2d	\|- ( ph -> ( var1 ` S ) = ( var1 ` ( S \|`s B ) ) )
19	12 14 18	3eqtr2d	\|- ( ph -> V = ( var1 ` ( S \|`s B ) ) )
20	19	fveq2d	\|- ( ph -> ( ( S evalSub1 B ) ` V ) = ( ( S evalSub1 B ) ` ( var1 ` ( S \|`s B ) ) ) )
21		eqid	\|- ( S evalSub1 B ) = ( S evalSub1 B )
22		eqid	\|- ( var1 ` ( S \|`s B ) ) = ( var1 ` ( S \|`s B ) )
23		eqid	\|- ( S \|`s B ) = ( S \|`s B )
24		crngring	\|- ( S e. CRing -> S e. Ring )
25	5	subrgid	\|- ( S e. Ring -> B e. ( SubRing ` S ) )
26	6 24 25	3syl	\|- ( ph -> B e. ( SubRing ` S ) )
27	21 22 23 5 6 26	evls1var	\|- ( ph -> ( ( S evalSub1 B ) ` ( var1 ` ( S \|`s B ) ) ) = ( _I \|` B ) )
28	11 20 27	3eqtrrd	\|- ( ph -> ( _I \|` B ) = ( O ` V ) )
29	8 28	eqtrd	\|- ( ph -> ( Q ` V ) = ( O ` V ) )

Metamath Proof Explorer

Theorem evls1varsrng

Proof