![]() |
Metamath
Proof Explorer Theorem List (p. 212 of 479) | < 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-30159) |
![]() (30160-31682) |
![]() (31683-47806) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | znle2 21101 | 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‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) | ||
Theorem | znleval 21102 | 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 | znleval2 21103 | 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 21104 | Lemma for zntos 21105. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = (le‘𝑌) & ⊢ 𝑋 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ Toset) | ||
Theorem | zntos 21105 | 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 21106 | The ℤ/nℤ structure has 𝑛 elements. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → (♯‘𝐵) = 𝑁) | ||
Theorem | znfi 21107 | The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin) | ||
Theorem | znfld 21108 | The ℤ/nℤ structure is a finite field when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℙ → 𝑌 ∈ Field) | ||
Theorem | znidomb 21109 | 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 21110 | Cyclic rings are defined by their characteristic. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (chr‘𝑌) = 𝑁) | ||
Theorem | znunit 21111 | 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 21112 | The size of the unit group of ℤ/nℤ. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝑈 = (Unit‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → (♯‘𝑈) = (ϕ‘𝑁)) | ||
Theorem | znrrg 21113 | 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 21114* | Lemma for cygzn 21118. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ · = (.g‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) ⇒ ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝐿‘𝐾) = (𝐿‘𝑀) ↔ (𝐾 · 𝑋) = (𝑀 · 𝑋))) | ||
Theorem | cygznlem2a 21115* | Lemma for cygzn 21118. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ · = (.g‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ 〈(𝐿‘𝑚), (𝑚 · 𝑋)〉) ⇒ ⊢ (𝜑 → 𝐹:(Base‘𝑌)⟶𝐵) | ||
Theorem | cygznlem2 21116* | Lemma for cygzn 21118. (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 21117* | 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 21118 | 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 21119* | 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 21120 | Cyclic groups are isomorphic precisely when they have the same order. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = (Base‘𝐻) ⇒ ⊢ ((𝐺 ∈ CycGrp ∧ 𝐻 ∈ CycGrp) → (𝐺 ≃𝑔 𝐻 ↔ 𝐵 ≈ 𝐶)) | ||
Theorem | frgpcyg 21121 | 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 21122 | 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 21123 | 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 21124 | The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1}) ⇒ ⊢ 𝑈 ∈ Grp | ||
Theorem | psgnghm 21125 | 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 21126 | 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 21127 | 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 21128 | Multiplicativity of the permutation sign function. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → (𝑁‘(𝐹 ∘ 𝐺)) = ((𝑁‘𝐹) · (𝑁‘𝐺))) | ||
Theorem | zrhpsgnmhm 21129 | 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 21130 | 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 21131 | Even permutations are permutations. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) ⇒ ⊢ (pmEven‘𝐷) ⊆ 𝑃 | ||
Theorem | psgnevpmb 21132 | 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 21133 | 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 21134 | A permutation which is even has sign 1. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) & ⊢ 𝑁 = (pmSgn‘𝐷) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ (pmEven‘𝐷)) → (𝑁‘𝐹) = 1) | ||
Theorem | psgnodpmr 21135 | 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 21136 | 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 21137 | 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 21138 | 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 21139 | 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 21140 | 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 21141* | 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 21142 | A transposition is an odd permutation. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) & ⊢ 𝑇 = ran (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝑃 ∖ (pmEven‘𝐷))) | ||
Theorem | psgnfix1 21143* | 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 21144* | 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 21145* | Lemma 1 for psgndif 21147. (Contributed by AV, 27-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑍 = (SymGrp‘𝑁) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊)) → ((𝑈 ∈ Word 𝑅 ∧ (♯‘𝑊) = (♯‘𝑈) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → 𝑄 = (𝑍 Σg 𝑈)))) | ||
Theorem | psgndiflemA 21146* | Lemma 2 for psgndif 21147. (Contributed by AV, 31-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑍 = (SymGrp‘𝑁) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊) ∧ 𝑈 ∈ Word 𝑅) → (𝑄 = ((SymGrp‘𝑁) Σg 𝑈) → (-1↑(♯‘𝑊)) = (-1↑(♯‘𝑈))))) | ||
Theorem | psgndif 21147* | 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 21148* | 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 21149 | Extend class notation with the field of real numbers. |
class ℝfld | ||
Definition | df-refld 21150 | The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ ℝfld = (ℂfld ↾s ℝ) | ||
Theorem | rebase 21151 | The base of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ℝ = (Base‘ℝfld) | ||
Theorem | remulg 21152 | The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝑁(.g‘ℝfld)𝐴) = (𝑁 · 𝐴)) | ||
Theorem | resubdrg 21153 | 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 21154 | Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ − = (-g‘ℝfld) ⇒ ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋 − 𝑌) = (𝑋 − 𝑌)) | ||
Theorem | replusg 21155 | The addition operation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ + = (+g‘ℝfld) | ||
Theorem | remulr 21156 | The multiplication operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ · = (.r‘ℝfld) | ||
Theorem | re0g 21157 | The zero element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ 0 = (0g‘ℝfld) | ||
Theorem | re1r 21158 | The unity element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ 1 = (1r‘ℝfld) | ||
Theorem | rele2 21159 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ ≤ = (le‘ℝfld) | ||
Theorem | relt 21160 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ < = (lt‘ℝfld) | ||
Theorem | reds 21161 | The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019.) |
⊢ (abs ∘ − ) = (dist‘ℝfld) | ||
Theorem | redvr 21162 | The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴(/r‘ℝfld)𝐵) = (𝐴 / 𝐵)) | ||
Theorem | retos 21163 | The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
⊢ ℝfld ∈ Toset | ||
Theorem | refld 21164 | The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ℝfld ∈ Field | ||
Theorem | refldcj 21165 | The conjugation operation of the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ ∗ = (*𝑟‘ℝfld) | ||
Theorem | resrng 21166 | 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 21167* | 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 21168 | The quotient group ℝ / ℤ is a group. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
⊢ 𝑅 = (ℝfld /s (ℝfld ~QG ℤ)) ⇒ ⊢ 𝑅 ∈ Grp | ||
Syntax | cphl 21169 | Extend class notation with class of all pre-Hilbert spaces. |
class PreHil | ||
Syntax | cipf 21170 | Extend class notation with inner product function. |
class ·if | ||
Definition | df-phl 21171* | 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 21172* | 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 21196), while ·𝑖 only has closure (ipcl 21178). (Contributed by Mario Carneiro, 12-Aug-2015.) |
⊢ ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦))) | ||
Theorem | isphl 21173* | 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 21174 | A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec) | ||
Theorem | phllmod 21175 | A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) | ||
Theorem | phlsrng 21176 | The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil → 𝐹 ∈ *-Ring) | ||
Theorem | phllmhm 21177* | 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 21178 | Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ 𝐾) | ||
Theorem | ipcj 21179 | 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 21180 | 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 21181 | 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 21182 | 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 21183 | 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 21184 | 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 21185 | 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 21186 | 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 21187 | 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 21188 | 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 21189 | Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝑆 = (-g‘𝐹) & ⊢ + = (+g‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶)))) | ||
Theorem | ipass 21190 | 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 21191 | "Associative" law for second argument of inner product (compare ipass 21190). (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝐹) & ⊢ ∗ = (*𝑟‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → (𝐴 , (𝐶 · 𝐵)) = ((𝐴 , 𝐵) × ( ∗ ‘𝐶))) | ||
Theorem | ipassr2 21192 | "Associative" law for inner product. Conjugate version of ipassr 21191. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ × = (.r‘𝐹) & ⊢ ∗ = (*𝑟‘𝐹) ⇒ ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → ((𝐴 , 𝐵) × 𝐶) = (𝐴 , (( ∗ ‘𝐶) · 𝐵))) | ||
Theorem | ipffval 21193* | 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 21194 | The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ · = (·if‘𝑊) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 · 𝑌) = (𝑋 , 𝑌)) | ||
Theorem | ipfeq 21195 | 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 21196 | The inner product operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·if‘𝑊) ⇒ ⊢ , Fn (𝑉 × 𝑉) | ||
Theorem | phlipf 21197 | The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·if‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) ⇒ ⊢ (𝑊 ∈ PreHil → , :(𝑉 × 𝑉)⟶𝐾) | ||
Theorem | ip2eq 21198* | 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 21199* | 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 21200* | 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)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |