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