P. 275 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27401-27500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ablogrpo 27401	An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp)
Theorem	ablocom 27402	An Abelian group operation is commutative. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴))
Theorem	ablo32 27403	Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵))
Theorem	ablo4 27404	Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐶𝐺𝐷)) = ((𝐴𝐺𝐶)𝐺(𝐵𝐺𝐷)))
Theorem	isabloi 27405*	Properties that determine an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ GrpOp    &   ⊢ dom 𝐺 = (𝑋 × 𝑋)    &   ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥))    ⇒   ⊢ 𝐺 ∈ AbelOp
Theorem	ablomuldiv 27406	Law for group multiplication and division. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐷𝐶) = ((𝐴𝐷𝐶)𝐺𝐵))
Theorem	ablodivdiv 27407	Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷(𝐵𝐷𝐶)) = ((𝐴𝐷𝐵)𝐺𝐶))
Theorem	ablodivdiv4 27408	Law for double group division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷𝐶) = (𝐴𝐷(𝐵𝐺𝐶)))
Theorem	ablodiv32 27409	Swap the second and third terms in a double division. (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷𝐶) = ((𝐴𝐷𝐶)𝐷𝐵))
Theorem	ablonnncan 27410	Cancellation law for group division. (nnncan 10316 analog.) (Contributed by NM, 29-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷(𝐵𝐷𝐶))𝐷𝐶) = (𝐴𝐷𝐵))
Theorem	ablonncan 27411	Cancellation law for group division. (nncan 10310 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷(𝐴𝐷𝐵)) = 𝐵)
Theorem	ablonnncan1 27412	Cancellation law for group division. (nnncan1 10317 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝐷 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐵)𝐷(𝐴𝐷𝐶)) = (𝐶𝐷𝐵))
18.2  Complex vector spaces
18.2.1  Definition and basic properties
Syntax	cvc 27413	Extend class notation with the class of all complex vector spaces.
class CVecOLD
Definition	df-vc 27414*	Define the class of all complex vector spaces. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ CVecOLD = {⟨𝑔, 𝑠⟩ ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))}
Theorem	vcrel 27415	The class of all complex vector spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.)
⊢ Rel CVecOLD
Theorem	vciOLD 27416*	Obsolete version of cvsi 22930 as of 21-Sep-2021. The properties of a complex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. The variable 𝑊 was chosen because V is already used for the universal class. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑊 ∈ CVecOLD → (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥)))))))
Theorem	vcsm 27417	Functionality of th scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑊 ∈ CVecOLD → 𝑆:(ℂ × 𝑋)⟶𝑋)
Theorem	vccl 27418	Closure of the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋)
Theorem	vcidOLD 27419	Identity element for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) Obsolete as of 21-Sep-2021. Use clmvs1 22893 together with cvsclm 22926 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
Theorem	vcdi 27420	Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶)))
Theorem	vcdir 27421	Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶)))
Theorem	vcass 27422	Associative law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶)))
Theorem	vc2OLD 27423	A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007.) Obsolete as of 21-Sep-2021. Use clmvs2 22894 together with cvsclm 22926 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝐴) = (2𝑆𝐴))
Theorem	vcablo 27424	Vector addition is an Abelian group operation. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    ⇒   ⊢ (𝑊 ∈ CVecOLD → 𝐺 ∈ AbelOp)
Theorem	vcgrp 27425	Vector addition is a group operation. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    ⇒   ⊢ (𝑊 ∈ CVecOLD → 𝐺 ∈ GrpOp)
Theorem	vclcan 27426	Left cancellation law for vector addition. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐶𝐺𝐴) = (𝐶𝐺𝐵) ↔ 𝐴 = 𝐵))
Theorem	vczcl 27427	The zero vector is a vector. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑊 ∈ CVecOLD → 𝑍 ∈ 𝑋)
Theorem	vc0rid 27428	The zero vector is a right identity element. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴)
Theorem	vc0 27429	Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = 𝑍)
Theorem	vcz 27430	Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (Contributed by NM, 24-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ ℂ) → (𝐴𝑆𝑍) = 𝑍)
Theorem	vcm 27431	Minus 1 times a vector is the underlying group's inverse element. Equation 2 of [Kreyszig] p. 51. (Contributed by NM, 25-Nov-2006.) (New usage is discouraged.)
⊢ 𝐺 = (1st ‘𝑊)    &   ⊢ 𝑆 = (2nd ‘𝑊)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑀 = (inv‘𝐺)    ⇒   ⊢ ((𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (-1𝑆𝐴) = (𝑀‘𝐴))
Theorem	isvclem 27432*	Lemma for isvcOLD 27434. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (⟨𝐺, 𝑆⟩ ∈ CVecOLD ↔ (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥))))))))
Theorem	vcex 27433	The components of a complex vector space are sets. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
⊢ (⟨𝐺, 𝑆⟩ ∈ CVecOLD → (𝐺 ∈ V ∧ 𝑆 ∈ V))
Theorem	isvcOLD 27434*	The predicate "is a complex vector space." (Contributed by NM, 31-May-2008.) Obsolete as of 4-Oct-2021. Use iscvsp 22928 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (⟨𝐺, 𝑆⟩ ∈ CVecOLD ↔ (𝐺 ∈ AbelOp ∧ 𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ((1𝑆𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ 𝑋 (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)) ∧ ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥)))))))
Theorem	isvciOLD 27435*	Properties that determine a complex vector space. (Contributed by NM, 5-Nov-2006.) Obsolete as of 4-Oct-2021. Use iscvsi 22929 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐺 ∈ AbelOp    &   ⊢ dom 𝐺 = (𝑋 × 𝑋)    &   ⊢ 𝑆:(ℂ × 𝑋)⟶𝑋    &   ⊢ (𝑥 ∈ 𝑋 → (1𝑆𝑥) = 𝑥)    &   ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦𝑆(𝑥𝐺𝑧)) = ((𝑦𝑆𝑥)𝐺(𝑦𝑆𝑧)))    &   ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝑋) → ((𝑦 + 𝑧)𝑆𝑥) = ((𝑦𝑆𝑥)𝐺(𝑧𝑆𝑥)))    &   ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝑋) → ((𝑦 · 𝑧)𝑆𝑥) = (𝑦𝑆(𝑧𝑆𝑥)))    &   ⊢ 𝑊 = ⟨𝐺, 𝑆⟩    ⇒   ⊢ 𝑊 ∈ CVecOLD
18.2.2  Examples of complex vector spaces
Theorem	cnaddabloOLD 27436	Obsolete as of 23-Jan-2020. Use cnaddabl 18272 instead. Complex number addition is an Abelian group operation. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ + ∈ AbelOp
Theorem	cnidOLD 27437	Obsolete as of 23-Jan-2020. Use cnaddid 18273 instead. The group identity element of complex number addition is zero. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 0 = (GId‘ + )
Theorem	cncvcOLD 27438	Obsolete version of cncvs 22945 as of 20-Sep-2021. The set of complex numbers is a complex vector space. The vector operation is +, and the scalar product is ·. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ⟨ + , · ⟩ ∈ CVecOLD
18.3  Normed complex vector spaces
18.3.1  Definition and basic properties
Syntax	cnv 27439	Extend class notation with the class of all normed complex vector spaces.
class NrmCVec
Syntax	cpv 27440	Extend class notation with vector addition in a normed complex vector space. In the literature, the subscript "v" is omitted, but we need it to avoid ambiguity with complex number addition + caddc 9939.
class +𝑣
Syntax	cba 27441	Extend class notation with the base set of a normed complex vector space. (Note that BaseSet is capitalized because, once it is fixed for a particular vector space 𝑈, it is not a function, unlike e.g. normCV. This is our typical convention.) (New usage is discouraged.)
class BaseSet
Syntax	cns 27442	Extend class notation with scalar multiplication in a normed complex vector space. In the literature scalar multiplication is usually indicated by juxtaposition, but we need an explicit symbol to prevent ambiguity.
class ·𝑠OLD
Syntax	cn0v 27443	Extend class notation with zero vector in a normed complex vector space.
class 0vec
Syntax	cnsb 27444	Extend class notation with vector subtraction in a normed complex vector space.
class −𝑣
Syntax	cnmcv 27445	Extend class notation with the norm function in a normed complex vector space. In the literature, the norm of 𝐴 is usually written "|| 𝐴 ||", but we use function notation to take advantage of our existing theorems about functions.
class normCV
Syntax	cims 27446	Extend class notation with the class of the induced metrics on normed complex vector spaces.
class IndMet
Definition	df-nv 27447*	Define the class of all normed complex vector spaces. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
⊢ NrmCVec = {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))}
Theorem	nvss 27448	Structure of the class of all normed complex vectors spaces. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 1-May-2015.) (New usage is discouraged.)
⊢ NrmCVec ⊆ (CVecOLD × V)
Theorem	nvvcop 27449	A normed complex vector space is a vector space. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 1-May-2015.) (New usage is discouraged.)
⊢ (⟨𝑊, 𝑁⟩ ∈ NrmCVec → 𝑊 ∈ CVecOLD)
Definition	df-va 27450	Define vector addition on a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.)
⊢ +𝑣 = (1st ∘ 1st )
Definition	df-ba 27451	Define the base set of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.)
⊢ BaseSet = (𝑥 ∈ V ↦ ran ( +𝑣 ‘𝑥))
Definition	df-sm 27452	Define scalar multiplication on a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.)
⊢ ·𝑠OLD = (2nd ∘ 1st )
Definition	df-0v 27453	Define the zero vector in a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.)
⊢ 0vec = (GId ∘ +𝑣 )
Definition	df-vs 27454	Define vector subtraction on a normed complex vector space. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ −𝑣 = ( /𝑔 ∘ +𝑣 )
Definition	df-nmcv 27455	Define the norm function in a normed complex vector space. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.)
⊢ normCV = 2nd
Definition	df-ims 27456	Define the induced metric on a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ IndMet = (𝑢 ∈ NrmCVec ↦ ((normCV‘𝑢) ∘ ( −𝑣 ‘𝑢)))
Theorem	nvrel 27457	The class of all normed complex vectors spaces is a relation. (Contributed by NM, 14-Nov-2006.) (New usage is discouraged.)
⊢ Rel NrmCVec
Theorem	vafval 27458	Value of the function for the vector addition (group) operation on a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ 𝐺 = (1st ‘(1st ‘𝑈))
Theorem	bafval 27459	Value of the function for the base set of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ 𝑋 = ran 𝐺
Theorem	smfval 27460	Value of the function for the scalar multiplication operation on a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (New usage is discouraged.)
⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ 𝑆 = (2nd ‘(1st ‘𝑈))
Theorem	0vfval 27461	Value of the function for the zero vector on a normed complex vector space. (Contributed by NM, 24-Apr-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ (𝑈 ∈ 𝑉 → 𝑍 = (GId‘𝐺))
Theorem	nmcvfval 27462	Value of the norm function in a normed complex vector space. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.)
⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ 𝑁 = (2nd ‘𝑈)
Theorem	nvop2 27463	A normed complex vector space is an ordered pair of a vector space and a norm operation. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.)
⊢ 𝑊 = (1st ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑈 = ⟨𝑊, 𝑁⟩)
Theorem	nvvop 27464	The vector space component of a normed complex vector space is an ordered pair of the underlying group and a scalar product. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.)
⊢ 𝑊 = (1st ‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑊 = ⟨𝐺, 𝑆⟩)
Theorem	isnvlem 27465*	Lemma for isnv 27467. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD ∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))))))
Theorem	nvex 27466	The components of a normed complex vector space are sets. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 1-May-2015.) (New usage is discouraged.)
⊢ (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec → (𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V))
Theorem	isnv 27467*	The predicate "is a normed complex vector space." (Contributed by NM, 5-Jun-2008.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD ∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))
Theorem	isnvi 27468*	Properties that determine a normed complex vector space. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ ⟨𝐺, 𝑆⟩ ∈ CVecOLD    &   ⊢ 𝑁:𝑋⟶ℝ    &   ⊢ ((𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) = 0) → 𝑥 = 𝑍)    &   ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)))    &   ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))    &   ⊢ 𝑈 = ⟨⟨𝐺, 𝑆⟩, 𝑁⟩    ⇒   ⊢ 𝑈 ∈ NrmCVec
Theorem	nvi 27469*	The properties of a normed complex vector space, which is a vector space accompanied by a norm. (Contributed by NM, 11-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → (⟨𝐺, 𝑆⟩ ∈ CVecOLD ∧ 𝑁:𝑋⟶ℝ ∧ ∀𝑥 ∈ 𝑋 (((𝑁‘𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁‘𝑥)) ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))
Theorem	nvvc 27470	The vector space component of a normed complex vector space. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑊 = (1st ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑊 ∈ CVecOLD)
Theorem	nvablo 27471	The vector addition operation of a normed complex vector space is an Abelian group. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐺 ∈ AbelOp)
Theorem	nvgrp 27472	The vector addition operation of a normed complex vector space is a group. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐺 ∈ GrpOp)
Theorem	nvgf 27473	Mapping for the vector addition operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐺:(𝑋 × 𝑋)⟶𝑋)
Theorem	nvsf 27474	Mapping for the scalar multiplication operation. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑆:(ℂ × 𝑋)⟶𝑋)
Theorem	nvgcl 27475	Closure law for the vector addition (group) operation of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
Theorem	nvcom 27476	The vector addition (group) operation is commutative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴))
Theorem	nvass 27477	The vector addition (group) operation is associative. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶)))
Theorem	nvadd32 27478	Commutative/associative law for vector addition. (Contributed by NM, 27-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = ((𝐴𝐺𝐶)𝐺𝐵))
Theorem	nvrcan 27479	Right cancellation law for vector addition. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵))
Theorem	nvadd4 27480	Rearrangement of 4 terms in a vector sum. (Contributed by NM, 8-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐶𝐺𝐷)) = ((𝐴𝐺𝐶)𝐺(𝐵𝐺𝐷)))
Theorem	nvscl 27481	Closure law for the scalar product operation of a normed complex vector space. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴𝑆𝐵) ∈ 𝑋)
Theorem	nvsid 27482	Identity element for the scalar product of a normed complex vector space. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
Theorem	nvsass 27483	Associative law for the scalar product of a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶)))
Theorem	nvscom 27484	Commutative law for the scalar product of a normed complex vector space. (Contributed by NM, 14-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝑆𝐶)) = (𝐵𝑆(𝐴𝑆𝐶)))
Theorem	nvdi 27485	Distributive law for the scalar product of a complex vector space. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶)))
Theorem	nvdir 27486	Distributive law for the scalar product of a complex vector space. (Contributed by NM, 4-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶)))
Theorem	nv2 27487	A vector plus itself is two times the vector. (Contributed by NM, 9-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝐴) = (2𝑆𝐴))
Theorem	vsfval 27488	Value of the function for the vector subtraction operation on a normed complex vector space. (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 27-Dec-2014.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ 𝑀 = ( /𝑔 ‘𝐺)
Theorem	nvzcl 27489	Closure law for the zero vector of a normed complex vector space. (Contributed by NM, 27-Nov-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋)
Theorem	nv0rid 27490	The zero vector is a right identity element. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴)
Theorem	nv0lid 27491	The zero vector is a left identity element. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑍𝐺𝐴) = 𝐴)
Theorem	nv0 27492	Zero times a vector is the zero vector. (Contributed by NM, 27-Nov-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = 𝑍)
Theorem	nvsz 27493	Anything times the zero vector is the zero vector. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ) → (𝐴𝑆𝑍) = 𝑍)
Theorem	nvinv 27494	Minus 1 times a vector is the underlying group's inverse element. Equation 2 of [Kreyszig] p. 51. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑀 = (inv‘𝐺)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (-1𝑆𝐴) = (𝑀‘𝐴))
Theorem	nvinvfval 27495	Function for the negative of a vector on a normed complex vector space, in terms of the underlying addition group inverse. (We currently do not have a separate notation for the negative of a vector.) (Contributed by NM, 27-Mar-2008.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (𝑆 ∘ ◡(2nd ↾ ({-1} × V)))    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑁 = (inv‘𝐺))
Theorem	nvm 27496	Vector subtraction in terms of group division operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = ( /𝑔 ‘𝐺)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑀𝐵) = (𝐴𝑁𝐵))
Theorem	nvmval 27497	Value of vector subtraction on a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑀𝐵) = (𝐴𝐺(-1𝑆𝐵)))
Theorem	nvmval2 27498	Value of vector subtraction on a normed complex vector space. (Contributed by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑀𝐵) = ((-1𝑆𝐵)𝐺𝐴))
Theorem	nvmfval 27499*	Value of the function for the vector subtraction operation on a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑀 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥𝐺(-1𝑆𝑦))))
Theorem	nvmf 27500	Mapping for the vector subtraction operation. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑀:(𝑋 × 𝑋)⟶𝑋)