evlsscasrng

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

	Ref	Expression
Hypotheses	evlsscasrng.q	$⊢ Q = (I evalSub S) (R)$
	evlsscasrng.o	$⊢ O = I eval S$
	evlsscasrng.w	$⊢ W = I mPoly U$
	evlsscasrng.u	$⊢ U = S ↾_{𝑠} R$
	evlsscasrng.p	$⊢ P = I mPoly S$
	evlsscasrng.b	$⊢ B = {Base}_{S}$
	evlsscasrng.a	$⊢ A = algSc (W)$
	evlsscasrng.c	$⊢ C = algSc (P)$
	evlsscasrng.i	$⊢ φ \to I \in V$
	evlsscasrng.s	$⊢ φ \to S \in CRing$
	evlsscasrng.r	$⊢ φ \to R \in SubRing (S)$
	evlsscasrng.x	$⊢ φ \to X \in R$
Assertion	evlsscasrng	$⊢ φ \to Q (A (X)) = O (C (X))$

Proof

Step	Hyp	Ref	Expression
1		evlsscasrng.q	$⊢ Q = (I evalSub S) (R)$
2		evlsscasrng.o	$⊢ O = I eval S$
3		evlsscasrng.w	$⊢ W = I mPoly U$
4		evlsscasrng.u	$⊢ U = S ↾_{𝑠} R$
5		evlsscasrng.p	$⊢ P = I mPoly S$
6		evlsscasrng.b	$⊢ B = {Base}_{S}$
7		evlsscasrng.a	$⊢ A = algSc (W)$
8		evlsscasrng.c	$⊢ C = algSc (P)$
9		evlsscasrng.i	$⊢ φ \to I \in V$
10		evlsscasrng.s	$⊢ φ \to S \in CRing$
11		evlsscasrng.r	$⊢ φ \to R \in SubRing (S)$
12		evlsscasrng.x	$⊢ φ \to X \in R$
13	6	ressid	$⊢ S \in CRing \to S ↾_{𝑠} B = S$
14	13	eqcomd	$⊢ S \in CRing \to S = S ↾_{𝑠} B$
15	10 14	syl	$⊢ φ \to S = S ↾_{𝑠} B$
16	15	oveq2d	$⊢ φ \to I mPoly S = I mPoly (S ↾_{𝑠} B)$
17	5 16	syl5eq	$⊢ φ \to P = I mPoly (S ↾_{𝑠} B)$
18	17	fveq2d	$⊢ φ \to algSc (P) = algSc (I mPoly (S ↾_{𝑠} B))$
19	8 18	syl5eq	$⊢ φ \to C = algSc (I mPoly (S ↾_{𝑠} B))$
20	19	fveq1d	$⊢ φ \to C (X) = algSc (I mPoly (S ↾_{𝑠} B)) (X)$
21	20	fveq2d	$⊢ φ \to (I evalSub S) (B) (C (X)) = (I evalSub S) (B) (algSc (I mPoly (S ↾_{𝑠} B)) (X))$
22		eqid	$⊢ (I evalSub S) (B) = (I evalSub S) (B)$
23		eqid	$⊢ I mPoly (S ↾_{𝑠} B) = I mPoly (S ↾_{𝑠} B)$
24		eqid	$⊢ S ↾_{𝑠} B = S ↾_{𝑠} B$
25		eqid	$⊢ algSc (I mPoly (S ↾_{𝑠} B)) = algSc (I mPoly (S ↾_{𝑠} B))$
26		crngring	$⊢ S \in CRing \to S \in Ring$
27	6	subrgid	$⊢ S \in Ring \to B \in SubRing (S)$
28	10 26 27	3syl	$⊢ φ \to B \in SubRing (S)$
29	6	subrgss	$⊢ R \in SubRing (S) \to R \subseteq B$
30	11 29	syl	$⊢ φ \to R \subseteq B$
31	30 12	sseldd	$⊢ φ \to X \in B$
32	22 23 24 6 25 9 10 28 31	evlssca	$⊢ φ \to (I evalSub S) (B) (algSc (I mPoly (S ↾_{𝑠} B)) (X)) = (B^{I}) \times \{X\}$
33	21 32	eqtrd	$⊢ φ \to (I evalSub S) (B) (C (X)) = (B^{I}) \times \{X\}$
34	2 6	evlval	$⊢ O = (I evalSub S) (B)$
35	34	a1i	$⊢ φ \to O = (I evalSub S) (B)$
36	35	fveq1d	$⊢ φ \to O (C (X)) = (I evalSub S) (B) (C (X))$
37	1 3 4 6 7 9 10 11 12	evlssca	$⊢ φ \to Q (A (X)) = (B^{I}) \times \{X\}$
38	33 36 37	3eqtr4rd	$⊢ φ \to Q (A (X)) = O (C (X))$

Metamath Proof Explorer

Theorem evlsscasrng

Proof