:: GROUP_8 semantic presentation
begin
theorem :: GROUP_8:1
for p being Element of NAT
for G being finite strict Group st p is prime & card G = p holds
ex a being Element of G st ord a = p
proof
let p be Element of NAT ; ::_thesis: for G being finite strict Group st p is prime & card G = p holds
ex a being Element of G st ord a = p
let G be finite strict Group; ::_thesis: ( p is prime & card G = p implies ex a being Element of G st ord a = p )
assume that
A1: p is prime and
A2: card G = p ; ::_thesis: ex a being Element of G st ord a = p
G is cyclic Group by A1, A2, GR_CY_1:21;
hence ex a being Element of G st ord a = p by A2, GR_CY_1:19; ::_thesis: verum
end;
theorem :: GROUP_8:2
for G being Group
for H being Subgroup of G
for a1, a2 being Element of H
for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds
a1 * a2 = b1 * b2
proof
let G be Group; ::_thesis: for H being Subgroup of G
for a1, a2 being Element of H
for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds
a1 * a2 = b1 * b2
let H be Subgroup of G; ::_thesis: for a1, a2 being Element of H
for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds
a1 * a2 = b1 * b2
let a1, a2 be Element of H; ::_thesis: for b1, b2 being Element of G st a1 = b1 & a2 = b2 holds
a1 * a2 = b1 * b2
A1: the carrier of H c= the carrier of G by GROUP_2:def_5;
let b1, b2 be Element of G; ::_thesis: ( a1 = b1 & a2 = b2 implies a1 * a2 = b1 * b2 )
assume that
A2: a1 = b1 and
A3: a2 = b2 ; ::_thesis: a1 * a2 = b1 * b2
dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def_1;
then A4: the multF of G is ManySortedSet of [: the carrier of G, the carrier of G:] by PARTFUN1:def_2;
the multF of H = the multF of G || the carrier of H by GROUP_2:def_5;
hence a1 * a2 = b1 * b2 by A1, A2, A3, A4, ALTCAT_1:5; ::_thesis: verum
end;
theorem :: GROUP_8:3
for G being Group
for H being Subgroup of G
for a being Element of H
for b being Element of G st a = b holds
for n being Element of NAT holds a |^ n = b |^ n by GROUP_4:1;
theorem :: GROUP_8:4
for G being Group
for H being Subgroup of G
for a being Element of H
for b being Element of G st a = b holds
for i being Integer holds a |^ i = b |^ i by GROUP_4:2;
theorem :: GROUP_8:5
for G being Group
for H being Subgroup of G
for a being Element of H
for b being Element of G st a = b & G is finite holds
ord a = ord b
proof
let G be Group; ::_thesis: for H being Subgroup of G
for a being Element of H
for b being Element of G st a = b & G is finite holds
ord a = ord b
let H be Subgroup of G; ::_thesis: for a being Element of H
for b being Element of G st a = b & G is finite holds
ord a = ord b
let a be Element of H; ::_thesis: for b being Element of G st a = b & G is finite holds
ord a = ord b
let b be Element of G; ::_thesis: ( a = b & G is finite implies ord a = ord b )
assume that
A1: a = b and
A2: G is finite ; ::_thesis: ord a = ord b
A3: not a is being_of_order_0 by A2, GR_CY_1:6;
A4: not b is being_of_order_0 by A2, GR_CY_1:6;
A5: a |^ (ord a) = 1_ H by A3, GROUP_1:def_11;
A6: b |^ (ord b) = 1_ G by A4, GROUP_1:def_11;
a |^ (ord a) = b |^ (ord a) by A1, GROUP_4:1;
then A7: ord b divides ord a by A5, A6, GROUP_1:44, GROUP_2:44;
a |^ (ord b) = 1_ G by A1, A6, GROUP_4:1;
then a |^ (ord b) = 1_ H by GROUP_2:44;
then ord a divides ord b by GROUP_1:44;
hence ord a = ord b by A7, NAT_D:5; ::_thesis: verum
end;
theorem :: GROUP_8:6
for G being Group
for H being Subgroup of G
for h being Element of G st h in H holds
H * h c= the carrier of H
proof
let G be Group; ::_thesis: for H being Subgroup of G
for h being Element of G st h in H holds
H * h c= the carrier of H
let H be Subgroup of G; ::_thesis: for h being Element of G st h in H holds
H * h c= the carrier of H
let h be Element of G; ::_thesis: ( h in H implies H * h c= the carrier of H )
assume A1: h in H ; ::_thesis: H * h c= the carrier of H
for a being set st a in H * h holds
a in the carrier of H
proof
let a be set ; ::_thesis: ( a in H * h implies a in the carrier of H )
assume a in H * h ; ::_thesis: a in the carrier of H
then consider g being Element of G such that
A2: a = g * h and
A3: g in H by GROUP_2:104;
g * h in H by A1, A3, GROUP_2:50;
hence a in the carrier of H by A2, STRUCT_0:def_5; ::_thesis: verum
end;
hence H * h c= the carrier of H by TARSKI:def_3; ::_thesis: verum
end;
theorem Th7: :: GROUP_8:7
for G being Group
for a being Element of G st a <> 1_ G holds
gr {a} <> (1). G
proof
let G be Group; ::_thesis: for a being Element of G st a <> 1_ G holds
gr {a} <> (1). G
let a be Element of G; ::_thesis: ( a <> 1_ G implies gr {a} <> (1). G )
assume A1: a <> 1_ G ; ::_thesis: gr {a} <> (1). G
assume A2: gr {a} = (1). G ; ::_thesis: contradiction
A3: the carrier of ((1). G) = {(1_ G)} by GROUP_2:def_7;
A4: {a} c= the carrier of (gr {a}) by GROUP_4:def_4;
for xx being set st xx = a holds
xx = 1_ G
proof
let xx be set ; ::_thesis: ( xx = a implies xx = 1_ G )
assume xx = a ; ::_thesis: xx = 1_ G
then xx in {a} by TARSKI:def_1;
hence xx = 1_ G by A2, A3, A4, TARSKI:def_1; ::_thesis: verum
end;
hence contradiction by A1; ::_thesis: verum
end;
theorem :: GROUP_8:8
for G being Group
for m being Integer holds (1_ G) |^ m = 1_ G by GROUP_1:31;
theorem Th9: :: GROUP_8:9
for G being strict Group
for a being Element of G
for m being Integer holds a |^ (m * (ord a)) = 1_ G
proof
let G be strict Group; ::_thesis: for a being Element of G
for m being Integer holds a |^ (m * (ord a)) = 1_ G
let a be Element of G; ::_thesis: for m being Integer holds a |^ (m * (ord a)) = 1_ G
let m be Integer; ::_thesis: a |^ (m * (ord a)) = 1_ G
percases ( a is being_of_order_0 or not a is being_of_order_0 ) ;
suppose a is being_of_order_0 ; ::_thesis: a |^ (m * (ord a)) = 1_ G
then ord a = 0 by GROUP_1:def_11;
hence a |^ (m * (ord a)) = 1_ G by GROUP_1:25; ::_thesis: verum
end;
suppose not a is being_of_order_0 ; ::_thesis: a |^ (m * (ord a)) = 1_ G
then A1: a |^ (ord a) = 1_ G by GROUP_1:def_11;
(1_ G) |^ m = 1_ G by GROUP_1:31;
hence a |^ (m * (ord a)) = 1_ G by A1, GROUP_1:35; ::_thesis: verum
end;
end;
end;
theorem Th10: :: GROUP_8:10
for G being strict Group
for a being Element of G st not a is being_of_order_0 holds
for m being Integer holds a |^ m = a |^ (m mod (ord a))
proof
let G be strict Group; ::_thesis: for a being Element of G st not a is being_of_order_0 holds
for m being Integer holds a |^ m = a |^ (m mod (ord a))
let a be Element of G; ::_thesis: ( not a is being_of_order_0 implies for m being Integer holds a |^ m = a |^ (m mod (ord a)) )
assume A1: not a is being_of_order_0 ; ::_thesis: for m being Integer holds a |^ m = a |^ (m mod (ord a))
let m be Integer; ::_thesis: a |^ m = a |^ (m mod (ord a))
ord a <> 0 by A1, GROUP_1:def_11;
then m mod (ord a) = m - ((m div (ord a)) * (ord a)) by INT_1:def_10;
then a |^ (m mod (ord a)) = a |^ (m + (- ((1 * (m div (ord a))) * (ord a))))
.= (a |^ m) * (a |^ ((- (m div (ord a))) * (ord a))) by GROUP_1:33
.= (a |^ m) * (1_ G) by Th9
.= a |^ m by GROUP_1:def_4 ;
hence a |^ m = a |^ (m mod (ord a)) ; ::_thesis: verum
end;
theorem Th11: :: GROUP_8:11
for G being strict Group
for b being Element of G st not b is being_of_order_0 holds
gr {b} is finite
proof
let G be strict Group; ::_thesis: for b being Element of G st not b is being_of_order_0 holds
gr {b} is finite
let b be Element of G; ::_thesis: ( not b is being_of_order_0 implies gr {b} is finite )
assume A1: not b is being_of_order_0 ; ::_thesis: gr {b} is finite
then A2: ord b <> 0 by GROUP_1:def_11;
deffunc H1( Nat) -> Element of the carrier of G = b |^ $1;
consider f being FinSequence such that
A3: ( len f = ord b & ( for i being Nat st i in dom f holds
f . i = H1(i) ) ) from FINSEQ_1:sch_2();
A4: dom f = Seg (ord b) by A3, FINSEQ_1:def_3;
the carrier of (gr {b}) c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (gr {b}) or x in rng f )
assume x in the carrier of (gr {b}) ; ::_thesis: x in rng f
then A5: x in gr {b} by STRUCT_0:def_5;
then x in G by GROUP_2:40;
then reconsider a = x as Element of G by STRUCT_0:def_5;
consider m being Integer such that
A6: a = b |^ m by A5, GR_CY_1:5;
set k = m mod (ord b);
reconsider k = m mod (ord b) as Element of NAT by INT_1:3, NEWTON:64;
A7: a = b |^ k by A1, A6, Th10;
percases ( k = 0 or k <> 0 ) ;
supposeA8: k = 0 ; ::_thesis: x in rng f
ord b >= 0 + 1 by A2, NAT_1:13;
then A9: ord b in Seg (ord b) by FINSEQ_1:1;
a = 1_ G by A7, A8, GROUP_1:25
.= b |^ (ord b) by A1, GROUP_1:def_11
.= f . (ord b) by A3, A4, A9 ;
hence x in rng f by A4, A9, FUNCT_1:def_3; ::_thesis: verum
end;
supposeA10: k <> 0 ; ::_thesis: x in rng f
A11: k < ord b by A2, NEWTON:65;
k >= 0 + 1 by A10, NAT_1:13;
then A12: k in Seg (ord b) by A11, FINSEQ_1:1;
then a = f . k by A3, A4, A7;
hence x in rng f by A4, A12, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
hence the carrier of (gr {b}) is finite ; :: according to STRUCT_0:def_11 ::_thesis: verum
end;
theorem Th12: :: GROUP_8:12
for G being strict Group
for b being Element of G st b is being_of_order_0 holds
b " is being_of_order_0
proof
let G be strict Group; ::_thesis: for b being Element of G st b is being_of_order_0 holds
b " is being_of_order_0
let b be Element of G; ::_thesis: ( b is being_of_order_0 implies b " is being_of_order_0 )
assume A1: b is being_of_order_0 ; ::_thesis: b " is being_of_order_0
for n being Nat st (b ") |^ n = 1_ G holds
n = 0
proof
let n be Nat; ::_thesis: ( (b ") |^ n = 1_ G implies n = 0 )
assume (b ") |^ n = 1_ G ; ::_thesis: n = 0
then (b |^ n) " = 1_ G by GROUP_1:37;
then (b |^ n) " = (1_ G) " by GROUP_1:8;
then b |^ n = 1_ G by GROUP_1:9;
hence n = 0 by A1, GROUP_1:def_10; ::_thesis: verum
end;
hence b " is being_of_order_0 by GROUP_1:def_10; ::_thesis: verum
end;
theorem Th13: :: GROUP_8:13
for G being strict Group
for b being Element of G holds
( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds
n = 0 )
proof
let G be strict Group; ::_thesis: for b being Element of G holds
( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds
n = 0 )
let b be Element of G; ::_thesis: ( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds
n = 0 )
thus ( b is being_of_order_0 implies for n being Integer st b |^ n = 1_ G holds
n = 0 ) ::_thesis: ( ( for n being Integer st b |^ n = 1_ G holds
n = 0 ) implies b is being_of_order_0 )
proof
assume A1: b is being_of_order_0 ; ::_thesis: for n being Integer st b |^ n = 1_ G holds
n = 0
A2: for m being Element of NAT st b |^ (- m) = 1_ G holds
m = 0
proof
let m be Element of NAT ; ::_thesis: ( b |^ (- m) = 1_ G implies m = 0 )
assume A3: b |^ (- m) = 1_ G ; ::_thesis: m = 0
b |^ (- m) = (b |^ m) " by GROUP_1:36;
then A4: (b ") |^ m = 1_ G by A3, GROUP_1:37;
b " is being_of_order_0 by A1, Th12;
hence m = 0 by A4, GROUP_1:def_10; ::_thesis: verum
end;
for n being Integer st b |^ n = 1_ G holds
n = 0
proof
let n be Integer; ::_thesis: ( b |^ n = 1_ G implies n = 0 )
assume A5: b |^ n = 1_ G ; ::_thesis: n = 0
consider k being Element of NAT such that
A6: ( n = k or n = - k ) by INT_1:2;
percases ( n = k or n = - k ) by A6;
suppose n = k ; ::_thesis: n = 0
hence n = 0 by A1, A5, GROUP_1:def_10; ::_thesis: verum
end;
supposeA7: n = - k ; ::_thesis: n = 0
then k = 0 by A2, A5;
hence n = 0 by A7; ::_thesis: verum
end;
end;
end;
hence for n being Integer st b |^ n = 1_ G holds
n = 0 ; ::_thesis: verum
end;
assume for n being Integer st b |^ n = 1_ G holds
n = 0 ; ::_thesis: b is being_of_order_0
then for n being Nat st b |^ n = 1_ G holds
n = 0 ;
hence b is being_of_order_0 by GROUP_1:def_10; ::_thesis: verum
end;
theorem :: GROUP_8:14
for G being strict Group st ex a being Element of G st a <> 1_ G holds
( ( for H being strict Subgroup of G 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 ) ) )
proof
let G be strict Group; ::_thesis: ( ex a being Element of G st a <> 1_ G implies ( ( for H being strict Subgroup of G 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 ) ) ) )
assume A1: ex a being Element of G st a <> 1_ G ; ::_thesis: ( ( for H being strict Subgroup of G 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 ) ) )
thus ( ( for H being strict Subgroup of G holds
( H = G or H = (1). G ) ) implies ( G is cyclic & G is finite & ex p being Element of NAT st
( card G = p & p is prime ) ) ) ::_thesis: ( G is cyclic & G is finite & ex p being Element of NAT st
( card G = p & p is prime ) implies for H being strict Subgroup of G holds
( H = G or H = (1). G ) )
proof
assume A2: for H being strict Subgroup of G holds
( H = G or H = (1). G ) ; ::_thesis: ( G is cyclic & G is finite & ex p being Element of NAT st
( card G = p & p is prime ) )
consider b being Element of G such that
A3: b <> 1_ G by A1;
A4: gr {b} = G by A2, A3, Th7;
A5: not b is being_of_order_0
proof
assume A6: b is being_of_order_0 ; ::_thesis: contradiction
then A7: b |^ 2 <> 1_ G by GROUP_1:def_10;
not b in gr {(b |^ 2)}
proof
assume b in gr {(b |^ 2)} ; ::_thesis: contradiction
then consider j1 being Integer such that
A8: b = (b |^ 2) |^ j1 by GR_CY_1:5;
b = b |^ (2 * j1) by A8, GROUP_1:35;
then (b ") * (b |^ (2 * j1)) = 1_ G by GROUP_1:def_5;
then (b |^ (- 1)) * (b |^ (2 * j1)) = 1_ G by GROUP_1:32;
then b |^ ((- 1) + (2 * j1)) = 1_ G by GROUP_1:33;
then (- 1) + (2 * j1) = 0 by A6, Th13;
hence contradiction by INT_1:9; ::_thesis: verum
end;
then gr {(b |^ 2)} <> G by A4, GR_CY_2:2;
hence contradiction by A2, A7, Th7; ::_thesis: verum
end;
then consider n being Element of NAT such that
A9: n = ord b and
not b is being_of_order_0 ;
A10: G is finite by A4, A5, Th11;
then A11: card G = n by A4, A9, GR_CY_1:7;
n is prime
proof
assume A12: not n is prime ; ::_thesis: contradiction
ex u, v being Element of NAT st
( u > 1 & v > 1 & n = u * v )
proof
A13: ( not n > 1 or ex m being Nat st
( m divides n & not m = 1 & not m = n ) ) by A12, INT_2:def_4;
n >= 1 by A10, A11, GROUP_1:45;
then n > 1 by A3, A9, GROUP_1:43, XXREAL_0:1;
then consider m being Nat such that
A14: m <> 1 and
A15: m <> n and
A16: m divides n by A13;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
consider o being Nat such that
A17: n = m * o by A16, NAT_D:def_3;
reconsider o = o as Element of NAT by ORDINAL1:def_12;
take u = m; ::_thesis: ex v being Element of NAT st
( u > 1 & v > 1 & n = u * v )
take v = o; ::_thesis: ( u > 1 & v > 1 & n = u * v )
u <> 0
proof
assume u = 0 ; ::_thesis: contradiction
then n = 0 * (n div 0) by A16, NAT_D:3;
hence contradiction by A10, A11; ::_thesis: verum
end;
then A18: 0 + 1 <= u by INT_1:7;
0 < v by A10, A11, A17;
then A19: 0 + 1 <= v by INT_1:7;
v <> 1 by A15, A17;
hence ( u > 1 & v > 1 & n = u * v ) by A14, A17, A18, A19, XXREAL_0:1; ::_thesis: verum
end;
then consider u, v being Element of NAT such that
A20: u > 1 and
A21: v > 1 and
A22: n = u * v ;
ord (b |^ v) = u by A4, A10, A11, A22, GR_CY_2:8;
then A23: card (gr {(b |^ v)}) = u by A10, GR_CY_1:7;
A24: u <> n by A20, A21, A22, XCMPLX_1:7;
gr {(b |^ v)} <> (1). G by A20, A23, GROUP_2:69;
hence contradiction by A2, A11, A23, A24; ::_thesis: verum
end;
hence ( G is cyclic & G is finite & ex p being Element of NAT st
( card G = p & p is prime ) ) by A4, A5, A11, Th11, GR_CY_2:4; ::_thesis: verum
end;
assume that
G is cyclic and
A25: G is finite and
A26: ex p being Element of NAT st
( card G = p & p is prime ) ; ::_thesis: for H being strict Subgroup of G holds
( H = G or H = (1). G )
let H be strict Subgroup of G; ::_thesis: ( H = G or H = (1). G )
reconsider G = G as finite Group by A25;
reconsider H = H as Subgroup of G ;
card G = (card H) * (index H) by GROUP_2:147;
then A27: card H divides card G by NAT_D:def_3;
percases ( card H = card G or card H = 1 ) by A26, A27, INT_2:def_4;
suppose card H = card G ; ::_thesis: ( H = G or H = (1). G )
hence ( H = G or H = (1). G ) by GROUP_2:73; ::_thesis: verum
end;
suppose card H = 1 ; ::_thesis: ( H = G or H = (1). G )
hence ( H = G or H = (1). G ) by GROUP_2:70; ::_thesis: verum
end;
end;
end;
theorem Th15: :: GROUP_8:15
for G being Group
for 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 ) )
proof
let G be Group; ::_thesis: for 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 ) )
let x, y, z be Element of G; ::_thesis: 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 ) )
let A be Subset of G; ::_thesis: ( z in (x * A) * y iff ex a being Element of G st
( z = (x * a) * y & a in A ) )
thus ( z in (x * A) * y implies ex a being Element of G st
( z = (x * a) * y & a in A ) ) ::_thesis: ( ex a being Element of G st
( z = (x * a) * y & a in A ) implies z in (x * A) * y )
proof
assume z in (x * A) * y ; ::_thesis: ex a being Element of G st
( z = (x * a) * y & a in A )
then consider b being Element of G such that
A1: z = b * y and
A2: b in x * A by GROUP_2:28;
consider u being Element of G such that
A3: b = x * u and
A4: u in A by A2, GROUP_2:27;
take u ; ::_thesis: ( z = (x * u) * y & u in A )
thus ( z = (x * u) * y & u in A ) by A1, A3, A4; ::_thesis: verum
end;
given a being Element of G such that A5: z = (x * a) * y and
A6: a in A ; ::_thesis: z in (x * A) * y
ex h being Element of G st
( z = h * y & h in x * A )
proof
take x * a ; ::_thesis: ( z = (x * a) * y & x * a in x * A )
thus ( z = (x * a) * y & x * a in x * A ) by A5, A6, GROUP_2:27; ::_thesis: verum
end;
hence z in (x * A) * y by GROUP_2:28; ::_thesis: verum
end;
theorem :: GROUP_8:16
for G being Group
for A being non empty Subset of G
for x being Element of G holds card A = card (((x ") * A) * x)
proof
let G be Group; ::_thesis: for A being non empty Subset of G
for x being Element of G holds card A = card (((x ") * A) * x)
let A be non empty Subset of G; ::_thesis: for x being Element of G holds card A = card (((x ") * A) * x)
let x be Element of G; ::_thesis: card A = card (((x ") * A) * x)
set B = ((x ") * A) * x;
( not A is empty & not ((x ") * A) * x is empty )
proof
set a = the Element of A;
((x ") * the Element of A) * x in ((x ") * A) * x by Th15;
hence ( not A is empty & not ((x ") * A) * x is empty ) ; ::_thesis: verum
end;
then reconsider B = ((x ") * A) * x as non empty Subset of G ;
deffunc H1( Element of G) -> Element of the carrier of G = ((x ") * $1) * x;
consider f being Function of A, the carrier of G such that
A1: for a being Element of A holds f . a = H1(a) from FUNCT_2:sch_4();
A2: dom f = A by FUNCT_2:def_1;
A3: rng f c= B
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in rng f or s in B )
assume s in rng f ; ::_thesis: s in B
then consider a being set such that
A4: a in A and
A5: s = f . a by A2, FUNCT_1:def_3;
reconsider a = a as Element of A by A4;
s = H1(a) by A1, A5;
hence s in B by Th15; ::_thesis: verum
end;
A6: B c= rng f
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in B or s in rng f )
assume s in B ; ::_thesis: s in rng f
then consider a being Element of G such that
A7: s = ((x ") * a) * x and
A8: a in A by Th15;
ex x being Element of G st
( x in dom f & s = f . x )
proof
take a ; ::_thesis: ( a in dom f & s = f . a )
thus ( a in dom f & s = f . a ) by A1, A7, A8, FUNCT_2:def_1; ::_thesis: verum
end;
hence s in rng f by FUNCT_1:def_3; ::_thesis: verum
end;
reconsider f = f as Function of A,B by A2, A3, FUNCT_2:2;
deffunc H2( Element of G) -> Element of the carrier of G = (x * $1) * (x ");
consider g being Function of B, the carrier of G such that
A9: for b being Element of B holds g . b = H2(b) from FUNCT_2:sch_4();
A10: dom g = B by FUNCT_2:def_1;
rng g c= A
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in rng g or s in A )
assume s in rng g ; ::_thesis: s in A
then consider a being set such that
A11: a in B and
A12: s = g . a by A10, FUNCT_1:def_3;
reconsider a = a as Element of B by A11;
A13: s = H2(a) by A9, A12;
consider c being Element of G such that
A14: a = ((x ") * c) * x and
A15: c in A by Th15;
s = ((x * ((x ") * c)) * x) * (x ") by A13, A14, GROUP_1:def_3
.= (((x * (x ")) * c) * x) * (x ") by GROUP_1:def_3
.= ((x * (x ")) * c) * (x * (x ")) by GROUP_1:def_3
.= ((1_ G) * c) * (x * (x ")) by GROUP_1:def_5
.= ((1_ G) * c) * (1_ G) by GROUP_1:def_5
.= (1_ G) * c by GROUP_1:def_4
.= c by GROUP_1:def_4 ;
hence s in A by A15; ::_thesis: verum
end;
then reconsider g = g as Function of B,A by A10, FUNCT_2:2;
A16: for a, b being Element of A st f . a = f . b holds
a = b
proof
let a, b be Element of A; ::_thesis: ( f . a = f . b implies a = b )
assume A17: f . a = f . b ; ::_thesis: a = b
A18: ((x ") * a) * x in B by Th15;
A19: ((x ") * b) * x in B by Th15;
A20: g . (f . a) = g . (((x ") * a) * x) by A1
.= (x * (((x ") * a) * x)) * (x ") by A9, A18
.= ((x * ((x ") * a)) * x) * (x ") by GROUP_1:def_3
.= (((x * (x ")) * a) * x) * (x ") by GROUP_1:def_3
.= ((x * (x ")) * a) * (x * (x ")) by GROUP_1:def_3
.= ((1_ G) * a) * (x * (x ")) by GROUP_1:def_5
.= a * (x * (x ")) by GROUP_1:def_4
.= a * (1_ G) by GROUP_1:def_5
.= a by GROUP_1:def_4 ;
g . (f . b) = g . (((x ") * b) * x) by A1
.= (x * (((x ") * b) * x)) * (x ") by A9, A19
.= ((x * ((x ") * b)) * x) * (x ") by GROUP_1:def_3
.= (((x * (x ")) * b) * x) * (x ") by GROUP_1:def_3
.= ((x * (x ")) * b) * (x * (x ")) by GROUP_1:def_3
.= ((1_ G) * b) * (x * (x ")) by GROUP_1:def_5
.= b * (x * (x ")) by GROUP_1:def_4
.= b * (1_ G) by GROUP_1:def_5
.= b by GROUP_1:def_4 ;
hence a = b by A17, A20; ::_thesis: verum
end;
A,B are_equipotent
proof
take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = A & rng f = B )
thus ( f is one-to-one & dom f = A & rng f = B ) by A3, A6, A16, FUNCT_2:def_1, GROUP_6:1, XBOOLE_0:def_10; ::_thesis: verum
end;
hence card A = card (((x ") * A) * x) by CARD_1:5; ::_thesis: verum
end;
definition
let G be strict Group;
let H, K be strict Subgroup of G;
func Double_Cosets (H,K) -> Subset-Family of G means :: GROUP_8:def 1
for A being Subset of G holds
( A in it iff ex a being Element of G st A = (H * a) * K );
existence
ex b1 being Subset-Family of G st
for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = (H * a) * K )
proof
defpred S1[ set ] means ex a being Element of G st $1 = (H * a) * K;
ex F being Subset-Family of G st
for A being Subset of G holds
( A in F iff S1[A] ) from SUBSET_1:sch_3();
hence ex b1 being Subset-Family of G st
for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = (H * a) * K ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of G st ( for A being Subset of G holds
( A in b1 iff ex a being Element of G st A = (H * a) * K ) ) & ( for A being Subset of G holds
( A in b2 iff ex a being Element of G st A = (H * a) * K ) ) holds
b1 = b2
proof
let F1, F2 be Subset-Family of G; ::_thesis: ( ( for A being Subset of G holds
( A in F1 iff ex a being Element of G st A = (H * a) * K ) ) & ( for A being Subset of G holds
( A in F2 iff ex a being Element of G st A = (H * a) * K ) ) implies F1 = F2 )
defpred S1[ set ] means ex a being Element of G st $1 = (H * a) * K;
assume A1: for A being Subset of G holds
( A in F1 iff S1[A] ) ; ::_thesis: ( ex A being Subset of G st
( ( A in F2 implies ex a being Element of G st A = (H * a) * K ) implies ( ex a being Element of G st A = (H * a) * K & not A in F2 ) ) or F1 = F2 )
assume A2: for A being Subset of G holds
( A in F2 iff S1[A] ) ; ::_thesis: F1 = F2
thus F1 = F2 from SUBSET_1:sch_4(A1, A2); ::_thesis: verum
end;
end;
:: deftheorem defines Double_Cosets GROUP_8:def_1_:_
for G being strict Group
for H, K being strict Subgroup of G
for b4 being Subset-Family of G holds
( b4 = Double_Cosets (H,K) iff for A being Subset of G holds
( A in b4 iff ex a being Element of G st A = (H * a) * K ) );
theorem Th17: :: GROUP_8:17
for G being strict Group
for z, x being Element of G
for H, K being strict Subgroup of G holds
( z in (H * x) * K iff ex g, h being Element of G st
( z = (g * x) * h & g in H & h in K ) )
proof
let G be strict Group; ::_thesis: for z, x being Element of G
for H, K being strict Subgroup of G holds
( z in (H * x) * K iff ex g, h being Element of G st
( z = (g * x) * h & g in H & h in K ) )
let z, x be Element of G; ::_thesis: for H, K being strict Subgroup of G holds
( z in (H * x) * K iff ex g, h being Element of G st
( z = (g * x) * h & g in H & h in K ) )
let H, K be strict Subgroup of G; ::_thesis: ( z in (H * x) * K iff ex g, h being Element of G st
( z = (g * x) * h & g in H & h in K ) )
thus ( z in (H * x) * K implies ex g, h being Element of G st
( z = (g * x) * h & g in H & h in K ) ) ::_thesis: ( ex g, h being Element of G st
( z = (g * x) * h & g in H & h in K ) implies z in (H * x) * K )
proof
assume z in (H * x) * K ; ::_thesis: ex g, h being Element of G st
( z = (g * x) * h & g in H & h in K )
then consider g1, g2 being Element of G such that
A1: z = g1 * g2 and
A2: g1 in H * x and
A3: g2 in K by GROUP_2:94;
ex h1 being Element of G st
( g1 = h1 * x & h1 in H ) by A2, GROUP_2:104;
hence ex g, h being Element of G st
( z = (g * x) * h & g in H & h in K ) by A1, A3; ::_thesis: verum
end;
given g, h being Element of G such that A4: z = (g * x) * h and
A5: g in H and
A6: h in K ; ::_thesis: z in (H * x) * K
ex g1, g2 being Element of G st
( z = g1 * g2 & g1 in H * x & g2 in K )
proof
set g1 = g * x;
g * x in H * x by A5, GROUP_2:104;
hence ex g1, g2 being Element of G st
( z = g1 * g2 & g1 in H * x & g2 in K ) by A4, A6; ::_thesis: verum
end;
hence z in (H * x) * K by GROUP_2:94; ::_thesis: verum
end;
theorem :: GROUP_8:18
for G being strict Group
for x, y being Element of G
for H, K being strict Subgroup of G holds
( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )
proof
let G be strict Group; ::_thesis: for x, y being Element of G
for H, K being strict Subgroup of G holds
( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )
let x, y be Element of G; ::_thesis: for H, K being strict Subgroup of G holds
( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )
let H, K be strict Subgroup of G; ::_thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )
percases ( for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) or ex z being Element of G st
( z in (H * x) * K & z in (H * y) * K ) ) ;
suppose for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) ; ::_thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )
hence ( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) ) ; ::_thesis: verum
end;
suppose ex z being Element of G st
( z in (H * x) * K & z in (H * y) * K ) ; ::_thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) )
then consider z being Element of G such that
A1: z in (H * x) * K and
A2: z in (H * y) * K ;
consider h1, k1 being Element of G such that
A3: z = (h1 * x) * k1 and
A4: h1 in H and
A5: k1 in K by A1, Th17;
consider h2, k2 being Element of G such that
A6: z = (h2 * y) * k2 and
A7: h2 in H and
A8: k2 in K by A2, Th17;
for a being set st a in (H * x) * K holds
a in (H * y) * K
proof
let a be set ; ::_thesis: ( a in (H * x) * K implies a in (H * y) * K )
assume a in (H * x) * K ; ::_thesis: a in (H * y) * K
then consider h, k being Element of G such that
A9: a = (h * x) * k and
A10: h in H and
A11: k in K by Th17;
ex c, d being Element of G st
( a = (c * y) * d & c in H & d in K )
proof
h = h * (1_ G) by GROUP_1:def_4;
then A12: (h * x) * k = (((h * (1_ G)) * x) * (1_ G)) * k by GROUP_1:def_4;
1_ G = (h1 ") * h1 by GROUP_1:def_5;
then A13: (h * x) * k = (((h * ((h1 ") * h1)) * x) * (k1 * (k1 "))) * k by A12, GROUP_1:def_5
.= ((((h * ((h1 ") * h1)) * x) * k1) * (k1 ")) * k by GROUP_1:def_3
.= (((((h * (h1 ")) * h1) * x) * k1) * (k1 ")) * k by GROUP_1:def_3
.= ((((h * (h1 ")) * (h1 * x)) * k1) * (k1 ")) * k by GROUP_1:def_3
.= (((h * (h1 ")) * ((h2 * y) * k2)) * (k1 ")) * k by A3, A6, GROUP_1:def_3
.= ((((h * (h1 ")) * (h2 * y)) * k2) * (k1 ")) * k by GROUP_1:def_3
.= (((((h * (h1 ")) * h2) * y) * k2) * (k1 ")) * k by GROUP_1:def_3
.= ((((h * (h1 ")) * h2) * y) * (k2 * (k1 "))) * k by GROUP_1:def_3
.= (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) by GROUP_1:def_3 ;
take (h * (h1 ")) * h2 ; ::_thesis: ex d being Element of G st
( a = (((h * (h1 ")) * h2) * y) * d & (h * (h1 ")) * h2 in H & d in K )
take (k2 * (k1 ")) * k ; ::_thesis: ( a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) & (h * (h1 ")) * h2 in H & (k2 * (k1 ")) * k in K )
h1 " in H by A4, GROUP_2:51;
then A14: h * (h1 ") in H by A10, GROUP_2:50;
k1 " in K by A5, GROUP_2:51;
then k2 * (k1 ") in K by A8, GROUP_2:50;
hence ( a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) & (h * (h1 ")) * h2 in H & (k2 * (k1 ")) * k in K ) by A7, A9, A11, A13, A14, GROUP_2:50; ::_thesis: verum
end;
hence a in (H * y) * K by Th17; ::_thesis: verum
end;
then A15: (H * x) * K c= (H * y) * K by TARSKI:def_3;
for a being set st a in (H * y) * K holds
a in (H * x) * K
proof
let a be set ; ::_thesis: ( a in (H * y) * K implies a in (H * x) * K )
assume a in (H * y) * K ; ::_thesis: a in (H * x) * K
then consider h, k being Element of G such that
A16: a = (h * y) * k and
A17: h in H and
A18: k in K by Th17;
ex c, d being Element of G st
( a = (c * x) * d & c in H & d in K )
proof
h = h * (1_ G) by GROUP_1:def_4;
then A19: (h * y) * k = (((h * (1_ G)) * y) * (1_ G)) * k by GROUP_1:def_4;
1_ G = (h2 ") * h2 by GROUP_1:def_5;
then A20: (h * y) * k = (((h * ((h2 ") * h2)) * y) * (k2 * (k2 "))) * k by A19, GROUP_1:def_5
.= ((((h * ((h2 ") * h2)) * y) * k2) * (k2 ")) * k by GROUP_1:def_3
.= (((((h * (h2 ")) * h2) * y) * k2) * (k2 ")) * k by GROUP_1:def_3
.= ((((h * (h2 ")) * (h2 * y)) * k2) * (k2 ")) * k by GROUP_1:def_3
.= (((h * (h2 ")) * ((h1 * x) * k1)) * (k2 ")) * k by A3, A6, GROUP_1:def_3
.= ((((h * (h2 ")) * (h1 * x)) * k1) * (k2 ")) * k by GROUP_1:def_3
.= (((((h * (h2 ")) * h1) * x) * k1) * (k2 ")) * k by GROUP_1:def_3
.= ((((h * (h2 ")) * h1) * x) * (k1 * (k2 "))) * k by GROUP_1:def_3
.= (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) by GROUP_1:def_3 ;
take (h * (h2 ")) * h1 ; ::_thesis: ex d being Element of G st
( a = (((h * (h2 ")) * h1) * x) * d & (h * (h2 ")) * h1 in H & d in K )
take (k1 * (k2 ")) * k ; ::_thesis: ( a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) & (h * (h2 ")) * h1 in H & (k1 * (k2 ")) * k in K )
h2 " in H by A7, GROUP_2:51;
then A21: h * (h2 ") in H by A17, GROUP_2:50;
k2 " in K by A8, GROUP_2:51;
then k1 * (k2 ") in K by A5, GROUP_2:50;
hence ( a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) & (h * (h2 ")) * h1 in H & (k1 * (k2 ")) * k in K ) by A4, A16, A18, A20, A21, GROUP_2:50; ::_thesis: verum
end;
hence a in (H * x) * K by Th17; ::_thesis: verum
end;
then (H * y) * K c= (H * x) * K by TARSKI:def_3;
hence ( (H * x) * K = (H * y) * K or for z being Element of G holds
( not z in (H * x) * K or not z in (H * y) * K ) ) by A15, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;
registration
let G be Group;
let A be Subgroup of G;
cluster Left_Cosets A -> non empty ;
coherence
not Left_Cosets A is empty by GROUP_2:135;
end;
notation
let G be Group;
let H be Subgroup of G;
synonym index (G,H) for index H;
end;
theorem Th19: :: GROUP_8:19
for G being Group
for A, B being Subgroup of G
for D being Subgroup of A st D = A /\ B & G is finite holds
index (G,B) >= index (A,D)
proof
let G be Group; ::_thesis: for A, B being Subgroup of G
for D being Subgroup of A st D = A /\ B & G is finite holds
index (G,B) >= index (A,D)
let A, B be Subgroup of G; ::_thesis: for D being Subgroup of A st D = A /\ B & G is finite holds
index (G,B) >= index (A,D)
let D be Subgroup of A; ::_thesis: ( D = A /\ B & G is finite implies index (G,B) >= index (A,D) )
assume that
A1: D = A /\ B and
A2: G is finite ; ::_thesis: index (G,B) >= index (A,D)
reconsider LCB = Left_Cosets B as non empty finite set by A2;
reconsider LCD = Left_Cosets D as non empty finite set by A2;
A3: now__::_thesis:_for_x,_y_being_Element_of_G
for_x9,_y9_being_Element_of_A_st_x9_=_x_&_y9_=_y_holds_
(_x_*_B_=_y_*_B_iff_x9_*_D_=_y9_*_D_)
let x, y be Element of G; ::_thesis: for x9, y9 being Element of A st x9 = x & y9 = y holds
( x * B = y * B iff x9 * D = y9 * D )
let x9, y9 be Element of A; ::_thesis: ( x9 = x & y9 = y implies ( x * B = y * B iff x9 * D = y9 * D ) )
assume that
A4: x9 = x and
A5: y9 = y ; ::_thesis: ( x * B = y * B iff x9 * D = y9 * D )
A6: y9 " = y " by A5, GROUP_2:48;
A7: (y9 ") * x9 in A by STRUCT_0:def_5;
( x * B = y * B iff (y ") * x in B ) by GROUP_2:114;
then ( x * B = y * B iff (y9 ") * x9 in B ) by A4, A6, GROUP_2:43;
then ( x * B = y * B iff (y9 ") * x9 in D ) by A1, A7, GROUP_2:82;
hence ( x * B = y * B iff x9 * D = y9 * D ) by GROUP_2:114; ::_thesis: verum
end;
defpred S1[ set , set ] means ex a being Element of G ex a9 being Element of A st
( a = a9 & $2 = a * B & $1 = a9 * D );
A8: for x being Element of LCD ex y being Element of LCB st S1[x,y]
proof
let x be Element of LCD; ::_thesis: ex y being Element of LCB st S1[x,y]
x in LCD ;
then consider a9 being Element of A such that
A9: x = a9 * D by GROUP_2:def_15;
reconsider a = a9 as Element of G by GROUP_2:42;
reconsider y = a * B as Element of LCB by GROUP_2:def_15;
take y ; ::_thesis: S1[x,y]
take a ; ::_thesis: ex a9 being Element of A st
( a = a9 & y = a * B & x = a9 * D )
take a9 ; ::_thesis: ( a = a9 & y = a * B & x = a9 * D )
thus ( a = a9 & y = a * B & x = a9 * D ) by A9; ::_thesis: verum
end;
consider F being Function of LCD,LCB such that
A10: for a being Element of LCD holds S1[a,F . a] from FUNCT_2:sch_3(A8);
A11: dom F = LCD by FUNCT_2:def_1;
A12: rng F c= LCB by RELAT_1:def_19;
A13: index D = card LCD by GROUP_2:def_18;
A14: index B = card LCB by GROUP_2:def_18;
F is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom F or not x2 in dom F or not F . x1 = F . x2 or x1 = x2 )
assume that
A15: x1 in dom F and
A16: x2 in dom F ; ::_thesis: ( not F . x1 = F . x2 or x1 = x2 )
reconsider z1 = x1, z2 = x2 as Element of LCD by A15, A16, FUNCT_2:def_1;
A17: ex a being Element of G ex a9 being Element of A st
( a = a9 & F . z1 = a * B & z1 = a9 * D ) by A10;
ex b being Element of G ex b9 being Element of A st
( b = b9 & F . z2 = b * B & z2 = b9 * D ) by A10;
hence ( not F . x1 = F . x2 or x1 = x2 ) by A3, A17; ::_thesis: verum
end;
then index D c= index B by A11, A12, A13, A14, CARD_1:10;
hence index (G,B) >= index (A,D) by NAT_1:39; ::_thesis: verum
end;
theorem Th20: :: GROUP_8:20
for G being finite Group
for H being Subgroup of G holds index (G,H) > 0
proof
let G be finite Group; ::_thesis: for H being Subgroup of G holds index (G,H) > 0
let H be Subgroup of G; ::_thesis: index (G,H) > 0
card G = (card H) * (index H) by GROUP_2:147;
hence index (G,H) > 0 ; ::_thesis: verum
end;
theorem :: GROUP_8:21
for G being Group st G is finite holds
for C being Subgroup of G
for A, B being Subgroup of C
for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
proof
let G be Group; ::_thesis: ( G is finite implies for C being Subgroup of G
for A, B being Subgroup of C
for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A1: G is finite ; ::_thesis: for C being Subgroup of G
for A, B being Subgroup of C
for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
let C be Subgroup of G; ::_thesis: for A, B being Subgroup of C
for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
let A, B be Subgroup of C; ::_thesis: for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
let D be Subgroup of A; ::_thesis: ( D = A /\ B implies for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A2: D = A /\ B ; ::_thesis: for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
let E be Subgroup of B; ::_thesis: ( E = A /\ B implies for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A3: E = A /\ B ; ::_thesis: for F being Subgroup of C st F = A /\ B & index (C,A), index (C,B) are_relative_prime holds
( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
let F be Subgroup of C; ::_thesis: ( F = A /\ B & index (C,A), index (C,B) are_relative_prime implies ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A4: F = A /\ B ; ::_thesis: ( not index (C,A), index (C,B) are_relative_prime or ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) )
assume A5: index A, index B are_relative_prime ; ::_thesis: ( index (C,B) = index (A,D) & index (C,A) = index (B,E) )
index F = (index E) * (index B) by A1, A3, A4, GROUP_2:149;
then A6: (index E) * (index B) = (index D) * (index A) by A1, A2, A4, GROUP_2:149;
then index B divides (index A) * (index D) by INT_1:def_3;
then A7: index B divides index D by A5, INT_2:25;
ex n being Element of NAT st index D = (index B) * n
proof
consider i being Integer such that
A8: index D = (index B) * i by A7, INT_1:def_3;
0 <= i by A1, A8, Th20;
then reconsider i = i as Element of NAT by INT_1:3;
take i ; ::_thesis: index D = (index B) * i
thus index D = (index B) * i by A8; ::_thesis: verum
end;
then A9: index B divides index D by NAT_D:def_3;
A10: index (C,B) >= index (A,D) by A1, A2, Th19;
A11: index B = index D
proof
assume A12: index B <> index D ; ::_thesis: contradiction
index D > 0 by A1, Th20;
then index B <= index D by A9, NAT_D:7;
hence contradiction by A10, A12, XXREAL_0:1; ::_thesis: verum
end;
index A divides (index B) * (index E) by A6, INT_1:def_3;
then A13: index A divides index E by A5, INT_2:25;
ex n being Element of NAT st index E = (index A) * n
proof
consider i being Integer such that
A14: index E = (index A) * i by A13, INT_1:def_3;
0 <= i by A1, A14, Th20;
then reconsider i = i as Element of NAT by INT_1:3;
take i ; ::_thesis: index E = (index A) * i
thus index E = (index A) * i by A14; ::_thesis: verum
end;
then A15: index A divides index E by NAT_D:def_3;
A16: index A >= index E by A1, A3, Th19;
index A = index E
proof
assume A17: index A <> index E ; ::_thesis: contradiction
index E > 0 by A1, Th20;
then index A <= index E by A15, NAT_D:7;
hence contradiction by A16, A17, XXREAL_0:1; ::_thesis: verum
end;
hence ( index (C,B) = index (A,D) & index (C,A) = index (B,E) ) by A11; ::_thesis: verum
end;
theorem Th22: :: GROUP_8:22
for G being Group
for H being Subgroup of G
for a being Element of G st a in H holds
for j being Integer holds a |^ j in H
proof
let G be Group; ::_thesis: for H being Subgroup of G
for a being Element of G st a in H holds
for j being Integer holds a |^ j in H
let H be Subgroup of G; ::_thesis: for a being Element of G st a in H holds
for j being Integer holds a |^ j in H
let a be Element of G; ::_thesis: ( a in H implies for j being Integer holds a |^ j in H )
assume A1: a in H ; ::_thesis: for j being Integer holds a |^ j in H
let j be Integer; ::_thesis: a |^ j in H
consider k being Element of NAT such that
A2: ( j = k or j = - k ) by INT_1:2;
percases ( j = k or j = - k ) by A2;
supposeA3: j = k ; ::_thesis: a |^ j in H
defpred S1[ Element of NAT ] means a |^ $1 in H;
a |^ 0 = 1_ G by GROUP_1:25;
then A4: S1[ 0 ] by GROUP_2:46;
A5: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then (a |^ n) * a in H by A1, GROUP_2:50;
hence S1[n + 1] by GROUP_1:34; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A5);
hence a |^ j in H by A3; ::_thesis: verum
end;
supposeA6: j = - k ; ::_thesis: a |^ j in H
defpred S1[ Element of NAT ] means a |^ (- $1) in H;
a |^ 0 = 1_ G by GROUP_1:25;
then A7: S1[ 0 ] by GROUP_2:46;
A8: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A9: S1[n] ; ::_thesis: S1[n + 1]
a " in H by A1, GROUP_2:51;
then (a |^ (- n)) * (a ") in H by A9, GROUP_2:50;
then (a |^ (- n)) * (a |^ (- 1)) in H by GROUP_1:32;
then a |^ ((- n) + (- 1)) in H by GROUP_1:33;
hence S1[n + 1] ; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A8);
hence a |^ j in H by A6; ::_thesis: verum
end;
end;
end;
theorem Th23: :: GROUP_8:23
for G being strict Group st G <> (1). G holds
ex b being Element of G st b <> 1_ G
proof
let G be strict Group; ::_thesis: ( G <> (1). G implies ex b being Element of G st b <> 1_ G )
assume A1: G <> (1). G ; ::_thesis: ex b being Element of G st b <> 1_ G
assume A2: for b being Element of G holds not b <> 1_ G ; ::_thesis: contradiction
for x, y being Element of G holds x = y
proof
let x, y be Element of G; ::_thesis: x = y
x = 1_ G by A2;
hence x = y by A2; ::_thesis: verum
end;
then G is trivial by STRUCT_0:def_10;
hence contradiction by A1, GROUP_6:12; ::_thesis: verum
end;
theorem Th24: :: GROUP_8:24
for G being strict Group
for a being Element of G st G = gr {a} holds
for H being strict Subgroup of G st H <> (1). G holds
ex k being Element of NAT st
( 0 < k & a |^ k in H )
proof
let G be strict Group; ::_thesis: for a being Element of G st G = gr {a} holds
for H being strict Subgroup of G st H <> (1). G holds
ex k being Element of NAT st
( 0 < k & a |^ k in H )
let a be Element of G; ::_thesis: ( G = gr {a} implies for H being strict Subgroup of G st H <> (1). G holds
ex k being Element of NAT st
( 0 < k & a |^ k in H ) )
assume A1: G = gr {a} ; ::_thesis: for H being strict Subgroup of G st H <> (1). G holds
ex k being Element of NAT st
( 0 < k & a |^ k in H )
let H be strict Subgroup of G; ::_thesis: ( H <> (1). G implies ex k being Element of NAT st
( 0 < k & a |^ k in H ) )
assume H <> (1). G ; ::_thesis: ex k being Element of NAT st
( 0 < k & a |^ k in H )
then A2: H <> (1). H by GROUP_2:63;
consider c being Element of H such that
A3: c <> 1_ H by A2, Th23;
A4: c in H by STRUCT_0:def_5;
then c in G by GROUP_2:40;
then reconsider c = c as Element of G by STRUCT_0:def_5;
A5: c in gr {a} by A1, STRUCT_0:def_5;
ex j being Integer st
( c = a |^ j & j <> 0 )
proof
assume A6: for j being Integer holds
( not c = a |^ j or not j <> 0 ) ; ::_thesis: contradiction
consider i being Integer such that
A7: c = a |^ i by A5, GR_CY_1:5;
A8: a |^ i <> 1_ G by A3, A7, GROUP_2:44;
i = 0 by A6, A7;
hence contradiction by A8, GROUP_1:25; ::_thesis: verum
end;
then consider j being Integer such that
A9: c = a |^ j and
A10: j <> 0 ;
consider n being Element of NAT such that
A11: ( j = n or j = - n ) by INT_1:2;
percases ( j = n or j = - n ) by A11;
suppose j = n ; ::_thesis: ex k being Element of NAT st
( 0 < k & a |^ k in H )
hence ex k being Element of NAT st
( 0 < k & a |^ k in H ) by A4, A9, A10; ::_thesis: verum
end;
supposeA12: j = - n ; ::_thesis: ex k being Element of NAT st
( 0 < k & a |^ k in H )
then A13: 0 < n by A10;
(a |^ n) " in H by A4, A9, A12, GROUP_1:36;
then ((a |^ n) ") " in H by GROUP_2:51;
hence ex k being Element of NAT st
( 0 < k & a |^ k in H ) by A13; ::_thesis: verum
end;
end;
end;
theorem :: GROUP_8:25
for G being strict cyclic Group
for H being strict Subgroup of G holds H is cyclic Group
proof
let G be strict cyclic Group; ::_thesis: for H being strict Subgroup of G holds H is cyclic Group
let H be strict Subgroup of G; ::_thesis: H is cyclic Group
percases ( H = (1). G or H <> (1). G ) ;
suppose H = (1). G ; ::_thesis: H is cyclic Group
hence H is cyclic Group ; ::_thesis: verum
end;
supposeA1: H <> (1). G ; ::_thesis: H is cyclic Group
consider b being Element of G such that
A2: multMagma(# the carrier of G, the multF of G #) = gr {b} by GR_CY_1:def_7;
ex m being Nat st
( 0 < m & b |^ m in H & ( for j being Nat st 0 < j & b |^ j in H holds
m <= j ) )
proof
defpred S1[ Nat] means ( 0 < $1 & b |^ $1 in H );
ex k being Element of NAT st S1[k] by A1, A2, Th24;
then A3: ex k being Nat st S1[k] ;
ex m being Nat st
( S1[m] & ( for j being Nat st S1[j] holds
m <= j ) ) from NAT_1:sch_5(A3);
hence ex m being Nat st
( 0 < m & b |^ m in H & ( for j being Nat st 0 < j & b |^ j in H holds
m <= j ) ) ; ::_thesis: verum
end;
then consider m being Nat such that
A4: 0 < m and
A5: b |^ m in H and
A6: for j being Nat st 0 < j & b |^ j in H holds
m <= j ;
set c = b |^ m;
reconsider c = b |^ m as Element of H by A5, STRUCT_0:def_5;
for a being Element of H ex i being Integer st a = c |^ i
proof
let a be Element of H; ::_thesis: ex i being Integer st a = c |^ i
ex t being Integer st
( b |^ t in H & b |^ t = a )
proof
A7: a in G by GROUP_2:41;
A8: a in gr {b} by A2, GROUP_2:41;
a is Element of G by A7, STRUCT_0:def_5;
then consider j1 being Integer such that
A9: a = b |^ j1 by A8, GR_CY_1:5;
b |^ j1 in H by A9, STRUCT_0:def_5;
hence ex t being Integer st
( b |^ t in H & b |^ t = a ) by A9; ::_thesis: verum
end;
then consider t being Integer such that
A10: b |^ t in H and
A11: b |^ t = a ;
ex r, s being Integer st
( 0 <= s & s < m & t = (m * r) + s )
proof
take t div m ; ::_thesis: ex s being Integer st
( 0 <= s & s < m & t = (m * (t div m)) + s )
take t mod m ; ::_thesis: ( 0 <= t mod m & t mod m < m & t = (m * (t div m)) + (t mod m) )
thus ( 0 <= t mod m & t mod m < m & t = (m * (t div m)) + (t mod m) ) by A4, NEWTON:64, NEWTON:65, NEWTON:66; ::_thesis: verum
end;
then consider r, s being Integer such that
A12: 0 <= s and
A13: s < m and
A14: t = (m * r) + s ;
reconsider s = s as Element of NAT by A12, INT_1:3;
A15: b |^ t = (b |^ (m * r)) * (b |^ s) by A14, GROUP_1:33
.= ((b |^ m) |^ r) * (b |^ s) by GROUP_1:35 ;
A16: (b |^ m) |^ r in H by A5, Th22;
b |^ s in H
proof
set u = b |^ t;
set v = (b |^ m) |^ r;
A17: (((b |^ m) |^ r) ") * (b |^ t) = ((((b |^ m) |^ r) ") * ((b |^ m) |^ r)) * (b |^ s) by A15, GROUP_1:def_3
.= (1_ G) * (b |^ s) by GROUP_1:def_5
.= b |^ s by GROUP_1:def_4 ;
((b |^ m) |^ r) " in H by A16, GROUP_2:51;
hence b |^ s in H by A10, A17, GROUP_2:50; ::_thesis: verum
end;
then s = 0 by A6, A13;
then b |^ s = 1_ G by GROUP_1:25;
then A18: b |^ t = (b |^ m) |^ r by A15, GROUP_1:def_4;
(b |^ m) |^ r = c |^ r by GROUP_4:2;
hence ex i being Integer st a = c |^ i by A11, A18; ::_thesis: verum
end;
then H = gr {c} by GR_CY_2:5;
hence H is cyclic Group by GR_CY_2:4; ::_thesis: verum
end;
end;
end;