coe1sclmulfv

Description: A single coefficient of a polynomial multiplied on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	coe1sclmul.p	$⊢ P = {Poly}_{1} (R)$
	coe1sclmul.b	$⊢ B = {Base}_{P}$
	coe1sclmul.k	$⊢ K = {Base}_{R}$
	coe1sclmul.a	$⊢ A = algSc (P)$
	coe1sclmul.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
	coe1sclmul.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	coe1sclmulfv	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \to {coe}_{1} (A (X) \underset{˙}{∙} Y) (\underset{˙}{0}) = X \underset{˙}{\cdot} {coe}_{1} (Y) (\underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		coe1sclmul.p	$⊢ P = {Poly}_{1} (R)$
2		coe1sclmul.b	$⊢ B = {Base}_{P}$
3		coe1sclmul.k	$⊢ K = {Base}_{R}$
4		coe1sclmul.a	$⊢ A = algSc (P)$
5		coe1sclmul.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
6		coe1sclmul.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
7	1 2 3 4 5 6	coe1sclmul	$⊢ (R \in Ring \land X \in K \land Y \in B) \to {coe}_{1} (A (X) \underset{˙}{∙} Y) = (ℕ_{0} \times \{X\}) {\underset{˙}{\cdot}}_{f} {coe}_{1} (Y)$
8	7	3expb	$⊢ (R \in Ring \land (X \in K \land Y \in B)) \to {coe}_{1} (A (X) \underset{˙}{∙} Y) = (ℕ_{0} \times \{X\}) {\underset{˙}{\cdot}}_{f} {coe}_{1} (Y)$
9	8	3adant3	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \to {coe}_{1} (A (X) \underset{˙}{∙} Y) = (ℕ_{0} \times \{X\}) {\underset{˙}{\cdot}}_{f} {coe}_{1} (Y)$
10	9	fveq1d	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \to {coe}_{1} (A (X) \underset{˙}{∙} Y) (\underset{˙}{0}) = ((ℕ_{0} \times \{X\}) {\underset{˙}{\cdot}}_{f} {coe}_{1} (Y)) (\underset{˙}{0})$
11		simp3	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \to \underset{˙}{0} \in ℕ_{0}$
12		nn0ex	$⊢ ℕ_{0} \in V$
13	12	a1i	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \to ℕ_{0} \in V$
14		simp2l	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \to X \in K$
15		simp2r	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \to Y \in B$
16		eqid	$⊢ {coe}_{1} (Y) = {coe}_{1} (Y)$
17		eqid	$⊢ {Base}_{R} = {Base}_{R}$
18	16 2 1 17	coe1f	$⊢ Y \in B \to {coe}_{1} (Y) : ℕ_{0} ⟶ {Base}_{R}$
19		ffn	$⊢ {coe}_{1} (Y) : ℕ_{0} ⟶ {Base}_{R} \to {coe}_{1} (Y) Fn ℕ_{0}$
20	15 18 19	3syl	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \to {coe}_{1} (Y) Fn ℕ_{0}$
21		eqidd	$⊢ ((R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \land \underset{˙}{0} \in ℕ_{0}) \to {coe}_{1} (Y) (\underset{˙}{0}) = {coe}_{1} (Y) (\underset{˙}{0})$
22	13 14 20 21	ofc1	$⊢ ((R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \land \underset{˙}{0} \in ℕ_{0}) \to ((ℕ_{0} \times \{X\}) {\underset{˙}{\cdot}}_{f} {coe}_{1} (Y)) (\underset{˙}{0}) = X \underset{˙}{\cdot} {coe}_{1} (Y) (\underset{˙}{0})$
23	11 22	mpdan	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \to ((ℕ_{0} \times \{X\}) {\underset{˙}{\cdot}}_{f} {coe}_{1} (Y)) (\underset{˙}{0}) = X \underset{˙}{\cdot} {coe}_{1} (Y) (\underset{˙}{0})$
24	10 23	eqtrd	$⊢ (R \in Ring \land (X \in K \land Y \in B) \land \underset{˙}{0} \in ℕ_{0}) \to {coe}_{1} (A (X) \underset{˙}{∙} Y) (\underset{˙}{0}) = X \underset{˙}{\cdot} {coe}_{1} (Y) (\underset{˙}{0})$

Metamath Proof Explorer

Theorem coe1sclmulfv

Proof