![]() |
Metamath
Proof Explorer Theorem List (p. 204 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | re0g 20301 | The neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ 0 = (0g‘ℝfld) | ||
Theorem | re1r 20302 | The multiplicative neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ 1 = (1r‘ℝfld) | ||
Theorem | rele2 20303 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ ≤ = (le‘ℝfld) | ||
Theorem | relt 20304 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ < = (lt‘ℝfld) | ||
Theorem | reds 20305 | The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019.) |
⊢ (abs ∘ − ) = (dist‘ℝfld) | ||
Theorem | redvr 20306 | The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴(/r‘ℝfld)𝐵) = (𝐴 / 𝐵)) | ||
Theorem | retos 20307 | The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ ℝfld ∈ Toset | ||
Theorem | refld 20308 | The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ℝfld ∈ Field | ||
Theorem | refldcj 20309 | The conjugation operation of the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ ∗ = (*𝑟‘ℝfld) | ||
Theorem | recrng 20310 | The real numbers form a star ring. (Contributed by Thierry Arnoux, 19-Apr-2019.) |
⊢ ℝfld ∈ *-Ring | ||
Theorem | regsumsupp 20311* | 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 20312 | The quotient group ℝ / ℤ is a group. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
⊢ 𝑅 = (ℝfld /s (ℝfld ~QG ℤ)) ⇒ ⊢ 𝑅 ∈ Grp | ||
Syntax | cphl 20313 | Extend class notation with class of all pre-Hilbert spaces. |
class PreHil | ||
Syntax | cipf 20314 | Extend class notation with inner product function. |
class ·if | ||
Definition | df-phl 20315* | 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 20316* | 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 20340), while ·𝑖 only has closure (ipcl 20322). (Contributed by Mario Carneiro, 12-Aug-2015.) |
⊢ ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦))) | ||
Theorem | isphl 20317* | 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 20318 | A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec) | ||
Theorem | phllmod 20319 | A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) | ||
Theorem | phlsrng 20320 | The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil → 𝐹 ∈ *-Ring) | ||
Theorem | phllmhm 20321* | 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 20322 | Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ 𝐾) | ||
Theorem | ipcj 20323 | 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 20324 | 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 20325 | 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 20326 | 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 20327 | 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 20328 | 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 20329 | 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 20330 | 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 20331 | 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 20332 | 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 20333 | Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝑆 = (-g‘𝐹) & ⊢ + = (+g‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶)))) | ||
Theorem | ipass 20334 | 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 20335 | "Associative" law for second argument of inner product (compare ipass 20334). (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝐹) & ⊢ ∗ = (*𝑟‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → (𝐴 , (𝐶 · 𝐵)) = ((𝐴 , 𝐵) × ( ∗ ‘𝐶))) | ||
Theorem | ipassr2 20336 | "Associative" law for inner product. Conjugate version of ipassr 20335. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝐹) & ⊢ ∗ = (*𝑟‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → ((𝐴 , 𝐵) × 𝐶) = (𝐴 , (( ∗ ‘𝐶) · 𝐵))) | ||
Theorem | ipffval 20337* | 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 20338 | The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ · = (·if‘𝑊) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 · 𝑌) = (𝑋 , 𝑌)) | ||
Theorem | ipfeq 20339 | 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 20340 | The inner product operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·if‘𝑊) ⇒ ⊢ , Fn (𝑉 × 𝑉) | ||
Theorem | phlipf 20341 | The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·if‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑊 ∈ PreHil → , :(𝑉 × 𝑉)⟶𝐾) | ||
Theorem | ip2eq 20342* | 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 20343* | 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 20344* | 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 20345 | The inner product on a subspace equals the inner product on the parent space. (Contributed by AV, 19-Oct-2021.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑃 = (·𝑖‘𝑋) ⇒ ⊢ (𝑈 ∈ 𝑆 → 𝑃 = , ) | ||
Theorem | phssipval 20346 | 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 20347 | 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 20348 | 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 20349 | Extend class notation with orthocomplement of a subset. |
class ocv | ||
Syntax | ccss 20350 | Extend class notation with set of closed subspaces. |
class ClSubSp | ||
Syntax | cthl 20351 | Extend class notation with the Hilbert lattice. |
class toHL | ||
Definition | df-ocv 20352* | 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 20353* | 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 20354 | 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 20355* | The orthocomplement operation. (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐹) & ⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → ⊥ = (𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 })) | ||
Theorem | ocvval 20356* | 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 20357* | 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 20358 | 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 20359 | The orthocomplement of a subset is a subset of the base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ ( ⊥ ‘𝑆) ⊆ 𝑉 | ||
Theorem | ocvocv 20360 | A set is contained in its double orthocomplement. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆))) | ||
Theorem | ocvlss 20361 | 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 20362 | Orthocomplements reverse subset inclusion. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ (𝑇 ⊆ 𝑆 → ( ⊥ ‘𝑆) ⊆ ( ⊥ ‘𝑇)) | ||
Theorem | ocvin 20363 | An orthocomplement has trivial intersection with the original subspace. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ ⊥ = (ocv‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿) → (𝑆 ∩ ( ⊥ ‘𝑆)) = { 0 }) | ||
Theorem | ocvsscon 20364 | Two ways to say that 𝑆 and 𝑇 are orthogonal subspaces. (Contributed by Mario Carneiro, 23-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉) → (𝑆 ⊆ ( ⊥ ‘𝑇) ↔ 𝑇 ⊆ ( ⊥ ‘𝑆))) | ||
Theorem | ocvlsp 20365 | The orthocomplement of a linear span. (Contributed by Mario Carneiro, 23-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘(𝑁‘𝑆)) = ( ⊥ ‘𝑆)) | ||
Theorem | ocv0 20366 | The orthocomplement of the empty set. (Contributed by Mario Carneiro, 23-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ ( ⊥ ‘∅) = 𝑉 | ||
Theorem | ocvz 20367 | The orthocomplement of the zero subspace. (Contributed by Mario Carneiro, 23-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil → ( ⊥ ‘{ 0 }) = 𝑉) | ||
Theorem | ocv1 20368 | The orthocomplement of the base set. (Contributed by Mario Carneiro, 23-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil → ( ⊥ ‘𝑉) = { 0 }) | ||
Theorem | unocv 20369 | The orthocomplement of a union. (Contributed by Mario Carneiro, 23-Oct-2015.) |
⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ ( ⊥ ‘(𝐴 ∪ 𝐵)) = (( ⊥ ‘𝐴) ∩ ( ⊥ ‘𝐵)) | ||
Theorem | iunocv 20370* | The orthocomplement of an indexed union. (Contributed by Mario Carneiro, 23-Oct-2015.) |
⊢ ⊥ = (ocv‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ( ⊥ ‘∪ 𝑥 ∈ 𝐴 𝐵) = (𝑉 ∩ ∩ 𝑥 ∈ 𝐴 ( ⊥ ‘𝐵)) | ||
Theorem | cssval 20371* | The set of closed subspaces of a pre-Hilbert space. (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 13-Oct-2015.) |
⊢ ⊥ = (ocv‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝐶 = {𝑠 ∣ 𝑠 = ( ⊥ ‘( ⊥ ‘𝑠))}) | ||
Theorem | iscss 20372 | The predicate "is a closed subspace" (of a pre-Hilbert space). (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 13-Oct-2015.) |
⊢ ⊥ = (ocv‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → (𝑆 ∈ 𝐶 ↔ 𝑆 = ( ⊥ ‘( ⊥ ‘𝑆)))) | ||
Theorem | cssi 20373 | Property of a closed subspace (of a pre-Hilbert space). (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ⊥ = (ocv‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) ⇒ ⊢ (𝑆 ∈ 𝐶 → 𝑆 = ( ⊥ ‘( ⊥ ‘𝑆))) | ||
Theorem | cssss 20374 | A closed subspace is a subset of the base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) ⇒ ⊢ (𝑆 ∈ 𝐶 → 𝑆 ⊆ 𝑉) | ||
Theorem | iscss2 20375 | It is sufficient to prove that the double orthocomplement is a subset of the target set to show that the set is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → (𝑆 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝑆)) | ||
Theorem | ocvcss 20376 | The orthocomplement of any set is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘𝑆) ∈ 𝐶) | ||
Theorem | cssincl 20377 | The zero subspace is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐶 = (ClSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶) | ||
Theorem | css0 20378 | The zero subspace is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐶 = (ClSubSp‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil → { 0 } ∈ 𝐶) | ||
Theorem | css1 20379 | The whole space is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil → 𝑉 ∈ 𝐶) | ||
Theorem | csslss 20380 | A closed subspace of a pre-Hilbert space is a linear subspace. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐶 = (ClSubSp‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐶) → 𝑆 ∈ 𝐿) | ||
Theorem | lsmcss 20381 | A subset of a pre-Hilbert space whose double orthocomplement has a projection decomposition is a closed subspace. This is the core of the proof that a topologically closed subspace is algebraically closed in a Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐶 = (ClSubSp‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝑆 ⊆ 𝑉) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ (𝑆 ⊕ ( ⊥ ‘𝑆))) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐶) | ||
Theorem | cssmre 20382 | The closed subspaces of a pre-Hilbert space are a Moore system. Unlike many of our other examples of closure systems, this one is not usually an algebraic closure system df-acs 16852: consider the Hilbert space of sequences ℕ⟶ℝ with convergent sum; the subspace of all sequences with finite support is the classic example of a non-closed subspace, but for every finite set of sequences of finite support, there is a finite-dimensional (and hence closed) subspace containing all of the sequences, so if closed subspaces were an algebraic closure system this would violate acsfiel 16917. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil → 𝐶 ∈ (Moore‘𝑉)) | ||
Theorem | mrccss 20383 | The Moore closure corresponding to the system of closed subspaces is the double orthocomplement operation. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) & ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → (𝐹‘𝑆) = ( ⊥ ‘( ⊥ ‘𝑆))) | ||
Theorem | thlval 20384 | Value of the Hilbert lattice. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ 𝐾 = (toHL‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) & ⊢ 𝐼 = (toInc‘𝐶) & ⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑉 → 𝐾 = (𝐼 sSet 〈(oc‘ndx), ⊥ 〉)) | ||
Theorem | thlbas 20385 | Base set of the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ 𝐾 = (toHL‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) ⇒ ⊢ 𝐶 = (Base‘𝐾) | ||
Theorem | thlle 20386 | Ordering on the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ 𝐾 = (toHL‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) & ⊢ 𝐼 = (toInc‘𝐶) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ≤ = (le‘𝐾) | ||
Theorem | thlleval 20387 | Ordering on the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ 𝐾 = (toHL‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐶) → (𝑆 ≤ 𝑇 ↔ 𝑆 ⊆ 𝑇)) | ||
Theorem | thloc 20388 | Orthocomplement on the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ 𝐾 = (toHL‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ ⊥ = (oc‘𝐾) | ||
Syntax | cpj 20389 | Extend class notation with orthogonal projection function. |
class proj | ||
Syntax | chil 20390 | Extend class notation with class of all Hilbert spaces. |
class Hil | ||
Syntax | cobs 20391 | Extend class notation with the set of orthonormal bases. |
class OBasis | ||
Definition | df-pj 20392* | Define orthogonal projection onto a subspace. This is just a wrapping of df-pj1 18754, but we restrict the domain of this function to only total projection functions. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ proj = (ℎ ∈ V ↦ ((𝑥 ∈ (LSubSp‘ℎ) ↦ (𝑥(proj1‘ℎ)((ocv‘ℎ)‘𝑥))) ∩ (V × ((Base‘ℎ) ↑m (Base‘ℎ))))) | ||
Definition | df-hil 20393 | Define class of all Hilbert spaces. Based on Proposition 4.5, p. 176, Gudrun Kalmbach, Quantum Measures and Spaces, Kluwer, Dordrecht, 1998. (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 16-Oct-2015.) |
⊢ Hil = {ℎ ∈ PreHil ∣ dom (proj‘ℎ) = (ClSubSp‘ℎ)} | ||
Definition | df-obs 20394* | Define the set of all orthonormal bases for a pre-Hilbert space. An orthonormal basis is a set of mutually orthogonal vectors with norm 1 and such that the linear span is dense in the whole space. (As this is an "algebraic" definition, before we have topology available, we express this denseness by saying that the double orthocomplement is the whole space, or equivalently, the single orthocomplement is trivial.) (Contributed by Mario Carneiro, 23-Oct-2015.) |
⊢ OBasis = (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})}) | ||
Theorem | pjfval 20395* | The value of the projection function. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) & ⊢ 𝑃 = (proj1‘𝑊) & ⊢ 𝐾 = (proj‘𝑊) ⇒ ⊢ 𝐾 = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) | ||
Theorem | pjdm 20396 | A subspace is in the domain of the projection function iff the subspace admits a projection decomposition of the whole space. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) & ⊢ 𝑃 = (proj1‘𝑊) & ⊢ 𝐾 = (proj‘𝑊) ⇒ ⊢ (𝑇 ∈ dom 𝐾 ↔ (𝑇 ∈ 𝐿 ∧ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉)) | ||
Theorem | pjpm 20397 | The projection map is a partial function from subspaces of the pre-Hilbert space to total operators. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ 𝐾 = (proj‘𝑊) ⇒ ⊢ 𝐾 ∈ ((𝑉 ↑m 𝑉) ↑pm 𝐿) | ||
Theorem | pjfval2 20398* | Value of the projection map with implicit domain. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ ⊥ = (ocv‘𝑊) & ⊢ 𝑃 = (proj1‘𝑊) & ⊢ 𝐾 = (proj‘𝑊) ⇒ ⊢ 𝐾 = (𝑥 ∈ dom 𝐾 ↦ (𝑥𝑃( ⊥ ‘𝑥))) | ||
Theorem | pjval 20399 | Value of the projection map. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ ⊥ = (ocv‘𝑊) & ⊢ 𝑃 = (proj1‘𝑊) & ⊢ 𝐾 = (proj‘𝑊) ⇒ ⊢ (𝑇 ∈ dom 𝐾 → (𝐾‘𝑇) = (𝑇𝑃( ⊥ ‘𝑇))) | ||
Theorem | pjdm2 20400 | A subspace is in the domain of the projection function iff the subspace admits a projection decomposition of the whole space. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ ⊥ = (ocv‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐾 = (proj‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil → (𝑇 ∈ dom 𝐾 ↔ (𝑇 ∈ 𝐿 ∧ (𝑇 ⊕ ( ⊥ ‘𝑇)) = 𝑉))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |