Theorem 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	⊢ 𝐾 = ( Base ‘ 𝑅 )
	ply1sclrmsm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1sclrmsm.b	⊢ 𝐸 = ( Base ‘ 𝑃 )
	ply1sclrmsm.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	ply1sclrmsm.s	⊢ · = ( ·𝑠 ‘ 𝑃 )
	ply1sclrmsm.m	⊢ × = ( .r ‘ 𝑃 )
	ply1sclrmsm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
	ply1sclrmsm.e	⊢ ↑ = ( .g ‘ 𝑁 )
	ply1sclrmsm.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion	ply1sclrmsm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸 ) → ( ( 𝐴 ‘ 𝐹 ) × 𝑍 ) = ( 𝐹 · 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1sclrmsm.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
2		ply1sclrmsm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		ply1sclrmsm.b	⊢ 𝐸 = ( Base ‘ 𝑃 )
4		ply1sclrmsm.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
5		ply1sclrmsm.s	⊢ · = ( ·𝑠 ‘ 𝑃 )
6		ply1sclrmsm.m	⊢ × = ( .r ‘ 𝑃 )
7		ply1sclrmsm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
8		ply1sclrmsm.e	⊢ ↑ = ( .g ‘ 𝑁 )
9		ply1sclrmsm.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
10	2	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
11	10	fveq2d	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
12	1 11	syl5eq	⊢ ( 𝑅 ∈ Ring → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
13	12	eleq2d	⊢ ( 𝑅 ∈ Ring → ( 𝐹 ∈ 𝐾 ↔ 𝐹 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
14	13	biimpa	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → 𝐹 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
15		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
16		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
17		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
18	9 15 16 5 17	asclval	⊢ ( 𝐹 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) → ( 𝐴 ‘ 𝐹 ) = ( 𝐹 · ( 1r ‘ 𝑃 ) ) )
19	14 18	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( 𝐴 ‘ 𝐹 ) = ( 𝐹 · ( 1r ‘ 𝑃 ) ) )
20	19	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸 ) → ( 𝐴 ‘ 𝐹 ) = ( 𝐹 · ( 1r ‘ 𝑃 ) ) )
21	20	oveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸 ) → ( ( 𝐴 ‘ 𝐹 ) × 𝑍 ) = ( ( 𝐹 · ( 1r ‘ 𝑃 ) ) × 𝑍 ) )
22		simp1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸 ) → 𝑅 ∈ Ring )
23	1	eleq2i	⊢ ( 𝐹 ∈ 𝐾 ↔ 𝐹 ∈ ( Base ‘ 𝑅 ) )
24	23	biimpi	⊢ ( 𝐹 ∈ 𝐾 → 𝐹 ∈ ( Base ‘ 𝑅 ) )
25	24	3ad2ant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸 ) → 𝐹 ∈ ( Base ‘ 𝑅 ) )
26	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
27	3 17	ringidcl	⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ 𝐸 )
28	26 27	syl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ 𝐸 )
29	28	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸 ) → ( 1r ‘ 𝑃 ) ∈ 𝐸 )
30		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸 ) → 𝑍 ∈ 𝐸 )
31		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
32	2 6 3 31 5	ply1ass23l	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑃 ) ∈ 𝐸 ∧ 𝑍 ∈ 𝐸 ) ) → ( ( 𝐹 · ( 1r ‘ 𝑃 ) ) × 𝑍 ) = ( 𝐹 · ( ( 1r ‘ 𝑃 ) × 𝑍 ) ) )
33	22 25 29 30 32	syl13anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸 ) → ( ( 𝐹 · ( 1r ‘ 𝑃 ) ) × 𝑍 ) = ( 𝐹 · ( ( 1r ‘ 𝑃 ) × 𝑍 ) ) )
34	3 6 17	ringlidm	⊢ ( ( 𝑃 ∈ Ring ∧ 𝑍 ∈ 𝐸 ) → ( ( 1r ‘ 𝑃 ) × 𝑍 ) = 𝑍 )
35	26 34	sylan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐸 ) → ( ( 1r ‘ 𝑃 ) × 𝑍 ) = 𝑍 )
36	35	3adant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸 ) → ( ( 1r ‘ 𝑃 ) × 𝑍 ) = 𝑍 )
37	36	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸 ) → ( 𝐹 · ( ( 1r ‘ 𝑃 ) × 𝑍 ) ) = ( 𝐹 · 𝑍 ) )
38	21 33 37	3eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝑍 ∈ 𝐸 ) → ( ( 𝐴 ‘ 𝐹 ) × 𝑍 ) = ( 𝐹 · 𝑍 ) )