![]() |
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-30158) |
![]() (30159-31681) |
![]() (31682-47805) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | znleval 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βπ) & β’ π = (Baseβπ) β β’ (π β β0 β (π΄ β€ π΅ β (π΄ β π β§ π΅ β π β§ (β‘πΉβπ΄) β€ (β‘πΉβπ΅)))) | ||
Theorem | znleval2 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 | zntoslem 21103 | Lemma for zntos 21104. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
β’ π = (β€/nβ€βπ) & β’ πΉ = ((β€RHomβπ) βΎ π) & β’ π = if(π = 0, β€, (0..^π)) & β’ β€ = (leβπ) & β’ π = (Baseβπ) β β’ (π β β0 β π β Toset) | ||
Theorem | zntos 21104 | 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 21105 | The β€/nβ€ structure has π elements. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) β β’ (π β β β (β―βπ΅) = π) | ||
Theorem | znfi 21106 | The β€/nβ€ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.) |
β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) β β’ (π β β β π΅ β Fin) | ||
Theorem | znfld 21107 | The β€/nβ€ structure is a finite field when π is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (β€/nβ€βπ) β β’ (π β β β π β Field) | ||
Theorem | znidomb 21108 | 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 21109 | Cyclic rings are defined by their characteristic. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ π = (β€/nβ€βπ) β β’ (π β β0 β (chrβπ) = π) | ||
Theorem | znunit 21110 | 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 21111 | The size of the unit group of β€/nβ€. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π = (β€/nβ€βπ) & β’ π = (Unitβπ) β β’ (π β β β (β―βπ) = (Οβπ)) | ||
Theorem | znrrg 21112 | 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 21113* | Lemma for cygzn 21117. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = if(π΅ β Fin, (β―βπ΅), 0) & β’ π = (β€/nβ€βπ) & β’ Β· = (.gβπΊ) & β’ πΏ = (β€RHomβπ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} & β’ (π β πΊ β CycGrp) & β’ (π β π β πΈ) β β’ ((π β§ (πΎ β β€ β§ π β β€)) β ((πΏβπΎ) = (πΏβπ) β (πΎ Β· π) = (π Β· π))) | ||
Theorem | cygznlem2a 21114* | Lemma for cygzn 21117. (Contributed by Mario Carneiro, 23-Dec-2016.) |
β’ π΅ = (BaseβπΊ) & β’ π = if(π΅ β Fin, (β―βπ΅), 0) & β’ π = (β€/nβ€βπ) & β’ Β· = (.gβπΊ) & β’ πΏ = (β€RHomβπ) & β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} & β’ (π β πΊ β CycGrp) & β’ (π β π β πΈ) & β’ πΉ = ran (π β β€ β¦ β¨(πΏβπ), (π Β· π)β©) β β’ (π β πΉ:(Baseβπ)βΆπ΅) | ||
Theorem | cygznlem2 21115* | Lemma for cygzn 21117. (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 21116* | 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 21117 | 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 21118* | 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 21119 | Cyclic groups are isomorphic precisely when they have the same order. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ πΆ = (Baseβπ») β β’ ((πΊ β CycGrp β§ π» β CycGrp) β (πΊ βπ π» β π΅ β πΆ)) | ||
Theorem | frgpcyg 21120 | 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 21121 | 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 21122 | 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 21123 | The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
β’ π = ((mulGrpββfld) βΎs {1, -1}) β β’ π β Grp | ||
Theorem | psgnghm 21124 | 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 21125 | 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 21126 | 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 21127 | Multiplicativity of the permutation sign function. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (pmSgnβπ·) & β’ π = (Baseβπ) β β’ ((π· β Fin β§ πΉ β π β§ πΊ β π) β (πβ(πΉ β πΊ)) = ((πβπΉ) Β· (πβπΊ))) | ||
Theorem | zrhpsgnmhm 21128 | 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 21129 | 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 21130 | Even permutations are permutations. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) β β’ (pmEvenβπ·) β π | ||
Theorem | psgnevpmb 21131 | 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 21132 | 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 21133 | A permutation which is even has sign 1. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) & β’ π = (pmSgnβπ·) β β’ ((π· β Fin β§ πΉ β (pmEvenβπ·)) β (πβπΉ) = 1) | ||
Theorem | psgnodpmr 21134 | 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 21135 | 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 21136 | 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 21137 | 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 21138 | 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 21139 | 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 21140* | 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 21141 | A transposition is an odd permutation. (Contributed by SO, 9-Jul-2018.) |
β’ π = (SymGrpβπ·) & β’ π = (Baseβπ) & β’ π = ran (pmTrspβπ·) β β’ ((π· β Fin β§ πΉ β π) β πΉ β (π β (pmEvenβπ·))) | ||
Theorem | psgnfix1 21142* | 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 21143* | 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 21144* | Lemma 1 for psgndif 21146. (Contributed by AV, 27-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = (SymGrpβ(π β {πΎ})) & β’ π = (SymGrpβπ) & β’ π = ran (pmTrspβπ) β β’ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π)) β ((π β Word π β§ (β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))) β π = (π Ξ£g π)))) | ||
Theorem | psgndiflemA 21145* | Lemma 2 for psgndif 21146. (Contributed by AV, 31-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = (SymGrpβ(π β {πΎ})) & β’ π = (SymGrpβπ) & β’ π = ran (pmTrspβπ) β β’ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π ) β (π = ((SymGrpβπ) Ξ£g π) β (-1β(β―βπ)) = (-1β(β―βπ))))) | ||
Theorem | psgndif 21146* | 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 21147* | 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 21148 | Extend class notation with the field of real numbers. |
class βfld | ||
Definition | df-refld 21149 | The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ βfld = (βfld βΎs β) | ||
Theorem | rebase 21150 | The base of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ β = (Baseββfld) | ||
Theorem | remulg 21151 | The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ ((π β β€ β§ π΄ β β) β (π(.gββfld)π΄) = (π Β· π΄)) | ||
Theorem | resubdrg 21152 | 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 21153 | Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ β = (-gββfld) β β’ ((π β β β§ π β β) β (π β π) = (π β π)) | ||
Theorem | replusg 21154 | The addition operation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ + = (+gββfld) | ||
Theorem | remulr 21155 | The multiplication operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ Β· = (.rββfld) | ||
Theorem | re0g 21156 | The zero element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ 0 = (0gββfld) | ||
Theorem | re1r 21157 | The unity element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ 1 = (1rββfld) | ||
Theorem | rele2 21158 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ β€ = (leββfld) | ||
Theorem | relt 21159 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ < = (ltββfld) | ||
Theorem | reds 21160 | The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019.) |
β’ (abs β β ) = (distββfld) | ||
Theorem | redvr 21161 | The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π΄(/rββfld)π΅) = (π΄ / π΅)) | ||
Theorem | retos 21162 | The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ βfld β Toset | ||
Theorem | refld 21163 | The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ βfld β Field | ||
Theorem | refldcj 21164 | The conjugation operation of the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ β = (*πββfld) | ||
Theorem | resrng 21165 | 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 21166* | 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 21167 | The quotient group β / β€ is a group. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
β’ π = (βfld /s (βfld ~QG β€)) β β’ π β Grp | ||
Syntax | cphl 21168 | Extend class notation with class of all pre-Hilbert spaces. |
class PreHil | ||
Syntax | cipf 21169 | Extend class notation with inner product function. |
class Β·if | ||
Definition | df-phl 21170* | 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 21171* | 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 21195), while Β·π only has closure (ipcl 21177). (Contributed by Mario Carneiro, 12-Aug-2015.) |
β’ Β·if = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯(Β·πβπ)π¦))) | ||
Theorem | isphl 21172* | 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 21173 | A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β PreHil β π β LVec) | ||
Theorem | phllmod 21174 | A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ (π β PreHil β π β LMod) | ||
Theorem | phlsrng 21175 | The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β PreHil β πΉ β *-Ring) | ||
Theorem | phllmhm 21176* | 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 21177 | Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β PreHil β§ π΄ β π β§ π΅ β π) β (π΄ , π΅) β πΎ) | ||
Theorem | ipcj 21178 | 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 21179 | 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 21180 | 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 21181 | 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 21182 | 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 21183 | 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 21184 | 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 21185 | 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 21186 | 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 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 | ip2subdi 21188 | Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (-gβπΉ) & β’ + = (+gβπΉ) & β’ (π β π β PreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β ((π΄ β π΅) , (πΆ β π·)) = (((π΄ , πΆ) + (π΅ , π·))π((π΄ , π·) + (π΅ , πΆ)))) | ||
Theorem | ipass 21189 | 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 21190 | "Associative" law for second argument of inner product (compare ipass 21189). (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπΉ) & β’ β = (*πβπΉ) β β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β (π΄ , (πΆ Β· π΅)) = ((π΄ , π΅) Γ ( β βπΆ))) | ||
Theorem | ipassr2 21191 | "Associative" law for inner product. Conjugate version of ipassr 21190. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ , = (Β·πβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπΉ) & β’ β = (*πβπΉ) β β’ ((π β PreHil β§ (π΄ β π β§ π΅ β π β§ πΆ β πΎ)) β ((π΄ , π΅) Γ πΆ) = (π΄ , (( β βπΆ) Β· π΅))) | ||
Theorem | ipffval 21192* | 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 21193 | The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ Β· = (Β·ifβπ) β β’ ((π β π β§ π β π) β (π Β· π) = (π , π)) | ||
Theorem | ipfeq 21194 | 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 21195 | The inner product operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·ifβπ) β β’ , Fn (π Γ π) | ||
Theorem | phlipf 21196 | The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·ifβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) β β’ (π β PreHil β , :(π Γ π)βΆπΎ) | ||
Theorem | ip2eq 21197* | 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 21198* | 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 21199* | 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 21200 | The inner product on a subspace equals the inner product on the parent space. (Contributed by AV, 19-Oct-2021.) |
β’ π = (π βΎs π) & β’ , = (Β·πβπ) & β’ π = (Β·πβπ) β β’ (π β π β π = , ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |