![]() |
Metamath
Proof Explorer Theorem List (p. 250 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ncvsprp 24901 | 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.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β (NrmVec β© βVec) β§ π΄ β πΎ β§ π΅ β π) β (πβ(π΄ Β· π΅)) = ((absβπ΄) Β· (πβπ΅))) | ||
Theorem | ncvsge0 24902 | The norm of a scalar product with a nonnegative real. (Contributed by NM, 1-Jan-2008.) (Revised by AV, 8-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β (NrmVec β© βVec) β§ (π΄ β (πΎ β© β) β§ 0 β€ π΄) β§ π΅ β π) β (πβ(π΄ Β· π΅)) = (π΄ Β· (πβπ΅))) | ||
Theorem | ncvsm1 24903 | The norm of the opposite of a vector. (Contributed by NM, 28-Nov-2006.) (Revised by AV, 8-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) β β’ ((π β (NrmVec β© βVec) β§ π΄ β π) β (πβ(-1 Β· π΄)) = (πβπ΄)) | ||
Theorem | ncvsdif 24904 | The norm of the difference between two vectors. (Contributed by NM, 1-Dec-2006.) (Revised by AV, 8-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) β β’ ((π β (NrmVec β© βVec) β§ π΄ β π β§ π΅ β π) β (πβ(π΄ + (-1 Β· π΅))) = (πβ(π΅ + (-1 Β· π΄)))) | ||
Theorem | ncvspi 24905 | The norm of a vector plus the imaginary scalar product of another. (Contributed by NM, 2-Feb-2007.) (Revised by AV, 8-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β (NrmVec β© βVec) β§ (π΄ β π β§ π΅ β π) β§ i β πΎ) β (πβ(π΄ + (i Β· π΅))) = (πβ(π΅ + (-i Β· π΄)))) | ||
Theorem | ncvs1 24906 | From any nonzero vector of a normed subcomplex vector space, construct a collinear vector whose norm is one. (Contributed by NM, 6-Dec-2007.) (Revised by AV, 8-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) & β’ Β· = ( Β·π βπΊ) & β’ πΉ = (ScalarβπΊ) & β’ πΎ = (BaseβπΉ) β β’ ((πΊ β (NrmVec β© βVec) β§ (π΄ β π β§ π΄ β 0 ) β§ (1 / (πβπ΄)) β πΎ) β (πβ((1 / (πβπ΄)) Β· π΄)) = 1) | ||
Theorem | cnrnvc 24907 | The module of complex numbers (as a module over itself) is a normed vector space over itself. The vector operation is +, and the scalar product is Β·, and the norm function is abs. (Contributed by AV, 9-Oct-2021.) |
β’ πΆ = (ringLModββfld) β β’ πΆ β NrmVec | ||
Theorem | cnncvs 24908 | The module of complex numbers (as a module over itself) is a normed subcomplex vector space. The vector operation is +, the scalar product is Β·, and the norm is abs (see cnnm 24909) . (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 9-Oct-2021.) |
β’ πΆ = (ringLModββfld) β β’ πΆ β (NrmVec β© βVec) | ||
Theorem | cnnm 24909 | The norm of the normed subcomplex vector space of complex numbers is the absolute value. (Contributed by NM, 12-Jan-2008.) (Revised by AV, 9-Oct-2021.) |
β’ πΆ = (ringLModββfld) β β’ (normβπΆ) = abs | ||
Theorem | ncvspds 24910 | 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.) |
β’ π = (normβπΊ) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π· = (distβπΊ) & β’ Β· = ( Β·π βπΊ) β β’ ((πΊ β (NrmVec β© βVec) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (πβ(π΄ + (-1 Β· π΅)))) | ||
Theorem | cnindmet 24911 | The metric induced on the complex numbers. cnmet 24509 proves that it is a metric. The induced metric is identical with the original metric on the complex numbers, see cnfldds 21155 and also cnmet 24509. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by AV, 17-Oct-2021.) |
β’ π = (βfld toNrmGrp abs) β β’ (distβπ) = (abs β β ) | ||
Theorem | cnncvsaddassdemo 24912 | Derive the associative law for complex number addition addass 11201 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.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ + π΅) + πΆ) = (π΄ + (π΅ + πΆ))) | ||
Theorem | cnncvsmulassdemo 24913 | Derive the associative law for complex number multiplication mulass 11202 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.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β ((π΄ Β· π΅) Β· πΆ) = (π΄ Β· (π΅ Β· πΆ))) | ||
Theorem | cnncvsabsnegdemo 24914 | Derive the absolute value of a negative complex number absneg 15229 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.) |
β’ (π΄ β β β (absβ-π΄) = (absβπ΄)) | ||
Syntax | ccph 24915 | Extend class notation with the class of subcomplex pre-Hilbert spaces. |
class βPreHil | ||
Syntax | ctcph 24916 | Function to put a norm on a pre-Hilbert space. |
class toβPreHil | ||
Definition | df-cph 24917* | Define the class of subcomplex pre-Hilbert spaces. By restricting the scalar field to a subfield of βfld closed under square roots of nonnegative reals, we have enough structure to define a norm, with the associated connection to a metric and topology. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ βPreHil = {π€ β (PreHil β© NrmMod) β£ [(Scalarβπ€) / π][(Baseβπ) / π](π = (βfld βΎs π) β§ (β β (π β© (0[,)+β))) β π β§ (normβπ€) = (π₯ β (Baseβπ€) β¦ (ββ(π₯(Β·πβπ€)π₯))))} | ||
Definition | df-tcph 24918* | 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 (see tcphcph 24986). (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ toβPreHil = (π€ β V β¦ (π€ toNrmGrp (π₯ β (Baseβπ€) β¦ (ββ(π₯(Β·πβπ€)π₯))))) | ||
Theorem | iscph 24919* | A subcomplex pre-Hilbert space is exactly a pre-Hilbert space over a subfield of the field of complex numbers closed under square roots of nonnegative reals equipped with a norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π = (normβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βPreHil β ((π β PreHil β§ π β NrmMod β§ πΉ = (βfld βΎs πΎ)) β§ (β β (πΎ β© (0[,)+β))) β πΎ β§ π = (π₯ β π β¦ (ββ(π₯ , π₯))))) | ||
Theorem | cphphl 24920 | A subcomplex pre-Hilbert space is a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β βPreHil β π β PreHil) | ||
Theorem | cphnlm 24921 | A subcomplex pre-Hilbert space is a normed module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β βPreHil β π β NrmMod) | ||
Theorem | cphngp 24922 | A subcomplex pre-Hilbert space is a normed group. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π β βPreHil β π β NrmGrp) | ||
Theorem | cphlmod 24923 | A subcomplex pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β βPreHil β π β LMod) | ||
Theorem | cphlvec 24924 | A subcomplex pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β βPreHil β π β LVec) | ||
Theorem | cphnvc 24925 | A subcomplex pre-Hilbert space is a normed vector space. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ (π β βPreHil β π β NrmVec) | ||
Theorem | cphsubrglem 24926 | Lemma for cphsubrg 24929. (Contributed by Mario Carneiro, 9-Oct-2015.) |
β’ πΎ = (BaseβπΉ) & β’ (π β πΉ = (βfld βΎs π΄)) & β’ (π β πΉ β DivRing) β β’ (π β (πΉ = (βfld βΎs πΎ) β§ πΎ = (π΄ β© β) β§ πΎ β (SubRingββfld))) | ||
Theorem | cphreccllem 24927 | Lemma for cphreccl 24930. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΎ = (BaseβπΉ) & β’ (π β πΉ = (βfld βΎs π΄)) & β’ (π β πΉ β DivRing) β β’ ((π β§ π β πΎ β§ π β 0) β (1 / π) β πΎ) | ||
Theorem | cphsca 24928 | A subcomplex pre-Hilbert space is a vector space over a subfield of βfld. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βPreHil β πΉ = (βfld βΎs πΎ)) | ||
Theorem | cphsubrg 24929 | The scalar field of a subcomplex pre-Hilbert space is a subring of βfld. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βPreHil β πΎ β (SubRingββfld)) | ||
Theorem | cphreccl 24930 | The scalar field of a subcomplex pre-Hilbert space is closed under reciprocal. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ π΄ β πΎ β§ π΄ β 0) β (1 / π΄) β πΎ) | ||
Theorem | cphdivcl 24931 | The scalar field of a subcomplex pre-Hilbert space is closed under reciprocal. (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ (π΄ β πΎ β§ π΅ β πΎ β§ π΅ β 0)) β (π΄ / π΅) β πΎ) | ||
Theorem | cphcjcl 24932 | The scalar field of a subcomplex pre-Hilbert space is closed under conjugation. (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ π΄ β πΎ) β (ββπ΄) β πΎ) | ||
Theorem | cphsqrtcl 24933 | The scalar field of a subcomplex pre-Hilbert space is closed under square roots of nonnegative reals. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ (π΄ β πΎ β§ π΄ β β β§ 0 β€ π΄)) β (ββπ΄) β πΎ) | ||
Theorem | cphabscl 24934 | The scalar field of a subcomplex pre-Hilbert space is closed under the absolute value operation. (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ π΄ β πΎ) β (absβπ΄) β πΎ) | ||
Theorem | cphsqrtcl2 24935 | 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.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ π΄ β πΎ β§ Β¬ -π΄ β β+) β (ββπ΄) β πΎ) | ||
Theorem | cphsqrtcl3 24936 | If the scalar field of a subcomplex pre-Hilbert space contains the imaginary unit i, then it is closed under square roots (i.e., it is quadratically closed). (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ i β πΎ β§ π΄ β πΎ) β (ββπ΄) β πΎ) | ||
Theorem | cphqss 24937 | The scalar field of a subcomplex pre-Hilbert space contains the rational numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βPreHil β β β πΎ) | ||
Theorem | cphclm 24938 | A subcomplex pre-Hilbert space is a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ (π β βPreHil β π β βMod) | ||
Theorem | cphnmvs 24939 | Norm of a scalar product. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ π β πΎ β§ π β π) β (πβ(π Β· π)) = ((absβπ) Β· (πβπ))) | ||
Theorem | cphipcl 24940 | An inner product is a member of the complex numbers. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ ((π β βPreHil β§ π΄ β π β§ π΅ β π) β (π΄ , π΅) β β) | ||
Theorem | cphnmfval 24941* | 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.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π = (normβπ) β β’ (π β βPreHil β π = (π₯ β π β¦ (ββ(π₯ , π₯)))) | ||
Theorem | cphnm 24942 | 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.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π = (normβπ) β β’ ((π β βPreHil β§ π΄ β π) β (πβπ΄) = (ββ(π΄ , π΄))) | ||
Theorem | nmsq 24943 | 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.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π = (normβπ) β β’ ((π β βPreHil β§ π΄ β π) β ((πβπ΄)β2) = (π΄ , π΄)) | ||
Theorem | cphnmf 24944 | 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.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π = (normβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βPreHil β π:πβΆπΎ) | ||
Theorem | cphnmcl 24945 | 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.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π = (normβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ π΄ β π) β (πβπ΄) β πΎ) | ||
Theorem | reipcl 24946 | An inner product of an element with itself is real. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ ((π β βPreHil β§ π΄ β π) β (π΄ , π΄) β β) | ||
Theorem | ipge0 24947 | The inner product in a subcomplex pre-Hilbert space is positive definite. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ ((π β βPreHil β§ π΄ β π) β 0 β€ (π΄ , π΄)) | ||
Theorem | cphipcj 24948 | Conjugate of an inner product in a subcomplex pre-Hilbert space. Complex version of ipcj 21407. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) β β’ ((π β βPreHil β§ π΄ β π β§ π΅ β π) β (ββ(π΄ , π΅)) = (π΅ , π΄)) | ||
Theorem | cphipipcj 24949 | An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (Revised by AV, 19-Oct-2021.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) β β’ ((π β βPreHil β§ π΄ β π β§ π΅ β π) β ((π΄ , π΅) Β· (π΅ , π΄)) = ((absβ(π΄ , π΅))β2)) | ||
Theorem | cphorthcom 24950 | Orthogonality (meaning inner product is 0) is commutative. Complex version of iporthcom 21408. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) β β’ ((π β βPreHil β§ π΄ β π β§ π΅ β π) β ((π΄ , π΅) = 0 β (π΅ , π΄) = 0)) | ||
Theorem | cphip0l 24951 | Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. Complex version of ip0l 21409. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β βPreHil β§ π΄ β π) β ( 0 , π΄) = 0) | ||
Theorem | cphip0r 24952 | Inner product with a zero second argument. Complex version of ip0r 21410. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β βPreHil β§ π΄ β π) β (π΄ , 0 ) = 0) | ||
Theorem | cphipeq0 24953 | 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 21411. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β βPreHil β§ π΄ β π) β ((π΄ , π΄) = 0 β π΄ = 0 )) | ||
Theorem | cphdir 24954 | Distributive law for inner product (right-distributivity). Equation I3 of [Ponnusamy] p. 362. Complex version of ipdir 21412. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β βPreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ + π΅) , πΆ) = ((π΄ , πΆ) + (π΅ , πΆ))) | ||
Theorem | cphdi 24955 | Distributive law for inner product (left-distributivity). Complex version of ipdi 21413. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β βPreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ , (π΅ + πΆ)) = ((π΄ , π΅) + (π΄ , πΆ))) | ||
Theorem | cph2di 24956 | Distributive law for inner product. Complex version of ip2di 21414. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β ((π΄ + π΅) , (πΆ + π·)) = (((π΄ , πΆ) + (π΅ , π·)) + ((π΄ , π·) + (π΅ , πΆ)))) | ||
Theorem | cphsubdir 24957 | Distributive law for inner product subtraction. Complex version of ipsubdir 21415. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) β β’ ((π β βPreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ β π΅) , πΆ) = ((π΄ , πΆ) β (π΅ , πΆ))) | ||
Theorem | cphsubdi 24958 | Distributive law for inner product subtraction. Complex version of ipsubdi 21416. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) β β’ ((π β βPreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ , (π΅ β πΆ)) = ((π΄ , π΅) β (π΄ , πΆ))) | ||
Theorem | cph2subdi 24959 | Distributive law for inner product subtraction. Complex version of ip2subdi 21417. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β ((π΄ β π΅) , (πΆ β π·)) = (((π΄ , πΆ) + (π΅ , π·)) β ((π΄ , π·) + (π΅ , πΆ)))) | ||
Theorem | cphass 24960 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. See ipass 21418, his5 30607. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) β β’ ((π β βPreHil β§ (π΄ β πΎ β§ π΅ β π β§ πΆ β π)) β ((π΄ Β· π΅) , πΆ) = (π΄ Β· (π΅ , πΆ))) | ||
Theorem | cphassr 24961 | "Associative" law for second argument of inner product (compare cphass 24960). See ipassr 21419, his52 . (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) β β’ ((π β βPreHil β§ (π΄ β πΎ β§ π΅ β π β§ πΆ β π)) β (π΅ , (π΄ Β· πΆ)) = ((ββπ΄) Β· (π΅ , πΆ))) | ||
Theorem | cph2ass 24962 | Move scalar multiplication to outside of inner product. See his35 30609. (Contributed by Mario Carneiro, 17-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) β β’ ((π β βPreHil β§ (π΄ β πΎ β§ π΅ β πΎ) β§ (πΆ β π β§ π· β π)) β ((π΄ Β· πΆ) , (π΅ Β· π·)) = ((π΄ Β· (ββπ΅)) Β· (πΆ , π·))) | ||
Theorem | cphassi 24963 | Associative law for the first argument of an inner product with scalar _π. (Contributed by AV, 17-Oct-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (((π β βPreHil β§ i β πΎ) β§ π΄ β π β§ π΅ β π) β ((i Β· π΅) , π΄) = (i Β· (π΅ , π΄))) | ||
Theorem | cphassir 24964 | "Associative" law for the second argument of an inner product with scalar _π. (Contributed by AV, 17-Oct-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (((π β βPreHil β§ i β πΎ) β§ π΄ β π β§ π΅ β π) β (π΄ , (i Β· π΅)) = (-i Β· (π΄ , π΅))) | ||
Theorem | cphpyth 24965 | The pythagorean theorem for a subcomplex pre-Hilbert space. The square of the norm of the sum of two orthogonal vectors (i.e., whose inner product is 0) is the sum of the squares of their norms. Problem 2 in [Kreyszig] p. 135. This is Metamath 100 proof #4. (Contributed by NM, 17-Apr-2008.) (Revised by SN, 22-Sep-2024.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ + = (+gβπ) & β’ π = (normβπ) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ ((π β§ (π΄ , π΅) = 0) β ((πβ(π΄ + π΅))β2) = (((πβπ΄)β2) + ((πβπ΅)β2))) | ||
Theorem | tcphex 24966* | Lemma for tcphbas 24968 and similar theorems. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) β β’ (π₯ β π β¦ (ββ(π₯ , π₯))) β V | ||
Theorem | tcphval 24967* | Define a function to augment a subcomplex pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ πΊ = (π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯)))) | ||
Theorem | tcphbas 24968 | The base set of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) β β’ π = (BaseβπΊ) | ||
Theorem | tchplusg 24969 | The addition operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ + = (+gβπ) β β’ + = (+gβπΊ) | ||
Theorem | tcphsub 24970 | The subtraction operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ πΊ = (toβPreHilβπ) & β’ β = (-gβπ) β β’ β = (-gβπΊ) | ||
Theorem | tcphmulr 24971 | The ring operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ Β· = (.rβπ) β β’ Β· = (.rβπΊ) | ||
Theorem | tcphsca 24972 | The scalar field of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ πΉ = (Scalarβπ) β β’ πΉ = (ScalarβπΊ) | ||
Theorem | tcphvsca 24973 | The scalar multiplication of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ Β· = ( Β·π βπ) β β’ Β· = ( Β·π βπΊ) | ||
Theorem | tcphip 24974 | The inner product of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ Β· = (Β·πβπ) β β’ Β· = (Β·πβπΊ) | ||
Theorem | tcphtopn 24975 | The topology of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π· = (distβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ (π β π β π½ = (MetOpenβπ·)) | ||
Theorem | tcphphl 24976 | Augmentation of a subcomplex 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.) |
β’ πΊ = (toβPreHilβπ) β β’ (π β PreHil β πΊ β PreHil) | ||
Theorem | tchnmfval 24977* | The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (normβπΊ) & β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ (π β Grp β π = (π₯ β π β¦ (ββ(π₯ , π₯)))) | ||
Theorem | tcphnmval 24978 | The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (normβπΊ) & β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ ((π β Grp β§ π β π) β (πβπ) = (ββ(π , π))) | ||
Theorem | cphtcphnm 24979 | The norm of a norm-augmented subcomplex pre-Hilbert space is the same as the original norm on it. (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (normβπ) β β’ (π β βPreHil β π = (normβπΊ)) | ||
Theorem | tcphds 24980 | The distance of a pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (normβπΊ) & β’ β = (-gβπ) β β’ (π β Grp β (π β β ) = (distβπΊ)) | ||
Theorem | phclm 24981 | A pre-Hilbert space whose field of scalars is a restriction of the field of complex numbers is a subcomplex module. TODO: redundant hypotheses. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) β β’ (π β π β βMod) | ||
Theorem | tcphcphlem3 24982 | Lemma for tcphcph 24986: real closure of an inner product of a vector with itself. (Contributed by Mario Carneiro, 10-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) β β’ ((π β§ π β π) β (π , π) β β) | ||
Theorem | ipcau2 24983* | The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space built from a pre-Hilbert space with certain properties. The main theorem is ipcau 24987. (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ π = (normβπΊ) & β’ πΆ = ((π , π) / (π , π)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (absβ(π , π)) β€ ((πβπ) Β· (πβπ))) | ||
Theorem | tcphcphlem1 24984* | Lemma for tcphcph 24986: the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ β = (-gβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ββ((π β π) , (π β π))) β€ ((ββ(π , π)) + (ββ(π , π)))) | ||
Theorem | tcphcphlem2 24985* | Lemma for tcphcph 24986: homogeneity. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ (π β π β πΎ) & β’ (π β π β π) β β’ (π β (ββ((π Β· π) , (π Β· π))) = ((absβπ) Β· (ββ(π , π)))) | ||
Theorem | tcphcph 24986* | The standard definition of a norm turns any pre-Hilbert space over a subfield of βfld closed under square roots of nonnegative reals into a subcomplex pre-Hilbert space (which allows access to a norm, metric, and topology). (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) β β’ (π β πΊ β βPreHil) | ||
Theorem | ipcau 24987 | The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. Part of Lemma 3.2-1(a) of [Kreyszig] p. 137. This is Metamath 100 proof #78. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 11-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π = (normβπ) β β’ ((π β βPreHil β§ π β π β§ π β π) β (absβ(π , π)) β€ ((πβπ) Β· (πβπ))) | ||
Theorem | nmparlem 24988 | Lemma for nmpar 24989. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ π = (normβπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (((πβ(π΄ + π΅))β2) + ((πβ(π΄ β π΅))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | nmpar 24989 | A subcomplex pre-Hilbert space satisfies the parallelogram law. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ π = (normβπ) β β’ ((π β βPreHil β§ π΄ β π β§ π΅ β π) β (((πβ(π΄ + π΅))β2) + ((πβ(π΄ β π΅))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | cphipval2 24990 | Value of the inner product expressed by the norm defined by it. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (normβπ) & β’ , = (Β·πβπ) & β’ β = (-gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (((π β βPreHil β§ i β πΎ) β§ π΄ β π β§ π΅ β π) β (π΄ , π΅) = (((((πβ(π΄ + π΅))β2) β ((πβ(π΄ β π΅))β2)) + (i Β· (((πβ(π΄ + (i Β· π΅)))β2) β ((πβ(π΄ β (i Β· π΅)))β2)))) / 4)) | ||
Theorem | 4cphipval2 24991 | Four times the inner product value cphipval2 24990. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 18-Oct-2021.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (normβπ) & β’ , = (Β·πβπ) & β’ β = (-gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (((π β βPreHil β§ i β πΎ) β§ π΄ β π β§ π΅ β π) β (4 Β· (π΄ , π΅)) = ((((πβ(π΄ + π΅))β2) β ((πβ(π΄ β π΅))β2)) + (i Β· (((πβ(π΄ + (i Β· π΅)))β2) β ((πβ(π΄ β (i Β· π΅)))β2))))) | ||
Theorem | cphipval 24992* | Value of the inner product expressed by a sum of terms with the norm defined by the inner product. Equation 6.45 of [Ponnusamy] p. 361. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (normβπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (((π β βPreHil β§ i β πΎ) β§ π΄ β π β§ π΅ β π) β (π΄ , π΅) = (Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄ + ((iβπ) Β· π΅)))β2)) / 4)) | ||
Theorem | ipcnlem2 24993 | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π· = (distβπ) & β’ π = (normβπ) & β’ π = ((π / 2) / ((πβπ΄) + 1)) & β’ π = ((π / 2) / ((πβπ΅) + π)) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β β+) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π΄π·π) < π) & β’ (π β (π΅π·π) < π) β β’ (π β (absβ((π΄ , π΅) β (π , π))) < π ) | ||
Theorem | ipcnlem1 24994* | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π· = (distβπ) & β’ π = (normβπ) & β’ π = ((π / 2) / ((πβπ΄) + 1)) & β’ π = ((π / 2) / ((πβπ΅) + π)) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β β+) β β’ (π β βπ β β+ βπ₯ β π βπ¦ β π (((π΄π·π₯) < π β§ (π΅π·π¦) < π) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π )) | ||
Theorem | ipcn 24995 | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ , = (Β·ifβπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenββfld) β β’ (π β βPreHil β , β ((π½ Γt π½) Cn πΎ)) | ||
Theorem | cnmpt1ip 24996* | Continuity of inner product; analogue of cnmpt12f 23391 which cannot be used directly because Β·π is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π½ = (TopOpenβπ) & β’ πΆ = (TopOpenββfld) & β’ , = (Β·πβπ) & β’ (π β π β βPreHil) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (πΎ Cn π½)) & β’ (π β (π₯ β π β¦ π΅) β (πΎ Cn π½)) β β’ (π β (π₯ β π β¦ (π΄ , π΅)) β (πΎ Cn πΆ)) | ||
Theorem | cnmpt2ip 24997* | Continuity of inner product; analogue of cnmpt22f 23400 which cannot be used directly because Β·π is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π½ = (TopOpenβπ) & β’ πΆ = (TopOpenββfld) & β’ , = (Β·πβπ) & β’ (π β π β βPreHil) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((πΎ Γt πΏ) Cn π½)) & β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((πΎ Γt πΏ) Cn π½)) β β’ (π β (π₯ β π, π¦ β π β¦ (π΄ , π΅)) β ((πΎ Γt πΏ) Cn πΆ)) | ||
Theorem | csscld 24998 | A "closed subspace" in a subcomplex pre-Hilbert space is actually closed in the topology induced by the norm, thus justifying the terminology "closed subspace". (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ πΆ = (ClSubSpβπ) & β’ π½ = (TopOpenβπ) β β’ ((π β βPreHil β§ π β πΆ) β π β (Clsdβπ½)) | ||
Theorem | clsocv 24999 | The orthogonal complement of the closure of a subset is the same as the orthogonal complement of the subset itself. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ π = (ocvβπ) & β’ π½ = (TopOpenβπ) β β’ ((π β βPreHil β§ π β π) β (πβ((clsβπ½)βπ)) = (πβπ)) | ||
Theorem | cphsscph 25000 | A subspace of a subcomplex pre-Hilbert space is a subcomplex pre-Hilbert space. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 25-Sep-2022.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β βPreHil β§ π β π) β π β βPreHil) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |