Theorem coe1vr1

Description: Polynomial coefficient of the variable. (Contributed by Thierry Arnoux, 22-Jun-2025)

	Ref	Expression
Hypotheses	coe1vr1.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	coe1vr1.2	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	coe1vr1.3	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	coe1vr1.4	⊢ 0 = ( 0g ‘ 𝑅 )
	coe1vr1.5	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	coe1vr1	⊢ ( 𝜑 → ( coe1 ‘ 𝑋 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 1 , 1 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1vr1.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		coe1vr1.2	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		coe1vr1.3	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		coe1vr1.4	⊢ 0 = ( 0g ‘ 𝑅 )
5		coe1vr1.5	⊢ 1 = ( 1r ‘ 𝑅 )
6		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
7	2 1 6	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
8		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
9	8 6	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
10		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
11	9 10	mulg1	⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) = 𝑋 )
12	3 7 11	3syl	⊢ ( 𝜑 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) = 𝑋 )
13	12	fveq2d	⊢ ( 𝜑 → ( coe1 ‘ ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = ( coe1 ‘ 𝑋 ) )
14		1nn0	⊢ 1 ∈ ℕ0
15	14	a1i	⊢ ( 𝜑 → 1 ∈ ℕ0 )
16	1 2 10 3 15 4 5	coe1mon	⊢ ( 𝜑 → ( coe1 ‘ ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 1 , 1 , 0 ) ) )
17	13 16	eqtr3d	⊢ ( 𝜑 → ( coe1 ‘ 𝑋 ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 1 , 1 , 0 ) ) )