P. 230 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22901-23000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	clmmulg 22901	The group multiple function matches the scalar multiplication function. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- V = ( Base ` W )   &    |- .xb = (.g ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CMod /\ A e. ZZ /\ B e. V ) -> ( A .xb B ) = ( A .x. B ) )
Theorem	clmsubdir 22902	Scalar multiplication distributive law for subtraction. (lmodsubdir 18921 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .- = ( -g ` W )   &    |- ( ph -> W e. CMod )   &    |- ( ph -> A e. K )   &    |- ( ph -> B e. K )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( A - B ) .x. X ) = ( ( A .x. X ) .- ( B .x. X ) ) )
Theorem	clmpm1dir 22903	Subtractive distributive law for the scalar product of a subcomplex module. (Contributed by NM, 31-Jul-2007.) (Revised by AV, 21-Sep-2021.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   &    |- K = ( Base ` (Scalar ` W ) )   =>    |- ( ( W e. CMod /\ ( A e. K /\ B e. K /\ C e. V ) ) -> ( ( A - B ) .x. C ) = ( ( A .x. C ) .+ ( -u 1 .x. ( B .x. C ) ) ) )
Theorem	clmnegneg 22904	Double negative of a vector. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 21-Sep-2021.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. CMod /\ A e. V ) -> ( -u 1 .x. ( -u 1 .x. A ) ) = A )
Theorem	clmnegsubdi2 22905	Distribution of negative over vector subtraction. (Contributed by NM, 6-Aug-2007.) (Revised by AV, 29-Sep-2021.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( -u 1 .x. ( A .+ ( -u 1 .x. B ) ) ) = ( B .+ ( -u 1 .x. A ) ) )
Theorem	clmsub4 22906	Rearrangement of 4 terms in a mixed vector addition and subtraction. (Contributed by NM, 5-Aug-2007.) (Revised by AV, 29-Sep-2021.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. CMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .+ B ) .+ ( -u 1 .x. ( C .+ D ) ) ) = ( ( A .+ ( -u 1 .x. C ) ) .+ ( B .+ ( -u 1 .x. D ) ) ) )
Theorem	clmvsrinv 22907	A vector minus itself. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 28-Sep-2021.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. CMod /\ A e. V ) -> ( A .+ ( -u 1 .x. A ) ) = .0. )
Theorem	clmvslinv 22908	Minus a vector plus itself. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 28-Sep-2021.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. CMod /\ A e. V ) -> ( ( -u 1 .x. A ) .+ A ) = .0. )
Theorem	clmvsubval 22909	Value of vector subtraction in terms of addition in a subcomplex module. Analogue of lmodvsubval2 18918. (Contributed by NM, 31-Mar-2014.) (Revised by AV, 7-Oct-2021.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .- = ( -g ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( A .- B ) = ( A .+ ( -u 1 .x. B ) ) )
Theorem	clmvsubval2 22910	Value of vector subtraction on a subcomplex module. (Contributed by Mario Carneiro, 19-Nov-2013.) (Revised by AV, 7-Oct-2021.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .- = ( -g ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( A .- B ) = ( ( -u 1 .x. B ) .+ A ) )
Theorem	clmvz 22911	Two ways to express the negative of a vector. (Contributed by NM, 29-Feb-2008.) (Revised by AV, 7-Oct-2021.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. CMod /\ A e. V ) -> ( .0. .- A ) = ( -u 1 .x. A ) )
Theorem	zlmclm 22912	The ZZ-module operation turns an arbitrary abelian group into a subcomplex module. (Contributed by Mario Carneiro, 30-Oct-2015.)
|- W = ( ZMod ` G )   =>    |- ( G e. Abel <-> W e. CMod )
Theorem	clmzlmvsca 22913	The scalar product of a subcomplex module matches the scalar product of the derived ZZ-module, which implies, together with zlmbas 19866 and zlmplusg 19867, that any module over ZZ is structure-equivalent to the canonical ZZ-module ZMod ` G. (Contributed by Mario Carneiro, 30-Oct-2015.)
|- W = ( ZMod ` G )   &    |- X = ( Base ` G )   =>    |- ( ( G e. CMod /\ ( A e. ZZ /\ B e. X ) ) -> ( A ( .s ` G ) B ) = ( A ( .s ` W ) B ) )
Theorem	nmoleub2lem 22914*	Lemma for nmoleub2a 22917 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   &    |- G = (Scalar ` S )   &    |- K = ( Base ` G )   &    |- ( ph -> S e. (NrmMod i^i CMod ) )   &    |- ( ph -> T e. (NrmMod i^i CMod ) )   &    |- ( ph -> F e. ( S LMHom T ) )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> 0 <_ A )   &    |- ( ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) )   &    |- ( ( ph /\ x e. V ) -> ( ps -> ( L ` x ) <_ R ) )   =>    |- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )
Theorem	nmoleub2lem3 22915*	Lemma for nmoleub2a 22917 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.) (Proof shortened by AV, 29-Sep-2021.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   &    |- G = (Scalar ` S )   &    |- K = ( Base ` G )   &    |- ( ph -> S e. (NrmMod i^i CMod ) )   &    |- ( ph -> T e. (NrmMod i^i CMod ) )   &    |- ( ph -> F e. ( S LMHom T ) )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> QQ C_ K )   &    |- .x. = ( .s ` S )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. V )   &    |- ( ph -> B =/= ( 0g ` S ) )   &    |- ( ph -> ( ( r .x. B ) e. V -> ( ( L ` ( r .x. B ) ) < R -> ( ( M ` ( F ` ( r .x. B ) ) ) / R ) <_ A ) ) )   &    |- ( ph -> -. ( M ` ( F ` B ) ) <_ ( A x. ( L ` B ) ) )   =>    |- -. ph
Theorem	nmoleub2lem2 22916*	Lemma for nmoleub2a 22917 and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   &    |- G = (Scalar ` S )   &    |- K = ( Base ` G )   &    |- ( ph -> S e. (NrmMod i^i CMod ) )   &    |- ( ph -> T e. (NrmMod i^i CMod ) )   &    |- ( ph -> F e. ( S LMHom T ) )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> QQ C_ K )   &    |- ( ( ( L ` x ) e. RR /\ R e. RR ) -> ( ( L ` x ) O R -> ( L ` x ) <_ R ) )   &    |- ( ( ( L ` x ) e. RR /\ R e. RR ) -> ( ( L ` x ) < R -> ( L ` x ) O R ) )   =>    |- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ( L ` x ) O R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )
Theorem	nmoleub2a 22917*	The operator norm is the supremum of the value of a linear operator in the closed unit ball. (Contributed by Mario Carneiro, 19-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   &    |- G = (Scalar ` S )   &    |- K = ( Base ` G )   &    |- ( ph -> S e. (NrmMod i^i CMod ) )   &    |- ( ph -> T e. (NrmMod i^i CMod ) )   &    |- ( ph -> F e. ( S LMHom T ) )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> QQ C_ K )   =>    |- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ( L ` x ) <_ R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )
Theorem	nmoleub2b 22918*	The operator norm is the supremum of the value of a linear operator in the open unit ball. (Contributed by Mario Carneiro, 19-Oct-2015.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   &    |- G = (Scalar ` S )   &    |- K = ( Base ` G )   &    |- ( ph -> S e. (NrmMod i^i CMod ) )   &    |- ( ph -> T e. (NrmMod i^i CMod ) )   &    |- ( ph -> F e. ( S LMHom T ) )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> QQ C_ K )   =>    |- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ( L ` x ) < R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )
Theorem	nmoleub3 22919*	The operator norm is the supremum of the value of a linear operator on the closed unit sphere. (Contributed by Mario Carneiro, 19-Oct-2015.) (Proof shortened by AV, 29-Sep-2021.)
|- N = ( S normOp T )   &    |- V = ( Base ` S )   &    |- L = ( norm ` S )   &    |- M = ( norm ` T )   &    |- G = (Scalar ` S )   &    |- K = ( Base ` G )   &    |- ( ph -> S e. (NrmMod i^i CMod ) )   &    |- ( ph -> T e. (NrmMod i^i CMod ) )   &    |- ( ph -> F e. ( S LMHom T ) )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> RR C_ K )   =>    |- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ( L ` x ) = R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )
Theorem	nmhmcn 22920	A linear operator over a normed subcomplex module is bounded iff it is continuous. (Contributed by Mario Carneiro, 22-Oct-2015.)
|- J = ( TopOpen ` S )   &    |- K = ( TopOpen ` T )   &    |- G = (Scalar ` S )   &    |- B = ( Base ` G )   =>    |- ( ( S e. (NrmMod i^i CMod ) /\ T e. (NrmMod i^i CMod ) /\ QQ C_ B ) -> ( F e. ( S NMHom T ) <-> ( F e. ( S LMHom T ) /\ F e. ( J Cn K ) ) ) )
Theorem	cmodscexp 22921	The powers of _i belong to the scalar subring of a subcomplex module if _i belongs to the scalar subring . (Contributed by AV, 18-Oct-2021.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( ( W e. CMod /\ _i e. K ) /\ N e. NN ) -> ( _i ^ N ) e. K )
Theorem	cmodscmulexp 22922	The scalar product of a vector with powers of _i belongs to the base set of a subcomplex module if the scalar subring of th subcomplex module contains _i. (Contributed by AV, 18-Oct-2021.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- X = ( Base ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CMod /\ ( _i e. K /\ B e. X /\ N e. NN ) ) -> ( ( _i ^ N ) .x. B ) e. X )
12.5.2  Subcomplex vector spaces Usually, "complex vector spaces" are vector spaces over the field of the complex numbers, see for example the definition in [Roman] p. 36. In the setting of set.mm, it is convenient to consider collectively vector spaces on subfields of the field of complex numbers. We call these, "subcomplex vector spaces" and collect them in the class CVec defined in df-cvs 22924 and characterized in iscvs 22927. These include rational vector spaces (qcvs 22947), real vector spaces (recvs 22946) and complex vector spaces (cncvs 22945). This definition is analogous to the definition of subcomplex modules (and their class CMod), which are modules over subrings of the field of complex numbers. Note that ZZ-modules (that are roughly the same thing as Abelian groups, see zlmclm 22912) are subcomplex modules but are not subcomplex vector spaces (see zclmncvs 22948), because the ring ZZ is not a division ring (see zringndrg 19838). Since the field of complex numbers is commutative, so are its subrings, so there is no need to explicitly state "left module" or "left vector space" for subcomplex modules or vector spaces.
Syntax	ccvs 22923	Syntax for the class of subcomplex vector spaces.
class CVec
Definition	df-cvs 22924	Define the class of subcomplex vector spaces, which are the subcomplex modules which are also vector spaces. (Contributed by Thierry Arnoux, 22-May-2019.)
|- CVec = (CMod i^i LVec )
Theorem	cvslvec 22925	A subcomplex vector space is a (left) vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
|- ( ph -> W e. CVec )   =>    |- ( ph -> W e. LVec )
Theorem	cvsclm 22926	A subcomplex vector space is a subcomplex module. (Contributed by Thierry Arnoux, 22-May-2019.)
|- ( ph -> W e. CVec )   =>    |- ( ph -> W e. CMod )
Theorem	iscvs 22927	A subcomplex vector space is a subcomplex module over a division ring. For example, the subcomplex modules over the rational or real or complex numbers are subcomplex vector spaces. (Contributed by AV, 4-Oct-2021.)
|- ( W e. CVec <-> ( W e. CMod /\ (Scalar ` W ) e. DivRing ) )
Theorem	iscvsp 22928*	The predicate "is a subcomplex vector space." (Contributed by NM, 31-May-2008.) (Revised by AV, 4-Oct-2021.)
|- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   &    |- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- K = ( Base ` S )   =>    |- ( W e. CVec <-> ( ( W e. Grp /\ ( S e. DivRing /\ S = (ℂfld ↾s K ) ) /\ K e. (SubRing ` ℂfld ) ) /\ A. x e. V ( ( 1 .x. x ) = x /\ A. y e. K ( ( y .x. x ) e. V /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. K ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) ) ) ) )
Theorem	iscvsi 22929*	Properties that determine a subcomplex vector space. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 4-Oct-2021.)
|- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   &    |- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- K = ( Base ` S )   &    |- W e. Grp   &    |- S = (ℂfld ↾s K )   &    |- S e. DivRing   &    |- K e. (SubRing ` ℂfld )   &    |- ( x e. V -> ( 1 .x. x ) = x )   &    |- ( ( y e. K /\ x e. V ) -> ( y .x. x ) e. V )   &    |- ( ( y e. K /\ x e. V /\ z e. V ) -> ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) )   &    |- ( ( y e. K /\ z e. K /\ x e. V ) -> ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) )   &    |- ( ( y e. K /\ z e. K /\ x e. V ) -> ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) )   =>    |- W e. CVec
Theorem	cvsi 22930*	The properties of a subcomplex 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. (Contributed by NM, 3-Nov-2006.) (Revised by AV, 21-Sep-2021.)
|- X = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- S = ( Base ` (Scalar ` W ) )   &    |- .xb = ( .sf ` W )   &    |- .x. = ( .s ` W )   =>    |- ( W e. CVec -> ( W e. Abel /\ ( S C_ CC /\ .xb : ( S X. X ) --> X ) /\ A. x e. X ( ( 1 .x. x ) = x /\ A. y e. S ( A. z e. X ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. S ( ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) /\ ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) ) ) ) ) )
Theorem	cvsunit 22931	Unit group of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CVec -> ( K \ { 0 } ) = (Unit ` F ) )
Theorem	cvsdiv 22932	Division of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) = ( A (/r ` F ) B ) )
Theorem	cvsdivcl 22933	The scalar field of a subcomplex vector space is closed under division. (Contributed by Thierry Arnoux, 22-May-2019.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CVec /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) e. K )
Theorem	cvsmuleqdivd 22934	An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- ( ph -> W e. CVec )   &    |- ( ph -> A e. K )   &    |- ( ph -> B e. K )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> ( A .x. X ) = ( B .x. Y ) )   =>    |- ( ph -> X = ( ( B / A ) .x. Y ) )
Theorem	cvsdiveqd 22935	An equality involving ratios in a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- ( ph -> W e. CVec )   &    |- ( ph -> A e. K )   &    |- ( ph -> B e. K )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> X = ( ( A / B ) .x. Y ) )   =>    |- ( ph -> ( ( B / A ) .x. X ) = Y )
Theorem	cnlmodlem1 22936	Lemma 1 for cnlmod 22940. (Contributed by AV, 20-Sep-2021.)
|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. (Scalar ` ndx ) , ℂfld >. , <. ( .s ` ndx ) , x. >. } )   =>    |- ( Base ` W ) = CC
Theorem	cnlmodlem2 22937	Lemma 2 for cnlmod 22940. (Contributed by AV, 20-Sep-2021.)
|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. (Scalar ` ndx ) , ℂfld >. , <. ( .s ` ndx ) , x. >. } )   =>    |- ( +g ` W ) = +
Theorem	cnlmodlem3 22938	Lemma 3 for cnlmod 22940. (Contributed by AV, 20-Sep-2021.)
|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. (Scalar ` ndx ) , ℂfld >. , <. ( .s ` ndx ) , x. >. } )   =>    |- (Scalar ` W ) = ℂfld
Theorem	cnlmod4 22939	Lemma 4 for cnlmod 22940. (Contributed by AV, 20-Sep-2021.)
|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. (Scalar ` ndx ) , ℂfld >. , <. ( .s ` ndx ) , x. >. } )   =>    |- ( .s ` W ) = x.
Theorem	cnlmod 22940	The set of complex numbers is a left module over itself. The vector operation is +, and the scalar product is x.. (Contributed by AV, 20-Sep-2021.)
|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. (Scalar ` ndx ) , ℂfld >. , <. ( .s ` ndx ) , x. >. } )   =>    |- W e. LMod
Theorem	cnstrcvs 22941	The set of complex numbers is a subcomplex vector space. The vector operation is +, and the scalar product is x.. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 20-Sep-2021.)
|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. (Scalar ` ndx ) , ℂfld >. , <. ( .s ` ndx ) , x. >. } )   =>    |- W e. CVec
Theorem	cnrbas 22942	The set of complex numbers is the base set of the complex left module of complex numbers. (Contributed by AV, 21-Sep-2021.)
|- C = (ringLMod ` ℂfld )   =>    |- ( Base ` C ) = CC
Theorem	cnrlmod 22943	The complex left module of complex numbers is a left module. The vector operation is +, and the scalar product is x.. (Contributed by AV, 21-Sep-2021.)
|- C = (ringLMod ` ℂfld )   =>    |- C e. LMod
Theorem	cnrlvec 22944	The complex left module of complex numbers is a left vector space. The vector operation is +, and the scalar product is x.. (Contributed by AV, 21-Sep-2021.)
|- C = (ringLMod ` ℂfld )   =>    |- C e. LVec
Theorem	cncvs 22945	The complex left module of complex numbers is a subcomplex vector space. The vector operation is +, and the scalar product is x.. (Contributed by NM, 5-Nov-2006.) (Revised by AV, 21-Sep-2021.)
|- C = (ringLMod ` ℂfld )   =>    |- C e. CVec
Theorem	recvs 22946	The field of the real numbers as left module over itself is a subcomplex vector space. The vector operation is +, and the scalar product is x.. (Contributed by AV, 22-Oct-2021.)
|- R = (ringLMod ` RRfld )   =>    |- R e. CVec
Theorem	qcvs 22947	The field of rational numbers as left module over itself is a subcomplex vector space. The vector operation is +, and the scalar product is x.. (Contributed by AV, 22-Oct-2021.)
|- Q = (ringLMod ` (ℂfld ↾s QQ ) )   =>    |- Q e. CVec
Theorem	zclmncvs 22948	The ring of integers as left module over itself is a subcomplex module, but not a subcomplex vector space. The vector operation is +, and the scalar product is x.. (Contributed by AV, 22-Oct-2021.)
|- Z = (ringLMod ` ℤring )   =>    |- ( Z e. CMod /\ Z e/ CVec )
12.5.3  Normed subcomplex vector spaces This section characterizes normed subcomplex vector spaces as subcomplex vector spaces which are also normed vector spaces (that is, normed groups with a positively homogeneous norm). For the moment, there is no need of a special token to represent their class, so we only use the characterization isncvsngp 22949. Most theorems for normed subcomplex vector spaces have a label containing "ncvs". The idiom W e. (NrmVec i^i CVec ) is used in the following to say that W is a normed subcomplex vector space, i.e. a subcomplex vector space which is also a normed vector space.
Theorem	isncvsngp 22949*	A normed subcomplex vector space is a subcomplex vector space which is a normed group with a positively homogeneous norm. (Contributed by NM, 5-Jun-2008.) (Revised by AV, 7-Oct-2021.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. (NrmVec i^i CVec ) <-> ( W e. CVec /\ W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) )
Theorem	isncvsngpd 22950*	Properties that determine a normed subcomplex vector space. (Contributed by NM, 15-Apr-2007.) (Revised by AV, 7-Oct-2021.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- ( ph -> W e. CVec )   &    |- ( ph -> W e. NrmGrp )   &    |- ( ( ph /\ ( x e. V /\ k e. K ) ) -> ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) )   =>    |- ( ph -> W e. (NrmVec i^i CVec ) )
Theorem	ncvsi 22951*	The properties of a normed subcomplex vector space, which is a vector space accompanied by a norm. (Contributed by NM, 11-Nov-2006.) (Revised by AV, 7-Oct-2021.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .- = ( -g ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( W e. (NrmVec i^i CVec ) -> ( W e. CVec /\ N : V --> RR /\ A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
Theorem	ncvsprp 22952	Proportionality property of the norm of a scalar product in a normed subcomplex vector space. (Contributed by NM, 11-Nov-2006.) (Revised by AV, 8-Oct-2021.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. (NrmVec i^i CVec ) /\ A e. K /\ B e. V ) -> ( N ` ( A .x. B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )
Theorem	ncvsge0 22953	The norm of a scalar product with a nonnegative real. (Contributed by NM, 1-Jan-2008.) (Revised by AV, 8-Oct-2021.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. (NrmVec i^i CVec ) /\ ( A e. ( K i^i RR ) /\ 0 <_ A ) /\ B e. V ) -> ( N ` ( A .x. B ) ) = ( A x. ( N ` B ) ) )
Theorem	ncvsm1 22954	The norm of the negative of a vector. (Contributed by NM, 28-Nov-2006.) (Revised by AV, 8-Oct-2021.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. (NrmVec i^i CVec ) /\ A e. V ) -> ( N ` ( -u 1 .x. A ) ) = ( N ` A ) )
Theorem	ncvsdif 22955	The norm of the difference between two vectors. (Contributed by NM, 1-Dec-2006.) (Revised by AV, 8-Oct-2021.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. (NrmVec i^i CVec ) /\ A e. V /\ B e. V ) -> ( N ` ( A .+ ( -u 1 .x. B ) ) ) = ( N ` ( B .+ ( -u 1 .x. A ) ) ) )
Theorem	ncvspi 22956	The norm of a vector plus the imaginary scalar product of another. (Contributed by NM, 2-Feb-2007.) (Revised by AV, 8-Oct-2021.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .x. = ( .s ` W )   &    |- .+ = ( +g ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. (NrmVec i^i CVec ) /\ ( A e. V /\ B e. V ) /\ _i e. K ) -> ( N ` ( A .+ ( _i .x. B ) ) ) = ( N ` ( B .+ ( -u _i .x. A ) ) ) )
Theorem	ncvs1 22957	From any nonzero vector, construct a vector whose norm is one. (Contributed by NM, 6-Dec-2007.) (Revised by AV, 8-Oct-2021.)
|- X = ( Base ` G )   &    |- N = ( norm ` G )   &    |- .0. = ( 0g ` G )   &    |- .x. = ( .s ` G )   &    |- F = (Scalar ` G )   &    |- K = ( Base ` F )   =>    |- ( ( G e. (NrmVec i^i CVec ) /\ ( A e. X /\ A =/= .0. ) /\ ( 1 / ( N ` A ) ) e. K ) -> ( N ` ( ( 1 / ( N ` A ) ) .x. A ) ) = 1 )
Theorem	cnrnvc 22958	The set of complex numbers (as a subring of itself) is a normed vector space over itself. The vector operation is +, and the scalar product is x., and the norm function is abs. (Contributed by AV, 9-Oct-2021.)
|- C = (ringLMod ` ℂfld )   =>    |- C e. NrmVec
Theorem	cnncvs 22959	The set of complex numbers (as a subring of itself) is a normed subcomplex vector space. The vector operation is +, and the scalar product is x., and the norm function is abs. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 9-Oct-2021.)
|- C = (ringLMod ` ℂfld )   =>    |- C e. (NrmVec i^i CVec )
Theorem	cnnm 22960	The norm operation of the normed subcomplex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (Revised by AV, 9-Oct-2021.)
|- C = (ringLMod ` ℂfld )   =>    |- ( norm ` C ) = abs
Theorem	ncvspds 22961	Value of the distance function in terms of the norm of a normed subcomplex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (Revised by AV, 13-Oct-2021.)
|- N = ( norm ` G )   &    |- X = ( Base ` G )   &    |- .+ = ( +g ` G )   &    |- D = ( dist ` G )   &    |- .x. = ( .s ` G )   =>    |- ( ( G e. (NrmVec i^i CVec ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( N ` ( A .+ ( -u 1 .x. B ) ) ) )
Theorem	cnindmet 22962	The metric induced on the complex numbers. cnmet 22575 proves that it is a metric. The induced metric is identical with the original metric on the complex numbers, see cnfldds 19756 and also cnmet 22575. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by AV, 17-Oct-2021.)
|- T = (ℂfld toNrmGrp abs )   =>    |- ( dist ` T ) = ( abs o. - )
Theorem	cnncvsaddassdemo 22963	Derive the associative law for complex number addition addass 10023 to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by NM, 12-Jan-2008.) (Revised by AV, 9-Oct-2021.) (Proof modification is discouraged.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Theorem	cnncvsmulassdemo 22964	Derive the associative law for complex number multiplication mulass 10024 interpreted as scalar multiplication to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by AV, 9-Oct-2021.) (Proof modification is discouraged.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
Theorem	cnncvsabsnegdemo 22965	Derive the absolute value of a negative complex number absneg 14017 to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by AV, 9-Oct-2021.) (Proof modification is discouraged.)
|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )
12.5.4  Subcomplex pre-Hilbert space
Syntax	ccph 22966	Extend class notation with a class of subcomplex pre-Hilbert spaces.
class CPreHil
Syntax	ctch 22967	Function to put a norm on a Hilbert space.
class toCHil
Definition	df-cph 22968*	Define the class of subcomplex pre-Hilbert spaces. By restricting the scalar field to a quadratically closed subfield of ℂfld, we have enough structure to define a norm, with the associated connection to a metric and topology. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- CPreHil = { w e. ( PreHil i^i NrmMod ) | [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) }
Definition	df-tch 22969*	Define a function to augment a (pre-)Hilbert space with a norm. No extra parameters are needed, but some conditions must be satisfied to ensure that this in fact creates a normed subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- toCHil = ( w e. _V |-> ( w toNrmGrp ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) )
Theorem	iscph 22970*	A subcomplex pre-Hilbert space is a pre-Hilbert space over a quadratically closed subfield of the field of complex numbers, with a norm defined. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   &    |- N = ( norm ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CPreHil <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = (ℂfld ↾s K ) ) /\ ( sqr " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) ) )
Theorem	cphphl 22971	A subcomplex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- ( W e. CPreHil -> W e. PreHil )
Theorem	cphnlm 22972	A subcomplex pre-Hilbert space is a normed module. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- ( W e. CPreHil -> W e. NrmMod )
Theorem	cphngp 22973	A subcomplex pre-Hilbert space is a normed group. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( W e. CPreHil -> W e. NrmGrp )
Theorem	cphlmod 22974	A subcomplex pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- ( W e. CPreHil -> W e. LMod )
Theorem	cphlvec 22975	A subcomplex pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- ( W e. CPreHil -> W e. LVec )
Theorem	cphnvc 22976	A subcomplex pre-Hilbert space is a normed vector space. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- ( W e. CPreHil -> W e. NrmVec )
Theorem	cphsubrglem 22977	Lemma for cphsubrg 22980. (Contributed by Mario Carneiro, 9-Oct-2015.)
|- K = ( Base ` F )   &    |- ( ph -> F = (ℂfld ↾s A ) )   &    |- ( ph -> F e. DivRing )   =>    |- ( ph -> ( F = (ℂfld ↾s K ) /\ K = ( A i^i CC ) /\ K e. (SubRing ` ℂfld ) ) )
Theorem	cphreccllem 22978	Lemma for cphreccl 22981. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- K = ( Base ` F )   &    |- ( ph -> F = (ℂfld ↾s A ) )   &    |- ( ph -> F e. DivRing )   =>    |- ( ( ph /\ X e. K /\ X =/= 0 ) -> ( 1 / X ) e. K )
Theorem	cphsca 22979	A subcomplex pre-Hilbert space is a vector space over a subfield of ℂfld. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CPreHil -> F = (ℂfld ↾s K ) )
Theorem	cphsubrg 22980	The scalar field of a subcomplex pre-Hilbert space is a subring of ℂfld. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CPreHil -> K e. (SubRing ` ℂfld ) )
Theorem	cphreccl 22981	The scalar field of a subcomplex pre-Hilbert space is closed under reciprocal. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CPreHil /\ A e. K /\ A =/= 0 ) -> ( 1 / A ) e. K )
Theorem	cphdivcl 22982	The scalar field of a subcomplex pre-Hilbert space is closed under reciprocal. (Contributed by Mario Carneiro, 11-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CPreHil /\ ( A e. K /\ B e. K /\ B =/= 0 ) ) -> ( A / B ) e. K )
Theorem	cphcjcl 22983	The scalar field of a subcomplex pre-Hilbert space is closed under conjugation. (Contributed by Mario Carneiro, 11-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CPreHil /\ A e. K ) -> ( * ` A ) e. K )
Theorem	cphsqrtcl 22984	The scalar field of a subcomplex pre-Hilbert space is closed under square roots of positive reals (i.e. it is quadratically closed relative to RR). (Contributed by Mario Carneiro, 8-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CPreHil /\ ( A e. K /\ A e. RR /\ 0 <_ A ) ) -> ( sqr ` A ) e. K )
Theorem	cphabscl 22985	The scalar field of a subcomplex pre-Hilbert space is closed under the absolute value operation. (Contributed by Mario Carneiro, 11-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CPreHil /\ A e. K ) -> ( abs ` A ) e. K )
Theorem	cphsqrtcl2 22986	The scalar field of a subcomplex pre-Hilbert space is closed under square roots of all numbers except possibly the negative reals. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) -> ( sqr ` A ) e. K )
Theorem	cphsqrtcl3 22987	If the scalar field contains _i, it is completely closed under square roots (i.e. it is quadratically closed). (Contributed by Mario Carneiro, 11-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CPreHil /\ _i e. K /\ A e. K ) -> ( sqr ` A ) e. K )
Theorem	cphqss 22988	The scalar field of a subcomplex pre-Hilbert space contains all rational numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CPreHil -> QQ C_ K )
Theorem	cphclm 22989	A subcomplex pre-Hilbert space is a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ( W e. CPreHil -> W e. CMod )
Theorem	cphnmvs 22990	Norm of a scalar product. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- N = ( norm ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CPreHil /\ X e. K /\ Y e. V ) -> ( N ` ( X .x. Y ) ) = ( ( abs ` X ) x. ( N ` Y ) ) )
Theorem	cphipcl 22991	An inner product is a member of the complex numbers. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   =>    |- ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. CC )
Theorem	cphnmfval 22992*	The value of the norm in a subcomplex pre-Hilbert space is the square root of the inner product of a vector with itself. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   &    |- N = ( norm ` W )   =>    |- ( W e. CPreHil -> N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) )
Theorem	cphnm 22993	The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   &    |- N = ( norm ` W )   =>    |- ( ( W e. CPreHil /\ A e. V ) -> ( N ` A ) = ( sqr ` ( A ., A ) ) )
Theorem	nmsq 22994	The square of the norm is the norm of an inner product in a subcomplex pre-Hilbert space. Equation I4 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   &    |- N = ( norm ` W )   =>    |- ( ( W e. CPreHil /\ A e. V ) -> ( ( N ` A ) ^ 2 ) = ( A ., A ) )
Theorem	cphnmf 22995	The norm of a vector is a member of the scalar field in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 9-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   &    |- N = ( norm ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CPreHil -> N : V --> K )
Theorem	cphnmcl 22996	The norm of a vector is a member of the scalar field in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 9-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   &    |- N = ( norm ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CPreHil /\ A e. V ) -> ( N ` A ) e. K )
Theorem	reipcl 22997	An inner product of an element with itself is real. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   =>    |- ( ( W e. CPreHil /\ A e. V ) -> ( A ., A ) e. RR )
Theorem	ipge0 22998	The inner product in a subcomplex pre-Hilbert space is positive definite. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   =>    |- ( ( W e. CPreHil /\ A e. V ) -> 0 <_ ( A ., A ) )
Theorem	cphipcj 22999	Conjugate of an inner product in a subcomplex pre-Hilbert space. Complex version of ipcj 19979. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   =>    |- ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( * ` ( A ., B ) ) = ( B ., A ) )
Theorem	cphipipcj 23000	An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (Revised by AV, 19-Oct-2021.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   =>    |- ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( A ., B ) x. ( B ., A ) ) = ( ( abs ` ( A ., B ) ) ^ 2 ) )