:: 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;