This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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