![]() |
Metamath
Proof Explorer Theorem List (p. 248 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cphabscl 24701 | 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 24702 | 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 24703 | 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 24704 | 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 24705 | A subcomplex pre-Hilbert space is a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ (π β βPreHil β π β βMod) | ||
Theorem | cphnmvs 24706 | Norm of a scalar product. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β βPreHil β§ π β πΎ β§ π β π) β (πβ(π Β· π)) = ((absβπ) Β· (πβπ))) | ||
Theorem | cphipcl 24707 | An inner product is a member of the complex numbers. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ ((π β βPreHil β§ π΄ β π β§ π΅ β π) β (π΄ , π΅) β β) | ||
Theorem | cphnmfval 24708* | 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 24709 | 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 24710 | 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 24711 | 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 24712 | 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 24713 | An inner product of an element with itself is real. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ ((π β βPreHil β§ π΄ β π) β (π΄ , π΄) β β) | ||
Theorem | ipge0 24714 | The inner product in a subcomplex pre-Hilbert space is positive definite. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ ((π β βPreHil β§ π΄ β π) β 0 β€ (π΄ , π΄)) | ||
Theorem | cphipcj 24715 | Conjugate of an inner product in a subcomplex pre-Hilbert space. Complex version of ipcj 21186. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) β β’ ((π β βPreHil β§ π΄ β π β§ π΅ β π) β (ββ(π΄ , π΅)) = (π΅ , π΄)) | ||
Theorem | cphipipcj 24716 | An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (Revised by AV, 19-Oct-2021.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) β β’ ((π β βPreHil β§ π΄ β π β§ π΅ β π) β ((π΄ , π΅) Β· (π΅ , π΄)) = ((absβ(π΄ , π΅))β2)) | ||
Theorem | cphorthcom 24717 | Orthogonality (meaning inner product is 0) is commutative. Complex version of iporthcom 21187. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) β β’ ((π β βPreHil β§ π΄ β π β§ π΅ β π) β ((π΄ , π΅) = 0 β (π΅ , π΄) = 0)) | ||
Theorem | cphip0l 24718 | Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. Complex version of ip0l 21188. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β βPreHil β§ π΄ β π) β ( 0 , π΄) = 0) | ||
Theorem | cphip0r 24719 | Inner product with a zero second argument. Complex version of ip0r 21189. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β βPreHil β§ π΄ β π) β (π΄ , 0 ) = 0) | ||
Theorem | cphipeq0 24720 | 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 21190. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β βPreHil β§ π΄ β π) β ((π΄ , π΄) = 0 β π΄ = 0 )) | ||
Theorem | cphdir 24721 | Distributive law for inner product (right-distributivity). Equation I3 of [Ponnusamy] p. 362. Complex version of ipdir 21191. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β βPreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ + π΅) , πΆ) = ((π΄ , πΆ) + (π΅ , πΆ))) | ||
Theorem | cphdi 24722 | Distributive law for inner product (left-distributivity). Complex version of ipdi 21192. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β βPreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ , (π΅ + πΆ)) = ((π΄ , π΅) + (π΄ , πΆ))) | ||
Theorem | cph2di 24723 | Distributive law for inner product. Complex version of ip2di 21193. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β ((π΄ + π΅) , (πΆ + π·)) = (((π΄ , πΆ) + (π΅ , π·)) + ((π΄ , π·) + (π΅ , πΆ)))) | ||
Theorem | cphsubdir 24724 | Distributive law for inner product subtraction. Complex version of ipsubdir 21194. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) β β’ ((π β βPreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ β π΅) , πΆ) = ((π΄ , πΆ) β (π΅ , πΆ))) | ||
Theorem | cphsubdi 24725 | Distributive law for inner product subtraction. Complex version of ipsubdi 21195. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) β β’ ((π β βPreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ , (π΅ β πΆ)) = ((π΄ , π΅) β (π΄ , πΆ))) | ||
Theorem | cph2subdi 24726 | Distributive law for inner product subtraction. Complex version of ip2subdi 21196. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β ((π΄ β π΅) , (πΆ β π·)) = (((π΄ , πΆ) + (π΅ , π·)) β ((π΄ , π·) + (π΅ , πΆ)))) | ||
Theorem | cphass 24727 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. See ipass 21197, his5 30334. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) β β’ ((π β βPreHil β§ (π΄ β πΎ β§ π΅ β π β§ πΆ β π)) β ((π΄ Β· π΅) , πΆ) = (π΄ Β· (π΅ , πΆ))) | ||
Theorem | cphassr 24728 | "Associative" law for second argument of inner product (compare cphass 24727). See ipassr 21198, his52 . (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) β β’ ((π β βPreHil β§ (π΄ β πΎ β§ π΅ β π β§ πΆ β π)) β (π΅ , (π΄ Β· πΆ)) = ((ββπ΄) Β· (π΅ , πΆ))) | ||
Theorem | cph2ass 24729 | Move scalar multiplication to outside of inner product. See his35 30336. (Contributed by Mario Carneiro, 17-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) β β’ ((π β βPreHil β§ (π΄ β πΎ β§ π΅ β πΎ) β§ (πΆ β π β§ π· β π)) β ((π΄ Β· πΆ) , (π΅ Β· π·)) = ((π΄ Β· (ββπ΅)) Β· (πΆ , π·))) | ||
Theorem | cphassi 24730 | 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 24731 | "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 24732 | 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 24733* | Lemma for tcphbas 24735 and similar theorems. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) β β’ (π₯ β π β¦ (ββ(π₯ , π₯))) β V | ||
Theorem | tcphval 24734* | 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 24735 | 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 24736 | 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 24737 | 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 24738 | 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 24739 | 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 24740 | The scalar multiplication of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ Β· = ( Β·π βπ) β β’ Β· = ( Β·π βπΊ) | ||
Theorem | tcphip 24741 | The inner product of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ Β· = (Β·πβπ) β β’ Β· = (Β·πβπΊ) | ||
Theorem | tcphtopn 24742 | 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 24743 | 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 24744* | 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 24745 | 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 24746 | 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 24747 | 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 24748 | 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 24749 | Lemma for tcphcph 24753: 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 24750* | The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space built from a pre-Hilbert space with certain properties. The main theorem is ipcau 24754. (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ π = (normβπΊ) & β’ πΆ = ((π , π) / (π , π)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (absβ(π , π)) β€ ((πβπ) Β· (πβπ))) | ||
Theorem | tcphcphlem1 24751* | Lemma for tcphcph 24753: the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ β = (-gβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ββ((π β π) , (π β π))) β€ ((ββ(π , π)) + (ββ(π , π)))) | ||
Theorem | tcphcphlem2 24752* | Lemma for tcphcph 24753: homogeneity. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ (π β π β πΎ) & β’ (π β π β π) β β’ (π β (ββ((π Β· π) , (π Β· π))) = ((absβπ) Β· (ββ(π , π)))) | ||
Theorem | tcphcph 24753* | 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 24754 | 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 24755 | Lemma for nmpar 24756. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ π = (normβπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (((πβ(π΄ + π΅))β2) + ((πβ(π΄ β π΅))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | nmpar 24756 | 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 24757 | 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 24758 | Four times the inner product value cphipval2 24757. (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 24759* | 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 24760 | 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 24761* | 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 24762 | 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 24763* | Continuity of inner product; analogue of cnmpt12f 23169 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 24764* | Continuity of inner product; analogue of cnmpt22f 23178 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 24765 | 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 24766 | 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 24767 | 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) | ||
Syntax | ccfil 24768 | Extend class notation with the class of Cauchy filters. |
class CauFil | ||
Syntax | ccau 24769 | Extend class notation with the class of Cauchy sequences. |
class Cau | ||
Syntax | ccmet 24770 | Extend class notation with the class of complete metrics. |
class CMet | ||
Definition | df-cfil 24771* | Define the set of Cauchy filters on a given extended metric space. A Cauchy filter is a filter on the set such that for every 0 < π₯ there is an element of the filter whose metric diameter is less than π₯. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ CauFil = (π β βͺ ran βMet β¦ {π β (Filβdom dom π) β£ βπ₯ β β+ βπ¦ β π (π β (π¦ Γ π¦)) β (0[,)π₯)}) | ||
Definition | df-cau 24772* | Define the set of Cauchy sequences on a given extended metric space. (Contributed by NM, 8-Sep-2006.) |
β’ Cau = (π β βͺ ran βMet β¦ {π β (dom dom π βpm β) β£ βπ₯ β β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯)}) | ||
Definition | df-cmet 24773* | Define the set of complete metrics on a given set. (Contributed by Mario Carneiro, 1-May-2014.) |
β’ CMet = (π₯ β V β¦ {π β (Metβπ₯) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β }) | ||
Theorem | lmmbr 24774* | Express the binary relation "sequence πΉ converges to point π " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition πΉ β (β Γ π) allows to use objects more general than sequences when convenient; see the comment in df-lm 22732. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) | ||
Theorem | lmmbr2 24775* | Express the binary relation "sequence πΉ converges to point π " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition πΉ β (β Γ π) allows to use objects more general than sequences when convenient; see the comment in df-lm 22732. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) | ||
Theorem | lmmbr3 24776* | Express the binary relation "sequence πΉ converges to point π " in a metric space using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) | ||
Theorem | lmmcvg 24777* | Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β π β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)(π΄ β π β§ (π΄π·π) < π )) | ||
Theorem | lmmbrf 24778* | Express the binary relation "sequence πΉ converges to point π " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 24775 presupposes that πΉ is a function. (Contributed by NM, 20-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΄π·π) < π₯))) | ||
Theorem | lmnn 24779* | A condition that implies convergence. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ (π β π β π) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((πΉβπ)π·π) < (1 / π)) β β’ (π β πΉ(βπ‘βπ½)π) | ||
Theorem | cfilfval 24780* | The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (CauFilβπ·) = {π β (Filβπ) β£ βπ₯ β β+ βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯)}) | ||
Theorem | iscfil 24781* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) | ||
Theorem | iscfil2 24782* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯))) | ||
Theorem | cfilfil 24783 | A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β πΉ β (Filβπ)) | ||
Theorem | cfili 24784* | Property of a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((πΉ β (CauFilβπ·) β§ π β β+) β βπ₯ β πΉ βπ¦ β π₯ βπ§ β π₯ (π¦π·π§) < π ) | ||
Theorem | cfil3i 24785* | A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·) β§ π β β+) β βπ₯ β π (π₯(ballβπ·)π ) β πΉ) | ||
Theorem | cfilss 24786 | A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β§ (πΊ β (Filβπ) β§ πΉ β πΊ)) β πΊ β (CauFilβπ·)) | ||
Theorem | fgcfil 24787* | The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β ((πfilGenπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) | ||
Theorem | fmcfil 24788* | The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (((π FilMap πΉ)βπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) | ||
Theorem | iscfil3 24789* | A filter is Cauchy iff it contains a ball of any chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ))) | ||
Theorem | cfilfcls 24790 | Similar to ultrafilters (uffclsflim 23534), the cluster points and limit points of a Cauchy filter coincide. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π½ = (MetOpenβπ·) & β’ π = dom dom π· β β’ (πΉ β (CauFilβπ·) β (π½ fClus πΉ) = (π½ fLim πΉ)) | ||
Theorem | caufval 24791* | The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006.) (Revised by Mario Carneiro, 5-Sep-2015.) |
β’ (π· β (βMetβπ) β (Cauβπ·) = {π β (π βpm β) β£ βπ₯ β β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯)}) | ||
Theorem | iscau 24792* | Express the property "πΉ is a Cauchy sequence of metric π·". Part of Definition 1.4-3 of [Kreyszig] p. 28. The condition πΉ β (β Γ π) allows to use objects more general than sequences when convenient; see the comment in df-lm 22732. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ (π· β (βMetβπ) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§ βπ₯ β β+ βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯)))) | ||
Theorem | iscau2 24793* | Express the property "πΉ is a Cauchy sequence of metric π· " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ (π· β (βMetβπ) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§ βπ₯ β β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) | ||
Theorem | iscau3 24794* | Express the Cauchy sequence property in the more conventional three-quantifier form. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π· β (βMetβπ)) & β’ (π β π β β€) β β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)))) | ||
Theorem | iscau4 24795* | Express the property "πΉ is a Cauchy sequence of metric π· " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π· β (βMetβπ)) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β (πΉβπ) = π΅) β β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯)))) | ||
Theorem | iscauf 24796* | Express the property "πΉ is a Cauchy sequence of metric π· " presupposing πΉ is a function. (Contributed by NM, 24-Jul-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π· β (βMetβπ)) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ β (Cauβπ·) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΅π·π΄) < π₯)) | ||
Theorem | caun0 24797 | A metric with a Cauchy sequence cannot be empty. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.) |
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β π β β ) | ||
Theorem | caufpm 24798 | Inclusion of a Cauchy sequence, under our definition. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.) |
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β πΉ β (π βpm β)) | ||
Theorem | caucfil 24799 | A Cauchy sequence predicate can be expressed in terms of the Cauchy filter predicate for a suitably chosen filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (β€β₯βπ) & β’ πΏ = ((π FilMap πΉ)β(β€β₯ β π)) β β’ ((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β (πΉ β (Cauβπ·) β πΏ β (CauFilβπ·))) | ||
Theorem | iscmet 24800* | The property "π· is a complete metric." meaning all Cauchy filters converge to a point in the space. (Contributed by Mario Carneiro, 1-May-2014.) (Revised by Mario Carneiro, 13-Oct-2015.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (CMetβπ) β (π· β (Metβπ) β§ βπ β (CauFilβπ·)(π½ fLim π) β β )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |