ply1ass23l

Description: Associative identity with scalar and ring multiplication for the polynomial ring. (Contributed by AV, 14-Aug-2019)

	Ref	Expression
Hypotheses	ply1ass23l.p	$⊢ P = {Poly}_{1} (R)$
	ply1ass23l.t	$⊢ \underset{˙}{\times} = \cdot_{P}$
	ply1ass23l.b	$⊢ B = {Base}_{P}$
	ply1ass23l.k	$⊢ K = {Base}_{R}$
	ply1ass23l.n	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
Assertion	ply1ass23l	$⊢ (R \in Ring \land (A \in K \land X \in B \land Y \in B)) \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} Y = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$

Proof

Step	Hyp	Ref	Expression
1		ply1ass23l.p	$⊢ P = {Poly}_{1} (R)$
2		ply1ass23l.t	$⊢ \underset{˙}{\times} = \cdot_{P}$
3		ply1ass23l.b	$⊢ B = {Base}_{P}$
4		ply1ass23l.k	$⊢ K = {Base}_{R}$
5		ply1ass23l.n	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		eqid	$⊢ 1_{𝑜} mPwSer R = 1_{𝑜} mPwSer R$
7		1on	$⊢ 1_{𝑜} \in On$
8	7	a1i	$⊢ (R \in Ring \land (A \in K \land X \in B \land Y \in B)) \to 1_{𝑜} \in On$
9		simpl	$⊢ (R \in Ring \land (A \in K \land X \in B \land Y \in B)) \to R \in Ring$
10		eqid	$⊢ \{f \in ({ℕ_{0}}^{1_{𝑜}}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{1_{𝑜}}) \| f^{-1} [ℕ] \in Fin\}$
11		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
12	1 11 2	ply1mulr	$⊢ \underset{˙}{\times} = \cdot_{(1_{𝑜} mPoly R)}$
13	11 6 12	mplmulr	$⊢ \underset{˙}{\times} = \cdot_{(1_{𝑜} mPwSer R)}$
14		eqid	$⊢ {Base}_{(1_{𝑜} mPwSer R)} = {Base}_{(1_{𝑜} mPwSer R)}$
15		eqid	$⊢ {Base}_{(1_{𝑜} mPoly R)} = {Base}_{(1_{𝑜} mPoly R)}$
16	11 6 15 14	mplbasss	$⊢ {Base}_{(1_{𝑜} mPoly R)} \subseteq {Base}_{(1_{𝑜} mPwSer R)}$
17	1 3	ply1bascl2	$⊢ X \in B \to X \in {Base}_{(1_{𝑜} mPoly R)}$
18	16 17	sselid	$⊢ X \in B \to X \in {Base}_{(1_{𝑜} mPwSer R)}$
19	18	3ad2ant2	$⊢ (A \in K \land X \in B \land Y \in B) \to X \in {Base}_{(1_{𝑜} mPwSer R)}$
20	19	adantl	$⊢ (R \in Ring \land (A \in K \land X \in B \land Y \in B)) \to X \in {Base}_{(1_{𝑜} mPwSer R)}$
21	1 3	ply1bascl2	$⊢ Y \in B \to Y \in {Base}_{(1_{𝑜} mPoly R)}$
22	16 21	sselid	$⊢ Y \in B \to Y \in {Base}_{(1_{𝑜} mPwSer R)}$
23	22	3ad2ant3	$⊢ (A \in K \land X \in B \land Y \in B) \to Y \in {Base}_{(1_{𝑜} mPwSer R)}$
24	23	adantl	$⊢ (R \in Ring \land (A \in K \land X \in B \land Y \in B)) \to Y \in {Base}_{(1_{𝑜} mPwSer R)}$
25	1 11 5	ply1vsca	$⊢ \underset{˙}{\cdot} = \cdot_{(1_{𝑜} mPoly R)}$
26	11 6 25	mplvsca2	$⊢ \underset{˙}{\cdot} = \cdot_{(1_{𝑜} mPwSer R)}$
27		simpr1	$⊢ (R \in Ring \land (A \in K \land X \in B \land Y \in B)) \to A \in K$
28	6 8 9 10 13 14 20 24 4 26 27	psrass23l	$⊢ (R \in Ring \land (A \in K \land X \in B \land Y \in B)) \to (A \underset{˙}{\cdot} X) \underset{˙}{\times} Y = A \underset{˙}{\cdot} (X \underset{˙}{\times} Y)$

Metamath Proof Explorer

Theorem ply1ass23l

Proof