This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 sselid ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( 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 sselid ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( 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 ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐴 · 𝑋 ) × 𝑌 ) = ( 𝐴 · ( 𝑋 × 𝑌 ) ) )