Theorem ply1ass23l

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

	Ref	Expression
Hypotheses	ply1ass23l.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1ass23l.t	⊢ × = ( .r ‘ 𝑃 )
	ply1ass23l.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1ass23l.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	ply1ass23l.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
Assertion	ply1ass23l	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1ass23l.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1ass23l.t	⊢ × = ( .r ‘ 𝑃 )
3		ply1ass23l.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		ply1ass23l.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5		ply1ass23l.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
6		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
7		1on	⊢ 1o ∈ On
8	7	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 1o ∈ On )
9		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
10		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
11		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
12	1 11 2	ply1mulr	⊢ × = ( .r ‘ ( 1o mPoly 𝑅 ) )
13	11 6 12	mplmulr	⊢ × = ( .r ‘ ( 1o mPwSer 𝑅 ) )
14		eqid	⊢ ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( Base ‘ ( 1o mPwSer 𝑅 ) )
15		eqid	⊢ ( Base ‘ ( 1o mPoly 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
16	11 6 15 14	mplbasss	⊢ ( Base ‘ ( 1o mPoly 𝑅 ) ) ⊆ ( Base ‘ ( 1o mPwSer 𝑅 ) )
17	1 3	ply1bascl2	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
18	16 17	sseldi	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
19	18	3ad2ant2	⊢ ( ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
20	19	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
21	1 3	ply1bascl2	⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
22	16 21	sseldi	⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
23	22	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
24	23	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
25	1 11 5	ply1vsca	⊢ · = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
26	11 6 25	mplvsca2	⊢ · = ( ·𝑠 ‘ ( 1o mPwSer 𝑅 ) )
27		simpr1	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐴 ∈ 𝐾 )
28	6 8 9 10 13 14 20 24 4 26 27	psrass23l	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )