set GP = product F;
set CF = Carrier F;
A1:
dom (Carrier F) = I
by PARTFUN1:def 2;
reconsider g = 1_ (product F) as Element of product (Carrier F) by Def2;
A2:
dom g = dom (Carrier F)
by CARD_3:9;
defpred S1[ object ] means ex J being finite Subset of I ex f being ManySortedSet of J st
( $1 = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) );
consider A being set such that
A3:
for x being object holds
( x in A iff ( x in product (Carrier F) & S1[x] ) )
from XBOOLE_0:sch 1();
A4:
A c= the carrier of (product F)
A5:
S1[g]
then reconsider A = A as non empty set by A3;
set b = the multF of (product F) || A;
A6:
for p being Element of product (Carrier F) holds dom p = I
by PARTFUN1:def 2;
( dom ( the multF of (product F) || A) = [:A,A:] & rng ( the multF of (product F) || A) c= A )
proof
dom the
multF of
(product F) = [: the carrier of (product F), the carrier of (product F):]
by FUNCT_2:def 1;
hence A7:
dom ( the multF of (product F) || A) = [:A,A:]
by A4, RELAT_1:62, ZFMISC_1:96;
rng ( the multF of (product F) || A) c= A
let y be
object ;
TARSKI:def 3 ( not y in rng ( the multF of (product F) || A) or y in A )
assume
y in rng ( the multF of (product F) || A)
;
y in A
then consider x being
object such that A8:
x in dom ( the multF of (product F) || A)
and A9:
( the multF of (product F) || A) . x = y
by FUNCT_1:def 3;
consider x1,
x2 being
object such that A10:
x1 in A
and A11:
x2 in A
and A12:
x = [x1,x2]
by A7, A8, ZFMISC_1:def 2;
consider J1 being
finite Subset of
I,
f1 being
ManySortedSet of
J1 such that A13:
x1 = g +* f1
and A14:
for
j being
set st
j in J1 holds
ex
G being non
empty Group-like multMagma st
(
G = F . j &
f1 . j in the
carrier of
G &
f1 . j <> 1_ G )
by A3, A10;
consider J2 being
finite Subset of
I,
f2 being
ManySortedSet of
J2 such that A15:
x2 = g +* f2
and A16:
for
j being
set st
j in J2 holds
ex
G being non
empty Group-like multMagma st
(
G = F . j &
f2 . j in the
carrier of
G &
f2 . j <> 1_ G )
by A3, A11;
reconsider x1 =
x1,
x2 =
x2 as
Function by A13, A15;
A17:
dom f1 = J1
by PARTFUN1:def 2;
A24:
dom f2 = J2
by PARTFUN1:def 2;
A31:
dom x1 =
(dom g) \/ (dom f1)
by A13, FUNCT_4:def 1
.=
I
by A2, A1, A17, XBOOLE_1:12
;
dom x2 =
(dom g) \/ (dom f2)
by A15, FUNCT_4:def 1
.=
I
by A2, A1, A24, XBOOLE_1:12
;
then reconsider x2 =
x2 as
Element of
product (Carrier F) by A1, A25, CARD_3:9;
reconsider x1 =
x1 as
Element of
product (Carrier F) by A1, A31, A18, CARD_3:9;
reconsider X1 =
x1,
X2 =
x2 as
Element of
(product F) by Def2;
A32:
[x1,x2] in [:A,A:]
by A10, A11, ZFMISC_1:87;
then A33:
y = X1 * X2
by A9, A12, FUNCT_1:49;
then reconsider y1 =
y as
Element of
product (Carrier F) by Def2;
defpred S2[
object ]
means ex
G being non
empty Group-like multMagma ex
k1,
k2 being
Element of
G st
(
G = F . $1 &
k1 = x1 . $1 &
k2 = x2 . $1 &
k1 * k2 = 1_ G &
f1 . $1
<> 1_ G &
f2 . $1
<> 1_ G );
consider K being
set such that A34:
for
k being
object holds
(
k in K iff (
k in I &
S2[
k] ) )
from XBOOLE_0:sch 1();
A35:
S1[
y]
proof
defpred S3[
object ,
object ]
means ex
G being non
empty Group-like multMagma ex
k1,
k2 being
Element of
G st
(
G = F . $1 &
k1 = x1 . $1 &
k2 = x2 . $1 & $2
= k1 * k2 );
reconsider J =
(J1 \/ J2) \ K as
finite Subset of
I ;
take
J
;
ex f being ManySortedSet of J st
( y = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
A36:
dom y1 = I
by A6;
A37:
for
j being
object st
j in J holds
ex
t being
object st
S3[
j,
t]
consider f being
ManySortedSet of
J such that A40:
for
j being
object st
j in J holds
S3[
j,
f . j]
from PBOOLE:sch 3(A37);
take
f
;
( y = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
set gf =
g +* f;
A41:
dom f = J
by PARTFUN1:def 2;
A42:
now for i being object st i in I holds
y1 . i = (g +* f) . ilet i be
object ;
( i in I implies y1 . b1 = (g +* f) . b1 )assume A43:
i in I
;
y1 . b1 = (g +* f) . b1then consider Fi being non
empty multMagma ,
h being
Function such that A44:
Fi = F . i
and A45:
h = the
multF of
(product F) . (
x1,
x2)
and A46:
h . i = the
multF of
Fi . (
(x1 . i),
(x2 . i))
by Def2;
consider FF being non
empty Group-like multMagma such that A47:
FF = F . i
by A43, Def3;
reconsider Fi =
Fi as non
empty Group-like multMagma by A44, A47;
reconsider x1i =
x1 . i,
x2i =
x2 . i as
Element of
Fi by A43, A44, Lm1;
A48:
y1 . i = x1i * x2i
by A9, A12, A32, A45, A46, FUNCT_1:49;
per cases
( i in J or not i in J )
;
suppose A50:
not
i in J
;
y1 . b1 = (g +* f) . b1then A51:
(g +* f) . i =
g . i
by A41, FUNCT_4:11
.=
1_ FF
by A43, A47, Th6
;
now ( ( not i in J1 \/ J2 & y1 . i = (g +* f) . i ) or ( i in K & y1 . i = (g +* f) . i ) )per cases
( not i in J1 \/ J2 or i in K )
by A50, XBOOLE_0:def 5;
case A52:
not
i in J1 \/ J2
;
y1 . i = (g +* f) . ithen
not
i in J2
by XBOOLE_0:def 3;
then
x2 . i = g . i
by A15, A24, FUNCT_4:11;
then A53:
x2 . i = 1_ FF
by A43, A47, Th6;
not
i in J1
by A52, XBOOLE_0:def 3;
then
x1 . i = g . i
by A13, A17, FUNCT_4:11;
then
x1 . i = 1_ FF
by A43, A47, Th6;
hence
y1 . i = (g +* f) . i
by A44, A47, A48, A51, A53, GROUP_1:def 4;
verum end; end; end; hence
y1 . i = (g +* f) . i
;
verum end; end; end;
dom (g +* f) =
(dom g) \/ (dom f)
by FUNCT_4:def 1
.=
I
by A2, A1, A41, XBOOLE_1:12
;
hence
y = g +* f
by A36, A42, FUNCT_1:2;
for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
let j be
set ;
( j in J implies ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) )
assume A54:
j in J
;
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
then consider G being non
empty Group-like multMagma ,
k1,
k2 being
Element of
G such that A55:
G = F . j
and A56:
k1 = x1 . j
and A57:
k2 = x2 . j
and A58:
f . j = k1 * k2
by A40;
take
G
;
( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
thus
G = F . j
by A55;
( f . j in the carrier of G & f . j <> 1_ G )
thus
f . j in the
carrier of
G
by A58;
f . j <> 1_ G
A59:
j in J1 \/ J2
by A54, XBOOLE_0:def 5;
per cases
( ( j in J1 & not j in J2 ) or ( not j in J1 & j in J2 ) or ( j in J1 & j in J2 ) )
by A59, XBOOLE_0:def 3;
suppose A60:
(
j in J1 & not
j in J2 )
;
f . j <> 1_ Gthen A61:
x1 . j = f1 . j
by A13, A17, FUNCT_4:13;
consider G1 being non
empty Group-like multMagma such that A62:
G1 = F . j
and
f1 . j in the
carrier of
G1
and A63:
f1 . j <> 1_ G1
by A14, A60;
x2 . j =
g . j
by A15, A24, A60, FUNCT_4:11
.=
1_ G1
by A54, A62, Th6
;
hence
f . j <> 1_ G
by A55, A56, A57, A58, A61, A62, A63, GROUP_1:def 4;
verum end; suppose A64:
( not
j in J1 &
j in J2 )
;
f . j <> 1_ Gthen A65:
x2 . j = f2 . j
by A15, A24, FUNCT_4:13;
consider G2 being non
empty Group-like multMagma such that A66:
G2 = F . j
and
f2 . j in the
carrier of
G2
and A67:
f2 . j <> 1_ G2
by A16, A64;
x1 . j =
g . j
by A13, A17, A64, FUNCT_4:11
.=
1_ G2
by A54, A66, Th6
;
hence
f . j <> 1_ G
by A55, A56, A57, A58, A65, A66, A67, GROUP_1:def 4;
verum end; end;
end;
reconsider ff =
X1 * X2 as
Element of
product (Carrier F) by Def2;
hence
y in A
by A3, A33, A35;
verum
end;
then reconsider b = the multF of (product F) || A as BinOp of A by FUNCT_2:def 1, RELSET_1:4;
set H = multMagma(# A,b #);
multMagma(# A,b #) is Group-like
proof
reconsider e =
g as
Element of
multMagma(#
A,
b #)
by A3, A5;
take
e
;
GROUP_1:def 2 for b1 being Element of the carrier of multMagma(# A,b #) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of multMagma(# A,b #) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be
Element of
multMagma(#
A,
b #);
( h * e = h & e * h = h & ex b1 being Element of the carrier of multMagma(# A,b #) st
( h * b1 = e & b1 * h = e ) )
reconsider h1 =
h as
Element of
(product F) by A4;
[h,e] in [:A,A:]
by ZFMISC_1:87;
hence h * e =
h1 * (1_ (product F))
by FUNCT_1:49
.=
h
by GROUP_1:def 4
;
( e * h = h & ex b1 being Element of the carrier of multMagma(# A,b #) st
( h * b1 = e & b1 * h = e ) )
[e,h] in [:A,A:]
by ZFMISC_1:87;
hence e * h =
(1_ (product F)) * h1
by FUNCT_1:49
.=
h
by GROUP_1:def 4
;
ex b1 being Element of the carrier of multMagma(# A,b #) st
( h * b1 = e & b1 * h = e )
reconsider h2 =
h1,
hh =
h1 " as
Element of
product (Carrier F) by Def2;
A71:
S1[
h1 " ]
proof
consider J being
finite Subset of
I,
f being
ManySortedSet of
J such that A72:
h = g +* f
and A73:
for
j being
set st
j in J holds
ex
G being non
empty Group-like multMagma st
(
G = F . j &
f . j in the
carrier of
G &
f . j <> 1_ G )
by A3;
defpred S2[
object ,
object ]
means ex
G being
Group ex
m being
Element of
G st
(
G = F . $1 &
m = f . $1 & $2
= m " );
A74:
for
i being
object st
i in J holds
ex
j being
object st
S2[
i,
j]
consider f9 being
ManySortedSet of
J such that A77:
for
j being
object st
j in J holds
S2[
j,
f9 . j]
from PBOOLE:sch 3(A74);
set gf9 =
g +* f9;
A78:
dom f9 = J
by PARTFUN1:def 2;
A79:
dom f = J
by PARTFUN1:def 2;
A80:
now for i being object st i in I holds
hh . i = (g +* f9) . ilet i be
object ;
( i in I implies hh . b1 = (g +* f9) . b1 )assume A81:
i in I
;
hh . b1 = (g +* f9) . b1then consider G3 being non
empty Group-like multMagma such that A82:
G3 = F . i
by Def3;
ex
G4 being non
empty associative multMagma st
G4 = F . i
by A81, Def4;
then consider G5 being
Group such that A83:
G5 = F . i
by A82;
per cases
( i in J or not i in J )
;
suppose A87:
not
i in J
;
hh . b1 = (g +* f9) . b1then A88:
(g +* f9) . i =
g . i
by A78, FUNCT_4:11
.=
1_ G3
by A81, A82, Th6
;
A89:
1_ G5 = (1_ G5) "
by GROUP_1:8;
h2 . i =
g . i
by A72, A79, A87, FUNCT_4:11
.=
1_ G3
by A81, A82, Th6
;
hence
hh . i = (g +* f9) . i
by A81, A82, A83, A88, A89, Th8;
verum end; end; end;
take
J
;
ex f being ManySortedSet of J st
( h1 " = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
take
f9
;
( h1 " = g +* f9 & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G ) ) )
A90:
dom hh = I
by A6;
dom (g +* f9) =
(dom g) \/ (dom f9)
by FUNCT_4:def 1
.=
I
by A2, A1, A78, XBOOLE_1:12
;
hence
h1 " = g +* f9
by A90, A80;
for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G )
let j be
set ;
( j in J implies ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G ) )
assume A91:
j in J
;
ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G )
then consider G being
Group,
m being
Element of
G such that A92:
G = F . j
and A93:
m = f . j
and A94:
f9 . j = m "
by A77;
take
G
;
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G )
thus
(
G = F . j &
f9 . j in the
carrier of
G )
by A92, A94;
f9 . j <> 1_ G
ex
G1 being non
empty Group-like multMagma st
(
G1 = F . j &
f . j in the
carrier of
G1 &
f . j <> 1_ G1 )
by A73, A91;
hence
f9 . j <> 1_ G
by A92, A93, A94, GROUP_1:10;
verum
end;
product (Carrier F) = the
carrier of
(product F)
by Def2;
then reconsider h9 =
h1 " as
Element of
multMagma(#
A,
b #)
by A3, A71;
take
h9
;
( h * h9 = e & h9 * h = e )
[h,h9] in [:A,A:]
by ZFMISC_1:87;
hence h * h9 =
h1 * (h1 ")
by FUNCT_1:49
.=
e
by GROUP_1:def 5
;
h9 * h = e
[h9,h] in [:A,A:]
by ZFMISC_1:87;
hence h9 * h =
(h1 ") * h1
by FUNCT_1:49
.=
e
by GROUP_1:def 5
;
verum
end;
then reconsider H = multMagma(# A,b #) as non empty Group-like multMagma ;
reconsider H = H as strict Subgroup of product F by A4, GROUP_2:def 5;
take
H
; for x being object holds
( x in the carrier of H iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) )
let x be object ; ( x in the carrier of H iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) )
given g being Element of product (Carrier F), J being finite Subset of I, f being ManySortedSet of J such that A95:
g = 1_ (product F)
and
A96:
x = g +* f
and
A97:
for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
; x in the carrier of H
A98:
dom g = I
by A6;
set gf = g +* f;
A99:
dom f = J
by PARTFUN1:def 2;
dom (g +* f) =
(dom g) \/ (dom f)
by FUNCT_4:def 1
.=
I
by A98, A99, XBOOLE_1:12
;
then
x in product (Carrier F)
by A1, A96, A100, CARD_3:9;
hence
x in the carrier of H
by A3, A95, A96, A97; verum