HomeTheorem List (p. 217 of 504)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 217 of 504) | < 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-31067) |
Hilbert Space Explorer
(31068-32590) |
Users' Mathboxes
(32591-50390) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cygznlem3 21601* | A cyclic group with 𝑛 elements is isomorphic to ℤ / 𝑛ℤ. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ · = (.g‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ ⟨(𝐿‘𝑚), (𝑚 · 𝑋)⟩) ⇒ ⊢ (𝜑 → 𝐺 ≃𝑔 𝑌) | ||
| Theorem | cygzn 21602 | A cyclic group with 𝑛 elements is isomorphic to ℤ / 𝑛ℤ, and an infinite cyclic group is isomorphic to ℤ / 0ℤ ≈ ℤ. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝐺 ∈ CycGrp → 𝐺 ≃𝑔 𝑌) | ||
| Theorem | cygth 21603* | 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 21604 | Cyclic groups are isomorphic precisely when they have the same order. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = (Base‘𝐻) ⇒ ⊢ ((𝐺 ∈ CycGrp ∧ 𝐻 ∈ CycGrp) → (𝐺 ≃𝑔 𝐻 ↔ 𝐵 ≈ 𝐶)) | ||
| Theorem | frgpcyg 21605 | 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 | freshmansdream 21606 | For a prime number 𝑃, if 𝑋 and 𝑌 are members of a commutative ring 𝑅 of characteristic 𝑃, then ((𝑋 + 𝑌)↑𝑃) = ((𝑋↑𝑃) + (𝑌↑𝑃)). This theorem is sometimes referred to as "the freshman's dream" . (Contributed by Thierry Arnoux, 18-Sep-2023.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ 𝑃 = (chr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝑌)) = ((𝑃 ↑ 𝑋) + (𝑃 ↑ 𝑌))) | ||
| Theorem | frobrhm 21607* | In a commutative ring with prime characteristic, the Frobenius function 𝐹 is a ring endomorphism, thus named the Frobenius endomorphism. (Contributed by Thierry Arnoux, 31-May-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (chr‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑃 ↑ 𝑥)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑃 ∈ ℙ) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑅)) | ||
| Theorem | ofldchr 21608 | The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21-Jan-2018.) (Proof shortened by AV, 6-Oct-2020.) |
| ⊢ (𝐹 ∈ oField → (chr‘𝐹) = 0) | ||
| Theorem | cnmsgnsubg 21609 | 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 21610 | 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 21611 | The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
| ⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1}) ⇒ ⊢ 𝑈 ∈ Grp | ||
| Theorem | psgnghm 21612 | 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 21613 | 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 21614 | 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 21615 | Multiplicativity of the permutation sign function. (Contributed by SO, 9-Jul-2018.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → (𝑁‘(𝐹 ∘ 𝐺)) = ((𝑁‘𝐹) · (𝑁‘𝐺))) | ||
| Theorem | zrhpsgnmhm 21616 | 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 21617 | 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 21618 | Even permutations are permutations. (Contributed by SO, 9-Jul-2018.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) ⇒ ⊢ (pmEven‘𝐷) ⊆ 𝑃 | ||
| Theorem | psgnevpmb 21619 | 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 21620 | 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 21621 | A permutation which is even has sign 1. (Contributed by SO, 9-Jul-2018.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) & ⊢ 𝑁 = (pmSgn‘𝐷) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ (pmEven‘𝐷)) → (𝑁‘𝐹) = 1) | ||
| Theorem | psgnodpmr 21622 | 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 21623 | 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 21624 | 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 21625 | 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 21626 | 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 21627 | 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 21628* | 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 21629 | A transposition is an odd permutation. (Contributed by SO, 9-Jul-2018.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) & ⊢ 𝑇 = ran (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝑃 ∖ (pmEven‘𝐷))) | ||
| Theorem | psgnfix1 21630* | 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 21631* | 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 21632* | Lemma 1 for psgndif 21634. (Contributed by AV, 27-Jan-2019.) |
| ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑍 = (SymGrp‘𝑁) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊)) → ((𝑈 ∈ Word 𝑅 ∧ (♯‘𝑊) = (♯‘𝑈) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → 𝑄 = (𝑍 Σg 𝑈)))) | ||
| Theorem | psgndiflemA 21633* | Lemma 2 for psgndif 21634. (Contributed by AV, 31-Jan-2019.) |
| ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑍 = (SymGrp‘𝑁) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊) ∧ 𝑈 ∈ Word 𝑅) → (𝑄 = ((SymGrp‘𝑁) Σg 𝑈) → (-1↑(♯‘𝑊)) = (-1↑(♯‘𝑈))))) | ||
| Theorem | psgndif 21634* | 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 21635* | 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 21636 | Extend class notation with the field of real numbers. |
| class ℝfld | ||
| Definition | df-refld 21637 | The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
| ⊢ ℝfld = (ℂfld ↾s ℝ) | ||
| Theorem | rebase 21638 | The base of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
| ⊢ ℝ = (Base‘ℝfld) | ||
| Theorem | remulg 21639 | The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
| ⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝑁(.g‘ℝfld)𝐴) = (𝑁 · 𝐴)) | ||
| Theorem | resubdrg 21640 | 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 21641 | Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
| ⊢ − = (-g‘ℝfld) ⇒ ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋 − 𝑌) = (𝑋 − 𝑌)) | ||
| Theorem | replusg 21642 | The addition operation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ + = (+g‘ℝfld) | ||
| Theorem | remulr 21643 | The multiplication operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
| ⊢ · = (.r‘ℝfld) | ||
| Theorem | re0g 21644 | The zero element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
| ⊢ 0 = (0g‘ℝfld) | ||
| Theorem | re1r 21645 | The unity element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
| ⊢ 1 = (1r‘ℝfld) | ||
| Theorem | rele2 21646 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ ≤ = (le‘ℝfld) | ||
| Theorem | relt 21647 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ < = (lt‘ℝfld) | ||
| Theorem | reds 21648 | The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019.) |
| ⊢ (abs ∘ − ) = (dist‘ℝfld) | ||
| Theorem | redvr 21649 | The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴(/r‘ℝfld)𝐵) = (𝐴 / 𝐵)) | ||
| Theorem | retos 21650 | The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
| ⊢ ℝfld ∈ Toset | ||
| Theorem | refld 21651 | The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
| ⊢ ℝfld ∈ Field | ||
| Theorem | refldcj 21652 | The conjugation operation of the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
| ⊢ ∗ = (*𝑟‘ℝfld) | ||
| Theorem | resrng 21653 | 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 21654* | 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 21655 | The quotient group ℝ / ℤ is a group. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
| ⊢ 𝑅 = (ℝfld /s (ℝfld ~QG ℤ)) ⇒ ⊢ 𝑅 ∈ Grp | ||
| Syntax | cphl 21656 | Extend class notation with class of all pre-Hilbert spaces. |
| class PreHil | ||
| Syntax | cipf 21657 | Extend class notation with inner product function. |
| class ·if | ||
| Definition | df-phl 21658* | 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 21659* | 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 21683), while ·𝑖 only has closure (ipcl 21665). (Contributed by Mario Carneiro, 12-Aug-2015.) |
| ⊢ ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦))) | ||
| Theorem | isphl 21660* | 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 21661 | A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
| ⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec) | ||
| Theorem | phllmod 21662 | A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
| ⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) | ||
| Theorem | phlsrng 21663 | The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil → 𝐹 ∈ *-Ring) | ||
| Theorem | phllmhm 21664* | 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 21665 | Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ 𝐾) | ||
| Theorem | ipcj 21666 | 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 21667 | 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 21668 | 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 21669 | 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 21670 | 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 21671 | 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 21672 | 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 21673 | 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 21674 | 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 21675 | 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 21676 | Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝑆 = (-g‘𝐹) & ⊢ + = (+g‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶)))) | ||
| Theorem | ipass 21677 | 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 21678 | "Associative" law for second argument of inner product (compare ipass 21677). (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝐹) & ⊢ ∗ = (*𝑟‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → (𝐴 , (𝐶 · 𝐵)) = ((𝐴 , 𝐵) × ( ∗ ‘𝐶))) | ||
| Theorem | ipassr2 21679 | "Associative" law for inner product. Conjugate version of ipassr 21678. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
| ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝐹) & ⊢ ∗ = (*𝑟‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → ((𝐴 , 𝐵) × 𝐶) = (𝐴 , (( ∗ ‘𝐶) · 𝐵))) | ||
| Theorem | ipffval 21680* | 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 21681 | The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ · = (·if‘𝑊) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 · 𝑌) = (𝑋 , 𝑌)) | ||
| Theorem | ipfeq 21682 | 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 21683 | The inner product operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·if‘𝑊) ⇒ ⊢ , Fn (𝑉 × 𝑉) | ||
| Theorem | phlipf 21684 | The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·if‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑊 ∈ PreHil → , :(𝑉 × 𝑉)⟶𝐾) | ||
| Theorem | ip2eq 21685* | 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 21686* | 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 21687* | 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 21688 | The inner product on a subspace equals the inner product on the parent space. (Contributed by AV, 19-Oct-2021.) |
| ⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑃 = (·𝑖‘𝑋) ⇒ ⊢ (𝑈 ∈ 𝑆 → 𝑃 = , ) | ||
| Theorem | phssipval 21689 | 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 21690 | 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 21691 | 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 21692 | Extend class notation with orthocomplement of a subset. |
| class ocv | ||
| Syntax | ccss 21693 | Extend class notation with set of closed subspaces. |
| class ClSubSp | ||
| Syntax | cthl 21694 | Extend class notation with the Hilbert lattice. |
| class toHL | ||
| Definition | df-ocv 21695* | 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 21696* | 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 21697 | 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 21698* | The orthocomplement operation. (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 13-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐹) & ⊢ ⊥ = (ocv‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → ⊥ = (𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 })) | ||
| Theorem | ocvval 21699* | 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 21700* | 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 )) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |