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

Metamath Proof Explorer

Theorem cply1coe0

Description: All but the first coefficient of a constant polynomial ( i.e. a "lifted scalar") are zero. (Contributed by AV, 16-Nov-2019)

Ref Expression
Hypotheses cply1coe0.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
cply1coe0.0 ⊢ 0 = ( 0g ‘ 𝑅 )
cply1coe0.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cply1coe0.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
cply1coe0.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion cply1coe0 ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) → ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝐴 ‘ 𝑆 ) ) ‘ 𝑛 ) = 0 )

Proof

Step Hyp Ref Expression
1 cply1coe0.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 cply1coe0.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 cply1coe0.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 cply1coe0.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
5 cply1coe0.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
6 3 5 1 2 coe1scl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) → ( coe1 ‘ ( 𝐴 ‘ 𝑆 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , 𝑆 , 0 ) ) )
7 6 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) → ( coe1 ‘ ( 𝐴 ‘ 𝑆 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , 𝑆 , 0 ) ) )
8 nnne0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
9 8 neneqd ⊢ ( 𝑛 ∈ ℕ → ¬ 𝑛 = 0 )
10 9 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) → ¬ 𝑛 = 0 )
11 10 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ¬ 𝑛 = 0 )
12 eqeq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 = 0 ↔ 𝑛 = 0 ) )
13 12 notbid ⊢ ( 𝑘 = 𝑛 → ( ¬ 𝑘 = 0 ↔ ¬ 𝑛 = 0 ) )
14 13 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( ¬ 𝑘 = 0 ↔ ¬ 𝑛 = 0 ) )
15 11 14 mpbird ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ¬ 𝑘 = 0 )
16 15 iffalsed ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → if ( 𝑘 = 0 , 𝑆 , 0 ) = 0 )
17 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
18 17 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
19 2 fvexi ⊢ 0 ∈ V
20 19 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) → 0 ∈ V )
21 7 16 18 20 fvmptd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) → ( ( coe1 ‘ ( 𝐴 ‘ 𝑆 ) ) ‘ 𝑛 ) = 0 )
22 21 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) → ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝐴 ‘ 𝑆 ) ) ‘ 𝑛 ) = 0 )