P. 214 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21301-21400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	clmfgrp 21301	The scalar ring of a complex module is a group. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> F e. Grp )
Theorem	clm0 21302	The zero of the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> 0 = ( 0g ` F ) )
Theorem	clm1 21303	The identity of the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> 1 = ( 1r ` F ) )
Theorem	clmadd 21304	The addition of the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> + = ( +g ` F ) )
Theorem	clmmul 21305	The multiplication of the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> x. = ( .r ` F ) )
Theorem	clmcj 21306	The conjugation of the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. CMod -> * = ( *r ` F ) )
Theorem	isclmi 21307	Reverse direction of isclm 21294. (Contributed by Mario Carneiro, 30-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( ( W e. LMod /\ F = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> W e. CMod )
Theorem	clmzss 21308	The scalar ring of a complex module contains the integers. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CMod -> ZZ C_ K )
Theorem	clmsscn 21309	The scalar ring of a complex module is a subset of the complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CMod -> K C_ CC )
Theorem	clmsub 21310	Subtraction in the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ A e. K /\ B e. K ) -> ( A - B ) = ( A ( -g ` F ) B ) )
Theorem	clmneg 21311	Negation in the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ A e. K ) -> -u A = ( ( invg ` F ) ` A ) )
Theorem	clmabs 21312	Norm in the scalar ring of a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ A e. K ) -> ( abs ` A ) = ( ( norm ` F ) ` A ) )
Theorem	clmacl 21313	Closure of ring addition for a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ X e. K /\ Y e. K ) -> ( X + Y ) e. K )
Theorem	clmmcl 21314	Closure of ring multiplication for a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ X e. K /\ Y e. K ) -> ( X x. Y ) e. K )
Theorem	clmsubcl 21315	Closure of ring subtraction for a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ X e. K /\ Y e. K ) -> ( X - Y ) e. K )
Theorem	lmhmclm 21316	The domain of a linear operator is a complex module iff the range is. (Contributed by Mario Carneiro, 21-Oct-2015.)
|- ( F e. ( S LMHom T ) -> ( S e. CMod <-> T e. CMod ) )
Theorem	clmvsass 21317	Associative law for scalar product. (lmodvsass 17315 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q x. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )
Theorem	clmvsdir 21318	Distributive law for scalar product (right-distributivity). (lmodvsdir 17314 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q + R ) .x. X ) = ( ( Q .x. X ) .+ ( R .x. X ) ) )
Theorem	clmvs1 21319	Scalar product with ring unit. (lmodvs1 17318 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CMod /\ X e. V ) -> ( 1 .x. X ) = X )
Theorem	clm0vs 21320	Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (lmod0vs 17323 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. CMod /\ X e. V ) -> ( 0 .x. X ) = .0. )
Theorem	clmvneg1 21321	Minus 1 times a vector is the negative of the vector. Equation 2 of [Kreyszig] p. 51. (lmodvneg1 17331 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- V = ( Base ` W )   &    |- N = ( invg ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CMod /\ X e. V ) -> ( -u 1 .x. X ) = ( N ` X ) )
Theorem	clmvsneg 21322	Multiplication of a vector by a negated scalar. (lmodvsneg 17332 analog.) (Contributed by Mario Carneiro, 16-Oct-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( invg ` W )   &    |- K = ( Base ` F )   &    |- ( ph -> W e. CMod )   &    |- ( ph -> X e. B )   &    |- ( ph -> R e. K )   =>    |- ( ph -> ( N ` ( R .x. X ) ) = ( -u R .x. X ) )
Theorem	clmmulg 21323	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 21324	Scalar multiplication distributive law for subtraction. (lmodsubdir 17346 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	zlmclm 21325	The ZZ-module operation turns an arbitrary abelian group into a complex module. (Contributed by Mario Carneiro, 30-Oct-2015.)
|- W = ( ZMod ` G )   =>    |- ( G e. Abel <-> W e. CMod )
Theorem	clmzlmvsca 21326	The scalar product of a complex module matches the scalar product of the derived ZZ-module, which implies, together with zlmbas 18317 and zlmplusg 18318, 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 21327*	Lemma for nmoleub2a 21330 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 21328*	Lemma for nmoleub2a 21330 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 )   &    |- .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 21329*	Lemma for nmoleub2a 21330 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 21330*	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 21331*	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 21332*	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.)
|- 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 21333	A linear operator over a normed complex 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 ) ) ) )
12.5.2  Complex vector spaces
Syntax	ccvs 21334	Complex vector space.
class CVec
Definition	df-cvs 21335	Define a complex vector space, which is just a complex left module and a vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
|- CVec = (CMod i^i LVec )
Theorem	cvslvec 21336	A complex vector space is a (left) vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
|- ( ph -> W e. CVec )   =>    |- ( ph -> W e. LVec )
Theorem	cvsclm 21337	A complex vector space is a complex left module. (Contributed by Thierry Arnoux, 22-May-2019.)
|- ( ph -> W e. CVec )   =>    |- ( ph -> W e. CMod )
Theorem	cvsunit 21338	Unit group of the scalar ring of a complex vector space. (Contributed by Thierry Arnoux, 22-May-2019.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CVec -> ( K \ { 0 } ) = (Unit ` F ) )
Theorem	cvsdiv 21339	Division of the scalar ring of a complex 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 21340	The scalar field of a complex 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 21341	An equality involving ratios in a complex 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 21342	An equality involving ratios in a complex 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 )
12.5.3  Complex pre-Hilbert space
Syntax	ccph 21343	Extend class notation with a complex pre-Hilbert space.
class CPreHil
Syntax	ctch 21344	Function to put a norm on a Hilbert space.
class toCHil
Definition	df-cph 21345*	Define a complex pre-Hilbert space. By restricting the scalar field to a quadratically closed subfield of CC, 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 21346*	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 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 21347*	A complex pre-Hilbert space is a pre-Hilbert space over a quadratically closed subfield of the 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 21348	A complex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- ( W e. CPreHil -> W e. PreHil )
Theorem	cphnlm 21349	A complex pre-Hilbert space is a normed module. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- ( W e. CPreHil -> W e. NrmMod )
Theorem	cphngp 21350	A complex pre-Hilbert space is a normed group. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( W e. CPreHil -> W e. NrmGrp )
Theorem	cphlmod 21351	A complex pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- ( W e. CPreHil -> W e. LMod )
Theorem	cphlvec 21352	A complex pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- ( W e. CPreHil -> W e. LVec )
Theorem	cphnvc 21353	A complex pre-Hilbert space is a normed vector space. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- ( W e. CPreHil -> W e. NrmVec )
Theorem	cphsubrglem 21354	Lemma for cphsubrg 21357. (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 21355	Lemma for cphreccl 21358. (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 21356	A complex pre-Hilbert space is a vector space over a subfield of CC. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CPreHil -> F = (ℂfld ↾s K ) )
Theorem	cphsubrg 21357	The scalar field of a complex pre-Hilbert space is a subring of CC. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CPreHil -> K e. (SubRing ` ℂfld ) )
Theorem	cphreccl 21358	The scalar field of a complex 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 21359	The scalar field of a complex 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 21360	The scalar field of a complex 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	cphsqrcl 21361	The scalar field of a complex 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 21362	The scalar field of a complex 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	cphsqrcl2 21363	The scalar field of a complex 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	cphsqrcl3 21364	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 21365	The scalar field of a complex 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 21366	A complex pre-Hilbert space is a complex module. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ( W e. CPreHil -> W e. CMod )
Theorem	cphnmvs 21367	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 21368	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 21369*	The value of the norm in a complex 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 21370	The square of the norm is the norm of an inner product in a normed 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 21371	The square of the norm is the norm of an inner product in a normed 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 ) ^ 2 ) = ( A ., A ) )
Theorem	cphnmf 21372	The norm of a vector is a member of the scalar field in a complex 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 21373	The norm of a vector is a member of the scalar field in a complex 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 21374	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 21375	The inner product in a complex 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 21376	Conjugate of an inner product in a complex pre-Hilbert space. Complex version of ipcj 18431. (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	cphorthcom 21377	Orthogonality (meaning inner product is 0) is commutative. Complex version of iporthcom 18432. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   =>    |- ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( A ., B ) = 0 <-> ( B ., A ) = 0 ) )
Theorem	cphip0l 21378	Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. Complex version of ip0l 18433. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. CPreHil /\ A e. V ) -> ( .0. ., A ) = 0 )
Theorem	cphip0r 21379	Inner product with a zero second argument. Complex version of ip0r 18434. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. CPreHil /\ A e. V ) -> ( A ., .0. ) = 0 )
Theorem	cphipeq0 21380	The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. Complex version of ipeq0 18435. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. CPreHil /\ A e. V ) -> ( ( A ., A ) = 0 <-> A = .0. ) )
Theorem	cphdir 21381	Distributive law for inner product (right-distributivity). Equation I3 of [Ponnusamy] p. 362. Complex version of ipdir 18436. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .+ B ) ., C ) = ( ( A ., C ) + ( B ., C ) ) )
Theorem	cphdi 21382	Distributive law for inner product (left-distributivity). Complex version of ipdi 18437. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .+ C ) ) = ( ( A ., B ) + ( A ., C ) ) )
Theorem	cph2di 21383	Distributive law for inner product. Complex version of ip2di 18438. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- ( ph -> W e. CPreHil )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( ( A .+ B ) ., ( C .+ D ) ) = ( ( ( A ., C ) + ( B ., D ) ) + ( ( A ., D ) + ( B ., C ) ) ) )
Theorem	cphsubdir 21384	Distributive law for inner product subtraction. Complex version of ipsubdir 18439. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .- = ( -g ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) ., C ) = ( ( A ., C ) - ( B ., C ) ) )
Theorem	cphsubdi 21385	Distributive law for inner product subtraction. Complex version of ipsubdi 18440. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .- = ( -g ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .- C ) ) = ( ( A ., B ) - ( A ., C ) ) )
Theorem	cph2subdi 21386	Distributive law for inner product subtraction. Complex version of ip2subdi 18441. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- ( ph -> W e. CPreHil )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( ( A .- B ) ., ( C .- D ) ) = ( ( ( A ., C ) + ( B ., D ) ) - ( ( A ., D ) + ( B ., C ) ) ) )
Theorem	cphass 21387	Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. See ipass 18442, his5 25667. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( A .x. B ) ., C ) = ( A x. ( B ., C ) ) )
Theorem	cphassr 21388	"Associative" law for second argument of inner product (compare cphass 21387). See ipassr 18443, his52 . (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( B ., ( A .x. C ) ) = ( ( * ` A ) x. ( B ., C ) ) )
Theorem	cph2ass 21389	Move scalar multiplication to outside of inner product. See his35 25669. (Contributed by Mario Carneiro, 17-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .x. C ) ., ( B .x. D ) ) = ( ( A x. ( * ` B ) ) x. ( C ., D ) ) )
Theorem	tchex 21390*	Lemma for tchbas 21392 and similar theorems. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- V = ( Base ` W )   =>    |- ( x e. V |-> ( sqr ` ( x ., x ) ) ) e. _V
Theorem	tchval 21391*	Define a function to augment a pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- G = (toCHil ` W )   &    |- V = ( Base ` W )   &    |- ., = ( .i ` W )   =>    |- G = ( W toNrmGrp ( x e. V |-> ( sqr ` ( x ., x ) ) ) )
Theorem	tchbas 21392	The base set of a pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- V = ( Base ` W )   =>    |- V = ( Base ` G )
Theorem	tchplusg 21393	The addition operation of a pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- .+ = ( +g ` W )   =>    |- .+ = ( +g ` G )
Theorem	tchsub 21394	The subtraction operation of a pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- G = (toCHil ` W )   &    |- .- = ( -g ` W )   =>    |- .- = ( -g ` G )
Theorem	tchmulr 21395	The ring operation of a pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- .x. = ( .r ` W )   =>    |- .x. = ( .r ` G )
Theorem	tchsca 21396	The scalar field of a pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- F = (Scalar ` W )   =>    |- F = (Scalar ` G )
Theorem	tchvsca 21397	The scalar multiplication of a pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- .x. = ( .s ` W )   =>    |- .x. = ( .s ` G )
Theorem	tchip 21398	The inner product of a pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- .x. = ( .i ` W )   =>    |- .x. = ( .i ` G )
Theorem	tchtopn 21399	The topology of a pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- D = ( dist ` G )   &    |- J = ( TopOpen ` G )   =>    |- ( W e. V -> J = ( MetOpen ` D ) )
Theorem	tchphl 21400	Augmentation of a pre-Hilbert space with a norm does not affect whether it is still a pre-Hilbert space because all the original components are the same. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   =>    |- ( W e. PreHil <-> G e. PreHil )