:: Properties of Groups :: by Gijs Geleijnse and Grzegorz Bancerek :: :: Received May 31, 2004 :: Copyright (c) 2004-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, STRUCT_0, GROUP_1, SUBSET_1, GROUP_2, FINSET_1, INT_2, CARD_1, GRAPH_1, RELAT_1, TARSKI, ALGSTR_0, ZFMISC_1, PBOOLE, REALSET1, NEWTON, INT_1, ARYTM_3, GROUP_4, ARYTM_1, NAT_1, FINSEQ_1, FUNCT_1, XXREAL_0, CQC_SIM1, XBOOLE_0, SETFAM_1, GROUP_8; notations XBOOLE_0, CARD_1, TARSKI, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, REALSET1, FUNCT_1, FUNCT_2, PBOOLE, INT_1, NAT_1, FINSET_1, GROUP_2, GROUP_4, GR_CY_1, FINSEQ_1, DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, INT_2; constructors WELLORD2, BINOP_1, REAL_1, NAT_D, BINOP_2, REALSET2, GROUP_4, GR_CY_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, STRUCT_0, GROUP_1, GROUP_2, GR_CY_1, ORDINAL1, FINSET_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve G for strict Group, a,b,x,y,z for Element of G, H,K for strict Subgroup of G, p for Element of NAT, A for Subset of G; theorem :: GROUP_8:1 for G being strict finite Group holds p is prime & card G = p implies ex a being Element of G st ord a = p; theorem :: GROUP_8:2 for G being Group, H being Subgroup of G, a1,a2 being Element of H for b1,b2 being Element of G st a1 = b1 & a2 = b2 holds a1*a2 = b1*b2; theorem :: GROUP_8:3 for G being Group, H being Subgroup of G, a being Element of H for b being Element of G st a = b for n being Element of NAT holds a|^n = b|^n; theorem :: GROUP_8:4 for G being Group, H being Subgroup of G, a being Element of H for b being Element of G st a = b for i being Integer holds a|^i = b|^i; theorem :: GROUP_8:5 for G being Group, H being Subgroup of G, a being Element of H for b being Element of G st a = b & G is finite holds ord a = ord b; theorem :: GROUP_8:6 for G being Group, H being Subgroup of G, h being Element of G st h in H holds H * h c= the carrier of H; theorem :: GROUP_8:7 for G being Group for a being Element of G st a <> 1_G holds gr {a} <> (1).G; theorem :: GROUP_8:8 for G being Group, m being Integer holds (1_G) |^ m = 1_G; theorem :: GROUP_8:9 for m being Integer holds a |^ (m * ord a) = 1_G; theorem :: GROUP_8:10 for a st a is not being_of_order_0 for m being Integer holds a |^ m = a |^(m mod ord a); theorem :: GROUP_8:11 b is not being_of_order_0 implies gr {b} is finite; theorem :: GROUP_8:12 b is being_of_order_0 implies b" is being_of_order_0; theorem :: GROUP_8:13 b is being_of_order_0 iff for n being Integer st b |^n = 1_G holds n = 0; theorem :: GROUP_8:14 for G st ex a st a <> 1_G holds (for H holds H = G or H = (1).G) iff G is cyclic & G is finite & ex p being Element of NAT st card G = p & p is prime; theorem :: GROUP_8:15 for G being Group, x,y,z being Element of G for A being Subset of G holds z in x * A * y iff ex a being Element of G st z = x * a * y & a in A; theorem :: GROUP_8:16 for G being Group, A being non empty Subset of G holds for x being Element of G holds card A = card (x" * A * x); definition let G, H, K; func Double_Cosets (H, K) -> Subset-Family of G means :: GROUP_8:def 1 A in it iff ex a st A = H * a * K; end; theorem :: GROUP_8:17 z in H * x * K iff ex g,h being Element of G st z = g * x * h & g in H & h in K; theorem :: GROUP_8:18 for H, K holds H * x * K = H * y * K or not ex z st z in H * x * K & z in H * y * K; reserve G for Group; reserve H, B, A for Subgroup of G, D for Subgroup of A; registration let G,A; cluster Left_Cosets A -> non empty; end; notation let G be Group; let H be Subgroup of G; synonym index (G,H) for index H; end; theorem :: GROUP_8:19 D = A /\ B & G is finite implies index(G,B) >= index(A,D); theorem :: GROUP_8:20 for G being finite Group, H be Subgroup of G holds index (G,H) > 0; theorem :: GROUP_8:21 for G being Group st G is finite for C being Subgroup of G for A,B being Subgroup of C for D being Subgroup of A st D = A /\ B for E being Subgroup of B st E = A /\ B for F being Subgroup of C st F = A /\ B holds index (C,A), index (C,B) are_coprime implies index (C,B) = index (A,D) & index (C,A) = index (B,E); theorem :: GROUP_8:22 for a being Element of G st a in H holds for j being Integer holds a |^ j in H; theorem :: GROUP_8:23 for G being strict Group st G <> (1).G ex b being Element of G st b <> 1_G; theorem :: GROUP_8:24 for G being strict Group for a being Element of G st G = gr{a} for H being strict Subgroup of G st H <> (1).G holds ex k being Nat st 0 < k & a |^k in H; theorem :: GROUP_8:25 for G being strict cyclic Group for H being strict Subgroup of G holds H is cyclic Group;