:: Definition and Properties of Direct Sum Decomposition of Groups
:: by Kazuhisa Nakasho , Hiroshi Yamazaki , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 31, 2014
:: Copyright (c) 2014-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1,
GROUP_1, XXREAL_0, GROUP_2, CARD_1, NUMBERS, FUNCT_4, GROUP_6, GROUP_7,
FUNCOP_1, ALGSTR_0, GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0,
STRUCT_0, NAT_1, ORDINAL4, ARYTM_1, ARYTM_3, FINSET_1, ZFMISC_1, PBOOLE,
REALSET1, NEWTON, GROUP_4, FINSEQ_2, PRE_POLY, UPROOTS, GROUP_19,
SEMI_AF1, MONOID_0, QC_LANG1, RLSUB_1, VECTMETR, PRALG_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, FUNCOP_1, REALSET1, FUNCT_4,
FINSET_1, CARD_1, PBOOLE, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, FINSEQ_1,
FINSEQ_2, FUNCT_7, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_4,
GROUP_6, MONOID_0, PRALG_1, GRSOLV_1, GROUP_7, GROUP_12, GROUP_17;
constructors REALSET1, FUNCT_4, MONOID_0, PRALG_1, GROUP_12, GROUP_4, FUNCT_7,
RELSET_1, FUNCT_3, GROUP_17, GRSOLV_1;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1,
FUNCT_2, CARD_3, GROUP_7, RELSET_1, INT_1, GR_CY_1, FINSET_1, RELAT_1,
FUNCT_1, NUMBERS, GROUP_12, PBOOLE;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities GROUP_2, FINSEQ_1, STRUCT_0, GRSOLV_1;
expansions TARSKI, FINSEQ_1, MONOID_0, STRUCT_0;
theorems PRALG_1, FUNCT_1, CARD_3, FUNCT_2, FUNCOP_1, TARSKI, GROUP_1,
GROUP_2, FUNCT_4, FINSEQ_1, GROUP_4, GROUP_6, FINSEQ_2, XREAL_1,
FINSEQ_3, XBOOLE_0, RELAT_1, GROUP_7, FUNCT_7, CARD_2, XBOOLE_1,
REALSET1, GROUP_12, PARTFUN1, ZFMISC_1, GROUP_17, PENCIL_3;
schemes NAT_1, FUNCT_2, XBOOLE_0, CLASSES1;
begin :: 1. Miscellanies
definition
let D be non empty set;
let x be Element of D;
redefine func <*x*> -> FinSequence of D; :: redefines <* (FINSEQ_1, definition)
coherence
proof
for y be object holds y in rng <*x*> implies y in D;
hence thesis;
end;
end;
definition
let I be set;
mode Group-Family of I is associative Group-like multMagma-Family of I;
end;
registration
let G be Group;
cluster commutative for Subgroup of G;
correctness
proof
(1).G is commutative;
hence thesis;
end;
end;
theorem Th1:
for I be set, F be Group-Family of I holds
for i be object st i in I holds F.i is Group
proof
let I be set;
let F be Group-Family of I;
let i be object;
assume
A1: i in I; then
ex Fi be Group-like non empty multMagma st Fi = F.i by GROUP_7:def 3;
hence thesis by A1;
end;
definition
let I be non empty set;
let F be Group-Family of I;
let i be Element of I;
redefine func F.i -> Group; :: redefines . (FUNCT_1, definition)
coherence by Th1;
end;
registration
let I be set;
let F be Group-Family of I;
cluster sum F -> non empty constituted-Functions;
correctness
proof
now
let x be Element of sum F;
x is Element of product F by GROUP_2:42;
hence x is Function;
end;
hence thesis;
end;
end;
theorem Th2:
for I be set, F be Function st I = dom F
& for i be object st i in I holds F.i is Group
holds F is Group-Family of I
proof
let I be set;
let F be Function;
assume
A1: I = dom F;
assume
A2: for i be object st i in I holds F.i is Group;
reconsider F as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
now
let y be set;
assume y in rng F; then
consider i be object such that
A3: i in dom F & y = F.i by FUNCT_1:def 3;
thus y is non empty multMagma by A2,A3;
end; then
reconsider F as multMagma-Family of I by GROUP_7:def 1;
A4: for i being set st i in I ex Fi being
Group-like non empty multMagma st Fi = F.i
proof
let i be set;
assume i in I; then
reconsider Fi = F.i as Group-like non empty multMagma by A2;
take Fi;
thus thesis;
end;
for i being set st i in I ex Fi being
associative non empty multMagma st Fi = F.i
proof
let i be set;
assume i in I; then
reconsider Fi = F.i as associative non empty multMagma by A2;
take Fi;
thus thesis;
end;
hence thesis by A4,GROUP_7:def 3,def 4;
end;
theorem Th3:
for I be set,
F be multMagma-Family of I,
a be Element of product F
holds dom a = I
proof
let I be set,
F be multMagma-Family of I,
a be Element of product F;
a in product F; then
a in product Carrier F by GROUP_7:def 2;
hence thesis by PARTFUN1:def 2;
end;
::$CT
theorem Th5:
for I be non empty set,
F be multMagma-Family of I,
x be Function,
i be Element of I
st x in product F
holds x.i in F.i
proof
let I be non empty set;
let F be multMagma-Family of I;
let x be Function;
let i be Element of I;
assume
A1: x in product F;
A2: (Carrier F).i = [#](F.i) by PENCIL_3:7;
i in I; then
A4: i in dom(Carrier F) by PARTFUN1:def 2;
x in product Carrier F by A1,GROUP_7:def 2;
hence thesis by A2,A4,CARD_3:9;
end;
theorem Th6:
for G,H be Group,
I be Subgroup of H,
f be Homomorphism of G,I
holds f is Homomorphism of G,H
proof
let G,H be Group,
I be Subgroup of H,
f be Homomorphism of G,I;
[#]I c= [#]H by GROUP_2:def 5; then
reconsider g = f as Function of G,H by FUNCT_2:7;
now
let a,b be Element of G;
thus g.(a*b) = f.a * f.b by GROUP_6:def 6
.= g.a * g.b by GROUP_2:43;
end;
hence thesis by GROUP_6:def 6;
end;
begin :: 2. Support of Element of Direct Product Group
definition
let I be set;
let F be Group-Family of I;
let a be Function;
func support(a,F) -> Subset of I means
:Def1:
for i be object holds i in it iff
ex G being Group st G = F.i & a.i <> 1_G & i in I;
existence
proof
defpred P[object] means ex G being Group st G = F.$1 & a.$1 <> 1_G;
consider X being set such that
A1: for x be object holds x in X iff x in I & P[x] from XBOOLE_0:sch 1;
for x be object st x in X holds x in I by A1; then
reconsider X as Subset of I by TARSKI:def 3;
take X;
let i be object;
thus i in X implies
ex G being Group st G = F.i & a.i <> 1_G & i in I
proof
assume
A2: i in X;
then ex G being Group st G = F.i & a.i <> 1_G by A1;
hence thesis by A2;
end;
thus thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset of I such that
A2: for i be object holds i in X1 iff
ex G being Group st G = F.i & a.i <> 1_G & i in I and
A3: for i be object holds i in X2 iff
ex G being Group st G = F.i & a.i <> 1_G & i in I;
now
let i be object;
i in X1 iff ex G being Group st G = F.i & a.i <> 1_G & i in I by A2;
hence i in X1 iff i in X2 by A3;
end;
hence X1 = X2 by TARSKI:2;
end;
end;
theorem Th7:
for I be set,
F be Group-Family of I,
a be Element of sum F holds
ex J being finite Subset of I,
b being ManySortedSet of J
st J = support(a,F)
& a = 1_product F +* b
& (for j being object, G being Group st j in I \ J & G = F.j holds a.j = 1_G)
& (for j being object st j in J holds a.j = b.j)
proof
let I be set,
F be Group-Family of I,
a be Element of sum F;
consider g being Element of product Carrier F,
J being finite Subset of I,
b being ManySortedSet of J such that
A1: g = 1_product F & a = g +* b
& for j being set st j in J
ex G being Group-like non empty multMagma
st G = F.j & b.j in the carrier of G & b.j <> 1_G
by GROUP_7:def 9;
take J,b;
A2: dom b = J by PARTFUN1:def 2;
A3: dom(1_product F) = I by Th3;
A4: for j being object, G being Group st j in I \ J & G = F.j holds a.j = 1_G
proof
let j be object;
let G be Group;
assume that
A6: j in I \ J and
A7: G = F.j;
j in dom(1_product F) & not j in dom b by A3,A6,XBOOLE_0:def 5;
hence a.j = (1_product F).j by A1,FUNCT_4:11
.= 1_G by A6,A7,GROUP_7:6;
end;
for j be object holds j in support(a,F) iff j in J
proof
let j be object;
hereby
assume
A11: j in support(a,F); then
consider G being Group such that
A12: G = F.j & a.j <> 1_G & j in I by Def1;
assume not j in J; then
j in I \ J by A11,XBOOLE_0:def 5;
hence contradiction by A4,A12;
end;
assume
A13: j in J; then
consider G being Group-like non empty multMagma such that
A14: G = F.j & b.j in the carrier of G & b.j <> 1_G by A1;
a.j <> 1_G by A1,A2,A13,A14,FUNCT_4:13;
hence j in support(a,F) by A13,A14,Def1;
end;
hence thesis by A1,A2,A4,FUNCT_4:13,TARSKI:2;
end;
registration
let I be set;
let F be Group-Family of I;
let a be Element of sum F;
cluster support(a,F) -> finite;
correctness
proof
ex J being finite Subset of I,
f being ManySortedSet of J st J = support(a,F)
& a = 1_product F +* f
&(for j being object, G being Group st j in I \ J & G = F.j
holds a.j = 1_G)
&(for j being object st j in J holds a.j = f.j) by Th7;
hence thesis;
end;
end;
definition
let I be set;
let G be Group;
let a be Function of I,G;
func support a -> Subset of I means
:Def2:
for i be object holds i in it iff a.i <> 1_G & i in I;
existence
proof
defpred P[object] means a.$1 <> 1_G;
consider X being set such that
A1: for x be object holds x in X iff x in I & P[x] from XBOOLE_0:sch 1;
for x be object st x in X holds x in I by A1; then
reconsider X as Subset of I by TARSKI:def 3;
take X;
thus thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset of I such that
A2: for i be object holds i in X1 iff a.i <> 1_G & i in I and
A3: for i be object holds i in X2 iff a.i <> 1_G & i in I;
now
let i be object;
i in X1 iff a.i <> 1_G & i in I by A2;
hence i in X1 iff i in X2 by A3;
end;
hence X1 = X2 by TARSKI:2;
end;
end;
definition
let I be set;
let G be Group;
let a be Function of I,G;
attr a is finite-support means
:Def3:
support a is finite;
end;
registration
let I be set;
let G be Group;
cluster finite-support for Function of I,G;
correctness
proof
set a = I --> 1_G;
take a;
support a = {}
proof
assume support a <> {}; then
consider x be object such that
A1: x in support a by XBOOLE_0:def 1;
a.x <> 1_G & x in I by A1,Def2;
hence contradiction by FUNCOP_1:7;
end;
hence thesis;
end;
end;
registration
let I be set;
let G be Group;
let a be finite-support Function of I,G;
cluster support a -> finite;
correctness by Def3;
end;
definition
let I be set;
let G be Group;
let a be finite-support Function of I,G;
func Product a -> Element of G equals
Product(a|support(a));
correctness;
end;
theorem Th8:
for I be set,
F be Group-Family of I,
a be Element of product F
holds
a in sum F
iff
support(a,F) is finite
proof
let I be set,
F be Group-Family of I,
a be Element of product F;
thus a in sum F implies support(a,F) is finite;
assume support(a,F) is finite; then
reconsider J = support(a,F) as finite Subset of I;
A2: [#] product F = product Carrier F by GROUP_7:def 2;
set k = a|J;
A3: dom a = I by A2,PARTFUN1:def 2; then
A4: dom k = J by RELAT_1:62; then
reconsider k as ManySortedSet of J by PARTFUN1:def 2,RELAT_1:def 18;
set x = 1_product F +* k;
A5: 1_product F is Element of product Carrier F by GROUP_7:def 2;
for j being set st j in J
ex G being Group-like non empty multMagma
st G = F.j & k.j in the carrier of G & k.j <> 1_G
proof
let j be set;
assume
A6: j in J;
then consider G being Group such that
A: G = F.j & a.j <> 1_G & j in I by Def1;
take G;
thus G = F.j by A;
a in product F; then
a.j in G by A,Th5;
hence k.j in the carrier of G by A6,FUNCT_1:49;
thus k.j <> 1_G by A,A6,FUNCT_1:49;
end; then
reconsider x as Element of sum F by A5,GROUP_7:def 9;
x in sum F; then
A10: x in product F by GROUP_2:40; then
A11: dom x = I by Th3;
for i be object st i in dom x holds x.i = a.i
proof
let i be object;
assume
A12: i in dom x;
then reconsider G = F.i as Group by A11,Th1;
per cases;
suppose
A15: not i in J; then
not i in dom k; then
x.i = (1_product F).i by FUNCT_4:11
.= 1_G by A11,A12,GROUP_7:6;
hence x.i = a.i by A11,A12,A15,Def1;
end;
suppose
A16: i in J;
hence x.i = k.i by A4,FUNCT_4:13
.= a.i by A16,FUNCT_1:49;
end;
end; then
x = a by A3,A10,Th3,FUNCT_1:2;
hence a in sum F;
end;
theorem Th9:
for I be set,
G be Group,
H be Group-Family of I,
x be Function of I,G,
y be Element of product H
st x = y
& for i be object st i in I holds H.i is Subgroup of G
holds support(x) = support(y,H)
proof
let I be set,
G be Group,
H be Group-Family of I,
x be Function of I,G,
y be Element of product H;
assume that
A1: x = y and
A2: for i be object st i in I holds H.i is Subgroup of G;
A5: for i be object, Z being Group st i in I & Z = H.i holds 1_Z = 1_G
proof
let i be object;
let Z be Group;
assume i in I; then
H.i is Subgroup of G by A2;
hence thesis by GROUP_2:44;
end;
for i be object holds i in support(y,H) iff i in support(x)
proof
let i be object;
A6: i in support(x) iff (x.i <> 1_G & i in I) by Def2;
hereby
assume i in support(y,H); then
ex Z being Group st Z = H.i & y.i <> 1_Z & i in I by Def1;
hence i in support(x) by A1,A5,A6;
end;
assume
A89: i in support(x); then
A90: x.i <> 1_G & i in I by Def2;
reconsider Z = H.i as Group by A89,Th1;
1_Z = 1_G by A5,A89;
hence i in support(y,H) by A1,A90,Def1;
end;
hence support(x) = support(y,H) by TARSKI:2;
end;
theorem Th10:
for I be set,
G be Group,
F be Group-Family of I,
a be object
st a in sum F
& for i be object st i in I holds F.i is Subgroup of G
holds a is finite-support Function of I,G
proof
let I be set,
G be Group,
F be Group-Family of I,
a be object;
assume that
A1: a in sum F and
A2: for i be object st i in I holds F.i is Subgroup of G;
a in product F by A1,GROUP_2:40; then
reconsider b = a as Element of product F;
A8: dom b = I by Th3;
for z be object st z in rng b holds z in [#]G
proof
let z be object;
assume z in rng b; then
consider i be object such that
A9: i in dom b & z = b.i by FUNCT_1:def 3;
i in I by A9,Th3;
then reconsider Z = F.i as Subgroup of G by A2;
reconsider I as non empty set by A9,Th3;
reconsider i as Element of I by A9,Th3;
reconsider F as multMagma-Family of I;
b.i in F.i by A1,Th5,GROUP_2:40;
then b.i in Z;
then b.i in G by GROUP_2:40;
hence z in [#]G by A9;
end; then
rng b c= [#] G; then
reconsider b as Function of I,G by A8,FUNCT_2:2;
support(b,F) = support(b) by A2,Th9;
hence thesis by A1,Def3;
end;
theorem
for I be non empty set,
F be Group-Family of I holds
support(1_product F,F) is empty
proof
let I be non empty set,
F be Group-Family of I;
for i be object holds not i in support(1_product F,F)
proof
let i be object;
assume i in support(1_product F,F); then
ex Z being Group st Z = F.i & (1_product F).i <> 1_Z & i in I by Def1;
hence contradiction by GROUP_7:6;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem Th12:
for I be non empty set, G be Group,
a be Function of I,G
st a = I --> 1_G
holds support(a) is empty
proof
let I be non empty set, G be Group,
a be Function of I,G;
assume
A1: a = I --> 1_G;
for i be object holds not i in support(a)
proof
let i be object;
assume
A2: i in support(a); then
a.i = 1_G by A1,FUNCOP_1:7;
hence contradiction by A2,Def2;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem Th13:
for I be non empty set, G be Group,
F be Group-Family of I
st for i be Element of I holds F.i is Subgroup of G
holds 1_product F = I --> 1_G
proof
let I be non empty set, G be Group,
F be Group-Family of I;
assume
A1: for i be Element of I holds F.i is Subgroup of G;
A2: dom(1_product F) = I by Th3;
A3: dom(I --> 1_G) = I by FUNCOP_1:13;
for j be object st j in I holds (1_product F).j = (I --> 1_G).j
proof
let j be object;
assume
A4: j in I; then
reconsider Z = F.j as Group by Th1;
A5: (1_product F).j = 1_Z by A4,GROUP_7:6;
A6: (I --> 1_G).j = 1_G by A4,FUNCOP_1:7;
reconsider j as Element of I by A4;
F.j is Subgroup of G by A1;
hence thesis by A5,A6,GROUP_2:44;
end;
hence thesis by A2,A3,FUNCT_1:2;
end;
theorem
for I be non empty set,
F be Group-Family of I,
G be Group,
x be finite-support Function of I,G
st support(x) = {}
& for i be object st i in I holds F.i is Subgroup of G
holds x = 1_product F
proof
let I be non empty set,
F be Group-Family of I,
G be Group,
x be finite-support Function of I,G;
assume that
A1: support(x) = {} and
A2: for i be object st i in I holds F.i is Subgroup of G;
for i being set st i in I
ex G being Group-like non empty multMagma st G = F.i & x.i = 1_G
proof
let i being set;
assume
A3: i in I; then
A4: x.i= 1_G by A1,Def2;
reconsider Fi = F.i as Subgroup of G by A2,A3;
take Fi;
thus Fi = F.i & x.i = 1_Fi by A4,GROUP_2:44;
end;
hence x = 1_product F by GROUP_7:5;
end;
theorem Th15:
for I be set,
G be Group,
x be finite-support Function of I,G
st support(x) = {}
holds Product x = 1_G
proof
let I be set,
G be Group,
x be finite-support Function of I,G;
assume support(x) = {}; then
(x|support(x)) * canFS(support(x)) = <*>(the carrier of G); then
Product(x|support(x)) = Product(<*>(the carrier of G)) by GROUP_17:def 1
.= 1_G by GROUP_4:8;
hence thesis;
end;
theorem Th16:
for I be non empty set, G be Group,
a be finite-support Function of I,G
st a = I --> 1_G
holds Product a = 1_G
proof
let I be non empty set, G be Group,
a be finite-support Function of I,G;
assume a = I --> 1_G; then
support(a) is empty by Th12;
hence thesis by Th15;
end;
theorem Th17:
for I be non empty set,
F be Group-Family of I,
x be Element of product F,
i be Element of I,
g be Element of F.i
st x = 1_product F +* (i,g)
holds support(x,F) c= {i}
proof
let I be non empty set,
F be Group-Family of I,
x be Element of product F,
i be Element of I,
g be Element of F.i;
assume
A1: x = 1_product F +* (i,g);
for j be object holds j in support(x,F) implies j in {i}
proof
let j be object;
assume j in support(x,F); then
ex Z being Group st Z = F.j & x.j <> 1_Z & j in I by Def1; then
j = i by A1,GROUP_12:1;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
theorem
for I be non empty set,
F be Group-Family of I,
x be Element of product F,
i be Element of I,
g be Element of F.i
st x = 1_product F +* (i,g)
& g <> 1_F.i
holds support(x,F) = {i}
proof
let I be non empty set,
F be Group-Family of I,
x be Element of product F,
i be Element of I,
g be Element of F.i;
assume that
A1: x = 1_product F +* (i,g) and
A2: g <> 1_F.i;
A3: dom x = I & x.i = g
& for j be Element of I st j <> i holds x.j = 1_F.j by A1,GROUP_12:1;
A4: support(x,F) c= {i} by A1,Th17;
i in support(x,F) by A2,A3,Def1; then
{i} c= support(x,F) by ZFMISC_1:31;
hence thesis by A4,XBOOLE_0:def 10;
end;
theorem Th19:
for I be non empty set, G be Group,
i be Element of I, g be Element of G,
a be Function of I,G
st a = (I --> 1_G) +* (i,g)
holds support(a) c= {i}
proof
let I be non empty set, G be Group,
i be Element of I, g be Element of G,
a be Function of I,G;
assume
A1: a = (I --> 1_G) +* (i,g);
for j be object holds j in support(a) implies j in {i}
proof
let j be object;
assume
A2: j in support(a);
j = i
proof
assume j <> i; then
a.j = (I --> 1_G).j by A1,FUNCT_7:32
.= 1_G by A2,FUNCOP_1:7;
hence contradiction by A2,Def2;
end;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
theorem Th20:
for I be non empty set, G be Group,
i be Element of I, g be Element of G,
a be Function of I,G
st a = (I --> 1_G) +* (i,g) & g <> 1_G
holds support(a) = {i}
proof
let I be non empty set, G be Group,
i be Element of I, g be Element of G,
a be Function of I,G;
assume that
A1: a = (I --> 1_G) +* (i,g) and
A2: g <> 1_G;
A3: support(a) c= {i} by A1,Th19;
dom(I --> 1_G) = I by FUNCOP_1:13; then
a.i = g by A1,FUNCT_7:31; then
i in support(a) by A2,Def2; then
{i} c= support(a) by ZFMISC_1:31;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th21:
for I be non empty set, G be Group,
a be finite-support Function of I,G,
i be Element of I, g be Element of G
st a = (I --> 1_G) +* (i,g)
holds Product a = g
proof
let I be non empty set, G be Group,
a be finite-support Function of I,G,
i be Element of I, g be Element of G;
assume
A1: a = (I --> 1_G) +* (i,g);
A2: dom(I --> 1_G) = I by FUNCOP_1:13;
per cases;
suppose
A3: g <> 1_G; then
support(a) = {i} by A1,Th20; then
i in support(a) by TARSKI:def 1; then
A6: i in dom(a|support(a)) by FUNCT_2:def 1;
(a|support(a)) * canFS(support(a))
= (a|support(a)) * canFS({i}) by A1,A3,Th20
.= (a|support(a)) * <*i*> by FINSEQ_1:94
.= <* (a|support(a)).i *> by A6,FINSEQ_2:34
.= <* a.i *> by A6,FUNCT_1:47
.= <*g*> by A1,A2,FUNCT_7:31;
hence Product a = Product(<*g*>) by GROUP_17:def 1
.= g by GROUP_4:9;
end;
suppose
A7: g = 1_G;
a = I --> 1_G
proof
A8: dom a = dom(I --> 1_G) by A1,FUNCT_7:30;
for j be object st j in I holds a.j = (I --> 1_G).j
proof
let j be object;
assume
A9: j in I; then
A10: (I --> 1_G).j = 1_G by FUNCOP_1:7;
per cases;
suppose
j = i;
hence thesis by A1,A2,A7,A10,FUNCT_7:31;
end;
suppose
j <> i; then
a.j = (I --> 1_G).j by A1,FUNCT_7:32
.= 1_G by A9,FUNCOP_1:7;
hence thesis by A9,FUNCOP_1:7;
end;
end;
hence thesis by A2,A8,FUNCT_1:2;
end;
hence thesis by A7,Th16;
end;
end;
theorem
for I be non empty set,
F be Group-Family of I,
x be Function,
i be Element of I,
g be Element of F.i
holds support(x,F) is finite implies support(x+*(i,g),F) is finite
proof
let I be non empty set,
F be Group-Family of I,
x be Function,
i be Element of I,
g be Element of F.i;
reconsider y = x +* (i,g) as Function;
assume
A1: support(x,F) is finite;
for j be object holds
j in support(y,F) implies j in support(x,F) \/ {i}
proof
let j be object;
assume j in support(y,F); then
A2: ex Z being Group st Z = F.j & y.j <> 1_Z & j in I by Def1;
per cases;
suppose
j = i; then
j in {i} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
j <> i; then
y.j = x.j by FUNCT_7:32; then
j in support(x,F) by A2,Def1;
hence thesis by XBOOLE_0:def 3;
end;
end; then
support(y,F) c= support(x,F) \/ {i};
hence thesis by A1;
end;
theorem Th23:
for I be non empty set, G be Group,
a be Function of I,G,
i be Element of I, g be Element of G
holds support(a) is finite implies support(a +* (i,g)) is finite
proof
let I be non empty set, G be Group,
a be Function of I,G,
i be Element of I, g be Element of G;
reconsider b = a +* (i,g) as Function of I,G;
assume
A1: support(a) is finite;
for j be object holds
j in support(b) implies j in support(a) \/ {i}
proof
let j be object;
assume j in support(b); then
A2: b.j <> 1_G & j in I by Def2;
per cases;
suppose
i = j; then
j in {i} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
i <> j; then
b.j = a.j by FUNCT_7:32; then
j in support(a) by A2,Def2;
hence thesis by XBOOLE_0:def 3;
end;
end; then
support(b) c= support(a) \/ {i};
hence thesis by A1;
end;
theorem Th24:
for I be non empty set,
F be Group-Family of I,
x be Function,
i be Element of I,
g be Element of F.i
holds x in product F implies x +* (i,g) in product F
proof
let I be non empty set,
F be Group-Family of I,
x be Function,
i be Element of I,
g be Element of F.i;
assume
A1: x in product F; then
A2: x in product Carrier F by GROUP_7:def 2; then
A3: dom x = dom(Carrier F) &
for j be object st j in dom(Carrier F) holds x.j in (Carrier F).j
by CARD_3:9;
A4: dom x = I by A1,Th3;
set y = x +* (i,g);
A6: dom y = I by A4,FUNCT_7:30;
A7: for j be object st j in dom(Carrier F) holds y.j in (Carrier F).j
proof
let j be object;
assume
A8: j in dom(Carrier F);
per cases;
suppose
A9: j = i; then
A10: y.j = g by A4,FUNCT_7:31;
g in [#](F.i);
hence thesis by A9,A10,PENCIL_3:7;
end;
suppose
j <> i; then
y.j = x.j by FUNCT_7:32;
hence thesis by A2,A8,CARD_3:9;
end;
end;
y in product Carrier F by A3,A4,A6,A7,CARD_3:9;
hence thesis by GROUP_7:def 2;
end;
theorem Th25:
for I be non empty set,
F be Group-Family of I,
x be Function,
i be Element of I,
g be Element of F.i
holds x in sum F implies x +* (i,g) in sum F
proof
let I be non empty set,
F be Group-Family of I,
x be Function,
i be Element of I,
g be Element of F.i;
set y = x +* (i,g);
assume
A1: x in sum F; then
A2: y in product F by Th24,GROUP_2:40;
for j be object holds j in support(y,F) implies j in support(x,F) \/ {i}
proof
let j be object;
assume j in support(y,F); then
consider Z being Group such that
A3: Z = F.j & y.j <> 1_Z & j in I by Def1;
per cases;
suppose
j = i; then
j in {i} by TARSKI:def 1;
hence thesis by TARSKI:def 3,XBOOLE_1:7;
end;
suppose
j <> i; then
x.j <> 1_Z & j in I by A3,FUNCT_7:32; then
j in support(x,F) by A3,Def1;
hence thesis by TARSKI:def 3,XBOOLE_1:7;
end;
end; then
support(y,F) c= support(x,F) \/ {i};
hence thesis by A1,A2,Th8;
end;
theorem
for I be non empty set, G be Group,
a be finite-support Function of I,G,
i be Element of I, g be Element of G
holds a +* (i,g) is finite-support Function of I,G
proof
let I be non empty set, G be Group,
a be finite-support Function of I,G,
i be Element of I, g be Element of G;
reconsider b = a +* (i,g) as Function of I,G;
support(a) is finite; then
support(b) is finite by Th23;
hence thesis by Def3;
end;
theorem Th27:
for I be non empty set,
F be Group-Family of I,
i be Element of I,
a,b be Function
st dom a = I & b = a +* (i,1_F.i)
holds support(b,F) = support(a,F) \ {i}
proof
let I be non empty set,
F be Group-Family of I,
i be Element of I,
a,b be Function;
assume that
A2: dom a = I and
A3: b = a +* (i,1_F.i);
for j be object holds j in support(b,F) iff j in support(a,F) \ {i}
proof
let j be object;
hereby
assume j in support(b,F); then
consider Z being Group such that
A: Z = F.j & b.j <> 1_Z & j in I by Def1;
A8: j <> i by A,A2,A3,FUNCT_7:31; then
{j} misses {i} by ZFMISC_1:11; then
A9: not j in {i} by ZFMISC_1:48;
a.j = b.j by A3,A8,FUNCT_7:32; then
j in support(a,F) by A,Def1;
hence j in support(a,F) \ {i} by A9,XBOOLE_0:def 5;
end;
assume j in support(a,F) \ {i}; then
A10: j in support(a,F) & not j in {i} by XBOOLE_0:def 5;
then consider Z being Group such that
A: Z = F.j & a.j <> 1_Z & j in I by Def1;
{j} misses {i} by A10,ZFMISC_1:50; then
b.j = a.j by A3,FUNCT_7:32;
hence j in support(b,F) by A,Def1;
end;
hence thesis by TARSKI:2;
end;
theorem Th28:
for I be non empty set,
G be Group,
i be object,
a,b be Function of I,G
st i in support(a) & b = a +* (i,1_G)
holds support(b) = support(a) \ {i}
proof
let I be non empty set,
G be Group,
i be object,
a,b be Function of I,G;
assume that
A1: i in support(a) and
A2: b = a +* (i,1_G);
A4: dom a = I by FUNCT_2:def 1;
A5: b.i = 1_G by A1,A2,A4,FUNCT_7:31;
for j be object holds j in support(b) iff j in support(a) \ {i}
proof
let j be object;
hereby
assume j in support(b); then
A7: b.j <> 1_G & j in I by Def2; then
{j} misses {i} by A5,ZFMISC_1:11; then
A9: not j in {i} by ZFMISC_1:48;
a.j = b.j by A2,A5,A7,FUNCT_7:32; then
j in support(a) by A7,Def2;
hence j in support(a) \ {i} by A9,XBOOLE_0:def 5;
end;
assume j in support(a) \ {i}; then
A10: j in support(a) & not j in {i} by XBOOLE_0:def 5;
{j} misses {i} by A10,ZFMISC_1:50; then
A11: b.j = a.j by A2,FUNCT_7:32;
a.j <> 1_G & j in I by A10,Def2;
hence j in support(b) by A11,Def2;
end;
hence thesis by TARSKI:2;
end;
theorem
for I be non empty set,
F be Group-Family of I,
i be Element of I,
a be Element of sum F,
b be Function
st i in support(a,F) & b = a +* (i,1_F.i)
holds card support(b,F) = card support(a,F) - 1
proof
let I be non empty set,
F be Group-Family of I,
i be Element of I,
a be Element of sum F,
b be Function;
assume that
A1: i in support(a,F) and
A2: b = a +* (i,1_F.i);
a is Element of product F by GROUP_2:42; then
dom a = I by Th3; then
support(b,F) = support(a,F) \ {i} by A2,Th27; then
card support(b,F) = card support(a,F) - card {i}
by A1,CARD_2:44,ZFMISC_1:31
.= card support(a,F) - 1 by CARD_2:42;
hence thesis;
end;
theorem
for I be non empty set,
G be Group,
i be object,
a be finite-support Function of I,G,
b be Function of I,G
st i in support(a) & b = a +* (i,1_G)
holds card support(b) = card support(a) - 1
proof
let I be non empty set,
G be Group,
i be object,
a be finite-support Function of I,G,
b be Function of I,G;
assume
A1: i in support(a) & b = a +* (i,1_G); then
support(b) = support(a) \ {i} by Th28; then
card support(b) = card support(a) - card {i}
by A1,CARD_2:44,ZFMISC_1:31
.= card support(a) - 1 by CARD_2:42;
hence thesis;
end;
theorem
for I be non empty set,
F be Group-Family of I,
a,b be Element of product F
st support(a,F) misses support(b,F)
holds a +* (b|support(b,F)) = a * b
proof
let I be non empty set,
F be Group-Family of I,
a,b be Element of product F;
assume
A1: support(a,F) misses support(b,F);
reconsider c = a +* (b|support(b,F)) as Function;
reconsider d = a * b as Element of product F;
A2: dom a = I by Th3;
A3: dom b = I by Th3;
A5: dom c = dom a \/ dom(b|support(b,F)) by FUNCT_4:def 1
.= I by A2,A3,RELAT_1:60,XBOOLE_1:12;
A6: dom d = I by Th3;
A8: dom(b|support(b,F)) = support(b,F) by A3,RELAT_1:62;
for i be object st i in I holds c.i = d.i
proof
let i be object;
assume i in I; then
reconsider i as Element of I;
a in product F & b in product F; then
a.i in F.i & b.i in F.i by Th5; then
reconsider ai = a.i, bi = b.i as Element of F.i;
per cases;
suppose
A9: not i in support(b,F);
c.i = a.i by A8,A9,FUNCT_4:11
.= ai * 1_F.i by GROUP_1:def 4
.= ai * bi by A9,Def1
.= d.i by GROUP_7:1;
hence thesis;
end;
suppose
A11: i in support(b,F); then
A12: not i in support(a,F) by A1,XBOOLE_0:3;
c.i = (b|support(b,F)).i by A8,A11,FUNCT_4:13
.= bi by A11,FUNCT_1:49
.= 1_F.i * bi by GROUP_1:def 4
.= ai * bi by A12,Def1
.= d.i by GROUP_7:1;
hence thesis;
end;
end;
hence thesis by A5,A6,FUNCT_1:2;
end;
theorem Th32:
for I be non empty set,
F be Group-Family of I,
a,b be Element of product F
st support(a,F) misses support(b,F)
holds a * b = b * a
proof
let I be non empty set,
F be Group-Family of I,
a,b be Element of product F;
assume
A1: support(a,F) misses support(b,F);
reconsider c = a * b as Element of product F;
reconsider d = b * a as Element of product F;
A2: dom c = I by Th3;
A3: dom d = I by Th3;
for i be object st i in I holds c.i = d.i
proof
let i be object;
assume i in I; then
reconsider i as Element of I;
a in product F; then
a.i in F.i by Th5; then
reconsider ai = a.i as Element of F.i;
b in product F; then
b.i in F.i by Th5; then
reconsider bi = b.i as Element of F.i;
per cases;
suppose
i in support(a,F); then
A4: not i in support(b,F) by A1,XBOOLE_0:3;
c.i = ai * bi by GROUP_7:1
.= ai * 1_F.i by A4,Def1
.= ai by GROUP_1:def 4
.= 1_F.i * ai by GROUP_1:def 4
.= bi * ai by A4,Def1
.= d.i by GROUP_7:1;
hence thesis;
end;
suppose
A5: not i in support(a,F);
c.i = ai * bi by GROUP_7:1
.= 1_F.i * bi by A5,Def1
.= bi by GROUP_1:def 4
.= bi * 1_F.i by GROUP_1:def 4
.= bi * ai by A5,Def1
.= d.i by GROUP_7:1;
hence thesis;
end;
end;
hence thesis by A2,A3,FUNCT_1:2;
end;
theorem Th33:
for I be non empty set,
F be Group-Family of I,
i be Element of I
holds ProjGroup(F,i) is Subgroup of sum F
proof
let I be non empty set,
F be Group-Family of I,
i be Element of I;
set S = ProjGroup(F,i);
set G = sum F;
for x be object st x in [#]S holds x in [#]G
proof
let x be object;
assume
A1: x in [#]S; then
x in S; then
x in product F by GROUP_2:40; then
reconsider x as Element of product F;
x in ProjSet(F,i) by A1,GROUP_12:def 2; then
consider h be Element of F.i such that
A3: x = 1_product F +* (i,h) by GROUP_12:def 1;
support(x,F) c= {i} by A3,Th17; then
x in sum F by Th8;
hence thesis;
end; then
A14: [#]S c= [#]G;
A16: the multF of G
= (the multF of (product F)) || (the carrier of G) by GROUP_2:def 5
.= (the multF of (product F)) | [:[#]G,[#]G:] by REALSET1:def 2;
(the multF of G) || [#]S
= ((the multF of (product F)) | [:[#]G,[#]G:]) | [:[#]S,[#]S:]
by A16,REALSET1:def 2
.= (the multF of (product F)) | [:[#]S,[#]S:]
by A14,RELAT_1:74,ZFMISC_1:96
.= (the multF of (product F)) || [#]S by REALSET1:def 2
.= the multF of S by GROUP_2:def 5;
hence thesis by A14,GROUP_2:def 5;
end;
theorem Th34:
for I be non empty set,
F,G be Group-Family of I,
x,y be Function
st for i be Element of I
ex hi be Homomorphism of F.i,G.i
st y.i = hi.(x.i)
holds support(y,G) c= support(x,F)
proof
let I be non empty set,
F,G be Group-Family of I,
x,y be Function;
assume
A1: for i be Element of I holds
ex hi be Homomorphism of F.i,G.i
st y.i = hi.(x.i);
for i be Element of I holds i in support(y,G) implies i in support(x,F)
proof
let i be Element of I;
assume
A2: i in support(y,G);
consider hi be Homomorphism of F.i,G.i such that
A3: y.i = hi.(x.i) by A1;
ex Z be Group st Z = G.i & hi.(x.i) <> 1_Z & i in I by A2,A3,Def1; then
x.i <> 1_ F.i by GROUP_6:31;
hence thesis by Def1;
end;
hence thesis;
end;
begin :: 3. Product Map and Sum Map
definition
let F, G be non-empty non empty Function,
h be non empty Function;
assume
A1: dom F = dom G = dom h
& for i be object st i in dom h holds h.i is Function of F.i,G.i;
func ProductMap(F,G,h) -> Function of product F,product G means
:Def5:
for x being Element of product F, i being object st i in dom h holds
ex hi be Function of F.i,G.i st hi = h.i & (it.x).i = hi.(x.i);
existence
proof
defpred P[Element of product F,Element of product G] means
for i being object st i in dom h holds
ex hi be Function of F.i,G.i st hi = h.i & $2.i = hi.($1.i);
A2: for x being Element of product F
ex y being Element of product G st P[x,y]
proof
let x be Element of product F;
defpred Q[object,object] means
ex hi be Function of F.$1,G.$1
st hi = h.$1 & $2 = hi.(x.$1);
A3: for i be object st i in dom h ex y be object st Q[i,y]
proof
let i be object;
assume i in dom h; then
reconsider hi = h.i as Function of F.i,G.i by A1;
take hi.(x.i);
thus thesis;
end;
consider y being Function such that
A4: dom y = dom h & for i being object st i in dom h holds Q[i,y.i]
from CLASSES1:sch 1(A3);
now
let i be object;
assume
A5: i in dom G; then
consider hi be Function of F.i,G.i such that
A7: hi = h.i & y.i = hi.(x.i) by A1,A4;
thus y.i in G.i by A1,A5,A7,CARD_3:9,FUNCT_2:5;
end; then
reconsider y as Element of product G by A1,A4,CARD_3:9;
take y;
let i be object;
assume i in dom h;
hence thesis by A4;
end;
thus ex p being Function of product F,product G
st for x being Element of product F holds P[x,p.x]
from FUNCT_2:sch 3(A2);
end;
uniqueness
proof
let p,q be Function of product F,product G such that
A8: for f being Element of product F, i being object st i in dom h holds
ex hi be Function of F.i,G.i st hi = h.i & (p.f).i = hi.(f.i) and
A9: for f being Element of product F, i being object st i in dom h holds
ex hi be Function of F.i,G.i st hi = h.i & (q.f).i = hi.(f.i);
now
let f being Element of product F;
A10: dom(p.f) = dom G & dom(q.f) = dom G by CARD_3:9;
now
let i be object;
assume i in dom(p.f); then
A12: i in dom h by A1,CARD_3:9;
A13: ex hi be Function of F.i,G.i
st hi = h.i & (p.f).i = hi.(f.i) by A8,A12;
ex hi be Function of F.i,G.i
st hi = h.i & (q.f).i = hi.(f.i) by A9,A12;
hence (p.f).i = (q.f).i by A13;
end;
hence p.f = q.f by A10,FUNCT_1:2;
end;
hence thesis by FUNCT_2:def 8;
end;
end;
theorem Th35:
for F,G be non-empty non empty Function,
h be non empty Function
st dom F = dom G = dom h
& for i be object st i in dom h holds
ex hi be Function of F.i,G.i
st hi = h.i & hi is onto
holds ProductMap(F,G,h) is onto
proof
let F, G be non-empty non empty Function,
h be non empty Function;
assume that
A1: dom F = dom G = dom h and
A2: for i be object st i in dom h holds
ex hi be Function of F.i,G.i st hi = h.i & hi is onto;
set p = ProductMap(F,G,h);
A4: for i be object st i in dom h holds h.i is Function of F.i,G.i
proof
let i be object;
assume i in dom h; then
ex hi be Function of F.i,G.i st hi = h.i & hi is onto by A2;
hence thesis;
end;
for y being object st y in product G
ex x being object st x in product F & y = p.x
proof
let y being object;
assume
A5: y in product G; then
reconsider y as Function;
A6: dom y = dom G
& for x being object st x in dom G holds y.x in G.x by A5,CARD_3:9;
defpred P[object,object] means
ex i be Element of dom h, hi be Function of F.i,G.i
st $1 =i & hi = h.i & $2 in F.i & y.i = hi.($2);
A7: for i be object st i in dom F ex x be object st P[i,x]
proof
let i be object;
assume i in dom F; then
reconsider i as Element of dom h by A1;
consider hi be Function of F.i,G.i such that
A9: hi = h.i & hi is onto by A2;
rng hi = G.i by A9,FUNCT_2:def 3; then
consider x be object such that
A11: x in F.i & y.i = hi.x by A1,A5,CARD_3:9,FUNCT_2:11;
take x;
thus thesis by A9,A11;
end;
consider x being Function such that
A12: dom x = dom F & for i being object st i in dom F holds P[i,x.i]
from CLASSES1:sch 1(A7);
now
let i be object;
assume i in dom F; then
ex i0 be Element of dom h, hi be Function of F.i0,G.i0
st i = i0 & hi = h.i0 & x.i in F.i0 & y.i0 = hi.(x.i) by A12;
hence x.i in F.i;
end; then
reconsider x as Element of product F by A12,CARD_3:9;
take x;
A14: dom y = dom(p.x) by A6,CARD_3:9;
now
let i be object;
assume i in dom y; then
i in dom F by A1,A5,CARD_3:9; then
consider i0 be Element of dom h, hi be Function of F.i0,G.i0 such that
A16: i = i0 & hi = h.i0 & x.i in F.i0 & y.i0 = hi.(x.i) by A12;
ex hi be Function of F.i0,G.i0
st hi = h.i0 & (p.x).i0 = hi.(x.i0) by A1,A4,Def5;
hence y.i = (p.x).i by A16;
end;
hence thesis by A14,FUNCT_1:2;
end; then
rng p = product G by FUNCT_2:10;
hence thesis by FUNCT_2:def 3;
end;
theorem Th36:
for F,G be non-empty non empty Function,
h be non empty Function
st dom F = dom G = dom h
& for i be object st i in dom h holds
ex hi be Function of F.i,G.i st hi = h.i & hi is one-to-one
holds ProductMap(F,G,h) is one-to-one
proof
let F,G be non-empty non empty Function,
h be non empty Function;
assume that
A1: dom F = dom G = dom h and
A2: for i be object st i in dom h holds
ex hi be Function of F.i,G.i st hi = h.i & hi is one-to-one;
set p = ProductMap(F,G,h);
A4: for i be object st i in dom h holds h.i is Function of F.i,G.i
proof
let i be object;
assume i in dom h; then
ex hi be Function of F.i,G.i st hi = h.i & hi is one-to-one by A2;
hence thesis;
end;
for x1,x2 being object st x1 in product F & x2 in product F & p.x1 = p.x2
holds x1 = x2
proof
let x1,x2 be object;
assume
A5: x1 in product F & x2 in product F & p.x1 = p.x2;
thus x1 = x2
proof
reconsider x1, x2 as Element of product F by A5;
A7: dom x2 = dom F by CARD_3:9;
for i be object st i in dom x1 holds x1.i = x2.i
proof
let i be object;
assume i in dom x1; then
reconsider i as Element of dom h by A1,CARD_3:9;
consider hi1 be Function of F.i,G.i such that
A9: hi1 = h.i & (p.x1).i = hi1.(x1.i) by A1,A4,Def5;
consider hi2 be Function of F.i,G.i such that
A10: hi2 = h.i & (p.x2).i = hi2.(x2.i) by A1,A4,Def5;
A14: ex hi be Function of F.i,G.i
st hi = h.i & hi is one-to-one by A2;
A15: x1.i in F.i by A1,CARD_3:9;
x2.i in F.i by A1,CARD_3:9;
hence thesis by A1,A5,A9,A10,A14,A15,FUNCT_2:19;
end;
hence thesis by A7,CARD_3:9,FUNCT_1:2;
end;
end;
hence thesis by FUNCT_2:19;
end;
theorem Th37:
for F,G be non-empty non empty Function,
h be non empty Function
st dom F = dom G = dom h
& for i be object st i in dom h holds
ex hi be Function of F.i,G.i st hi = h.i & hi is bijective
holds ProductMap(F,G,h) is bijective
proof
let F,G be non-empty non empty Function,
h be non empty Function;
assume that
A1: dom F = dom G = dom h and
A2: for i be object st i in dom h holds
ex hi be Function of F.i,G.i st hi = h.i & hi is bijective;
set p = ProductMap(F,G,h);
now
let i be object;
assume i in dom h; then
ex hi be Function of F.i,G.i
st hi = h.i & hi is bijective by A2;
hence ex hi be Function of F.i,G.i st hi = h.i & hi is onto;
end; then
A3: p is onto by A1,Th35;
now
let i be object;
assume i in dom h; then
ex hi be Function of F.i,G.i
st hi = h.i & hi is bijective by A2;
hence ex hi be Function of F.i,G.i
st hi = h.i & hi is one-to-one;
end; then
p is one-to-one by A1,Th36;
hence thesis by A3;
end;
theorem Th38:
for I be non empty set,
F,G be Group-Family of I,
h be non empty Function,
x be Element of product F,
y be Element of product G
st I = dom h
& y = ProductMap(Carrier F,Carrier G,h).x
& for i be Element of I holds
h.i is Homomorphism of F.i,G.i
holds
for i be Element of I holds
ex hi be Homomorphism of F.i,G.i
st hi = h.i & y.i = hi.(x.i)
proof
let I be non empty set,
F,G be Group-Family of I,
h be non empty Function,
x be Element of product F,
y be Element of product G;
assume that
A1: I = dom h and
A2: y = ProductMap(Carrier F,Carrier G,h).x and
A3: for i be Element of I holds h.i is Homomorphism of F.i,G.i;
set p = ProductMap(Carrier F,Carrier G,h);
dom Carrier G = I by PARTFUN1:def 2; then
A6: dom Carrier F = dom Carrier G = dom h by A1,PARTFUN1:def 2;
A7: for i be object st i in dom h holds
h.i is Function of (Carrier F).i,(Carrier G).i
proof
let i be object;
assume i in dom h; then
reconsider i as Element of I by A1;
A8: [#](F.i) = (Carrier F).i by PENCIL_3:7;
[#](G.i) = (Carrier G).i by PENCIL_3:7;
hence thesis by A3,A8;
end;
for i be Element of I holds
ex hi be Homomorphism of F.i,G.i st hi = h.i & y.i = hi.(x.i)
proof
let i be Element of I;
reconsider x as Element of product Carrier F by GROUP_7:def 2;
consider hi be Function of (Carrier F).i,(Carrier G).i such that
A13: hi = h.i and
A14: (p.x).i = hi.(x.i) by A1,A6,A7,Def5;
hi is Homomorphism of F.i, G.i by A3,A13;
hence thesis by A2,A13,A14;
end;
hence thesis;
end;
definition
let I be non empty set,
F,G be Group-Family of I,
h be non empty Function;
assume
A1: I = dom h
& for i be Element of I holds h.i is Homomorphism of F.i,G.i;
func ProductMap(F,G,h) -> Homomorphism of product F,product G equals
:Def6:
ProductMap(Carrier F,Carrier G,h);
coherence
proof
set p = ProductMap(Carrier F,Carrier G,h);
A3: [#] product F = product Carrier F by GROUP_7:def 2;
reconsider p as Function of product F,product G by A3,GROUP_7:def 2;
for a,b being Element of product F holds p.(a * b) = p.a * p.b
proof
let a,b being Element of product F;
A5: dom(p.(a * b)) = I by Th3;
A6: dom(p.a * p.b) = I by Th3;
:: for i be Element of I holds (p.(a * b)).i = (p.a * p.b).i
for i be object st i in I holds (p.(a * b)).i = (p.a * p.b).i
proof
let i be object;
assume i in I;
then reconsider i as Element of I;
consider hi be Homomorphism of F.i,G.i such that
A8: hi = h.i & (p.(a * b)).i = hi.((a * b).i) by A1,Th38;
consider hi1 be Homomorphism of F.i,G.i such that
A9: hi1 = h.i & (p.a).i = hi1.(a.i) by A1,Th38;
consider hi2 be Homomorphism of F.i,G.i such that
A10: hi2 = h.i & (p.b).i = hi2.(b.i) by A1,Th38;
a in product F; then
a.i in F.i by Th5; then
reconsider ai = a.i as Element of F.i;
b in product F; then
b.i in F.i by Th5; then
reconsider bi = b.i as Element of F.i;
(p.(a * b)).i = hi.(ai * bi) by A8,GROUP_7:1
.= hi.ai * hi.bi by GROUP_6:def 6
.= (p.a * p.b).i by A8,A9,A10,GROUP_7:1;
hence thesis;
end;
hence p.(a * b) = p.a * p.b by A5,A6,FUNCT_1:2;
end;
hence thesis by GROUP_6:def 6;
end;
end;
theorem Th39:
for I be non empty set,
F,G be Group-Family of I,
h be non empty Function,
x be Element of product F,
y be Element of product G
st I = dom h
& y = ProductMap(F,G,h).x
& for i be Element of I holds
h.i is Homomorphism of F.i,G.i
holds
for i be Element of I holds
ex hi be Homomorphism of F.i,G.i
st hi = h.i & y.i = hi.(x.i)
proof
let I be non empty set,
F,G be Group-Family of I,
h be non empty Function,
x be Element of product F,
y be Element of product G;
assume that
A1: I = dom h and
A2: y = ProductMap(F,G,h).x and
A3: for i be Element of I holds
h.i is Homomorphism of F.i,G.i;
y = ProductMap(Carrier F,Carrier G,h).x by A1,A2,A3,Def6;
hence thesis by A1,A3,Th38;
end;
theorem Th40:
for I be non empty set,
F,G be Group-Family of I,
h be non empty Function
st I = dom h
& for i be Element of I holds
ex hi be Homomorphism of F.i,G.i
st hi = h.i & hi is bijective
holds ProductMap(F,G,h) is bijective
proof
let I be non empty set,
F,G be Group-Family of I,
h be non empty Function;
assume
A1: I = dom h
& for i be Element of I holds
ex hi be Homomorphism of F.i,G.i st hi = h.i & hi is bijective;
set p = ProductMap(Carrier F,Carrier G,h);
A3: dom(Carrier F) = I & dom(Carrier G) = I by PARTFUN1:def 2;
for i be object st i in I holds
ex hi be Function of (Carrier F).i,(Carrier G).i
st hi = h.i & hi is bijective
proof
let i be object;
assume i in I;
then reconsider j = i as Element of I;
consider hi be Homomorphism of F.j,G.j such that
A5: hi = h.j & hi is bijective by A1;
A6: (Carrier F).j = [#](F.j) by PENCIL_3:7;
A7: (Carrier G).j = [#](G.j) by PENCIL_3:7; then
reconsider hi as Function of (Carrier F).i,(Carrier G).i by A6;
take hi;
thus thesis by A5,A7;
end; then
A8: p is bijective by A1,A3,Th37;
A9: [#] product F = product Carrier F by GROUP_7:def 2;
A10: [#] product G = product Carrier G by GROUP_7:def 2;
reconsider p as Function of product F,product G by A9,GROUP_7:def 2;
for i be Element of I holds h.i is Homomorphism of F.i,G.i
proof
let i be Element of I;
ex hi be Homomorphism of F.i,G.i st
hi = h.i & hi is bijective by A1;
hence thesis;
end; then
p = ProductMap(F,G,h) by A1,Def6;
hence thesis by A8,A10;
end;
definition
let I be non empty set,
F be Group-Family of I,
i be Element of I;
redefine func ProjGroup(F,i) -> strict Subgroup of sum F; :: redefines ProjGroup (GROUP_12, definition)
correctness by Th33;
end;
definition
let I be non empty set,
F,G be Group-Family of I,
h be non empty Function;
assume
A1: I = dom h
& for i be Element of I holds
h.i is Homomorphism of F.i,G.i;
func SumMap(F,G,h) -> Homomorphism of sum F,sum G equals
:Def7:
ProductMap(F,G,h) | sum F;
correctness
proof
set p = ProductMap(F,G,h);
set s = p | sum F;
for y being object holds y in rng s implies y in [#] sum G
proof
let y be object;
assume
A4: y in rng s; then
consider x being object such that
A5: x in dom s and
A6: y = s.x by FUNCT_1:def 3;
dom s c= dom p by RELAT_1:60; then
x in dom p by A5; then
reconsider x as Element of product F;
reconsider y as Element of product G by A4;
A8: y = p.x by A5,A6,FUNCT_1:47;
for i be Element of I holds
ex hi be Homomorphism of F.i,G.i st y.i = hi.(x.i)
proof
let i be Element of I;
consider hi be Homomorphism of F.i,G.i such that
A9: hi = h.i & y.i = hi.(x.i) by A1,A8,Th39;
thus thesis by A9;
end; then
support(y,G) c= support(x,F) by Th34; then
y in sum G by A5,Th8;
hence thesis;
end; then
rng s c= [#] sum G; then
[#] Image(s) c= [#] sum G by GROUP_6:44; then
A10: Image(s) is Subgroup of sum G by GROUP_2:57;
s is Homomorphism of sum F,Image(s) by GROUP_6:49;
hence thesis by A10,Th6;
end;
end;
theorem
for I be non empty set,
F,G be Group-Family of I,
h be non empty Function
st I = dom h
& for i be Element of I holds
ex hi be Homomorphism of F.i,G.i
st hi = h.i
& hi is bijective
holds SumMap(F,G,h) is bijective
proof
let I be non empty set,
F,G be Group-Family of I,
h be non empty Function;
assume that
A1: I = dom h and
A2: for i be Element of I holds
ex hi be Homomorphism of F.i,G.i st hi = h.i & hi is bijective;
A3: for i be Element of I holds h.i is Homomorphism of F.i,G.i
proof
let i be Element of I;
consider hi be Homomorphism of F.i,G.i such that
A4: hi = h.i & hi is bijective by A2;
thus thesis by A4;
end;
set p = ProductMap(F,G,h);
set s = SumMap(F,G,h);
A5: p is bijective by A1,A2,Th40;
A6: s = p | sum F by A1,A3,Def7; then
A7: s is one-to-one by A5,FUNCT_1:52;
A9: rng s c= [#] sum G;
for y be object holds y in [#] sum G implies y in rng s
proof
let y be object;
assume
A10: y in [#] sum G; then
y in sum G; then
A11: y in product G by GROUP_2:40; then
y in rng p by A5,GROUP_6:61; then
consider x be object such that
A12: x in dom p and
A13: y = p.x by FUNCT_1:def 3;
reconsider x as Element of product F by A12;
reconsider y as Element of product G by A11;
A15: x in sum F
proof
assume
A16: not x in sum F;
for i be Element of I holds
ex ki be Homomorphism of G.i,F.i st x.i = ki.(y.i)
proof
let i be Element of I;
consider hi be Homomorphism of F.i,G.i such that
A18: hi = h.i and
A19: y.i = hi.(x.i) by A1,A3,A13,Th39;
consider li be Homomorphism of F.i,G.i such that
A20: li = h.i & li is bijective by A2;
reconsider ki = hi" as Homomorphism of G.i,F.i by A18,A20,GROUP_6:62;
take ki;
x in product F; then
x.i in F.i by Th5;
hence thesis by A18,A19,A20,FUNCT_2:26;
end; then
support(x,F) c= support(y,G) by Th34;
hence contradiction by A10,A16,Th8;
end;
A22: x in dom s by A15,FUNCT_2:def 1; then
s.x = p.x by A6,FUNCT_1:47;
hence thesis by A13,A22,FUNCT_1:3;
end;
hence thesis by A7,A9,TARSKI:2,GROUP_6:60;
end;
theorem
for I be non empty set,
F,G be Group-Family of I,
h be non empty Function
st I = dom h
& for i be Element of I holds h.i is Homomorphism of F.i,G.i
holds
for i be Element of I,
f be Element of F.i,
hi be Homomorphism of F.i,G.i
st hi = h.i
holds SumMap(F,G,h).(1ProdHom(F,i).f) = 1ProdHom(G,i).(hi.f)
proof
let I be non empty set,
F,G be Group-Family of I,
h be non empty Function;
assume that
A1: I = dom h and
A2: for i be Element of I holds h.i is Homomorphism of F.i,G.i;
let i be Element of I,
f be Element of F.i,
hi be Homomorphism of F.i,G.i;
assume
A3: hi = h.i;
set x = 1ProdHom(F,i).f;
set y = SumMap(F,G,h).x;
x in ProjGroup(F,i); then
A6: x in sum F by GROUP_2:40;
reconsider x as Element of product F by GROUP_2:42;
y in sum G by A6,FUNCT_2:5; then
reconsider y as Element of product G by GROUP_2:42;
A8: x in dom SumMap(F,G,h) by A6,FUNCT_2:def 1;
SumMap(F,G,h) = ProductMap(F,G,h) | sum F by A1,A2,Def7; then
A10: y = ProductMap(F,G,h).x by A8,FUNCT_1:47;
A11: dom y = I by Th3;
A13: x = (1_product F) +* (i,f) by GROUP_12:def 3;
consider hi0 be Homomorphism of F.i,G.i such that
A15: hi0 = h.i & y.i = hi0.(x.i) by A1,A2,A10,Th39;
A16: y.i = hi.f by A3,A13,A15,GROUP_12:1;
A17: for j be Element of I st j <> i holds y.j = 1_G.j
proof
let j be Element of I;
assume j <> i; then
A18: x.j = 1_F.j by A13,GROUP_12:1;
consider hj be Homomorphism of F.j,G.j such that
A19: hj = h.j & y.j = hj.(x.j) by A1,A2,A10,Th39;
thus thesis by A18,A19,GROUP_6:31;
end;
y = (1_product G) +* (i,hi.f) by A11,A16,A17,GROUP_12:1;
hence thesis by GROUP_12:def 3;
end;
begin :: 4. Definition of Internal and External Direct Sum Decomposition
theorem Th43:
for I be non empty set,
G be Group,
i be object st i in I holds
ex F be Group-Family of I,
h be Homomorphism of sum F, G
st h is bijective
& F = (I --> (1).G) +* ({i} --> G)
&(for j be Element of I holds 1_F.j = 1_G)
&(for x be Element of sum F holds h.x = x.i)
& for x be Element of sum F
ex J being finite Subset of I,
a being ManySortedSet of J
st J c= {i}
& J = support(x,F)
& (support(x,F) = {} or support(x,F) = {i})
& x = 1_product F +* a
& (for j being Element of I st j in I \ J holds x.j = 1_F.j)
& (for j being object st j in J holds x.j = a.j)
proof
let I be non empty set,
G be Group,
i be object;
assume
A1: i in I;
set v = I --> (1).G;
set w = {i} --> G;
set F = v +* w;
A4: dom F = dom(v) \/ dom(w) by FUNCT_4:def 1
.= dom(v) \/ {i} by FUNCOP_1:13
.= I \/ {i} by FUNCOP_1:13
.= I by A1,XBOOLE_1:12,ZFMISC_1:31;
A5: i in {i} by TARSKI:def 1; then
i in dom w by FUNCOP_1:13; then
A7: F.i = w.i by FUNCT_4:13; then
A8: F.i = G by A5,FUNCOP_1:7;
A9: for j be object st j in I \ {i} holds F.j = (1).G
proof
let j be object;
assume
A10: j in I \ {i}; then
j in dom F by A4; then
A11: j in dom(v) \/ dom(w) by FUNCT_4:def 1;
not j in dom w by A10,XBOOLE_0:def 5;
hence F.j = v.j by A11,FUNCT_4:def 1
.= (1).G by A10,FUNCOP_1:7;
end;
for j be object st j in I holds F.j is Group
proof
let j be object;
assume
A12: j in I;
per cases;
suppose
j in {i};
hence F.j is Group by A8,TARSKI:def 1;
end;
suppose
not j in {i}; then
j in I \ {i} by A12,XBOOLE_0:def 5;
hence F.j is Group by A9;
end;
end; then
reconsider F as Group-Family of I by A4,Th2;
A17: for j be Element of I holds 1_F.j = 1_G
proof
let j be Element of I;
per cases;
suppose
j in {i};
hence 1_F.j = 1_G by A8,TARSKI:def 1;
end;
suppose
not j in {i}; then
j in I \ {i} by XBOOLE_0:def 5; then
F.j = (1).G by A9;
hence 1_F.j = 1_G by GROUP_2:44;
end;
end;
defpred P[Element of sum F,Element of G] means $2 = $1.i;
A24: for x being Element of sum F ex y being Element of G st P[x,y]
proof
let x be Element of sum F;
B01: x in sum F;
reconsider i as Element of I by A1;
A25: x.i in F.i by GROUP_2:40,Th5,B01;
A26: i in {i} by TARSKI:def 1; then
A27: i in dom w by FUNCOP_1:13; then
i in dom(v) \/ dom(w) by XBOOLE_0:def 3; then
F.i = w.i by A27,FUNCT_4:def 1; then
reconsider y = x.i as Element of G by A25,A26,FUNCOP_1:7;
take y;
thus thesis;
end;
consider h being Function of sum F,G such that
A29: for x being Element of sum F holds P[x,h.x] from FUNCT_2:sch 3(A24);
for y being object st y in [#]G
ex x being object st x in [#]sum F & y = h.x
proof
let y be object;
assume
A30: y in [#]G;
reconsider i as Element of I by A1;
set x = 1_product F +* (i,y);
A32: 1_product F in product F;
A33: y in F.i by A5,A7,A30,FUNCOP_1:7; then
x in product F by A32,Th24; then
reconsider x as Element of product F;
support(x,F) c= {i} by A33,Th17; then
A35: x in sum F by Th8;
take x;
thus x in [#]sum F by A35;
A36: dom(1_product F) = I by Th3;
reconsider x as Element of sum F by A35;
reconsider y as Element of G by A30;
P[x,y] by A36,FUNCT_7:31;
hence thesis by A29;
end; then
rng h = [#]G by FUNCT_2:10; then
A42: h is onto by FUNCT_2:def 3;
A43: for x be Element of sum F holds support(x,F) c= {i}
proof
let x be Element of sum F;
now
let j be object;
assume
A44: j in support(x,F); then
consider Z be Group such that
A45: Z = F.j & x.j <> 1_Z & j in I by Def1;
assume not j in {i}; then
j in I \ {i} by A44,XBOOLE_0:def 5; then
A46: F.j = (1).G by A9;
x in sum F; then
x.j in Z by A45,GROUP_2:40,Th5; then
x.j in {1_G} by A45,A46,GROUP_2:def 7; then
x.j = 1_G by TARSKI:def 1;
hence contradiction by A45,A46,GROUP_2:44;
end;
hence thesis;
end;
for x1,x2 being object
st x1 in [#]sum F & x2 in [#]sum F & h.x1 = h.x2 holds x1 = x2
proof
let x1,x2 be object;
assume
A48: x1 in [#]sum F & x2 in [#]sum F & h.x1 = h.x2; then
reconsider x1,x2 as Element of sum F;
x1 in sum F & x2 in sum F; then
A49: x1 in product F & x2 in product F by GROUP_2:40; then
A50: dom x1 = I & dom x2 = I by Th3;
consider J1 being finite Subset of I,
a1 being ManySortedSet of J1 such that
A51: J1 = support(x1,F)
& x1 = 1_product F +* a1
&(for j being object, G being Group st j in I \ J1 & G = F.j
holds x1.j = 1_G)
&(for j being object st j in J1 holds x1.j = a1.j) by Th7;
consider J2 being finite Subset of I,
a2 being ManySortedSet of J2 such that
A52: J2 = support(x2,F)
& x2 = 1_product F +* a2
&(for j being object, G being Group st j in I \ J2 & G = F.j
holds x2.j = 1_G)
&(for j being object st j in J2 holds x2.j = a2.j) by Th7;
A53: support(x1,F) c= {i} by A43;
A54: support(x2,F) c= {i} by A43;
for j be object st j in dom x1 holds x1.j = x2.j
proof
let j be object;
assume j in dom x1; then
A56: j in I by A49,Th3;
then reconsider Z = F.j as Group by Th1;
per cases;
suppose
not j in {i}; then
not j in J1 & not j in J2 by A51,A52,A53,A54; then
A59: j in I \ J1 & j in I \ J2 by A56,XBOOLE_0:def 5;
hence x1.j = 1_Z by A51
.= x2.j by A52,A59;
end;
suppose
j in {i}; then
A61: j = i by TARSKI:def 1;
hence x1.j = h.x2 by A29,A48
.= x2.j by A29,A61;
end;
end;
hence thesis by A50,FUNCT_1:2;
end; then
A62: h is one-to-one by FUNCT_2:19;
for x, y being Element of sum F holds h.(x * y) = h.x * h.y
proof
let x, y being Element of sum F;
A68: for j be set st j in I holds
ex Fi being non empty multMagma, xi,yi being Element of Fi
st xi = x.j & yi = y.j & Fi = F.j & (x * y).j = xi * yi
proof
let j be set;
assume j in I; then
reconsider j as Element of I;
x in sum F; then
x in product F by GROUP_2:40; then
reconsider x0 = x as Element of product F;
x0 in product F; then
x0.j in F.j by Th5; then
reconsider xi = x0.j as Element of F.j;
y in sum F; then
y in product F by GROUP_2:40; then
reconsider y0 = y as Element of product F;
y0 in product F; then
y0.j in F.j by Th5; then
reconsider yi = y0.j as Element of F.j;
(x * y).j = (x0 * y0).j by GROUP_2:43
.= xi * yi by GROUP_7:1;
hence thesis;
end;
h.(x * y) = h.x * h.y
proof
consider Fa being non empty multMagma,
xa,ya being Element of Fa such that
A72: xa = x.i & ya = y.i & Fa = F.i & (x * y).i = xa * ya by A1,A68;
A74: xa = h.x by A29,A72;
thus h.(x * y) = xa * ya by A29,A72
.= h.x * h.y by A8,A29,A72,A74;
end;
hence thesis;
end; then
reconsider h as Homomorphism of sum F, G by GROUP_6:def 6;
take F,h;
thus h is bijective by A42,A62;
thus F = (I --> (1).G) +* ({i} --> G);
thus for j be Element of I holds 1_F.j = 1_G by A17;
thus for x be Element of sum F holds h.x = x.i by A29;
let x be Element of sum F;
A78: support(x,F) c= {i} by A43;
A79: support(x,F) = {} or support(x,F) = {i}
proof
per cases;
suppose
support(x,F) = {};
hence thesis;
end;
suppose
support(x,F) <> {}; then
consider j be object such that
A82: j in support(x,F) by XBOOLE_0:def 1;
A83: {j} c= support(x,F) by A82,ZFMISC_1:31;
j = i by A78,A82,TARSKI:def 1;
hence thesis by A78,A83,XBOOLE_0:def 10;
end;
end;
consider J being finite Subset of I,
a being ManySortedSet of J such that
A85: J = support(x,F)
& x = 1_product F +* a
&(for j being object, G being Group st j in I \ J & G = F.j
holds x.j = 1_G)
&(for j being object st j in J holds x.j = a.j) by Th7;
take J,a;
thus thesis by A79,A85;
end;
definition
let I be non empty set;
let G be Group;
mode DirectSumComponents of G,I -> Group-Family of I means
:Def8:
ex h be Homomorphism of sum it, G st h is bijective;
existence
proof
consider i be object such that
A1: i in I by XBOOLE_0:def 1;
consider F be Group-Family of I,
h be Homomorphism of sum F, G such that
A2: h is bijective
& F = (I --> (1).G) +* ({i} --> G)
&(for j be Element of I holds 1_F.j = 1_G)
&(for x be Element of sum F holds h.x = x.i)
& for x be Element of sum F
ex J being finite Subset of I,
a being ManySortedSet of J
st J c= {i}
& J = support(x,F)
& (support(x,F) = {} or support(x,F) = {i})
& x = 1_product F +* a
& (for j being Element of I st j in I \ J holds x.j = 1_F.j)
& (for j being object st j in J holds x.j = a.j) by A1,Th43;
thus thesis by A2;
end;
end;
definition
let I be non empty set;
let G be Group;
let F be DirectSumComponents of G,I;
attr F is internal means
:Def9:
(for i be Element of I holds F.i is Subgroup of G)
& ex h be Homomorphism of sum F, G
st h is bijective
& for x be finite-support Function of I,G st x in sum F holds
h.x = Product x;
end;
registration
let I be non empty set;
let G be Group;
cluster internal for DirectSumComponents of G,I;
existence
proof
consider i be object such that
A1: i in I by XBOOLE_0:def 1;
consider F be Group-Family of I,
h be Homomorphism of sum F,(Omega).G such that
A2: h is bijective
& F = (I --> (1).((Omega).G)) +* ({i} --> (Omega).G)
&(for j be Element of I holds 1_F.j = 1_(Omega).G)
&(for x be Element of sum F holds h.x = x.i)
& for x be Element of sum F
ex J being finite Subset of I,
a being ManySortedSet of J
st J c= {i}
& J = support(x,F)
& (support(x,F) = {} or support(x,F) = {i})
& x = 1_product F +* a
& (for j being Element of I st j in I \ J holds x.j = 1_F.j)
& (for j being object st j in J holds x.j = a.j) by A1,Th43;
reconsider W = F.i as Group by A1,Th1;
reconsider h as Homomorphism of sum F,G by Th6;
h is bijective by A2; then
reconsider F as DirectSumComponents of G,I by Def8;
set v = (I --> (1).((Omega).G));
set w = ({i} --> (Omega).G);
A8: dom F = dom v \/ dom w by A2,FUNCT_4:def 1
.= dom v \/ {i} by FUNCOP_1:13
.= I \/ {i} by FUNCOP_1:13
.= I by A1,XBOOLE_1:12,ZFMISC_1:31;
A9: i in {i} by TARSKI:def 1; then
i in dom w by FUNCOP_1:13; then
A11: F.i = w.i by A2,FUNCT_4:13; then
A12: F.i = (Omega).G by A9,FUNCOP_1:7;
A13: for j be object st j in I \ {i} holds F.j = (1).((Omega).G)
proof
let j be object;
assume
A14: j in I \ {i}; then
j in dom F by A8; then
A15: j in dom v \/ dom w by A2,FUNCT_4:def 1;
not j in dom w by A14,XBOOLE_0:def 5;
hence F.j = v.j by A2,A15,FUNCT_4:def 1
.= (1).((Omega).G) by A14,FUNCOP_1:7;
end;
A21: for j be object st j in I holds F.j is Subgroup of G
proof
let j be object;
assume
A22: j in I;
then reconsider Z = F.j as Group by Th1;
per cases;
suppose
j in {i};
hence thesis by A12,TARSKI:def 1;
end;
suppose
not j in {i}; then
j in I \ {i} by A22,XBOOLE_0:def 5; then
F.j is strict Subgroup of (Omega).G by A13;
hence thesis;
end;
end;
for x be finite-support Function of I,G st x in sum F
holds h.x = Product x
proof
let x be finite-support Function of I,G;
assume
A23: x in sum F; then
reconsider x0 = x as Element of sum F;
set p = x|support(x);
A24: dom p = support(x) by FUNCT_2:def 1;
A28: x0 in product F by A23,GROUP_2:40; then
A29: support(x0,F) = support(x) by A21,Th9;
A30: h.x0 = x0.i by A2;
consider J being finite Subset of I,
a being ManySortedSet of J such that
A31: J c= {i}
& J = support(x0,F)
& (support(x0,F) = {} or support(x0,F) = {i})
& x0 = 1_product F +* a
& (for j being Element of I st j in I \ J holds x0.j = 1_F.j)
& (for j being object st j in J holds x0.j = a.j) by A2;
per cases by A31;
suppose
A32: support(x0,F) = {};
A34: x.i = 1_W by A1,A31,A32
.= 1_(Omega).G by A9,A11,FUNCOP_1:7;
p * canFS(support(x)) = <*>(the carrier of G) by A29,A32; then
Product p = Product(<*>(the carrier of G)) by GROUP_17:def 1
.= 1_G by GROUP_4:8;
hence thesis by A30,A34,GROUP_2:44;
end;
suppose
A36: support(x0,F) = {i};
reconsider xi = x0.i as Element of G by A30,FUNCT_2:5;
A37: i in dom p by A24,A29,A36,TARSKI:def 1;
p * canFS(support(x)) = p * canFS({i}) by A21,A28,A36,Th9
.= p * (<*i*>) by FINSEQ_1:94
.= <* p.i *> by A37,FINSEQ_2:34
.= <* xi *> by A37,FUNCT_1:47; then
Product p = Product(<* xi *>) by GROUP_17:def 1
.= x0.i by GROUP_4:9;
hence thesis by A2;
end;
end; then
F is internal by A2,A21;
hence thesis;
end;
end;
begin :: 5. Equivalent Expression of Internal Direct Sum Decomposition
theorem Th44:
for G be Group, A be non empty Subset of G
st for x,y be Element of G st x in A & y in A holds x * y = y * x
holds gr A is commutative
proof
let G be Group, A be non empty Subset of G;
assume
A1: for x,y be Element of G st x in A & y in A holds x * y = y * x;
A2: for x,y be Element of G, i,j be Element of INT st x in A & y in A
holds (x|^i) * (y|^j) = (y|^j) * (x|^i)
proof
let x,y be Element of G, i,j be Element of INT;
assume x in A & y in A; then
x * y = y * x by A1;
hence thesis by GROUP_1:39;
end;
A3: for y be Element of G, j be Element of INT st y in A holds
for F be FinSequence of G, I be FinSequence of INT
st len F = len I & rng F c= A
holds Product(F|^I) * (y|^j) = (y|^j) * Product(F|^I)
proof
let y be Element of G, j be Element of INT;
assume
A4: y in A;
set x = y|^j;
defpred P[Nat] means
for F be FinSequence of G, I be FinSequence of INT
st len F = $1 & len F = len I & rng F c= A
holds Product(F|^I) * x = x * Product(F|^I);
A5: P[0]
proof
let F be FinSequence of G,
I be FinSequence of INT such that
A6: len F = 0 & len F = len I & rng F c= A;
F = <*>([#]G) & I = <*>INT by A6; then
F|^I = <*>([#]G) by GROUP_4:21; then
A7: Product(F|^I) = 1_G by GROUP_4:8;
hence Product(F|^I) * x = x by GROUP_1:def 4
.= x * Product(F|^I) by A7,GROUP_1:def 4;
end;
A8: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A9: P[k];
let F be FinSequence of G,
I be FinSequence of INT such that
A10: len F = k+1 & len F = len I & rng F c= A;
reconsider g = F/.(k+1) as Element of G;
reconsider i = I/.(k+1) as Element of INT;
reconsider F0 = F|k as FinSequence of G;
reconsider I0 = I|k as FinSequence of INT;
rng F0 c= rng F by RELAT_1:70; then
A11: rng F0 c= A by A10;
reconsider F1 = <*g*> as FinSequence of G;
reconsider I1 = <*i*> as FinSequence of INT;
A12: <* @i *> = I1 by GROUP_4:def 1;
k+1 in Seg (k+1) by FINSEQ_1:4; then
A13: k+1 in dom F by A10,FINSEQ_1:def 3; then
F/.(k+1) = F.(k+1) by PARTFUN1:def 6; then
A14: F = F0^F1 by A10,FINSEQ_3:55;
k+1 in Seg (k+1) by FINSEQ_1:4; then
k+1 in dom I by A10,FINSEQ_1:def 3; then
A15: I/.(k+1) = I.(k+1) by PARTFUN1:def 6;
g = F.(k+1) by A13,PARTFUN1:def 6; then
A17: g in A by A10,A13,FUNCT_1:3;
k <= len F & k <= len I by A10,XREAL_1:31; then
A18: len F0 = k & len I0 = k by FINSEQ_1:17;
A19: len F1 = 1 & len I1 = 1 by FINSEQ_1:39;
A20: F|^I = (F0^F1) |^ (I0^I1) by A10,A14,A15,FINSEQ_3:55
.= (F0|^I0)^(F1|^I1) by A18,A19,GROUP_4:19
.= (F0|^I0)^<*g|^i*> by A12,GROUP_4:22;
hence Product(F|^I) * x
= (Product(F0|^I0) * (g|^i)) * x by GROUP_4:6
.= Product(F0|^I0) * ((g|^i) * x) by GROUP_1:def 3
.= Product(F0|^I0) * (x * (g|^i)) by A2,A4,A17
.= Product(F0|^I0) * x * (g|^i) by GROUP_1:def 3
.= x * Product(F0|^I0) * (g|^i) by A9,A11,A18
.= x * (Product(F0|^I0) * (g|^i)) by GROUP_1:def 3
.= x * Product(F|^I) by A20,GROUP_4:6;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A5,A8);
hence thesis;
end;
A22: for x,g be Element of G, i be Element of INT st x in gr A & g in A
holds x * g|^i = g|^i * x
proof
let x,g be Element of G, i be Element of INT such that
A23: x in gr A & g in A;
consider F be FinSequence of G,
I be FinSequence of INT such that
A24: len F = len I & rng F c= A & Product(F|^I) = x by A23,GROUP_4:28;
thus x * g|^i = g|^i * x by A3,A23,A24;
end;
A25: for x be Element of G st x in gr A holds
for F be FinSequence of G, I be FinSequence of INT
st len F = len I & rng F c= A
holds Product(F|^I) * x = x * Product(F|^I)
proof
let x be Element of G;
assume
A26: x in gr A;
defpred P[Nat] means
for x be Element of G st x in gr A holds
for F be FinSequence of G, I be FinSequence of INT
st len F = $1 & len F = len I & rng F c= A
holds Product(F|^I) * x = x * Product(F|^I);
A27: P[0]
proof
let x be Element of G;
assume x in gr A;
let F be FinSequence of G,
I be FinSequence of INT such that
A29: len F = 0 & len F = len I & rng F c= A;
F = <*>([#]G) & I = <*>INT by A29; then
F|^I = <*>(the carrier of G) by GROUP_4:21; then
A30: Product(F|^I) = 1_G by GROUP_4:8;
hence Product(F|^I) * x = x by GROUP_1:def 4
.= x * Product(F|^I) by A30,GROUP_1:def 4;
end;
A31: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A32: P[k];
let x be Element of G;
assume
A33: x in gr A;
let F be FinSequence of G,
I be FinSequence of INT such that
A34: len F = k+1 & len F = len I & rng F c= A;
reconsider g = F/.(k+1) as Element of G;
reconsider i = I/.(k+1) as Element of INT;
reconsider F0 = F|k as FinSequence of G;
reconsider I0 = I|k as FinSequence of INT;
rng F0 c= rng F by RELAT_1:70; then
A35: rng F0 c= A by A34;
reconsider F1 = <*g*> as FinSequence of G;
reconsider I1 = <*i*> as FinSequence of INT;
A36: <* @i *> = I1 by GROUP_4:def 1;
k+1 in Seg (k+1) by FINSEQ_1:4; then
A37: k+1 in dom F by A34,FINSEQ_1:def 3; then
F/.(k+1) = F.(k+1) by PARTFUN1:def 6; then
A38: F = F0^F1 by A34,FINSEQ_3:55;
k+1 in Seg(k+1) by FINSEQ_1:4; then
k+1 in dom I by A34,FINSEQ_1:def 3; then
A39: I/.(k+1) = I.(k+1) by PARTFUN1:def 6;
g = F.(k+1) by A37,PARTFUN1:def 6; then
A40: g in A by A34,A37,FUNCT_1:3;
k <= len F & k <= len I by A34,XREAL_1:31; then
A41: len F0 = k & len I0 = k by FINSEQ_1:17;
A42: len F1 = 1 & len I1 = 1 by FINSEQ_1:39;
A43: F|^I = (F0^F1) |^ (I0^I1) by A34,A38,A39,FINSEQ_3:55
.= (F0|^I0) ^ (F1|^I1) by A41,A42,GROUP_4:19
.= (F0|^I0) ^ <*g|^i*> by A36,GROUP_4:22;
hence Product(F|^I) * x
= (Product(F0|^I0) * (g|^i)) * x by GROUP_4:6
.= Product(F0|^I0) * ((g|^i) * x) by GROUP_1:def 3
.= Product(F0|^I0) * (x * (g|^i)) by A22,A33,A40
.= Product(F0|^I0) * x * (g|^i) by GROUP_1:def 3
.= x * Product(F0|^I0) * (g|^i) by A32,A33,A35,A41
.= x * (Product(F0|^I0) * (g|^i)) by GROUP_1:def 3
.= x * Product(F|^I) by A43,GROUP_4:6;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A27,A31);
hence thesis by A26;
end;
for x,y be Element of gr A holds x * y = y * x
proof
let x be Element of gr A;
let y be Element of gr A;
A45: x in gr A;
x in G by GROUP_2:41; then
reconsider x0 = x as Element of G;
consider F be FinSequence of G,
I be FinSequence of INT such that
A46: len F = len I & rng F c= A & Product(F|^I) = x0 by A45,GROUP_4:28;
y in G by GROUP_2:41; then
reconsider z = y as Element of G;
A47: z in gr A;
thus x * y = Product(F|^I) * z by A46,GROUP_2:43
.= z * Product(F|^I) by A25,A46,A47
.= y * x by A46,GROUP_2:43;
end;
hence gr A is commutative by GROUP_1:def 12;
end;
theorem Th45:
for G be Group,
H be Subgroup of G,
a be FinSequence of G,
b be FinSequence of H
st a = b
holds Product a = Product b
proof
let G be Group, H be Subgroup of G;
defpred P[Nat] means
for a be FinSequence of G,
b be FinSequence of H
st len a = $1 & a = b
holds Product a = Product b;
A1: P[0]
proof
let a be FinSequence of G,
b be FinSequence of H;
assume len a = 0 & a = b; then
a = <*>([#]G) & b = <*>([#]H); then
Product a = 1_G & Product b = 1_H by GROUP_4:8;
hence Product a = Product b by GROUP_2:44;
end;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A5: P[k];
let a be FinSequence of G, b be FinSequence of H;
assume
A6: len a = k+1 & a = b;
reconsider g = a/.(k+1) as Element of G;
reconsider i = b/.(k+1) as Element of H;
reconsider a0 = a|k as FinSequence of G;
reconsider b0 = b|k as FinSequence of H;
k+1 in Seg(k+1) by FINSEQ_1:4; then
A7: k+1 in dom a by A6,FINSEQ_1:def 3; then
A8: a/.(k+1) = a.(k+1) by PARTFUN1:def 6;
k+1 in Seg(k+1) by FINSEQ_1:4; then
A9: k+1 in dom b by A6,FINSEQ_1:def 3; then
A10: b/.(k+1) = b.(k+1) by PARTFUN1:def 6;
k <= len a & k <= len b by A6,XREAL_1:31; then
len a0 = k & len b0 = k by FINSEQ_1:17; then
A13: Product a0 = Product b0 by A5,A6;
A14: g = a.(k+1) by A7,PARTFUN1:def 6
.= i by A6,A9,PARTFUN1:def 6;
thus Product a = Product(a0^<*g*>) by A6,A8,FINSEQ_3:55
.= (Product a0) * g by GROUP_4:6
.= (Product b0) * i by A13,A14,GROUP_2:43
.= Product (b0^<*i*>) by GROUP_4:6
.= Product b by A6,A10,FINSEQ_3:55;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A1,A4);
hence thesis;
end;
theorem Th46:
for G be Group,
h be Element of G
holds
for F be FinSequence of G
st for k be Nat st k in dom F
holds h * F/.k = (F/.k) * h
holds h * Product(F) = Product(F) * h
proof
let G be Group, h be Element of G;
defpred P[Nat] means
for F be FinSequence of G
st len F = $1
& for i be Nat st i in dom F holds h * F/.i = (F/.i) * h
holds h * Product(F) = Product(F) * h;
A1: P[0]
proof
let F be FinSequence of G;
assume len F = 0
& for i be Nat st i in dom F holds h * F/.i = (F/.i) * h; then
F = <*>([#]G); then
A2: Product F = 1_G by GROUP_4:8;
hence h * Product(F) = h by GROUP_1:def 4
.= Product(F) * h by A2,GROUP_1:def 4;
end;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
let F be FinSequence of G;
assume
A5: len F = k+1
& for i be Nat st i in dom F holds h * F/.i = (F/.i) * h;
reconsider g = F/.(k+1) as Element of G;
reconsider F0 = F|k as FinSequence of G;
k+1 in Seg(k+1) by FINSEQ_1:4; then
A6: k+1 in dom F by A5,FINSEQ_1:def 3; then
A7: F/.(k+1) = F.(k+1) by PARTFUN1:def 6;
A8: k <= len F by A5,XREAL_1:31; then
A9: len F0 = k by FINSEQ_1:17;
A11: Seg k c= Seg(k+1) by XREAL_1:31,FINSEQ_1:5;
A12: dom F0 = Seg k by A8,FINSEQ_1:17;
A13: dom F = Seg(k+1) by A5,FINSEQ_1:def 3;
A14: for i be Nat st i in dom F0 holds h * F0/.i = F0/.i * h
proof
let i be Nat;
assume
A15: i in dom F0; then
F0/.i = F/.i by PARTFUN1:80;
hence thesis by A5,A11,A12,A13,A15;
end;
A19: Product F = Product(F0^<*g*>) by A5,A7,FINSEQ_3:55
.= (Product F0) * g by GROUP_4:6;
hence h * Product F = (h * (Product F0)) * g by GROUP_1:def 3
.= ((Product F0) * h) * g by A4,A9,A14
.= (Product F0) * (h * g) by GROUP_1:def 3
.= (Product F0) * (g * h) by A5,A6
.= (Product F) * h by A19,GROUP_1:def 3;
end;
A20: for i be Nat holds P[i] from NAT_1:sch 2(A1,A3);
let F be FinSequence of G;
assume
A21: for k be Nat st k in dom F holds h * F/.k = (F/.k) * h;
len F is Nat;
hence thesis by A20,A21;
end;
theorem Th47:
for G be Group,
F,F1,F2 be FinSequence of G
st len F = len F1 & len F = len F2
&(for i,j be Nat st i in dom F & j in dom F & i <> j
holds F1/.i * F2/.j = F2/.j * F1/.i)
& for k be Nat st k in dom F holds F.k = (F1/.k) * (F2/.k)
holds Product(F) = Product(F1) * Product(F2)
proof
let G be Group;
defpred P[Nat] means
for F,F1,F2 be FinSequence of G
st len F = $1 & len F = len F1 & len F = len F2
&(for i,j be Nat st i in dom F & j in dom F & i <> j
holds F1/.i * F2/.j = F2/.j * F1/.i)
& for k be Nat st k in dom F holds F.k = (F1/.k) * (F2/.k)
holds Product(F) = Product(F1) * Product(F2);
A1: P[0]
proof
let F,F1,F2 be FinSequence of G;
assume
len F = 0 & len F = len F1 & len F = len F2
& (for i,j be Nat st i in dom F & j in dom F & i <> j
holds F1/.i * F2/.j = F2/.j * F1/.i)
& for k be Nat st k in dom F holds F.k = (F1/.k) * (F2/.k); then
F = <*>([#]G) & F1 = <*>([#]G) & F2 = <*>([#]G); then
Product F = 1_G & Product F1 = 1_G & Product F2 = 1_G by GROUP_4:8;
hence thesis by GROUP_1:def 4;
end;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
let F,F1,F2 be FinSequence of G;
assume
A5: len F = k+1 & len F = len F1 & len F = len F2
& (for i,j be Nat st i in dom F & j in dom F & i <> j
holds F1/.i * F2/.j = F2/.j * F1/.i)
& for k be Nat st k in dom F holds F.k = (F1/.k) * (F2/.k);
reconsider g = F/.(k+1) as Element of G;
reconsider h = F1/.(k+1) as Element of G;
reconsider i = F2/.(k+1) as Element of G;
reconsider F0 = F|k as FinSequence of G;
reconsider F10 = F1|k as FinSequence of G;
reconsider F20 = F2|k as FinSequence of G;
A6: k+1 in Seg(k+1) by FINSEQ_1:4; then
A7: k+1 in dom F by A5,FINSEQ_1:def 3; then
A8: F/.(k+1) = F.(k+1) by PARTFUN1:def 6;
k+1 in Seg(k+1) by FINSEQ_1:4; then
k+1 in dom F1 by A5,FINSEQ_1:def 3; then
A9: F1/.(k+1) = F1.(k+1) by PARTFUN1:def 6;
k+1 in Seg(k+1) by FINSEQ_1:4; then
k+1 in dom F2 by A5,FINSEQ_1:def 3; then
A10: F2/.(k+1) = F2.(k+1) by PARTFUN1:def 6;
A12: k <= len F & k <= len F1 & k <= len F2 by A5,XREAL_1:31; then
A13: len F0 = k & len F10 = k & len F20 = k by FINSEQ_1:17;
A15: Seg k c= Seg (k+1) by FINSEQ_1:5,XREAL_1:31;
A16: dom F0 = Seg k by A12,FINSEQ_1:17; then
A17: dom F10 = dom F0 by A12,FINSEQ_1:17;
A18: dom F20 = dom F0 by A12,A16,FINSEQ_1:17;
A19: dom F = Seg(k+1) by A5,FINSEQ_1:def 3;
A22: for i,j be Nat st i in dom F0 & j in dom F0 & i <> j
holds F10/.i * F20/.j = F20/.j * F10/.i
proof
let i,j be Nat;
assume
A23: i in dom F0 & j in dom F0 & i <> j; then
A27: F10/.i = F1/.i by A17,PARTFUN1:80;
hence F10/.i * F20/.j = F1/.i * F2/.j by A18,A23,PARTFUN1:80
.= F2/.j * F1/.i by A5,A15,A16,A19,A23
.= F20/.j * F10/.i by A18,A23,A27,PARTFUN1:80;
end;
A29: for k be Nat st k in dom F0 holds F0.k = (F10/.k) * (F20/.k)
proof
let k be Nat;
assume
A30: k in dom F0; then
A34: F10/.k = F1/.k by A17,PARTFUN1:80;
thus F0.k = F.k by A30,FUNCT_1:47
.= F1/.k * F2/.k by A5,A15,A16,A19,A30
.= F10/.k * F20/.k by A18,A30,A34,PARTFUN1:80;
end;
A36: for i be Nat st i in dom F20 holds h * F20/.i = F20/.i * h
proof
let i be Nat;
assume
A37: i in dom F20; then
A40: F20/.i = F2/.i by PARTFUN1:80;
dom F20 = Seg k by A12,FINSEQ_1:17; then
A41: 1 <= i & i <= k by A37,FINSEQ_1:1;
k + 0 < k+1 by XREAL_1:8;
hence thesis by A5,A6,A15,A16,A18,A19,A37,A40,A41;
end;
A43: g = F.(k+1) by A7,PARTFUN1:def 6
.= h * i by A5,A7;
A44: Product F1 = Product(F10^<*h*>) by A5,A9,FINSEQ_3:55
.= (Product F10) * h by GROUP_4:6;
A45: Product F2 = Product(F20^<*i*>) by A5,A10,FINSEQ_3:55
.= (Product F20) * i by GROUP_4:6;
thus Product F = Product(F0^<*g*>) by A5,A8,FINSEQ_3:55
.= (Product F0) * g by GROUP_4:6
.= (Product F10 * Product F20) * (h * i)
by A4,A13,A22,A29,A43
.= (Product F10 * Product F20 * h) * i by GROUP_1:def 3
.= (Product F10 * (Product F20 * h)) * i by GROUP_1:def 3
.= (Product F10 * (h * Product F20)) * i by A36,Th46
.= (Product F10 * h * Product F20) * i by GROUP_1:def 3
.= Product F1 * Product F2 by A44,A45,GROUP_1:def 3;
end;
for i be Nat holds P[i] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem Th48:
for G be Group, a be FinSequence of G
st for i be object st i in dom a holds a.i = 1_G
holds Product a = 1_G
proof
let G be Group, a be FinSequence of G;
assume
A1: for i be object st i in dom a holds a.i = 1_G;
set n = len a;
a = n |-> 1_G
proof
n |-> 1_G = Seg n --> 1_G by FINSEQ_2:def 2; then
A2: dom(n |-> 1_G) = Seg n by FUNCOP_1:13;
A3: dom a = Seg n by FINSEQ_1:def 3;
for i be object st i in dom a holds a.i = (n |-> 1_G).i
proof
let i be object;
assume
A4: i in dom a; then
i in Seg n by FINSEQ_1:def 3; then
(n |-> 1_G).i = 1_G by FINSEQ_2:57;
hence thesis by A1,A4;
end;
hence thesis by A2,A3,FUNCT_1:2;
end; then
Product a = (1_G) |^ n by GROUP_4:12
.= 1_G by GROUP_1:31;
hence thesis;
end;
theorem Th49:
for I be finite set,
G be Group,
a be (the carrier of G)-valued total I-defined Function
st for i be object st i in I holds a.i = 1_G
holds Product a = 1_G
proof
let I be finite set,
G be Group,
a be (the carrier of G)-valued total I-defined Function;
assume
A1: for i be object st i in I holds a.i = 1_G;
set cs = canFS(I);
set acs = a * cs;
A2: rng acs c= the carrier of G;
A3: I = dom a & rng cs = I by FUNCT_2:def 3,PARTFUN1:def 2; then
dom acs = dom cs by RELAT_1:27; then
dom acs = Seg len cs by FINSEQ_1:def 3; then
acs is FinSequence by FINSEQ_1:def 2; then
reconsider acs as FinSequence of G by A2,FINSEQ_1:def 4;
A4: Product a = Product acs by GROUP_17:def 1;
for i be object st i in dom acs holds acs.i = 1_G
proof
let i be object;
assume
A5: i in dom acs; then
i in dom cs by A3,RELAT_1:27; then
cs.i in rng cs by FUNCT_1:3; then
a.(cs.i) =1_G by A1;
hence thesis by A5,FUNCT_1:12;
end;
hence thesis by A4,Th48;
end;
theorem Th50:
for A be finite set, B be non empty set,
f be B-valued total A-defined Function
holds f * canFS(A) is FinSequence of B
proof
let A be finite set, B be non empty set,
f be B-valued total A-defined Function;
A1: rng(f * canFS(A)) c= B;
A = dom f & rng canFS(A) = A by FUNCT_2:def 3,PARTFUN1:def 2; then
dom(f * canFS(A)) = dom canFS(A) by RELAT_1:27; then
dom(f * canFS(A)) = Seg len canFS(A) by FINSEQ_1:def 3; then
f * canFS(A) is FinSequence by FINSEQ_1:def 2;
hence thesis by A1,FINSEQ_1:def 4;
end;
theorem Th51:
for I be non empty set,
G be Group,
a be finite-support Function of I,G,
W be finite Subset of I
st support(a) c= W
& for i,j be Element of I holds a.i * a.j = a.j * a.i
holds Product a = Product(a|W)
proof
let I be non empty set,
G be Group,
a be finite-support Function of I,G,
W be finite Subset of I;
assume that
A1: support(a) c= W and
A2: for i,j be Element of I holds a.i * a.j = a.j * a.i;
reconsider ra = rng a as non empty Subset of G;
for x,y be Element of G st x in ra & y in ra holds x * y = y * x
proof
let x,y be Element of G;
assume
A3: x in ra & y in ra; then
consider i be Element of I such that
A4: x = a.i by FUNCT_2:113;
consider j be Element of I such that
A5: y = a.j by A3,FUNCT_2:113;
thus thesis by A2,A4,A5;
end; then
reconsider H = gr(ra) as non empty commutative Subgroup of G by Th44;
reconsider A = support(a) as finite Subset of W by A1;
reconsider B = W \ support(a) as finite Subset of W by XBOOLE_1:36;
per cases;
suppose
A6: A = {}; then
(a|A) * canFS(A) = {}; then
A7: Product(a) = Product(<*>(the carrier of G)) by GROUP_17:def 1
.= 1_G by GROUP_4:8;
for i be object st i in W holds (a|W).i = 1_G
proof
let i be object;
assume
A8: i in W; then
a.i = 1_G by A6,Def2;
hence (a|W).i = 1_G by A8,FUNCT_1:49;
end;
hence Product a = Product(a|W) by A7,Th49;
end;
suppose
A11: A <> {};
per cases;
suppose
B = {}; then
W c= A by XBOOLE_1:37; then
A = W by XBOOLE_0:def 10;
hence Product a = Product(a|W);
end;
suppose
A12: B <> {};
rng a c= [#]H by GROUP_4:def 4; then
A14: a is Function of I,H by FUNCT_2:6; then
reconsider fa = a|support(a) as (the carrier of H)-valued
total A-defined Function;
reconsider B0 = B as finite Subset of I;
reconsider fb = a|B0 as (the carrier of H)-valued
total B0-defined Function by A14;
A15: A \/ B = W by XBOOLE_1:45; then
reconsider fab = a|W as (the carrier of H)-valued
total A \/ B -defined Function by A14;
A16: A misses B by XBOOLE_1:79;
A17: dom fab = A \/ B by A15,FUNCT_2:def 1
.= dom fa \/ B by FUNCT_2:def 1
.= dom fa \/ dom fb by FUNCT_2:def 1;
A18: for x be object st x in dom fab holds fab.x = (fa +* fb).x
proof
let x be object;
assume
A19: x in dom fab; then
per cases by A17,XBOOLE_0:def 3;
suppose
A22: x in dom fa;
A24: not x in dom fb
proof
assume x in dom fb; then
x in A /\ B by A22,XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 7,XBOOLE_1:79;
end;
thus fab.x = a.x by A19,FUNCT_1:47
.= fa.x by A22,FUNCT_1:47
.= (fa +* fb).x by A24,FUNCT_4:11;
end;
suppose
A25: x in dom fb;
thus fab.x = a.x by A19,FUNCT_1:47
.= fb.x by A25,FUNCT_1:47
.= (fa +* fb).x by A25,FUNCT_4:13;
end;
end;
A27: dom(fa +* fb) = dom fa \/ dom fb by FUNCT_4:def 1;
reconsider fca = fa * canFS(A) as FinSequence of H by Th50;
reconsider fcsa = fa * canFS(support(a)) as FinSequence of G by Th50;
reconsider fcab = fab * canFS(A \/ B) as FinSequence of H by Th50;
reconsider fcw = (a|W) * canFS(W) as FinSequence of G by Th50;
A31: Product(fa) = Product(fca) by GROUP_17:def 1
.= Product(fcsa) by Th45
.= Product(a) by GROUP_17:def 1;
A35: fcab = fcw by XBOOLE_1:45;
A36: Product(fab) = Product(fcab) by GROUP_17:def 1
.= Product(fcw) by A35,Th45
.= Product(a|W) by GROUP_17:def 1;
for i be object st i in B0 holds fb.i = 1_H
proof
let i be object;
assume
A38: i in B0; then
A39: i in W & not i in support(a) by XBOOLE_0:def 5;
i in dom fb by A38,FUNCT_2:def 1;
hence fb.i = a.i by FUNCT_1:47
.= 1_G by A39,Def2
.= 1_H by GROUP_2:44;
end; then
A41: Product(fb) = 1_H by Th49
.= 1_G by GROUP_2:44;
thus Product(a|W) = Product(fa) * Product(fb)
by A11,A12,A16,A17,A18,A27,A36,FUNCT_1:2,GROUP_17:8
.= Product(a) * 1_G by A31,A41,GROUP_2:43
.= Product(a) by GROUP_1:def 4;
end;
end;
end;
theorem
for I be non empty set,
G be Group,
a be finite-support Function of I,G,
W be finite Subset of I
st support a c= W
holds
ex aW be finite-support Function of W,G
st aW = a|W
& support a = support(aW)
& Product a = Product(aW)
proof
let I be non empty set,
G be Group,
a be finite-support Function of I,G,
W be finite Subset of I;
assume
A1: support a c= W;
A2: for i be object holds i in support a iff i in support(a|W)
proof
let i be object;
hereby
assume
A3: i in support a; then
A4: a.i <> 1_G & i in I by Def2;
(a|W).i = a.i by A1,A3,FUNCT_1:49;
hence i in support (a|W) by A1,A3,A4,Def2;
end;
assume
A6: i in support(a|W); then
A7: (a|W).i <> 1_G & i in W by Def2;
(a|W).i = a.i by A6,FUNCT_1:49;
hence i in support a by A7,Def2;
end;
support(a|W) is finite; then
reconsider aW = a|W as finite-support Function of W,G by Def3;
take aW;
aW|support(aW) = (a|W) | support(a) by A2,TARSKI:2
.= a|support(a) by A1,RELAT_1:74;
hence thesis by A2,TARSKI:2;
end;
theorem Th53:
for I be non empty set, G be Group,
F be Group-Family of I,
sx,sy being Element of sum F,
x,y,xy be finite-support Function of I,G
st (for i be Element of I holds F.i is Subgroup of G)
& (for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi)
& sx = x & sy = y & sx * sy = xy
holds Product xy = Product(x) * Product(y)
proof
let I be non empty set,
G be Group,
F be Group-Family of I,
sx, sy being Element of sum F,
x,y,xy be finite-support Function of I,G;
assume that
A1: for i be Element of I holds F.i is Subgroup of G and
A2: for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi and
A3: sx = x & sy = y & sx * sy = xy;
reconsider W = support(x) \/ support(y) as finite Subset of I;
A9: sx in sum F; then
x in product F by A3,GROUP_2:40; then
reconsider px = x as Element of product F;
A10: sy in sum F; then
y in product F by A3,GROUP_2:40; then
reconsider py = y as Element of product F;
A11: sx * sy in sum F; then
xy in product F by A3,GROUP_2:40; then
reconsider pxy = xy as Element of product F;
for i be object st i in support(xy) holds i in W
proof
let i be object;
assume
A12: i in support xy;
i in W
proof
assume
A13: not i in W;
reconsider i as Element of I by A12;
A14: not i in support(x) & not i in support(y)
by A13,XBOOLE_0:def 3; then
A15: x.i = 1_G by Def2;
A16: y.i = 1_G by A14,Def2;
A17: F.i is Subgroup of G by A1;
x.i in F.i by A3,A9,Th5,GROUP_2:40; then
reconsider fxi = x.i as Element of F.i;
y.i in F.i by A3,A10,Th5,GROUP_2:40; then
reconsider fyi = y.i as Element of F.i;
xy.i = (px * py).i by A3,GROUP_2:43
.= fxi * fyi by GROUP_7:1
.= x.i * y.i by A17,GROUP_2:43
.= 1_G by A15,A16,GROUP_1:def 4;
hence contradiction by A12,Def2;
end;
hence i in W;
end; then
A22: support xy c= W;
A23: for a be Function of I,G, i,j be Element of I st a in product F
holds a.i * a.j = a.j * a.i
proof
let a be Function of I,G;
let i,j be Element of I;
assume
A24: a in product F; then
A25: a.i in F.i by Th5;
A26: a.j in F.j by A24,Th5;
per cases;
suppose
i = j;
hence thesis;
end;
suppose
i <> j;
hence thesis by A2,A25,A26;
end;
end;
for i,j be Element of I holds x.i * x.j = x.j * x.i
by A3,A9,A23,GROUP_2:40; then
A28: Product x = Product(x|W) by Th51,XBOOLE_1:7;
for i,j be Element of I holds y.i * y.j = y.j * y.i
by A3,A10,A23,GROUP_2:40; then
A34: Product y = Product(y|W) by Th51,XBOOLE_1:7;
for i,j be Element of I holds xy.i * xy.j = xy.j * xy.i
by A3,A11,A23,GROUP_2:40; then
A40: Product xy = Product(xy|W) by A22,Th51;
set cs = canFS(W);
reconsider wx = (x|W) * cs as FinSequence of G by Th50;
reconsider wy = (y|W) * cs as FinSequence of G by Th50;
reconsider wxy = (xy|W) * cs as FinSequence of G by Th50;
A41: rng cs = W by FUNCT_2:def 3;
W = dom(x|W) & W = dom(y|W) & W = dom(xy|W) by PARTFUN1:def 2; then
A43: dom cs = dom wx & dom cs = dom wy & dom cs = dom wxy
by A41,RELAT_1:27; then
dom cs = Seg len wx & dom cs = Seg len wy & dom cs = Seg len wxy
by FINSEQ_1:def 3; then
A45: len wxy = len wx & len wxy = len wy by FINSEQ_1:6;
A50: Product(x|W) = Product(wx) by GROUP_17:def 1;
A51: Product(y|W) = Product(wy) by GROUP_17:def 1;
A55: for i,j be Nat st i in dom wxy & j in dom wxy & i <> j
holds wx/.i * wy/.j = wy/.j * wx/.i
proof
let i,j be Nat;
assume
A56: i in dom wxy & j in dom wxy & i <> j; then
A57: cs.i in rng cs & cs.j in rng cs by A43,FUNCT_1:3; then
A59: cs.i in W & cs.j in W;
A60: wx/.i = wx.i by A43,A56,PARTFUN1:def 6
.= (x|W).(cs.i) by A43,A56,FUNCT_1:12
.= x.(cs.i) by A57,FUNCT_1:49;
A61: wy/.j = wy.j by A43,A56,PARTFUN1:def 6
.= (y|W).(cs.j) by A43,A56,FUNCT_1:12
.= y.(cs.j) by A57,FUNCT_1:49;
reconsider i0 = cs.i as Element of I by A59;
reconsider j0 = cs.j as Element of I by A59;
A64: x.i0 in F.i0 by A3,A9,Th5,GROUP_2:40;
reconsider gi = x.i0 as Element of G;
A65: y.j0 in F.j0 by A3,A10,Th5,GROUP_2:40;
reconsider gj = y.j0 as Element of G;
thus thesis by A2,A43,A56,A60,A61,A64,A65,FUNCT_1:def 4;
end;
A67: for i be Nat st i in dom wxy holds wxy.i = (wx/.i) * (wy/.i)
proof
let i be Nat;
assume
A68: i in dom wxy;
A70: cs.i in rng cs by A43,A68,FUNCT_1:3; then
A71: cs.i in W;
A72: wx/.i = wx.i by A43,A68,PARTFUN1:def 6
.= (x|W).(cs.i) by A43,A68,FUNCT_1:12
.= x.(cs.i) by A70,FUNCT_1:49;
A73: wy/.i = wy.i by A43,A68,PARTFUN1:def 6
.= (y|W).(cs.i) by A43,A68,FUNCT_1:12
.= y.(cs.i) by A70,FUNCT_1:49;
A74: wxy/.i = wxy.i by A68,PARTFUN1:def 6
.= (xy|W).(cs.i) by A68,FUNCT_1:12
.= xy.(cs.i) by A70,FUNCT_1:49;
reconsider i0 = cs.i as Element of I by A71;
A75: F.i0 is Subgroup of G by A1;
x.i0 in F.i0 by A3,A9,Th5,GROUP_2:40; then
reconsider fxi = x.i0 as Element of F.i0;
y.i0 in F.i0 by A3,A10,Th5,GROUP_2:40; then
reconsider fyi = y.i0 as Element of F.i0;
thus wxy.i = xy.i0 by A68,A74,PARTFUN1:def 6
.= (px * py).i0 by A3,GROUP_2:43
.= fxi * fyi by GROUP_7:1
.= (wx/.i) * (wy/.i) by A72,A73,A75,GROUP_2:43;
end;
Product(wxy) = Product(wx) * Product(wy) by A45,A55,A67,Th47;
hence thesis by A28,A34,A40,A50,A51,GROUP_17:def 1;
end;
theorem
for I be non empty set,
G be Group,
F be Group-Family of I
holds
F is internal DirectSumComponents of G,I
iff
(for i be Element of I holds F.i is Subgroup of G)
&(for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j holds gi * gj = gj * gi)
&(for y be Element of G
ex x be finite-support Function of I,G
st x in sum F & y = Product x)
&(for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds x1 = x2)
proof
let I be non empty set,
G be Group,
F be Group-Family of I;
hereby
assume
A0: F is internal DirectSumComponents of G,I; then
A1: (for i be Element of I holds F.i is Subgroup of G)
& ex h be Homomorphism of sum F,G
st h is bijective
& for a be finite-support Function of I,G st a in sum F
holds h.a = Product(a) by Def9;
A2: for i be object st i in I holds F.i is Subgroup of G
by A0,Def9;
consider h be Homomorphism of sum F,G such that
A3: h is bijective
& for a be finite-support Function of I,G st a in sum F
holds h.a = Product(a) by A0,Def9;
A4: for y be Element of G
ex x be finite-support Function of I,G
st x in sum F & y = Product x
proof
let y be Element of G;
rng h = the carrier of G by A3,FUNCT_2:def 3; then
consider x be Element of sum F such that
A5: y = h.x by FUNCT_2:113;
x in sum F; then
reconsider x as finite-support Function of I,G by A2,Th10;
take x;
thus x in sum F;
hence y = Product(x) by A3,A5;
end;
A6: for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product x1 = Product x2
holds x1 = x2
proof
let x1,x2 be finite-support Function of I,G;
assume
A7: x1 in sum F & x2 in sum F & Product x1 = Product x2;
reconsider sx1 = x1, sx2 = x2 as Element of sum F by A7;
h.sx1 = Product x1 by A3,A7
.= h.sx2 by A3,A7;
hence x1 = x2 by A3,FUNCT_2:19;
end;
for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi
proof
let i,j be Element of I, gi,gj be Element of G;
assume that
A10: i <> j and
A11: gi in F.i and
A12: gj in F.j;
set xi = 1_product F +* (i,gi);
set xj = 1_product F +* (j,gj);
1_sum F = 1_product F by GROUP_2:44; then
A13: 1_product F in sum F; then
A14: xi in sum F by A11,Th25;
A15: xj in sum F by A12,A13,Th25;
reconsider xi as finite-support Function of I,G
by A2,A11,A13,Th10,Th25;
reconsider xj as finite-support Function of I,G
by A2,A12,A13,Th10,Th25;
reconsider sxi = xi as Element of sum F by A14;
reconsider sxj = xj as Element of sum F by A15;
reconsider pxi = sxi as Element of product F by GROUP_2:42;
reconsider pxj = sxj as Element of product F by GROUP_2:42;
xi = (I --> 1_G) +* (i,gi) by A1,Th13; then
A17: Product xi = gi by Th21;
xj = (I --> 1_G) +* (j,gj) by A1,Th13; then
A18: Product xj = gj by Th21;
A19: support(pxi,F) misses support(pxj,F)
proof
A20: support(pxi,F) c= {i} by A11,Th17;
support(pxj,F) c= {j} by A12,Th17;
hence thesis by A10,A20,ZFMISC_1:11,XBOOLE_1:64;
end;
gi * gj = h.sxi * gj by A3,A11,A13,A17,Th25
.= h.sxi * h.sxj by A3,A12,A13,A18,Th25
.= h.(sxi * sxj) by GROUP_6:def 6
.= h.(pxi * pxj) by GROUP_2:43
.= h.(pxj * pxi) by A19,Th32
.= h.(sxj * sxi) by GROUP_2:43
.= h.sxj * h.sxi by GROUP_6:def 6
.= gj * h.sxi by A3,A12,A13,A18,Th25
.= gj * gi by A3,A11,A13,A17,Th25;
hence thesis;
end;
hence (for i be Element of I holds F.i is Subgroup of G)
& (for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j holds gi * gj = gj * gi)
& (for y be Element of G
ex x be finite-support Function of I,G
st x in sum F & y = Product x)
& (for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product x1 = Product x2
holds x1 = x2) by A0,A4,A6,Def9;
end;
assume
A32: (for i be Element of I holds F.i is Subgroup of G)
& (for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi)
& (for y be Element of G
ex x be finite-support Function of I,G
st x in sum F & y = Product x)
& (for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product x1 = Product x2
holds x1 = x2);
A33: for i be object st i in I holds F.i is Subgroup of G by A32;
defpred P[object,object] means
ex x be finite-support Function of I,G st $1 = x & $2 = Product x;
A34: for x being Element of sum F ex y being Element of G st P[x,y]
proof
let x be Element of sum F;
x in sum F; then
reconsider x as finite-support Function of I,G by A33,Th10;
Product x is Element of G;
hence thesis;
end;
consider h being Function of sum F,G such that
A35: for x being Element of sum F holds P[x,h.x] from FUNCT_2:sch 3(A34);
for y being object st y in [#]G
ex x being object st x in [#]sum F & y = h.x
proof
let y being object;
assume y in [#]G; then
reconsider y as Element of G;
consider x be finite-support Function of I,G such that
A36: x in sum F & y = Product x by A32;
ex x0 be finite-support Function of I,G
st x = x0 & h.x = Product x0 by A35,A36;
hence thesis by A36;
end; then
rng h = [#]G by FUNCT_2:10; then
A38: h is onto by FUNCT_2:def 3;
for x1,x2 being object st x1 in [#]sum F & x2 in [#]sum F & h.x1 = h.x2
holds x1 = x2
proof
let x1,x2 be object;
assume
A39: x1 in [#]sum F & x2 in [#]sum F & h.x1 = h.x2; then
reconsider sx1 = x1, sx2 = x2 as Element of sum F;
x1 in sum F by A39; then
reconsider x1 as finite-support Function of I,G by A33,Th10;
x2 in sum F by A39; then
reconsider x2 as finite-support Function of I,G by A33,Th10;
A40: ex x be finite-support Function of I,G
st x1 = x & h.x1 = Product x by A35,A39;
A42: ex x be finite-support Function of I,G
st x2 = x & h.x2 = Product x by A35,A39;
x1 in sum F & x2 in sum F by A39;
hence thesis by A32,A39,A40,A42;
end; then
A43: h is one-to-one by FUNCT_2:19;
A44: for a be finite-support Function of I,G st a in sum F
holds h.a = Product(a)
proof
let a be finite-support Function of I,G;
assume a in sum F; then
reconsider sa = a as Element of sum F;
ex x be finite-support Function of I,G
st sa = x & h.sa = Product x by A35;
hence h.a = Product(a);
end;
for x, y being Element of sum F holds h.(x * y) = h.x * h.y
proof
let x, y be Element of sum F;
consider x0 be finite-support Function of I,G such that
A45: x = x0 & h.x = Product x0 by A35;
consider y0 be finite-support Function of I,G such that
A46: y = y0 & h.y = Product y0 by A35;
consider xy0 be finite-support Function of I,G such that
A47: x * y = xy0 & h.(x * y) = Product xy0 by A35;
thus h.(x * y) = h.x * h.y by A32,A45,A46,A47,Th53;
end; then
reconsider h as Homomorphism of sum F,G by GROUP_6:def 6;
h is bijective by A38,A43;
hence F is internal DirectSumComponents of G,I by A32,A44,Def8,Def9;
end;