group_4.miz
begin
definition
let D be non
empty
set;
let F be
FinSequence of D;
let X be
set;
:: original:
-
redefine
func F
- X ->
FinSequence of D ;
coherence by
FINSEQ_3: 86;
end
scheme ::
GROUP_4:sch1
MeetSbgEx { G() ->
Group , P[
set] } :
ex H be
strict
Subgroup of G() st the
carrier of H
= (
meet { A where A be
Subset of G() : ex K be
strict
Subgroup of G() st A
= the
carrier of K & P[K] })
provided
A1: ex H be
strict
Subgroup of G() st P[H];
set X = { A where A be
Subset of G() : ex K be
strict
Subgroup of G() st A
= the
carrier of K & P[K] };
consider T be
strict
Subgroup of G() such that
A2: P[T] by
A1;
A3: (
carr T)
in X by
A2;
then
reconsider Y = (
meet X) as
Subset of G() by
SETFAM_1: 7;
A4:
now
let a be
Element of G();
assume
A5: a
in Y;
now
let Z be
set;
assume
A6: Z
in X;
then
consider A be
Subset of G() such that
A7: A
= Z and
A8: ex H be
strict
Subgroup of G() st A
= the
carrier of H & P[H];
consider H be
Subgroup of G() such that
A9: A
= the
carrier of H and P[H] by
A8;
a
in the
carrier of H by
A5,
A6,
A7,
A9,
SETFAM_1:def 1;
then a
in H by
STRUCT_0:def 5;
then (a
" )
in H by
GROUP_2: 51;
hence (a
" )
in Z by
A7,
A9,
STRUCT_0:def 5;
end;
hence (a
" )
in Y by
A3,
SETFAM_1:def 1;
end;
A10:
now
let a,b be
Element of G();
assume that
A11: a
in Y and
A12: b
in Y;
now
let Z be
set;
assume
A13: Z
in X;
then
consider A be
Subset of G() such that
A14: A
= Z and
A15: ex H be
strict
Subgroup of G() st A
= the
carrier of H & P[H];
consider H be
Subgroup of G() such that
A16: A
= the
carrier of H and P[H] by
A15;
b
in the
carrier of H by
A12,
A13,
A14,
A16,
SETFAM_1:def 1;
then
A17: b
in H by
STRUCT_0:def 5;
a
in the
carrier of H by
A11,
A13,
A14,
A16,
SETFAM_1:def 1;
then a
in H by
STRUCT_0:def 5;
then (a
* b)
in H by
A17,
GROUP_2: 50;
hence (a
* b)
in Z by
A14,
A16,
STRUCT_0:def 5;
end;
hence (a
* b)
in Y by
A3,
SETFAM_1:def 1;
end;
now
let Z be
set;
assume Z
in X;
then
consider A be
Subset of G() such that
A18: Z
= A and
A19: ex K be
strict
Subgroup of G() st A
= the
carrier of K & P[K];
consider H be
Subgroup of G() such that
A20: A
= the
carrier of H and P[H] by
A19;
(
1_ G())
in H by
GROUP_2: 46;
hence (
1_ G())
in Z by
A18,
A20,
STRUCT_0:def 5;
end;
then Y
<>
{} by
A3,
SETFAM_1:def 1;
hence thesis by
A10,
A4,
GROUP_2: 52;
end;
reserve x,y,X,Y for
set,
k,l,n for
Nat,
i,i1,i2,i3,j for
Integer,
G for
Group,
a,b,c,d for
Element of G,
A,B,C for
Subset of G,
H,H1,H2,H3 for
Subgroup of G,
h for
Element of H,
F,F1,F2 for
FinSequence of the
carrier of G,
I,I1,I2 for
FinSequence of
INT ;
scheme ::
GROUP_4:sch2
SubgrSep { G() ->
Group , P[
set] } :
ex X st X
c= (
Subgroups G()) & for H be
strict
Subgroup of G() holds H
in X iff P[H];
defpred
R[
object] means ex H be
Subgroup of G() st $1
= H & P[H];
consider X such that
A1: for x be
object holds x
in X iff x
in (
Subgroups G()) &
R[x] from
XBOOLE_0:sch 1;
take X;
thus X
c= (
Subgroups G()) by
A1;
let H be
strict
Subgroup of G();
thus H
in X implies P[H]
proof
assume H
in X;
then ex H1 be
Subgroup of G() st H
= H1 & P[H1] by
A1;
hence thesis;
end;
A2: H
in (
Subgroups G()) by
GROUP_3:def 1;
assume P[H];
hence thesis by
A1,
A2;
end;
definition
let i;
::
GROUP_4:def1
func
@ i ->
Element of
INT equals i;
coherence by
INT_1:def 2;
end
theorem ::
GROUP_4:1
Th1: a
= h implies (a
|^ n)
= (h
|^ n)
proof
defpred
P[
Nat] means (a
|^ $1)
= (h
|^ $1);
assume
A1: a
= h;
A2:
now
let n;
assume
A3:
P[n];
(a
|^ (n
+ 1))
= ((a
|^ n)
* a) by
GROUP_1: 34
.= ((h
|^ n)
* h) by
A1,
A3,
GROUP_2: 43
.= (h
|^ (n
+ 1)) by
GROUP_1: 34;
hence
P[(n
+ 1)];
end;
(a
|^
0 )
= (
1_ G) by
GROUP_1: 25
.= (
1_ H) by
GROUP_2: 44
.= (h
|^
0 ) by
GROUP_1: 25;
then
A4:
P[
0 ];
for n holds
P[n] from
NAT_1:sch 2(
A4,
A2);
hence thesis;
end;
theorem ::
GROUP_4:2
a
= h implies (a
|^ i)
= (h
|^ i)
proof
assume
A1: a
= h;
now
per cases ;
suppose
A2: i
>=
0 ;
hence (a
|^ i)
= (a
|^
|.i.|) by
ABSVALUE:def 1
.= (h
|^
|.i.|) by
A1,
Th1
.= (h
|^ i) by
A2,
ABSVALUE:def 1;
end;
suppose
A3: i
<
0 ;
A4: (a
|^
|.i.|)
= (h
|^
|.i.|) by
A1,
Th1;
thus (a
|^ i)
= ((a
|^
|.i.|)
" ) by
A3,
GROUP_1: 30
.= ((h
|^
|.i.|)
" ) by
A4,
GROUP_2: 48
.= (h
|^ i) by
A3,
GROUP_1: 30;
end;
end;
hence thesis;
end;
theorem ::
GROUP_4:3
Th3: a
in H implies (a
|^ n)
in H
proof
defpred
P[
Nat] means (a
|^ $1)
in H;
assume
A1: a
in H;
A2:
now
let n;
A3: (a
|^ (n
+ 1))
= ((a
|^ n)
* a) by
GROUP_1: 34;
assume
P[n];
hence
P[(n
+ 1)] by
A1,
A3,
GROUP_2: 50;
end;
(a
|^
0 )
= (
1_ G) by
GROUP_1: 25;
then
A4:
P[
0 ] by
GROUP_2: 46;
for n holds
P[n] from
NAT_1:sch 2(
A4,
A2);
hence thesis;
end;
theorem ::
GROUP_4:4
Th4: a
in H implies (a
|^ i)
in H
proof
assume
A1: a
in H;
now
per cases ;
suppose i
>=
0 ;
then (a
|^ i)
= (a
|^
|.i.|) by
ABSVALUE:def 1;
hence thesis by
A1,
Th3;
end;
suppose i
<
0 ;
then
A2: (a
|^ i)
= ((a
|^
|.i.|)
" ) by
GROUP_1: 30;
(a
|^
|.i.|)
in H by
A1,
Th3;
hence thesis by
A2,
GROUP_2: 51;
end;
end;
hence thesis;
end;
definition
let G be non
empty
multMagma;
let F be
FinSequence of the
carrier of G;
::
GROUP_4:def2
func
Product F ->
Element of G equals (the
multF of G
"**" F);
correctness ;
end
theorem ::
GROUP_4:5
for G be
associative
unital non
empty
multMagma, F1,F2 be
FinSequence of the
carrier of G holds (
Product (F1
^ F2))
= ((
Product F1)
* (
Product F2)) by
FINSOP_1: 5;
theorem ::
GROUP_4:6
for G be
unital non
empty
multMagma, F be
FinSequence of the
carrier of G, a be
Element of G holds (
Product (F
^
<*a*>))
= ((
Product F)
* a) by
FINSOP_1: 4;
theorem ::
GROUP_4:7
for G be
associative
unital non
empty
multMagma, F be
FinSequence of the
carrier of G, a be
Element of G holds (
Product (
<*a*>
^ F))
= (a
* (
Product F)) by
FINSOP_1: 6;
theorem ::
GROUP_4:8
Th8: for G be
unital non
empty
multMagma holds (
Product (
<*> the
carrier of G))
= (
1_ G)
proof
let G be
unital non
empty
multMagma;
set g = the
multF of G;
(
len (
<*> the
carrier of G))
=
0 & g is
having_a_unity;
hence (
Product (
<*> the
carrier of G))
= (
the_unity_wrt g) by
FINSOP_1:def 1
.= (
1_ G) by
GROUP_1: 22;
end;
theorem ::
GROUP_4:9
for G be non
empty
multMagma, a be
Element of G holds (
Product
<*a*>)
= a by
FINSOP_1: 11;
theorem ::
GROUP_4:10
for G be non
empty
multMagma, a,b be
Element of G holds (
Product
<*a, b*>)
= (a
* b) by
FINSOP_1: 12;
theorem ::
GROUP_4:11
(
Product
<*a, b, c*>)
= ((a
* b)
* c) & (
Product
<*a, b, c*>)
= (a
* (b
* c))
proof
A1: (
Product
<*a*>)
= a & (
Product
<*c*>)
= c by
FINSOP_1: 11;
A2: (
Product
<*a, b*>)
= (a
* b) & (
Product
<*b, c*>)
= (b
* c) by
FINSOP_1: 12;
<*a, b, c*>
= (
<*a*>
^
<*b, c*>) &
<*a, b, c*>
= (
<*a, b*>
^
<*c*>) by
FINSEQ_1: 43;
hence thesis by
A1,
A2,
FINSOP_1: 5;
end;
Lm1:
now
let G, a;
thus (
Product (
0
|-> a))
= (
Product (
<*> the
carrier of G))
.= (
1_ G) by
Th8
.= (a
|^
0 ) by
GROUP_1: 25;
end;
Lm2:
now
let G, a;
let n;
assume
A1: (
Product (n
|-> a))
= (a
|^ n);
thus (
Product ((n
+ 1)
|-> a))
= (
Product ((n
|-> a)
^
<*a*>)) by
FINSEQ_2: 60
.= ((
Product (n
|-> a))
* (
Product
<*a*>)) by
FINSOP_1: 5
.= ((a
|^ n)
* a) by
A1,
FINSOP_1: 11
.= (a
|^ (n
+ 1)) by
GROUP_1: 34;
end;
theorem ::
GROUP_4:12
(
Product (n
|-> a))
= (a
|^ n)
proof
defpred
P[
Nat] means (
Product ($1
|-> a))
= (a
|^ $1);
A1: for n be
Nat st
P[n] holds
P[(n
+ 1)] by
Lm2;
A2:
P[
0 ] by
Lm1;
for n be
Nat holds
P[n] from
NAT_1:sch 2(
A2,
A1);
hence thesis;
end;
theorem ::
GROUP_4:13
(
Product (F
-
{(
1_ G)}))
= (
Product F)
proof
defpred
P[
FinSequence of the
carrier of G] means (
Product ($1
-
{(
1_ G)}))
= (
Product $1);
A1: for F, a st
P[F] holds
P[(F
^
<*a*>)]
proof
let F, a;
assume
A2:
P[F];
A3: (
Product ((F
^
<*a*>)
-
{(
1_ G)}))
= (
Product ((F
-
{(
1_ G)})
^ (
<*a*>
-
{(
1_ G)}))) by
FINSEQ_3: 73
.= ((
Product F)
* (
Product (
<*a*>
-
{(
1_ G)}))) by
A2,
FINSOP_1: 5;
now
per cases ;
suppose
A4: a
= (
1_ G);
then a
in
{(
1_ G)} by
TARSKI:def 1;
then (
<*a*>
-
{(
1_ G)})
= (
<*> the
carrier of G) by
FINSEQ_3: 76;
then (
Product (
<*a*>
-
{(
1_ G)}))
= (
1_ G) by
Th8;
hence thesis by
A3,
A4,
FINSOP_1: 4;
end;
suppose a
<> (
1_ G);
then not a
in
{(
1_ G)} by
TARSKI:def 1;
then (
<*a*>
-
{(
1_ G)})
=
<*a*> by
FINSEQ_3: 75;
hence thesis by
A3,
FINSOP_1: 5;
end;
end;
hence thesis;
end;
A5:
P[(
<*> the
carrier of G)] by
FINSEQ_3: 74;
for F holds
P[F] from
FINSEQ_2:sch 2(
A5,
A1);
hence thesis;
end;
Lm3: for F1 be
FinSequence, y be
Element of
NAT st y
in (
dom F1) holds (((
len F1)
- y)
+ 1) is
Element of
NAT & (((
len F1)
- y)
+ 1)
>= 1 & (((
len F1)
- y)
+ 1)
<= (
len F1)
proof
let F1 be
FinSequence, y be
Element of
NAT ;
assume
A1: y
in (
dom F1);
now
assume (((
len F1)
- y)
+ 1)
<
0 ;
then 1
< (
0 qua
Nat
- ((
len F1)
- y)) by
XREAL_1: 20;
then 1
< (y
- (
len F1));
then
A2: ((
len F1)
+ 1)
< y by
XREAL_1: 20;
y
<= (
len F1) by
A1,
FINSEQ_3: 25;
hence contradiction by
A2,
NAT_1: 12;
end;
then
reconsider n = (((
len F1)
- y)
+ 1) as
Element of
NAT by
INT_1: 3;
y
>= 1 by
A1,
FINSEQ_3: 25;
then ((n
- 1)
- y)
<= (((
len F1)
- y)
- 1) by
XREAL_1: 13;
then
A3: (n
- (y
+ 1))
<= ((
len F1)
- (y
+ 1));
(y
+
0 )
<= (
len F1) by
A1,
FINSEQ_3: 25;
then (
0
+ 1)
= 1 &
0
<= ((
len F1)
- y) by
XREAL_1: 19;
hence thesis by
A3,
XREAL_1: 6,
XREAL_1: 9;
end;
theorem ::
GROUP_4:14
Th14: (
len F1)
= (
len F2) & (for k st k
in (
dom F1) holds (F2
. (((
len F1)
- k)
+ 1))
= ((F1
/. k)
" )) implies (
Product F1)
= ((
Product F2)
" )
proof
defpred
P[
Nat] means for F1, F2 st (
len F1)
= $1 & (
len F1)
= (
len F2) & (for k st k
in (
dom F1) holds (F2
. (((
len F1)
- k)
+ 1))
= ((F1
/. k)
" )) holds (
Product F1)
= ((
Product F2)
" );
A1: for n st
P[n] holds
P[(n
+ 1)]
proof
let n;
assume
A2:
P[n];
let F1, F2;
assume that
A3: (
len F1)
= (n
+ 1) and
A4: (
len F1)
= (
len F2) and
A5: for k st k
in (
dom F1) holds (F2
. (((
len F1)
- k)
+ 1))
= ((F1
/. k)
" );
reconsider p = (F1
| (
Seg n)) as
FinSequence of the
carrier of G by
FINSEQ_1: 18;
deffunc
F(
Nat) = (F2
. ($1
+ 1));
consider q be
FinSequence such that
A6: (
len q)
= (
len p) and
A7: for k be
Nat st k
in (
dom q) holds (q
. k)
=
F(k) from
FINSEQ_1:sch 2;
A8: (
dom q)
= (
dom p) by
A6,
FINSEQ_3: 29;
A9: (
len p)
= n by
A3,
FINSEQ_3: 53;
A10: (
rng q)
c= the
carrier of G
proof
let x be
object;
assume x
in (
rng q);
then
consider y be
object such that
A11: y
in (
dom q) and
A12: x
= (q
. y) by
FUNCT_1:def 3;
reconsider y as
Element of
NAT by
A11;
y
<= (
len p) by
A6,
A11,
FINSEQ_3: 25;
then 1
<= (y
+ 1) & (y
+ 1)
<= (
len F2) by
A3,
A4,
A9,
NAT_1: 12,
XREAL_1: 7;
then
A13: (y
+ 1)
in (
dom F2) by
FINSEQ_3: 25;
x
= (F2
. (y
+ 1)) by
A7,
A11,
A12;
then
A14: x
in (
rng F2) by
A13,
FUNCT_1:def 3;
(
rng F2)
c= the
carrier of G by
FINSEQ_1:def 4;
hence thesis by
A14;
end;
A15: (
rng F1)
c= the
carrier of G by
FINSEQ_1:def 4;
1
<= (n
+ 1) by
NAT_1: 12;
then (n
+ 1)
in (
dom F1) by
A3,
FINSEQ_3: 25;
then (F1
. (n
+ 1))
in (
rng F1) by
FUNCT_1:def 3;
then
reconsider a = (F1
. (n
+ 1)) as
Element of G by
A15;
A16: F1
= (p
^
<*a*>) by
A3,
FINSEQ_3: 55;
A17:
now
let k;
assume k
in (
dom
<*(a
" )*>);
then
A18: k
in
{1} by
FINSEQ_1: 2,
FINSEQ_1:def 8;
(
len F2)
>= 1 by
A3,
A4,
NAT_1: 12;
then
A19: (
len F2)
in (
dom F1) by
A4,
FINSEQ_3: 25;
then (F2
. (((
len F1)
- (
len F1))
+ 1))
= ((F1
/. (
len F1))
" ) by
A4,
A5;
then ((F1
/. (
len F1))
" )
= (F2
. k) by
A18,
TARSKI:def 1;
then
A20: (F2
. k)
= (a
" ) by
A3,
A4,
A19,
PARTFUN1:def 6;
k
= 1 by
A18,
TARSKI:def 1;
hence (
<*(a
" )*>
. k)
= (F2
. k) by
A20,
FINSEQ_1:def 8;
end;
reconsider q as
FinSequence of the
carrier of G by
A10,
FINSEQ_1:def 4;
now
let k;
assume
A21: k
in (
dom p);
then
reconsider i = (((
len p)
- k)
+ 1) as
Element of
NAT by
Lm3;
A22: (i
+ 1)
= (((
len F1)
- k)
+ 1) by
A3,
A9;
1
<= i & i
<= (
len p) by
A21,
Lm3;
then i
in (
dom p) by
FINSEQ_3: 25;
then
A23: (q
. i)
= (F2
. (i
+ 1)) by
A7,
A8;
k
<= (
len p) by
A21,
FINSEQ_3: 25;
then
A24: k
<= (
len F1) by
A3,
A9,
NAT_1: 12;
1
<= k by
A21,
FINSEQ_3: 25;
then
A25: k
in (
dom F1) by
A24,
FINSEQ_3: 25;
then (F1
/. k)
= (F1
. k) by
PARTFUN1:def 6
.= (p
. k) by
A21,
FUNCT_1: 47
.= (p
/. k) by
A21,
PARTFUN1:def 6;
hence (q
. (((
len p)
- k)
+ 1))
= ((p
/. k)
" ) by
A5,
A23,
A25,
A22;
end;
then
A26: (
Product p)
= ((
Product q)
" ) by
A2,
A9,
A6;
A27:
now
let k;
A28: (
len
<*(a
" )*>)
= 1 by
FINSEQ_1: 39;
assume k
in (
dom q);
hence (F2
. ((
len
<*(a
" )*>)
+ k))
= (q
. k) by
A7,
A28;
end;
(
len F2)
= ((
len
<*(a
" )*>)
+ (
len q)) by
A3,
A4,
A9,
A6,
FINSEQ_1: 39;
then F2
= (
<*(a
" )*>
^ q) by
A17,
A27,
FINSEQ_3: 38;
then (
Product F2)
= ((a
" )
* (
Product q)) by
FINSOP_1: 6
.= ((a
" )
* ((
Product p)
" )) by
A26
.= (((
Product p)
* a)
" ) by
GROUP_1: 17;
hence thesis by
A16,
FINSOP_1: 4;
end;
A29:
P[
0 ]
proof
let F1, F2;
assume that
A30: (
len F1)
=
0 and
A31: (
len F1)
= (
len F2);
F1
= (
<*> the
carrier of G) by
A30;
then
A32: (
Product F1)
= (
1_ G) by
Th8;
F2
= (
<*> the
carrier of G) by
A30,
A31;
then (
Product F2)
= (
1_ G) by
Th8;
hence thesis by
A32,
GROUP_1: 8;
end;
for k holds
P[k] from
NAT_1:sch 2(
A29,
A1);
hence thesis;
end;
theorem ::
GROUP_4:15
G is
commutative
Group implies for P be
Permutation of (
dom F1) st F2
= (F1
* P) holds (
Product F1)
= (
Product F2)
proof
set g = the
multF of G;
assume G is
commutative
Group;
then g is
commutative by
GROUP_3: 2;
hence thesis by
FINSOP_1: 7;
end;
theorem ::
GROUP_4:16
G is
commutative
Group & F1 is
one-to-one & F2 is
one-to-one & (
rng F1)
= (
rng F2) implies (
Product F1)
= (
Product F2)
proof
set g = the
multF of G;
assume G is
commutative
Group;
then g is
commutative by
GROUP_3: 2;
hence thesis by
FINSOP_1: 8;
end;
theorem ::
GROUP_4:17
G is
commutative
Group & (
len F)
= (
len F1) & (
len F)
= (
len F2) & (for k st k
in (
dom F) holds (F
. k)
= ((F1
/. k)
* (F2
/. k))) implies (
Product F)
= ((
Product F1)
* (
Product F2))
proof
set g = the
multF of G;
assume G is
commutative
Group;
then
A1: g is
commutative by
GROUP_3: 2;
assume that
A2: (
len F)
= (
len F1) and
A3: (
len F)
= (
len F2);
assume
A4: for k st k
in (
dom F) holds (F
. k)
= ((F1
/. k)
* (F2
/. k));
now
A5: (
dom F2)
= (
Seg (
len F2)) by
FINSEQ_1:def 3;
A6: (
dom F1)
= (
Seg (
len F1)) by
FINSEQ_1:def 3;
let k;
A7: (
dom F)
= (
Seg (
len F)) by
FINSEQ_1:def 3;
assume
A8: k
in (
dom F);
hence (F
. k)
= ((F1
/. k)
* (F2
/. k)) by
A4
.= (g
. ((F1
. k),(F2
/. k))) by
A2,
A8,
A7,
A6,
PARTFUN1:def 6
.= (g
. ((F1
. k),(F2
. k))) by
A3,
A8,
A7,
A5,
PARTFUN1:def 6;
end;
hence thesis by
A1,
A2,
A3,
FINSOP_1: 9;
end;
theorem ::
GROUP_4:18
Th18: (
rng F)
c= (
carr H) implies (
Product F)
in H
proof
defpred
P[
FinSequence of the
carrier of G] means (
rng $1)
c= (
carr H) implies (
Product $1)
in H;
A1:
now
let F, d;
assume
A2:
P[F];
thus
P[(F
^
<*d*>)]
proof
A3: (
rng F)
c= (
rng (F
^
<*d*>)) & (
Product (F
^
<*d*>))
= ((
Product F)
* d) by
FINSEQ_1: 29,
FINSOP_1: 4;
A4: (
rng
<*d*>)
=
{d} & d
in
{d} by
FINSEQ_1: 39,
TARSKI:def 1;
assume
A5: (
rng (F
^
<*d*>))
c= (
carr H);
(
rng
<*d*>)
c= (
rng (F
^
<*d*>)) by
FINSEQ_1: 30;
then (
rng
<*d*>)
c= (
carr H) by
A5;
then d
in H by
A4,
STRUCT_0:def 5;
hence thesis by
A2,
A5,
A3,
GROUP_2: 50,
XBOOLE_1: 1;
end;
end;
A6:
P[(
<*> the
carrier of G)]
proof
assume (
rng (
<*> the
carrier of G))
c= (
carr H);
(
1_ G)
in H by
GROUP_2: 46;
hence thesis by
Th8;
end;
for F holds
P[F] from
FINSEQ_2:sch 2(
A6,
A1);
hence thesis;
end;
definition
let G, I, F;
::
GROUP_4:def3
func F
|^ I ->
FinSequence of the
carrier of G means
:
Def3: (
len it )
= (
len F) & for k st k
in (
dom F) holds (it
. k)
= ((F
/. k)
|^ (
@ (I
/. k)));
existence
proof
deffunc
F(
Nat) = ((F
/. $1)
|^ (
@ (I
/. $1)));
consider p be
FinSequence such that
A1: (
len p)
= (
len F) and
A2: for k be
Nat st k
in (
dom p) holds (p
. k)
=
F(k) from
FINSEQ_1:sch 2;
A3: (
dom p)
= (
dom F) by
A1,
FINSEQ_3: 29;
(
rng p)
c= the
carrier of G
proof
let x be
object;
assume x
in (
rng p);
then
consider y be
object such that
A4: y
in (
dom p) and
A5: (p
. y)
= x by
FUNCT_1:def 3;
reconsider y as
Element of
NAT by
A4;
x
= ((F
/. y)
|^ (
@ (I
/. y))) by
A2,
A4,
A5;
hence thesis;
end;
then
reconsider p as
FinSequence of the
carrier of G by
FINSEQ_1:def 4;
take p;
thus thesis by
A1,
A2,
A3;
end;
uniqueness
proof
let F1, F2;
assume that
A6: (
len F1)
= (
len F) and
A7: for k st k
in (
dom F) holds (F1
. k)
= ((F
/. k)
|^ (
@ (I
/. k)));
assume that
A8: (
len F2)
= (
len F) and
A9: for k st k
in (
dom F) holds (F2
. k)
= ((F
/. k)
|^ (
@ (I
/. k)));
A10: (
dom F1)
= (
Seg (
len F)) by
A6,
FINSEQ_1:def 3;
now
let k be
Nat;
assume k
in (
dom F1);
then
A11: k
in (
dom F) by
A10,
FINSEQ_1:def 3;
hence (F1
. k)
= ((F
/. k)
|^ (
@ (I
/. k))) by
A7
.= (F2
. k) by
A9,
A11;
end;
hence thesis by
A6,
A8,
FINSEQ_2: 9;
end;
end
theorem ::
GROUP_4:19
Th19: (
len F1)
= (
len I1) & (
len F2)
= (
len I2) implies ((F1
^ F2)
|^ (I1
^ I2))
= ((F1
|^ I1)
^ (F2
|^ I2))
proof
assume that
A1: (
len F1)
= (
len I1) and
A2: (
len F2)
= (
len I2);
set r = (F2
|^ I2);
set q = (F1
|^ I1);
(
len (F1
^ F2))
= ((
len F1)
+ (
len F2)) by
FINSEQ_1: 22
.= (
len (I1
^ I2)) by
A1,
A2,
FINSEQ_1: 22;
then
A3: (
dom (F1
^ F2))
= (
dom (I1
^ I2)) by
FINSEQ_3: 29;
A4:
now
let k;
assume
A5: k
in (
dom (F1
^ F2));
now
per cases by
A5,
FINSEQ_1: 25;
suppose
A6: k
in (
dom F1);
(
len q)
= (
len F1) by
Def3;
then k
in (
dom q) by
A6,
FINSEQ_3: 29;
then
A7: ((q
^ r)
. k)
= (q
. k) by
FINSEQ_1:def 7
.= ((F1
/. k)
|^ (
@ (I1
/. k))) by
A6,
Def3;
A8: ((I1
^ I2)
. k)
= ((I1
^ I2)
/. k) by
A3,
A5,
PARTFUN1:def 6;
A9: (F1
/. k)
= (F1
. k) by
A6,
PARTFUN1:def 6
.= ((F1
^ F2)
. k) by
A6,
FINSEQ_1:def 7
.= ((F1
^ F2)
/. k) by
A5,
PARTFUN1:def 6;
A10: k
in (
dom I1) by
A1,
A6,
FINSEQ_3: 29;
then (I1
/. k)
= (I1
. k) by
PARTFUN1:def 6;
hence ((q
^ r)
. k)
= (((F1
^ F2)
/. k)
|^ (
@ ((I1
^ I2)
/. k))) by
A10,
A8,
A7,
A9,
FINSEQ_1:def 7;
end;
suppose ex n be
Nat st n
in (
dom F2) & k
= ((
len F1)
+ n);
then
consider n such that
A11: n
in (
dom F2) and
A12: k
= ((
len F1)
+ n);
A13: ((F1
^ F2)
. k)
= (F2
. n) & (F2
. n)
= (F2
/. n) by
A11,
A12,
FINSEQ_1:def 7,
PARTFUN1:def 6;
A14: (
len q)
= (
len F1) by
Def3;
(
len r)
= (
len F2) by
Def3;
then n
in (
dom r) by
A11,
FINSEQ_3: 29;
then
A15: ((q
^ r)
. k)
= (r
. n) by
A12,
A14,
FINSEQ_1:def 7;
A16: ((F1
^ F2)
. k)
= ((F1
^ F2)
/. k) & ((I1
^ I2)
/. k)
= ((I1
^ I2)
. k) by
A3,
A5,
PARTFUN1:def 6;
A17: n
in (
dom I2) by
A2,
A11,
FINSEQ_3: 29;
then
A18: (I2
/. n)
= (I2
. n) by
PARTFUN1:def 6;
((I1
^ I2)
. k)
= (I2
. n) by
A1,
A12,
A17,
FINSEQ_1:def 7;
hence ((q
^ r)
. k)
= (((F1
^ F2)
/. k)
|^ (
@ ((I1
^ I2)
/. k))) by
A11,
A15,
A13,
A16,
A18,
Def3;
end;
end;
hence ((q
^ r)
. k)
= (((F1
^ F2)
/. k)
|^ (
@ ((I1
^ I2)
/. k)));
end;
(
len (q
^ r))
= ((
len q)
+ (
len r)) by
FINSEQ_1: 22
.= ((
len F1)
+ (
len r)) by
Def3
.= ((
len F1)
+ (
len F2)) by
Def3
.= (
len (F1
^ F2)) by
FINSEQ_1: 22;
hence thesis by
A4,
Def3;
end;
theorem ::
GROUP_4:20
Th20: (
rng F)
c= (
carr H) implies (
Product (F
|^ I))
in H
proof
assume
A1: (
rng F)
c= (
carr H);
(
rng (F
|^ I))
c= (
carr H)
proof
let x be
object;
assume x
in (
rng (F
|^ I));
then
consider y be
object such that
A2: y
in (
dom (F
|^ I)) and
A3: x
= ((F
|^ I)
. y) by
FUNCT_1:def 3;
reconsider y as
Element of
NAT by
A2;
(
len (F
|^ I))
= (
len F) by
Def3;
then
A4: y
in (
dom F) by
A2,
FINSEQ_3: 29;
then (F
. y)
in (
rng F) & (F
. y)
= (F
/. y) by
FUNCT_1:def 3,
PARTFUN1:def 6;
then
A5: (F
/. y)
in H by
A1,
STRUCT_0:def 5;
x
= ((F
/. y)
|^ (
@ (I
/. y))) by
A3,
A4,
Def3;
then x
in H by
A5,
Th4;
hence thesis by
STRUCT_0:def 5;
end;
hence thesis by
Th18;
end;
theorem ::
GROUP_4:21
Th21: ((
<*> the
carrier of G)
|^ (
<*>
INT ))
=
{}
proof
(
len (
<*> the
carrier of G))
=
0 ;
then (
len ((
<*> the
carrier of G)
|^ (
<*>
INT )))
=
0 by
Def3;
hence thesis;
end;
theorem ::
GROUP_4:22
Th22: (
<*a*>
|^
<*(
@ i)*>)
=
<*(a
|^ i)*>
proof
A1: (
len
<*a*>)
= 1 by
FINSEQ_1: 39;
A2:
now
let k;
A3: (
@ i)
= (
<*(
@ i)*>
/. 1) by
FINSEQ_4: 16;
A4: (
dom
<*a*>)
= (
Seg (
len
<*a*>)) by
FINSEQ_1:def 3;
assume k
in (
dom
<*a*>);
then
A5: k
= 1 by
A1,
A4,
FINSEQ_1: 2,
TARSKI:def 1;
hence (
<*(a
|^ i)*>
. k)
= (a
|^ i) by
FINSEQ_1: 40
.= ((
<*a*>
/. k)
|^ (
@ (
<*(
@ i)*>
/. k))) by
A3,
A5,
FINSEQ_4: 16;
end;
(
len
<*(a
|^ i)*>)
= 1 by
FINSEQ_1: 39;
hence thesis by
A1,
A2,
Def3;
end;
theorem ::
GROUP_4:23
Th23: (
<*a, b*>
|^
<*(
@ i), (
@ j)*>)
=
<*(a
|^ i), (b
|^ j)*>
proof
A1: (
len
<*(
@ i)*>)
= 1 & (
len
<*(
@ j)*>)
= 1 by
FINSEQ_1: 39;
A2:
<*a, b*>
= (
<*a*>
^
<*b*>) &
<*(
@ i), (
@ j)*>
= (
<*(
@ i)*>
^
<*(
@ j)*>) by
FINSEQ_1:def 9;
(
len
<*a*>)
= 1 & (
len
<*b*>)
= 1 by
FINSEQ_1: 39;
hence (
<*a, b*>
|^
<*(
@ i), (
@ j)*>)
= ((
<*a*>
|^
<*(
@ i)*>)
^ (
<*b*>
|^
<*(
@ j)*>)) by
A1,
A2,
Th19
.= (
<*(a
|^ i)*>
^ (
<*b*>
|^
<*(
@ j)*>)) by
Th22
.= (
<*(a
|^ i)*>
^
<*(b
|^ j)*>) by
Th22
.=
<*(a
|^ i), (b
|^ j)*> by
FINSEQ_1:def 9;
end;
theorem ::
GROUP_4:24
(
<*a, b, c*>
|^
<*(
@ i1), (
@ i2), (
@ i3)*>)
=
<*(a
|^ i1), (b
|^ i2), (c
|^ i3)*>
proof
A1: (
len
<*(
@ i1)*>)
= 1 & (
len
<*(
@ i2), (
@ i3)*>)
= 2 by
FINSEQ_1: 39,
FINSEQ_1: 44;
A2:
<*a, b, c*>
= (
<*a*>
^
<*b, c*>) &
<*(
@ i1), (
@ i2), (
@ i3)*>
= (
<*(
@ i1)*>
^
<*(
@ i2), (
@ i3)*>) by
FINSEQ_1: 43;
(
len
<*a*>)
= 1 & (
len
<*b, c*>)
= 2 by
FINSEQ_1: 39,
FINSEQ_1: 44;
hence (
<*a, b, c*>
|^
<*(
@ i1), (
@ i2), (
@ i3)*>)
= ((
<*a*>
|^
<*(
@ i1)*>)
^ (
<*b, c*>
|^
<*(
@ i2), (
@ i3)*>)) by
A1,
A2,
Th19
.= (
<*(a
|^ i1)*>
^ (
<*b, c*>
|^
<*(
@ i2), (
@ i3)*>)) by
Th22
.= (
<*(a
|^ i1)*>
^
<*(b
|^ i2), (c
|^ i3)*>) by
Th23
.=
<*(a
|^ i1), (b
|^ i2), (c
|^ i3)*> by
FINSEQ_1: 43;
end;
theorem ::
GROUP_4:25
(F
|^ ((
len F)
|-> (
@ 1)))
= F
proof
defpred
P[
FinSequence of the
carrier of G] means ($1
|^ ((
len $1)
|-> (
@ 1)))
= $1;
A1: for F, a st
P[F] holds
P[(F
^
<*a*>)]
proof
let F, a;
set A = (F
^
<*a*>);
assume
A2:
P[F];
A3: (
len
<*a*>)
= 1 by
FINSEQ_1: 40;
A4: (
len
<*(
@ 1)*>)
= 1 & (
len ((
len F)
|-> (
@ 1)))
= (
len F) by
CARD_1:def 7;
(
len A)
= ((
len F)
+ (
len
<*a*>)) by
FINSEQ_1: 22;
hence (A
|^ ((
len A)
|-> (
@ 1)))
= (A
|^ (((
len F)
|-> (
@ 1))
^
<*(
@ 1)*>)) by
A3,
FINSEQ_2: 60
.= ((F
|^ ((
len F)
|-> (
@ 1)))
^ (
<*a*>
|^
<*(
@ 1)*>)) by
A3,
A4,
Th19
.= (F
^
<*(a
|^ 1)*>) by
A2,
Th22
.= (F
^
<*a*>) by
GROUP_1: 26;
end;
A5:
P[(
<*> the
carrier of G)]
proof
set A = (
<*> the
carrier of G);
thus (A
|^ ((
len A)
|-> (
@ 1)))
= (A
|^ (
0
|-> (
@ 1)))
.= (A
|^ (
<*>
INT ))
.= A by
Th21;
end;
for F holds
P[F] from
FINSEQ_2:sch 2(
A5,
A1);
hence thesis;
end;
theorem ::
GROUP_4:26
(F
|^ ((
len F)
|-> (
@
0 )))
= ((
len F)
|-> (
1_ G))
proof
defpred
P[
FinSequence of the
carrier of G] means ($1
|^ ((
len $1)
|-> (
@
0 )))
= ((
len $1)
|-> (
1_ G));
A1: for F, a st
P[F] holds
P[(F
^
<*a*>)]
proof
let F, a;
set A = (F
^
<*a*>);
assume
A2:
P[F];
A3: (
len
<*a*>)
= 1 by
FINSEQ_1: 40;
A4: (
len
<*(
@
0 )*>)
= 1 & (
len ((
len F)
|-> (
@
0 )))
= (
len F) by
CARD_1:def 7;
A5: (
len A)
= ((
len F)
+ (
len
<*a*>)) by
FINSEQ_1: 22;
hence (A
|^ ((
len A)
|-> (
@
0 )))
= (A
|^ (((
len F)
|-> (
@
0 ))
^
<*(
@
0 )*>)) by
A3,
FINSEQ_2: 60
.= ((F
|^ ((
len F)
|-> (
@
0 )))
^ (
<*a*>
|^
<*(
@
0 )*>)) by
A3,
A4,
Th19
.= (((
len F)
|-> (
1_ G))
^
<*(a
|^
0 )*>) by
A2,
Th22
.= (((
len F)
|-> (
1_ G))
^
<*(
1_ G)*>) by
GROUP_1: 25
.= ((
len A)
|-> (
1_ G)) by
A5,
A3,
FINSEQ_2: 60;
end;
A6:
P[(
<*> the
carrier of G)]
proof
set A = (
<*> the
carrier of G);
thus (A
|^ ((
len A)
|-> (
@
0 )))
= (A
|^ (
0
|-> (
@
0 )))
.= (A
|^ (
<*>
INT ))
.=
{} by
Th21
.= ((
len A)
|-> (
1_ G));
end;
for F holds
P[F] from
FINSEQ_2:sch 2(
A6,
A1);
hence thesis;
end;
theorem ::
GROUP_4:27
(
len I)
= n implies ((n
|-> (
1_ G))
|^ I)
= (n
|-> (
1_ G))
proof
defpred
P[
Nat] means for I st (
len I)
= $1 holds (($1
|-> (
1_ G))
|^ I)
= ($1
|-> (
1_ G));
A1: for k st
P[k] holds
P[(k
+ 1)]
proof
let k;
assume
A2:
P[k];
let I;
reconsider J = (I
| (
Seg k)) as
FinSequence of
INT by
FINSEQ_1: 18;
assume
A3: (
len I)
= (k
+ 1);
then
A4: (
len J)
= k by
FINSEQ_3: 53;
then
A5: ((k
|-> (
1_ G))
|^ J)
= (k
|-> (
1_ G)) by
A2;
A6: (
rng I)
c=
INT by
FINSEQ_1:def 4;
1
<= (k
+ 1) by
NAT_1: 12;
then (k
+ 1)
in (
dom I) by
A3,
FINSEQ_3: 25;
then (I
. (k
+ 1))
in (
rng I) by
FUNCT_1:def 3;
then
reconsider i = (I
. (k
+ 1)) as
Integer by
A6;
A7: (
len
<*(
1_ G)*>)
= 1 & (
len
<*(
@ i)*>)
= 1 by
FINSEQ_1: 40;
A8: ((k
+ 1)
|-> (
1_ G))
= ((k
|-> (
1_ G))
^
<*(
1_ G)*>) & (
len (k
|-> (
1_ G)))
= k by
CARD_1:def 7,
FINSEQ_2: 60;
I
= (J
^
<*(
@ i)*>) by
A3,
FINSEQ_3: 55;
then (((k
+ 1)
|-> (
1_ G))
|^ I)
= (((k
|-> (
1_ G))
|^ J)
^ (
<*(
1_ G)*>
|^
<*(
@ i)*>)) by
A4,
A8,
A7,
Th19
.= ((k
|-> (
1_ G))
^
<*((
1_ G)
|^ i)*>) by
A5,
Th22
.= ((k
|-> (
1_ G))
^
<*(
1_ G)*>) by
GROUP_1: 31;
hence thesis by
FINSEQ_2: 60;
end;
A9:
P[
0 ]
proof
let I;
assume (
len I)
=
0 ;
then
A10: I
= (
<*>
INT );
{}
= (
<*> the
carrier of G);
hence thesis by
A10,
Th21;
end;
for k holds
P[k] from
NAT_1:sch 2(
A9,
A1);
hence thesis;
end;
definition
let G, A;
::
GROUP_4:def4
func
gr A ->
strict
Subgroup of G means
:
Def4: A
c= the
carrier of it & for H be
strict
Subgroup of G st A
c= the
carrier of H holds it is
Subgroup of H;
existence
proof
defpred
P[
set] means ex H st $1
= (
carr H) & A
c= $1;
consider X such that
A1: Y
in X iff Y
in (
bool the
carrier of G) &
P[Y] from
XFAMILY:sch 1;
set M = (
meet X);
A2: (
carr (
(Omega). G))
= the
carrier of (
(Omega). G);
then
A3: X
<>
{} by
A1;
A4: the
carrier of G
in X by
A1,
A2;
A5: M
c= the
carrier of G by
A4,
SETFAM_1:def 1;
now
let Y;
assume Y
in X;
then
consider H such that
A6: Y
= (
carr H) and A
c= Y by
A1;
(
1_ G)
in H by
GROUP_2: 46;
hence (
1_ G)
in Y by
A6,
STRUCT_0:def 5;
end;
then
A7: M
<>
{} by
A3,
SETFAM_1:def 1;
reconsider M as
Subset of G by
A5;
A8:
now
let a, b;
assume
A9: a
in M & b
in M;
now
let Y;
assume
A10: Y
in X;
then
consider H such that
A11: Y
= (
carr H) and A
c= Y by
A1;
a
in (
carr H) & b
in (
carr H) by
A9,
A10,
A11,
SETFAM_1:def 1;
hence (a
* b)
in Y by
A11,
GROUP_2: 74;
end;
hence (a
* b)
in M by
A3,
SETFAM_1:def 1;
end;
now
let a;
assume
A12: a
in M;
now
let Y;
assume
A13: Y
in X;
then
consider H such that
A14: Y
= (
carr H) and A
c= Y by
A1;
a
in (
carr H) by
A12,
A13,
A14,
SETFAM_1:def 1;
hence (a
" )
in Y by
A14,
GROUP_2: 75;
end;
hence (a
" )
in M by
A3,
SETFAM_1:def 1;
end;
then
consider H be
strict
Subgroup of G such that
A15: the
carrier of H
= M by
A7,
A8,
GROUP_2: 52;
take H;
now
let Y;
assume Y
in X;
then ex H st Y
= (
carr H) & A
c= Y by
A1;
hence A
c= Y;
end;
hence A
c= the
carrier of H by
A3,
A15,
SETFAM_1: 5;
let H1 be
strict
Subgroup of G;
A16: the
carrier of H1
= (
carr H1);
assume A
c= the
carrier of H1;
then the
carrier of H1
in X by
A1,
A16;
hence thesis by
A15,
GROUP_2: 57,
SETFAM_1: 3;
end;
uniqueness
proof
let H1,H2 be
strict
Subgroup of G;
assume A
c= the
carrier of H1 & (for H be
strict
Subgroup of G st A
c= the
carrier of H holds H1 is
Subgroup of H) & A
c= the
carrier of H2 & for H be
strict
Subgroup of G st A
c= the
carrier of H holds H2 is
Subgroup of H;
then H1 is
Subgroup of H2 & H2 is
Subgroup of H1;
hence thesis by
GROUP_2: 55;
end;
end
theorem ::
GROUP_4:28
Th28: a
in (
gr A) iff ex F, I st (
len F)
= (
len I) & (
rng F)
c= A & (
Product (F
|^ I))
= a
proof
thus a
in (
gr A) implies ex F, I st (
len F)
= (
len I) & (
rng F)
c= A & (
Product (F
|^ I))
= a
proof
defpred
P[
set] means ex F, I st $1
= (
Product (F
|^ I)) & (
len F)
= (
len I) & (
rng F)
c= A;
assume
A1: a
in (
gr A);
reconsider B = { b :
P[b] } as
Subset of G from
DOMAIN_1:sch 7;
A2:
now
let c, d;
assume that
A3: c
in B and
A4: d
in B;
ex d1 be
Element of G st c
= d1 & ex F, I st d1
= (
Product (F
|^ I)) & (
len F)
= (
len I) & (
rng F)
c= A by
A3;
then
consider F1, I1 such that
A5: c
= (
Product (F1
|^ I1)) and
A6: (
len F1)
= (
len I1) and
A7: (
rng F1)
c= A;
ex d2 be
Element of G st d
= d2 & ex F, I st d2
= (
Product (F
|^ I)) & (
len F)
= (
len I) & (
rng F)
c= A by
A4;
then
consider F2, I2 such that
A8: d
= (
Product (F2
|^ I2)) and
A9: (
len F2)
= (
len I2) and
A10: (
rng F2)
c= A;
A11: (
len (F1
^ F2))
= ((
len I1)
+ (
len I2)) by
A6,
A9,
FINSEQ_1: 22
.= (
len (I1
^ I2)) by
FINSEQ_1: 22;
(
rng (F1
^ F2))
= ((
rng F1)
\/ (
rng F2)) by
FINSEQ_1: 31;
then
A12: (
rng (F1
^ F2))
c= A by
A7,
A10,
XBOOLE_1: 8;
(c
* d)
= (
Product ((F1
|^ I1)
^ (F2
|^ I2))) by
A5,
A8,
FINSOP_1: 5
.= (
Product ((F1
^ F2)
|^ (I1
^ I2))) by
A6,
A9,
Th19;
hence (c
* d)
in B by
A12,
A11;
end;
A13:
now
let c;
assume c
in B;
then ex d1 be
Element of G st c
= d1 & ex F, I st d1
= (
Product (F
|^ I)) & (
len F)
= (
len I) & (
rng F)
c= A;
then
consider F1, I1 such that
A14: c
= (
Product (F1
|^ I1)) and
A15: (
len F1)
= (
len I1) and
A16: (
rng F1)
c= A;
deffunc
F(
Nat) = (F1
. (((
len F1)
- $1)
+ 1));
consider F2 be
FinSequence such that
A17: (
len F2)
= (
len F1) and
A18: for k be
Nat st k
in (
dom F2) holds (F2
. k)
=
F(k) from
FINSEQ_1:sch 2;
A19: (
Seg (
len I1))
= (
dom I1) by
FINSEQ_1:def 3;
A20: (
rng F2)
c= (
rng F1)
proof
let x be
object;
assume x
in (
rng F2);
then
consider y be
object such that
A21: y
in (
dom F2) and
A22: (F2
. y)
= x by
FUNCT_1:def 3;
reconsider y as
Element of
NAT by
A21;
reconsider n = (((
len F1)
- y)
+ 1) as
Element of
NAT by
A17,
A21,
Lm3;
1
<= n & n
<= (
len F1) by
A17,
A21,
Lm3;
then
A23: n
in (
dom F1) by
FINSEQ_3: 25;
x
= (F1
. (((
len F1)
- y)
+ 1)) by
A18,
A21,
A22;
hence thesis by
A23,
FUNCT_1:def 3;
end;
then
A24: (
rng F2)
c= A by
A16;
defpred
P[
Nat,
object] means ex i st i
= (I1
. (((
len I1)
- $1)
+ 1)) & $2
= (
- i);
A25: for k be
Nat st k
in (
Seg (
len I1)) holds ex x be
object st
P[k, x]
proof
let k be
Nat;
assume k
in (
Seg (
len I1));
then
A26: k
in (
dom I1) by
FINSEQ_1:def 3;
then
reconsider n = (((
len I1)
- k)
+ 1) as
Element of
NAT by
Lm3;
1
<= n & n
<= (
len I1) by
A26,
Lm3;
then n
in (
dom I1) by
FINSEQ_3: 25;
then
A27: (I1
. n)
in (
rng I1) by
FUNCT_1:def 3;
(
rng I1)
c=
INT by
FINSEQ_1:def 4;
then
reconsider i = (I1
. n) as
Element of
INT qua non
empty
set by
A27;
take (
- i), i;
thus thesis;
end;
consider I2 be
FinSequence such that
A28: (
dom I2)
= (
Seg (
len I1)) and
A29: for k be
Nat st k
in (
Seg (
len I1)) holds
P[k, (I2
. k)] from
FINSEQ_1:sch 1(
A25);
A30: (
len F2)
= (
len I2) by
A15,
A17,
A28,
FINSEQ_1:def 3;
A31: (
rng I2)
c=
INT
proof
let x be
object;
assume x
in (
rng I2);
then
consider y be
object such that
A32: y
in (
dom I2) and
A33: x
= (I2
. y) by
FUNCT_1:def 3;
reconsider y as
Element of
NAT by
A32;
ex i st i
= (I1
. (((
len I1)
- y)
+ 1)) & x
= (
- i) by
A28,
A29,
A32,
A33;
hence thesis by
INT_1:def 2;
end;
(
rng F1)
c= the
carrier of G by
FINSEQ_1:def 4;
then
A34: (
rng F2)
c= the
carrier of G by
A20;
set p = (F1
|^ I1);
A35: (
Seg (
len F1))
= (
dom F1) by
FINSEQ_1:def 3;
A36: (
len p)
= (
len F1) by
Def3;
A37: (
dom F2)
= (
dom I2) by
A15,
A17,
A28,
FINSEQ_1:def 3;
reconsider I2 as
FinSequence of
INT by
A31,
FINSEQ_1:def 4;
reconsider F2 as
FinSequence of the
carrier of G by
A34,
FINSEQ_1:def 4;
set q = (F2
|^ I2);
A38: (
len q)
= (
len F2) by
Def3;
then
A39: (
dom q)
= (
dom F2) by
FINSEQ_3: 29;
A40: (
dom F1)
= (
dom I1) by
A15,
FINSEQ_3: 29;
now
let k;
A41: (I2
/. k)
= (
@ (I2
/. k));
assume
A42: k
in (
dom q);
then
reconsider n = (((
len p)
- k)
+ 1) as
Element of
NAT by
A17,
A36,
A38,
Lm3;
A43: (I1
/. n)
= (
@ (I1
/. n)) & (q
/. k)
= (q
. k) by
A42,
PARTFUN1:def 6;
(
dom q)
= (
dom I1) by
A15,
A17,
A38,
FINSEQ_3: 29;
then
consider i such that
A44: i
= (I1
. n) and
A45: (I2
. k)
= (
- i) by
A15,
A29,
A19,
A36,
A42;
(I2
. k)
= (I2
/. k) by
A37,
A39,
A42,
PARTFUN1:def 6;
then
A46: (q
. k)
= ((F2
/. k)
|^ (
- i)) by
A39,
A42,
A45,
A41,
Def3;
A47: (F2
/. k)
= (F2
. k) & (F2
. k)
= (F1
. n) by
A18,
A36,
A39,
A42,
PARTFUN1:def 6;
1
<= n & (
len p)
>= n by
A17,
A36,
A38,
A42,
Lm3;
then
A48: n
in (
dom I2) by
A17,
A30,
A36,
FINSEQ_3: 25;
then
A49: (I1
. n)
= (I1
/. n) by
A28,
A19,
PARTFUN1:def 6;
(F1
/. n)
= (F1
. n) by
A15,
A35,
A28,
A48,
PARTFUN1:def 6;
then (q
. k)
= (((F1
/. n)
|^ i)
" ) by
A46,
A47,
GROUP_1: 36;
hence ((q
/. k)
" )
= (p
. (((
len p)
- k)
+ 1)) by
A40,
A28,
A19,
A48,
A44,
A49,
A43,
Def3;
end;
then ((
Product p)
" )
= (
Product q) by
A17,
A36,
A38,
Th14;
hence (c
" )
in B by
A14,
A30,
A24;
end;
A50: (
len
{} )
=
0 ;
A51: (
rng (
<*> the
carrier of G))
=
{} &
{}
c= A;
(
1_ G)
= (
Product (
<*> the
carrier of G)) & ((
<*> the
carrier of G)
|^ (
<*>
INT ))
=
{} by
Th8,
Th21;
then (
1_ G)
in B by
A51,
A50;
then
consider H be
strict
Subgroup of G such that
A52: the
carrier of H
= B by
A2,
A13,
GROUP_2: 52;
A
c= B
proof
reconsider p = 1 as
Integer;
let x be
object;
assume
A53: x
in A;
then
reconsider a = x as
Element of G;
A54: (
rng
<*a*>)
=
{a} &
{a}
c= A by
A53,
FINSEQ_1: 39,
ZFMISC_1: 31;
A55: (
len
<*a*>)
= 1 & (
len
<*(
@ p)*>)
= 1 by
FINSEQ_1: 39;
(
Product (
<*a*>
|^
<*(
@ p)*>))
= (
Product
<*(a
|^ 1)*>) by
Th22
.= (a
|^ 1) by
FINSOP_1: 11
.= a by
GROUP_1: 26;
hence thesis by
A55,
A54;
end;
then (
gr A) is
Subgroup of H by
A52,
Def4;
then a
in H by
A1,
GROUP_2: 40;
then a
in B by
A52,
STRUCT_0:def 5;
then ex b st b
= a & ex F, I st b
= (
Product (F
|^ I)) & (
len F)
= (
len I) & (
rng F)
c= A;
hence thesis;
end;
given F, I such that (
len F)
= (
len I) and
A56: (
rng F)
c= A and
A57: (
Product (F
|^ I))
= a;
A
c= the
carrier of (
gr A) by
Def4;
then (
rng F)
c= (
carr (
gr A)) by
A56;
hence thesis by
A57,
Th20;
end;
theorem ::
GROUP_4:29
Th29: a
in A implies a
in (
gr A)
proof
assume
A1: a
in A;
A
c= the
carrier of (
gr A) by
Def4;
hence thesis by
A1,
STRUCT_0:def 5;
end;
theorem ::
GROUP_4:30
(
gr (
{} the
carrier of G))
= (
(1). G)
proof
(
{} the
carrier of G)
c= the
carrier of (
(1). G) & for H be
strict
Subgroup of G st (
{} the
carrier of G)
c= the
carrier of H holds (
(1). G) is
Subgroup of H by
GROUP_2: 65;
hence thesis by
Def4;
end;
theorem ::
GROUP_4:31
Th31: for H be
strict
Subgroup of G holds (
gr (
carr H))
= H
proof
let H be
strict
Subgroup of G;
for H1 be
strict
Subgroup of G st (
carr H)
c= the
carrier of H1 holds H is
Subgroup of H1 by
GROUP_2: 57;
hence thesis by
Def4;
end;
theorem ::
GROUP_4:32
Th32: A
c= B implies (
gr A) is
Subgroup of (
gr B)
proof
assume
A1: A
c= B;
now
let a;
assume a
in (
gr A);
then
consider F, I such that
A2: (
len F)
= (
len I) and
A3: (
rng F)
c= A and
A4: (
Product (F
|^ I))
= a by
Th28;
(
rng F)
c= B by
A1,
A3;
hence a
in (
gr B) by
A2,
A4,
Th28;
end;
hence thesis by
GROUP_2: 58;
end;
theorem ::
GROUP_4:33
(
gr (A
/\ B)) is
Subgroup of ((
gr A)
/\ (
gr B))
proof
now
let a;
assume a
in (
gr (A
/\ B));
then
consider F, I such that
A1: (
len F)
= (
len I) and
A2: (
rng F)
c= (A
/\ B) and
A3: (
Product (F
|^ I))
= a by
Th28;
(A
/\ B)
c= B by
XBOOLE_1: 17;
then (
rng F)
c= B by
A2;
then
A4: a
in (
gr B) by
A1,
A3,
Th28;
(A
/\ B)
c= A by
XBOOLE_1: 17;
then (
rng F)
c= A by
A2;
then a
in (
gr A) by
A1,
A3,
Th28;
hence a
in ((
gr A)
/\ (
gr B)) by
A4,
GROUP_2: 82;
end;
hence thesis by
GROUP_2: 58;
end;
theorem ::
GROUP_4:34
Th34: the
carrier of (
gr A)
= (
meet { B : ex H be
strict
Subgroup of G st B
= the
carrier of H & A
c= (
carr H) })
proof
defpred
P[
Subgroup of G] means A
c= (
carr $1);
set X = { B : ex H be
strict
Subgroup of G st B
= the
carrier of H & A
c= (
carr H) };
A1:
now
let Y;
assume Y
in X;
then ex B st Y
= B & ex H be
strict
Subgroup of G st B
= the
carrier of H & A
c= (
carr H);
hence A
c= Y;
end;
the
carrier of (
(Omega). G)
= (
carr (
(Omega). G));
then
A2: ex H be
strict
Subgroup of G st
P[H];
consider H be
strict
Subgroup of G such that
A3: the
carrier of H
= (
meet { B : ex H be
strict
Subgroup of G st B
= the
carrier of H &
P[H] }) from
MeetSbgEx(
A2);
A4:
now
let H1 be
strict
Subgroup of G;
A5: the
carrier of H1
= (
carr H1);
assume A
c= the
carrier of H1;
then the
carrier of H1
in X by
A5;
hence H is
Subgroup of H1 by
A3,
GROUP_2: 57,
SETFAM_1: 3;
end;
(
carr (
(Omega). G))
in X;
then A
c= the
carrier of H by
A3,
A1,
SETFAM_1: 5;
hence thesis by
A3,
A4,
Def4;
end;
theorem ::
GROUP_4:35
Th35: (
gr A)
= (
gr (A
\
{(
1_ G)}))
proof
set X = { B : ex H be
strict
Subgroup of G st B
= the
carrier of H & A
c= (
carr H) };
set Y = { C : ex H be
strict
Subgroup of G st C
= the
carrier of H & (A
\
{(
1_ G)})
c= (
carr H) };
A1: X
= Y
proof
thus X
c= Y
proof
let x be
object;
assume x
in X;
then
consider B such that
A2: x
= B and
A3: ex H be
strict
Subgroup of G st B
= the
carrier of H & A
c= (
carr H);
consider H be
strict
Subgroup of G such that
A4: B
= the
carrier of H and
A5: A
c= (
carr H) by
A3;
(A
\
{(
1_ G)})
c= A by
XBOOLE_1: 36;
then (A
\
{(
1_ G)})
c= (
carr H) by
A5;
hence thesis by
A2,
A4;
end;
let x be
object;
assume x
in Y;
then
consider B such that
A6: x
= B and
A7: ex H be
strict
Subgroup of G st B
= the
carrier of H & (A
\
{(
1_ G)})
c= (
carr H);
consider H be
strict
Subgroup of G such that
A8: B
= the
carrier of H and
A9: (A
\
{(
1_ G)})
c= (
carr H) by
A7;
(
1_ G)
in H by
GROUP_2: 46;
then (
1_ G)
in (
carr H) by
STRUCT_0:def 5;
then
{(
1_ G)}
c= (
carr H) by
ZFMISC_1: 31;
then
A10: ((A
\
{(
1_ G)})
\/
{(
1_ G)})
c= (
carr H) by
A9,
XBOOLE_1: 8;
now
per cases ;
suppose (
1_ G)
in A;
then
{(
1_ G)}
c= A by
ZFMISC_1: 31;
hence A
c= (
carr H) by
A10,
XBOOLE_1: 45;
end;
suppose not (
1_ G)
in A;
hence A
c= (
carr H) by
A9,
ZFMISC_1: 57;
end;
end;
hence thesis by
A6,
A8;
end;
the
carrier of (
gr A)
= (
meet X) by
Th34
.= the
carrier of (
gr (A
\
{(
1_ G)})) by
A1,
Th34;
hence thesis by
GROUP_2: 59;
end;
definition
let G, a;
::
GROUP_4:def5
attr a is
generating means not for A st (
gr A)
= the multMagma of G holds (
gr (A
\
{a}))
= the multMagma of G;
end
theorem ::
GROUP_4:36
(
1_ G) is non
generating by
Th35;
definition
let G, H;
::
GROUP_4:def6
attr H is
maximal means the multMagma of H
<> the multMagma of G & for K be
strict
Subgroup of G st the multMagma of H
<> K & H is
Subgroup of K holds K
= the multMagma of G;
end
theorem ::
GROUP_4:37
Th37: for G be
strict
Group, H be
strict
Subgroup of G, a be
Element of G holds H is
maximal & not a
in H implies (
gr ((
carr H)
\/
{a}))
= G
proof
let G be
strict
Group, H be
strict
Subgroup of G, a be
Element of G;
assume that
A1: H is
maximal and
A2: not a
in H;
(
gr (
carr H)) is
Subgroup of (
gr ((
carr H)
\/
{a})) by
Th32,
XBOOLE_1: 7;
then
A3: H is
Subgroup of (
gr ((
carr H)
\/
{a})) by
Th31;
a
in
{a} by
TARSKI:def 1;
then a
in ((
carr H)
\/
{a}) by
XBOOLE_0:def 3;
then H
<> (
gr ((
carr H)
\/
{a})) by
A2,
Th29;
hence thesis by
A1,
A3;
end;
definition
let G be
Group;
::$Notion-Name
::
GROUP_4:def7
func
Phi (G) ->
strict
Subgroup of G means
:
Def7: the
carrier of it
= (
meet { A where A be
Subset of G : ex H be
strict
Subgroup of G st A
= the
carrier of H & H is
maximal }) if ex H be
strict
Subgroup of G st H is
maximal
otherwise it
= the multMagma of G;
existence
proof
defpred
P[
Subgroup of G] means $1 is
maximal;
now
per cases ;
suppose
A1: ex H be
strict
Subgroup of G st
P[H];
ex H be
strict
Subgroup of G st the
carrier of H
= (
meet { A where A be
Subset of G : ex K be
strict
Subgroup of G st A
= the
carrier of K &
P[K] }) from
MeetSbgEx(
A1);
hence thesis by
A1;
end;
suppose
A2: for H be
strict
Subgroup of G holds not H is
maximal;
(
(Omega). G)
= the multMagma of G;
hence thesis by
A2;
end;
end;
hence thesis;
end;
uniqueness by
GROUP_2: 59;
correctness ;
end
theorem ::
GROUP_4:38
Th38: for G be
Group holds (ex H be
strict
Subgroup of G st H is
maximal) implies (a
in (
Phi G) iff for H be
strict
Subgroup of G st H is
maximal holds a
in H)
proof
let G be
Group;
set X = { A where A be
Subset of G : ex K be
strict
Subgroup of G st A
= the
carrier of K & K is
maximal };
assume
A1: ex H be
strict
Subgroup of G st H is
maximal;
then
consider H be
strict
Subgroup of G such that
A2: H is
maximal;
thus a
in (
Phi G) implies for H be
strict
Subgroup of G st H is
maximal holds a
in H
proof
assume a
in (
Phi G);
then a
in the
carrier of (
Phi G) by
STRUCT_0:def 5;
then
A3: a
in (
meet X) by
A1,
Def7;
let H be
strict
Subgroup of G;
assume H is
maximal;
then (
carr H)
in X;
then a
in (
carr H) by
A3,
SETFAM_1:def 1;
hence thesis by
STRUCT_0:def 5;
end;
assume
A4: for H be
strict
Subgroup of G st H is
maximal holds a
in H;
A5:
now
let Y;
assume Y
in X;
then
consider A be
Subset of G such that
A6: Y
= A and
A7: ex H be
strict
Subgroup of G st A
= the
carrier of H & H is
maximal;
consider H be
strict
Subgroup of G such that
A8: A
= the
carrier of H and
A9: H is
maximal by
A7;
a
in H by
A4,
A9;
hence a
in Y by
A6,
A8,
STRUCT_0:def 5;
end;
(
carr H)
in X by
A2;
then a
in (
meet X) by
A5,
SETFAM_1:def 1;
then a
in the
carrier of (
Phi G) by
A1,
Def7;
hence thesis by
STRUCT_0:def 5;
end;
theorem ::
GROUP_4:39
for G be
Group, a be
Element of G holds (for H be
strict
Subgroup of G holds not H is
maximal) implies a
in (
Phi G)
proof
let G be
Group, a be
Element of G;
assume for H be
strict
Subgroup of G holds not H is
maximal;
then (
Phi G)
= the multMagma of G by
Def7;
hence thesis by
STRUCT_0:def 5;
end;
theorem ::
GROUP_4:40
Th40: for G be
Group, H be
strict
Subgroup of G holds H is
maximal implies (
Phi G) is
Subgroup of H
proof
let G be
Group, H be
strict
Subgroup of G;
assume H is
maximal;
then for a be
Element of G holds a
in (
Phi G) implies a
in H by
Th38;
hence thesis by
GROUP_2: 58;
end;
theorem ::
GROUP_4:41
Th41: for G be
strict
Group holds the
carrier of (
Phi G)
= { a where a be
Element of G : a is non
generating }
proof
let G be
strict
Group;
set A = { a where a be
Element of G : a is non
generating };
thus the
carrier of (
Phi G)
c= A
proof
defpred
P[
set,
set] means ex H1,H2 be
strict
Subgroup of G st $1
= H1 & $2
= H2 & H1 is
Subgroup of H2;
let x be
object;
assume
A1: x
in the
carrier of (
Phi G);
then x
in (
Phi G) 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;
assume not x
in A;
then a is
generating;
then
consider B be
Subset of G such that
A2: (
gr B)
= G and
A3: (
gr (B
\
{a}))
<> G;
set M = (B
\
{a});
A4:
now
assume
A5: a
in (
gr M);
now
let b be
Element of G;
b
in (
gr B) by
A2,
STRUCT_0:def 5;
then
consider F be
FinSequence of the
carrier of G, I such that (
len I)
= (
len F) and
A6: (
rng F)
c= B and
A7: b
= (
Product (F
|^ I)) by
Th28;
(
rng (F
|^ I))
c= (
carr (
gr M))
proof
let x be
object;
assume x
in (
rng (F
|^ I));
then
consider y be
object such that
A8: y
in (
dom (F
|^ I)) and
A9: ((F
|^ I)
. y)
= x by
FUNCT_1:def 3;
reconsider y as
Element of
NAT by
A8;
(
len (F
|^ I))
= (
len F) by
Def3;
then
A10: y
in (
dom F) by
A8,
FINSEQ_3: 29;
then
A11: x
= ((F
/. y)
|^ (
@ (I
/. y))) by
A9,
Def3;
now
per cases ;
suppose (F
/. y)
= a;
then x
in (
gr M) by
A5,
A11,
Th4;
hence thesis by
STRUCT_0:def 5;
end;
suppose (F
/. y)
<> a;
then
A12: not (F
/. y)
in
{a} by
TARSKI:def 1;
(F
/. y)
= (F
. y) & (F
. y)
in (
rng F) by
A10,
FUNCT_1:def 3,
PARTFUN1:def 6;
then (F
/. y)
in M by
A6,
A12,
XBOOLE_0:def 5;
then x
in (
gr M) by
A11,
Th4,
Th29;
hence thesis by
STRUCT_0:def 5;
end;
end;
hence thesis;
end;
hence b
in (
gr M) by
A7,
Th18;
end;
hence contradiction by
A3,
GROUP_2: 62;
end;
defpred
P[
Subgroup of G] means M
c= (
carr $1) & not a
in $1;
consider X such that
A13: X
c= (
Subgroups G) and
A14: for H be
strict
Subgroup of G holds H
in X iff
P[H] from
SubgrSep;
M
c= (
carr (
gr M)) by
Def4;
then
reconsider X as non
empty
set by
A14,
A4;
A15: for x,y,z be
Element of X st
P[x, y] &
P[y, z] holds
P[x, z]
proof
let x,y,z be
Element of X;
given H1,H2 be
strict
Subgroup of G such that
A16: x
= H1 and
A17: y
= H2 & H1 is
Subgroup of H2;
given H3,H4 be
strict
Subgroup of G such that
A18: y
= H3 and
A19: z
= H4 and
A20: H3 is
Subgroup of H4;
H1 is
Subgroup of H4 by
A17,
A18,
A20,
GROUP_2: 56;
hence thesis by
A16,
A19;
end;
A21: for Y st Y
c= X & (for x,y be
Element of X st x
in Y & y
in Y holds
P[x, y] or
P[y, x]) holds ex y be
Element of X st for x be
Element of X st x
in Y holds
P[x, y]
proof
let Y;
assume
A22: Y
c= X;
set C = { D where D be
Subset of G : ex H be
strict
Subgroup of G st H
in Y & D
= (
carr H) };
now
let Z be
set;
assume Z
in C;
then ex D be
Subset of G st Z
= D & ex H be
strict
Subgroup of G st H
in Y & D
= (
carr H);
hence Z
c= the
carrier of G;
end;
then
reconsider E = (
union C) as
Subset of G by
ZFMISC_1: 76;
assume
A23: for x,y be
Element of X st x
in Y & y
in Y holds
P[x, y] or
P[y, x];
now
per cases ;
suppose
A24: Y
=
{} ;
set y = the
Element of X;
take y;
let x be
Element of X;
assume x
in Y;
hence
P[x, y] by
A24;
end;
suppose
A25: Y
<>
{} ;
A26:
now
let a,b be
Element of G;
assume that
A27: a
in E and
A28: b
in E;
consider Z be
set such that
A29: a
in Z and
A30: Z
in C by
A27,
TARSKI:def 4;
consider Z1 be
set such that
A31: b
in Z1 and
A32: Z1
in C by
A28,
TARSKI:def 4;
consider D be
Subset of G such that
A33: Z
= D and
A34: ex H be
strict
Subgroup of G st H
in Y & D
= (
carr H) by
A30;
consider B be
Subset of G such that
A35: Z1
= B and
A36: ex H be
strict
Subgroup of G st H
in Y & B
= (
carr H) by
A32;
consider H1 be
Subgroup of G such that
A37: H1
in Y and
A38: D
= (
carr H1) by
A34;
consider H2 be
Subgroup of G such that
A39: H2
in Y and
A40: B
= (
carr H2) by
A36;
now
per cases by
A22,
A23,
A37,
A39;
suppose
P[H1, H2];
then (
carr H1)
c= the
carrier of H2 by
GROUP_2:def 5;
then (a
* b)
in (
carr H2) by
A29,
A33,
A38,
A31,
A35,
A40,
GROUP_2: 74;
hence (a
* b)
in E by
A32,
A35,
A40,
TARSKI:def 4;
end;
suppose
P[H2, H1];
then (
carr H2)
c= the
carrier of H1 by
GROUP_2:def 5;
then (a
* b)
in (
carr H1) by
A29,
A33,
A38,
A31,
A35,
A40,
GROUP_2: 74;
hence (a
* b)
in E by
A30,
A33,
A38,
TARSKI:def 4;
end;
end;
hence (a
* b)
in E;
end;
A41:
now
let a be
Element of G;
assume a
in E;
then
consider Z be
set such that
A42: a
in Z and
A43: Z
in C by
TARSKI:def 4;
consider D be
Subset of G such that
A44: Z
= D and
A45: ex H be
strict
Subgroup of G st H
in Y & D
= (
carr H) by
A43;
consider H1 be
Subgroup of G such that H1
in Y and
A46: D
= (
carr H1) by
A45;
(a
" )
in (
carr H1) by
A42,
A44,
A46,
GROUP_2: 75;
hence (a
" )
in E by
A43,
A44,
A46,
TARSKI:def 4;
end;
set s = the
Element of Y;
A47: s
in X by
A22,
A25;
then
reconsider s as
strict
Subgroup of G by
A13,
GROUP_3:def 1;
A48: (
carr s)
in C by
A25;
then
A49: (
carr s)
c= E by
ZFMISC_1: 74;
E
<>
{} by
A48,
ORDERS_1: 6;
then
consider H be
strict
Subgroup of G such that
A50: the
carrier of H
= E by
A26,
A41,
GROUP_2: 52;
A51:
now
assume a
in H;
then a
in E by
A50,
STRUCT_0:def 5;
then
consider Z be
set such that
A52: a
in Z and
A53: Z
in C by
TARSKI:def 4;
consider D be
Subset of G such that
A54: Z
= D and
A55: ex H be
strict
Subgroup of G st H
in Y & D
= (
carr H) by
A53;
consider H1 be
strict
Subgroup of G such that
A56: H1
in Y and
A57: D
= (
carr H1) by
A55;
not a
in H1 by
A14,
A22,
A56;
hence contradiction by
A52,
A54,
A57,
STRUCT_0:def 5;
end;
M
c= (
carr s) by
A14,
A47;
then
A58: M
c= E by
A49;
the
carrier of H
= (
carr H);
then
reconsider y = H as
Element of X by
A14,
A58,
A50,
A51;
take y;
let x be
Element of X;
assume
A59: x
in Y;
x
in (
Subgroups G) by
A13;
then
reconsider K = x as
strict
Subgroup of G by
GROUP_3:def 1;
take K, H;
thus x
= K & y
= H;
(
carr K)
= the
carrier of K;
then the
carrier of K
in C by
A59;
hence K is
Subgroup of H by
A50,
GROUP_2: 57,
ZFMISC_1: 74;
end;
end;
hence thesis;
end;
A60:
now
let x be
Element of X;
x
in (
Subgroups G) by
A13;
hence x is
strict
Subgroup of G by
GROUP_3:def 1;
end;
A61: for x be
Element of X holds
P[x, x]
proof
let x be
Element of X;
reconsider H = x as
strict
Subgroup of G by
A60;
H is
Subgroup of H by
GROUP_2: 54;
hence thesis;
end;
A62: for x,y be
Element of X st
P[x, y] &
P[y, x] holds x
= y by
GROUP_2: 55;
consider s be
Element of X such that
A63: for y be
Element of X st s
<> y holds not
P[s, y] from
ORDERS_1:sch 1(
A61,
A62,
A15,
A21);
reconsider H = s as
strict
Subgroup of G by
A60;
H is
maximal
proof
not a
in H by
A14;
hence the multMagma of H
<> the multMagma of G by
STRUCT_0:def 5;
let K be
strict
Subgroup of G;
assume that
A64: K
<> the multMagma of H and
A65: H is
Subgroup of K and
A66: K
<> the multMagma of G;
A67: M
c= (
carr H) by
A14;
the
carrier of H
c= the
carrier of K by
A65,
GROUP_2:def 5;
then
A68: M
c= (
carr K) by
A67;
now
A69: B
c= (M
\/
{a})
proof
let x be
object;
assume
A70: x
in B;
now
per cases ;
suppose x
= a;
then x
in
{a} by
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 3;
end;
suppose x
<> a;
then not x
in
{a} by
TARSKI:def 1;
then x
in M by
A70,
XBOOLE_0:def 5;
hence thesis by
XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
assume a
in K;
then a
in (
carr K) by
STRUCT_0:def 5;
then
{a}
c= (
carr K) by
ZFMISC_1: 31;
then (M
\/
{a})
c= (
carr K) by
A68,
XBOOLE_1: 8;
then (
gr B) is
Subgroup of (
gr (
carr K)) by
A69,
Th32,
XBOOLE_1: 1;
then G is
Subgroup of K by
A2,
Th31;
hence contradiction by
A66,
GROUP_2: 55;
end;
then
reconsider v = K as
Element of X by
A14,
A68;
not
P[s, v] by
A63,
A64;
hence thesis by
A65;
end;
then (
Phi G) is
Subgroup of H by
Th40;
then the
carrier of (
Phi G)
c= the
carrier of H by
GROUP_2:def 5;
then x
in H by
A1,
STRUCT_0:def 5;
hence thesis by
A14;
end;
let x be
object;
assume x
in A;
then
consider a be
Element of G such that
A71: x
= a and
A72: a is non
generating;
now
per cases ;
suppose for H be
strict
Subgroup of G holds not H is
maximal;
then (
Phi G)
= G by
Def7;
hence thesis by
A71;
end;
suppose
A73: ex H be
strict
Subgroup of G st H is
maximal;
now
let H be
strict
Subgroup of G;
assume
A74: H is
maximal;
now
assume
A75: not a
in H;
((
carr H)
/\
{a})
c=
{}
proof
let x be
object;
assume
A76: x
in ((
carr H)
/\
{a});
then x
in
{a} by
XBOOLE_0:def 4;
then
A77: x
= a by
TARSKI:def 1;
x
in (
carr H) by
A76,
XBOOLE_0:def 4;
hence thesis by
A75,
A77,
STRUCT_0:def 5;
end;
then ((
carr H)
/\
{a})
=
{} ;
then
A78: (
carr H)
misses
{a};
(((
carr H)
\/
{a})
\
{a})
= ((
carr H)
\
{a}) by
XBOOLE_1: 40
.= (
carr H) by
A78,
XBOOLE_1: 83;
then
A79: (
gr (((
carr H)
\/
{a})
\
{a}))
= H by
Th31;
A80: H
<> G by
A74;
(
gr ((
carr H)
\/
{a}))
= G by
A74,
A75,
Th37;
hence contradiction by
A72,
A79,
A80;
end;
hence a
in H;
end;
then a
in (
Phi G) by
A73,
Th38;
hence thesis by
A71,
STRUCT_0:def 5;
end;
end;
hence thesis;
end;
theorem ::
GROUP_4:42
for G be
strict
Group, a be
Element of G holds a
in (
Phi G) iff a is non
generating
proof
let G be
strict
Group, a be
Element of G;
thus a
in (
Phi G) implies a is non
generating
proof
assume a
in (
Phi G);
then a
in the
carrier of (
Phi G) by
STRUCT_0:def 5;
then a
in { b where b be
Element of G : b is non
generating } by
Th41;
then ex b be
Element of G st a
= b & b is non
generating;
hence thesis;
end;
assume a is non
generating;
then a
in { b where b be
Element of G : b is non
generating };
then a
in the
carrier of (
Phi G) by
Th41;
hence thesis by
STRUCT_0:def 5;
end;
definition
let G, H1, H2;
::
GROUP_4:def8
func H1
* H2 ->
Subset of G equals ((
carr H1)
* (
carr H2));
correctness ;
end
theorem ::
GROUP_4:43
(H1
* H2)
= ((
carr H1)
* (
carr H2)) & (H1
* H2)
= (H1
* (
carr H2)) & (H1
* H2)
= ((
carr H1)
* H2);
theorem ::
GROUP_4:44
((H1
* H2)
* H3)
= (H1
* (H2
* H3))
proof
thus ((H1
* H2)
* H3)
= ((
carr H1)
* ((
carr H2)
* H3)) by
GROUP_2: 96
.= (H1
* (H2
* H3));
end;
theorem ::
GROUP_4:45
((a
* H1)
* H2)
= (a
* (H1
* H2))
proof
thus ((a
* H1)
* H2)
= (a
* ((
carr H1)
* H2)) by
GROUP_2: 96
.= (a
* (H1
* H2));
end;
theorem ::
GROUP_4:46
((H1
* H2)
* a)
= (H1
* (H2
* a))
proof
thus ((H1
* H2)
* a)
= ((H1
* (
carr H2))
* a)
.= (H1
* (H2
* a)) by
GROUP_2: 98;
end;
theorem ::
GROUP_4:47
((A
* H1)
* H2)
= (A
* (H1
* H2))
proof
thus ((A
* H1)
* H2)
= (A
* (H1
* (
carr H2))) by
GROUP_2: 99
.= (A
* (H1
* H2));
end;
theorem ::
GROUP_4:48
((H1
* H2)
* A)
= (H1
* (H2
* A))
proof
thus ((H1
* H2)
* A)
= ((H1
* (
carr H2))
* A)
.= (H1
* (H2
* A)) by
GROUP_2: 98;
end;
definition
let G, H1, H2;
::
GROUP_4:def9
func H1
"\/" H2 ->
strict
Subgroup of G equals (
gr ((
carr H1)
\/ (
carr H2)));
correctness ;
end
theorem ::
GROUP_4:49
a
in (H1
"\/" H2) iff ex F, I st (
len F)
= (
len I) & (
rng F)
c= ((
carr H1)
\/ (
carr H2)) & a
= (
Product (F
|^ I)) by
Th28;
theorem ::
GROUP_4:50
(H1
"\/" H2)
= (
gr (H1
* H2))
proof
set H = (
gr ((
carr H1)
* (
carr H2)));
now
let a;
assume a
in H;
then
consider F, I such that
A1: (
len F)
= (
len I) and
A2: (
rng F)
c= ((
carr H1)
* (
carr H2)) and
A3: a
= (
Product (F
|^ I)) by
Th28;
(
rng (F
|^ I))
c= (
carr (H1
"\/" H2))
proof
set f = (F
|^ I);
let x be
object;
A4: (
rng I)
c=
INT by
FINSEQ_1:def 4;
assume x
in (
rng f);
then
consider y be
object such that
A5: y
in (
dom f) and
A6: (f
. y)
= x by
FUNCT_1:def 3;
reconsider y as
Element of
NAT by
A5;
A7: (
len f)
= (
len F) by
Def3;
then
A8: y
in (
dom I) by
A1,
A5,
FINSEQ_3: 29;
then
A9: (I
/. y)
= (I
. y) by
PARTFUN1:def 6;
(I
. y)
in (
rng I) by
A8,
FUNCT_1:def 3;
then
reconsider i = (I
. y) as
Integer by
A4;
A10: (
@ (I
/. y))
= (I
/. y);
y
in (
dom F) by
A5,
A7,
FINSEQ_3: 29;
then (F
/. y)
= (F
. y) & (F
. y)
in (
rng F) by
FUNCT_1:def 3,
PARTFUN1:def 6;
then
consider b, c such that
A11: (F
/. y)
= (b
* c) and
A12: b
in (
carr H1) and
A13: c
in (
carr H2) by
A2,
GROUP_2: 8;
y
in (
dom F) by
A5,
A7,
FINSEQ_3: 29;
then
A14: x
= ((F
/. y)
|^ i) by
A6,
A9,
A10,
Def3;
now
per cases ;
suppose i
>=
0 ;
then
reconsider n = i as
Element of
NAT by
INT_1: 3;
defpred
P[
Nat,
object] means (($1
mod 2)
= 1 implies $2
= b) & (($1
mod 2)
=
0 implies $2
= c);
A15: for k be
Nat st k
in (
Seg (2
* n)) holds ex x be
object st
P[k, x]
proof
let k be
Nat;
assume k
in (
Seg (2
* n));
now
per cases by
NAT_D: 12;
suppose
A16: (k
mod 2)
= 1;
reconsider x = b as
set;
take x;
thus ((k
mod 2)
= 1 implies x
= b) & ((k
mod 2)
=
0 implies x
= c) by
A16;
end;
suppose
A17: (k
mod 2)
=
0 ;
reconsider x = c as
set;
take x;
thus ((k
mod 2)
= 1 implies x
= b) & ((k
mod 2)
=
0 implies x
= c) by
A17;
end;
end;
hence thesis;
end;
consider p be
FinSequence such that
A18: (
dom p)
= (
Seg (2
* n)) and
A19: for k be
Nat st k
in (
Seg (2
* n)) holds
P[k, (p
. k)] from
FINSEQ_1:sch 1(
A15);
A20: (
len p)
= (2
* n) by
A18,
FINSEQ_1:def 3;
A21: (
rng p)
c=
{b, c}
proof
let x be
object;
assume x
in (
rng p);
then
consider y be
object such that
A22: y
in (
dom p) and
A23: (p
. y)
= x by
FUNCT_1:def 3;
reconsider y as
Element of
NAT by
A22;
now
per cases by
NAT_D: 12;
suppose (y
mod 2)
=
0 ;
then x
= c by
A18,
A19,
A22,
A23;
hence thesis by
TARSKI:def 2;
end;
suppose (y
mod 2)
= 1;
then x
= b by
A18,
A19,
A22,
A23;
hence thesis by
TARSKI:def 2;
end;
end;
hence thesis;
end;
then (
rng p)
c= the
carrier of G by
XBOOLE_1: 1;
then
reconsider p as
FinSequence of the
carrier of G by
FINSEQ_1:def 4;
A24: ((
carr H1)
\/ (
carr H2))
c= the
carrier of (
gr ((
carr H1)
\/ (
carr H2))) & (
carr (
gr ((
carr H1)
\/ (
carr H2))))
= the
carrier of (
gr ((
carr H1)
\/ (
carr H2))) by
Def4;
defpred
Q[
Nat] means $1
<= (2
* n) & ($1
mod 2)
=
0 implies for F1 st F1
= (p
| (
Seg $1)) holds (
Product F1)
= ((F
/. y)
|^ ($1
div 2));
A25: for k be
Nat st for l be
Nat st l
< k holds
Q[l] holds
Q[k]
proof
let k be
Nat;
assume
A26: for l be
Nat st l
< k holds
Q[l];
assume that
A27: k
<= (2
* n) and
A28: (k
mod 2)
=
0 ;
let F1;
assume
A29: F1
= (p
| (
Seg k));
now
per cases ;
suppose
A30: k
=
0 ;
(2
*
0 )
=
0 ;
then
A31: (
0
div 2)
=
0 by
NAT_D: 18;
F1
= (
<*> the
carrier of G) by
A29,
A30;
then (
Product F1)
= (
1_ G) by
Th8;
hence thesis by
A30,
A31,
GROUP_1: 25;
end;
suppose
A32: k
<>
0 ;
A33: k
<> 1 by
A28,
NAT_D: 14;
k
>= 1 by
A32,
NAT_1: 14;
then k
> 1 by
A33,
XXREAL_0: 1;
then k
>= (1
+ 1) by
NAT_1: 13;
then (k
- 2)
>= (2
- 2) by
XREAL_1: 9;
then
reconsider m = (k
- 2) as
Element of
NAT by
INT_1: 3;
reconsider q = (p
| (
Seg m)) as
FinSequence of the
carrier of G by
FINSEQ_1: 18;
(1
* 2)
= 2;
then
A34: (m
mod 2)
=
0 by
A28,
NAT_D: 15;
A35: (m
+ 2)
= k;
then
A36: m
<= (2
* n) by
A27,
NAT_1: 16,
XXREAL_0: 2;
then ex o be
Nat st (2
* n)
= (m
+ o) by
NAT_1: 10;
then
A37: (
len q)
= m by
A20,
FINSEQ_3: 53;
A38: ex j be
Nat st (2
* n)
= (k
+ j) by
A27,
NAT_1: 10;
then
A39: (
len F1)
= k by
A20,
A29,
FINSEQ_3: 53;
A40:
now
let l;
assume
A41: l
in (
dom q);
then l
<= (
len q) by
FINSEQ_3: 25;
then
A42: l
<= (
len F1) by
A35,
A39,
A37,
NAT_1: 16,
XXREAL_0: 2;
1
<= l by
A41,
FINSEQ_3: 25;
then l
in (
dom F1) by
A42,
FINSEQ_3: 25;
then (F1
. l)
= (p
. l) by
A29,
FUNCT_1: 47;
hence (F1
. l)
= (q
. l) by
A41,
FUNCT_1: 47;
end;
A43: m
< k by
A35,
NAT_1: 16;
then
A44: (
Product q)
= ((F
/. y)
|^ (m
div 2)) by
A26,
A36,
A34;
A45:
now
let l;
assume l
in (
dom
<*b, c*>);
then
A46: l
in
{1, 2} by
FINSEQ_1: 2,
FINSEQ_1: 89;
now
per cases by
A46,
TARSKI:def 2;
suppose
A47: l
= 1;
then
A48: (
<*b, c*>
. l)
= b by
FINSEQ_1: 44;
A49: ((m
+ 1)
mod 2)
= 1 & (
dom F1)
c= (
dom p) by
A29,
A34,
NAT_D: 16,
RELAT_1: 60;
(m
+ 1)
<= k & 1
<= (m
+ 1) by
A43,
NAT_1: 12,
NAT_1: 13;
then
A50: (m
+ 1)
in (
dom F1) by
A39,
FINSEQ_3: 25;
then (F1
. ((
len q)
+ l))
= (p
. (m
+ 1)) by
A29,
A37,
A47,
FUNCT_1: 47;
hence (F1
. ((
len q)
+ l))
= (
<*b, c*>
. l) by
A18,
A19,
A48,
A50,
A49;
end;
suppose
A51: l
= 2;
then
A52: (
<*b, c*>
. l)
= c by
FINSEQ_1: 44;
A53: (
dom F1)
c= (
dom p) by
A29,
RELAT_1: 60;
1
<= (m
+ (1
+ 1)) by
NAT_1: 12;
then
A54: (m
+ 2)
in (
dom F1) by
A39,
FINSEQ_3: 25;
then (F1
. ((
len q)
+ l))
= (p
. (m
+ 2)) by
A29,
A37,
A51,
FUNCT_1: 47;
hence (F1
. ((
len q)
+ l))
= (
<*b, c*>
. l) by
A18,
A19,
A28,
A52,
A54,
A53;
end;
end;
hence (F1
. ((
len q)
+ l))
= (
<*b, c*>
. l);
end;
A55: ((m
div (2
* 1))
+ 1)
= ((m
div 2)
+ (2
div 2)) by
NAT_D: 18
.= (k
div 2) by
A35,
A34,
NAT_D: 19;
(
len F1)
= (m
+ 2) by
A20,
A29,
A38,
FINSEQ_3: 53
.= ((
len q)
+ (
len
<*b, c*>)) by
A37,
FINSEQ_1: 44;
then F1
= (q
^
<*b, c*>) by
A40,
A45,
FINSEQ_3: 38;
then (
Product F1)
= ((
Product q)
* (
Product
<*b, c*>)) by
FINSOP_1: 5
.= ((
Product q)
* (F
/. y)) by
A11,
FINSOP_1: 12
.= ((F
/. y)
|^ ((m
div 2)
+ 1)) by
A44,
GROUP_1: 34;
hence thesis by
A55;
end;
end;
hence thesis;
end;
A56: for k be
Nat holds
Q[k] from
NAT_1:sch 4(
A25);
b
in ((
carr H1)
\/ (
carr H2)) & c
in ((
carr H1)
\/ (
carr H2)) by
A12,
A13,
XBOOLE_0:def 3;
then
{b, c}
c= ((
carr H1)
\/ (
carr H2)) by
ZFMISC_1: 32;
then
A57: (
rng p)
c= ((
carr H1)
\/ (
carr H2)) by
A21;
(
len p)
= (2
* n) by
A18,
FINSEQ_1:def 3;
then
A58: p
= (p
| (
Seg (2
* n))) by
FINSEQ_3: 49;
((2
* n)
mod 2)
=
0 & ((2
* n)
div 2)
= n by
NAT_D: 13,
NAT_D: 18;
then x
= (
Product p) by
A14,
A56,
A58;
then x
in (
gr ((
carr H1)
\/ (
carr H2))) by
A57,
A24,
Th18,
XBOOLE_1: 1;
hence thesis by
STRUCT_0:def 5;
end;
suppose
A59: i
<
0 ;
defpred
P[
Nat,
object] means (($1
mod 2)
= 1 implies $2
= (c
" )) & (($1
mod 2)
=
0 implies $2
= (b
" ));
set n =
|.i.|;
A60: ((2
* n)
mod 2)
=
0 & ((2
* n)
div 2)
= n by
NAT_D: 13,
NAT_D: 18;
A61: for k be
Nat st k
in (
Seg (2
* n)) holds ex x be
object st
P[k, x]
proof
let k be
Nat;
assume k
in (
Seg (2
* n));
now
per cases by
NAT_D: 12;
suppose
A62: (k
mod 2)
= 1;
reconsider x = (c
" ) as
set;
take x;
thus ((k
mod 2)
= 1 implies x
= (c
" )) & ((k
mod 2)
=
0 implies x
= (b
" )) by
A62;
end;
suppose
A63: (k
mod 2)
=
0 ;
reconsider x = (b
" ) as
set;
take x;
thus ((k
mod 2)
= 1 implies x
= (c
" )) & ((k
mod 2)
=
0 implies x
= (b
" )) by
A63;
end;
end;
hence thesis;
end;
consider p be
FinSequence such that
A64: (
dom p)
= (
Seg (2
* n)) and
A65: for k be
Nat st k
in (
Seg (2
* n)) holds
P[k, (p
. k)] from
FINSEQ_1:sch 1(
A61);
A66: (
len p)
= (2
* n) by
A64,
FINSEQ_1:def 3;
A67: (
rng p)
c=
{(b
" ), (c
" )}
proof
let x be
object;
assume x
in (
rng p);
then
consider y be
object such that
A68: y
in (
dom p) and
A69: (p
. y)
= x by
FUNCT_1:def 3;
reconsider y as
Element of
NAT by
A68;
now
per cases by
NAT_D: 12;
suppose (y
mod 2)
=
0 ;
then x
= (b
" ) by
A64,
A65,
A68,
A69;
hence thesis by
TARSKI:def 2;
end;
suppose (y
mod 2)
= 1;
then x
= (c
" ) by
A64,
A65,
A68,
A69;
hence thesis by
TARSKI:def 2;
end;
end;
hence thesis;
end;
then (
rng p)
c= the
carrier of G by
XBOOLE_1: 1;
then
reconsider p as
FinSequence of the
carrier of G by
FINSEQ_1:def 4;
A70: ((
carr H1)
\/ (
carr H2))
c= the
carrier of (
gr ((
carr H1)
\/ (
carr H2))) & (
carr (
gr ((
carr H1)
\/ (
carr H2))))
= the
carrier of (
gr ((
carr H1)
\/ (
carr H2))) by
Def4;
defpred
Q[
Nat] means $1
<= (2
* n) & ($1
mod 2)
=
0 implies for F1 st F1
= (p
| (
Seg $1)) holds (
Product F1)
= (((F
/. y)
|^ ($1
div 2))
" );
A71: for k be
Nat st for l be
Nat st l
< k holds
Q[l] holds
Q[k]
proof
let k be
Nat;
assume
A72: for l be
Nat st l
< k holds
Q[l];
assume that
A73: k
<= (2
* n) and
A74: (k
mod 2)
=
0 ;
let F1;
assume
A75: F1
= (p
| (
Seg k));
now
per cases ;
suppose
A76: k
=
0 ;
(2
*
0 )
=
0 ;
then (
0
div 2)
=
0 by
NAT_D: 18;
then
A77: ((F
/. y)
|^ (k
div 2))
= (
1_ G) by
A76,
GROUP_1: 25;
F1
= (
<*> the
carrier of G) by
A75,
A76;
then (
Product F1)
= (
1_ G) by
Th8;
hence thesis by
A77,
GROUP_1: 8;
end;
suppose
A78: k
<>
0 ;
A79: k
<> 1 by
A74,
NAT_D: 14;
k
>= 1 by
A78,
NAT_1: 14;
then k
> 1 by
A79,
XXREAL_0: 1;
then k
>= (1
+ 1) by
NAT_1: 13;
then (k
- 2)
>= (2
- 2) by
XREAL_1: 9;
then
reconsider m = (k
- 2) as
Element of
NAT by
INT_1: 3;
reconsider q = (p
| (
Seg m)) as
FinSequence of the
carrier of G by
FINSEQ_1: 18;
(1
* 2)
= 2;
then
A80: (m
mod 2)
=
0 by
A74,
NAT_D: 15;
A81: (m
+ 2)
= k;
then
A82: m
<= (2
* n) by
A73,
NAT_1: 16,
XXREAL_0: 2;
then ex o be
Nat st (2
* n)
= (m
+ o) by
NAT_1: 10;
then
A83: (
len q)
= m by
A66,
FINSEQ_3: 53;
A84: ex j be
Nat st (2
* n)
= (k
+ j) by
A73,
NAT_1: 10;
then
A85: (
len F1)
= k by
A66,
A75,
FINSEQ_3: 53;
A86:
now
let l;
assume
A87: l
in (
dom q);
then l
<= (
len q) by
FINSEQ_3: 25;
then
A88: l
<= (
len F1) by
A81,
A85,
A83,
NAT_1: 16,
XXREAL_0: 2;
1
<= l by
A87,
FINSEQ_3: 25;
then l
in (
dom F1) by
A88,
FINSEQ_3: 25;
then (F1
. l)
= (p
. l) by
A75,
FUNCT_1: 47;
hence (F1
. l)
= (q
. l) by
A87,
FUNCT_1: 47;
end;
A89: m
< k by
A81,
NAT_1: 16;
then
A90: (
Product q)
= (((F
/. y)
|^ (m
div 2))
" ) by
A72,
A82,
A80;
A91:
now
let l;
assume l
in (
dom
<*(c
" ), (b
" )*>);
then
A92: l
in
{1, 2} by
FINSEQ_1: 2,
FINSEQ_1: 89;
now
per cases by
A92,
TARSKI:def 2;
suppose
A93: l
= 1;
then
A94: (
<*(c
" ), (b
" )*>
. l)
= (c
" ) by
FINSEQ_1: 44;
A95: ((m
+ 1)
mod 2)
= 1 & (
dom F1)
c= (
dom p) by
A75,
A80,
NAT_D: 16,
RELAT_1: 60;
(m
+ 1)
<= k & 1
<= (m
+ 1) by
A89,
NAT_1: 12,
NAT_1: 13;
then
A96: (m
+ 1)
in (
dom F1) by
A85,
FINSEQ_3: 25;
then (F1
. ((
len q)
+ l))
= (p
. (m
+ 1)) by
A75,
A83,
A93,
FUNCT_1: 47;
hence (F1
. ((
len q)
+ l))
= (
<*(c
" ), (b
" )*>
. l) by
A64,
A65,
A94,
A96,
A95;
end;
suppose
A97: l
= 2;
then
A98: (
<*(c
" ), (b
" )*>
. l)
= (b
" ) by
FINSEQ_1: 44;
A99: (
dom F1)
c= (
dom p) by
A75,
RELAT_1: 60;
1
<= (m
+ (1
+ 1)) by
NAT_1: 12;
then
A100: (m
+ 2)
in (
dom F1) by
A85,
FINSEQ_3: 25;
then (F1
. ((
len q)
+ l))
= (p
. (m
+ 2)) by
A75,
A83,
A97,
FUNCT_1: 47;
hence (F1
. ((
len q)
+ l))
= (
<*(c
" ), (b
" )*>
. l) by
A64,
A65,
A74,
A98,
A100,
A99;
end;
end;
hence (F1
. ((
len q)
+ l))
= (
<*(c
" ), (b
" )*>
. l);
end;
A101: ((m
div (2
* 1))
+ 1)
= ((m
div 2)
+ (2
div 2)) by
NAT_D: 18
.= (k
div 2) by
A81,
A80,
NAT_D: 19;
(
len F1)
= (m
+ 2) by
A66,
A75,
A84,
FINSEQ_3: 53
.= ((
len q)
+ (
len
<*(c
" ), (b
" )*>)) by
A83,
FINSEQ_1: 44;
then F1
= (q
^
<*(c
" ), (b
" )*>) by
A86,
A91,
FINSEQ_3: 38;
then (
Product F1)
= ((
Product q)
* (
Product
<*(c
" ), (b
" )*>)) by
FINSOP_1: 5
.= ((
Product q)
* ((c
" )
* (b
" ))) by
FINSOP_1: 12
.= ((
Product q)
* ((F
/. y)
" )) by
A11,
GROUP_1: 17
.= (((F
/. y)
* ((F
/. y)
|^ (m
div 2)))
" ) by
A90,
GROUP_1: 17
.= (((F
/. y)
|^ ((m
div 2)
+ 1))
" ) by
GROUP_1: 34;
hence thesis by
A101;
end;
end;
hence thesis;
end;
A102: for k be
Nat holds
Q[k] from
NAT_1:sch 4(
A71);
(c
" )
in (
carr H2) by
A13,
GROUP_2: 75;
then
A103: (c
" )
in ((
carr H1)
\/ (
carr H2)) by
XBOOLE_0:def 3;
(
len p)
= (2
* n) by
A64,
FINSEQ_1:def 3;
then
A104: p
= (p
| (
Seg (2
* n))) by
FINSEQ_3: 49;
(b
" )
in (
carr H1) by
A12,
GROUP_2: 75;
then (b
" )
in ((
carr H1)
\/ (
carr H2)) by
XBOOLE_0:def 3;
then
{(b
" ), (c
" )}
c= ((
carr H1)
\/ (
carr H2)) by
A103,
ZFMISC_1: 32;
then
A105: (
rng p)
c= ((
carr H1)
\/ (
carr H2)) by
A67;
x
= (((F
/. y)
|^ n)
" ) by
A14,
A59,
GROUP_1: 30;
then x
= (
Product p) by
A102,
A60,
A104;
then x
in (
gr ((
carr H1)
\/ (
carr H2))) by
A105,
A70,
Th18,
XBOOLE_1: 1;
hence thesis by
STRUCT_0:def 5;
end;
end;
hence thesis;
end;
hence a
in (H1
"\/" H2) by
A3,
Th18;
end;
then
A106: H is
Subgroup of (H1
"\/" H2) by
GROUP_2: 58;
((
carr H1)
\/ (
carr H2))
c= ((
carr H1)
* (
carr H2))
proof
let x be
object;
assume
A107: x
in ((
carr H1)
\/ (
carr H2));
then
reconsider a = x as
Element of G;
now
per cases by
A107,
XBOOLE_0:def 3;
suppose
A108: x
in (
carr H1);
(
1_ G)
in H2 by
GROUP_2: 46;
then
A109: (
1_ G)
in (
carr H2) by
STRUCT_0:def 5;
(a
* (
1_ G))
= a by
GROUP_1:def 4;
hence thesis by
A108,
A109;
end;
suppose
A110: x
in (
carr H2);
(
1_ G)
in H1 by
GROUP_2: 46;
then
A111: (
1_ G)
in (
carr H1) by
STRUCT_0:def 5;
((
1_ G)
* a)
= a by
GROUP_1:def 4;
hence thesis by
A110,
A111;
end;
end;
hence thesis;
end;
then (H1
"\/" H2) is
Subgroup of H by
Th32;
hence (
gr (H1
* H2))
= (H1
"\/" H2) by
A106,
GROUP_2: 55;
end;
theorem ::
GROUP_4:51
Th51: (H1
* H2)
= (H2
* H1) implies the
carrier of (H1
"\/" H2)
= (H1
* H2)
proof
assume (H1
* H2)
= (H2
* H1);
then
consider H be
strict
Subgroup of G such that
A1: the
carrier of H
= ((
carr H1)
* (
carr H2)) by
GROUP_2: 78;
now
reconsider p = 1 as
Integer;
let a;
assume a
in H;
then a
in ((
carr H1)
* (
carr H2)) by
A1,
STRUCT_0:def 5;
then
consider b, c such that
A2: a
= (b
* c) and
A3: b
in (
carr H1) & c
in (
carr H2);
b
in ((
carr H1)
\/ (
carr H2)) & c
in ((
carr H1)
\/ (
carr H2)) by
A3,
XBOOLE_0:def 3;
then
A4: (
rng
<*b, c*>)
=
{b, c} &
{b, c}
c= ((
carr H1)
\/ (
carr H2)) by
FINSEQ_2: 127,
ZFMISC_1: 32;
A5: (
len
<*b, c*>)
= 2 & (
len
<*(
@ p), (
@ p)*>)
= 2 by
FINSEQ_1: 44;
a
= ((
Product
<*b*>)
* c) by
A2,
FINSOP_1: 11
.= ((
Product
<*b*>)
* (
Product
<*c*>)) by
FINSOP_1: 11
.= (
Product (
<*b*>
^
<*c*>)) by
FINSOP_1: 5
.= (
Product
<*b, c*>) by
FINSEQ_1:def 9
.= (
Product
<*(b
|^ p), c*>) by
GROUP_1: 26
.= (
Product
<*(b
|^ p), (c
|^ p)*>) by
GROUP_1: 26
.= (
Product (
<*b, c*>
|^
<*(
@ p), (
@ p)*>)) by
Th23;
hence a
in (H1
"\/" H2) by
A5,
A4,
Th28;
end;
then
A6: H is
Subgroup of (H1
"\/" H2) by
GROUP_2: 58;
((
carr H1)
\/ (
carr H2))
c= ((
carr H1)
* (
carr H2))
proof
let x be
object;
assume
A7: x
in ((
carr H1)
\/ (
carr H2));
then
reconsider a = x as
Element of G;
now
per cases by
A7,
XBOOLE_0:def 3;
suppose
A8: x
in (
carr H1);
(
1_ G)
in H2 by
GROUP_2: 46;
then
A9: (
1_ G)
in (
carr H2) by
STRUCT_0:def 5;
(a
* (
1_ G))
= a by
GROUP_1:def 4;
hence thesis by
A8,
A9;
end;
suppose
A10: x
in (
carr H2);
(
1_ G)
in H1 by
GROUP_2: 46;
then
A11: (
1_ G)
in (
carr H1) by
STRUCT_0:def 5;
((
1_ G)
* a)
= a by
GROUP_1:def 4;
hence thesis by
A10,
A11;
end;
end;
hence thesis;
end;
then (H1
"\/" H2) is
Subgroup of H by
A1,
Def4;
hence thesis by
A1,
A6,
GROUP_2: 55;
end;
theorem ::
GROUP_4:52
G is
commutative
Group implies the
carrier of (H1
"\/" H2)
= (H1
* H2)
proof
assume G is
commutative
Group;
then (H1
* H2)
= (H2
* H1) by
GROUP_2: 25;
hence thesis by
Th51;
end;
theorem ::
GROUP_4:53
Th53: for N1,N2 be
strict
normal
Subgroup of G holds the
carrier of (N1
"\/" N2)
= (N1
* N2)
proof
let N1,N2 be
strict
normal
Subgroup of G;
(N1
* N2)
= (N2
* N1) by
GROUP_3: 125;
hence thesis by
Th51;
end;
theorem ::
GROUP_4:54
for N1,N2 be
strict
normal
Subgroup of G holds (N1
"\/" N2) is
normal
Subgroup of G
proof
let N1,N2 be
strict
normal
Subgroup of G;
(ex N be
strict
normal
Subgroup of G st the
carrier of N
= ((
carr N1)
* (
carr N2))) & the
carrier of (N1
"\/" N2)
= (N1
* N2) by
Th53,
GROUP_3: 126;
hence thesis by
GROUP_2: 59;
end;
theorem ::
GROUP_4:55
for H be
strict
Subgroup of G holds (H
"\/" H)
= H by
Th31;
theorem ::
GROUP_4:56
(H1
"\/" H2)
= (H2
"\/" H1);
Lm4: H1 is
Subgroup of (H1
"\/" H2)
proof
(
carr H1)
c= ((
carr H1)
\/ (
carr H2)) & ((
carr H1)
\/ (
carr H2))
c= the
carrier of (
gr ((
carr H1)
\/ (
carr H2))) by
Def4,
XBOOLE_1: 7;
hence thesis by
GROUP_2: 57,
XBOOLE_1: 1;
end;
Lm5: ((H1
"\/" H2)
"\/" H3) is
Subgroup of (H1
"\/" (H2
"\/" H3))
proof
now
let a;
assume a
in ((H1
"\/" H2)
"\/" H3);
then
consider F, I such that
A1: (
len F)
= (
len I) and
A2: (
rng F)
c= ((
carr (H1
"\/" H2))
\/ (
carr H3)) and
A3: a
= (
Product (F
|^ I)) by
Th28;
(
rng F)
c= (
carr (
gr ((
carr H1)
\/ (
carr (H2
"\/" H3)))))
proof
let x be
object;
assume
A4: x
in (
rng F);
now
per cases by
A2,
A4,
XBOOLE_0:def 3;
suppose
A5: x
in (
carr (H1
"\/" H2));
then
reconsider b = x as
Element of G;
x
in (H1
"\/" H2) by
A5,
STRUCT_0:def 5;
then
consider F1, I1 such that
A6: (
len F1)
= (
len I1) and
A7: (
rng F1)
c= ((
carr H1)
\/ (
carr H2)) and
A8: b
= (
Product (F1
|^ I1)) by
Th28;
H2 is
Subgroup of (H2
"\/" H3) by
Lm4;
then the
carrier of H2
c= the
carrier of (H2
"\/" H3) by
GROUP_2:def 5;
then ((
carr H1)
\/ (
carr H2))
c= ((
carr H1)
\/ (
carr (H2
"\/" H3))) by
XBOOLE_1: 9;
then (
rng F1)
c= ((
carr H1)
\/ (
carr (H2
"\/" H3))) by
A7;
then b
in (H1
"\/" (H2
"\/" H3)) by
A6,
A8,
Th28;
hence thesis by
STRUCT_0:def 5;
end;
suppose
A9: x
in (
carr H3);
A10: H3 is
Subgroup of (H3
"\/" H2) by
Lm4;
x
in H3 by
A9,
STRUCT_0:def 5;
then x
in (H3
"\/" H2) by
A10,
GROUP_2: 40;
then x
in (
carr (H2
"\/" H3)) by
STRUCT_0:def 5;
then
A11: x
in ((
carr H1)
\/ (
carr (H2
"\/" H3))) by
XBOOLE_0:def 3;
((
carr H1)
\/ (
carr (H2
"\/" H3)))
c= the
carrier of (
gr ((
carr H1)
\/ (
carr (H2
"\/" H3)))) by
Def4;
hence thesis by
A11;
end;
end;
hence thesis;
end;
then a
in (
gr (
carr (
gr ((
carr H1)
\/ (
carr (H2
"\/" H3)))))) by
A1,
A3,
Th28;
hence a
in (H1
"\/" (H2
"\/" H3)) by
Th31;
end;
hence thesis by
GROUP_2: 58;
end;
theorem ::
GROUP_4:57
Th57: ((H1
"\/" H2)
"\/" H3)
= (H1
"\/" (H2
"\/" H3))
proof
((H2
"\/" H3)
"\/" H1) is
Subgroup of (H2
"\/" (H3
"\/" H1)) & ((H3
"\/" H1)
"\/" H2) is
Subgroup of (H3
"\/" (H1
"\/" H2)) by
Lm5;
then
A1: (H1
"\/" (H2
"\/" H3)) is
Subgroup of (H3
"\/" (H1
"\/" H2)) by
GROUP_2: 56;
((H1
"\/" H2)
"\/" H3) is
Subgroup of (H1
"\/" (H2
"\/" H3)) by
Lm5;
hence thesis by
A1,
GROUP_2: 55;
end;
theorem ::
GROUP_4:58
for H be
strict
Subgroup of G holds ((
(1). G)
"\/" H)
= H & (H
"\/" (
(1). G))
= H
proof
let H be
strict
Subgroup of G;
(
1_ G)
in H by
GROUP_2: 46;
then (
1_ G)
in (
carr H) by
STRUCT_0:def 5;
then
{(
1_ G)}
c= (
carr H) by
ZFMISC_1: 31;
then
A1: (
carr (
(1). G))
=
{(
1_ G)} & (
{(
1_ G)}
\/ (
carr H))
= (
carr H) by
GROUP_2:def 7,
XBOOLE_1: 12;
hence ((
(1). G)
"\/" H)
= H by
Th31;
thus thesis by
A1,
Th31;
end;
theorem ::
GROUP_4:59
Th59: ((
(Omega). G)
"\/" H)
= (
(Omega). G) & (H
"\/" (
(Omega). G))
= (
(Omega). G)
proof
A1: (the
carrier of (
(Omega). G)
\/ (
carr H))
= (
[#] the
carrier of G) by
SUBSET_1: 11;
hence ((
(Omega). G)
"\/" H)
= (
(Omega). G) by
Th31;
thus thesis by
A1,
Th31;
end;
theorem ::
GROUP_4:60
Th60: H1 is
Subgroup of (H1
"\/" H2) & H2 is
Subgroup of (H1
"\/" H2)
proof
(H1
"\/" H2)
= (H2
"\/" H1);
hence thesis by
Lm4;
end;
theorem ::
GROUP_4:61
Th61: for H2 be
strict
Subgroup of G holds H1 is
Subgroup of H2 iff (H1
"\/" H2)
= H2
proof
let H2 be
strict
Subgroup of G;
thus H1 is
Subgroup of H2 implies (H1
"\/" H2)
= H2
proof
assume H1 is
Subgroup of H2;
then the
carrier of H1
c= the
carrier of H2 by
GROUP_2:def 5;
hence (H1
"\/" H2)
= (
gr (
carr H2)) by
XBOOLE_1: 12
.= H2 by
Th31;
end;
thus thesis by
Th60;
end;
theorem ::
GROUP_4:62
H1 is
Subgroup of H2 implies H1 is
Subgroup of (H2
"\/" H3)
proof
H2 is
Subgroup of (H2
"\/" H3) by
Th60;
hence thesis by
GROUP_2: 56;
end;
theorem ::
GROUP_4:63
for H3 be
strict
Subgroup of G holds H1 is
Subgroup of H3 & H2 is
Subgroup of H3 implies (H1
"\/" H2) is
Subgroup of H3
proof
let H3 be
strict
Subgroup of G;
assume
A1: H1 is
Subgroup of H3 & H2 is
Subgroup of H3;
now
let a;
assume a
in (H1
"\/" H2);
then
consider F, I such that
A2: (
len F)
= (
len I) and
A3: (
rng F)
c= ((
carr H1)
\/ (
carr H2)) and
A4: a
= (
Product (F
|^ I)) by
Th28;
the
carrier of H1
c= the
carrier of H3 & the
carrier of H2
c= the
carrier of H3 by
A1,
GROUP_2:def 5;
then ((
carr H1)
\/ (
carr H2))
c= (
carr H3) by
XBOOLE_1: 8;
then (
rng F)
c= (
carr H3) by
A3;
then a
in (
gr (
carr H3)) by
A2,
A4,
Th28;
hence a
in H3 by
Th31;
end;
hence thesis by
GROUP_2: 58;
end;
theorem ::
GROUP_4:64
for H3,H2 be
strict
Subgroup of G holds H1 is
Subgroup of H2 implies (H1
"\/" H3) is
Subgroup of (H2
"\/" H3)
proof
let H3,H2 be
strict
Subgroup of G;
assume
A1: H1 is
Subgroup of H2;
((H1
"\/" H3)
"\/" (H2
"\/" H3))
= (((H1
"\/" H3)
"\/" H2)
"\/" H3) by
Th57
.= ((H1
"\/" (H3
"\/" H2))
"\/" H3) by
Th57
.= ((H1
"\/" (H2
"\/" H3))
"\/" H3)
.= (((H1
"\/" H2)
"\/" H3)
"\/" H3) by
Th57
.= ((H2
"\/" H3)
"\/" H3) by
A1,
Th61
.= (H2
"\/" (H3
"\/" H3)) by
Th57
.= (H2
"\/" H3) by
Th31;
hence thesis by
Th61;
end;
theorem ::
GROUP_4:65
(H1
/\ H2) is
Subgroup of (H1
"\/" H2)
proof
(H1
/\ H2) is
Subgroup of H1 & H1 is
Subgroup of (H1
"\/" H2) by
Th60,
GROUP_2: 88;
hence thesis by
GROUP_2: 56;
end;
theorem ::
GROUP_4:66
Th66: for H2 be
strict
Subgroup of G holds ((H1
/\ H2)
"\/" H2)
= H2
proof
let H2 be
strict
Subgroup of G;
(H1
/\ H2) is
Subgroup of H2 by
GROUP_2: 88;
hence thesis by
Th61;
end;
theorem ::
GROUP_4:67
Th67: for H1 be
strict
Subgroup of G holds (H1
/\ (H1
"\/" H2))
= H1
proof
let H1 be
strict
Subgroup of G;
H1 is
Subgroup of (H1
"\/" H2) by
Th60;
hence thesis by
GROUP_2: 89;
end;
theorem ::
GROUP_4:68
for H1,H2 be
strict
Subgroup of G holds (H1
"\/" H2)
= H2 iff (H1
/\ H2)
= H1
proof
let H1,H2 be
strict
Subgroup of G;
(H1
"\/" H2)
= H2 iff H1 is
Subgroup of H2 by
Th61;
hence thesis by
GROUP_2: 89;
end;
reserve S1,S2 for
Element of (
Subgroups G);
definition
let G;
::
GROUP_4:def10
func
SubJoin G ->
BinOp of (
Subgroups G) means
:
Def10: for H1,H2 be
strict
Subgroup of G holds (it
. (H1,H2))
= (H1
"\/" H2);
existence
proof
defpred
P[
set,
set,
set] means for H1, H2 st $1
= H1 & $2
= H2 holds $3
= (H1
"\/" H2);
A1: for S1, S2 holds ex B be
Element of (
Subgroups G) st
P[S1, S2, B]
proof
let S1, S2;
reconsider H1 = S1, H2 = S2 as
Subgroup of G by
GROUP_3:def 1;
reconsider C = (H1
"\/" H2) as
Element of (
Subgroups G) by
GROUP_3:def 1;
take C;
thus thesis;
end;
consider o be
BinOp of (
Subgroups G) such that
A2: for a,b be
Element of (
Subgroups G) holds
P[a, b, (o
. (a,b))] from
BINOP_1:sch 3(
A1);
take o;
let H1,H2 be
strict
Subgroup of G;
H1
in (
Subgroups G) & H2
in (
Subgroups G) by
GROUP_3:def 1;
hence thesis by
A2;
end;
uniqueness
proof
let o1,o2 be
BinOp of (
Subgroups G);
assume that
A3: for H1,H2 be
strict
Subgroup of G holds (o1
. (H1,H2))
= (H1
"\/" H2) and
A4: for H1,H2 be
strict
Subgroup of G holds (o2
. (H1,H2))
= (H1
"\/" H2);
now
let x,y be
set;
assume
A5: x
in (
Subgroups G) & y
in (
Subgroups G);
then
reconsider A = x, B = y as
Element of (
Subgroups G);
reconsider H1 = x, H2 = y as
strict
Subgroup of G by
A5,
GROUP_3:def 1;
(o1
. (A,B))
= (H1
"\/" H2) by
A3;
hence (o1
. (x,y))
= (o2
. (x,y)) by
A4;
end;
hence thesis by
BINOP_1: 1;
end;
end
definition
let G;
::
GROUP_4:def11
func
SubMeet G ->
BinOp of (
Subgroups G) means
:
Def11: for H1,H2 be
strict
Subgroup of G holds (it
. (H1,H2))
= (H1
/\ H2);
existence
proof
defpred
P[
set,
set,
set] means for H1, H2 st $1
= H1 & $2
= H2 holds $3
= (H1
/\ H2);
A1: for S1, S2 holds ex B be
Element of (
Subgroups G) st
P[S1, S2, B]
proof
let S1, S2;
reconsider H1 = S1, H2 = S2 as
Subgroup of G by
GROUP_3:def 1;
reconsider C = (H1
/\ H2) as
Element of (
Subgroups G) by
GROUP_3:def 1;
take C;
thus thesis;
end;
consider o be
BinOp of (
Subgroups G) such that
A2: for a,b be
Element of (
Subgroups G) holds
P[a, b, (o
. (a,b))] from
BINOP_1:sch 3(
A1);
take o;
let H1,H2 be
strict
Subgroup of G;
H1
in (
Subgroups G) & H2
in (
Subgroups G) by
GROUP_3:def 1;
hence thesis by
A2;
end;
uniqueness
proof
let o1,o2 be
BinOp of (
Subgroups G);
assume that
A3: for H1,H2 be
strict
Subgroup of G holds (o1
. (H1,H2))
= (H1
/\ H2) and
A4: for H1,H2 be
strict
Subgroup of G holds (o2
. (H1,H2))
= (H1
/\ H2);
now
let x,y be
set;
assume
A5: x
in (
Subgroups G) & y
in (
Subgroups G);
then
reconsider A = x, B = y as
Element of (
Subgroups G);
reconsider H1 = x, H2 = y as
strict
Subgroup of G by
A5,
GROUP_3:def 1;
(o1
. (A,B))
= (H1
/\ H2) by
A3;
hence (o1
. (x,y))
= (o2
. (x,y)) by
A4;
end;
hence thesis by
BINOP_1: 1;
end;
end
Lm6:
LattStr (# (
Subgroups G), (
SubJoin G), (
SubMeet G) #) is
Lattice &
LattStr (# (
Subgroups G), (
SubJoin G), (
SubMeet G) #) is
0_Lattice &
LattStr (# (
Subgroups G), (
SubJoin G), (
SubMeet G) #) is
1_Lattice
proof
set L =
LattStr (# (
Subgroups G), (
SubJoin G), (
SubMeet G) #);
A1:
now
let A,B be
Element of L;
let H1,H2 be
strict
Subgroup of G;
assume
A2: A
= H1 & B
= H2;
thus (A
"\/" B)
= ((
SubJoin G)
. (A,B)) by
LATTICES:def 1
.= (H1
"\/" H2) by
A2,
Def10;
end;
A3:
now
let A,B be
Element of L;
let H1,H2 be
strict
Subgroup of G;
assume
A4: A
= H1 & B
= H2;
thus (A
"/\" B)
= ((
SubMeet G)
. (A,B)) by
LATTICES:def 2
.= (H1
/\ H2) by
A4,
Def11;
end;
now
let A,B,C be
Element of L;
reconsider H1 = A, H2 = B, H3 = C as
strict
Subgroup of G by
GROUP_3:def 1;
A5: (H2
"\/" H3)
= (B
"\/" C) by
A1;
thus (A
"\/" B)
= (H1
"\/" H2) by
A1
.= (H2
"\/" H1)
.= (B
"\/" A) by
A1;
A6: (H1
"\/" H2)
= (A
"\/" B) by
A1;
hence ((A
"\/" B)
"\/" C)
= ((H1
"\/" H2)
"\/" H3) by
A1
.= (H1
"\/" (H2
"\/" H3)) by
Th57
.= (A
"\/" (B
"\/" C)) by
A1,
A5;
A7: (H1
/\ H2)
= (A
"/\" B) by
A3;
hence ((A
"/\" B)
"\/" B)
= ((H1
/\ H2)
"\/" H2) by
A1
.= B by
Th66;
A8: (H2
/\ H3)
= (B
"/\" C) by
A3;
thus (A
"/\" B)
= (H2
/\ H1) by
A3
.= (B
"/\" A) by
A3;
thus ((A
"/\" B)
"/\" C)
= ((H1
/\ H2)
/\ H3) by
A3,
A7
.= (H1
/\ (H2
/\ H3)) by
GROUP_2: 84
.= (A
"/\" (B
"/\" C)) by
A3,
A8;
thus (A
"/\" (A
"\/" B))
= (H1
/\ (H1
"\/" H2)) by
A3,
A6
.= A by
Th67;
end;
then
A9: L is
join-commutative
join-associative
meet-absorbing
meet-commutative
meet-associative
join-absorbing by
LATTICES:def 4,
LATTICES:def 5,
LATTICES:def 6,
LATTICES:def 7,
LATTICES:def 8,
LATTICES:def 9;
hence L is
Lattice;
reconsider L as
Lattice by
A9;
reconsider E = (
(1). G) as
Element of L by
GROUP_3:def 1;
now
let A be
Element of L;
reconsider H = A as
strict
Subgroup of G by
GROUP_3:def 1;
thus (E
"/\" A)
= ((
(1). G)
/\ H) by
A3
.= E by
GROUP_2: 85;
hence (A
"/\" E)
= E;
end;
hence
LattStr (# (
Subgroups G), (
SubJoin G), (
SubMeet G) #) is
0_Lattice by
LATTICES:def 13;
reconsider F = (
(Omega). G) as
Element of L by
GROUP_3:def 1;
now
let A be
Element of L;
reconsider H = A as
strict
Subgroup of G by
GROUP_3:def 1;
thus (F
"\/" A)
= ((
(Omega). G)
"\/" H) by
A1
.= F by
Th59;
hence (A
"\/" F)
= F;
end;
hence thesis by
LATTICES:def 14;
end;
definition
let G be
Group;
::
GROUP_4:def12
func
lattice G ->
strict
Lattice equals
LattStr (# (
Subgroups G), (
SubJoin G), (
SubMeet G) #);
coherence by
Lm6;
end
theorem ::
GROUP_4:69
the
carrier of (
lattice G)
= (
Subgroups G);
theorem ::
GROUP_4:70
the
L_join of (
lattice G)
= (
SubJoin G);
theorem ::
GROUP_4:71
the
L_meet of (
lattice G)
= (
SubMeet G);
registration
let G be
Group;
cluster (
lattice G) ->
lower-bounded
upper-bounded;
coherence by
Lm6;
end
theorem ::
GROUP_4:72
(
Bottom (
lattice G))
= (
(1). G)
proof
set L = (
lattice G);
reconsider E = (
(1). G) as
Element of L by
GROUP_3:def 1;
now
let A be
Element of L;
reconsider H = A as
strict
Subgroup of G by
GROUP_3:def 1;
thus (A
"/\" E)
= ((
SubMeet G)
. (A,E)) by
LATTICES:def 2
.= (H
/\ (
(1). G)) by
Def11
.= E by
GROUP_2: 85;
end;
hence thesis by
RLSUB_2: 64;
end;
theorem ::
GROUP_4:73
(
Top (
lattice G))
= (
(Omega). G)
proof
set L = (
lattice G);
reconsider E = (
(Omega). G) as
Element of L by
GROUP_3:def 1;
now
let A be
Element of L;
reconsider H = A as
strict
Subgroup of G by
GROUP_3:def 1;
thus (A
"\/" E)
= ((
SubJoin G)
. (A,E)) by
LATTICES:def 1
.= (H
"\/" (
(Omega). G)) by
Def10
.= E by
Th59;
end;
hence thesis by
RLSUB_2: 65;
end;