Theorem coe1mon

Description: Coefficient vector of a monomial. (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	ply1moneq.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1moneq.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	ply1moneq.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	coe1mon.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	coe1mon.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	coe1mon.0	⊢ 0 = ( 0g ‘ 𝑅 )
	coe1mon.1	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	coe1mon	⊢ ( 𝜑 → ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝑁 , 1 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1moneq.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1moneq.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		ply1moneq.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
4		coe1mon.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		coe1mon.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		coe1mon.0	⊢ 0 = ( 0g ‘ 𝑅 )
7		coe1mon.1	⊢ 1 = ( 1r ‘ 𝑅 )
8	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
9	4 8	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
10	9	fveq2d	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
11	7 10	eqtrid	⊢ ( 𝜑 → 1 = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
12	11	oveq1d	⊢ ( 𝜑 → ( 1 ( ·𝑠 ‘ 𝑃 ) ( 𝑁 ↑ 𝑋 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑁 ↑ 𝑋 ) ) )
13	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
14	4 13	syl	⊢ ( 𝜑 → 𝑃 ∈ LMod )
15		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
16		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
17	1 2 15 3 16	ply1moncl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
18	4 5 17	syl2anc	⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
19		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
20		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
21		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
22	16 19 20 21	lmodvs1	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑁 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑁 ↑ 𝑋 ) ) = ( 𝑁 ↑ 𝑋 ) )
23	14 18 22	syl2anc	⊢ ( 𝜑 → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑁 ↑ 𝑋 ) ) = ( 𝑁 ↑ 𝑋 ) )
24	12 23	eqtrd	⊢ ( 𝜑 → ( 1 ( ·𝑠 ‘ 𝑃 ) ( 𝑁 ↑ 𝑋 ) ) = ( 𝑁 ↑ 𝑋 ) )
25	24	fveq2d	⊢ ( 𝜑 → ( coe1 ‘ ( 1 ( ·𝑠 ‘ 𝑃 ) ( 𝑁 ↑ 𝑋 ) ) ) = ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) ) )
26		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27	26 7	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
28	4 27	syl	⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝑅 ) )
29	6 26 1 2 20 15 3	coe1tm	⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ ( Base ‘ 𝑅 ) ∧ 𝑁 ∈ ℕ0 ) → ( coe1 ‘ ( 1 ( ·𝑠 ‘ 𝑃 ) ( 𝑁 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝑁 , 1 , 0 ) ) )
30	4 28 5 29	syl3anc	⊢ ( 𝜑 → ( coe1 ‘ ( 1 ( ·𝑠 ‘ 𝑃 ) ( 𝑁 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝑁 , 1 , 0 ) ) )
31	25 30	eqtr3d	⊢ ( 𝜑 → ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝑁 , 1 , 0 ) ) )