Metamath Proof Explorer

Definition df-ims

Description: Define the induced metric on a normed complex vector space. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

Ref Expression
Assertion df-ims ⊢ IndMet = u ∈ NrmCVec ⟼ norm CV ⁡ u ∘ - v ⁡ u

Detailed syntax breakdown

Step Hyp Ref Expression
0 cims class IndMet
1 vu setvar u
2 cnv class NrmCVec
3 cnmcv class norm CV
4 1 cv setvar u
5 4 3 cfv class norm CV ⁡ u
6 cnsb class - v
7 4 6 cfv class - v ⁡ u
8 5 7 ccom class norm CV ⁡ u ∘ - v ⁡ u
9 1 2 8 cmpt class u ∈ NrmCVec ⟼ norm CV ⁡ u ∘ - v ⁡ u
10 0 9 wceq wff IndMet = u ∈ NrmCVec ⟼ norm CV ⁡ u ∘ - v ⁡ u