ply10s0

Description: Zero times a univariate polynomial is the zero polynomial ( lmod0vs analog.) (Contributed by AV, 2-Dec-2019)

	Ref	Expression
Hypotheses	ply10s0.p	$⊢ P = {Poly}_{1} (R)$
	ply10s0.b	$⊢ B = {Base}_{P}$
	ply10s0.m	$⊢ \underset{˙}{*} = \cdot_{P}$
	ply10s0.e	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	ply10s0	$⊢ (R \in Ring \land M \in B) \to \underset{˙}{0} \underset{˙}{*} M = 0_{P}$

Step	Hyp	Ref	Expression
1		ply10s0.p	$⊢ P = {Poly}_{1} (R)$
2		ply10s0.b	$⊢ B = {Base}_{P}$
3		ply10s0.m	$⊢ \underset{˙}{*} = \cdot_{P}$
4		ply10s0.e	$⊢ \underset{˙}{0} = 0_{R}$
5	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
6	5	adantr	$⊢ (R \in Ring \land M \in B) \to R = Scalar (P)$
7	6	fveq2d	$⊢ (R \in Ring \land M \in B) \to 0_{R} = 0_{Scalar (P)}$
8	4 7	eqtrid	$⊢ (R \in Ring \land M \in B) \to \underset{˙}{0} = 0_{Scalar (P)}$
9	8	oveq1d	$⊢ (R \in Ring \land M \in B) \to \underset{˙}{0} \underset{˙}{} M = 0_{Scalar (P)} \underset{˙}{} M$
10	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
11		eqid	$⊢ Scalar (P) = Scalar (P)$
12		eqid	$⊢ 0_{Scalar (P)} = 0_{Scalar (P)}$
13		eqid	$⊢ 0_{P} = 0_{P}$
14	2 11 3 12 13	lmod0vs	$⊢ (P \in LMod \land M \in B) \to 0_{Scalar (P)} \underset{˙}{*} M = 0_{P}$
15	10 14	sylan	$⊢ (R \in Ring \land M \in B) \to 0_{Scalar (P)} \underset{˙}{*} M = 0_{P}$
16	9 15	eqtrd	$⊢ (R \in Ring \land M \in B) \to \underset{˙}{0} \underset{˙}{*} M = 0_{P}$

Metamath Proof Explorer