![]() |
Metamath
Proof Explorer Theorem List (p. 329 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fzto1st1 32801* | Special case where the permutation defined in psgnfzto1st 32804 is the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
β’ π· = (1...π) & β’ π = (π β π· β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) β β’ (πΌ = 1 β π = ( I βΎ π·)) | ||
Theorem | fzto1st 32802* | 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 32803* | 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 32804* | 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 32805 | Extend class notation with the permutation cycle builder. |
class toCyc | ||
Definition | df-tocyc 32806* | 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 32807* | Value of the cycle builder. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
β’ πΆ = (toCycβπ·) β β’ (π· β π β πΆ = (π€ β {π’ β Word π· β£ π’:dom π’β1-1βπ·} β¦ (( I βΎ (π· β ran π€)) βͺ ((π€ cyclShift 1) β β‘π€)))) | ||
Theorem | tocycfv 32808 | 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 32809 | 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 32810 | 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 32811 | Lemma for cycpmfv1 32812 and cycpmfv2 32813. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ (π β π β (0..^(β―βπ))) β β’ (π β ((πΆβπ)β(πβπ)) = (((π cyclShift 1) β β‘π)β(πβπ))) | ||
Theorem | cycpmfv1 32812 | 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 32813 | 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 32814 | 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 32815 | Cyclic permutations are permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ π = (SymGrpβπ·) β β’ (π β (πΆβπ) β (Baseβπ)) | ||
Theorem | tocycf 32816* | The permutation cycle builder as a function. (Contributed by Thierry Arnoux, 25-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ π΅ = (Baseβπ) β β’ (π· β π β πΆ:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆπ΅) | ||
Theorem | tocyc01 32817 | 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 32818 | A cyclic permutation of 2 elements is a transposition. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΌ β π½) & β’ π = (pmTrspβπ·) β β’ (π β (πΆββ¨βπΌπ½ββ©) = (πβ{πΌ, π½})) | ||
Theorem | cycpm2cl 32819 | Closure for the 2-cycles. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΌ β π½) & β’ π = (SymGrpβπ·) β β’ (π β (πΆββ¨βπΌπ½ββ©) β (Baseβπ)) | ||
Theorem | cyc2fv1 32820 | Function value of a 2-cycle at the first point. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΌ β π½) & β’ π = (SymGrpβπ·) β β’ (π β ((πΆββ¨βπΌπ½ββ©)βπΌ) = π½) | ||
Theorem | cyc2fv2 32821 | Function value of a 2-cycle at the second point. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΌ β π½) & β’ π = (SymGrpβπ·) β β’ (π β ((πΆββ¨βπΌπ½ββ©)βπ½) = πΌ) | ||
Theorem | trsp2cyc 32822* | Exhibit the word a transposition corresponds to, as a cycle. (Contributed by Thierry Arnoux, 25-Sep-2023.) |
β’ π = ran (pmTrspβπ·) & β’ πΆ = (toCycβπ·) β β’ ((π· β π β§ π β π) β βπ β π· βπ β π· (π β π β§ π = (πΆββ¨βππββ©))) | ||
Theorem | cycpmco2f1 32823 | The word U used in cycpmco2 32832 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 32824 | 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 32825 | Lemma for cycpmco2 32832. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β β’ (π β ((πβπ)β((πββ¨βπΌπ½ββ©)βπΌ)) = ((πβπ)βπ½)) | ||
Theorem | cycpmco2lem2 32826 | Lemma for cycpmco2 32832. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β β’ (π β (πβπΈ) = πΌ) | ||
Theorem | cycpmco2lem3 32827 | Lemma for cycpmco2 32832. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β β’ (π β ((β―βπ) β 1) = (β―βπ)) | ||
Theorem | cycpmco2lem4 32828 | Lemma for cycpmco2 32832. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β β’ (π β ((πβπ)β((πββ¨βπΌπ½ββ©)βπΌ)) = ((πβπ)βπΌ)) | ||
Theorem | cycpmco2lem5 32829 | Lemma for cycpmco2 32832. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) & β’ (π β πΎ β ran π) & β’ (π β (β‘πβπΎ) = ((β―βπ) β 1)) β β’ (π β ((πβπ)βπΎ) = ((πβπ)βπΎ)) | ||
Theorem | cycpmco2lem6 32830 | Lemma for cycpmco2 32832. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) & β’ (π β πΎ β ran π) & β’ (π β πΎ β πΌ) & β’ (π β (β‘πβπΎ) β (πΈ..^((β―βπ) β 1))) β β’ (π β ((πβπ)βπΎ) = ((πβπ)βπΎ)) | ||
Theorem | cycpmco2lem7 32831 | Lemma for cycpmco2 32832. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
β’ π = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β π β dom π) & β’ (π β πΌ β (π· β ran π)) & β’ (π β π½ β ran π) & β’ πΈ = ((β‘πβπ½) + 1) & β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) & β’ (π β πΎ β ran π) & β’ (π β πΎ β π½) & β’ (π β (β‘πβπΎ) β (0..^πΈ)) β β’ (π β ((πβπ)βπΎ) = ((πβπ)βπΎ)) | ||
Theorem | cycpmco2 32832 | 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 32833 | Function value of a 2-cycle outside of its orbit. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β ((πΆββ¨βπΌπ½ββ©)βπΎ) = πΎ) | ||
Theorem | cycpm3cl 32834 | Closure of the 3-cycles in the permutations. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β (πΆββ¨βπΌπ½πΎββ©) β (Baseβπ)) | ||
Theorem | cycpm3cl2 32835 | Closure of the 3-cycles in the class of 3-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β (πΆββ¨βπΌπ½πΎββ©) β (πΆ β (β‘β― β {3}))) | ||
Theorem | cyc3fv1 32836 | Function value of a 3-cycle at the first point. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β ((πΆββ¨βπΌπ½πΎββ©)βπΌ) = π½) | ||
Theorem | cyc3fv2 32837 | Function value of a 3-cycle at the second point. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β ((πΆββ¨βπΌπ½πΎββ©)βπ½) = πΎ) | ||
Theorem | cyc3fv3 32838 | Function value of a 3-cycle at the third point. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) β β’ (π β ((πΆββ¨βπΌπ½πΎββ©)βπΎ) = πΌ) | ||
Theorem | cyc3co2 32839 | Represent a 3-cycle as a composition of two 2-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
β’ πΆ = (toCycβπ·) & β’ π = (SymGrpβπ·) & β’ (π β π· β π) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΌ β π½) & β’ (π β π½ β πΎ) & β’ (π β πΎ β πΌ) & β’ Β· = (+gβπ) β β’ (π β (πΆββ¨βπΌπ½πΎββ©) = ((πΆββ¨βπΌπΎββ©) Β· (πΆββ¨βπΌπ½ββ©))) | ||
Theorem | cycpmconjvlem 32840 | Lemma for cycpmconjv 32841. (Contributed by Thierry Arnoux, 9-Oct-2023.) |
β’ (π β πΉ:π·β1-1-ontoβπ·) & β’ (π β π΅ β π·) β β’ (π β ((πΉ βΎ (π· β π΅)) β β‘πΉ) = ( I βΎ (π· β ran (πΉ βΎ π΅)))) | ||
Theorem | cycpmconjv 32841 | 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 32842 | 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 32843* | 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 32844 | Value of the set of even permutations, the alternating group. (Contributed by Thierry Arnoux, 1-Nov-2023.) |
β’ π΄ = (pmEvenβπ·) β β’ (π· β π β π΄ = (β‘(pmSgnβπ·) β {1})) | ||
Theorem | cnmsgn0g 32845 | 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 32846 | The alternating group is a subgroup of the symmetric group. (Contributed by Thierry Arnoux, 1-Nov-2023.) |
β’ π = (SymGrpβπ·) & β’ π΄ = (pmEvenβπ·) β β’ (π· β Fin β π΄ β (SubGrpβπ)) | ||
Theorem | evpmid 32847 | The identity is an even permutation. (Contributed by Thierry Arnoux, 18-Sep-2023.) |
β’ π = (SymGrpβπ·) β β’ (π· β Fin β ( I βΎ π·) β (pmEvenβπ·)) | ||
Theorem | altgnsg 32848 | 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 32849 | 3-Cycles are even permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = ((toCycβπ·) β (β‘β― β {3})) & β’ π΄ = (pmEvenβπ·) β β’ (π· β Fin β πΆ β π΄) | ||
Theorem | cyc3genpmlem 32850* | Lemma for cyc3genpm 32851. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
β’ πΆ = (π β (β‘β― β {3})) & β’ π΄ = (pmEvenβπ·) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ Β· = (+gβπ) & β’ (π β πΌ β π·) & β’ (π β π½ β π·) & β’ (π β πΎ β π·) & β’ (π β πΏ β π·) & β’ (π β πΈ = (πββ¨βπΌπ½ββ©)) & β’ (π β πΉ = (πββ¨βπΎπΏββ©)) & β’ (π β π· β π) & β’ (π β πΌ β π½) & β’ (π β πΎ β πΏ) β β’ (π β βπ β Word πΆ(πΈ Β· πΉ) = (π Ξ£g π)) | ||
Theorem | cyc3genpm 32851* | 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 32852 | Cyclic permutations are permutations, similar to cycpmcl 32815, 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 32853 | Lemma for cycpmconjs 32855. (Contributed by Thierry Arnoux, 14-Oct-2023.) |
β’ πΆ = (π β (β‘β― β {π})) & β’ π = (SymGrpβπ·) & β’ π = (β―βπ·) & β’ π = (toCycβπ·) & β’ (π β π· β π) & β’ (π β π β Word π·) & β’ (π β π:dom πβ1-1βπ·) & β’ (π β (β―βπ) = π) β β’ (π β ((β‘π β (πβπ)) β π) = (( I βΎ (0..^π)) cyclShift 1)) | ||
Theorem | cycpmconjslem2 32854* | Lemma for cycpmconjs 32855. (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 32855* | 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 32856* | 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 32857 | Extend class notation to include the Signum function. |
class sgns | ||
Definition | df-sgns 32858* | Signum function for a structure. See also df-sgn 15058 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 32859* | The sign mapping. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ < = (ltβπ ) & β’ π = (sgnsβπ ) β β’ (π β π β π = (π₯ β π΅ β¦ if(π₯ = 0 , 0, if( 0 < π₯, 1, -1)))) | ||
Theorem | sgnsval 32860 | The sign value. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ < = (ltβπ ) & β’ π = (sgnsβπ ) β β’ ((π β π β§ π β π΅) β (πβπ) = if(π = 0 , 0, if( 0 < π, 1, -1))) | ||
Theorem | sgnsf 32861 | The sign function. (Contributed by Thierry Arnoux, 9-Sep-2018.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ < = (ltβπ ) & β’ π = (sgnsβπ ) β β’ (π β π β π:π΅βΆ{-1, 0, 1}) | ||
Syntax | cinftm 32862 | Class notation for the infinitesimal relation. |
class β | ||
Syntax | carchi 32863 | Class notation for the Archimedean property. |
class Archi | ||
Definition | df-inftm 32864* | 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 32865 | A structure said to be Archimedean if it has no infinitesimal elements. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ Archi = {π€ β£ (ββπ€) = β } | ||
Theorem | inftmrel 32866 | The infinitesimal relation for a structure π. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) β β’ (π β π β (ββπ) β (π΅ Γ π΅)) | ||
Theorem | isinftm 32867* | Express π₯ is infinitesimal with respect to π¦ for a structure π. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ Β· = (.gβπ) & β’ < = (ltβπ) β β’ ((π β π β§ π β π΅ β§ π β π΅) β (π(ββπ)π β ( 0 < π β§ βπ β β (π Β· π) < π))) | ||
Theorem | isarchi 32868* | Express the predicate "π is Archimedean ". (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ < = (ββπ) β β’ (π β π β (π β Archi β βπ₯ β π΅ βπ¦ β π΅ Β¬ π₯ < π¦)) | ||
Theorem | pnfinf 32869 | Plus infinity is an infinite for the completed real line, as any real number is infinitesimal compared to it. (Contributed by Thierry Arnoux, 1-Feb-2018.) |
β’ (π΄ β β+ β π΄(βββ*π )+β) | ||
Theorem | xrnarchi 32870 | The completed real line is not Archimedean. (Contributed by Thierry Arnoux, 1-Feb-2018.) |
β’ Β¬ β*π β Archi | ||
Theorem | isarchi2 32871* | Alternative way to express the predicate "π is Archimedean ", for Tosets. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ Β· = (.gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) β β’ ((π β Toset β§ π β Mnd) β (π β Archi β βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦ β€ (π Β· π₯)))) | ||
Theorem | submarchi 32872 | A submonoid is archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
β’ (((π β Toset β§ π β Archi) β§ π΄ β (SubMndβπ)) β (π βΎs π΄) β Archi) | ||
Theorem | isarchi3 32873* | This is the usual definition of the Archimedean property for an ordered group. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) β β’ (π β oGrp β (π β Archi β βπ₯ β π΅ βπ¦ β π΅ ( 0 < π₯ β βπ β β π¦ < (π Β· π₯)))) | ||
Theorem | archirng 32874* | Property of Archimedean ordered groups, framing positive π between multiples of π. (Contributed by Thierry Arnoux, 12-Apr-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ < = (ltβπ) & β’ β€ = (leβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ (π β 0 < π) β β’ (π β βπ β β0 ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) | ||
Theorem | archirngz 32875* | Property of Archimedean left and right ordered groups. (Contributed by Thierry Arnoux, 6-May-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ < = (ltβπ) & β’ β€ = (leβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ (π β (oppgβπ) β oGrp) β β’ (π β βπ β β€ ((π Β· π) < π β§ π β€ ((π + 1) Β· π))) | ||
Theorem | archiexdiv 32876* | In an Archimedean group, given two positive elements, there exists a "divisor" π. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) β β’ (((π β oGrp β§ π β Archi) β§ (π β π΅ β§ π β π΅) β§ 0 < π) β βπ β β π < (π Β· π)) | ||
Theorem | archiabllem1a 32877* | Lemma for archiabl 32884: In case an archimedean group π admits a smallest positive element π, then any positive element π of π can be written as (π Β· π) with π β β. Since the reciprocal holds for negative elements, π is then isomorphic to β€. (Contributed by Thierry Arnoux, 12-Apr-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ ((π β§ π₯ β π΅ β§ 0 < π₯) β π β€ π₯) & β’ (π β π β π΅) & β’ (π β 0 < π) β β’ (π β βπ β β π = (π Β· π)) | ||
Theorem | archiabllem1b 32878* | Lemma for archiabl 32884. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ ((π β§ π₯ β π΅ β§ 0 < π₯) β π β€ π₯) β β’ ((π β§ π¦ β π΅) β βπ β β€ π¦ = (π Β· π)) | ||
Theorem | archiabllem1 32879* | Archimedean ordered groups with a minimal positive value are abelian. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ (π β π β π΅) & β’ (π β 0 < π) & β’ ((π β§ π₯ β π΅ β§ 0 < π₯) β π β€ π₯) β β’ (π β π β Abel) | ||
Theorem | archiabllem2a 32880* | Lemma for archiabl 32884, which requires the group to be both left- and right-ordered. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ + = (+gβπ) & β’ (π β (oppgβπ) β oGrp) & β’ ((π β§ π β π΅ β§ 0 < π) β βπ β π΅ ( 0 < π β§ π < π)) & β’ (π β π β π΅) & β’ (π β 0 < π) β β’ (π β βπ β π΅ ( 0 < π β§ (π + π) β€ π)) | ||
Theorem | archiabllem2c 32881* | Lemma for archiabl 32884. (Contributed by Thierry Arnoux, 1-May-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ + = (+gβπ) & β’ (π β (oppgβπ) β oGrp) & β’ ((π β§ π β π΅ β§ 0 < π) β βπ β π΅ ( 0 < π β§ π < π)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β Β¬ (π + π) < (π + π)) | ||
Theorem | archiabllem2b 32882* | Lemma for archiabl 32884. (Contributed by Thierry Arnoux, 1-May-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ + = (+gβπ) & β’ (π β (oppgβπ) β oGrp) & β’ ((π β§ π β π΅ β§ 0 < π) β βπ β π΅ ( 0 < π β§ π < π)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π + π) = (π + π)) | ||
Theorem | archiabllem2 32883* | Archimedean ordered groups with no minimal positive value are abelian. (Contributed by Thierry Arnoux, 1-May-2018.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ β€ = (leβπ) & β’ < = (ltβπ) & β’ Β· = (.gβπ) & β’ (π β π β oGrp) & β’ (π β π β Archi) & β’ + = (+gβπ) & β’ (π β (oppgβπ) β oGrp) & β’ ((π β§ π β π΅ β§ 0 < π) β βπ β π΅ ( 0 < π β§ π < π)) β β’ (π β π β Abel) | ||
Theorem | archiabl 32884 | Archimedean left- and right- ordered groups are Abelian. (Contributed by Thierry Arnoux, 1-May-2018.) |
β’ ((π β oGrp β§ (oppgβπ) β oGrp β§ π β Archi) β π β Abel) | ||
Syntax | cslmd 32885 | Extend class notation with class of all semimodules. |
class SLMod | ||
Definition | df-slmd 32886* | Define the class of all (left) modules over semirings, i.e. semimodules, which are generalizations of left modules. A semimodule is a commutative monoid (=vectors) together with a semiring (=scalars) and a left scalar product connecting them. (0[,]+β) for example is not a full fledged left module, but is a semimodule. Definition of [Golan] p. 149. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
β’ SLMod = {π β CMnd β£ [(Baseβπ) / π£][(+gβπ) / π][( Β·π βπ) / π ][(Scalarβπ) / π][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β SRing β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€ β§ ((0gβπ)π π€) = (0gβπ))))} | ||
Theorem | isslmd 32887* | The predicate "is a semimodule". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) & β’ Γ = (.rβπΉ) & β’ 1 = (1rβπΉ) & β’ π = (0gβπΉ) β β’ (π β SLMod β (π β CMnd β§ πΉ β SRing β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€ β§ (π Β· π€) = 0 )))) | ||
Theorem | slmdlema 32888 | Lemma for properties of a semimodule. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & ⒠⨣ = (+gβπΉ) & β’ Γ = (.rβπΉ) & β’ 1 = (1rβπΉ) & β’ π = (0gβπΉ) β β’ ((π β SLMod β§ (π β πΎ β§ π β πΎ) β§ (π β π β§ π β π)) β (((π Β· π) β π β§ (π Β· (π + π)) = ((π Β· π) + (π Β· π)) β§ ((π ⨣ π ) Β· π) = ((π Β· π) + (π Β· π))) β§ (((π Γ π ) Β· π) = (π Β· (π Β· π)) β§ ( 1 Β· π) = π β§ (π Β· π) = 0 ))) | ||
Theorem | lmodslmd 32889 | Left semimodules generalize the notion of left modules. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ (π β LMod β π β SLMod) | ||
Theorem | slmdcmn 32890 | A semimodule is a commutative monoid. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ (π β SLMod β π β CMnd) | ||
Theorem | slmdmnd 32891 | A semimodule is a monoid. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ (π β SLMod β π β Mnd) | ||
Theorem | slmdsrg 32892 | The scalar component of a semimodule is a semiring. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
β’ πΉ = (Scalarβπ) β β’ (π β SLMod β πΉ β SRing) | ||
Theorem | slmdbn0 32893 | The base set of a semimodule is nonempty. (Contributed by Thierry Arnoux, 1-Apr-2018.) (Proof shortened by AV, 10-Jan-2023.) |
β’ π΅ = (Baseβπ) β β’ (π β SLMod β π΅ β β ) | ||
Theorem | slmdacl 32894 | Closure of ring addition for a semimodule. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ + = (+gβπΉ) β β’ ((π β SLMod β§ π β πΎ β§ π β πΎ) β (π + π) β πΎ) | ||
Theorem | slmdmcl 32895 | Closure of ring multiplication for a semimodule. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ Β· = (.rβπΉ) β β’ ((π β SLMod β§ π β πΎ β§ π β πΎ) β (π Β· π) β πΎ) | ||
Theorem | slmdsn0 32896 | The set of scalars in a semimodule is nonempty. (Contributed by Thierry Arnoux, 1-Apr-2018.) (Proof shortened by AV, 10-Jan-2023.) |
β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ (π β SLMod β π΅ β β ) | ||
Theorem | slmdvacl 32897 | Closure of vector addition for a semiring left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β SLMod β§ π β π β§ π β π) β (π + π) β π) | ||
Theorem | slmdass 32898 | Semiring left module vector sum is associative. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β SLMod β§ (π β π β§ π β π β§ π β π)) β ((π + π) + π) = (π + (π + π))) | ||
Theorem | slmdvscl 32899 | Closure of scalar product for a semiring left module. (hvmulcl 30810 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β SLMod β§ π β πΎ β§ π β π) β (π Β· π) β π) | ||
Theorem | slmdvsdi 32900 | Distributive law for scalar product. (ax-hvdistr1 30805 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (BaseβπΉ) β β’ ((π β SLMod β§ (π β πΎ β§ π β π β§ π β π)) β (π Β· (π + π)) = ((π Β· π) + (π Β· π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |