Home | Metamath
Proof Explorer Theorem List (p. 210 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cygth 20901* | The "fundamental theorem of cyclic groups". Cyclic groups are exactly the additive groups β€ / πβ€, for 0 β€ π (where π = 0 is the infinite cyclic group β€), up to isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (πΊ β CycGrp β βπ β β0 πΊ βπ (β€/nβ€βπ)) | ||
Theorem | cyggic 20902 | Cyclic groups are isomorphic precisely when they have the same order. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = (Baseβπ») β β’ ((πΊ β CycGrp β§ π» β CycGrp) β (πΊ βπ π» β π΅ β πΆ)) | ||
Theorem | frgpcyg 20903 | A free group is cyclic iff it has zero or one generator. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 18-Apr-2021.) |
β’ πΊ = (freeGrpβπΌ) β β’ (πΌ βΌ 1o β πΊ β CycGrp) | ||
Theorem | cnmsgnsubg 20904 | The signs form a multiplicative subgroup of the complex numbers. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
β’ π = ((mulGrpββfld) βΎs (β β {0})) β β’ {1, -1} β (SubGrpβπ) | ||
Theorem | cnmsgnbas 20905 | The base set of the sign subgroup of the complex numbers. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
β’ π = ((mulGrpββfld) βΎs {1, -1}) β β’ {1, -1} = (Baseβπ) | ||
Theorem | cnmsgngrp 20906 | The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
β’ π = ((mulGrpββfld) βΎs {1, -1}) β β’ π β Grp | ||
Theorem | psgnghm 20907 | The sign is a homomorphism from the finitary permutation group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
β’ π = (SymGrpβπ·) & β’ π = (pmSgnβπ·) & β’ πΉ = (π βΎs dom π) & β’ π = ((mulGrpββfld) βΎs {1, -1}) β β’ (π· β π β π β (πΉ GrpHom π)) | ||
Theorem | psgnghm2 20908 | The sign is a homomorphism from the finite symmetric group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
β’ π = (SymGrpβπ·) & β’ π = (pmSgnβπ·) & β’ π = ((mulGrpββfld) βΎs {1, -1}) β β’ (π· β Fin β π β (π GrpHom π)) | ||
Theorem | psgninv 20909 | The sign of a permutation equals the sign of the inverse of the permutation. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (pmSgnβπ·) & β’ π = (Baseβπ) β β’ ((π· β Fin β§ πΉ β π) β (πββ‘πΉ) = (πβπΉ)) | ||
Theorem | psgnco 20910 | Multiplicativity of the permutation sign function. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (pmSgnβπ·) & β’ π = (Baseβπ) β β’ ((π· β Fin β§ πΉ β π β§ πΊ β π) β (πβ(πΉ β πΊ)) = ((πβπΉ) Β· (πβπΊ))) | ||
Theorem | zrhpsgnmhm 20911 | Embedding of permutation signs into an arbitrary ring is a homomorphism. (Contributed by SO, 9-Jul-2018.) |
β’ ((π β Ring β§ π΄ β Fin) β ((β€RHomβπ ) β (pmSgnβπ΄)) β ((SymGrpβπ΄) MndHom (mulGrpβπ ))) | ||
Theorem | zrhpsgninv 20912 | The embedded sign of a permutation equals the embedded sign of the inverse of the permutation. (Contributed by SO, 9-Jul-2018.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = (β€RHomβπ ) & β’ π = (pmSgnβπ) β β’ ((π β Ring β§ π β Fin β§ πΉ β π) β ((π β π)ββ‘πΉ) = ((π β π)βπΉ)) | ||
Theorem | evpmss 20913 | Even permutations are permutations. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) β β’ (pmEvenβπ·) β π | ||
Theorem | psgnevpmb 20914 | A class is an even permutation if it is a permutation with sign 1. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) & β’ π = (pmSgnβπ·) β β’ (π· β Fin β (πΉ β (pmEvenβπ·) β (πΉ β π β§ (πβπΉ) = 1))) | ||
Theorem | psgnodpm 20915 | A permutation which is odd (i.e. not even) has sign -1. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) & β’ π = (pmSgnβπ·) β β’ ((π· β Fin β§ πΉ β (π β (pmEvenβπ·))) β (πβπΉ) = -1) | ||
Theorem | psgnevpm 20916 | A permutation which is even has sign 1. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) & β’ π = (pmSgnβπ·) β β’ ((π· β Fin β§ πΉ β (pmEvenβπ·)) β (πβπΉ) = 1) | ||
Theorem | psgnodpmr 20917 | If a permutation has sign -1 it is odd (not even). (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) & β’ π = (pmSgnβπ·) β β’ ((π· β Fin β§ πΉ β π β§ (πβπΉ) = -1) β πΉ β (π β (pmEvenβπ·))) | ||
Theorem | zrhpsgnevpm 20918 | The sign of an even permutation embedded into a ring is the unity element of the ring. (Contributed by SO, 9-Jul-2018.) |
β’ π = (β€RHomβπ ) & β’ π = (pmSgnβπ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β Fin β§ πΉ β (pmEvenβπ)) β ((π β π)βπΉ) = 1 ) | ||
Theorem | zrhpsgnodpm 20919 | The sign of an odd permutation embedded into a ring is the additive inverse of the unity element of the ring. (Contributed by SO, 9-Jul-2018.) |
β’ π = (β€RHomβπ ) & β’ π = (pmSgnβπ) & β’ 1 = (1rβπ ) & β’ π = (Baseβ(SymGrpβπ)) & β’ πΌ = (invgβπ ) β β’ ((π β Ring β§ π β Fin β§ πΉ β (π β (pmEvenβπ))) β ((π β π)βπΉ) = (πΌβ 1 )) | ||
Theorem | cofipsgn 20920 | Composition of any class π and the sign function for a finite permutation. (Contributed by AV, 27-Dec-2018.) (Revised by AV, 3-Jul-2022.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) β β’ ((π β Fin β§ π β π) β ((π β π)βπ) = (πβ(πβπ))) | ||
Theorem | zrhpsgnelbas 20921 | Embedding of permutation signs into a ring results in an element of the ring. (Contributed by AV, 1-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (β€RHomβπ ) β β’ ((π β Ring β§ π β Fin β§ π β π) β (πβ(πβπ)) β (Baseβπ )) | ||
Theorem | zrhcopsgnelbas 20922 | Embedding of permutation signs into a ring results in an element of the ring. (Contributed by AV, 1-Jan-2019.) (Proof shortened by AV, 3-Jul-2022.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (β€RHomβπ ) β β’ ((π β Ring β§ π β Fin β§ π β π) β ((π β π)βπ) β (Baseβπ )) | ||
Theorem | evpmodpmf1o 20923* | The function for performing an even permutation after a fixed odd permutation is one to one onto all odd permutations. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) β β’ ((π· β Fin β§ πΉ β (π β (pmEvenβπ·))) β (π β (pmEvenβπ·) β¦ (πΉ(+gβπ)π)):(pmEvenβπ·)β1-1-ontoβ(π β (pmEvenβπ·))) | ||
Theorem | pmtrodpm 20924 | A transposition is an odd permutation. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) & β’ π = ran (pmTrspβπ·) β β’ ((π· β Fin β§ πΉ β π) β πΉ β (π β (pmEvenβπ·))) | ||
Theorem | psgnfix1 20925* | A permutation of a finite set fixing one element is generated by transpositions not involving the fixed element. (Contributed by AV, 13-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = (SymGrpβ(π β {πΎ})) β β’ ((π β Fin β§ πΎ β π) β (π β {π β π β£ (πβπΎ) = πΎ} β βπ€ β Word π(π βΎ (π β {πΎ})) = (π Ξ£g π€))) | ||
Theorem | psgnfix2 20926* | A permutation of a finite set fixing one element is generated by transpositions not involving the fixed element. (Contributed by AV, 17-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = (SymGrpβ(π β {πΎ})) & β’ π = (SymGrpβπ) & β’ π = ran (pmTrspβπ) β β’ ((π β Fin β§ πΎ β π) β (π β {π β π β£ (πβπΎ) = πΎ} β βπ€ β Word π π = (π Ξ£g π€))) | ||
Theorem | psgndiflemB 20927* | Lemma 1 for psgndif 20929. (Contributed by AV, 27-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = (SymGrpβ(π β {πΎ})) & β’ π = (SymGrpβπ) & β’ π = ran (pmTrspβπ) β β’ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π)) β ((π β Word π β§ (β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))) β π = (π Ξ£g π)))) | ||
Theorem | psgndiflemA 20928* | Lemma 2 for psgndif 20929. (Contributed by AV, 31-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = (SymGrpβ(π β {πΎ})) & β’ π = (SymGrpβπ) & β’ π = ran (pmTrspβπ) β β’ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π ) β (π = ((SymGrpβπ) Ξ£g π) β (-1β(β―βπ)) = (-1β(β―βπ))))) | ||
Theorem | psgndif 20929* | Embedding of permutation signs restricted to a set without a single element into a ring. (Contributed by AV, 31-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (pmSgnβ(π β {πΎ})) β β’ ((π β Fin β§ πΎ β π) β (π β {π β π β£ (πβπΎ) = πΎ} β (πβ(π βΎ (π β {πΎ}))) = (πβπ))) | ||
Theorem | copsgndif 20930* | Embedding of permutation signs restricted to a set without a single element into a ring. (Contributed by AV, 31-Jan-2019.) (Revised by AV, 5-Jul-2022.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (pmSgnβ(π β {πΎ})) β β’ ((π β Fin β§ πΎ β π) β (π β {π β π β£ (πβπΎ) = πΎ} β ((π β π)β(π βΎ (π β {πΎ}))) = ((π β π)βπ))) | ||
Syntax | crefld 20931 | Extend class notation with the field of real numbers. |
class βfld | ||
Definition | df-refld 20932 | The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ βfld = (βfld βΎs β) | ||
Theorem | rebase 20933 | The base of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ β = (Baseββfld) | ||
Theorem | remulg 20934 | The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ ((π β β€ β§ π΄ β β) β (π(.gββfld)π΄) = (π Β· π΄)) | ||
Theorem | resubdrg 20935 | The real numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) (Revised by Thierry Arnoux, 30-Jun-2019.) |
β’ (β β (SubRingββfld) β§ βfld β DivRing) | ||
Theorem | resubgval 20936 | Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ β = (-gββfld) β β’ ((π β β β§ π β β) β (π β π) = (π β π)) | ||
Theorem | replusg 20937 | The addition operation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ + = (+gββfld) | ||
Theorem | remulr 20938 | The multiplication operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ Β· = (.rββfld) | ||
Theorem | re0g 20939 | The zero element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ 0 = (0gββfld) | ||
Theorem | re1r 20940 | The unity element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ 1 = (1rββfld) | ||
Theorem | rele2 20941 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ β€ = (leββfld) | ||
Theorem | relt 20942 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ < = (ltββfld) | ||
Theorem | reds 20943 | The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019.) |
β’ (abs β β ) = (distββfld) | ||
Theorem | redvr 20944 | The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π΄(/rββfld)π΅) = (π΄ / π΅)) | ||
Theorem | retos 20945 | The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ βfld β Toset | ||
Theorem | refld 20946 | The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ βfld β Field | ||
Theorem | refldcj 20947 | The conjugation operation of the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ β = (*πββfld) | ||
Theorem | resrng 20948 | The real numbers form a star ring. (Contributed by Thierry Arnoux, 19-Apr-2019.) (Proof shortened by Thierry Arnoux, 11-Jan-2025.) |
β’ βfld β *-Ring | ||
Theorem | regsumsupp 20949* | The group sum over the real numbers, expressed as a finite sum. (Contributed by Thierry Arnoux, 22-Jun-2019.) (Proof shortened by AV, 19-Jul-2019.) |
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β (βfld Ξ£g πΉ) = Ξ£π₯ β (πΉ supp 0)(πΉβπ₯)) | ||
Theorem | rzgrp 20950 | The quotient group β / β€ is a group. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
β’ π = (βfld /s (βfld ~QG β€)) β β’ π β Grp | ||
Syntax | cphl 20951 | Extend class notation with class of all pre-Hilbert spaces. |
class PreHil | ||
Syntax | cipf 20952 | Extend class notation with inner product function. |
class Β·if | ||
Definition | df-phl 20953* | Define the class of all pre-Hilbert spaces (inner product spaces) over arbitrary fields with involution. (Some textbook definitions are more restrictive and require the field of scalars to be the field of real or complex numbers). (Contributed by NM, 22-Sep-2011.) |
β’ PreHil = {π β LVec β£ [(Baseβπ) / π£][(Β·πβπ) / β][(Scalarβπ) / π](π β *-Ring β§ βπ₯ β π£ ((π¦ β π£ β¦ (π¦βπ₯)) β (π LMHom (ringLModβπ)) β§ ((π₯βπ₯) = (0gβπ) β π₯ = (0gβπ)) β§ βπ¦ β π£ ((*πβπ)β(π₯βπ¦)) = (π¦βπ₯)))} | ||
Definition | df-ipf 20954* | Define the inner product function. Usually we will use Β·π directly instead of Β·if, and they have the same behavior in most cases. The main advantage of Β·if is that it is a guaranteed function (ipffn 20978), while Β·π only has closure (ipcl 20960). (Contributed by Mario Carneiro, 12-Aug-2015.) |
β’ Β·if = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯(Β·πβπ)π¦))) | ||
Theorem | isphl 20955* | The predicate "is a generalized pre-Hilbert (inner product) space". (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ 0 = (0gβπ) & β’ β = (*πβπΉ) & β’ π = (0gβπΉ) β β’ (π β PreHil β (π β LVec β§ πΉ β *-Ring β§ βπ₯ β π ((π¦ β π β¦ (π¦ , π₯)) β (π LMHom (ringLModβπΉ)) β§ ((π₯ , π₯) = π β π₯ = 0 ) β§ βπ¦ β π ( β β(π₯ , π¦)) = (π¦ , π₯)))) | ||
Theorem | phllvec 20956 | A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β PreHil β π β LVec) | ||
Theorem | phllmod 20957 | A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β PreHil β π β LMod) | ||
Theorem | phlsrng 20958 | The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β PreHil β πΉ β *-Ring) | ||
Theorem | phllmhm 20959* | The inner product of a pre-Hilbert space is linear in its left argument. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΊ = (π₯ β π β¦ (π₯ , π΄)) β β’ ((π β PreHil β§ π΄ β π) β πΊ β (π LMHom (ringLModβπΉ))) | ||
Theorem | ipcl 20960 | Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β PreHil β§ π΄ β π β§ π΅ β π) β (π΄ , π΅) β πΎ) | ||
Theorem | ipcj 20961 | Conjugate of an inner product in a pre-Hilbert space. Equation I1 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (*πβπΉ) β β’ ((π β PreHil β§ π΄ β π β§ π΅ β π) β ( β β(π΄ , π΅)) = (π΅ , π΄)) | ||
Theorem | iporthcom 20962 | Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ π = (0gβπΉ) β β’ ((π β PreHil β§ π΄ β π β§ π΅ β π) β ((π΄ , π΅) = π β (π΅ , π΄) = π)) | ||
Theorem | ip0l 20963 | Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. (Contributed by NM, 5-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ π = (0gβπΉ) & β’ 0 = (0gβπ) β β’ ((π β PreHil β§ π΄ β π) β ( 0 , π΄) = π) | ||
Theorem | ip0r 20964 | Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ π = (0gβπΉ) & β’ 0 = (0gβπ) β β’ ((π β PreHil β§ π΄ β π) β (π΄ , 0 ) = π) | ||
Theorem | ipeq0 20965 | 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. (Contributed by NM, 24-Jan-2008.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ π = (0gβπΉ) & β’ 0 = (0gβπ) β β’ ((π β PreHil β§ π΄ β π) β ((π΄ , π΄) = π β π΄ = 0 )) | ||
Theorem | ipdir 20966 | Distributive law for inner product (right-distributivity). Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπΉ) β β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ + π΅) , πΆ) = ((π΄ , πΆ) ⨣ (π΅ , πΆ))) | ||
Theorem | ipdi 20967 | Distributive law for inner product (left-distributivity). (Contributed by NM, 20-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπΉ) β β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ , (π΅ + πΆ)) = ((π΄ , π΅) ⨣ (π΄ , πΆ))) | ||
Theorem | ip2di 20968 | Distributive law for inner product. (Contributed by NM, 17-Apr-2008.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπΉ) & β’ (π β π β PreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β ((π΄ + π΅) , (πΆ + π·)) = (((π΄ , πΆ) ⨣ (π΅ , π·)) ⨣ ((π΄ , π·) ⨣ (π΅ , πΆ)))) | ||
Theorem | ipsubdir 20969 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (-gβπΉ) β β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ β π΅) , πΆ) = ((π΄ , πΆ)π(π΅ , πΆ))) | ||
Theorem | ipsubdi 20970 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (-gβπΉ) β β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ , (π΅ β πΆ)) = ((π΄ , π΅)π(π΄ , πΆ))) | ||
Theorem | ip2subdi 20971 | Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (-gβπΉ) & β’ + = (+gβπΉ) & β’ (π β π β PreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β ((π΄ β π΅) , (πΆ β π·)) = (((π΄ , πΆ) + (π΅ , π·))π((π΄ , π·) + (π΅ , πΆ)))) | ||
Theorem | ipass 20972 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπΉ) β β’ ((π β PreHil β§ (π΄ β πΎ β§ π΅ β π β§ πΆ β π)) β ((π΄ Β· π΅) , πΆ) = (π΄ Γ (π΅ , πΆ))) | ||
Theorem | ipassr 20973 | "Associative" law for second argument of inner product (compare ipass 20972). (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπΉ) & β’ β = (*πβπΉ) β β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β (π΄ , (πΆ Β· π΅)) = ((π΄ , π΅) Γ ( β βπΆ))) | ||
Theorem | ipassr2 20974 | "Associative" law for inner product. Conjugate version of ipassr 20973. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπΉ) & β’ β = (*πβπΉ) β β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β ((π΄ , π΅) Γ πΆ) = (π΄ , (( β βπΆ) Β· π΅))) | ||
Theorem | ipffval 20975* | The inner product operation as a function. (Contributed by Mario Carneiro, 12-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ Β· = (Β·ifβπ) β β’ Β· = (π₯ β π, π¦ β π β¦ (π₯ , π¦)) | ||
Theorem | ipfval 20976 | The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ Β· = (Β·ifβπ) β β’ ((π β π β§ π β π) β (π Β· π) = (π , π)) | ||
Theorem | ipfeq 20977 | If the inner product operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ Β· = (Β·ifβπ) β β’ ( , Fn (π Γ π) β Β· = , ) | ||
Theorem | ipffn 20978 | The inner product operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·ifβπ) β β’ , Fn (π Γ π) | ||
Theorem | phlipf 20979 | The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·ifβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) β β’ (π β PreHil β , :(π Γ π)βΆπΎ) | ||
Theorem | ip2eq 20980* | Two vectors are equal iff their inner products with all other vectors are equal. (Contributed by NM, 24-Jan-2008.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ , = (Β·πβπ) & β’ π = (Baseβπ) β β’ ((π β PreHil β§ π΄ β π β§ π΅ β π) β (π΄ = π΅ β βπ₯ β π (π₯ , π΄) = (π₯ , π΅))) | ||
Theorem | isphld 20981* | Properties that determine a pre-Hilbert (inner product) space. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ (π β π = (Baseβπ)) & β’ (π β + = (+gβπ)) & β’ (π β Β· = ( Β·π βπ)) & β’ (π β πΌ = (Β·πβπ)) & β’ (π β 0 = (0gβπ)) & β’ (π β πΉ = (Scalarβπ)) & β’ (π β πΎ = (BaseβπΉ)) & β’ (π β ⨣ = (+gβπΉ)) & β’ (π β Γ = (.rβπΉ)) & β’ (π β β = (*πβπΉ)) & β’ (π β π = (0gβπΉ)) & β’ (π β π β LVec) & β’ (π β πΉ β *-Ring) & β’ ((π β§ π₯ β π β§ π¦ β π) β (π₯πΌπ¦) β πΎ) & β’ ((π β§ π β πΎ β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (((π Β· π₯) + π¦)πΌπ§) = ((π Γ (π₯πΌπ§)) ⨣ (π¦πΌπ§))) & β’ ((π β§ π₯ β π β§ (π₯πΌπ₯) = π) β π₯ = 0 ) & β’ ((π β§ π₯ β π β§ π¦ β π) β ( β β(π₯πΌπ¦)) = (π¦πΌπ₯)) β β’ (π β π β PreHil) | ||
Theorem | phlpropd 20982* | If two structures have the same components (properties), one is a pre-Hilbert space iff the other one is. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ (π β πΉ = (ScalarβπΎ)) & β’ (π β πΉ = (ScalarβπΏ)) & β’ π = (BaseβπΉ) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(Β·πβπΎ)π¦) = (π₯(Β·πβπΏ)π¦)) β β’ (π β (πΎ β PreHil β πΏ β PreHil)) | ||
Theorem | ssipeq 20983 | The inner product on a subspace equals the inner product on the parent space. (Contributed by AV, 19-Oct-2021.) |
β’ π = (π βΎs π) & β’ , = (Β·πβπ) & β’ π = (Β·πβπ) β β’ (π β π β π = , ) | ||
Theorem | phssipval 20984 | The inner product on a subspace in terms of the inner product on the parent space. (Contributed by NM, 28-Jan-2008.) (Revised by AV, 19-Oct-2021.) |
β’ π = (π βΎs π) & β’ , = (Β·πβπ) & β’ π = (Β·πβπ) & β’ π = (LSubSpβπ) β β’ (((π β PreHil β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π΄ππ΅) = (π΄ , π΅)) | ||
Theorem | phssip 20985 | The inner product (as a function) on a subspace is a restriction of the inner product (as a function) on the parent space. (Contributed by NM, 28-Jan-2008.) (Revised by AV, 19-Oct-2021.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ Β· = (Β·ifβπ) & β’ π = (Β·ifβπ) β β’ ((π β PreHil β§ π β π) β π = ( Β· βΎ (π Γ π))) | ||
Theorem | phlssphl 20986 | A subspace of an inner product space (pre-Hilbert space) is an inner product space. (Contributed by AV, 25-Sep-2022.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β PreHil β§ π β π) β π β PreHil) | ||
Syntax | cocv 20987 | Extend class notation with orthocomplement of a subset. |
class ocv | ||
Syntax | ccss 20988 | Extend class notation with set of closed subspaces. |
class ClSubSp | ||
Syntax | cthl 20989 | Extend class notation with the Hilbert lattice. |
class toHL | ||
Definition | df-ocv 20990* | Define the orthocomplement function in a given set (which usually is a pre-Hilbert space): it associates with a subset its orthogonal subset (which in the case of a closed linear subspace is its orthocomplement). (Contributed by NM, 7-Oct-2011.) |
β’ ocv = (β β V β¦ (π β π« (Baseββ) β¦ {π₯ β (Baseββ) β£ βπ¦ β π (π₯(Β·πββ)π¦) = (0gβ(Scalarββ))})) | ||
Definition | df-css 20991* | Define the set of closed (linear) subspaces of a given pre-Hilbert space. (Contributed by NM, 7-Oct-2011.) |
β’ ClSubSp = (β β V β¦ {π β£ π = ((ocvββ)β((ocvββ)βπ ))}) | ||
Definition | df-thl 20992 | Define the Hilbert lattice of closed subspaces of a given pre-Hilbert space. (Contributed by Mario Carneiro, 25-Oct-2015.) |
β’ toHL = (β β V β¦ ((toIncβ(ClSubSpββ)) sSet β¨(ocβndx), (ocvββ)β©)) | ||
Theorem | ocvfval 20993* | The orthocomplement operation. (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ 0 = (0gβπΉ) & β’ β₯ = (ocvβπ) β β’ (π β π β β₯ = (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 })) | ||
Theorem | ocvval 20994* | Value of the orthocomplement of a subset (normally a subspace) of a pre-Hilbert space. (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ 0 = (0gβπΉ) & β’ β₯ = (ocvβπ) β β’ (π β π β ( β₯ βπ) = {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) | ||
Theorem | elocv 20995* | Elementhood in the orthocomplement of a subset (normally a subspace) of a pre-Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ 0 = (0gβπΉ) & β’ β₯ = (ocvβπ) β β’ (π΄ β ( β₯ βπ) β (π β π β§ π΄ β π β§ βπ₯ β π (π΄ , π₯) = 0 )) | ||
Theorem | ocvi 20996 | Property of a member of the orthocomplement of a subset. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ 0 = (0gβπΉ) & β’ β₯ = (ocvβπ) β β’ ((π΄ β ( β₯ βπ) β§ π΅ β π) β (π΄ , π΅) = 0 ) | ||
Theorem | ocvss 20997 | The orthocomplement of a subset is a subset of the base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ β₯ = (ocvβπ) β β’ ( β₯ βπ) β π | ||
Theorem | ocvocv 20998 | A set is contained in its double orthocomplement. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ β₯ = (ocvβπ) β β’ ((π β PreHil β§ π β π) β π β ( β₯ β( β₯ βπ))) | ||
Theorem | ocvlss 20999 | The orthocomplement of a subset is a linear subspace of the pre-Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ β₯ = (ocvβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β PreHil β§ π β π) β ( β₯ βπ) β πΏ) | ||
Theorem | ocv2ss 21000 | Orthocomplements reverse subset inclusion. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ β₯ = (ocvβπ) β β’ (π β π β ( β₯ βπ) β ( β₯ βπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |