Home | Metamath
Proof Explorer Theorem List (p. 318 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xrge0omnd 31701 | The nonnegative extended real numbers form an ordered monoid. (Contributed by Thierry Arnoux, 22-Mar-2018.) |
β’ (β*π βΎs (0[,]+β)) β oMnd | ||
Theorem | omndmul2 31702 | In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ Β· = (.gβπ) & β’ 0 = (0gβπ) β β’ ((π β oMnd β§ (π β π΅ β§ π β β0) β§ 0 β€ π) β 0 β€ (π Β· π)) | ||
Theorem | omndmul3 31703 | In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ Β· = (.gβπ) & β’ 0 = (0gβπ) & β’ (π β π β oMnd) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π β€ π) & β’ (π β π β π΅) & β’ (π β 0 β€ π) β β’ (π β (π Β· π) β€ (π Β· π)) | ||
Theorem | omndmul 31704 | In a commutative ordered monoid, the ordering is compatible with group power. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ Β· = (.gβπ) & β’ (π β π β oMnd) & β’ (π β π β CMnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β β0) & β’ (π β π β€ π) β β’ (π β (π Β· π) β€ (π Β· π)) | ||
Theorem | ogrpinv0le 31705 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ β€ = (leβπΊ) & β’ πΌ = (invgβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β oGrp β§ π β π΅) β ( 0 β€ π β (πΌβπ) β€ 0 )) | ||
Theorem | ogrpsub 31706 | In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (BaseβπΊ) & β’ β€ = (leβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π β€ π) β (π β π) β€ (π β π)) | ||
Theorem | ogrpaddlt 31707 | In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β (π + π) < (π + π)) | ||
Theorem | ogrpaddltbi 31708 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π < π β (π + π) < (π + π))) | ||
Theorem | ogrpaddltrd 31709 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β π) & β’ (π β (oppgβπΊ) β oGrp) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π < π) β β’ (π β (π + π) < (π + π)) | ||
Theorem | ogrpaddltrbid 31710 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 4-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β π) & β’ (π β (oppgβπΊ) β oGrp) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π < π β (π + π) < (π + π))) | ||
Theorem | ogrpsublt 31711 | In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β (π β π) < (π β π)) | ||
Theorem | ogrpinv0lt 31712 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ πΌ = (invgβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β oGrp β§ π β π΅) β ( 0 < π β (πΌβπ) < 0 )) | ||
Theorem | ogrpinvlt 31713 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
β’ π΅ = (BaseβπΊ) & β’ < = (ltβπΊ) & β’ πΌ = (invgβπΊ) β β’ (((πΊ β oGrp β§ (oppgβπΊ) β oGrp) β§ π β π΅ β§ π β π΅) β (π < π β (πΌβπ) < (πΌβπ))) | ||
Theorem | gsumle 31714 | A finite sum in an ordered monoid is monotonic. This proof would be much easier in an ordered group, where an inverse element would be available. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
β’ π΅ = (Baseβπ) & β’ β€ = (leβπ) & β’ (π β π β oMnd) & β’ (π β π β CMnd) & β’ (π β π΄ β Fin) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΊ:π΄βΆπ΅) & β’ (π β πΉ βr β€ πΊ) β β’ (π β (π Ξ£g πΉ) β€ (π Ξ£g πΊ)) | ||
Theorem | symgfcoeu 31715* | Uniqueness property of permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ πΊ = (Baseβ(SymGrpβπ·)) β β’ ((π· β π β§ π β πΊ β§ π β πΊ) β β!π β πΊ π = (π β π)) | ||
Theorem | symgcom 31716 | Two permutations π and π commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (π βΎ πΈ) = ( I βΎ πΈ)) & β’ (π β (π βΎ πΉ) = ( I βΎ πΉ)) & β’ (π β (πΈ β© πΉ) = β ) & β’ (π β (πΈ βͺ πΉ) = π΄) β β’ (π β (π β π) = (π β π)) | ||
Theorem | symgcom2 31717 | Two permutations π and π commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 17-Nov-2023.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (dom (π β I ) β© dom (π β I )) = β ) β β’ (π β (π β π) = (π β π)) | ||
Theorem | symgcntz 31718* | All elements of a (finite) set of permutations commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π΅ = (Baseβπ) & β’ π = (Cntzβπ) & β’ (π β π΄ β π΅) & β’ (π β Disj π₯ β π΄ dom (π₯ β I )) β β’ (π β π΄ β (πβπ΄)) | ||
Theorem | odpmco 31719 | The composition of two odd permutations is even. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
β’ π = (SymGrpβπ·) & β’ π΅ = (Baseβπ) & β’ π΄ = (pmEvenβπ·) β β’ ((π· β Fin β§ π β (π΅ β π΄) β§ π β (π΅ β π΄)) β (π β π) β π΄) | ||
Theorem | symgsubg 31720 | The value of the group subtraction operation of the symmetric group. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) β β’ ((π β π΅ β§ π β π΅) β (π β π) = (π β β‘π)) | ||
Theorem | pmtrprfv2 31721 | In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π)) β ((πβ{π, π})βπ) = π) | ||
Theorem | pmtrcnel 31722 | Composing a permutation πΉ with a transposition which results in moving at least one less point. Here the set of points moved by a permutation πΉ is expressed as dom (πΉ β I ). (Contributed by Thierry Arnoux, 16-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π = (pmTrspβπ·) & β’ π΅ = (Baseβπ) & β’ π½ = (πΉβπΌ) & β’ (π β π· β π) & β’ (π β πΉ β π΅) & β’ (π β πΌ β dom (πΉ β I )) β β’ (π β dom (((πβ{πΌ, π½}) β πΉ) β I ) β (dom (πΉ β I ) β {πΌ})) | ||
Theorem | pmtrcnel2 31723 | Variation on pmtrcnel 31722. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π = (pmTrspβπ·) & β’ π΅ = (Baseβπ) & β’ π½ = (πΉβπΌ) & β’ (π β π· β π) & β’ (π β πΉ β π΅) & β’ (π β πΌ β dom (πΉ β I )) β β’ (π β (dom (πΉ β I ) β {πΌ, π½}) β dom (((πβ{πΌ, π½}) β πΉ) β I )) | ||
Theorem | pmtrcnelor 31724 | Composing a permutation πΉ with a transposition which results in moving one or two less points. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π = (pmTrspβπ·) & β’ π΅ = (Baseβπ) & β’ π½ = (πΉβπΌ) & β’ (π β π· β π) & β’ (π β πΉ β π΅) & β’ (π β πΌ β dom (πΉ β I )) & β’ πΈ = dom (πΉ β I ) & β’ π΄ = dom (((πβ{πΌ, π½}) β πΉ) β I ) β β’ (π β (π΄ = (πΈ β {πΌ, π½}) β¨ π΄ = (πΈ β {πΌ}))) | ||
Theorem | pmtridf1o 31725 | Transpositions of π and π (understood to be the identity when π = π), are bijections. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
β’ (π β π΄ β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ π = if(π = π, ( I βΎ π΄), ((pmTrspβπ΄)β{π, π})) β β’ (π β π:π΄β1-1-ontoβπ΄) | ||
Theorem | pmtridfv1 31726 | Value at X of the transposition of π and π (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022.) |
β’ (π β π΄ β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ π = if(π = π, ( I βΎ π΄), ((pmTrspβπ΄)β{π, π})) β β’ (π β (πβπ) = π) | ||
Theorem | pmtridfv2 31727 | Value at Y of the transposition of π and π (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022.) |
β’ (π β π΄ β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ π = if(π = π, ( I βΎ π΄), ((pmTrspβπ΄)β{π, π})) β β’ (π β (πβπ) = π) | ||
Theorem | psgnid 31728 | Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
β’ π = (pmSgnβπ·) β β’ (π· β Fin β (πβ( I βΎ π·)) = 1) | ||
Theorem | psgndmfi 31729 | For a finite base set, the permutation sign is defined for all permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π = (pmSgnβπ·) & β’ πΊ = (Baseβ(SymGrpβπ·)) β β’ (π· β Fin β π Fn πΊ) | ||
Theorem | pmtrto1cl 31730 | Useful lemma for the following theorems. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
β’ π· = (1...π) & β’ π = (pmTrspβπ·) β β’ ((πΎ β β β§ (πΎ + 1) β π·) β (πβ{πΎ, (πΎ + 1)}) β ran π) | ||
Theorem | psgnfzto1stlem 31731* | Lemma for psgnfzto1st 31736. Our permutation of rank (π + 1) can be written as a permutation of rank π composed with a transposition. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
β’ π· = (1...π) β β’ ((πΎ β β β§ (πΎ + 1) β π·) β (π β π· β¦ if(π = 1, (πΎ + 1), if(π β€ (πΎ + 1), (π β 1), π))) = (((pmTrspβπ·)β{πΎ, (πΎ + 1)}) β (π β π· β¦ if(π = 1, πΎ, if(π β€ πΎ, (π β 1), π))))) | ||
Theorem | fzto1stfv1 31732* | Value of our permutation π at 1. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
β’ π· = (1...π) & β’ π = (π β π· β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) β β’ (πΌ β π· β (πβ1) = πΌ) | ||
Theorem | fzto1st1 31733* | Special case where the permutation defined in psgnfzto1st 31736 is the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
β’ π· = (1...π) & β’ π = (π β π· β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) β β’ (πΌ = 1 β π = ( I βΎ π·)) | ||
Theorem | fzto1st 31734* | The function moving one element to the first position (and shifting all elements before it) is a permutation. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
β’ π· = (1...π) & β’ π = (π β π· β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ πΊ = (SymGrpβπ·) & β’ π΅ = (BaseβπΊ) β β’ (πΌ β π· β π β π΅) | ||
Theorem | fzto1stinvn 31735* | Value of the inverse of our permutation π at πΌ. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
β’ π· = (1...π) & β’ π = (π β π· β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ πΊ = (SymGrpβπ·) & β’ π΅ = (BaseβπΊ) β β’ (πΌ β π· β (β‘πβπΌ) = 1) | ||
Theorem | psgnfzto1st 31736* | The permutation sign for moving one element to the first position. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
β’ π· = (1...π) & β’ π = (π β π· β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ πΊ = (SymGrpβπ·) & β’ π΅ = (BaseβπΊ) & β’ π = (pmSgnβπ·) β β’ (πΌ β π· β (πβπ) = (-1β(πΌ + 1))) | ||
Syntax | ctocyc 31737 | Extend class notation with the permutation cycle builder. |
class toCyc | ||
Definition | df-tocyc 31738* | Define a convenience permutation cycle builder. Given a list of elements to be cycled, in the form of a word, this function produces the corresponding permutation cycle. See definition in [Lang] p. 30. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ toCyc = (π β V β¦ (π€ β {π’ β Word π β£ π’:dom π’β1-1βπ} β¦ (( I βΎ (π β ran π€)) βͺ ((π€ cyclShift 1) β β‘π€)))) | ||
Theorem | tocycval 31739* | Value of the cycle builder. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
β’ πΆ = (toCycβπ·) β β’ (π· β π β πΆ = (π€ β {π’ β Word π· β£ π’:dom π’β1-1βπ·} β¦ (( I βΎ (π· β ran π€)) βͺ ((π€ cyclShift 1) β β‘π€)))) | ||
Theorem | tocycfv 31740 | Function value of a permutation cycle built from a word. (Contributed by Thierry Arnoux, 18-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) β β’ (π β (πΆβπ) = (( I βΎ (π· β ran π)) βͺ ((π cyclShift 1) β β‘π))) | ||
Theorem | tocycfvres1 31741 | A cyclic permutation is a cyclic shift on its orbit. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) β β’ (π β ((πΆβπ) βΎ ran π) = ((π cyclShift 1) β β‘π)) | ||
Theorem | tocycfvres2 31742 | A cyclic permutation is the identity outside of its orbit. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) β β’ (π β ((πΆβπ) βΎ (π· β ran π)) = ( I βΎ (π· β ran π))) | ||
Theorem | cycpmfvlem 31743 | Lemma for cycpmfv1 31744 and cycpmfv2 31745. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ (π β π β (0..^(β―βπ))) β β’ (π β ((πΆβπ)β(πβπ)) = (((π cyclShift 1) β β‘π)β(πβπ))) | ||
Theorem | cycpmfv1 31744 | Value of a cycle function for any element but the last. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ (π β π β (0..^((β―βπ) β 1))) β β’ (π β ((πΆβπ)β(πβπ)) = (πβ(π + 1))) | ||
Theorem | cycpmfv2 31745 | Value of a cycle function for the last element of the orbit. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ (π β 0 < (β―βπ)) & β’ (π β π = ((β―βπ) β 1)) β β’ (π β ((πΆβπ)β(πβπ)) = (πβ0)) | ||
Theorem | cycpmfv3 31746 | Values outside of the orbit are unchanged by a cycle. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ (π β π β π·) & β’ (π β Β¬ π β ran π) β β’ (π β ((πΆβπ)βπ) = π) | ||
Theorem | cycpmcl 31747 | Cyclic permutations are permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ π = (SymGrpβπ·) β β’ (π β (πΆβπ) β (Baseβπ)) | ||
Theorem | tocycf 31748* | The permutation cycle builder as a function. (Contributed by Thierry Arnoux, 25-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ π΅ = (Baseβπ) β β’ (π· β π β πΆ:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆπ΅) | ||
Theorem | tocyc01 31749 | Permutation cycles built from the empty set or a singleton are the identity. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
β’ πΆ = (toCycβπ·) β β’ ((π· β π β§ π β (dom πΆ β© (β‘β― β {0, 1}))) β (πΆβπ) = ( I βΎ π·)) | ||
Theorem | cycpm2tr 31750 | A cyclic permutation of 2 elements is a transposition. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΌ β π½) & β’ π = (pmTrspβπ·) β β’ (π β (πΆββ¨βπΌπ½ββ©) = (πβ{πΌ, π½})) | ||
Theorem | cycpm2cl 31751 | Closure for the 2-cycles. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΌ β π½) & β’ π = (SymGrpβπ·) β β’ (π β (πΆββ¨βπΌπ½ββ©) β (Baseβπ)) | ||
Theorem | cyc2fv1 31752 | Function value of a 2-cycle at the first point. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΌ β π½) & β’ π = (SymGrpβπ·) β β’ (π β ((πΆββ¨βπΌπ½ββ©)βπΌ) = π½) | ||
Theorem | cyc2fv2 31753 | Function value of a 2-cycle at the second point. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΌ β π½) & β’ π = (SymGrpβπ·) β β’ (π β ((πΆββ¨βπΌπ½ββ©)βπ½) = πΌ) | ||
Theorem | trsp2cyc 31754* | Exhibit the word a transposition corresponds to, as a cycle. (Contributed by Thierry Arnoux, 25-Sep-2023.) |
β’ π = ran (pmTrspβπ·) & β’ πΆ = (toCycβπ·) β β’ ((π· β π β§ π β π) β βπ β π· βπ β π· (π β π β§ π = (πΆββ¨βππββ©))) | ||
Theorem | cycpmco2f1 31755 | The word U used in cycpmco2 31764 is injective, so it can represent a cycle and form a cyclic permutation (πβπ). (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β β’ (π β π:dom πβ1-1βπ·) | ||
Theorem | cycpmco2rn 31756 | The orbit of the composition of a cyclic permutation and a well-chosen transposition is one element more than the orbit of the original permutation. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β β’ (π β ran π = (ran π βͺ {πΌ})) | ||
Theorem | cycpmco2lem1 31757 | Lemma for cycpmco2 31764. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β β’ (π β ((πβπ)β((πββ¨βπΌπ½ββ©)βπΌ)) = ((πβπ)βπ½)) | ||
Theorem | cycpmco2lem2 31758 | Lemma for cycpmco2 31764. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β β’ (π β (πβπΈ) = πΌ) | ||
Theorem | cycpmco2lem3 31759 | Lemma for cycpmco2 31764. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β β’ (π β ((β―βπ) β 1) = (β―βπ)) | ||
Theorem | cycpmco2lem4 31760 | Lemma for cycpmco2 31764. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β β’ (π β ((πβπ)β((πββ¨βπΌπ½ββ©)βπΌ)) = ((πβπ)βπΌ)) | ||
Theorem | cycpmco2lem5 31761 | Lemma for cycpmco2 31764. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) & β’ (π β πΎ β ran π) & β’ (π β (β‘πβπΎ) = ((β―βπ) β 1)) β β’ (π β ((πβπ)βπΎ) = ((πβπ)βπΎ)) | ||
Theorem | cycpmco2lem6 31762 | Lemma for cycpmco2 31764. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) & β’ (π β πΎ β ran π) & β’ (π β πΎ β πΌ) & β’ (π β (β‘πβπΎ) β (πΈ..^((β―βπ) β 1))) β β’ (π β ((πβπ)βπΎ) = ((πβπ)βπΎ)) | ||
Theorem | cycpmco2lem7 31763 | Lemma for cycpmco2 31764. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) & β’ (π β πΎ β ran π) & β’ (π β πΎ β π½) & β’ (π β (β‘πβπΎ) β (0..^πΈ)) β β’ (π β ((πβπ)βπΎ) = ((πβπ)βπΎ)) | ||
Theorem | cycpmco2 31764 | The composition of a cyclic permutation and a transposition of one element in the cycle and one outside the cycle results in a cyclic permutation with one more element in its orbit. (Contributed by Thierry Arnoux, 2-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β β’ (π β ((πβπ) β (πββ¨βπΌπ½ββ©)) = (πβπ)) | ||
Theorem | cyc2fvx 31765 | Function value of a 2-cycle outside of its orbit. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β ((πΆββ¨βπΌπ½ββ©)βπΎ) = πΎ) | ||
Theorem | cycpm3cl 31766 | Closure of the 3-cycles in the permutations. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β (πΆββ¨βπΌπ½πΎββ©) β (Baseβπ)) | ||
Theorem | cycpm3cl2 31767 | Closure of the 3-cycles in the class of 3-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β (πΆββ¨βπΌπ½πΎββ©) β (πΆ β (β‘β― β {3}))) | ||
Theorem | cyc3fv1 31768 | Function value of a 3-cycle at the first point. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β ((πΆββ¨βπΌπ½πΎββ©)βπΌ) = π½) | ||
Theorem | cyc3fv2 31769 | Function value of a 3-cycle at the second point. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β ((πΆββ¨βπΌπ½πΎββ©)βπ½) = πΎ) | ||
Theorem | cyc3fv3 31770 | Function value of a 3-cycle at the third point. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β ((πΆββ¨βπΌπ½πΎββ©)βπΎ) = πΌ) | ||
Theorem | cyc3co2 31771 | Represent a 3-cycle as a composition of two 2-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) & β’ Β· = (+gβπ) β β’ (π β (πΆββ¨βπΌπ½πΎββ©) = ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))) | ||
Theorem | cycpmconjvlem 31772 | Lemma for cycpmconjv 31773. (Contributed by Thierry Arnoux, 9-Oct-2023.) |
β’ (π β πΉ:π·β1-1-ontoβπ·) & β’ (π β π΅ β π·) β β’ (π β ((πΉ βΎ (π· β π΅)) β β‘πΉ) = ( I βΎ (π· β ran (πΉ βΎ π΅)))) | ||
Theorem | cycpmconjv 31773 | A formula for computing conjugacy classes of cyclic permutations. Formula in property (b) of [Lang] p. 32. (Contributed by Thierry Arnoux, 9-Oct-2023.) |
β’ π = (SymGrpβπ·) & β’ π = (toCycβπ·) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ π΅ = (Baseβπ) β β’ ((π· β π β§ πΊ β π΅ β§ π β dom π) β ((πΊ + (πβπ)) β πΊ) = (πβ(πΊ β π))) | ||
Theorem | cycpmrn 31774 | The range of the word used to build a cycle is the cycle's orbit, i.e., the set of points it moves. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
β’ π = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ (π β 1 < (β―βπ)) β β’ (π β ran π = dom ((πβπ) β I )) | ||
Theorem | tocyccntz 31775* | All elements of a (finite) set of cycles commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π = (Cntzβπ) & β’ π = (toCycβπ·) & β’ (π β π· β π) & β’ (π β Disj π₯ β π΄ ran π₯) & β’ (π β π΄ β dom π) β β’ (π β (π β π΄) β (πβ(π β π΄))) | ||
Theorem | evpmval 31776 | Value of the set of even permutations, the alternating group. (Contributed by Thierry Arnoux, 1-Nov-2023.) |
β’ π΄ = (pmEvenβπ·) β β’ (π· β π β π΄ = (β‘(pmSgnβπ·) β {1})) | ||
Theorem | cnmsgn0g 31777 | The neutral element of the sign subgroup of the complex numbers. (Contributed by Thierry Arnoux, 1-Nov-2023.) |
β’ π = ((mulGrpββfld) βΎs {1, -1}) β β’ 1 = (0gβπ) | ||
Theorem | evpmsubg 31778 | The alternating group is a subgroup of the symmetric group. (Contributed by Thierry Arnoux, 1-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π΄ = (pmEvenβπ·) β β’ (π· β Fin β π΄ β (SubGrpβπ)) | ||
Theorem | evpmid 31779 | The identity is an even permutation. (Contributed by Thierry Arnoux, 18-Sep-2023.) |
β’ π = (SymGrpβπ·) β β’ (π· β Fin β ( I βΎ π·) β (pmEvenβπ·)) | ||
Theorem | altgnsg 31780 | The alternating group (pmEvenβπ·) is a normal subgroup of the symmetric group. (Contributed by Thierry Arnoux, 18-Sep-2023.) |
β’ π = (SymGrpβπ·) β β’ (π· β Fin β (pmEvenβπ·) β (NrmSGrpβπ)) | ||
Theorem | cyc3evpm 31781 | 3-Cycles are even permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = ((toCycβπ·) β (β‘β― β {3})) & β’ π΄ = (pmEvenβπ·) β β’ (π· β Fin β πΆ β π΄) | ||
Theorem | cyc3genpmlem 31782* | Lemma for cyc3genpm 31783. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (π β (β‘β― β {3})) & β’ π΄ = (pmEvenβπ·) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ Β· = (+gβπ) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΏ β π·) & β’ (π β πΈ = (πββ¨βπΌπ½ββ©)) & β’ (π β πΉ = (πββ¨βπΎπΏββ©)) & β’ (π β π· β π) & β’ (π β πΌ β π½) & β’ (π β πΎ β πΏ) β β’ (π β βπ β Word πΆ(πΈ Β· πΉ) = (π Ξ£g π)) | ||
Theorem | cyc3genpm 31783* | The alternating group π΄ is generated by 3-cycles. Property (a) of [Lang] p. 32 . (Contributed by Thierry Arnoux, 27-Sep-2023.) |
β’ πΆ = (π β (β‘β― β {3})) & β’ π΄ = (pmEvenβπ·) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) β β’ (π· β Fin β (π β π΄ β βπ€ β Word πΆπ = (π Ξ£g π€))) | ||
Theorem | cycpmgcl 31784 | Cyclic permutations are permutations, similar to cycpmcl 31747, but where the set of cyclic permutations of length π is expressed in terms of a preimage. (Contributed by Thierry Arnoux, 13-Oct-2023.) |
β’ πΆ = (π β (β‘β― β {π})) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ π΅ = (Baseβπ) β β’ ((π· β π β§ π β (0...π)) β πΆ β π΅) | ||
Theorem | cycpmconjslem1 31785 | Lemma for cycpmconjs 31787. (Contributed by Thierry Arnoux, 14-Oct-2023.) |
β’ πΆ = (π β (β‘β― β {π})) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ (π β (β―βπ) = π) β β’ (π β ((β‘π β (πβπ)) β π) = (( I βΎ (0..^π)) cyclShift 1)) | ||
Theorem | cycpmconjslem2 31786* | Lemma for cycpmconjs 31787. (Contributed by Thierry Arnoux, 14-Oct-2023.) |
β’ πΆ = (π β (β‘β― β {π})) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ (π β π β (0...π)) & β’ (π β π· β Fin) & β’ (π β π β πΆ) β β’ (π β βπ(π:(0..^π)β1-1-ontoβπ· β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) | ||
Theorem | cycpmconjs 31787* | All cycles of the same length are conjugate in the symmetric group. (Contributed by Thierry Arnoux, 14-Oct-2023.) |
β’ πΆ = (π β (β‘β― β {π})) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ (π β π β (0...π)) & β’ (π β π· β Fin) & β’ (π β π β πΆ) & β’ (π β π β πΆ) β β’ (π β βπ β π΅ π = ((π + π) β π)) | ||
Theorem | cyc3conja 31788* | All 3-cycles are conjugate in the alternating group An for n>= 5. Property (b) of [Lang] p. 32. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
β’ πΆ = (π β (β‘β― β {3})) & β’ π΄ = (pmEvenβπ·) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ (π β 5 β€ π) & β’ (π β π· β Fin) & β’ (π β π β πΆ) & β’ (π β π β πΆ) β β’ (π β βπ β π΄ π = ((π + π) β π)) | ||
Syntax | csgns 31789 | Extend class notation to include the Signum function. |
class sgns | ||
Definition | df-sgns 31790* | Signum function for a structure. See also df-sgn 14906 for the version for extended reals. (Contributed by Thierry Arnoux, 10-Sep-2018.) |
β’ sgns = (π β V β¦ (π₯ β (Baseβπ) β¦ if(π₯ = (0gβπ), 0, if((0gβπ)(ltβπ)π₯, 1, -1)))) | ||
Theorem | sgnsv 31791* | The sign mapping. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ < = (ltβπ ) & β’ π = (sgnsβπ ) β β’ (π β π β π = (π₯ β π΅ β¦ if(π₯ = 0 , 0, if( 0 < π₯, 1, -1)))) | ||
Theorem | sgnsval 31792 | The sign value. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ < = (ltβπ ) & β’ π = (sgnsβπ ) β β’ ((π β π β§ π β π΅) β (πβπ) = if(π = 0 , 0, if( 0 < π, 1, -1))) | ||
Theorem | sgnsf 31793 | The sign function. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ < = (ltβπ ) & β’ π = (sgnsβπ ) β β’ (π β π β π:π΅βΆ{-1, 0, 1}) | ||
Syntax | cinftm 31794 | Class notation for the infinitesimal relation. |
class β | ||
Syntax | carchi 31795 | Class notation for the Archimedean property. |
class Archi | ||
Definition | df-inftm 31796* | Define the relation "π₯ is infinitesimal with respect to π¦ " for a structure π€. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ β = (π€ β V β¦ {β¨π₯, π¦β© β£ ((π₯ β (Baseβπ€) β§ π¦ β (Baseβπ€)) β§ ((0gβπ€)(ltβπ€)π₯ β§ βπ β β (π(.gβπ€)π₯)(ltβπ€)π¦))}) | ||
Definition | df-archi 31797 | A structure said to be Archimedean if it has no infinitesimal elements. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ Archi = {π€ β£ (ββπ€) = β } | ||
Theorem | inftmrel 31798 | The infinitesimal relation for a structure π. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) β β’ (π β π β (ββπ) β (π΅ Γ π΅)) | ||
Theorem | isinftm 31799* | Express π₯ is infinitesimal with respect to π¦ for a structure π. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ Β· = (.gβπ) & β’ < = (ltβπ) β β’ ((π β π β§ π β π΅ β§ π β π΅) β (π(ββπ)π β ( 0 < π β§ βπ β β (π Β· π) < π))) | ||
Theorem | isarchi 31800* | Express the predicate "π is Archimedean ". (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ < = (ββπ) β β’ (π β π β (π β Archi β βπ₯ β π΅ βπ¦ β π΅ Β¬ π₯ < π¦)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |