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

Metamath Proof Explorer

Theorem hlmulid

Description: Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hlmulf.1 ⊢ X = BaseSet ⁡ U
hlmulf.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
Assertion hlmulid ⊢ U ∈ CHil OLD ∧ A ∈ X → 1 S A = A

Proof

Step Hyp Ref Expression
1 hlmulf.1 ⊢ X = BaseSet ⁡ U
2 hlmulf.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
3 hlnv ⊢ U ∈ CHil OLD → U ∈ NrmCVec
4 1 2 nvsid ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 S A = A
5 3 4 sylan ⊢ U ∈ CHil OLD ∧ A ∈ X → 1 S A = A