Home | Metamath
Proof Explorer Theorem List (p. 208 of 450) | < 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-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | znleval2 20701 | The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = (le‘𝑌) & ⊢ 𝑋 = (Base‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≤ 𝐵 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) | ||
Theorem | zntoslem 20702 | Lemma for zntos 20703. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = (le‘𝑌) & ⊢ 𝑋 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ Toset) | ||
Theorem | zntos 20703 | The ℤ/nℤ structure is a totally ordered set. (The order is not respected by the operations, except in the case 𝑁 = 0 when it coincides with the ordering on ℤ.) (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ Toset) | ||
Theorem | znhash 20704 | The ℤ/nℤ structure has 𝑛 elements. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → (♯‘𝐵) = 𝑁) | ||
Theorem | znfi 20705 | The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin) | ||
Theorem | znfld 20706 | The ℤ/nℤ structure is a finite field when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℙ → 𝑌 ∈ Field) | ||
Theorem | znidomb 20707 | The ℤ/nℤ structure is a domain (and hence a field) precisely when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ → (𝑌 ∈ IDomn ↔ 𝑁 ∈ ℙ)) | ||
Theorem | znchr 20708 | Cyclic rings are defined by their characteristic. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (chr‘𝑌) = 𝑁) | ||
Theorem | znunit 20709 | The units of ℤ/nℤ are the integers coprime to the base. (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝑈 = (Unit‘𝑌) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐴 gcd 𝑁) = 1)) | ||
Theorem | znunithash 20710 | The size of the unit group of ℤ/nℤ. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝑈 = (Unit‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → (♯‘𝑈) = (ϕ‘𝑁)) | ||
Theorem | znrrg 20711 | The regular elements of ℤ/nℤ are exactly the units. (This theorem fails for 𝑁 = 0, where all nonzero integers are regular, but only ±1 are units.) (Contributed by Mario Carneiro, 18-Apr-2016.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝑈 = (Unit‘𝑌) & ⊢ 𝐸 = (RLReg‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐸 = 𝑈) | ||
Theorem | cygznlem1 20712* | Lemma for cygzn 20716. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ · = (.g‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) ⇒ ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝐿‘𝐾) = (𝐿‘𝑀) ↔ (𝐾 · 𝑋) = (𝑀 · 𝑋))) | ||
Theorem | cygznlem2a 20713* | Lemma for cygzn 20716. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ · = (.g‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ 〈(𝐿‘𝑚), (𝑚 · 𝑋)〉) ⇒ ⊢ (𝜑 → 𝐹:(Base‘𝑌)⟶𝐵) | ||
Theorem | cygznlem2 20714* | Lemma for cygzn 20716. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ · = (.g‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ 〈(𝐿‘𝑚), (𝑚 · 𝑋)〉) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → (𝐹‘(𝐿‘𝑀)) = (𝑀 · 𝑋)) | ||
Theorem | cygznlem3 20715* | 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 20716 | 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 20717* | 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 20718 | Cyclic groups are isomorphic precisely when they have the same order. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = (Base‘𝐻) ⇒ ⊢ ((𝐺 ∈ CycGrp ∧ 𝐻 ∈ CycGrp) → (𝐺 ≃𝑔 𝐻 ↔ 𝐵 ≈ 𝐶)) | ||
Theorem | frgpcyg 20719 | 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 20720 | 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 20721 | 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 20722 | The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1}) ⇒ ⊢ 𝑈 ∈ Grp | ||
Theorem | psgnghm 20723 | 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 20724 | 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 20725 | 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 20726 | Multiplicativity of the permutation sign function. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → (𝑁‘(𝐹 ∘ 𝐺)) = ((𝑁‘𝐹) · (𝑁‘𝐺))) | ||
Theorem | zrhpsgnmhm 20727 | 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 20728 | 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 20729 | Even permutations are permutations. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) ⇒ ⊢ (pmEven‘𝐷) ⊆ 𝑃 | ||
Theorem | psgnevpmb 20730 | 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 20731 | 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 20732 | A permutation which is even has sign 1. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) & ⊢ 𝑁 = (pmSgn‘𝐷) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ (pmEven‘𝐷)) → (𝑁‘𝐹) = 1) | ||
Theorem | psgnodpmr 20733 | 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 20734 | The sign of an even permutation embedded into a ring is the multiplicative neutral element of the ring. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ (pmEven‘𝑁)) → ((𝑌 ∘ 𝑆)‘𝐹) = 1 ) | ||
Theorem | zrhpsgnodpm 20735 | The sign of an odd permutation embedded into a ring is the additive inverse of the multiplicative neutral element of the ring. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ (𝑃 ∖ (pmEven‘𝑁))) → ((𝑌 ∘ 𝑆)‘𝐹) = (𝐼‘ 1 )) | ||
Theorem | cofipsgn 20736 | 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 20737 | 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 20738 | 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 20739* | 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 20740 | A transposition is an odd permutation. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) & ⊢ 𝑇 = ran (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝑃 ∖ (pmEven‘𝐷))) | ||
Theorem | psgnfix1 20741* | 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 20742* | 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 20743* | Lemma 1 for psgndif 20745. (Contributed by AV, 27-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑍 = (SymGrp‘𝑁) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊)) → ((𝑈 ∈ Word 𝑅 ∧ (♯‘𝑊) = (♯‘𝑈) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → 𝑄 = (𝑍 Σg 𝑈)))) | ||
Theorem | psgndiflemA 20744* | Lemma 2 for psgndif 20745. (Contributed by AV, 31-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑍 = (SymGrp‘𝑁) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊) ∧ 𝑈 ∈ Word 𝑅) → (𝑄 = ((SymGrp‘𝑁) Σg 𝑈) → (-1↑(♯‘𝑊)) = (-1↑(♯‘𝑈))))) | ||
Theorem | psgndif 20745* | 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 20746* | 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 20747 | Extend class notation with the field of real numbers. |
class ℝfld | ||
Definition | df-refld 20748 | The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ ℝfld = (ℂfld ↾s ℝ) | ||
Theorem | rebase 20749 | The base of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ℝ = (Base‘ℝfld) | ||
Theorem | remulg 20750 | The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝑁(.g‘ℝfld)𝐴) = (𝑁 · 𝐴)) | ||
Theorem | resubdrg 20751 | 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 20752 | Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ − = (-g‘ℝfld) ⇒ ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋 − 𝑌) = (𝑋 − 𝑌)) | ||
Theorem | replusg 20753 | The addition operation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ + = (+g‘ℝfld) | ||
Theorem | remulr 20754 | The multiplication operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ · = (.r‘ℝfld) | ||
Theorem | re0g 20755 | The neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ 0 = (0g‘ℝfld) | ||
Theorem | re1r 20756 | The multiplicative neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ 1 = (1r‘ℝfld) | ||
Theorem | rele2 20757 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ ≤ = (le‘ℝfld) | ||
Theorem | relt 20758 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ < = (lt‘ℝfld) | ||
Theorem | reds 20759 | The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019.) |
⊢ (abs ∘ − ) = (dist‘ℝfld) | ||
Theorem | redvr 20760 | The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴(/r‘ℝfld)𝐵) = (𝐴 / 𝐵)) | ||
Theorem | retos 20761 | The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ ℝfld ∈ Toset | ||
Theorem | refld 20762 | The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ℝfld ∈ Field | ||
Theorem | refldcj 20763 | The conjugation operation of the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ ∗ = (*𝑟‘ℝfld) | ||
Theorem | recrng 20764 | The real numbers form a star ring. (Contributed by Thierry Arnoux, 19-Apr-2019.) |
⊢ ℝfld ∈ *-Ring | ||
Theorem | regsumsupp 20765* | 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 20766 | The quotient group ℝ / ℤ is a group. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
⊢ 𝑅 = (ℝfld /s (ℝfld ~QG ℤ)) ⇒ ⊢ 𝑅 ∈ Grp | ||
Syntax | cphl 20767 | Extend class notation with class of all pre-Hilbert spaces. |
class PreHil | ||
Syntax | cipf 20768 | Extend class notation with inner product function. |
class ·if | ||
Definition | df-phl 20769* | 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 20770* | 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 20794), while ·𝑖 only has closure (ipcl 20776). (Contributed by Mario Carneiro, 12-Aug-2015.) |
⊢ ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦))) | ||
Theorem | isphl 20771* | 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 20772 | A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec) | ||
Theorem | phllmod 20773 | A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) | ||
Theorem | phlsrng 20774 | The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil → 𝐹 ∈ *-Ring) | ||
Theorem | phllmhm 20775* | 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 20776 | Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ 𝐾) | ||
Theorem | ipcj 20777 | 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 20778 | 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 20779 | 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 20780 | 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 20781 | 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 20782 | 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 20783 | 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 20784 | 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 20785 | 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 20786 | 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 20787 | Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝑆 = (-g‘𝐹) & ⊢ + = (+g‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶)))) | ||
Theorem | ipass 20788 | 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 20789 | "Associative" law for second argument of inner product (compare ipass 20788). (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝐹) & ⊢ ∗ = (*𝑟‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → (𝐴 , (𝐶 · 𝐵)) = ((𝐴 , 𝐵) × ( ∗ ‘𝐶))) | ||
Theorem | ipassr2 20790 | "Associative" law for inner product. Conjugate version of ipassr 20789. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝐹) & ⊢ ∗ = (*𝑟‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → ((𝐴 , 𝐵) × 𝐶) = (𝐴 , (( ∗ ‘𝐶) · 𝐵))) | ||
Theorem | ipffval 20791* | 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 20792 | The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ · = (·if‘𝑊) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 · 𝑌) = (𝑋 , 𝑌)) | ||
Theorem | ipfeq 20793 | 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 20794 | The inner product operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·if‘𝑊) ⇒ ⊢ , Fn (𝑉 × 𝑉) | ||
Theorem | phlipf 20795 | The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·if‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑊 ∈ PreHil → , :(𝑉 × 𝑉)⟶𝐾) | ||
Theorem | ip2eq 20796* | 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 20797* | 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 20798* | 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 20799 | The inner product on a subspace equals the inner product on the parent space. (Contributed by AV, 19-Oct-2021.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑃 = (·𝑖‘𝑋) ⇒ ⊢ (𝑈 ∈ 𝑆 → 𝑃 = , ) | ||
Theorem | phssipval 20800 | 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 ∧ 𝑈 ∈ 𝑆) ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈)) → (𝐴𝑃𝐵) = (𝐴 , 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |