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 ) ) )