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

Metamath Proof Explorer

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