Theorem coe1scl

Description: Coefficient vector of a scalar. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	ply1scl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1scl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	coe1scl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	coe1scl.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	coe1scl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( coe1 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑋 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1scl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
3		coe1scl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		coe1scl.z	⊢ 0 = ( 0g ‘ 𝑅 )
5		eqid	⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
6		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
7		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
8		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
9	3 1 5 6 7 8 2	ply1scltm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
10	9	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( coe1 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( coe1 ‘ ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
11		0nn0	⊢ 0 ∈ ℕ0
12	4 3 1 5 6 7 8	coe1tm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 0 ∈ ℕ0 ) → ( coe1 ‘ ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑋 , 0 ) ) )
13	11 12	mp3an3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( coe1 ‘ ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑋 , 0 ) ) )
14	10 13	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( coe1 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑋 , 0 ) ) )