ply1sclrmsm

Description: The ring multiplication of a polynomial with a scalar polynomial is equal to the scalar multiplication of the polynomial with the corresponding scalar. (Contributed by AV, 14-Aug-2019)

	Ref	Expression
Hypotheses	ply1sclrmsm.k	$⊢ K = {Base}_{R}$
	ply1sclrmsm.p	$⊢ P = {Poly}_{1} (R)$
	ply1sclrmsm.b	$⊢ E = {Base}_{P}$
	ply1sclrmsm.x	$⊢ X = {var}_{1} (R)$
	ply1sclrmsm.s	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	ply1sclrmsm.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
	ply1sclrmsm.n	$⊢ N = {mulGrp}_{P}$
	ply1sclrmsm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
	ply1sclrmsm.a	$⊢ A = algSc (P)$
Assertion	ply1sclrmsm	$⊢ (R \in Ring \land F \in K \land Z \in E) \to A (F) \underset{˙}{\times} Z = F \underset{˙}{\cdot} Z$

Proof

Step	Hyp	Ref	Expression
1		ply1sclrmsm.k	$⊢ K = {Base}_{R}$
2		ply1sclrmsm.p	$⊢ P = {Poly}_{1} (R)$
3		ply1sclrmsm.b	$⊢ E = {Base}_{P}$
4		ply1sclrmsm.x	$⊢ X = {var}_{1} (R)$
5		ply1sclrmsm.s	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		ply1sclrmsm.m	$⊢ \underset{˙}{\times} = \cdot_{P}$
7		ply1sclrmsm.n	$⊢ N = {mulGrp}_{P}$
8		ply1sclrmsm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
9		ply1sclrmsm.a	$⊢ A = algSc (P)$
10	2	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
11	10	fveq2d	$⊢ R \in Ring \to {Base}_{R} = {Base}_{Scalar (P)}$
12	1 11	eqtrid	$⊢ R \in Ring \to K = {Base}_{Scalar (P)}$
13	12	eleq2d	$⊢ R \in Ring \to (F \in K \leftrightarrow F \in {Base}_{Scalar (P)})$
14	13	biimpa	$⊢ (R \in Ring \land F \in K) \to F \in {Base}_{Scalar (P)}$
15		eqid	$⊢ Scalar (P) = Scalar (P)$
16		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
17		eqid	$⊢ 1_{P} = 1_{P}$
18	9 15 16 5 17	asclval	$⊢ F \in {Base}_{Scalar (P)} \to A (F) = F \underset{˙}{\cdot} 1_{P}$
19	14 18	syl	$⊢ (R \in Ring \land F \in K) \to A (F) = F \underset{˙}{\cdot} 1_{P}$
20	19	3adant3	$⊢ (R \in Ring \land F \in K \land Z \in E) \to A (F) = F \underset{˙}{\cdot} 1_{P}$
21	20	oveq1d	$⊢ (R \in Ring \land F \in K \land Z \in E) \to A (F) \underset{˙}{\times} Z = (F \underset{˙}{\cdot} 1_{P}) \underset{˙}{\times} Z$
22		simp1	$⊢ (R \in Ring \land F \in K \land Z \in E) \to R \in Ring$
23	1	eleq2i	$⊢ F \in K \leftrightarrow F \in {Base}_{R}$
24	23	biimpi	$⊢ F \in K \to F \in {Base}_{R}$
25	24	3ad2ant2	$⊢ (R \in Ring \land F \in K \land Z \in E) \to F \in {Base}_{R}$
26	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
27	3 17	ringidcl	$⊢ P \in Ring \to 1_{P} \in E$
28	26 27	syl	$⊢ R \in Ring \to 1_{P} \in E$
29	28	3ad2ant1	$⊢ (R \in Ring \land F \in K \land Z \in E) \to 1_{P} \in E$
30		simp3	$⊢ (R \in Ring \land F \in K \land Z \in E) \to Z \in E$
31		eqid	$⊢ {Base}_{R} = {Base}_{R}$
32	2 6 3 31 5	ply1ass23l	$⊢ (R \in Ring \land (F \in {Base}_{R} \land 1_{P} \in E \land Z \in E)) \to (F \underset{˙}{\cdot} 1_{P}) \underset{˙}{\times} Z = F \underset{˙}{\cdot} (1_{P} \underset{˙}{\times} Z)$
33	22 25 29 30 32	syl13anc	$⊢ (R \in Ring \land F \in K \land Z \in E) \to (F \underset{˙}{\cdot} 1_{P}) \underset{˙}{\times} Z = F \underset{˙}{\cdot} (1_{P} \underset{˙}{\times} Z)$
34	3 6 17	ringlidm	$⊢ (P \in Ring \land Z \in E) \to 1_{P} \underset{˙}{\times} Z = Z$
35	26 34	sylan	$⊢ (R \in Ring \land Z \in E) \to 1_{P} \underset{˙}{\times} Z = Z$
36	35	3adant2	$⊢ (R \in Ring \land F \in K \land Z \in E) \to 1_{P} \underset{˙}{\times} Z = Z$
37	36	oveq2d	$⊢ (R \in Ring \land F \in K \land Z \in E) \to F \underset{˙}{\cdot} (1_{P} \underset{˙}{\times} Z) = F \underset{˙}{\cdot} Z$
38	21 33 37	3eqtrd	$⊢ (R \in Ring \land F \in K \land Z \in E) \to A (F) \underset{˙}{\times} Z = F \underset{˙}{\cdot} Z$

Metamath Proof Explorer

Theorem ply1sclrmsm

Proof