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