:: Conservation Rules of Direct Sum Decomposition of Groups
:: by Kazuhisa Nakasho , Hiroshi Yamazaki , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 31, 2015
:: Copyright (c) 2015-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, GROUP_2, CARD_1, FUNCT_4, GROUP_6, GROUP_7, FUNCT_7, FUNCOP_1,
ALGSTR_0, GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0,
NAT_1, FINSET_1, ZFMISC_1, PBOOLE, REALSET1, GROUP_4, PRE_POLY, UPROOTS,
GROUP_19, GROUP_20, MSSUBFAM, SEMI_AF1, VECTMETR, PROB_2, MONOID_0,
GROUP_21;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1,
FUNCT_4, FINSET_1, CARD_1, PBOOLE, CARD_3, FINSEQ_1, FUNCT_7, PROB_2,
STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_4, GROUP_6, MONOID_0,
PRALG_1, GRSOLV_1, GROUP_7, GROUP_12, GROUP_17, GROUP_19, GROUP_20;
constructors REALSET1, FUNCT_4, MONOID_0, PRALG_1, GROUP_4, FUNCT_7, RELSET_1,
WELLORD2, FUNCT_3, GROUP_17, GRSOLV_1, PROB_2, GROUP_19, GROUP_20;
registrations XBOOLE_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1, FUNCT_2,
CARD_1, GROUP_7, MSAFREE, PARTFUN1, RELSET_1, REALSET1, FINSEQ_1,
SUBSET_1, FINSET_1, RELAT_1, FUNCT_1, PBOOLE, GROUP_6, GROUP_19;
requirements NUMERALS, BOOLE, SUBSET;
definitions FUNCT_2, GROUP_19;
equalities STRUCT_0, GRSOLV_1, GROUP_19, REALSET1, CARD_3;
expansions STRUCT_0, TARSKI, GROUP_19, PROB_2, FUNCT_1, RELAT_1;
theorems FUNCT_1, CARD_3, FUNCT_2, FUNCOP_1, TARSKI, GROUP_1, GROUP_2,
FUNCT_4, FINSEQ_1, GROUP_4, GROUP_6, XTUPLE_0, XBOOLE_0, RELAT_1,
GROUP_7, SUBSET_1, FUNCT_7, BINOP_1, CARD_2, XBOOLE_1, ALGSTR_0,
GROUP_12, PARTFUN1, ZFMISC_1, CARD_1, GROUP_17, FINSET_1, GROUP_19,
GROUP_20, PROB_2, PENCIL_3;
schemes FUNCT_1, FUNCT_2, CLASSES1;
begin :: 1. Preliminaries
definition
let I,J be non empty set,
a be Function of I,J,
F be multMagma-Family of J;
redefine func F * a -> multMagma-Family of I; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
correctness
proof
reconsider E = F * a as ManySortedSet of I;
A1: dom a = I by FUNCT_2:def 1;
A2: dom E = I by PARTFUN1:def 2;
now
let x be set;
assume x in rng E; then
consider i be object such that
A3: i in I and
A4: E.i = x by A2,FUNCT_1:def 3;
reconsider j = a.i as Element of J by A3,FUNCT_2:5;
F.j is non empty multMagma;
hence x is non empty multMagma by A1,A3,A4,FUNCT_1:13;
end;
hence thesis by GROUP_7:def 1;
end;
end;
definition
let I,J be non empty set,
a be Function of I,J,
F be Group-Family of J;
redefine func F * a -> Group-Family of I; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
correctness
proof
reconsider E = F * a as ManySortedSet of I;
A1: dom a = I by FUNCT_2:def 1;
A2: dom E = I by PARTFUN1:def 2;
now
let i be object;
assume i in I; then
reconsider i1 = i as Element of I;
E.i1 = F.(a.i1) by A1,FUNCT_1:13;
hence E.i is Group;
end;
hence thesis by A2,GROUP_19:2;
end;
end;
definition
let I,J be non empty set,
a be Function of I,J,
G be Group,
F be Subgroup-Family of J,G;
func F * a -> Subgroup-Family of I,G equals
F * a;
correctness
proof
now
let i be object;
assume
A1: i in I; then
reconsider j = a.i as Element of J by FUNCT_2:5;
A2: F.j is Subgroup of G by GROUP_20:def 1;
dom a = I by FUNCT_2:def 1;
hence (F * a).i is Subgroup of G by A1,A2,FUNCT_1:13;
end;
hence thesis by GROUP_20:def 1;
end;
end;
scheme
Sch1{A()->set, B()->1-sorted, F(Element of B())->set}:
ex f being Function st
dom f = A() & for x being Element of B() st x in A() holds f.x = F(x)
proof
defpred P[object,object] means
($1 is Element of B() implies ex x being Element of B() st x=$1 & $2=F(x))
& (not $1 is Element of B() implies $2=0);
A1: for x being object st x in A() ex y being object st P[x,y]
proof
let x be object;
assume x in A();
per cases;
suppose
x is Element of B();
then reconsider z=x as Element of B();
take F(z);
thus thesis;
end;
suppose
x is not Element of B();
hence thesis;
end;
end;
consider f being Function such that
A2: dom f = A() and
A3: for x being object st x in A() holds P[x,f.x] from CLASSES1:sch 1(A1);
take f;
thus dom f = A() by A2;
let x be Element of B();
assume x in A();
then P[x,f.x] by A3;
hence f.x = F(x);
end;
registration
let I be set;
cluster non-empty disjoint_valued for ManySortedSet of I;
correctness
proof
deffunc DF(object) = {$1};
consider f being Function such that
A1: dom f = I &
for i be set st i in I holds f.i = DF(i) from FUNCT_1:sch 5;
reconsider f as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
take f;
not {} in rng f
proof
assume {} in rng f; then
consider x being object such that
A2: x in dom f & {} = f.x by FUNCT_1:def 3;
{} = {x} by A1,A2;
hence contradiction;
end;
hence f is non-empty;
for x,y be object st x <> y holds f.x misses f.y
proof
let x,y be object;
assume
A3: x <> y;
per cases;
suppose
not x in dom f or not y in dom f; then
f.x = {} or f.y = {} by FUNCT_1:def 2; then
f.x /\ f.y = {};
hence f.x misses f.y by XBOOLE_0:def 7;
end;
suppose
x in dom f & y in dom f; then
A4: f.x = {x} & f.y = {y} by A1;
{x} /\ {y} = {}
proof
assume {x} /\ {y} <> {}; then
consider z be object such that
A5: z in {x} /\ {y} by XBOOLE_0:def 1;
z in {x} & z in {y} by A5,XBOOLE_0:def 4; then
z = x & z = y by TARSKI:def 1;
hence contradiction by A3;
end;
hence f.x misses f.y by A4,XBOOLE_0:def 7;
end;
end;
hence f is disjoint_valued;
end;
end;
theorem Th30:
for f being non-empty disjoint_valued Function st Union f is finite
holds dom f is finite
proof
let f be non-empty disjoint_valued Function;
assume Union f is finite; then
A1: rng f is finite
& for X be set st X in rng f holds X is finite by FINSET_1:7;
for x,y be object st x in dom f & y in dom f & f.x = f.y holds x = y
proof
let x,y be object;
assume
A2: x in dom f & y in dom f & f.x = f.y;
assume x <> y; then
A3: f.x /\ f.y = {} by PROB_2:def 2,XBOOLE_0:def 7;
f.x in rng f by A2,FUNCT_1:3; then
consider i be object such that
A4: i in f.x by XBOOLE_0:def 1;
thus contradiction by A2,A3,A4;
end; then
f is one-to-one;
hence dom f is finite by A1,CARD_1:59;
end;
theorem Th35:
for X,Y be non empty set, X0,Y0 be set, f be Function of X,Y
st f is bijective & rng(f|X0) = Y0 holds (f|X0)" = f" | Y0
proof
let X,Y be non empty set, X0,Y0 be set, f be Function of X,Y;
assume that
A1: f is bijective and
A2: rng(f|X0) = Y0;
A3: rng f = dom(f") & dom f = rng(f") by A1,FUNCT_1:33;
A4: rng f = Y & Y = dom(f") by A1,A3,FUNCT_2:def 3;
A5: dom(f"|Y0) = Y0 by A2,A4,RELAT_1:62;
A6: f|X0 is one-to-one by A1,FUNCT_1:52; then
A7: rng(f|X0) = dom((f|X0)") & dom(f|X0) = rng((f|X0)") by FUNCT_1:33;
A8: dom((f|X0)") = Y0 by A2,A6,FUNCT_1:33;
for x be object st x in dom(f"|Y0) holds (f"|Y0).x = ((f|X0)").x
proof
let x be object;
assume x in dom(f"|Y0); then
A9: x in Y0 by A2,A4,RELAT_1:62; then
A10: (f"|Y0).x = f".x by FUNCT_1:49;
A11: x in dom((f|X0)") by A2,A6,A9,FUNCT_1:33;
A12: f|X0 c= f by RELAT_1:59;
for z be object st z in (f|X0)" holds z in f"
proof
let z be object;
assume
A13: z in (f|X0)"; then
consider x,y be object such that
A14: z = [x,y] by RELAT_1:def 1;
A15: x in dom((f|X0)") & y = ((f|X0)").x by A13,A14,FUNCT_1:1;
A16: x = (f|X0).y by A6,A7,A15,FUNCT_1:32;
y in rng((f|X0)") by A13,A14,XTUPLE_0:def 13; then
A17: [y,x] in f by A7,A12,A16,FUNCT_1:1; then
A18: y in dom f & x = f.y by FUNCT_1:1;
x in rng f by A17,XTUPLE_0:def 13; then
x in dom(f") & y = (f").x by A1,A18,FUNCT_1:32;
hence thesis by A14,FUNCT_1:1;
end; then
[x,((f|X0)").x] in f" by A11,FUNCT_1:1;
hence thesis by A10,FUNCT_1:1;
end;
hence thesis by A5,A8;
end;
begin :: 2. Conservation rule of direct sum decomposition
:: for substitution of subscript set
theorem Th1:
for I,J be non empty set,
a be Function of I,J,
F be multMagma-Family of J,
x be Element of product F
holds
x*a in product(F*a)
proof
let I,J be non empty set,
a be Function of I,J,
F be multMagma-Family of J,
x be Element of product F;
dom x = J by GROUP_19:3; then
rng a c= dom x; then
dom(x*a) = dom a by RELAT_1:27; then
dom(x*a) = I by PARTFUN1:def 2; then
reconsider y = x*a as ManySortedSet of I by PARTFUN1:def 2;
reconsider z = Carrier(F*a) as ManySortedSet of I;
A1: dom y = I by PARTFUN1:def 2;
A2: dom z = I by PARTFUN1:def 2;
A3: dom a = I by PARTFUN1:def 2;
for i be object st i in I holds y.i in z.i
proof
let i be object;
assume i in I; then
reconsider i as Element of I;
reconsider j = a.i as Element of J;
A4: z.i = [#]((F*a).i) by PENCIL_3:7
.= [#](F.j) by A3,FUNCT_1:13;
x in product F; then
x.j in F.j by GROUP_19:5;
hence thesis by A3,A4,FUNCT_1:13;
end; then
y in product z by A1,A2,CARD_3:def 5;
hence thesis by GROUP_7:def 2;
end;
definition
let I,J be non empty set;
let a be Function of I,J;
let F be multMagma-Family of J;
func trans_prod(F,a) -> Function of product F, product(F*a) means
:Def2:
for x be Element of product F holds it.x = x*a;
existence
proof
deffunc DF(Element of product F) = $1 * a;
consider f be Function such that
A1: dom f = [#] product F and
A2: for x being Element of product F st x in [#] product F
holds f.x = DF(x) from Sch1;
now
let y be object;
assume y in rng f; then
consider x be object such that
A3: x in dom f and
A4: f.x = y by FUNCT_1:def 3;
reconsider x as Element of product F by A1,A3;
x*a in product(F*a) by Th1;
hence y in [#] product(F*a) by A2,A4;
end; then
rng f c= [#] product(F*a); then
reconsider f as Function of product F, product(F*a) by A1,FUNCT_2:2;
take f;
thus thesis by A2;
end;
uniqueness
proof
let f0,f1 be Function of product F, product(F*a);
assume
A5: for x be Element of product F holds f0.x = x*a;
assume
A6: for x be Element of product F holds f1.x = x*a;
A7: dom f1 = [#](product F) by PARTFUN1:def 2;
for x be object st x in dom f0 holds f0.x = f1.x
proof
let x be object;
assume x in dom f0; then
reconsider x as Element of product F;
f0.x = x*a by A5
.= f1.x by A6;
hence thesis;
end;
hence f0 = f1 by A7,PARTFUN1:def 2;
end;
end;
theorem Th2:
for I,J be non empty set,
a be Function of I,J,
F be multMagma-Family of J
holds trans_prod(F,a) is multiplicative
proof
let I,J be non empty set,
a be Function of I,J,
F be multMagma-Family of J;
reconsider f = trans_prod(F,a) as Function of product F, product(F*a);
for x,y be Element of product F holds f.(x * y) = f.x * f.y
proof
let x,y be Element of product F;
A1: f.(x * y) = (x * y) * a by Def2;
A2: f.x = x * a by Def2;
x * a in product(F*a) by Th1; then
reconsider xa = x * a as Element of product(F*a);
y * a in product(F*a) by Th1; then
reconsider ya = y * a as Element of product(F*a);
A3: dom(xa * ya) = I by GROUP_19:3;
A4: dom a = I by FUNCT_2:def 1;
dom(x * y) = J by GROUP_19:3; then
A5: rng a c= dom(x * y);
for i be object st i in I holds (xa * ya).i = ((x * y) * a).i
proof
let i be object;
assume i in I; then
reconsider i as Element of I;
reconsider Fai = (F*a).i as multMagma;
reconsider j = a.i as Element of J;
reconsider Fj = F.j as multMagma;
xa in product(F*a); then
xa.i in (F*a).i by GROUP_19:5; then
reconsider xai = xa.i as Element of Fai;
ya in product(F*a); then
ya.i in (F*a).i by GROUP_19:5; then
reconsider yai = ya.i as Element of Fai;
x in product F; then
x.j in F.j by GROUP_19:5; then
reconsider xj = x.j as Element of Fj;
y in product F; then
y.j in F.j by GROUP_19:5; then
reconsider yj = y.j as Element of Fj;
A6: xa.i = x.j by A4,FUNCT_1:13;
A7: ya.i = y.j by A4,FUNCT_1:13;
((x * y) * a).i = (x * y).j by A4,FUNCT_1:13
.= xj * yj by GROUP_7:1
.= xai * yai by A4,A6,A7,FUNCT_1:13
.= (xa * ya).i by GROUP_7:1;
hence thesis;
end; then
xa * ya = (x * y) * a by A3,A4,A5,RELAT_1:27;
hence thesis by A1,A2,Def2;
end;
hence thesis by GROUP_6:def 6;
end;
definition
let I,J be non empty set;
let a be Function of I,J;
let F be Group-Family of J;
redefine func trans_prod(F,a) -> Homomorphism of product F, product(F*a); :: redefines trans_prod (GROUP_21, definition)
correctness by Th2;
end;
theorem Th3:
for I,J be non empty set,
a be Function of I,J,
F be multMagma-Family of J,
y be Element of product(F*a)
st a is bijective
holds y * a" in product F
proof
let I,J be non empty set,
a be Function of I,J,
F be multMagma-Family of J,
y be Element of product(F*a);
assume
A1: a is bijective; then
A2: dom a = I & rng a = J by GROUP_6:61; then
A3: dom(a") = J & rng(a") = I by A1,FUNCT_1:33;
set x = y * a";
dom y = I by GROUP_19:3; then
A4: dom x = J by A3,RELAT_1:27;
A5: dom(Carrier F) = J by PARTFUN1:def 2;
for j be object st j in J holds x.j in (Carrier F).j
proof
let j be object;
assume j in J; then
reconsider j as Element of J;
consider i be object such that
A6: i in I & j = a.i by A2,FUNCT_1:def 3;
reconsider i as Element of I by A6;
i = (a").j by A1,A2,A6,FUNCT_1:32; then
A7: x.j = y.i by A3,FUNCT_1:13;
A8: (Carrier F).j = [#](F.j) by PENCIL_3:7;
y in product(F*a); then
y.i in (F*a).i by GROUP_19:5;
hence thesis by A2,A6,A7,A8,FUNCT_1:13;
end; then
x in product(Carrier F) by A4,A5,CARD_3:def 5;
hence thesis by GROUP_7:def 2;
end;
theorem Th4:
for I,J be non empty set, a be Function of I,J, x,y be Function
st dom x = I & dom y = J & a is bijective
holds x = y * a iff y = x * a"
proof
let I,J be non empty set,
a be Function of I,J,
x,y be Function;
assume that
A1: dom x = I and
A2: dom y = J and
A3: a is bijective;
A4: dom a = I & rng a = J by A3,GROUP_6:61;
hereby
assume
A5: x = y * a;
thus y = y * (id J) by A2,RELAT_1:51
.= y * (a * a") by A3,A4,FUNCT_2:29
.= x * a" by A5,RELAT_1:36;
end;
assume
A6: y = x * a";
thus x = x * (id I) by A1,RELAT_1:51
.= x * (a" * a) by A3,A4,FUNCT_2:29
.= y * a by A6,RELAT_1:36;
end;
theorem Th5:
for I,J be non empty set,
F be multMagma-Family of J,
a be Function of I,J st a is bijective
holds dom trans_prod(F,a) = [#] product(F)
& rng trans_prod(F,a) = [#] product(F*a)
proof
let I,J be non empty set,
F be multMagma-Family of J,
a be Function of I,J;
assume
A1: a is bijective;
set f = trans_prod(F,a);
for y be object st y in [#] product(F*a) holds
ex x be object st x in [#] product(F) & y = f.x
proof
let y be object;
assume y in [#] product(F*a); then
reconsider y as Element of product(F*a);
set x = y * a";
x in product F by A1,Th3; then
reconsider x as Element of product F;
dom x = J & dom y = I by GROUP_19:3; then
y = x * a by A1,Th4; then
y = f.x by Def2;
hence thesis;
end;
hence thesis by FUNCT_2:10,def 1;
end;
theorem Th6:
for I,J be non empty set,
a be Function of I,J,
F be multMagma-Family of J
st a is bijective
holds trans_prod(F,a) is bijective
proof
let I,J be non empty set,
a be Function of I,J,
F be multMagma-Family of J;
assume
A1: a is bijective;
reconsider f = trans_prod(F,a) as Function of product F, product(F*a);
A2: dom f = [#](product F) & rng f = [#] product(F*a) by A1,Th5;
for x,y be object st x in dom f & y in dom f & f.x = f.y holds x = y
proof
let x,y be object;
assume that
A3: x in dom f and
A4: y in dom f and
A5: f.x = f.y;
reconsider x as Element of product F by A3;
reconsider y as Element of product F by A4;
A6: dom x = J & dom y = J by GROUP_19:3;
A7: rng a = J by A1,FUNCT_2:def 3;
f.x = x * a by Def2; then
x * a = y * a by A5,Def2;
hence thesis by A6,A7,FUNCT_1:86;
end; then
A8: f is one-to-one;
f is onto by A2,FUNCT_2:def 3;
hence thesis by A8;
end;
theorem Th7:
for I,J be non empty set,
a be Function of I,J,
F be Group-Family of J,
x be Function
holds a .: support(x*a, F*a) c= support(x,F)
proof
let I,J be non empty set,
a be Function of I,J,
F be Group-Family of J,
x be Function;
for j be object st j in a .: support(x*a, F*a) holds j in support(x,F)
proof
let j be object;
assume j in a .: support(x*a, F*a); then
consider i be object such that
A1: i in dom a and
A2: i in support(x*a, F*a) and
A3: j = a.i by FUNCT_1:def 6;
consider Z being Group such that
B1: Z = (F*a).i & (x*a).i <> 1_Z & i in I by A2,GROUP_19:def 1;
reconsider y = x*a as Function;
reconsider G = F*a as Group-Family of I;
reconsider i as Element of I by B1;
j = a.i by A3; then
reconsider j as Element of J;
A5: 1_G.i = 1_F.j by A1,A3,FUNCT_1:13;
x.j <> 1_F.j by A1,A3,B1,A5,FUNCT_1:13;
hence thesis by GROUP_19:def 1;
end;
hence thesis;
end;
theorem Th8:
for I,J be non empty set,
a be Function of I,J,
F be Group-Family of J,
x be Function
st a is onto
holds support(x,F) c= a .: support(x*a,F*a)
proof
let I,J be non empty set,
a be Function of I,J,
F be Group-Family of J,
x be Function;
assume
A1: a is onto;
for j be object st j in support(x,F) holds j in a .: support(x*a,F*a)
proof
let j be object;
assume
A2: j in support(x,F);
A3: dom a = I by FUNCT_2:def 1;
rng a = J by A1,FUNCT_2:def 3; then
consider i be object such that
A4: i in I and
A5: j = a.i by A2,FUNCT_2:11;
reconsider y = x*a as Function;
reconsider G = F*a as Group-Family of I;
consider Z being Group such that
B1: Z = F.j & x.j <> 1_Z & j in J by A2,GROUP_19:def 1;
reconsider j as Element of J by B1;
reconsider i as Element of I by A4;
A6: 1_G.i = 1_F.j by A3,A5,FUNCT_1:13;
x.j = y.i by A3,A5,FUNCT_1:13; then
i in support(y,G) by A6,B1,GROUP_19:def 1;
hence thesis by A3,A5,FUNCT_1:def 6;
end;
hence thesis;
end;
theorem Th9:
for I,J be non empty set,
a be Function of I,J,
F be Group-Family of J,
x be Function
st a is one-to-one
holds x in sum F implies x*a in sum(F*a)
proof
let I,J be non empty set,
a be Function of I,J,
F be Group-Family of J,
x be Function;
assume
A1: a is one-to-one;
assume
A2: x in sum F; then
x in product F by GROUP_2:40; then
reconsider x as Element of product F;
reconsider Fa = F*a as Group-Family of I;
x*a in product(F*a) by Th1; then
reconsider xa = x*a as Element of product(F*a);
A3: dom a = I by FUNCT_2:def 1;
A4: a .: support(xa,Fa) c= support(x,F) by Th7;
a .: support(xa,Fa), support(xa,Fa) are_equipotent by A1,A3,CARD_1:33; then
support(xa,Fa) is finite by A2,A4,CARD_1:38;
hence thesis by GROUP_19:8;
end;
theorem Th10:
for I,J be non empty set,
a be Function of I,J,
F be Group-Family of J,
x be Function
st a is bijective
holds x in sum F iff x*a in sum(F*a) & dom x = J
proof
let I,J be non empty set,
a be Function of I,J,
F be Group-Family of J,
x be Function;
assume
A1: a is bijective;
hereby
assume
A2: x in sum F; then
x in product F by GROUP_2:40;
hence x*a in sum(F*a) & dom x = J by A1,A2,Th9,GROUP_19:3;
end;
assume
A3: x*a in sum(F*a) & dom x = J;
A4: rng a = J & a is one-to-one by A1,FUNCT_2:def 3; then
reconsider b = a" as Function of J,I by FUNCT_2:25;
A5: a * b = id J & b * a = id I by A4,FUNCT_2:29;
A6: dom F = J by PARTFUN1:def 2;
(x*a)*b in sum((F*a)*b) by A3,A1,Th9; then
x*(a*b) in sum((F*a)*b) by RELAT_1:36; then
x*(id J) in sum(F*(id J)) by A5,RELAT_1:36; then
x in sum(F*(id J)) by A3,RELAT_1:52;
hence x in sum F by A6,RELAT_1:52;
end;
definition
let I,J be non empty set;
let a be Function of I,J;
let F be Group-Family of J;
assume
A1: a is bijective;
func trans_sum(F,a) -> Function of sum F, sum(F*a) equals :Def3:
trans_prod(F,a) | (sum F);
correctness
proof
set f = trans_prod(F,a);
set g = f | (sum F);
set G = F * a;
A2: dom g = [#] sum F by FUNCT_2:def 1;
for y be object st y in rng g holds y in [#] sum G
proof
let y be object;
assume
A3: y in rng g; then
consider x be object such that
A4: x in dom g and
A5: y = g.x by FUNCT_1:def 3;
[#] sum F c= [#] product F by GROUP_2:def 5;
then
reconsider x as Element of product F by A4;
reconsider y as Element of product G by A3;
A6: dom a = I by FUNCT_2:def 1;
y = f.x by A4,A5,FUNCT_1:49; then
A7: y = x * a by Def2; then
A8: a .: support(y,G) c= support(x,F) by Th7;
support(x,F) c= a .: support(y,G) by A1,A7,Th8; then
a".:support(x,F) = a".:(a.:support(y,G)) by A8,XBOOLE_0:def 10; then
support(y,G) is finite by A1,A4,A6,FUNCT_1:107; then
y in sum G by GROUP_19:8;
hence thesis;
end;
hence thesis by A2,FUNCT_2:2,TARSKI:def 3;
end;
end;
theorem Th11:
for G,H be Group,
H0 be Subgroup of H,
f be Homomorphism of G,H
st rng f c= [#]H0
holds f is Homomorphism of G,H0
proof
let G,H be Group,
H0 be Subgroup of H,
f be Homomorphism of G,H;
assume rng f c= [#]H0; then
reconsider g = f as Function of G,H0 by FUNCT_2:6;
for a,b be Element of G holds g.(a * b) = g.a * g.b
proof
let a,b be Element of G;
g.(a * b) = f.a * f.b by GROUP_6:def 6
.= g.a * g.b by GROUP_2:43;
hence thesis;
end;
hence thesis by GROUP_6:def 6;
end;
theorem TT:
for I,J be non empty set
for a be Function of I,J
for F be Group-Family of J st a is bijective holds
trans_sum(F,a) is Homomorphism of sum F, sum(F*a)
proof
let I,J be non empty set;
let a be Function of I,J;
let F be Group-Family of J;
assume
A1: a is bijective;
set f = trans_sum(F,a);
A2: f = trans_prod(F,a) | (sum F) by A1,Def3;
rng f c= [#] sum(F*a);
hence thesis by A2,Th11;
end;
theorem Th12:
for I,J be non empty set,
a be Function of I,J,
F be Group-Family of J
st a is bijective
holds trans_sum(F,a) is bijective
proof
let I,J be non empty set,
a be Function of I,J,
F be Group-Family of J;
assume
A1: a is bijective;
reconsider f = trans_prod(F,a) as Homomorphism of product F,product(F*a);
reconsider g = trans_sum(F,a) as Homomorphism of sum F,sum(F*a) by A1,TT;
A2: g = f | (sum F) by A1,Def3;
f is bijective by A1,Th6; then
A3: g is one-to-one by A2,FUNCT_1:52;
for y be object st y in [#] sum(F*a) holds y in rng g
proof
let y be object;
assume
A4: y in [#] sum(F*a); then
reconsider y as Element of product(F*a) by GROUP_2:42;
set x = y * a";
x in product F by A1,Th3; then
reconsider x as Element of product F;
A5: dom g = [#] sum F by FUNCT_2:def 1;
A6: dom x = J & dom y = I by GROUP_19:3; then
A7: y = x * a by A1,Th4;
y in sum(F*a) by A4; then
A8: x in sum F by A1,A6,A7,Th10;
y = f.x by A7,Def2; then
y = g.x by A2,A8,FUNCT_1:49;
hence thesis by A5,A8,FUNCT_1:def 3;
end; then
[#] sum(F*a) c= rng g; then
g is onto by FUNCT_2:def 3,XBOOLE_0:def 10;
hence thesis by A3;
end;
:: independent from subscript set
theorem Th13:
for G be Group,
I,J be non empty set,
F be DirectSumComponents of G,J,
a be Function of I,J st a is bijective
holds F * a is DirectSumComponents of G,I
proof
let G be Group,
I,J be non empty set,
F be DirectSumComponents of G,J,
a be Function of I,J;
assume
A1: a is bijective;
consider h1 be Homomorphism of sum F,G such that
A2: h1 is bijective by GROUP_19:def 8;
reconsider h2 = trans_sum(F,a) as Homomorphism of sum F,sum(F*a) by A1,TT;
A3: h2 is bijective by A1,Th12;
then reconsider h3 = h2" as Homomorphism of sum(F*a),sum F
by GROUP_6:62;
reconsider h = h1 * h3 as Homomorphism of sum(F*a),G;
h3 is bijective by A3,GROUP_6:63; then
h is bijective by A2,GROUP_6:64;
hence thesis by GROUP_19:def 8;
end;
theorem
for I be non empty set,
G be Group,
F be internal DirectSumComponents of G,I
holds F is Subgroup-Family of I,G
proof
let I be non empty set,
G be Group,
F be internal DirectSumComponents of G,I;
for i be object st i in I holds F.i is Subgroup of G by GROUP_19:def 9;
hence thesis by GROUP_20:def 1;
end;
theorem Th15:
for I,J be non empty set,
G be Group,
x be Function of I,G,
y be Function of J,G,
a be Function of I,J
st a is onto & x = y * a
holds support(y) = a .: support(x)
proof
let I,J be non empty set,
G be Group,
x be Function of I,G,
y be Function of J,G,
a be Function of I,J;
assume that
A1: a is onto and
A2: x = y * a;
A3: rng a = J by A1,FUNCT_2:def 3;
now
let j be object;
assume
A4: j in support(y); then
consider i be object such that
A5: i in dom a and
A6: j = a.i by A3,FUNCT_1:def 3;
x.i = y.j by A2,A5,A6,FUNCT_1:13; then
x.i <> 1_G by A4,GROUP_19:def 2; then
i in support(x) by A5,GROUP_19:def 2;
hence j in a .: support(x) by A5,A6,FUNCT_1:def 6;
end; then
A7: support(y) c= a .: support(x);
now
let j be object;
assume j in a .: support(x); then
consider i be object such that
A8: i in dom a and
A9: i in support(x) and
A10: j = a.i by FUNCT_1:def 6;
A11: j in J by A8,A10,FUNCT_2:5;
x.i = y.j by A2,A8,A10,FUNCT_1:13; then
y.j <> 1_G by A9,GROUP_19:def 2;
hence j in support(y) by A11,GROUP_19:def 2;
end; then
a .: support(x) c= support(y);
hence thesis by A7,XBOOLE_0:def 10;
end;
theorem Th16:
for I,J be non empty set,
G be commutative Group,
x be finite-support Function of I,G,
y be finite-support Function of J,G,
a be Function of I,J
st a is bijective & x = y * a
holds Product x = Product y
proof
let I,J be non empty set,
G be commutative Group,
x be finite-support Function of I,G,
y be finite-support Function of J,G,
a be Function of I,J;
assume that
A1: a is bijective and
A2: x = y * a;
A3: dom a = I by FUNCT_2:def 1;
A4: rng a = J by A1,FUNCT_2:def 3;
reconsider Sx = support(x) as finite set;
reconsider Sy = support(y) as finite set;
reconsider cx = canFS(Sx) as FinSequence of Sx;
reconsider cy = canFS(Sy) as FinSequence of Sy;
reconsider x1 = x|Sx as Function of Sx,G by FUNCT_2:32;
consider x2 be FinSequence of G such that
A5: Product x1 = Product x2 and
A6: x2 = x1 * cx by GROUP_17:def 1;
reconsider y1 = y|Sy as Function of Sy,G by FUNCT_2:32;
consider y2 be FinSequence of G such that
A7: Product y1 = Product y2 and
A8: y2 = y1 * cy by GROUP_17:def 1;
A9: Sy = a .: Sx by A1,A2,Th15;
A10: card Sx = card Sy
proof
A11: card Sy c= card Sx by A9,CARD_1:66;
reconsider ia = a" as Function of J,I by A1,A4,FUNCT_2:25;
A12: ia is bijective by A1,GROUP_6:63;
y = y * id J by FUNCT_2:17
.= y * (a * ia) by A1,A4,FUNCT_2:29
.= x * ia by A2,RELAT_1:36; then
Sx = ia .: Sy by A12,Th15; then
card Sx c= card Sy by CARD_1:66;
hence thesis by A11,XBOOLE_0:def 10;
end;
reconsider n = card Sx as Nat;
reconsider a1 = a|Sx as Function of Sx,J by FUNCT_2:32;
A13: dom a1 = Sx by FUNCT_2:def 1;
A14: rng a1 = Sy by A9,RELAT_1:115; then
reconsider a1 as Function of Sx,Sy by A13,FUNCT_2:1;
A15: len cx = n by FINSEQ_1:93; then
A16: dom cx = Seg n by FINSEQ_1:def 3;
A17: rng cx = Sx by FUNCT_2:def 3; then
reconsider cx as Function of Seg n, Sx by A16,FUNCT_2:1;
len cy = n by A10,FINSEQ_1:93; then
A18: dom cy = Seg n by FINSEQ_1:def 3;
A19: rng cy = Sy by FUNCT_2:def 3; then
reconsider cy as Function of Seg n, Sy by A18,FUNCT_2:1;
reconsider icy = cy" as Function of Sy, Seg n by A10,FINSEQ_1:95;
reconsider p = icy * a1 * cx as Function;
A20: dom a1 = rng cx by A13,FUNCT_2:def 3;
A21: dom icy = rng a1 by A14,A19,FUNCT_1:33;
A22: dom(a1 * cx) = dom cx by A20,RELAT_1:27;
A23: rng(a1 * cx) = rng a1 by A20,RELAT_1:28;
A24: dom p = dom(icy * (a1 * cx)) by RELAT_1:36
.= dom(a1 * cx) by A21,A23,RELAT_1:27
.= dom cx by A20,RELAT_1:27
.= Seg n by A15,FINSEQ_1:def 3;
A25: rng p = rng(icy * (a1 * cx)) by RELAT_1:36
.= rng icy by A21,A23,RELAT_1:28
.= Seg n by A18,FUNCT_1:33;
reconsider p as Function of Seg n,Seg n by A24,A25,FUNCT_2:1;
rng cy = dom y1 by A19,FUNCT_2:def 1; then
A26: dom y2 = Seg n by A8,A18,RELAT_1:27;
a1 is one-to-one by A1,FUNCT_1:52; then
p is one-to-one onto by A25,FUNCT_2:def 3; then
reconsider p as Permutation of dom y2 by A26;
A27: Sy is not empty implies x2 = y2 * p
proof
assume
A28: Sy is not empty;
A29: dom x1 = Sx by FUNCT_2:def 1; then
A30: dom x2 = Seg n by A6,A16,A17,RELAT_1:27;
for i be object st i in dom x2 holds x2.i = (y2 * p).i
proof
let i be object;
assume
A31: i in dom x2; then
A32: i in Seg n by A6,A16,A17,A29,RELAT_1:27;
A33: cx.i in Sx by A16,A17,A30,A31,FUNCT_1:3;
A34: x2.i = x1.(cx.i) by A6,A31,FUNCT_1:12
.= x.(cx.i) by A16,A17,A29,A30,A31,FUNCT_1:3,47;
A35: y1 * (cy * icy) = y1 * id(Sy) by A19,A28,FUNCT_2:29
.= y1 by FUNCT_2:17;
A36: y2 * p = (y1 * cy) * (icy * (a1 * cx)) by A8,RELAT_1:36
.= (y1 * cy * icy) * (a1 * cx) by RELAT_1:36
.= y1 * (a1 * cx) by A35,RELAT_1:36;
A37: (a1 * cx).i = a1.(cx.i) by A16,A32,FUNCT_1:13
.= a.(cx.i) by A16,A17,A30,A31,FUNCT_1:3,49;
(y2 * p).i = y1.((a1 * cx).i) by A16,A22,A32,A36,FUNCT_1:13
.= y.(a.(cx.i)) by A14,A16,A22,A23,A32,A37,FUNCT_1:3,49
.= x2.i by A2,A3,A33,A34,FUNCT_1:13;
hence thesis;
end;
hence thesis by A24,A25,A26,A30,RELAT_1:27;
end;
per cases;
suppose
A38: Sy is empty; then
Sx is empty by A10;
hence thesis by A38;
end;
suppose
Sy is not empty;
hence thesis by A5,A7,A27,GROUP_4:15;
end;
end;
theorem
for I,J be non empty set,
G be Group,
x be finite-support Function of I,G,
y be finite-support Function of J,G,
a be Function of I,J
st a is bijective & x = y * a
& for i,j be Element of I holds x.i * x.j = x.j * x.i
holds Product x = Product y
proof
let I,J be non empty set,
G be Group,
x be finite-support Function of I,G,
y be finite-support Function of J,G,
a be Function of I,J;
assume that
A1: a is bijective and
A2: x = y * a and
A3: for i,j be Element of I holds x.i * x.j = x.j * x.i;
reconsider rx = rng x as non empty Subset of G;
reconsider ry = rng y as non empty Subset of G;
A4: dom y = J by FUNCT_2:def 1;
A5: rng a = J by A1,FUNCT_2:def 3;
A6: gr(rx) = gr(ry) by A2,A4,A5,RELAT_1:28;
rng x c= [#]gr(rx) by GROUP_4:def 4; then
reconsider x1 = x as finite-support Function of I,gr(rx) by GROUP_20:5;
rng y c= [#]gr(ry) by GROUP_4:def 4; then
reconsider y1 = y as finite-support Function of J,gr(rx) by A6,GROUP_20:5;
now
let a,b be Element of G;
assume that
A7: a in rx and
A8: b in rx;
consider i be object such that
A9: i in dom x and
A10: a = x.i by A7,FUNCT_1:def 3;
consider j be object such that
A11: j in dom x and
A12: b = x.j by A8,FUNCT_1:def 3;
reconsider i as Element of I by A9;
reconsider j as Element of I by A11;
x.i * x.j = x.j * x.i by A3;
hence a * b = b * a by A10,A12;
end; then
gr(rx) is commutative by GROUP_19:44; then
A14: Product x1 = Product y1 by A1,A2,Th16;
Product x = Product x1 by GROUP_20:6;
hence thesis by A14,GROUP_20:6;
end;
theorem
for G be Group,
I,J be non empty set,
F be internal DirectSumComponents of G,J,
a be Function of I,J st a is bijective
holds F * a is internal DirectSumComponents of G,I
proof
let G be Group,
I,J be non empty set,
F be internal DirectSumComponents of G,J,
a be Function of I,J;
assume
A1: a is bijective; then
reconsider E = F*a as DirectSumComponents of G,I by Th13;
A2: for i be Element of I holds E.i is Subgroup of G
proof
let i be Element of I;
A3: dom a = I by FUNCT_2:def 1;
reconsider j = a.i as Element of J;
F.j is Subgroup of G by GROUP_19:def 9;
hence thesis by A3,FUNCT_1:13;
end;
A4: for i be object st i in I holds E.i is Subgroup of G by A2;
ex h be Homomorphism of sum E, G
st h is bijective
& for x be finite-support Function of I,G st x in sum E holds
h.x = Product x
proof
consider hFG be Homomorphism of sum F,G such that
A5: hFG is bijective and
A6: for y be finite-support Function of J,G st y in sum F holds
hFG.y = Product y by GROUP_19:def 9;
reconsider hFE = trans_sum(F,a) as Homomorphism of sum F, sum E by A1,TT;
A7: hFE is bijective by A1,Th12;
then reconsider hEF = hFE" as Homomorphism of sum E, sum F
by GROUP_6:62;
reconsider h = hFG * hEF as Homomorphism of sum E, G;
take h;
A8: hEF is bijective by A7,GROUP_6:63;
A9: for i be Element of I, g be Element of E.i
holds h.(1ProdHom(E,i).g) = g
proof
let i be Element of I, g be Element of E.i;
1_product E +* (i,g) in sum E by GROUP_19:25,GROUP_2:46; then
reconsider x = 1_product E +* (i,g) as Element of sum E;
reconsider j = a.i as Element of J;
A10: dom a = I by FUNCT_2:def 1; then
A11: E.i = F.j by FUNCT_1:13;
reconsider g1 = g as Element of F.j by A10,FUNCT_1:13;
F.j is Subgroup of G by A2,A11; then
[#](F.j) c= [#]G by GROUP_2:def 5; then
reconsider g2 = g1 as Element of G;
reconsider y = hEF.x as Element of sum F;
A12: for j be object st j in J holds F.j is Subgroup of G
by GROUP_19:def 9;
y in sum F; then
reconsider y1 = y as finite-support Function of J,G by A12,GROUP_19:10;
A13: hFE = trans_prod(F,a) | (sum F) by A1,Def3;
A14: x = y * a
proof
reconsider y2 = y1 as Element of product F by GROUP_2:42;
A15: rng hFE = [#](sum E) by A7,FUNCT_2:def 3;
A16: dom hEF = [#](sum E) by FUNCT_2:def 1;
x = (id [#](sum E)).x
.= (hFE * hEF).x by A7,A15,FUNCT_2:29
.= hFE.y by A16,FUNCT_1:13
.= trans_prod(F,a).y2 by A13,FUNCT_1:49
.= y2 * a by Def2;
hence thesis;
end;
A17: y = (J --> 1_G) +* (j, g2)
proof
reconsider z = (J --> 1_G) +* (j, g2) as Function;
y is Element of product F by GROUP_2:42; then
A18: dom y = J by GROUP_19:3;
A19: dom(J --> 1_G) = J by FUNCOP_1:13;
for j0 be object st j0 in J holds y.j0 = z.j0
proof
let j0 be object;
assume
j0 in J; then
reconsider j0 as Element of J;
A20: dom(1_product E) = I by GROUP_19:3;
per cases;
suppose
A21: j0 = j; then
y.j0 = x.i by A10,A14,FUNCT_1:13
.= g by A20,FUNCT_7:31;
hence thesis by A19,A21,FUNCT_7:31;
end;
suppose
A22: j0 <> j;
A23: a is one-to-one & rng a = J by A1,FUNCT_2:def 3; then
reconsider ia = a" as Function of J,I by FUNCT_2:25;
reconsider i0 = ia.j0 as Element of I;
A24: ia.j = (ia * a).i by A10,FUNCT_1:13
.= (id I).i by A23,FUNCT_2:29
.= i;
A25: dom ia = J by FUNCT_2:def 1;
A26: ia is one-to-one by A1;
A27: j0 = (id J).j0
.= (a * ia).j0 by A23,FUNCT_2:29
.= a.i0 by A25,FUNCT_1:13;
A28: y.j0 = (y*a).i0 by A10,A27,FUNCT_1:13
.= (1_product E).i0 by A14,A22,A24,A25,A26,FUNCT_7:32
.= (I --> 1_G).i0 by A2,GROUP_19:13
.= 1_G by FUNCOP_1:7;
z.j0 = (J --> 1_G).j0 by A22,FUNCT_7:32
.= 1_G by FUNCOP_1:7;
hence thesis by A28;
end;
end;
hence thesis by A18,A19,FUNCT_7:30;
end;
y in sum F; then
A29: hFG.y = Product y1 by A6
.= g2 by A17,GROUP_19:21;
x in sum E; then
A30: x in dom hEF by FUNCT_2:def 1;
h.x = g by A29,A30,FUNCT_1:13;
hence thesis by GROUP_12:def 3;
end;
E is Subgroup-Family of I,G by A4,GROUP_20:def 1;
hence thesis by A5,A8,A9,GROUP_20:18,GROUP_6:64;
end;
hence thesis by A2,GROUP_19:def 9;
end;
begin :: 3. Conservation rule of direct sum decomposition for flattening
definition
let I be non empty set;
let J be ManySortedSet of I;
mode multMagma-Family of I,J -> ManySortedSet of I means
:Def4:
for i be Element of I holds it.i is multMagma-Family of J.i;
existence
proof
set G = the non empty multMagma;
deffunc DF(object) = J.$1 --> G;
consider f being Function such that
A1: dom f = I &
for i be set st i in I holds f.i = DF(i) from FUNCT_1:sch 5;
reconsider f as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
take f;
let i be Element of I;
J.i --> G = f.i by A1;
hence thesis;
end;
end;
definition
let I be non empty set;
let J be ManySortedSet of I;
mode Group-Family of I,J -> multMagma-Family of I,J means :Def5:
for i be Element of I holds it.i is Group-Family of J.i;
existence
proof
set G = the Group;
deffunc DF(object) = J.$1 --> G;
consider f be Function such that
A1: dom f = I &
for i be set st i in I holds f.i = DF(i) from FUNCT_1:sch 5;
reconsider f as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
A2: for i be Element of I holds f.i is Group-Family of J.i
proof
let i be Element of I;
f.i = J.i --> G by A1;
hence thesis;
end; then
for i be Element of I holds f.i is multMagma-Family of J.i; then
reconsider f as multMagma-Family of I,J by Def4;
take f;
thus thesis by A2;
end;
end;
definition
let I be non empty set;
let J be ManySortedSet of I;
let N be multMagma-Family of I,J;
let i be Element of I;
redefine func N.i -> multMagma-Family of J.i; :: redefines . (FUNCT_1, definition)
correctness by Def4;
end;
definition
let I be non empty set;
let J be ManySortedSet of I;
let N be Group-Family of I,J;
let i be Element of I;
redefine func N.i -> Group-Family of J.i; :: redefines . (FUNCT_1, definition)
correctness by Def5;
end;
definition
let I be non empty set;
let J be disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
redefine func Union F -> Group-Family of Union J; :: redefines Union (CARD_3, definition)
correctness
proof
set UF = Union F;
A1: dom J = I by PARTFUN1:def 2;
A2: dom F = I by PARTFUN1:def 2;
for x be object st x in UF holds ex y,z be object st x = [y,z]
proof
let x be object;
assume x in UF; then
consider Y be set such that
A3: x in Y & Y in rng F by TARSKI:def 4;
consider i being object such that
A4: i in dom F & Y = F.i by A3,FUNCT_1:def 3;
reconsider i as Element of I by A4;
F.i is Relation;
hence thesis by A3,A4,RELAT_1:def 1;
end; then
reconsider UF as Relation by RELAT_1:def 1;
for x,y1,y2 be object st [x,y1] in UF & [x,y2] in UF holds y1 = y2
proof
let x,y1,y2 be object;
assume A5: [x,y1] in UF & [x,y2] in UF; then
consider Y1 be set such that
A6: [x,y1] in Y1 & Y1 in rng F by TARSKI:def 4;
consider i1 being object such that
A7: i1 in dom F & Y1 = F.i1 by A6,FUNCT_1:def 3;
reconsider i1 as Element of I by A7;
reconsider Fi1 = F.i1 as Function;
x in dom Fi1 by A6,A7,FUNCT_1:1; then
A8: x in J.i1 by PARTFUN1:def 2;
consider Y2 be set such that
A9: [x,y2] in Y2 & Y2 in rng F by A5,TARSKI:def 4;
consider i2 being object such that
A10: i2 in dom F & Y2 = F.i2 by A9,FUNCT_1:def 3;
reconsider i2 as Element of I by A10;
reconsider Fi2 = F.i2 as Function;
x in dom Fi2 by A9,A10,FUNCT_1:1; then
x in J.i2 by PARTFUN1:def 2; then
J.i1 /\ J.i2 <> {} by A8,XBOOLE_0:def 4; then
[x,y1] in F.i1 & [x,y2] in F.i1
by A6,A7,A9,A10,PROB_2:def 2,XBOOLE_0:def 7;
hence thesis by FUNCT_1:def 1;
end; then
reconsider UF as Function by FUNCT_1:def 1;
A11: for x be object holds x in dom UF iff x in Union J
proof
let x be object;
hereby
assume x in dom UF; then
consider y be object such that
A12: [x,y] in UF by XTUPLE_0:def 12;
consider Y be set such that
A13: [x,y] in Y & Y in rng F by A12,TARSKI:def 4;
consider i being object such that
A14: i in dom F & Y = F.i by A13,FUNCT_1:def 3;
reconsider i as Element of I by A14;
reconsider Fi = F.i as Function;
x in dom Fi by A13,A14,FUNCT_1:1; then
x in J.i & J.i in rng J by A1,FUNCT_1:3,PARTFUN1:def 2;
hence x in Union J by TARSKI:def 4;
end;
assume x in Union J; then
consider Y be set such that
A15: x in Y & Y in rng J by TARSKI:def 4;
consider i being object such that
A16: i in dom J & Y = J.i by A15,FUNCT_1:def 3;
reconsider i as Element of I by A16;
reconsider Fi = F.i as Function;
x in dom Fi by A15,A16,PARTFUN1:def 2; then
consider y be object such that
A17: [x,y] in Fi by XTUPLE_0:def 12;
Fi in rng F by A2,FUNCT_1:3; then
[x,y] in UF by A17,TARSKI:def 4;
hence x in dom UF by XTUPLE_0:def 12;
end;
for x be object st x in Union J holds UF.x is Group
proof
let x be object;
assume x in Union J; then
consider Y be set such that
A18: x in Y & Y in rng J by TARSKI:def 4;
consider i being object such that
A19: i in dom J & Y = J.i by A18,FUNCT_1:def 3;
reconsider i as Element of I by A19;
reconsider Fi = F.i as Group-Family of J.i;
x in dom Fi by A18,A19,PARTFUN1:def 2; then
consider y be object such that
A20: [x,y] in Fi by XTUPLE_0:def 12;
A21: y = Fi.x by A20,FUNCT_1:1;
Fi in rng F by A2,FUNCT_1:3; then
[x,y] in UF by A20,TARSKI:def 4;
then y = UF.x by FUNCT_1:1;
hence thesis by A18,A19,A21,GROUP_19:1;
end;
hence thesis by A11,GROUP_19:2,TARSKI:2;
end;
end;
theorem Th19:
for I be non empty set,
J be disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
j be Element of I,
i be object st i in J.j
holds (Union F).i = (F.j).i
proof
let I be non empty set,
J be disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
j be Element of I,
i be object;
assume
A1: i in J.j;
dom J = I by PARTFUN1:def 2; then
A3: J.j c= Union J by FUNCT_1:3,ZFMISC_1:74;
dom(Union F) = Union J by PARTFUN1:def 2; then
[i, (Union F).i] in Union F by A1,A3,FUNCT_1:1; then
consider Y0 be set such that
A4: [i, (Union F).i] in Y0 & Y0 in rng F by TARSKI:def 4;
consider k being object such that
A5: k in dom F & Y0 = F.k by A4,FUNCT_1:def 3;
reconsider k as Element of I by A5;
reconsider Fk = F.k as Function;
A6: dom Fk = J.k by PARTFUN1:def 2;
i in dom Fk by A4,A5,XTUPLE_0:def 12; then
J.k /\ J.j <> {} by A1,A6,XBOOLE_0:def 4; then
j = k by PROB_2:def 2,XBOOLE_0:def 7;
hence thesis by A4,A5,FUNCT_1:1;
end;
definition
let I be non empty set;
let J be ManySortedSet of I;
let F be multMagma-Family of I,J;
func prod_bundle F -> multMagma-Family of I means :Def6:
for i be Element of I holds it.i = product(F.i);
existence
proof
deffunc DF(object) = product(F.(In($1,I)));
consider f being Function such that
A1: dom f = I
& for i be Element of I holds f.i = DF(i) from FUNCT_1:sch 4;
reconsider f as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
A2: for i be Element of I holds f.i = product(F.i)
proof
let i be Element of I;
In(i,I) = i;
hence f.i = product(F.i) by A1;
end;
for a be set st a in rng f holds a is non empty multMagma
proof
let a be set;
assume a in rng f; then
consider i being object such that
A3: i in dom f & a = f.i by FUNCT_1:def 3;
reconsider i as Element of I by A3;
f.i = product(F.i) by A2;
hence thesis by A3;
end; then
reconsider f as multMagma-Family of I by GROUP_7:def 1;
take f;
thus thesis by A2;
end;
uniqueness
proof
let G1,G2 be multMagma-Family of I such that
A4: for i be Element of I holds G1.i = product(F.i) and
A5: for i be Element of I holds G2.i = product(F.i);
A6: dom G1 = I by PARTFUN1:def 2;
for i be object st i in dom G1 holds G1.i = G2.i
proof
let i be object;
assume i in dom G1; then
reconsider i0=i as Element of I;
thus G1.i = product(F.i0) by A4
.= G2.i by A5;
end;
hence G1 = G2 by A6,PARTFUN1:def 2;
end;
end;
definition
let I be non empty set;
let J be ManySortedSet of I;
let F be Group-Family of I,J;
redefine func prod_bundle F -> Group-Family of I; :: redefines prod_bundle (GROUP_21, definition)
correctness
proof
set H = prod_bundle F;
A1: dom H = I by PARTFUN1:def 2;
for i be object st i in I holds H.i is Group
proof
let i be object;
assume i in I; then
reconsider i as Element of I;
H.i = product(F.i) by Def6;
hence thesis;
end;
hence thesis by A1,GROUP_19:2;
end;
end;
definition
let I be non empty set;
let J be ManySortedSet of I;
let F be Group-Family of I,J;
func sum_bundle F -> Group-Family of I means
:Def7:
for i be Element of I holds it.i = sum(F.i);
existence
proof
deffunc DF(object) = sum(F.(In($1,I)));
consider f being Function such that
A1: dom f = I
& for i be Element of I holds f.i = DF(i) from FUNCT_1:sch 4;
reconsider f as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
A2: for i be Element of I holds f.i = sum(F.i)
proof
let i be Element of I;
In(i,I) = i;
hence f.i = sum(F.i) by A1;
end;
for i be object st i in I holds f.i is Group
proof
let i be object;
assume i in I; then
reconsider i as Element of I;
f.i = sum(F.i) by A2;
hence thesis;
end; then
f is Group-Family of I by A1,GROUP_19:2;
hence thesis by A2;
end;
uniqueness
proof
let G1,G2 be Group-Family of I such that
A4: for i be Element of I holds G1.i = sum(F.i) and
A5: for i be Element of I holds G2.i = sum(F.i);
A6: dom G1 = I by PARTFUN1:def 2;
for i be object st i in dom G1 holds G1.i = G2.i
proof
let i be object;
assume i in dom G1; then
reconsider i0 = i as Element of I;
thus G1.i = sum(F.i0) by A4
.= G2.i by A5;
end;
hence G1 = G2 by A6,PARTFUN1:def 2;
end;
end;
definition
let I be non empty set;
let J be ManySortedSet of I;
let F be multMagma-Family of I,J;
func dprod F -> multMagma equals
product(prod_bundle F);
correctness;
end;
registration
let I be non empty set;
let J be non-empty ManySortedSet of I;
let F be multMagma-Family of I,J;
cluster dprod F -> non empty constituted-Functions;
correctness;
end;
registration
let I be non empty set;
let J be non-empty ManySortedSet of I;
let F be Group-Family of I,J;
cluster dprod F -> Group-like associative;
coherence
proof
reconsider H = prod_bundle F as Group-Family of I;
dprod F = product(H);
hence thesis;
end;
end;
definition
let I be non empty set;
let J be non-empty ManySortedSet of I;
let F be Group-Family of I,J;
func dsum F -> Group equals
sum(sum_bundle F);
correctness;
end;
registration
let I be non empty set;
let J be non-empty ManySortedSet of I;
let F be Group-Family of I,J;
cluster dsum F -> non empty constituted-Functions;
correctness;
end;
theorem Th20:
for I be non empty set, F1,F2 be Group-Family of I
st for i be Element of I holds F1.i is Subgroup of F2.i
holds product F1 is Subgroup of product F2
proof
let I be non empty set, F1,F2 be Group-Family of I;
assume
A1: for i be Element of I holds F1.i is Subgroup of F2.i;
A2: for x be object st x in [#] product F1 holds x in [#] product F2
proof
let x be object;
assume x in [#] product F1; then
reconsider x as Element of product F1;
A3: dom x = I by GROUP_19:3;
reconsider z = Carrier F2 as ManySortedSet of I;
A4: dom z = I by PARTFUN1:def 2;
for i be object st i in I holds x.i in z.i
proof
let i be object;
assume i in I; then
reconsider i as Element of I;
A5: z.i = [#](F2.i) by PENCIL_3:7;
x in product F1; then
A6: x.i in F1.i by GROUP_19:5;
F1.i is Subgroup of F2.i by A1; then
[#](F1.i) c= [#](F2.i) by GROUP_2:def 5;
hence thesis by A5,A6;
end; then
x in product z by A3,A4,CARD_3:def 5;
hence thesis by GROUP_7:def 2;
end; then
A7: [#] product F1 c= [#] product F2; then
[:[#] product F1, [#] product F1:]
c= [:[#] product F2, [#] product F2:] by ZFMISC_1:96; then
reconsider f2 = (the multF of product F2) || [#] product F1
as Function of [:[#] product F1,[#] product F1:], [#] product F2
by FUNCT_2:32;
reconsider f1 = (the multF of product F1)
as Function of [:[#] product F1,[#] product F1:], [#] product F2
by A7,FUNCT_2:7;
for x,y being set st x in [#] product F1 & y in [#] product F1
holds f1.(x,y) = f2.(x,y)
proof
let x0,y0 be set;
assume
A8: x0 in [#] product F1 & y0 in [#] product F1; then
reconsider x1=x0,y1=y0 as Element of product F1;
reconsider x2=x0,y2=y0 as Element of product F2 by A2,A8;
A9: dom(x1*y1) = I by GROUP_19:3;
A10: for i be object st i in dom (x1*y1) holds (x1*y1).i = (x2*y2).i
proof
let i be object;
assume i in dom(x1*y1); then
reconsider i as Element of I by GROUP_19:3;
x1 in product F1; then
x1.i in F1.i by GROUP_19:5; then
reconsider x1i = x1.i as Element of (F1.i);
x2 in product F2; then
x2.i in F2.i by GROUP_19:5; then
reconsider x2i = x2.i as Element of (F2.i);
y1 in product F1; then
y1.i in F1.i by GROUP_19:5; then
reconsider y1i = y1.i as Element of (F1.i);
y2 in product F2; then
y2.i in F2.i by GROUP_19:5; then
reconsider y2i = y2.i as Element of (F2.i);
A11: F1.i is Subgroup of F2.i by A1;
(x1*y1).i = x1i*y1i by GROUP_7:1
.= x2i*y2i by A11,GROUP_2:43
.= (x2*y2).i by GROUP_7:1;
hence thesis;
end;
A12: f2.(x2,y2)
= ((the multF of product F2)
| [: [#] product F1,[#] product F1:]).[x2,y2] by BINOP_1:def 1
.= (the multF of product F2).[x2,y2] by A8,FUNCT_1:49,ZFMISC_1:87
.= (the multF of product F2).(x2,y2) by BINOP_1:def 1;
thus f1.(x0,y0) = x1*y1 by ALGSTR_0:def 18
.= x2*y2 by A9,A10,GROUP_19:3
.= f2.(x0,y0) by A12,ALGSTR_0:def 18;
end;
hence thesis by A7,BINOP_1:def 21,GROUP_2:def 5;
end;
theorem
for I be non empty set, F1,F2 be Group-Family of I
st for i be Element of I holds F1.i is Subgroup of F2.i
holds sum F1 is Subgroup of sum F2
proof
let I be non empty set, F1,F2 be Group-Family of I;
assume
A1: for i be Element of I holds F1.i is Subgroup of F2.i;
for x be object st x in [#] sum F1 holds x in [#] sum F2
proof
let x be object;
assume
A2: x in [#] sum F1; then
x in sum F1; then
x in product F1 by GROUP_2:40; then
reconsider x as Element of product F1;
product F1 is Subgroup of product F2 by A1,Th20; then
reconsider y = x as Element of product F2 by GROUP_2:42;
for i be object holds i in support(y,F2) implies i in support(x,F1)
proof
let i be object;
assume i in support(y,F2); then
consider Z being Group such that
A4: Z = F2.i & y.i <> 1_Z & i in I by GROUP_19:def 1;
reconsider i as Element of I by A4;
F1.i is Subgroup of F2.i by A1; then
x.i <> 1_F1.i & i in I by A4,GROUP_2:44;
hence thesis by GROUP_19:def 1;
end; then
support(y,F2) c= support(x,F1); then
y in sum F2 by A2,GROUP_19:8;
hence thesis;
end; then
A5: [#] sum F1 c= [#] sum F2;
set mp1 = the multF of product F1;
set mp2 = the multF of product F2;
set ms1 = the multF of sum F1;
set ms2 = the multF of sum F2;
set cp1 = [#]product F1;
set cp2 = [#]product F2;
set cs1 = [#]sum F1;
set cs2 = [#]sum F2;
cs1 c= cp1 by GROUP_2:def 5; then
A6: [:cs1,cs1:] c= [:cp1,cp1:] by ZFMISC_1:96;
A7: [:cs1,cs1:] c= [:cs2,cs2:] by A5,ZFMISC_1:96;
A8: product F1 is Subgroup of product F2 by A1,Th20;
ms1 = mp1 || cs1 by GROUP_2:def 5
.= (mp2 || cp1) || cs1 by A8,GROUP_2:def 5
.= mp2 || cs1 by A6,FUNCT_1:51
.= (mp2 || cs2) || cs1 by A7,FUNCT_1:51
.= ms2 || cs1 by GROUP_2:def 5;
hence thesis by A5,GROUP_2:def 5;
end;
theorem Th22:
for I be non empty set,
J be non-empty ManySortedSet of I,
F be Group-Family of I,J
holds dsum F is Subgroup of dprod F
proof
let I be non empty set,
J be non-empty ManySortedSet of I,
F be Group-Family of I,J;
for i be Element of I
holds (sum_bundle F).i is Subgroup of (prod_bundle F).i
proof
let i be Element of I;
(sum_bundle F).i = sum F.i by Def7;
hence thesis by Def6;
end; then
product(sum_bundle F) is Subgroup of product(prod_bundle F) by Th20;
hence thesis by GROUP_2:56;
end;
definition
let I be non empty set;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
redefine func dsum F -> Subgroup of dprod F; :: redefines dsum (GROUP_21, definition)
correctness by Th22;
end;
definition
let I be non empty set;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
func dprod2prod F -> Homomorphism of dprod F, product(Union F) means
:Def10:
for x be Element of dprod F, i be Element of I holds x.i = it.x | (J.i);
existence
proof
A1: dom J = I by PARTFUN1:def 2;
defpred P[Function,Function] means
for i be Element of I holds $1.i = $2 | (J.i);
A2: for x being Element of dprod F
ex y being Element of product(Union F) st P[x,y]
proof
let x being Element of dprod F;
A3: x in product(prod_bundle F);
A4: dom x = I by GROUP_19:3;
A5: for i be Element of I holds x.i in product(F.i)
proof
let i be Element of I;
x.i in (prod_bundle F).i by A3,GROUP_19:5;
hence x.i in product(F.i) by Def6;
end;
set y = Union x;
for z be object st z in y holds ex a,b be object st z = [a,b]
proof
let z be object;
assume z in y; then
consider Y be set such that
A6: z in Y & Y in rng x by TARSKI:def 4;
consider i being object such that
A7: i in dom x & Y = x.i by A6,FUNCT_1:def 3;
reconsider i as Element of I by A7,GROUP_19:3;
x.i in product(F.i) by A5;
hence thesis by A6,A7,RELAT_1:def 1;
end; then
y is Relation-like; then
reconsider y as Relation;
for a,b1,b2 be object st [a,b1] in y & [a,b2] in y holds b1 = b2
proof
let a,b1,b2 be object;
assume A8: [a,b1] in y & [a,b2] in y; then
consider Y1 be set such that
A9: [a,b1] in Y1 & Y1 in rng x by TARSKI:def 4;
consider i1 being object such that
A10: i1 in dom x & Y1 = x.i1 by A9,FUNCT_1:def 3;
reconsider i1 as Element of I by A10,GROUP_19:3;
A11: x.i1 in product(F.i1) by A5;
reconsider xi1 = x.i1 as Function by A11;
A12: a in dom xi1 by A9,A10,FUNCT_1:1;
A13: a in J.i1 by A11,A12,GROUP_19:3;
consider Y2 be set such that
A14: [a,b2] in Y2 & Y2 in rng x by A8,TARSKI:def 4;
consider i2 being object such that
A15: i2 in dom x & Y2 = x.i2 by A14,FUNCT_1:def 3;
reconsider i2 as Element of I by A15,GROUP_19:3;
A16: x.i2 in product(F.i2) by A5;
reconsider xi2 = x.i2 as Function by A16;
A17: a in dom xi2 by A14,A15,FUNCT_1:1;
a in J.i2 by A16,A17,GROUP_19:3; then
A18: J.i1 /\ J.i2 <> {} by A13,XBOOLE_0:def 4;
i1 = i2 by A18,PROB_2:def 2,XBOOLE_0:def 7;
hence b1 = b2 by A9,A10,A11,A14,A15,FUNCT_1:def 1;
end; then
y is Function-like; then
reconsider y as Function;
A19: for a be object holds a in dom y iff a in Union J
proof
let a be object;
hereby
assume a in dom y; then
consider b be object such that
A20: [a,b] in y by XTUPLE_0:def 12;
consider Y be set such that
A21: [a,b] in Y & Y in rng x by A20,TARSKI:def 4;
consider i being object such that
A22: i in dom x & Y = x.i by A21,FUNCT_1:def 3;
reconsider i as Element of I by A22,GROUP_19:3;
A23: x.i in product(F.i) by A5; then
reconsider xi = x.i as Function;
A24: a in dom xi by A21,A22,FUNCT_1:1;
a in J.i & J.i in rng J by A1,A23,A24,FUNCT_1:3,GROUP_19:3;
hence a in Union J by TARSKI:def 4;
end;
assume a in Union J; then
consider Y be set such that
A25: a in Y & Y in rng J by TARSKI:def 4;
consider i being object such that
A26: i in dom J & Y = J.i by A25,FUNCT_1:def 3;
reconsider i as Element of I by A26;
A27: x.i in product(F.i) by A5;
reconsider xi = x.i as Function by A27;
a in dom xi by A25,A26,A27,GROUP_19:3; then
consider b be object such that
A28: [a,b] in xi by XTUPLE_0:def 12;
xi in rng x by A4,FUNCT_1:3; then
[a,b] in y by A28,TARSKI:def 4;
hence a in dom y by XTUPLE_0:def 12;
end; then
A29: dom y = Union J by TARSKI:2; then
reconsider y as ManySortedSet of Union J
by PARTFUN1:def 2,RELAT_1:def 18;
reconsider z = Carrier Union F as ManySortedSet of Union J;
A30: dom z = Union J by PARTFUN1:def 2;
for i be object st i in Union J holds y.i in z.i
proof
let i be object;
assume i in Union J; then
reconsider i as Element of Union J;
[i,y.i] in y by A19,FUNCT_1:1; then
consider Yi be set such that
A31: [i,y.i] in Yi & Yi in rng x by TARSKI:def 4;
consider j being object such that
A32: j in dom x & Yi = x.j by A31,FUNCT_1:def 3;
reconsider j as Element of I by A32,GROUP_19:3;
A33: x.j in product(F.j) by A5;
reconsider xj = x.j as Function by A33;
A34: i in dom xj & y.i = xj.i by A31,A32,FUNCT_1:1;
A35: i in J.j by A33,A34,GROUP_19:3;
dom (Union F) = Union J by PARTFUN1:def 2; then
[i, (Union F).i] in Union F by FUNCT_1:1; then
consider Y0 be set such that
A36: [i, (Union F).i] in Y0 & Y0 in rng F by TARSKI:def 4;
consider k being object such that
A37: k in dom F & Y0 = F.k by A36,FUNCT_1:def 3;
reconsider k as Element of I by A37;
reconsider Fk = F.k as Function;
A38: dom Fk = J.k by PARTFUN1:def 2;
i in dom Fk by A36,A37,XTUPLE_0:def 12; then
A39: J.k /\ J.j <> {} by A35,A38,XBOOLE_0:def 4;
reconsider P = (F.j).i as Group by A35,GROUP_19:1;
j = k by A39,PROB_2:def 2,XBOOLE_0:def 7; then
A40: [#]P = [#]((Union F).i) by A36,A37,FUNCT_1:1;
xj.i in P by A33,A35,GROUP_19:5;
hence thesis by A34,A40,PENCIL_3:7;
end; then
y in product z by A29,A30,CARD_3:def 5; then
reconsider y as Element of product(Union F) by GROUP_7:def 2;
take y;
thus for i be Element of I holds x.i = y | (J.i)
proof
let i be Element of I;
A41: J.i c= Union J by A1,FUNCT_1:3,ZFMISC_1:74; then
A42: dom(y | (J.i)) = J.i by A29,RELAT_1:62;
A43: x.i in product(F.i) by A5; then
reconsider xi = x.i as Function;
for j be object st j in dom xi holds xi.j = (y | (J.i)).j
proof
let j be object;
assume j in dom xi; then
A44: j in J.i by A43,GROUP_19:3; then
A45: (y | (J.i)).j = y.j by FUNCT_1:49;
j in dom (y | (J.i)) by A29,A41,A44,RELAT_1:62; then
j in (dom y) /\ (J.i) by RELAT_1:61; then
j in dom y by XBOOLE_0:def 4; then
[j,y.j] in y by FUNCT_1:1; then
consider Y0 be set such that
A46: [j,y.j] in Y0 & Y0 in rng x by TARSKI:def 4;
consider k being object such that
A47: k in dom x & Y0 = x.k by A46,FUNCT_1:def 3;
reconsider k as Element of I by A47,GROUP_19:3;
A48: x.k in product(F.k) by A5; then
reconsider xk = x.k as Function;
A49: dom xk = J.k by A48,GROUP_19:3;
j in dom xk by A46,A47,XTUPLE_0:def 12; then
A50: J.k /\ J.i <> {} by A44,A49,XBOOLE_0:def 4;
i = k by A50,PROB_2:def 2,XBOOLE_0:def 7;
hence thesis by A45,A46,A47,FUNCT_1:1;
end;
hence thesis by A42,A43,FUNCT_1:2,GROUP_19:3;
end;
end;
consider f being Function of dprod F,product(Union F) such that
A51: for x being Element of dprod F holds P[x,f.x] from FUNCT_2:sch 3(A2);
for a,b be Element of dprod F holds f.(a * b) = f.a * f.b
proof
let a,b be Element of dprod F;
reconsider fa = f.a as Element of product(Union F);
reconsider fb = f.b as Element of product(Union F);
set fafb = fa*fb;
reconsider fab = f.(a*b) as Element of product(Union F);
A52: a in product(prod_bundle F) & b in product(prod_bundle F)
& a*b in product(prod_bundle F);
A53: for i be Element of I holds
a.i in product(F.i) & b.i in product(F.i) & (a*b).i in product(F.i)
proof
let i be Element of I;
a.i in (prod_bundle F).i & b.i in (prod_bundle F).i
& (a*b).i in (prod_bundle F).i by A52,GROUP_19:5;
hence thesis by Def6;
end;
A54: dom fab = Union J by GROUP_19:3;
for j be object st j in dom fab holds fab.j = fafb.j
proof
let j be object;
assume
A55: j in dom fab; then
consider Y be set such that
A56: j in Y & Y in rng J by A54,TARSKI:def 4;
consider i being object such that
A57: i in dom J & Y = J.i by A56,FUNCT_1:def 3;
reconsider i as Element of I by A57;
A58: a.i = f.a | (J.i) by A51;
A59: b.i = f.b | (J.i) by A51;
a.i in product(F.i) & b.i in product(F.i)
& (a*b).i in product(F.i) by A53; then
reconsider ai=a.i, bi=b.i, abi =(a*b).i as Element of product(F.i);
reconsider P = (F.i).j as Group by A56,A57,GROUP_19:1;
ai.j in P by A53,A56,A57,GROUP_19:5; then
reconsider aij = ai.j as Element of P;
bi.j in P by A53,A56,A57,GROUP_19:5; then
reconsider bij = bi.j as Element of P;
A60: aij = fa.j by A56,A57,A58,FUNCT_1:49; then
reconsider faj = fa.j as Element of P;
bij = fb.j by A56,A57,A59,FUNCT_1:49; then
reconsider fbj = fb.j as Element of P;
(prod_bundle F).i = product(F.i) by Def6; then
A61: abi.j = (ai * bi).j by GROUP_7:1
.= aij * bij by A56,A57,GROUP_7:1;
A62: j in Union J by A55,GROUP_19:3;
dom(Union F) = Union J by PARTFUN1:def 2; then
[j, (Union F).j] in Union F by A62,FUNCT_1:1; then
consider Y0 be set such that
A63: [j, (Union F).j ] in Y0 & Y0 in rng F by TARSKI:def 4;
consider k being object such that
A64: k in dom F & Y0 = F.k by A63,FUNCT_1:def 3;
reconsider k as Element of I by A64;
reconsider Fk = F.k as Function;
j in dom Fk by A63,A64,XTUPLE_0:def 12; then
j in J.k by PARTFUN1:def 2; then
A65: J.k /\ J.i <> {} by A56,A57,XBOOLE_0:def 4;
i = k by A65,PROB_2:def 2,XBOOLE_0:def 7; then
A66: (Union F).j = (F.i).j by A63,A64,FUNCT_1:1;
thus fab.j = (f.(a*b) | (J.i)).j by A56,A57,FUNCT_1:49
.= aij * bij by A51,A61
.= faj * fbj by A56,A57,A59,A60,FUNCT_1:49
.= fafb.j by A62,A66,GROUP_7:1;
end;
hence thesis by A54,GROUP_19:3;
end; then
reconsider f as Homomorphism of dprod F, product(Union F) by GROUP_6:def 6;
take f;
thus thesis by A51;
end;
uniqueness
proof
let H1,H2 be Homomorphism of dprod F, product(Union F) such that
A67: for x be Element of dprod F, i be Element of I holds
x.i = H1.x | (J.i) and
A68: for x be Element of dprod F, i be Element of I holds
x.i = H2.x | (J.i);
for x being Element of dprod F holds H1.x = H2.x
proof
let x being Element of dprod F;
A69: x in product(prod_bundle F);
A70: for i be Element of I holds x.i in product(F.i)
proof
let i be Element of I;
x.i in (prod_bundle F).i by A69,GROUP_19:5;
hence x.i in product(F.i) by Def6;
end;
reconsider H1x = H1.x, H2x = H2.x as Function;
A71: dom H1x = Union J by GROUP_19:3;
for j be object st j in dom H1x holds H1x.j = H2x.j
proof
let j be object;
assume j in dom H1x; then
consider Y be set such that
A72: j in Y & Y in rng J by A71,TARSKI:def 4;
consider i being object such that
A73: i in dom J & Y = J.i by A72,FUNCT_1:def 3;
reconsider i as Element of I by A73;
x.i in product(F.i) by A70; then
reconsider xi = x.i as Function;
thus H1x.j = (H1x | (J.i)).j by A72,A73,FUNCT_1:49
.= xi.j by A67
.= (H2x | (J.i)).j by A68
.= H2x.j by A72,A73,FUNCT_1:49;
end;
hence thesis by A71,GROUP_19:3;
end;
hence H1 = H2 by FUNCT_2:63;
end;
end;
theorem Th23:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
y be Element of product(Union F),
i be Element of I
holds y | (J.i) in product(F.i)
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
y be Element of product(Union F),
i be Element of I;
set x = y | (J.i);
A1: dom J = I by PARTFUN1:def 2;
A2: dom(Union F) = Union J by PARTFUN1:def 2;
A3: dom y = Union J by GROUP_19:3;
A4: J.i c= Union J by A1,FUNCT_1:3,ZFMISC_1:74; then
A5: dom x = J.i by A3,RELAT_1:62;
set z = Carrier(F.i);
A6: dom z = J.i by PARTFUN1:def 2;
for j be object st j in J.i holds x.j in z.j
proof
let j be object;
assume j in J.i; then
reconsider j as Element of J.i;
reconsider j1 = j as Element of Union J by A4;
reconsider D = Union F as Group-Family of Union J;
y in product(Union F); then
A8: y.j1 in D.j1 by GROUP_19:5;
A9: x.j = y.j by FUNCT_1:49;
[j, (Union F).j] in Union F by A2,A4,FUNCT_1:1; then
consider Y0 be set such that
A10: [j, (Union F).j] in Y0 & Y0 in rng F by TARSKI:def 4;
consider k being object such that
A11: k in dom F & Y0 = F.k by A10,FUNCT_1:def 3;
reconsider k as Element of I by A11;
reconsider Fk = F.k as Function;
A12: dom Fk = J.k by PARTFUN1:def 2;
j in dom Fk by A10,A11,XTUPLE_0:def 12; then
A13: J.k /\ J.i <> {} by A12,XBOOLE_0:def 4;
A14: i = k by A13,PROB_2:def 2,XBOOLE_0:def 7;
reconsider T = (F.i).j as Group;
z.j = [#]T by PENCIL_3:7;
hence thesis by A8,A9,A10,A11,A14,FUNCT_1:1;
end; then
x in product z by A5,A6,CARD_3:def 5;
hence thesis by GROUP_7:def 2;
end;
Th24:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J
holds dprod2prod F is bijective
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J;
set f = dprod2prod F;
for x1,x2 be object
st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be object such that
A1: x1 in dom f and
A2: x2 in dom f and
A3: f.x1 = f.x2;
reconsider x1, x2 as Element of dprod F by A1,A2;
A4: dom x1 = I by GROUP_19:3;
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 I by GROUP_19:3;
x1.i = f.x2 | (J.i) by A3,Def10
.= x2.i by Def10;
hence thesis;
end; then
x1 = x2 by A4,GROUP_19:3;
hence thesis;
end;
hence f is one-to-one;
for y be object st y in [#] product(Union F)
ex x be object st x in [#] dprod F & y = f.x
proof
let y being object;
assume y in [#] product(Union F); then
reconsider y as Element of product(Union F);
deffunc P(object) = y | (J.$1);
consider x being Function such that
A5: dom x = I
& for i be object st i in I holds x.i = P(i) from FUNCT_1:sch 3;
reconsider x as ManySortedSet of I by A5,PARTFUN1:def 2,RELAT_1:def 18;
set z = Carrier prod_bundle(F);
A6: dom z = I by PARTFUN1:def 2;
for i be object st i in I holds x.i in z.i
proof
let i be object;
assume i in I; then
reconsider i as Element of I;
A7: z.i = [#]((prod_bundle F).i) by PENCIL_3:7
.= [#](product(F.i)) by Def6;
y | (J.i) in product(F.i) by Th23;
hence thesis by A5,A7;
end; then
x in product z by A5,A6,CARD_3:def 5; then
reconsider x as Element of dprod F by GROUP_7:def 2;
take x;
thus x in [#] dprod(F);
A8: x in product(prod_bundle F);
A9: for i be Element of I holds x.i in product(F.i)
proof
let i be Element of I;
x.i in (prod_bundle F).i by A8,GROUP_19:5;
hence thesis by Def6;
end;
reconsider H1x = y, H2x = f.x as Function;
A10: dom H1x = Union J by GROUP_19:3;
for j be object st j in dom H1x holds H1x.j = H2x.j
proof
let j be object;
assume j in dom H1x; then
consider Y be set such that
A11: j in Y & Y in rng J by A10,TARSKI:def 4;
consider i being object such that
A12: i in dom J & Y = J.i by A11,FUNCT_1:def 3;
reconsider i as Element of I by A12;
x.i in product(F.i) by A9; then
reconsider xi = x.i as Function;
thus H1x.j = (H1x | (J.i)).j by A11,A12,FUNCT_1:49
.= xi.j by A5
.= (H2x | (J.i)).j by Def10
.= H2x.j by A11,A12,FUNCT_1:49;
end; then
y = f.x by A10,GROUP_19:3;
hence thesis;
end; then
rng f = [#] product(Union F) by FUNCT_2:10;
hence f is onto by FUNCT_2:def 3;
end;
registration
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J;
cluster dprod2prod F -> bijective;
coherence by Th24;
end;
definition
let I be non empty set;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
func prod2dprod F -> Homomorphism of product(Union F), dprod F equals
(dprod2prod F)";
correctness by GROUP_6:62;
end;
theorem Th25:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J
holds
for x be Element of product(Union F), i be Element of I holds
x | (J.i) = ((prod2dprod F).x).i
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J;
set f1 = dprod2prod F;
set f2 = prod2dprod F;
let x be Element of product(Union F), i be Element of I;
A2: rng f1 = the carrier of product(Union F) by FUNCT_2:def 3;
reconsider y = f2.x as Element of dprod F;
((prod2dprod F).x).i = f1.y | (J.i) by Def10
.= x | (J.i) by A2,FUNCT_1:35;
hence thesis;
end;
registration
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J;
cluster prod2dprod F -> bijective;
coherence by GROUP_6:63;
end;
theorem
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J
holds prod2dprod F = (dprod2prod F)";
definition
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
x be Function;
func supp_restr(x,F) -> disjoint_valued ManySortedSet of I means
:Def12:
for i be Element of I holds it.i = support(x | (J.i), F.i);
existence
proof
deffunc P(object) = support(x | (J.In($1,I)), F.In($1,I));
consider sz being Function such that
A1: dom sz = I
& for i be object st i in I holds sz.i = P(i) from FUNCT_1:sch 3;
reconsider sz as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
A2: for i be Element of I holds sz.i = support(x | (J.i), F.i)
proof
let i be Element of I;
In(i,I) = i;
hence thesis by A1;
end;
A3: J is disjoint_valued;
for i,j be object st i<>j holds sz.i misses sz.j
proof
let i,j be object;
assume
A4: i<>j;
per cases;
suppose
not i in dom sz or not j in dom sz; then
sz.i = {} or sz.j = {} by FUNCT_1:def 2; then
sz.i /\ sz.j = {};
hence sz.i misses sz.j by XBOOLE_0:def 7;
end;
suppose
i in dom sz & j in dom sz; then
reconsider i, j as Element of I;
A6: sz.i = support(x | (J.i), F.i)
& sz.j = support(x | (J.j), F.j) by A2;
A7: sz.i /\ sz.j c= J.i /\ J.j by A6,XBOOLE_1:27;
J.i /\ J.j = {} by A3,A4,XBOOLE_0:def 7; then
sz.i /\ sz.j = {} by A7;
hence thesis by XBOOLE_0:def 7;
end;
end; then
sz is disjoint_valued; then
reconsider sz as disjoint_valued ManySortedSet of I;
take sz;
thus thesis by A2;
end;
uniqueness
proof
let f1,f2 be disjoint_valued ManySortedSet of I such that
A8: for i be Element of I holds f1.i = support(x| (J.i), F.i) and
A9: for i be Element of I holds f2.i = support(x| (J.i), F.i);
A10: dom f1 = I by PARTFUN1:def 2;
for i be object st i in dom f1 holds f1.i = f2.i
proof
let i be object;
assume i in dom f1; then
reconsider i0 = i as Element of I;
thus f1.i = support(x| (J.i), F.i0) by A8
.= f2.i by A9;
end;
hence f1 = f2 by A10,PARTFUN1:def 2;
end;
end;
theorem Th28:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
x be Function
holds support(x,Union F) = Union supp_restr(x,F)
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
x be Function;
set y = supp_restr(x,F);
A1: dom J = I by PARTFUN1:def 2;
A2: dom y = I by PARTFUN1:def 2;
for j be object holds j in support(x,Union F) iff j in Union y
proof
let j be object;
hereby
assume j in support(x,Union F); then
consider Z being Group such that
A3: Z = (Union F).j & x.j <> 1_Z & j in Union J by GROUP_19:def 1;
consider Y be set such that
A4: j in Y & Y in rng J by A3,TARSKI:def 4;
consider i being object such that
A5: i in dom J & Y = J.i by A4,FUNCT_1:def 3;
reconsider i as Element of I by A5;
reconsider j0 = j as Element of J.i by A4,A5;
(F.i).j0 = (Union F).j0 by Th19; then
(x | (J.i)).j <> 1_(F.i).j0 by A3,FUNCT_1:49; then
j in support (x | (J.i),F.i) by GROUP_19:def 1; then
A6: j in y.i by Def12;
y.i in rng y by A2,FUNCT_1:3;
hence j in Union y by A6,TARSKI:def 4;
end;
assume j in Union y; then
consider Y be set such that
A7: j in Y & Y in rng y by TARSKI:def 4;
consider i being object such that
A8: i in dom y & Y = y.i by A7,FUNCT_1:def 3;
reconsider i as Element of I by A8;
A9: y.i = support(x | (J.i), F.i) by Def12; then
consider Z being Group such that
A10: Z = (F.i).j & (x | (J.i)).j <> 1_Z & j in J.i
by A7,A8,GROUP_19:def 1;
A11: (x | (J.i)).j = x.j by A7,A8,A9,FUNCT_1:49;
J.i in rng J by A1,FUNCT_1:3;
then reconsider j0 = j as Element of Union J by A10,TARSKI:def 4;
reconsider ZZ = (Union F).j0 as Group;
1_Z = 1_ZZ by A10,Th19;
hence j in support(x,Union F) by A10,A11,GROUP_19:def 1;
end;
hence thesis by TARSKI:2;
end;
theorem Th29:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
x,y,z be Function
st z in dprod F & x = (dprod2prod F).z
holds
supp_restr(x,F) | support(z,sum_bundle F)
is non-empty disjoint_valued ManySortedSet of support(z,sum_bundle F)
& support(x,Union F) = Union(supp_restr(x,F) | support(z,sum_bundle F))
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
x,y,z be Function;
assume that
A1: z in dprod F and
A2: x = (dprod2prod F).z;
set srx = supp_restr(x,F);
set sz = support(z,sum_bundle F);
set f = srx | sz;
A3: dom srx = I by PARTFUN1:def 2;
dom f = sz by A3,RELAT_1:62; then
reconsider f as ManySortedSet of sz by PARTFUN1:def 2;
for s,t be object st s<>t holds f.s misses f.t
proof
let s,t be object;
assume
A4: s<>t;
per cases;
suppose
not s in dom f or not t in dom f; then
f.s = {} or f.t = {} by FUNCT_1:def 2; then
f.s /\ f.t = {};
hence thesis by XBOOLE_0:def 7;
end;
suppose
s in dom f & t in dom f; then
A5: f.s = srx.s & f.t = srx.t by FUNCT_1:47;
srx is disjoint_valued;
hence thesis by A4,A5;
end;
end; then
reconsider f as disjoint_valued ManySortedSet of sz by PROB_2:def 2;
not {} in rng f
proof
assume {} in rng f; then
consider i be object such that
A6: i in dom f & {} = f.i by FUNCT_1:def 3;
i in sz by A6; then
reconsider i as Element of I;
A7: {} = srx.i by A6,FUNCT_1:47;
A8: support(x | (J.i), F.i) = {} by A7,Def12;
ex Z being Group st Z = (sum_bundle F).i &
z.i <> 1_Z & i in I by A6,GROUP_19:def 1; then
A9: z.i <> 1_sum(F.i) by Def7;
z.i in (prod_bundle F).i by A1,GROUP_19:5; then
A10: z.i in product(F.i) by Def6; then
reconsider zi = z.i as Function;
ex j be Element of J.i st zi.j <> 1_(F.i).j
proof
assume
A11: for j be Element of J.i holds zi.j = 1_(F.i).j;
dom zi = J.i by A10,GROUP_19:3; then
reconsider zi as ManySortedSet of J.i by PARTFUN1:def 2,RELAT_1:def 18;
for k being set st k in J.i
ex G being Group-like non empty multMagma st G = (F.i).k & zi.k = 1_G
proof
let k being set;
assume k in J.i; then
reconsider j = k as Element of J.i;
take G = (F.i).j;
thus G = (F.i).k;
thus zi.k = 1_G by A11;
end; then
zi = 1_product(F.i) by GROUP_7:5;
hence contradiction by A9,GROUP_2:44;
end; then
consider j be Element of J.i such that
A12: zi.j <> 1_(F.i).j;
j in support(zi, F.i) by A12,GROUP_19:def 1;
hence contradiction by A1,A2,A8,Def10;
end; then
reconsider f as non-empty disjoint_valued ManySortedSet of sz
by RELAT_1:def 9;
f = srx | sz;
hence srx | sz is non-empty disjoint_valued ManySortedSet of sz;
A13: support(x,Union F) = Union srx by Th28;
Union(srx | sz) c= Union srx by RELAT_1:70,ZFMISC_1:77; then
A14: Union(srx | sz) c= support(x,Union F) by A13;
for k be object st k in support(x,Union F) holds k in Union(srx | sz)
proof
let k be object;
assume k in support(x,Union F); then
consider Y be set such that
A15: k in Y & Y in rng(srx) by A13,TARSKI:def 4;
consider i being object such that
A16: i in dom(srx) & Y = (srx).i by A15,FUNCT_1:def 3;
reconsider i as Element of I by A16;
k in support(x | (J.i), F.i) by A15,A16,Def12; then
consider Z being Group such that
A17: Z = (F.i).k & (x | (J.i)).k <> 1_Z & k in J.i by GROUP_19:def 1;
z.i in (prod_bundle F).i by A1,GROUP_19:5; then
A18: z.i in product(F.i) by Def6; then
reconsider zi = z.i as Function;
dom zi = J.i by A18,GROUP_19:3; then
reconsider zi as ManySortedSet of J.i by PARTFUN1:def 2,RELAT_1:def 18;
A19: zi.k <> 1_Z & k in J.i by A1,A2,A17,Def10;
zi <> 1_product(F.i) by A17,A19,GROUP_7:6; then
z.i <> 1_sum(F.i) by GROUP_2:44; then
z.i <> 1_(sum_bundle F).i by Def7; then
i in support(z,sum_bundle F) by GROUP_19:def 1; then
A20: i in dom(srx | sz) by A16,RELAT_1:57; then
Y = (srx | sz).i by A16,FUNCT_1:47; then
Y in rng(srx | sz) by A20,FUNCT_1:3;
hence k in Union(srx | sz) by A15,TARSKI:def 4;
end; then
support(x,Union F) c= Union(srx | sz);
hence support(x,Union F) = Union(srx | sz) by A14,XBOOLE_0:def 10;
end;
theorem Th31:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
y be Function st y in sum(Union F)
ex x be Function
st y = (dprod2prod F).x & x in dsum F
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
y be Function;
A1: [#] sum(Union F) c= [#] product(Union F) by GROUP_2:def 5;
assume
A2: y in sum(Union F); then
reconsider y as Element of product(Union F) by A1;
A3: y in product(Union F) & support(y,Union F) is finite by A2;
rng(dprod2prod F) = [#] product(Union F) by FUNCT_2:def 3; then
consider x be Element of [#] dprod(F) such that
A4: y = (dprod2prod F).x by FUNCT_2:113;
reconsider x as Function;
take x;
A5: x in dprod F;
set sry = supp_restr(y,F);
A6: support(y,Union F) = Union sry by Th28;
A7: for i be Element of I holds x.i in (sum_bundle F).i
proof
let i be Element of I;
i in I; then
i in dom sry by PARTFUN1:def 2; then
A8: sry.i c= Union sry by FUNCT_1:3,ZFMISC_1:74;
A9: support(y | (J.i), F.i) is finite by A2,A6,A8,Def12;
A10: y | (J.i) = x.i by A4,Def10;
x.i in (prod_bundle F).i by A5,GROUP_19:5; then
x.i in product(F.i) by Def6; then
x.i in sum(F.i) by A9,A10,GROUP_19:8;
hence thesis by Def7;
end;
set SBF = sum_bundle F;
A11: dom x = I by GROUP_19:3;
reconsider W = Carrier SBF as ManySortedSet of I;
A12: dom W = I by PARTFUN1:def 2;
for i be object st i in I holds x.i in W.i
proof
let i be object;
assume i in I; then
reconsider i as Element of I;
A13: W.i = [#](SBF.i) by PENCIL_3:7;
x.i in SBF.i by A7;
hence thesis by A13;
end; then
x in product W by A11,A12,CARD_3:def 5; then
reconsider x as Element of product(sum_bundle F) by GROUP_7:def 2;
reconsider sry1 = sry | support(x,sum_bundle F) as non-empty
disjoint_valued ManySortedSet of support(x,sum_bundle F)
by A4,A5,Th29;
Union sry1 is finite by A3,A4,A5,Th29; then
dom sry1 is finite by Th30; then
support(x,sum_bundle F) is finite by PARTFUN1:def 2;
hence thesis by A4,GROUP_19:8;
end;
theorem Th32:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
x,y be Function st x in dsum F & x in dsum F
holds (dprod2prod F).x in sum(Union F)
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J,
x,y be Function;
assume
A1: x in dsum F; then
A2: x in dprod(F) by GROUP_2:40; then
reconsider y = (dprod2prod F).x as Element of product(Union F)
by FUNCT_2:5;
deffunc P(object) = support(y | (J.In($1,I)), F.In($1,I));
set sry = supp_restr(y,F);
reconsider sry1 = sry | support(x,sum_bundle F) as non-empty
disjoint_valued ManySortedSet of support(x,sum_bundle F) by A2,Th29;
for i be object st i in dom sry1 holds sry1.i is finite
proof
let i be object;
assume
A3: i in dom sry1; then
i in support(x,sum_bundle F); then
reconsider i as Element of I;
A4: y | (J.i) = x.i by A2,Def10;
x.i in (sum_bundle F).i by A1,GROUP_2:40,GROUP_19:5; then
A5: x.i in sum(F.i) by Def7; then
x.i in product(F.i) by GROUP_2:40; then
reconsider zi = x.i as Element of product (F.i);
sry.i = support(y | (J.i), F.i) by Def12;
hence thesis by A3,A4,A5,FUNCT_1:49;
end; then
Union sry1 is finite by A1,CARD_2:88; then
support(y,Union F) is finite by A2,Th29;
hence thesis by GROUP_19:8;
end;
theorem Th33:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J
holds rng((dprod2prod F) | (dsum F)) = [#] sum(Union F)
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J;
for y be object holds
y in rng((dprod2prod F) | ([#] dsum F)) iff y in [#] sum(Union F)
proof
let y be object;
A1: dom dprod2prod F = [#] dprod F by FUNCT_2:def 1;
hereby
assume y in rng((dprod2prod F) | ([#] dsum F)); then
consider x be object such that
A2: x in dom((dprod2prod F) | ([#] dsum F))
& y = ((dprod2prod F) | ([#] dsum F)).x by FUNCT_1:def 3;
x in dom(dprod2prod F) /\ ([#] dsum F) by A2,RELAT_1:61; then
A3: x in dom(dprod2prod F) & x in [#] dsum F by XBOOLE_0:def 4;
reconsider x as Function by A2;
x in dprod F & x in dsum F by A3; then
(dprod2prod F).x in sum(Union F) by Th32;
hence y in [#] sum(Union F) by A2,FUNCT_1:47;
end;
assume
A4: y in [#] sum(Union F); then
reconsider y0 = y as Element of sum(Union F);
y0 in [#] product(Union F) by GROUP_2:def 5,TARSKI:def 3; then
reconsider y0 = y as Element of product(Union F);
y0 in sum(Union F) by A4; then
consider x be Function such that
A5: y0 = (dprod2prod F).x and
A6: x in dsum F by Th31;
A7: y = ((dprod2prod F) | ([#] dsum F)).x by A5,A6,FUNCT_1:49;
x in dom((dprod2prod F) | ([#] dsum F))
by A1,A6,GROUP_2:def 5,RELAT_1:62;
hence y in rng((dprod2prod F) | ([#] dsum F)) by A7,FUNCT_1:3;
end;
hence thesis by TARSKI:2;
end;
definition
let I be non empty set;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
func dsum2sum F -> Homomorphism of dsum(F), sum(Union F) equals
(dprod2prod F) | (dsum F);
correctness
proof
set f = dprod2prod F;
set h = f | (dsum F);
A1: [#] dsum F c= [#] dprod F by GROUP_2:def 5;
reconsider h as Function of dsum F, product(Union F);
A2: [#] sum(Union F) c= [#] product(Union F) by GROUP_2:def 5;
rng h = [#] sum(Union F) by Th33; then
reconsider h as Function of dsum F, sum(Union F) by FUNCT_2:6;
for a,b be Element of dsum F holds h.(a * b) = h.a * h.b
proof
let a,b be Element of dsum F;
reconsider a0 = a, b0 = b as Element of dprod F by A1;
reconsider ha = h.a, hb = h.b as Element of product(Union F) by A2;
A3: ha = f.a0 & hb = f.b0 by FUNCT_1:49;
h.(a * b) = f.(a * b) by FUNCT_1:49
.= f.(a0 * b0) by GROUP_2:43
.= ha * hb by A3,GROUP_6:def 6
.= h.a * h.b by GROUP_2:43;
hence thesis;
end;
hence thesis by GROUP_6:def 6;
end;
end;
Th34:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J
holds dsum2sum(F) is bijective
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J;
A1: dsum2sum F is one-to-one by FUNCT_1:52;
rng(dsum2sum F) = [#] sum(Union F) by Th33; then
dsum2sum F is onto by FUNCT_2:def 3;
hence thesis by A1;
end;
registration
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J;
cluster dsum2sum(F) -> bijective;
coherence by Th34;
end;
definition
let I be non empty set;
let J be non-empty disjoint_valued ManySortedSet of I;
let F be Group-Family of I,J;
func sum2dsum F -> Homomorphism of sum(Union F), dsum F equals
(dsum2sum F)";
correctness by GROUP_6:62;
end;
theorem Th36:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J
holds sum2dsum F = (prod2dprod F) | sum(Union F)
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J;
dsum2sum F is bijective; then
rng((dprod2prod F) | (dsum F)) = [#] sum(Union F) by FUNCT_2:def 3;
hence thesis by Th35;
end;
registration
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J;
cluster sum2dsum(F) -> bijective;
coherence by GROUP_6:63;
end;
theorem
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
F be Group-Family of I,J
holds dsum2sum(F) = (sum2dsum F)" by FUNCT_1:43;
definition
let I be non empty set;
let G be Group;
let F be internal DirectSumComponents of G,I;
func InterHom F -> Homomorphism of sum F, G means :Def15:
it is bijective
& for x be finite-support Function of I,G st x in sum F holds
it.x = Product x;
existence by GROUP_19:def 9;
uniqueness
proof
let h1,h2 be Homomorphism of sum F, G such that
A1: h1 is bijective
& for x be finite-support Function of I,G st x in sum F holds
h1.x = Product x and
A2: h2 is bijective
& for x be finite-support Function of I,G st x in sum F holds
h2.x = Product x;
A3: for i be object st i in I holds F.i is Subgroup of G
by GROUP_19:def 9;
for x being Element of sum F holds h1.x = h2.x
proof
let x being Element of sum F;
A4: x in sum F; then
reconsider x0 = x as finite-support Function of I,G by A3,GROUP_19:10;
thus h1.x = Product x0 by A1,A4
.= h2.x by A2,A4;
end;
hence h1 = h2 by FUNCT_2:63;
end;
end;
definition
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
G be Group,
M be DirectSumComponents of G,I,
N be Group-Family of I,J,
h be ManySortedSet of I;
assume
A2: for i be Element of I holds
ex hi be Homomorphism of (sum_bundle N).i, M.i
st hi = h.i & hi is bijective;
func ProductHom(G,M,N,h) -> Homomorphism of dsum N, sum M means :Def16:
it = SumMap(sum_bundle N,M,h) & it is bijective;
existence
proof
dom h = I by PARTFUN1:def 2;
hence thesis by A2,GROUP_19:41;
end;
uniqueness;
end;
theorem Th39:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
G be Group,
M be DirectSumComponents of G,I,
N be Group-Family of I,J
st for i be Element of I holds
N.i is DirectSumComponents of M.i,J.i
holds
Union N is DirectSumComponents of G,Union J
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
G be Group,
M be DirectSumComponents of G,I,
N be Group-Family of I,J;
assume
A1: for i be Element of I holds
N.i is DirectSumComponents of M.i,J.i;
consider fM2G be Homomorphism of sum M,G such that
A2: fM2G is bijective by GROUP_19:def 8;
deffunc P(object) = [#] sum N.In($1,I);
consider DS being Function such that
A3: dom DS = I
& for i be object st i in I holds DS.i = P(i) from FUNCT_1:sch 3;
reconsider DS as ManySortedSet of I by A3,PARTFUN1:def 2,RELAT_1:def 18;
deffunc Q(object) = [#](M.In($1,I));
consider RS being Function such that
A4: dom RS = I
& for i be object st i in I holds RS.i = Q(i) from FUNCT_1:sch 3;
reconsider RS as ManySortedSet of I by A4,PARTFUN1:def 2,RELAT_1:def 18;
defpred R[object,object] means
ex fi be Homomorphism of sum N.In($1,I), M.In($1,I)
st fi = $2 & fi is bijective;
A5: for i being Element of I
ex y being Element of PFuncs(Union DS,Union RS) st R[i,y]
proof
let i being Element of I;
N.i is DirectSumComponents of M.i,J.i by A1; then
consider h be Homomorphism of sum(N.i), M.i such that
A6: h is bijective by GROUP_19:def 8;
A7: In(i,I) = i;
DS.i = [#] sum(N.i) & RS.i = [#](M.i) by A3,A4,A7;
then [#] sum(N.i) c= Union DS & [#](M.i) c= Union RS
by A3,A4,FUNCT_1:3,ZFMISC_1:74; then
dom h c= Union DS & rng h c= Union RS; then
reconsider y = h as Element of PFuncs(Union DS,Union RS)
by PARTFUN1:def 3;
take y;
thus thesis by A6;
end;
consider fBN2M being Function of I,PFuncs(Union DS,Union RS) such that
A9: for i being Element of I holds R[i,fBN2M.i] from FUNCT_2:sch 3(A5);
reconsider fBN2M as ManySortedSet of I;
set fDN2M = ProductHom(G,M,N,fBN2M);
for i be Element of I holds
ex hi be Homomorphism of (sum_bundle N).i,M.i
st hi = fBN2M.i & hi is bijective
proof
let i be Element of I;
consider fi be Homomorphism of sum N.In(i,I), M.In(i,I) such that
A11: fi = fBN2M.i & fi is bijective by A9;
sum N.i = (sum_bundle N).i by Def7; then
reconsider fi as Homomorphism of (sum_bundle N).i, M.i;
take fi;
thus fi = fBN2M.i & fi is bijective by A11;
end; then
A12: fDN2M is bijective by Def16;
reconsider h = fM2G * fDN2M * sum2dsum(N)
as Homomorphism of sum(Union N),G;
take h;
fM2G * fDN2M is one-to-one onto by A2,A12,FUNCT_2:27; then
h is one-to-one onto by FUNCT_2:27;
hence thesis;
end;
theorem Th40:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
G be Group,
M be internal DirectSumComponents of G,I,
N be Group-Family of I,J
st for i be Element of I holds
N.i is internal DirectSumComponents of M.i,J.i
holds
Union N is internal DirectSumComponents of G,Union J
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
G be Group,
M be internal DirectSumComponents of G,I,
N be Group-Family of I,J;
assume
A1: for i be Element of I holds
N.i is internal DirectSumComponents of M.i,J.i;
A2: dom J = I by PARTFUN1:def 2;
consider fMtoG be Homomorphism of sum M,G such that
A3: fMtoG is bijective and
A4: for x be finite-support Function of I,G st x in sum M
holds fMtoG.x = Product x by GROUP_19:def 9;
defpred Q[object,object] means
ex Ni be internal DirectSumComponents of M.In($1,I),J.In($1,I)
st Ni = N.$1 & $2 = InterHom Ni;
A5: for i,f1,f2 be object st i in I & Q[i,f1] & Q[i,f2] holds f1 = f2;
A6: for x be object st x in I ex y be object st Q[x,y]
proof
let x be object;
assume x in I; then
reconsider i = x as Element of I;
reconsider Ni = N.i as internal DirectSumComponents of M.i,J.i by A1;
take y = InterHom(Ni);
thus thesis;
end;
consider fBNtoM being Function such that
A8: dom fBNtoM = I & for i be object st i in I holds Q[i,fBNtoM.i]
from FUNCT_1:sch 2(A5,A6);
reconsider fBNtoM as ManySortedSet of I
by A8,PARTFUN1:def 2,RELAT_1:def 18;
set fDNtoM = ProductHom(G,M,N,fBNtoM);
A9: for i be Element of I holds
ex hi be Homomorphism of (sum_bundle N).i,M.i
st hi = fBNtoM.i
& hi is bijective
& for x be finite-support Function of J.i,M.i
st x in (sum_bundle(N)).i holds hi.x = Product x
proof
let i be Element of I;
consider Ni be internal DirectSumComponents of M.In(i,I),J.In(i,I)
such that
A11: Ni = N.i & fBNtoM.i = InterHom Ni by A8;
A12: InterHom (Ni) is bijective
& for x be finite-support Function of J.i,M.i
st x in sum Ni holds (InterHom Ni).x = Product x by Def15;
A13: sum N.In(i,I) = (sum_bundle(N)).i by Def7; then
reconsider hi = InterHom Ni as Homomorphism of (sum_bundle N).i,M.i
by A11;
take hi;
thus hi = fBNtoM.i by A11;
thus hi is bijective by A12;
thus for x be finite-support Function of J.i,M.i
st x in (sum_bundle N).i holds hi.x = Product x
by A11,A13,Def15;
end;
A14: for i be Element of I holds
ex hi be Homomorphism of (sum_bundle N).i,M.i
st hi = fBNtoM.i & hi is bijective
proof
let i be Element of I;
consider hi be Homomorphism of (sum_bundle N).i,M.i such that
A15: hi = fBNtoM.i
& hi is bijective
& for x be finite-support Function of J.i,M.i
st x in (sum_bundle N).i holds hi.x = Product x by A9;
take hi;
thus thesis by A15;
end;
A16: fDNtoM is bijective by A14,Def16;
reconsider h = fMtoG * fDNtoM * sum2dsum(N)
as Homomorphism of sum(Union N),G;
fMtoG * fDNtoM is one-to-one onto by A3,A16,FUNCT_2:27; then
A18: h is one-to-one onto by FUNCT_2:27;
A19: for i be Element of I holds
N.i is DirectSumComponents of M.i,J.i by A1;
reconsider UJ = Union J as non empty set;
reconsider UN = Union N as DirectSumComponents of G,UJ by A19,Th39;
A20: for i be Element of I holds M.i is Subgroup of G by GROUP_19:def 9;
A21: for j be object st j in UJ holds UN.j is Subgroup of G
proof
let j be object;
assume j in UJ; then
consider Y be set such that
A22: j in Y & Y in rng J by TARSKI:def 4;
consider i being object such that
A23: i in dom J & Y = J.i by A22,FUNCT_1:def 3;
reconsider i as Element of I by A23;
A24: UN.j = (N.i).j by A22,A23,Th19;
N.i is internal DirectSumComponents of M.i,J.i by A1; then
A25: (N.i).j is Subgroup of M.i by A22,A23,GROUP_19:def 9;
M.i is Subgroup of G by GROUP_19:def 9;
hence UN.j is Subgroup of G by A24,A25,GROUP_2:56;
end; then
A26: for j be Element of UJ holds UN.j is Subgroup of G;
reconsider UN as Subgroup-Family of UJ,G by A21,GROUP_20:def 1;
for x be finite-support Function of UJ,G st x in sum UN
holds h.x = Product x
proof
let x be finite-support Function of UJ,G;
assume
A27: x in sum UN;
for j be Element of UJ, g be Element of UN.j
holds h.(1ProdHom(UN,j).g) = g
proof
let j be Element of UJ, g be Element of UN.j;
UN.j is Subgroup of G by A21; then
A28: g is Element of G by GROUP_2:42;
A29: 1ProdHom(UN,j).g in ProjGroup(UN,j); then
A30: 1ProdHom(UN,j).g in sum UN by GROUP_2:40; then
A31: 1ProdHom(UN,j).g in dom sum2dsum(N) by FUNCT_2:def 1; then
A32: h.(1ProdHom(UN,j).g)
= (fMtoG * fDNtoM).((sum2dsum N).(1ProdHom(UN,j).g)) by FUNCT_1:13;
A33: (sum2dsum N).(1ProdHom(UN,j).g) in [#] dsum N by A30,FUNCT_2:5;
A34: (fMtoG * fDNtoM).((sum2dsum N).(1ProdHom(UN,j).g))
= fMtoG.(fDNtoM.((sum2dsum N).(1ProdHom(UN,j).g)))
by A30,FUNCT_2:5,15;
A35: fDNtoM.((sum2dsum N).(1ProdHom(UN,j).g)) in sum M
by A33,FUNCT_2:5;
for i be object st i in I holds M.i is Subgroup of G
by GROUP_19:def 9; then
reconsider z = fDNtoM.((sum2dsum N).(1ProdHom(UN,j).g))
as finite-support Function of I,G by A35,GROUP_19:10;
A36: (fMtoG * fDNtoM).((sum2dsum N).(1ProdHom(UN,j).g))
= Product z by A4,A34,A35;
consider Y be set such that
A37: j in Y & Y in rng J by TARSKI:def 4;
consider k being object such that
A38: k in dom J & Y = J.k by A37,FUNCT_1:def 3;
reconsider k as Element of I by A38;
A39: UN.j = (N.k).j by A37,A38,Th19;
N.k is internal DirectSumComponents of M.k,J.k by A1; then
reconsider K = (N.k).j as Subgroup of M.k by A37,A38,GROUP_19:def 9;
A41: g in K by A39;
A42: sum2dsum N = (prod2dprod N) | sum(Union N) by Th36;
A43: (sum2dsum N).(1ProdHom(UN,j).g)
= (prod2dprod N).(1ProdHom(UN,j).g) by A31,A42,FUNCT_1:47;
1ProdHom(UN,j).g in product UN by A29,GROUP_2:40; then
reconsider y = 1ProdHom(UN,j).g as Element of product Union N;
reconsider t = (sum2dsum N).(1ProdHom(UN,j).g) as Element of dsum N
by A30,FUNCT_2:5;
A44: for i be Element of I
holds fBNtoM.i is Homomorphism of (sum_bundle N).i,M.i
proof
let i be Element of I;
ex hi be Homomorphism of (sum_bundle N).i,M.i
st hi = fBNtoM.i & hi is bijective by A14;
hence thesis;
end;
consider hk be Homomorphism of (sum_bundle N).k,M.k such that
A45: hk = fBNtoM.k & hk is bijective
& for x be finite-support Function of J.k,M.k
st x in (sum_bundle N).k holds hk.x = Product x by A9;
A46: hk is one-to-one & rng hk = [#](M.k) by A45,FUNCT_2:def 3; then
A47: hk" is Function of [#](M.k),[#]((sum_bundle N).k) by FUNCT_2:25;
A48: g in M.k by A41,GROUP_2:40; then
(hk").g is Element of (sum_bundle N).k by A47,FUNCT_2:5; then
SumMap(sum_bundle N,M,fBNtoM).(1ProdHom(sum_bundle N,k).((hk").g))
= 1ProdHom(M,k).(hk.((hk").g)) by A8,A44,A45,GROUP_19:42; then
A49: fDNtoM.(1ProdHom(sum_bundle N,k).((hk").g))
= 1ProdHom(M,k).(hk.((hk").g)) by A14,Def16
.= 1ProdHom(M,k).(g) by A46,A48,FUNCT_1:35;
reconsider hkg = (hk").g as Element of (sum_bundle N).k
by A47,A48,FUNCT_2:5;
A50: 1ProdHom(sum_bundle N,k).hkg in ProjGroup(sum_bundle N,k); then
A51: 1ProdHom(sum_bundle N,k).hkg in product(sum_bundle N)
by GROUP_2:40; then
reconsider p = 1ProdHom(sum_bundle N,k).hkg as Function;
A52: t in sum(sum_bundle N); then
t in product(sum_bundle N) by GROUP_2:40; then
A53: dom t = I by GROUP_19:3;
for i be object st i in dom p holds p.i = t.i
proof
let i0 be object;
assume i0 in dom p; then
reconsider i = i0 as Element of I by A51,GROUP_19:3;
reconsider yi = y | (J.i) as Function;
p.i in (sum_bundle N).i by A50,GROUP_2:40,GROUP_19:5; then
A54: p.i in sum(N.i) by Def7; then
A55: p.i in product(N.i) by GROUP_2:40;
reconsider xi = p.i as Function by A54;
y | (J.i) = t.i by A43,Th25; then
yi in (sum_bundle N).i by A52,GROUP_2:40,GROUP_19:5; then
yi in sum(N.i) by Def7; then
A56: yi in product(N.i) by GROUP_2:40; then
A57: dom yi = J.i by GROUP_19:3;
A58: p = 1_product(sum_bundle N) +* (k,hkg) by GROUP_12:def 3;
A59: y = 1_product(UN) +* (j,g) by GROUP_12:def 3;
per cases;
suppose
A60: i <> k; then
xi = 1_(sum_bundle N).i by A58,GROUP_12:1; then
A61: xi = 1_sum(N.i) by Def7;
for n be object st n in dom yi holds yi.n = xi.n
proof
let n0 be object;
assume
A62: n0 in dom yi; then
reconsider n = n0 as Element of J.i by A56,GROUP_19:3;
J.i /\ J.k = {} by A60,PROB_2:def 2,XBOOLE_0:def 7; then
A63: j <> n by A37,A38,XBOOLE_0:def 4;
J.i c= Union J by A2,FUNCT_1:3,ZFMISC_1:74; then
reconsider n1 = n as Element of UJ;
thus yi.n0 = y.n by A62,FUNCT_1:47
.= 1_UN.n1 by A59,A63,GROUP_12:1
.= 1_(N.i).n by Th19
.= (1_product(N.i)).n by GROUP_7:6
.= xi.n0 by A61,GROUP_2:44;
end; then
yi = xi by A55,A57,GROUP_19:3;
hence thesis by A43,Th25;
end;
suppose
A65: i = k; then
A66: xi = hkg by A58,GROUP_12:1;
for n be object st n in dom yi holds yi.n = xi.n
proof
let n0 be object;
assume
A67: n0 in dom yi; then
reconsider n = n0 as Element of J.i by A56,GROUP_19:3;
J.i c= Union J by A2,FUNCT_1:3,ZFMISC_1:74; then
reconsider n1 = n as Element of UJ;
A69: g is Element of K by A37,A38,Th19;
1_sum(N.k) in sum(N.k); then
A70: 1_sum(N.k) +* (j,g) in sum(N.k)
by A37,A38,A69,GROUP_19:25; then
A71: 1_sum(N.k) +* (j,g) in (sum_bundle N).k by Def7; then
1_sum(N.k) +* (j,g) in dom hk by FUNCT_2:def 1; then
A72: 1_product(N.k) +* (j,g) in dom hk by GROUP_2:44;
A73: N.k is internal DirectSumComponents of M.k,J.k by A1; then
A74: for j be Element of J.k holds (N.k).j is Subgroup of M.k
by GROUP_19:def 9;
A75: 1_product(N.k) = (J.k) --> 1_(M.k) by A74,GROUP_19:13;
set q = ((J.k) --> 1_(M.k)) +* (j,g);
A76: q in sum(N.k) by A70,A75,GROUP_2:44;
for j be object st j in J.k
holds (N.k).j is Subgroup of M.k by A73,GROUP_19:def 9; then
reconsider q as finite-support Function of (J.k),(M.k)
by A76,GROUP_19:10;
A77: q = 1_product(N.k) +* (j,g) by A74,GROUP_19:13
.= 1_sum(N.k) +* (j,g) by GROUP_2:44;
(N.k).j is Subgroup of M.k by A37,A38,A73,GROUP_19:def 9; then
g is Element of M.k by A39,GROUP_2:42; then
A78: Product q = g by A37,A38,GROUP_19:21;
hk.(1_sum(N.k) +* (j,g)) = g by A45,A71,A77,A78; then
(hk").(hk.(1_product(N.k) +* (j,g))) = (hk").g
by GROUP_2:44; then
A79: (hk").g = 1_product(N.k) +* (j,g) by A45,A72,FUNCT_1:34;
per cases;
suppose
A80: j <> n;
thus yi.n0 = y.n by A67,FUNCT_1:47
.= 1_UN.n1 by A59,A80,GROUP_12:1
.= 1_(N.i).n by Th19
.= xi.n0 by A37,A38,A39,A65,A66,A79,A80,GROUP_12:1;
end;
suppose
A81: j = n;
thus yi.n0 = y.n by A67,FUNCT_1:47
.= g by A59,A81,GROUP_12:1
.= xi.n0 by A37,A38,A39,A66,A79,A81,GROUP_12:1;
end;
end; then
yi = xi by A55,A57,GROUP_19:3;
hence thesis by A43,Th25;
end;
end; then
A82: z = (1ProdHom(M,k)).g by A49,A51,A53,FUNCT_1:2,GROUP_19:3;
g in M.k by A41,GROUP_2:40; then
A83: z = 1_product(M) +* (k,g) by A82,GROUP_12:def 3;
z = (I --> 1_G) +* (k,g) by A20,A83,GROUP_19:13;
hence thesis by A28,A32,A36,GROUP_19:21;
end;
hence thesis by A27,GROUP_20:18;
end;
hence thesis by A18,A26,GROUP_19:def 9;
end;
begin :: 4. Conservation rule of direct sum decomposition for layering
theorem Th41:
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
G be Group,
M be Group-Family of I
for N be Group-Family of I,J
st Union N is DirectSumComponents of G,Union J
& for i be Element of I holds
N.i is DirectSumComponents of M.i,J.i
holds
M is DirectSumComponents of G,I
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
G be Group,
M be Group-Family of I;
let N be Group-Family of I,J;
assume that
A1: Union N is DirectSumComponents of G,Union J and
A2: for i be Element of I holds
N.i is DirectSumComponents of M.i,J.i;
set UN = Union N;
consider fNtoG be Homomorphism of sum(UN),G such that
A3: fNtoG is bijective by A1,GROUP_19:def 8;
deffunc P(object) = the carrier of sum N.In($1,I);
consider DS being Function such that
A4: dom DS = I
& for i be object st i in I holds DS.i = P(i) from FUNCT_1:sch 3;
reconsider DS as ManySortedSet of I by A4,PARTFUN1:def 2,RELAT_1:def 18;
deffunc Q(object) = the carrier of M.In($1,I);
consider RS being Function such that
A5: dom RS = I
& for i be object st i in I holds RS.i = Q(i) from FUNCT_1:sch 3;
reconsider RS as ManySortedSet of I by A5,PARTFUN1:def 2,RELAT_1:def 18;
defpred R[object,object] means
ex fi be Homomorphism of M.In($1,I),sum N.In($1,I)
st fi = $2 & fi is bijective;
A6: for i being Element of I
ex y being Element of PFuncs(Union RS,Union DS) st R[i,y]
proof
let i being Element of I;
N.i is DirectSumComponents of M.i,J.i by A2; then
consider g be Homomorphism of sum (N.i), M.i such that
A7: g is bijective by GROUP_19:def 8;
reconsider h=g" as Homomorphism of M.i,sum (N.i) by A7,GROUP_6:62;
A8: h is bijective by A7,GROUP_6:63;
A9: In(i,I) = i;
DS.i in rng DS & RS.i in rng RS by A4,A5,FUNCT_1:3; then
the carrier of sum (N.i) in rng DS
& the carrier of (M.i) in rng RS by A4,A5,A9; then
the carrier of sum (N.i) c= Union DS
& the carrier of (M.i) c= Union RS by ZFMISC_1:74; then
dom h c= Union RS & rng h c= Union DS; then
reconsider y = h as Element of PFuncs(Union RS,Union DS)
by PARTFUN1:def 3;
take y;
thus ex h be Homomorphism of M.In(i,I), sum N.In(i,I)
st h = y & h is bijective by A8;
end;
consider fMtoBN being Function of I,PFuncs(Union RS,Union DS) such that
A10: for i being Element of I holds R[i,fMtoBN.i] from FUNCT_2:sch 3(A6);
A11: dom fMtoBN = I by FUNCT_2:def 1;
reconsider fMtoBN as ManySortedSet of I;
reconsider fMtoDN = SumMap(M,sum_bundle(N),fMtoBN)
as Homomorphism of sum M, dsum N;
for i be Element of I holds
ex hi be Homomorphism of M.i,(sum_bundle(N)).i
st hi = fMtoBN.i & hi is bijective
proof
let i be Element of I;
consider fi be Homomorphism of M.In(i,I),sum N.In(i,I) such that
A13: fi = fMtoBN.i & fi is bijective by A10;
sum N.In(i,I) = (sum_bundle N).i by Def7;
hence thesis by A13;
end; then
A14: fMtoDN is bijective by A11,GROUP_19:41;
reconsider h = fNtoG * dsum2sum(N) * fMtoDN as Homomorphism of sum M,G;
take h;
A15: fNtoG * dsum2sum(N) is one-to-one onto by A3,FUNCT_2:27;
h is one-to-one onto by A14,A15,FUNCT_2:27;
hence h is bijective;
end;
theorem
for I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
G be Group,
M be Subgroup-Family of I,G
for N be Group-Family of I,J
st Union N is internal DirectSumComponents of G,Union J
& for i be Element of I holds
N.i is internal DirectSumComponents of M.i,J.i
holds
M is internal DirectSumComponents of G,I
proof
let I be non empty set,
J be non-empty disjoint_valued ManySortedSet of I,
G be Group,
M be Subgroup-Family of I,G;
let N be Group-Family of I,J;
assume that
A1: Union N is internal DirectSumComponents of G,Union J and
A2: for i be Element of I holds
N.i is internal DirectSumComponents of M.i,J.i;
reconsider UJ = Union J as non empty set;
for i be Element of I holds
N.i is DirectSumComponents of M.i,J.i by A2; then
reconsider M as DirectSumComponents of G,I by A1,Th41;
A3: dom J = I by PARTFUN1:def 2;
consider fNtoG be Homomorphism of sum(Union N),G such that
A4: fNtoG is bijective and
A5: for x be finite-support Function of UJ,G st x in sum Union N
holds fNtoG.x = Product x by A1,GROUP_19:def 9;
defpred Q[object,object] means
ex Ni be internal DirectSumComponents of M.In($1,I),J.In($1,I)
st Ni = N.$1 & $2 = (InterHom Ni)";
A6: for x,y1,y2 be object st x in I & Q[x,y1] & Q[x,y2] holds y1 = y2;
A7: for x be object st x in I ex y be object st Q[x,y]
proof
let x be object;
assume
x in I; then
reconsider i = x as Element of I;
reconsider Ni = N.i as internal DirectSumComponents of M.i,J.i by A2;
take y = (InterHom Ni)";
thus thesis;
end;
consider fMtoBN being Function such that
A9: dom fMtoBN = I
& for i be object st i in I holds Q[i,fMtoBN.i]
from FUNCT_1:sch 2(A6,A7);
reconsider fMtoBN as ManySortedSet of I
by A9,PARTFUN1:def 2,RELAT_1:def 18;
reconsider fMtoDN = SumMap(M,sum_bundle(N),fMtoBN)
as Homomorphism of sum M, dsum N;
for i be Element of I holds
ex hi be Homomorphism of M.i,(sum_bundle(N)).i
st hi = fMtoBN.i & hi is bijective
proof
let i be Element of I;
consider Ni be internal DirectSumComponents of M.In(i,I),J.In(i,I)
such that
A11: Ni = N.i & fMtoBN.i = (InterHom Ni)" by A9;
reconsider g = (InterHom Ni) as Homomorphism of sum (N.i),M.i by A11;
reconsider fi=g" as Homomorphism of M.i,sum (N.i)
by A11,Def15,GROUP_6:62;
g is bijective by A11,Def15; then
A12: fi = fMtoBN.i & fi is bijective by A11,GROUP_6:63;
sum N.In(i,I) = (sum_bundle(N)).i by Def7;
hence thesis by A12;
end; then
A13: fMtoDN is bijective by A9,GROUP_19:41;
reconsider h = fNtoG * dsum2sum(N) * fMtoDN as Homomorphism of sum M,G;
A14: for i be Element of I holds
ex hi be Homomorphism of (sum_bundle N).i,M.i
st hi" = fMtoBN.i & hi is bijective
& for x be finite-support Function of J.i,M.i
st x in (sum_bundle N).i holds hi.x = Product x
proof
let i be Element of I;
consider Ni be internal DirectSumComponents of M.In(i,I),J.In(i,I)
such that
A16: Ni = N.i & fMtoBN.i = (InterHom Ni)" by A9;
A17: InterHom (Ni) is bijective
& for x be finite-support Function of J.i,M.i st x in sum Ni
holds (InterHom Ni).x = Product x by Def15;
A18: sum N.In(i,I) = (sum_bundle N).i by Def7; then
reconsider hi = InterHom Ni as Homomorphism of (sum_bundle N).i,M.i
by A16;
thus thesis by A16,A17,A18;
end;
A19: for i be Element of I holds
ex hi be Homomorphism of (sum_bundle N).i,M.i
st hi" = fMtoBN.i & hi is bijective
proof
let i be Element of I;
consider hi be Homomorphism of (sum_bundle N).i,M.i such that
A20: hi" = fMtoBN.i & hi is bijective
& for x be finite-support Function of J.i,M.i
st x in (sum_bundle N).i holds hi.x = Product x by A14;
take hi;
thus thesis by A20;
end;
fNtoG * dsum2sum(N) is one-to-one onto by A4,FUNCT_2:27; then
A21: h is one-to-one onto by A13,FUNCT_2:27;
for i be Element of I holds
N.i is DirectSumComponents of M.i,J.i by A2; then
reconsider UN = Union N as DirectSumComponents of G,UJ by Th39;
reconsider UJ = Union J as non empty set;
A22: for j be object st j in UJ holds UN.j is Subgroup of G
by A1,GROUP_19:def 9;
A23: for i be Element of I holds M.i is Subgroup of G
by GROUP_20:def 1;
reconsider UN as Subgroup-Family of UJ,G by A22,GROUP_20:def 1;
for x be finite-support Function of I,G st x in sum M holds h.x = Product x
proof
let x be finite-support Function of I,G;
assume
A24: x in sum M;
for i be Element of I, g be Element of M.i holds h.(1ProdHom(M,i).g) = g
proof
let i be Element of I, g be Element of M.i;
A25: dom dsum2sum N = the carrier of dsum(N) by FUNCT_2:def 1;
A26: 1ProdHom(M,i).g in ProjGroup(M,i); then
A27:1ProdHom(M,i).g in sum M by GROUP_2:40; then
1ProdHom(M,i).g in dom fMtoDN by FUNCT_2:def 1; then
A28: h.(1ProdHom(M,i).g)
= (fNtoG * dsum2sum(N)).(fMtoDN.(1ProdHom(M,i).g)) by FUNCT_1:13;
A29: (fMtoDN).(1ProdHom(M,i).g) in the carrier of dsum(N)
by A27,FUNCT_2:5;
A30: (fNtoG * dsum2sum(N)).(fMtoDN.(1ProdHom(M,i).g))
= fNtoG.((dsum2sum(N)).(fMtoDN.(1ProdHom(M,i).g)))
by A27,FUNCT_2:5,FUNCT_2:15;
A31: (dsum2sum(N)).(fMtoDN.(1ProdHom(M,i).g)) in sum(UN)
by A29,FUNCT_2:5;
for j be object st j in UJ holds UN.j is Subgroup of G
by A1,GROUP_19:def 9; then
reconsider z = (dsum2sum(N)).(fMtoDN.(1ProdHom(M,i).g))
as finite-support Function of UJ,G by A31,GROUP_19:10;
A32: (fNtoG * dsum2sum(N)).(fMtoDN.(1ProdHom(M,i).g))
= Product z by A5,A30,A31;
A33: (dsum2sum N).(fMtoDN.(1ProdHom(M,i).g))
= (dprod2prod N).(fMtoDN.(1ProdHom(M,i).g))
by A25,A27,FUNCT_1:47,FUNCT_2:5;
1ProdHom(M,i).g in product M by A26,GROUP_2:40; then
reconsider y = 1ProdHom(M,i).g as Element of product M;
fMtoDN.(1ProdHom(M,i).g) in dsum(N) by A27,FUNCT_2:5; then
fMtoDN.(1ProdHom(M,i).g) in dprod(N) by GROUP_2:40; then
reconsider t = fMtoDN.(1ProdHom(M,i).g) as Element of dprod(N);
A34: for k be Element of I holds t.k = z | (J.k) by A33,Def10;
A35: for i be Element of I
holds fMtoBN.i is Homomorphism of M.i,(sum_bundle(N)).i
proof
let i be Element of I;
ex hi be Homomorphism of (sum_bundle N).i,M.i st
hi" = fMtoBN.i & hi is bijective by A19;
hence thesis by GROUP_6:62;
end;
consider hi be Homomorphism of (sum_bundle N).i,M.i such that
A37: hi" = fMtoBN.i & hi is bijective
& for x be finite-support Function of J.i,M.i
st x in (sum_bundle N).i holds hi.x = Product x by A14;
A38: hi is one-to-one & rng hi = the carrier of (M.i)
by A37,FUNCT_2:def 3; then
A39: hi" is Function of the carrier of M.i,
the carrier of ((sum_bundle N).i) by FUNCT_2:25;
A40: hi" is Homomorphism of M.i,(sum_bundle(N)).i by A37,GROUP_6:62;
A41: fMtoDN.(1ProdHom(M,i).g)
= 1ProdHom(sum_bundle(N),i).(hi".g) by A9,A35,A37,A40,GROUP_19:42;
reconsider hkg = (hi").g as Element of (sum_bundle N).i
by A39,FUNCT_2:5;
1ProdHom(sum_bundle N,i).hkg in ProjGroup(sum_bundle N,i); then
1ProdHom(sum_bundle N,i).hkg in product(sum_bundle N)
by GROUP_2:40; then
reconsider p = 1ProdHom(sum_bundle N,i).hkg as Function;
A42: (hi").g in (sum_bundle N).i by A39,FUNCT_2:5; then
A43: (hi").g in sum(N.i) by Def7; then
reconsider hkg0= (hi").g as Function;
for j be object st j in J.i holds (N.i).j is Subgroup of G
proof
let j be object;
assume
A44: j in J.i;
N.i is internal DirectSumComponents of M.i,J.i by A2; then
A45: (N.i).j is Subgroup of M.i by A44,GROUP_19:def 9;
M.i is Subgroup of G by GROUP_20:def 1;
hence thesis by A45,GROUP_2:56;
end; then
reconsider hkg0 as finite-support Function of (J.i),G
by A43,GROUP_19:10;
J.i c= Union J by A3,FUNCT_1:3,ZFMISC_1:74; then
A46: J.i c= UJ;
A47: p.i = z| (J.i) by A34,A41;
A48: p = 1_product(sum_bundle N) +* (i,hkg) by GROUP_12:def 3;
A49: dom(1_product(sum_bundle N)) = I by GROUP_19:3; then
A50: z | (J.i) = hkg0 by A47,A48,FUNCT_7:31;
for m be object holds m in support(z) iff m in support (hkg0)
proof
let m be object;
hereby
assume QX: m in support(z); then
A51: z.m <> 1_G & m in UJ by GROUP_19:def 2; then
consider Y be set such that
A52: m in Y & Y in rng J by TARSKI:def 4;
consider k being object such that
A53: k in dom J & Y = J.k by A52,FUNCT_1:def 3;
reconsider k as Element of I by A53;
A54: k = i
proof
assume
A55: k <> i;
UN.m = (N.k).m by A52,A53,Th19; then
reconsider P = (N.k).m as Subgroup of G by A1,GROUP_19:def 9,QX;
p.k = 1_((sum_bundle(N)).k) by A48,A55,GROUP_12:1
.= 1_(sum (N.k)) by Def7; then
(z| (J.k)).m = (1_(sum (N.k))).m by A34,A41
.= (1_(product (N.k))).m by GROUP_2:44
.= 1_P by A52,A53,GROUP_7:6
.= 1_G by GROUP_2:44;
hence contradiction by A51,A52,A53,FUNCT_1:49;
end; then
z.m = (z| (J.i)).m by A52,A53,FUNCT_1:49
.= hkg0.m by A47,A48,A49,FUNCT_7:31;
hence m in support(hkg0) by A51,A52,A53,A54,GROUP_19:def 2;
end;
assume m in support(hkg0); then
A57: hkg0.m <> 1_G & m in J.i by GROUP_19:def 2;
z.m <> 1_G by A50,A57,FUNCT_1:49;
hence m in support z by A46,A57,GROUP_19:def 2;
end; then
A58: support(z) = support(hkg0) by TARSKI:2;
for j be object st j in J.i holds (N.i).j is Subgroup of M.i
proof
let j be object;
assume
A59: j in J.i;
N.i is internal DirectSumComponents of M.i,J.i by A2;
hence (N.i).j is Subgroup of M.i by A59,GROUP_19:def 9;
end; then
reconsider hkg01 = hkg0 as finite-support Function of (J.i),M.i
by A43,GROUP_19:10;
A60: M.i is Subgroup of G by GROUP_20:def 1;
g = hi.(hi".g) by A38,FUNCT_1:35
.= Product hkg01 by A37,A42
.= Product hkg0 by A60,GROUP_20:6;
hence thesis by A28,A32,A50,A58,RELAT_1:74;
end;
hence thesis by A24,GROUP_20:18;
end;
hence thesis by A21,A23,GROUP_19:def 9;
end;
::
:: trivial groups addition preservance
::
:: Corollary of Th39
::
theorem Th43:
for I2 be non empty set, F2 be Group-Family of I2
st for i be Element of I2 holds card (F2.i) = 1
holds card (the carrier of sum F2) = 1
proof
let I2 be non empty set,
F2 be Group-Family of I2;
assume
A1: for i be Element of I2 holds card (F2.i) = 1;
A2: for x be object holds 1_ sum F2 = x implies x in [#]sum F2;
for x be object holds x in [#]sum F2 implies x = 1_ sum F2
proof
let x be object;
assume
x in [#]sum F2; then
reconsider x as Element of product F2 by GROUP_2:42;
dom x = I2 by GROUP_19:3; then
reconsider x as ManySortedSet of I2 by PARTFUN1:def 2,RELAT_1:def 18;
for i be set st i in I2
ex G be Group-like non empty multMagma
st G = F2.i & x.i = 1_G
proof
let i be set;
assume i in I2; then
reconsider i as Element of I2;
reconsider G = F2.i as Group;
take G;
A3: card G = 1 by A1; then
A4: [#] G is finite;
A5: card {1_G} = 1 by CARD_1:30;
A6: [#]G = {1_G} by A3,A4,A5,CARD_2:102;
x in product F2; then
x.i in F2.i by GROUP_19:5;
hence thesis by A6,TARSKI:def 1;
end; then
x = 1_product F2 by GROUP_7:5;
hence thesis by GROUP_2:44;
end; then
[#]sum F2 = {1_ sum F2} by A2,TARSKI:def 1;
hence thesis by CARD_1:30;
end;
theorem Th44:
for I be non empty set,
G be Group,
x be finite-support Function of I,G
st for i be object st i in I holds x.i = 1_G
holds Product x = 1_G
proof
let I be non empty set,
G be Group,
x be finite-support Function of I,G;
assume
A1: for i be object st i in I holds x.i = 1_G;
support(x) = {}
proof
assume not support(x) = {}; then
consider i be object such that
A2: i in support(x) by XBOOLE_0:def 1;
x.i <> 1_G & i in I by A2,GROUP_19:def 2;
hence contradiction by A1;
end;
hence thesis by GROUP_19:15;
end;
theorem Th45:
for I be non empty set,
G be Group,
x be finite-support Function of I,G,
a be Element of G
st I = {1,2} & x = <*a,1_G*>
holds Product x = a
proof
let I be non empty set,
G be Group,
x be finite-support Function of I,G,
a be Element of G;
assume
A1: I = {1,2} & x = <*a,1_G*>;
reconsider i1 = 1 as Element of I by A1,TARSKI:def 2;
set y = (I --> 1_G) +* (i1,a);
A2: dom y = dom (I --> 1_G) by FUNCT_7:30
.= I by FUNCOP_1:13;
A3: dom (I --> 1_G) = I by FUNCOP_1:13;
for i be object st i in dom x holds x.i = y.i
proof
let i be object;
assume
A4: i in dom x; then
A5: i = 1 or i = 2 by A1,TARSKI:def 2;
reconsider i0 = i as Element of I by A4;
per cases;
suppose
A6: i = 1;
thus x.i = a by A1,A6
.= y.i by A3,A6,FUNCT_7:31;
end;
suppose
A7: i <> 1;
hence y.i = (I --> 1_G).i by FUNCT_7:32
.= 1_G by A4,FUNCOP_1:7
.= x.i by A1,A5,A7;
end;
end; then
x = (I --> 1_G) +* (i1,a) by A2,FUNCT_2:def 1;
hence thesis by GROUP_19:21;
end;
theorem
for G be Group,
I1,I2 be non empty set,
F1 be DirectSumComponents of G,I1,
F2 be Group-Family of I2
st I1 misses I2
& for i be Element of I2 holds card(F2.i) = 1
holds F1 +* F2 is DirectSumComponents of G,I1 \/ I2
proof
let G be Group,
I1, I2 be non empty set,
F1 be DirectSumComponents of G,I1,
F2 be Group-Family of I2;
assume that
A1: I1 misses I2 and
A2: for i be Element of I2 holds card (F2.i) = 1;
reconsider I = {1,2} as non empty set;
set J = {[1,I1], [2,I2]};
for x,y1,y2 be object st [x,y1] in J & [x,y2] in J holds y1 = y2
proof
let x,y1,y2 be object;
assume [x,y1] in J & [x,y2] in J; then
A3: ([x,y1] = [1,I1] or [x,y1] = [2,I2])
& ([x,y2] = [1,I1] or [x,y2] = [2,I2]) by TARSKI:def 2; then
per cases by XTUPLE_0:1;
suppose
x = 1 & y1 = I1;
hence y1 = y2 by A3,XTUPLE_0:1;
end;
suppose
x = 2 & y1 = I2;
hence y1 = y2 by A3,XTUPLE_0:1;
end;
end; then
reconsider J as Function by FUNCT_1:def 1;
dom J = I by RELAT_1:10; then
reconsider J as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
A4: rng J = {I1,I2} by RELAT_1:10;
[1,I1] in J by TARSKI:def 2; then
A5: 1 in dom J & J.1=I1 by FUNCT_1:1;
[2,I2] in J by TARSKI:def 2; then
A6: 2 in dom J & J.2=I2 by FUNCT_1:1;
not {} in rng J
proof
assume {} in rng J; then
consider x being object such that
A7: x in dom J & {} = J.x by FUNCT_1:def 3;
thus contradiction by A5,A6,A7,TARSKI:def 2;
end; then
J is non-empty; then
reconsider J as non-empty ManySortedSet of I;
for i,j be object st i<>j holds J.i misses J.j
proof
let i,j be object;
assume
A8: i<>j;
per cases;
suppose
not i in dom J or not j in dom J; then
J.i = {} or J.j = {} by FUNCT_1:def 2; then
J.i /\ J.j = {};
hence J.i misses J.j by XBOOLE_0:def 7;
end;
suppose
i in dom J & j in dom J; then
(i=1 or i=2) & (j=1 or j=2) by TARSKI:def 2;
hence J.i misses J.j by A1,A5,A6,A8;
end;
end; then
J is disjoint_valued; then
reconsider J as non-empty disjoint_valued ManySortedSet of I;
reconsider M = <* sum(F1), sum(F2) *> as Group-Family of I;
set w0 = the object;
card ([#] sum(F2)) = 1 by A2,Th43; then
card ([#] sum(F2)) = card {w0} by CARD_1:30; then
consider w be object such that
A9: {w} = [#] sum(F2) by CARD_1:29;
A10: for x,y be Function
st x in [#] product M & y in [#] product M & x.1 = y.1
holds x = y
proof
let x,y be Function;
assume that
A11: x in [#] product M and
A12: y in [#] product M and
A13: x.1 = y.1;
A14: dom x = I & dom y = I by A11,A12,GROUP_19:3;
for i be object st i in dom x holds x.i = y.i
proof
let i be object;
assume i in dom x; then
A15: i=1 or i=2 by A14,TARSKI:def 2;
A16: x in product M & y in product M by A11,A12;
reconsider p=x, q=y as Function;
B1: 2 is Element of I by TARSKI:def 2;
reconsider M2 = M.2 as Group;
p.2 in M2 & q.2 in M2 by A16,B1,GROUP_19:5; then
p.2 in sum F2 & q.2 in sum F2; then
p.2 = w & q.2 = w by A9,TARSKI:def 1;
hence thesis by A13,A15;
end;
hence thesis by A14;
end;
consider h1 be Homomorphism of sum F1, G such that
A17: h1 is bijective by GROUP_19:def 8;
set CS1 = the carrier of product M;
set CS2 = the carrier of G;
defpred P[Element of CS1,Element of CS2] means
$2 = h1.($1.1);
A18: for x being Element of CS1 ex y being Element of CS2 st P[x,y]
proof
let x be Element of CS1;
A19: x in product M;
reconsider x as Function;
B1: 1 is Element of I by TARSKI:def 2;
reconsider M1 = M.1 as Group;
x.1 in M1 by B1,A19,GROUP_19:5; then
x.1 in sum F1; then
h1.(x.1) in CS2 by FUNCT_2:5;
hence thesis;
end;
consider h being Function of CS1,CS2 such that
A20: for x being Element of CS1 holds P[x,h.x] from FUNCT_2:sch 3(A18);
reconsider h as Function of CS1,CS2;
for x1,x2 being object st x1 in CS1 & x2 in CS1 & h.x1 = h.x2 holds x1 = x2
proof
let x1,x2 be object;
assume
A21: x1 in CS1 & x2 in CS1 & h.x1 = h.x2; then
reconsider x10=x1, x20=x2 as Element of CS1;
A22: h.x10 = h1.(x10.1) by A20;
A23: h.x20 = h1.(x20.1) by A20;
A24:x1 in product M & x2 in product M by A21;
reconsider z1 = x1 as Function by A21;
reconsider z2 = x2 as Function by A21;
B2: 1 is Element of I by TARSKI:def 2;
reconsider M1 = M.1 as Group;
z1.1 in M1 & z2.1 in M1 by A24,B2,GROUP_19:5; then
A25: x10.1 in the carrier of sum F1
& x20.1 in the carrier of sum F1;
x10.1 = x20.1 by A17,A21,A22,A23,A25,FUNCT_2:19;
hence x1 = x2 by A10;
end; then
A26: h is one-to-one by FUNCT_2:19;
for y being object st y in CS2 ex x being object st x in CS1 & y = h.x
proof
let y being object;
assume y in CS2; then
y in rng h1 by A17,FUNCT_2:def 3; then
consider x1 be object such that
A27: x1 in [#](sum F1) & y = h1.x1 by FUNCT_2:11;
reconsider x1 as Element of [#] sum F1 by A27;
set z1 = the Element of [#] sum F2;
reconsider x = <*x1,z1*> as Element of CS1;
take x;
h.x = h1.(x.1) by A20
.= y by A27;
hence thesis;
end; then
rng h = CS2 by FUNCT_2:10; then
A28: h is onto by FUNCT_2:def 3;
for a,b be Element of CS1 holds h.(a * b) = h.a * h.b
proof
let a,b be Element of CS1;
A29: 1 in I by TARSKI:def 2;
A30: M.1 = sum F1;
A31: a in product M & b in product M;
reconsider a1=a, b1=b as Function;
B3: 1 is Element of I by TARSKI:def 2;
reconsider M1 = M.1 as Group;
a1.1 in M1 & b1.1 in M1 by B3,A31,GROUP_19:5; then
reconsider a1=a.1, b1=b.1 as Element of sum F1;
thus h.(a * b) = h1.((a*b).1) by A20
.= h1.(a1*b1) by A29,A30,GROUP_7:1
.= (h1.a1) * (h1.b1) by GROUP_6:def 6
.= (h1.a1) * (h.b) by A20
.= (h.a) * (h.b) by A20;
end; then
A32: h is Homomorphism of product M,G by GROUP_6:def 6;
product M = sum M by GROUP_7:9; then
reconsider M = <* sum(F1), sum(F2) *> as DirectSumComponents of G,I
by A26,A28,A32,GROUP_19:def 8;
set N = <* F1, F2 *>;
len N = 2 by FINSEQ_1:44; then
dom N = I by FINSEQ_1:2,def 3; then
reconsider N as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
A33: for i be Element of I holds N.i is Group-Family of J.i
proof
let i be Element of I;
per cases by TARSKI:def 2;
suppose
i = 1;
hence N.i is Group-Family of J.i by A5;
end;
suppose
i = 2;
hence N.i is Group-Family of J.i by A6;
end;
end; then
for i be Element of I holds N.i is multMagma-Family of J.i; then
reconsider N as multMagma-Family of I,J by Def4;
reconsider N as Group-Family of I,J by A33,Def5;
A34: for i be Element of I holds
N.i is DirectSumComponents of M.i,J.i
proof
let i be Element of I;
per cases by TARSKI:def 2;
suppose
A35: i=1;
set h = id the carrier of sum F1;
for a,b be Element of sum F1 holds h.(a * b) = h.a * h.b; then
A36: h is Homomorphism of sum(F1), sum(F1)
& h is bijective by GROUP_6:def 6;
thus N.i is DirectSumComponents of M.i,J.i
by A5,A35,A36,GROUP_19:def 8;
end;
suppose
A38: i=2;
set h = id the carrier of sum F2;
for a,b be Element of sum F2 holds h.(a * b) = h.a * h.b; then
A39: h is Homomorphism of sum(F2), sum(F2)
& h is bijective by GROUP_6:def 6;
thus N.i is DirectSumComponents of M.i,J.i
by A6,A38,A39,GROUP_19:def 8;
end;
end;
A41: I1 \/ I2 = Union J by A4,ZFMISC_1:75;
A42: dom (Union N) = Union J by PARTFUN1:def 2
.= (dom F1) \/ I2 by A41,PARTFUN1:def 2
.= (dom F1) \/ (dom F2) by PARTFUN1:def 2;
for x being object st x in dom F1 \/ dom F2 holds
(x in dom F2 implies (Union N).x = F2.x)
& (not x in dom F2 implies (Union N).x = F1.x)
proof
let x be object;
assume x in dom F1 \/ dom F2; then
A43: x in I1 \/ dom F2 by PARTFUN1:def 2; then
A44: x in I1 \/ I2 by PARTFUN1:def 2;
thus x in dom F2 implies (Union N).x = F2.x
proof
assume
A45: x in dom F2; then
reconsider i = x as Element of Union J by A41,XBOOLE_0:def 3;
reconsider j = 2 as Element of I by TARSKI:def 2;
(Union N).i = (N.j).i by A6,A45,Th19
.= F2.i;
hence thesis;
end;
thus not x in dom F2 implies (Union N).x = F1.x
proof
assume
A46: not x in dom F2;
reconsider i = x as Element of Union J by A41,A43,PARTFUN1:def 2;
reconsider j = 1 as Element of I by TARSKI:def 2;
not (x in I2) by A46,PARTFUN1:def 2; then
i in J.j by A5,A44,XBOOLE_0:def 3; then
(Union N).i = (N.j).i by Th19
.= F1.i;
hence thesis;
end;
end; then
F1 +* F2 =Union N by A42,FUNCT_4:def 1;
hence thesis by A34,A41,Th39;
end;
theorem
for G be Group,
I1, I2 be non empty set,
F1 be internal DirectSumComponents of G,I1,
F2 be Subgroup-Family of I2,G
st I1 misses I2 & F2 = I2 --> (1).G
holds
F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2
proof
let G be Group,
I1, I2 be non empty set,
F1 be internal DirectSumComponents of G,I1,
F2 be Subgroup-Family of I2,G;
assume that
A1: I1 misses I2 and
A2: F2 = I2 --> (1).G;
reconsider I = {1,2} as non empty set;
set J = {[1,I1], [2,I2]};
for x,y1,y2 be object
st [x,y1] in J & [x,y2] in J holds y1 = y2
proof
let x,y1,y2 be object;
assume
[x,y1] in J & [x,y2] in J; then
A3: ([x,y1] = [1,I1] or [x,y1] = [2,I2])
& ([x,y2] = [1,I1] or [x,y2] = [2,I2]) by TARSKI:def 2; then
per cases by XTUPLE_0:1;
suppose
x=1 & y1=I1;
hence y1=y2 by A3,XTUPLE_0:1;
end;
suppose
x=2 & y1=I2;
hence y1=y2 by A3,XTUPLE_0:1;
end;
end; then
reconsider J as Function by FUNCT_1:def 1;
dom J = I by RELAT_1:10; then
reconsider J as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
A4: rng J = {I1,I2} by RELAT_1:10;
[1,I1] in J & [2,I2] in J by TARSKI:def 2; then
A5: 1 in dom J & J.1=I1 & 2 in dom J & J.2=I2 by FUNCT_1:1;
not {} in rng J
proof
assume {} in rng J; then
consider x being object such that
A6: x in dom J & {} = J.x by FUNCT_1:def 3;
thus contradiction by A5,A6,TARSKI:def 2;
end; then
J is non-empty; then
reconsider J as non-empty ManySortedSet of I;
for i,j be object st i<>j holds J.i misses J.j
proof
let i,j be object;
assume
A7: i<>j;
per cases;
suppose
not i in dom J or not j in dom J; then
J.i = {} or J.j = {} by FUNCT_1:def 2; then
J.i /\ J.j = {};
hence J.i misses J.j by XBOOLE_0:def 7;
end;
suppose
i in dom J & j in dom J; then
(i=1 or i=2) & (j=1 or j=2) by TARSKI:def 2;
hence J.i misses J.j by A1,A5,A7;
end;
end; then
J is disjoint_valued; then
reconsider J as non-empty disjoint_valued ManySortedSet of I;
reconsider M = <* G, (1).G *> as Group-Family of I;
A8: for x,y be Function
st x in [#] product M & y in [#] product M & x.1 = y.1
holds x = y
proof
let x,y be Function;
assume that
A9: x in [#] product M and
A10: y in [#] product M and
A11: x.1 = y.1;
A12: dom x = I & dom y = I by A9,A10,GROUP_19:3;
for i be object st i in dom x holds x.i = y.i
proof
let i be object;
assume i in dom x; then
A13: i=1 or i=2 by A12,TARSKI:def 2;
A14: x in product M & y in product M by A9,A10;
reconsider p = x,q = y as Function;
B4: 2 is Element of I by TARSKI:def 2;
reconsider M2 = M.2 as Group;
p.2 in M2 & q.2 in M2 by A14,B4,GROUP_19:5; then
p.2 in (1).G & q.2 in (1).G; then
p.2 in {1_G} & q.2 in {1_G} by GROUP_2:def 7; then
p.2 = 1_G & q.2 = 1_G by TARSKI:def 1;
hence thesis by A11,A13;
end;
hence thesis by A12;
end;
set h1 = id the carrier of G;
for a,b be Element of G holds h1.(a*b) = h1.a * h1.b; then
reconsider h1 as Homomorphism of G,G by GROUP_6:def 6;
set CS1 = the carrier of product M;
set CS2 = the carrier of G;
defpred P[Element of CS1,Element of CS2] means
$2 = h1.($1.1);
A15: for x being Element of CS1
ex y being Element of CS2 st P[x,y]
proof
let x be Element of CS1;
A16: x in product M;
reconsider z = x as Function;
B5: 1 is Element of I by TARSKI:def 2;
reconsider M1 = M.1 as Group;
z.1 in M1 by A16,B5,GROUP_19:5; then
z.1 in G; then
h1.(z.1) in CS2 by FUNCT_2:5;
hence thesis;
end;
consider h being Function of CS1,CS2 such that
A17: for x being Element of CS1 holds P[x,h.x] from FUNCT_2:sch 3(A15);
reconsider h as Function of CS1,CS2;
A18: for x1,x2 being object st x1 in CS1 & x2 in CS1 & h.x1 = h.x2
holds x1 = x2
proof
let x1,x2 be object;
assume
A19: x1 in CS1 & x2 in CS1 & h.x1 = h.x2; then
reconsider x10=x1, x20=x2 as Element of CS1;
A20: h.x10 = h1.(x10.1) & h.x20 = h1.(x20.1) by A17;
A21: x1 in product M by A19;
reconsider z1 = x1 as Function by A19;
B6: 1 is Element of I by TARSKI:def 2;
reconsider M1 = M.1 as Group;
z1.1 in M1 by A21,B6,GROUP_19:5; then
A22: x10.1 in the carrier of G;
A23: x2 in product M by A19;
reconsider z2 = x2 as Function by A19;
z2.1 in M1 by A23,B6,GROUP_19:5; then
A24: x20.1 in the carrier of G;
x10.1 = x20.1 by A19,A20,A22,A24,FUNCT_2:19;
hence x1 = x2 by A8;
end; then
A25: h is one-to-one by FUNCT_2:19;
for y being object st y in CS2
ex x being object st x in CS1 & y = h.x
proof
let y be object;
assume y in CS2; then
y in rng h1; then
consider x1 be object such that
A26: x1 in the carrier of G & y = h1.x1 by FUNCT_2:11;
reconsider x1 as Element of G by A26;
set z1 = the Element of the carrier of (1).G;
reconsider x = <*x1,z1*> as Element of CS1;
take x;
h.x = h1.(x.1) by A17
.= y by A26;
hence thesis;
end; then
rng h = CS2 by FUNCT_2:10; then
A27: h is onto by FUNCT_2:def 3;
A28: for a,b be Element of CS1 holds h.(a * b) = h.a * h.b
proof
let a,b be Element of CS1;
A29: h.a = h1.(a.1) & h.b = h1.(b.1) by A17;
A30: 1 in I by TARSKI:def 2;
A31: M.1 = G;
A32: a in product M & b in product M;
reconsider a1 = a, b1 = b as Function;
B8: 1 is Element of I by TARSKI:def 2;
reconsider M1 = M.1 as Group;
a1.1 in M1 & b1.1 in M1 by A32,B8,GROUP_19:5; then
reconsider a1 = a.1, b1 = b.1 as Element of G;
thus h.(a * b) = h1.((a*b).1) by A17
.= h1.(a1*b1) by A30,A31,GROUP_7:1
.= (h.a) * (h.b) by A29;
end;
product M = sum M by GROUP_7:9; then
A33: h is Homomorphism of sum M, G by A28,GROUP_6:def 6; then
reconsider M = <* G, (1).G *> as DirectSumComponents of G,I
by A25,A27,GROUP_19:def 8;
A34: for i be Element of I holds M.i is Subgroup of G
proof
let i be Element of I;
i = 1 or i = 2 by TARSKI:def 2;
hence thesis by GROUP_2:54;
end;
for x be finite-support Function of I,G st x in sum M holds h.x = Product x
proof
let x be finite-support Function of I,G;
assume NN:x in sum M; then
A36: x in product M by GROUP_7:9;
reconsider x0 = x as Element of CS1 by GROUP_7:9,NN;
B10: 1 in I by TARSKI:def 2;
reconsider M1 = M.1 as Group;
x0.1 in M1 by A36,B10,GROUP_19:5; then
reconsider x01=x0.1 as Element of G;
1_G in {1_G} by TARSKI:def 1; then
reconsider z1 = 1_G as Element of (1).G by GROUP_2:def 7;
reconsider xx = <*x01,z1*> as Element of CS1;
A37: h.xx = h1.(xx.1) by A17
.= h1.x01
.= x01;
h.x = h1.(x0.1) by A17
.= x01; then
A38: x = <*x01,1_G*> by A18,A37;
thus h.x = h1.(x0.1) by A17
.= Product x by A38,Th45;
end; then
reconsider M as internal DirectSumComponents of G,I
by A25,A27,A33,A34,GROUP_19:def 9;
set N = <* F1, F2 *>;
len N = 2 by FINSEQ_1:44; then
dom N = I by FINSEQ_1:2,def 3; then
reconsider N as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
A39: for i be Element of I holds N.i is Group-Family of J.i
proof
let i be Element of I;
per cases by TARSKI:def 2;
suppose
i = 1;
hence N.i is Group-Family of J.i by A5;
end;
suppose
i = 2;
hence N.i is Group-Family of J.i by A5;
end;
end; then
for i be Element of I holds N.i is multMagma-Family of J.i; then
reconsider N as multMagma-Family of I,J by Def4;
reconsider N as Group-Family of I,J by A39,Def5;
A40: for i be Element of I holds
N.i is internal DirectSumComponents of M.i,J.i
proof
let i be Element of I;
per cases by TARSKI:def 2;
suppose i=1;
hence thesis by A5;
end;
suppose
A42: i=2;
for i be Element of I2 holds card(F2.i) = 1
proof
let i be Element of I2;
the carrier of (F2.i) = the carrier of ((1).G) by A2,FUNCOP_1:7
.= {1_G} by GROUP_2:def 7;
hence thesis by CARD_1:30;
end; then
A43: card(the carrier of sum F2) = 1 by Th43;
card { 0 } = 1 by CARD_1:30; then
consider a being object such that
A44: the carrier of sum F2 = { a } by A43,CARD_1:29;
A45: the carrier of sum F2 = {1_(sum F2)} by A44,TARSKI:def 1;
reconsider Z = the carrier of sum F2 as non empty set;
set h = Z --> 1_G;
A46: dom h = the carrier of sum F2 & rng h c= {1_G} by FUNCOP_1:13;
{1_G} = the carrier of (1).G by GROUP_2:def 7; then
reconsider h as Function of the carrier of sum F2,the carrier of (1).G
by A46,FUNCT_2:2;
for a,b be Element of the carrier of sum F2
holds h.(a * b) = h.a * h.b
proof
let a,b be Element of the carrier of sum F2;
A47: 1_G = 1_((1).G) by GROUP_2:44;
thus h.(a * b) = 1_G by FUNCOP_1:7
.= 1_((1).G) * 1_((1).G) by A47,GROUP_1:def 4
.= (h.a) * 1_((1).G) by A47,FUNCOP_1:7
.= (h.a) * (h.b) by A47,FUNCOP_1:7;
end; then
reconsider h as Homomorphism of sum F2, (1).G by GROUP_6:def 6;
for x1,x2 being object
st x1 in the carrier of sum F2
& x2 in the carrier of sum F2
& h.x1 = h.x2 holds x1 = x2
proof
let x1,x2 be object;
assume
A48: x1 in the carrier of sum F2
& x2 in the carrier of sum F2 & h.x1 = h.x2;
hence x1 = 1_(sum F2) by A45,TARSKI:def 1
.= x2 by A45,A48,TARSKI:def 1;
end; then
A49: h is one-to-one by FUNCT_2:19;
for y being object st y in the carrier of (1).G
ex x being object st x in the carrier of sum F2 & y = h.x
proof
let y be object;
assume y in the carrier of (1).G; then
y in {1_G} by GROUP_2:def 7; then
A50: y = 1_G by TARSKI:def 1;
set x = 1_(sum F2);
take x;
thus x in the carrier of sum F2;
thus thesis by A50,FUNCOP_1:7;
end; then
rng h = the carrier of (1).G by FUNCT_2:10; then
A51: h is onto by FUNCT_2:def 3;
A52:N.i= F2 & M.i = (1).G by A42;
reconsider h as Homomorphism of sum (N.i), M.i by A5,A42;
reconsider Ni = N.i as DirectSumComponents of M.i,J.i
by A5,A42,A49,A51,GROUP_19:def 8;
A53: for j be Element of J.i holds Ni.j is Subgroup of M.i
proof
let j be Element of J.i;
F2.j = (1).G by A2,A5,A42,FUNCOP_1:7;
hence Ni.j is Subgroup of M.i by A52,GROUP_2:54;
end;
A54: for x be finite-support Function of J.i,M.i st x in sum Ni
holds h.x = Product x
proof
let x be finite-support Function of J.i,M.i;
assume
A55: x in sum Ni;
for k be object st k in J.i holds x.k = 1_M.i
proof
let k be object;
assume
A56: k in J.i; then
reconsider k0 = k as Element of J.i;
reconsider N = F2.k0 as Group by A2,A5,A42,FUNCOP_1:7;
A57: F2.k = (1).G by A2,A5,A42,A56,FUNCOP_1:7;
x in sum F2 by A5,A42,A55; then
x in product F2 by GROUP_2:40; then
x.k0 in N by A5,A42,GROUP_19:5; then
A58:x.k in {1_G} by A57,GROUP_2:def 7;
1_G = 1_((1).G) by GROUP_2:44
.= 1_(M.i) by A42;
hence thesis by A58,TARSKI:def 1;
end; then
Product x = 1_M.i by Th44
.= 1_((1).G) by A42
.= 1_G by GROUP_2:44;
hence thesis by A5,A42,A55,FUNCOP_1:7;
end;
Ni is internal by A49,A51,A52,A53,A54;
hence thesis;
end;
end;
A59: I1 \/ I2 = Union J by A4,ZFMISC_1:75;
A60: dom (Union N) = Union J by PARTFUN1:def 2
.= (dom F1) \/ I2 by A59,PARTFUN1:def 2
.= (dom F1) \/ (dom F2) by PARTFUN1:def 2;
for x being object st x in dom F1 \/ dom F2 holds
(x in dom F2 implies (Union N).x = F2.x)
& (not x in dom F2 implies (Union N).x = F1.x)
proof
let x be object;
assume x in dom F1 \/ dom F2; then
A61: x in I1 \/ dom F2 by PARTFUN1:def 2; then
A62: x in I1 \/ I2 by PARTFUN1:def 2;
thus x in dom F2 implies (Union N).x = F2.x
proof
assume B32:x in dom F2; then
reconsider i=x as Element of Union J by A59,XBOOLE_0:def 3;
reconsider j=2 as Element of I by TARSKI:def 2;
(Union N).i = (N.j).i by A5,B32,Th19
.= F2.i;
hence thesis;
end;
thus not x in dom F2 implies (Union N).x = F1.x
proof
assume not x in dom F2; then
A63: not x in I2 by PARTFUN1:def 2;
reconsider i=x as Element of Union J by A59,A61,PARTFUN1:def 2;
reconsider j=1 as Element of I by TARSKI:def 2;
i in J.j by A5,A62,A63,XBOOLE_0:def 3; then
(Union N).i = (N.j).i by Th19
.= F1.i;
hence thesis;
end;
end; then
F1 +* F2 = Union N by A60,FUNCT_4:def 1;
hence thesis by A40,A59,Th40;
end;