![]() |
Metamath
Proof Explorer Theorem List (p. 216 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | psgninv 21501 | 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 21502 | Multiplicativity of the permutation sign function. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (pmSgnβπ·) & β’ π = (Baseβπ) β β’ ((π· β Fin β§ πΉ β π β§ πΊ β π) β (πβ(πΉ β πΊ)) = ((πβπΉ) Β· (πβπΊ))) | ||
Theorem | zrhpsgnmhm 21503 | 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 21504 | 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 21505 | Even permutations are permutations. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) β β’ (pmEvenβπ·) β π | ||
Theorem | psgnevpmb 21506 | 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 21507 | 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 21508 | A permutation which is even has sign 1. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) & β’ π = (pmSgnβπ·) β β’ ((π· β Fin β§ πΉ β (pmEvenβπ·)) β (πβπΉ) = 1) | ||
Theorem | psgnodpmr 21509 | 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 21510 | 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 21511 | 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 21512 | 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 21513 | 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 21514 | 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 21515* | 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 21516 | A transposition is an odd permutation. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) & β’ π = ran (pmTrspβπ·) β β’ ((π· β Fin β§ πΉ β π) β πΉ β (π β (pmEvenβπ·))) | ||
Theorem | psgnfix1 21517* | 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 21518* | 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 21519* | Lemma 1 for psgndif 21521. (Contributed by AV, 27-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = (SymGrpβ(π β {πΎ})) & β’ π = (SymGrpβπ) & β’ π = ran (pmTrspβπ) β β’ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π)) β ((π β Word π β§ (β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))) β π = (π Ξ£g π)))) | ||
Theorem | psgndiflemA 21520* | Lemma 2 for psgndif 21521. (Contributed by AV, 31-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = (SymGrpβ(π β {πΎ})) & β’ π = (SymGrpβπ) & β’ π = ran (pmTrspβπ) β β’ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π ) β (π = ((SymGrpβπ) Ξ£g π) β (-1β(β―βπ)) = (-1β(β―βπ))))) | ||
Theorem | psgndif 21521* | 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 21522* | 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 21523 | Extend class notation with the field of real numbers. |
class βfld | ||
Definition | df-refld 21524 | The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ βfld = (βfld βΎs β) | ||
Theorem | rebase 21525 | The base of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ β = (Baseββfld) | ||
Theorem | remulg 21526 | The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ ((π β β€ β§ π΄ β β) β (π(.gββfld)π΄) = (π Β· π΄)) | ||
Theorem | resubdrg 21527 | 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 21528 | Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ β = (-gββfld) β β’ ((π β β β§ π β β) β (π β π) = (π β π)) | ||
Theorem | replusg 21529 | The addition operation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ + = (+gββfld) | ||
Theorem | remulr 21530 | The multiplication operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ Β· = (.rββfld) | ||
Theorem | re0g 21531 | The zero element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ 0 = (0gββfld) | ||
Theorem | re1r 21532 | The unity element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ 1 = (1rββfld) | ||
Theorem | rele2 21533 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ β€ = (leββfld) | ||
Theorem | relt 21534 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ < = (ltββfld) | ||
Theorem | reds 21535 | The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019.) |
β’ (abs β β ) = (distββfld) | ||
Theorem | redvr 21536 | The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π΄(/rββfld)π΅) = (π΄ / π΅)) | ||
Theorem | retos 21537 | The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ βfld β Toset | ||
Theorem | refld 21538 | The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ βfld β Field | ||
Theorem | refldcj 21539 | The conjugation operation of the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ β = (*πββfld) | ||
Theorem | resrng 21540 | 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 21541* | 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 21542 | The quotient group β / β€ is a group. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
β’ π = (βfld /s (βfld ~QG β€)) β β’ π β Grp | ||
Syntax | cphl 21543 | Extend class notation with class of all pre-Hilbert spaces. |
class PreHil | ||
Syntax | cipf 21544 | Extend class notation with inner product function. |
class Β·if | ||
Definition | df-phl 21545* | 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 21546* | 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 21570), while Β·π only has closure (ipcl 21552). (Contributed by Mario Carneiro, 12-Aug-2015.) |
β’ Β·if = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯(Β·πβπ)π¦))) | ||
Theorem | isphl 21547* | 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 21548 | A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β PreHil β π β LVec) | ||
Theorem | phllmod 21549 | A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β PreHil β π β LMod) | ||
Theorem | phlsrng 21550 | The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β PreHil β πΉ β *-Ring) | ||
Theorem | phllmhm 21551* | 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 21552 | Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β PreHil β§ π΄ β π β§ π΅ β π) β (π΄ , π΅) β πΎ) | ||
Theorem | ipcj 21553 | 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 21554 | 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 21555 | 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 21556 | 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 21557 | 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 21558 | 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 21559 | 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 21560 | 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 21561 | 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 21562 | 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 21563 | Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (-gβπΉ) & β’ + = (+gβπΉ) & β’ (π β π β PreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β ((π΄ β π΅) , (πΆ β π·)) = (((π΄ , πΆ) + (π΅ , π·))π((π΄ , π·) + (π΅ , πΆ)))) | ||
Theorem | ipass 21564 | 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 21565 | "Associative" law for second argument of inner product (compare ipass 21564). (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπΉ) & β’ β = (*πβπΉ) β β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β (π΄ , (πΆ Β· π΅)) = ((π΄ , π΅) Γ ( β βπΆ))) | ||
Theorem | ipassr2 21566 | "Associative" law for inner product. Conjugate version of ipassr 21565. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπΉ) & β’ β = (*πβπΉ) β β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β ((π΄ , π΅) Γ πΆ) = (π΄ , (( β βπΆ) Β· π΅))) | ||
Theorem | ipffval 21567* | 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 21568 | The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ Β· = (Β·ifβπ) β β’ ((π β π β§ π β π) β (π Β· π) = (π , π)) | ||
Theorem | ipfeq 21569 | 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 21570 | The inner product operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·ifβπ) β β’ , Fn (π Γ π) | ||
Theorem | phlipf 21571 | The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·ifβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) β β’ (π β PreHil β , :(π Γ π)βΆπΎ) | ||
Theorem | ip2eq 21572* | 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 21573* | 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 21574* | 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 21575 | The inner product on a subspace equals the inner product on the parent space. (Contributed by AV, 19-Oct-2021.) |
β’ π = (π βΎs π) & β’ , = (Β·πβπ) & β’ π = (Β·πβπ) β β’ (π β π β π = , ) | ||
Theorem | phssipval 21576 | 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 21577 | 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 21578 | 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 21579 | Extend class notation with orthocomplement of a subset. |
class ocv | ||
Syntax | ccss 21580 | Extend class notation with set of closed subspaces. |
class ClSubSp | ||
Syntax | cthl 21581 | Extend class notation with the Hilbert lattice. |
class toHL | ||
Definition | df-ocv 21582* | 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 21583* | 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 21584 | 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 21585* | The orthocomplement operation. (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ 0 = (0gβπΉ) & β’ β₯ = (ocvβπ) β β’ (π β π β β₯ = (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 })) | ||
Theorem | ocvval 21586* | 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 21587* | 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 21588 | 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 21589 | The orthocomplement of a subset is a subset of the base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ β₯ = (ocvβπ) β β’ ( β₯ βπ) β π | ||
Theorem | ocvocv 21590 | A set is contained in its double orthocomplement. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ β₯ = (ocvβπ) β β’ ((π β PreHil β§ π β π) β π β ( β₯ β( β₯ βπ))) | ||
Theorem | ocvlss 21591 | 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 21592 | Orthocomplements reverse subset inclusion. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ β₯ = (ocvβπ) β β’ (π β π β ( β₯ βπ) β ( β₯ βπ)) | ||
Theorem | ocvin 21593 | An orthocomplement has trivial intersection with the original subspace. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ β₯ = (ocvβπ) & β’ πΏ = (LSubSpβπ) & β’ 0 = (0gβπ) β β’ ((π β PreHil β§ π β πΏ) β (π β© ( β₯ βπ)) = { 0 }) | ||
Theorem | ocvsscon 21594 | Two ways to say that π and π are orthogonal subspaces. (Contributed by Mario Carneiro, 23-Oct-2015.) |
β’ π = (Baseβπ) & β’ β₯ = (ocvβπ) β β’ ((π β PreHil β§ π β π β§ π β π) β (π β ( β₯ βπ) β π β ( β₯ βπ))) | ||
Theorem | ocvlsp 21595 | The orthocomplement of a linear span. (Contributed by Mario Carneiro, 23-Oct-2015.) |
β’ π = (Baseβπ) & β’ β₯ = (ocvβπ) & β’ π = (LSpanβπ) β β’ ((π β PreHil β§ π β π) β ( β₯ β(πβπ)) = ( β₯ βπ)) | ||
Theorem | ocv0 21596 | The orthocomplement of the empty set. (Contributed by Mario Carneiro, 23-Oct-2015.) |
β’ π = (Baseβπ) & β’ β₯ = (ocvβπ) β β’ ( β₯ ββ ) = π | ||
Theorem | ocvz 21597 | The orthocomplement of the zero subspace. (Contributed by Mario Carneiro, 23-Oct-2015.) |
β’ π = (Baseβπ) & β’ β₯ = (ocvβπ) & β’ 0 = (0gβπ) β β’ (π β PreHil β ( β₯ β{ 0 }) = π) | ||
Theorem | ocv1 21598 | The orthocomplement of the base set. (Contributed by Mario Carneiro, 23-Oct-2015.) |
β’ π = (Baseβπ) & β’ β₯ = (ocvβπ) & β’ 0 = (0gβπ) β β’ (π β PreHil β ( β₯ βπ) = { 0 }) | ||
Theorem | unocv 21599 | The orthocomplement of a union. (Contributed by Mario Carneiro, 23-Oct-2015.) |
β’ β₯ = (ocvβπ) β β’ ( β₯ β(π΄ βͺ π΅)) = (( β₯ βπ΄) β© ( β₯ βπ΅)) | ||
Theorem | iunocv 21600* | The orthocomplement of an indexed union. (Contributed by Mario Carneiro, 23-Oct-2015.) |
β’ β₯ = (ocvβπ) & β’ π = (Baseβπ) β β’ ( β₯ ββͺ π₯ β π΄ π΅) = (π β© β© π₯ β π΄ ( β₯ βπ΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |