evl1vsd

Description: Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	evl1addd.q	$⊢ O = {eval}_{1} (R)$
	evl1addd.p	$⊢ P = {Poly}_{1} (R)$
	evl1addd.b	$⊢ B = {Base}_{R}$
	evl1addd.u	$⊢ U = {Base}_{P}$
	evl1addd.1	$⊢ φ \to R \in CRing$
	evl1addd.2	$⊢ φ \to Y \in B$
	evl1addd.3	$⊢ φ \to (M \in U \land O (M) (Y) = V)$
	evl1vsd.4	$⊢ φ \to N \in B$
	evl1vsd.s	$⊢ \underset{˙}{∙} = \cdot_{P}$
	evl1vsd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	evl1vsd	$⊢ φ \to (N \underset{˙}{∙} M \in U \land O (N \underset{˙}{∙} M) (Y) = N \underset{˙}{\cdot} V)$

Proof

Step	Hyp	Ref	Expression
1		evl1addd.q	$⊢ O = {eval}_{1} (R)$
2		evl1addd.p	$⊢ P = {Poly}_{1} (R)$
3		evl1addd.b	$⊢ B = {Base}_{R}$
4		evl1addd.u	$⊢ U = {Base}_{P}$
5		evl1addd.1	$⊢ φ \to R \in CRing$
6		evl1addd.2	$⊢ φ \to Y \in B$
7		evl1addd.3	$⊢ φ \to (M \in U \land O (M) (Y) = V)$
8		evl1vsd.4	$⊢ φ \to N \in B$
9		evl1vsd.s	$⊢ \underset{˙}{∙} = \cdot_{P}$
10		evl1vsd.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
11		eqid	$⊢ algSc (P) = algSc (P)$
12	1 2 3 11 4 5 8 6	evl1scad	$⊢ φ \to (algSc (P) (N) \in U \land O (algSc (P) (N)) (Y) = N)$
13		eqid	$⊢ \cdot_{P} = \cdot_{P}$
14	1 2 3 4 5 6 12 7 13 10	evl1muld	$⊢ φ \to (algSc (P) (N) \cdot_{P} M \in U \land O (algSc (P) (N) \cdot_{P} M) (Y) = N \underset{˙}{\cdot} V)$
15	2	ply1assa	$⊢ R \in CRing \to P \in AssAlg$
16	5 15	syl	$⊢ φ \to P \in AssAlg$
17	2	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
18	5 17	syl	$⊢ φ \to R = Scalar (P)$
19	18	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (P)}$
20	3 19	eqtrid	$⊢ φ \to B = {Base}_{Scalar (P)}$
21	8 20	eleqtrd	$⊢ φ \to N \in {Base}_{Scalar (P)}$
22	7	simpld	$⊢ φ \to M \in U$
23		eqid	$⊢ Scalar (P) = Scalar (P)$
24		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
25	11 23 24 4 13 9	asclmul1	$⊢ (P \in AssAlg \land N \in {Base}_{Scalar (P)} \land M \in U) \to algSc (P) (N) \cdot_{P} M = N \underset{˙}{∙} M$
26	16 21 22 25	syl3anc	$⊢ φ \to algSc (P) (N) \cdot_{P} M = N \underset{˙}{∙} M$
27	26	eleq1d	$⊢ φ \to (algSc (P) (N) \cdot_{P} M \in U \leftrightarrow N \underset{˙}{∙} M \in U)$
28	26	fveq2d	$⊢ φ \to O (algSc (P) (N) \cdot_{P} M) = O (N \underset{˙}{∙} M)$
29	28	fveq1d	$⊢ φ \to O (algSc (P) (N) \cdot_{P} M) (Y) = O (N \underset{˙}{∙} M) (Y)$
30	29	eqeq1d	$⊢ φ \to (O (algSc (P) (N) \cdot_{P} M) (Y) = N \underset{˙}{\cdot} V \leftrightarrow O (N \underset{˙}{∙} M) (Y) = N \underset{˙}{\cdot} V)$
31	27 30	anbi12d	$⊢ φ \to ((algSc (P) (N) \cdot_{P} M \in U \land O (algSc (P) (N) \cdot_{P} M) (Y) = N \underset{˙}{\cdot} V) \leftrightarrow (N \underset{˙}{∙} M \in U \land O (N \underset{˙}{∙} M) (Y) = N \underset{˙}{\cdot} V))$
32	14 31	mpbid	$⊢ φ \to (N \underset{˙}{∙} M \in U \land O (N \underset{˙}{∙} M) (Y) = N \underset{˙}{\cdot} V)$

Metamath Proof Explorer

Theorem evl1vsd

Proof