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 ⊢ K = Base R
cply1coe0.0 ⊢ 0 ˙ = 0 R
cply1coe0.p ⊢ P = Poly 1 ⁡ R
cply1coe0.b ⊢ B = Base P
cply1coe0.a ⊢ A = algSc ⁡ P
Assertion cply1coe0 ⊢ R ∈ Ring ∧ S ∈ K → ∀ n ∈ ℕ coe 1 ⁡ A ⁡ S ⁡ n = 0 ˙

Proof

Step Hyp Ref Expression
1 cply1coe0.k ⊢ K = Base R
2 cply1coe0.0 ⊢ 0 ˙ = 0 R
3 cply1coe0.p ⊢ P = Poly 1 ⁡ R
4 cply1coe0.b ⊢ B = Base P
5 cply1coe0.a ⊢ A = algSc ⁡ P
6 3 5 1 2 coe1scl ⊢ R ∈ Ring ∧ S ∈ K → coe 1 ⁡ A ⁡ S = k ∈ ℕ 0 ⟼ if k = 0 S 0 ˙
7 6 adantr ⊢ R ∈ Ring ∧ S ∈ K ∧ n ∈ ℕ → coe 1 ⁡ A ⁡ S = k ∈ ℕ 0 ⟼ if k = 0 S 0 ˙
8 nnne0 ⊢ n ∈ ℕ → n ≠ 0
9 8 neneqd ⊢ n ∈ ℕ → ¬ n = 0
10 9 adantl ⊢ R ∈ Ring ∧ S ∈ K ∧ n ∈ ℕ → ¬ n = 0
11 10 adantr ⊢ R ∈ Ring ∧ S ∈ K ∧ n ∈ ℕ ∧ k = n → ¬ n = 0
12 eqeq1 ⊢ k = n → k = 0 ↔ n = 0
13 12 notbid ⊢ k = n → ¬ k = 0 ↔ ¬ n = 0
14 13 adantl ⊢ R ∈ Ring ∧ S ∈ K ∧ n ∈ ℕ ∧ k = n → ¬ k = 0 ↔ ¬ n = 0
15 11 14 mpbird ⊢ R ∈ Ring ∧ S ∈ K ∧ n ∈ ℕ ∧ k = n → ¬ k = 0
16 15 iffalsed ⊢ R ∈ Ring ∧ S ∈ K ∧ n ∈ ℕ ∧ k = n → if k = 0 S 0 ˙ = 0 ˙
17 nnnn0 ⊢ n ∈ ℕ → n ∈ ℕ 0
18 17 adantl ⊢ R ∈ Ring ∧ S ∈ K ∧ n ∈ ℕ → n ∈ ℕ 0
19 2 fvexi ⊢ 0 ˙ ∈ V
20 19 a1i ⊢ R ∈ Ring ∧ S ∈ K ∧ n ∈ ℕ → 0 ˙ ∈ V
21 7 16 18 20 fvmptd ⊢ R ∈ Ring ∧ S ∈ K ∧ n ∈ ℕ → coe 1 ⁡ A ⁡ S ⁡ n = 0 ˙
22 21 ralrimiva ⊢ R ∈ Ring ∧ S ∈ K → ∀ n ∈ ℕ coe 1 ⁡ A ⁡ S ⁡ n = 0 ˙