English
Let φ be as above and suppose a ∈ A satisfies a φ(id_s) = 0 and a φ(star(id_s)) = 0. Then for every f, a φ(f) = 0.
Русский
Пусть φ — как выше, и a ∈ A удовлетворяет a φ(id_s) = 0 и a φ(star(id_s)) = 0. Тогда для любого f выполняется a φ(f) = 0.
LaTeX
$$$\forall s,\, (0 \in s) \Rightarrow \forall φ: C(s, \mathbb{K})_{0} \to_{\ast n a}[\mathbb{K}] A,\; a,\; a \star\! φ(\mathrm{id}_s) = 0 \land a φ(\mathrm{id}_s) = 0 \Rightarrow \forall f \in C(s, \mathbb{K})_{0},\; a \ φ(f) = 0.$$$
Lean4
theorem mul_nonUnitalStarAlgHom_apply_eq_zero {𝕜 A : Type*} [RCLike 𝕜] [NonUnitalSemiring A] [Star A]
[TopologicalSpace A] [ContinuousMul A] [T2Space A] [DistribMulAction 𝕜 A] [SMulCommClass 𝕜 A A] {s : Set 𝕜}
[Fact (0 ∈ s)] [CompactSpace s] (φ : C(s, 𝕜)₀ →⋆ₙₐ[𝕜] A) (a : A) (hmul_id : a * φ (.id s) = 0)
(hmul_star_id : a * φ (star (.id s)) = 0) (hφ : Continuous φ) (f : C(s, 𝕜)₀) : a * φ f = 0 := by
induction f using ContinuousMapZero.induction_on_of_compact with
| zero => simp [map_zero]
| id => exact hmul_id
| star_id => exact hmul_star_id
| add _ _ h₁ h₂ => simp only [map_add, mul_add, h₁, h₂, zero_add]
| mul _ _ h _ => simp only [map_mul, ← mul_assoc, h, zero_mul]
| smul _ _ h => rw [map_smul, mul_smul_comm, h, smul_zero]
| frequently f h => exact h.mem_of_closed <| isClosed_eq (by fun_prop) continuous_zero
