Metamath Proof Explorer

Theorem 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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
coe1sclmul.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
coe1sclmul.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
coe1sclmul.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
coe1sclmul.t ⊢ ∙ = ( .r ‘ 𝑃 )
coe1sclmul.u ⊢ · = ( .r ‘ 𝑅 )
Assertion coe1sclmulfv ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) ‘ 0 ) = ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 0 ) ) )

Proof

Step Hyp Ref Expression
1 coe1sclmul.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 coe1sclmul.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 coe1sclmul.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 coe1sclmul.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
5 coe1sclmul.t ⊢ ∙ = ( .r ‘ 𝑃 )
6 coe1sclmul.u ⊢ · = ( .r ‘ 𝑅 )
7 1 2 3 4 5 6 coe1sclmul ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) = ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) )
8 7 3expb ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) = ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) )
9 8 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) = ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) )
10 9 fveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) ‘ 0 ) = ( ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) ‘ 0 ) )
11 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) → 0 ∈ ℕ0 )
12 nn0ex ⊢ ℕ0 ∈ V
13 12 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) → ℕ0 ∈ V )
14 simp2l ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) → 𝑋 ∈ 𝐾 )
15 simp2r ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) → 𝑌 ∈ 𝐵 )
16 eqid ⊢ ( coe1 ‘ 𝑌 ) = ( coe1 ‘ 𝑌 )
17 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18 16 2 1 17 coe1f ⊢ ( 𝑌 ∈ 𝐵 → ( coe1 ‘ 𝑌 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
19 ffn ⊢ ( ( coe1 ‘ 𝑌 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) → ( coe1 ‘ 𝑌 ) Fn ℕ0 )
20 15 18 19 3syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) → ( coe1 ‘ 𝑌 ) Fn ℕ0 )
21 eqidd ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑌 ) ‘ 0 ) = ( ( coe1 ‘ 𝑌 ) ‘ 0 ) )
22 13 14 20 21 ofc1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) ∧ 0 ∈ ℕ0 ) → ( ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) ‘ 0 ) = ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 0 ) ) )
23 11 22 mpdan ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) → ( ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) ‘ 0 ) = ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 0 ) ) )
24 10 23 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) ‘ 0 ) = ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 0 ) ) )