:: by Kazuhisa Nakasho , Hiroshi Yamazaki , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received December 31, 2015

:: Copyright (c) 2015-2016 Association of Mizar Users

definition

let I, J be non empty set ;

let a be Function of I,J;

let F be multMagma-Family of J;

:: original: *

redefine func F * a -> multMagma-Family of I;

correctness

coherence

a * F is multMagma-Family of I;

end;
let a be Function of I,J;

let F be multMagma-Family of J;

:: original: *

redefine func F * a -> multMagma-Family of I;

correctness

coherence

a * F is multMagma-Family of I;

proof end;

definition

let I, J be non empty set ;

let a be Function of I,J;

let F be Group-Family of J;

:: original: *

redefine func F * a -> Group-Family of I;

correctness

coherence

a * F is Group-Family of I;

end;
let a be Function of I,J;

let F be Group-Family of J;

:: original: *

redefine func F * a -> Group-Family of I;

correctness

coherence

a * F is Group-Family of I;

proof end;

definition

let I, J be non empty set ;

let a be Function of I,J;

let G be Group;

let F be Subgroup-Family of J,G;

correctness

coherence

F * a is Subgroup-Family of I,G;

end;
let a be Function of I,J;

let G be Group;

let F be Subgroup-Family of J,G;

correctness

coherence

F * a is Subgroup-Family of I,G;

proof end;

:: deftheorem defines * GROUP_21:def 1 :

for I, J being non empty set

for a being Function of I,J

for G being Group

for F being Subgroup-Family of J,G holds F * a = F * a;

for I, J being non empty set

for a being Function of I,J

for G being Group

for F being Subgroup-Family of J,G holds F * a = F * a;

registration

let I be set ;

correctness

existence

ex b_{1} being ManySortedSet of I st

( b_{1} is non-empty & b_{1} is disjoint_valued );

end;
correctness

existence

ex b

( b

proof end;

theorem Th35: :: GROUP_21:2

for X, Y being non empty set

for X0, Y0 being set

for f being Function of X,Y st f is bijective & rng (f | X0) = Y0 holds

(f | X0) " = (f ") | Y0

for X0, Y0 being set

for f being Function of X,Y st f is bijective & rng (f | X0) = Y0 holds

(f | X0) " = (f ") | Y0

proof end;

Lm0193: for I being set

for F being multMagma-Family of I

for x being Element of (product F) holds dom x = I

by GROUP_19:3;

Lm0194: for I being non empty set

for F being multMagma-Family of I

for x being Element of I holds (Carrier F) . x = [#] (F . x)

by GROUP_19:4;

Lm0195: for I being non empty set

for F being multMagma-Family of I

for x being Function

for i being Element of I st x in product F holds

x . i in F . i

by GROUP_19:5;

:: for substitution of subscript set

theorem Th1: :: GROUP_21:3

for I, J being non empty set

for a being Function of I,J

for F being multMagma-Family of J

for x being Element of (product F) holds x * a in product (F * a)

for a being Function of I,J

for F being multMagma-Family of J

for x being Element of (product F) holds x * a in product (F * a)

proof end;

definition

let I, J be non empty set ;

let a be Function of I,J;

let F be multMagma-Family of J;

ex b_{1} being Function of (product F),(product (F * a)) st

for x being Element of (product F) holds b_{1} . x = x * a

for b_{1}, b_{2} being Function of (product F),(product (F * a)) st ( for x being Element of (product F) holds b_{1} . x = x * a ) & ( for x being Element of (product F) holds b_{2} . x = x * a ) holds

b_{1} = b_{2}

end;
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: :: GROUP_21:def 2

for x being Element of (product F) holds it . x = x * a;

existence for x being Element of (product F) holds it . x = x * a;

ex b

for x being Element of (product F) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines trans_prod GROUP_21:def 2 :

for I, J being non empty set

for a being Function of I,J

for F being multMagma-Family of J

for b_{5} being Function of (product F),(product (F * a)) holds

( b_{5} = trans_prod (F,a) iff for x being Element of (product F) holds b_{5} . x = x * a );

for I, J being non empty set

for a being Function of I,J

for F being multMagma-Family of J

for b

( b

theorem Th2: :: GROUP_21:4

for I, J being non empty set

for a being Function of I,J

for F being multMagma-Family of J holds trans_prod (F,a) is multiplicative

for a being Function of I,J

for F being multMagma-Family of J holds trans_prod (F,a) is multiplicative

proof end;

definition

let I, J be non empty set ;

let a be Function of I,J;

let F be Group-Family of J;

:: original: trans_prod

redefine func trans_prod (F,a) -> Homomorphism of (product F),(product (F * a));

correctness

coherence

trans_prod (F,a) is Homomorphism of (product F),(product (F * a));

by Th2;

end;
let a be Function of I,J;

let F be Group-Family of J;

:: original: trans_prod

redefine func trans_prod (F,a) -> Homomorphism of (product F),(product (F * a));

correctness

coherence

trans_prod (F,a) is Homomorphism of (product F),(product (F * a));

by Th2;

theorem Th3: :: GROUP_21:5

for I, J being non empty set

for a being Function of I,J

for F being multMagma-Family of J

for y being Element of (product (F * a)) st a is bijective holds

y * (a ") in product F

for a being Function of I,J

for F being multMagma-Family of J

for y being Element of (product (F * a)) st a is bijective holds

y * (a ") in product F

proof end;

theorem Th4: :: GROUP_21:6

for I, J being non empty set

for a being Function of I,J

for x, y being Function st dom x = I & dom y = J & a is bijective holds

( x = y * a iff y = x * (a ") )

for a being Function of I,J

for x, y being Function st dom x = I & dom y = J & a is bijective holds

( x = y * a iff y = x * (a ") )

proof end;

theorem Th5: :: GROUP_21:7

for I, J being non empty set

for F being multMagma-Family of J

for a being Function of I,J st a is bijective holds

( dom (trans_prod (F,a)) = [#] (product F) & rng (trans_prod (F,a)) = [#] (product (F * a)) )

for F being multMagma-Family of J

for a being 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 end;

theorem Th6: :: GROUP_21:8

for I, J being non empty set

for a being Function of I,J

for F being multMagma-Family of J st a is bijective holds

trans_prod (F,a) is bijective

for a being Function of I,J

for F being multMagma-Family of J st a is bijective holds

trans_prod (F,a) is bijective

proof end;

theorem Th7: :: GROUP_21:9

for I, J being non empty set

for a being Function of I,J

for F being Group-Family of J

for x being Function st a is one-to-one holds

a .: (support ((x * a),(F * a))) c= support (x,F)

for a being Function of I,J

for F being Group-Family of J

for x being Function st a is one-to-one holds

a .: (support ((x * a),(F * a))) c= support (x,F)

proof end;

theorem Th8: :: GROUP_21:10

for I, J being non empty set

for a being Function of I,J

for F being Group-Family of J

for x being Function st a is onto holds

support (x,F) c= a .: (support ((x * a),(F * a)))

for a being Function of I,J

for F being Group-Family of J

for x being Function st a is onto holds

support (x,F) c= a .: (support ((x * a),(F * a)))

proof end;

theorem Th9: :: GROUP_21:11

for I, J being non empty set

for a being Function of I,J

for F being Group-Family of J

for x being Function st a is one-to-one & x in sum F holds

x * a in sum (F * a)

for a being Function of I,J

for F being Group-Family of J

for x being Function st a is one-to-one & x in sum F holds

x * a in sum (F * a)

proof end;

theorem Th10: :: GROUP_21:12

for I, J being non empty set

for a being Function of I,J

for F being Group-Family of J

for x being Function st a is bijective holds

( x in sum F iff ( x * a in sum (F * a) & dom x = J ) )

for a being Function of I,J

for F being Group-Family of J

for x being Function st a is bijective holds

( x in sum F iff ( x * a in sum (F * a) & dom x = J ) )

proof 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 ;

coherence

(trans_prod (F,a)) | (sum F) is Function of (sum F),(sum (F * a));

end;
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: :: GROUP_21:def 3

(trans_prod (F,a)) | (sum F);

correctness (trans_prod (F,a)) | (sum F);

coherence

(trans_prod (F,a)) | (sum F) is Function of (sum F),(sum (F * a));

proof end;

:: deftheorem Def3 defines trans_sum GROUP_21:def 3 :

for I, J being non empty set

for a being Function of I,J

for F being Group-Family of J st a is bijective holds

trans_sum (F,a) = (trans_prod (F,a)) | (sum F);

for I, J being non empty set

for a being Function of I,J

for F being Group-Family of J st a is bijective holds

trans_sum (F,a) = (trans_prod (F,a)) | (sum F);

theorem Th11: :: GROUP_21:13

for G, H being Group

for H0 being Subgroup of H

for f being Homomorphism of G,H st rng f c= [#] H0 holds

f is Homomorphism of G,H0

for H0 being Subgroup of H

for f being Homomorphism of G,H st rng f c= [#] H0 holds

f is Homomorphism of G,H0

proof 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 ;

:: original: trans_sum

redefine func trans_sum (F,a) -> Homomorphism of (sum F),(sum (F * a));

correctness

coherence

trans_sum (F,a) is Homomorphism of (sum F),(sum (F * a));

end;
let a be Function of I,J;

let F be Group-Family of J;

assume A1: a is bijective ;

:: original: trans_sum

redefine func trans_sum (F,a) -> Homomorphism of (sum F),(sum (F * a));

correctness

coherence

trans_sum (F,a) is Homomorphism of (sum F),(sum (F * a));

proof end;

theorem Th12: :: GROUP_21:14

for I, J being non empty set

for a being Function of I,J

for F being Group-Family of J st a is bijective holds

trans_sum (F,a) is bijective

for a being Function of I,J

for F being Group-Family of J st a is bijective holds

trans_sum (F,a) is bijective

proof end;

:: independent from subscript set

theorem Th13: :: GROUP_21:15

for G being Group

for I, J being non empty set

for F being DirectSumComponents of G,J

for a being Function of I,J st a is bijective holds

F * a is DirectSumComponents of G,I

for I, J being non empty set

for F being DirectSumComponents of G,J

for a being Function of I,J st a is bijective holds

F * a is DirectSumComponents of G,I

proof end;

theorem :: GROUP_21:16

for I being non empty set

for G being Group

for F being internal DirectSumComponents of G,I holds F is Subgroup-Family of I,G

for G being Group

for F being internal DirectSumComponents of G,I holds F is Subgroup-Family of I,G

proof end;

theorem Th15: :: GROUP_21:17

for I, J being non empty set

for G being Group

for x being Function of I,G

for y being Function of J,G

for a being Function of I,J st a is onto & x = y * a holds

support y = a .: (support x)

for G being Group

for x being Function of I,G

for y being Function of J,G

for a being Function of I,J st a is onto & x = y * a holds

support y = a .: (support x)

proof end;

theorem Th16: :: GROUP_21:18

for I, J being non empty set

for G being commutative Group

for x being finite-support Function of I,G

for y being finite-support Function of J,G

for a being Function of I,J st a is bijective & x = y * a holds

Product x = Product y

for G being commutative Group

for x being finite-support Function of I,G

for y being finite-support Function of J,G

for a being Function of I,J st a is bijective & x = y * a holds

Product x = Product y

proof end;

theorem :: GROUP_21:19

for I, J being non empty set

for G being Group

for x being finite-support Function of I,G

for y being finite-support Function of J,G

for a being Function of I,J st a is bijective & x = y * a & ( for i, j being Element of I holds (x . i) * (x . j) = (x . j) * (x . i) ) holds

Product x = Product y

for G being Group

for x being finite-support Function of I,G

for y being finite-support Function of J,G

for a being Function of I,J st a is bijective & x = y * a & ( for i, j being Element of I holds (x . i) * (x . j) = (x . j) * (x . i) ) holds

Product x = Product y

proof end;

theorem :: GROUP_21:20

for G being Group

for I, J being non empty set

for F being internal DirectSumComponents of G,J

for a being Function of I,J st a is bijective holds

F * a is internal DirectSumComponents of G,I

for I, J being non empty set

for F being internal DirectSumComponents of G,J

for a being Function of I,J st a is bijective holds

F * a is internal DirectSumComponents of G,I

proof end;

definition

let I be non empty set ;

let J be ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being Element of I holds b_{1} . i is multMagma-Family of J . i

end;
let J be ManySortedSet of I;

mode multMagma-Family of I,J -> ManySortedSet of I means :Def4: :: GROUP_21:def 4

for i being Element of I holds it . i is multMagma-Family of J . i;

existence for i being Element of I holds it . i is multMagma-Family of J . i;

ex b

for i being Element of I holds b

proof end;

:: deftheorem Def4 defines multMagma-Family GROUP_21:def 4 :

for I being non empty set

for J, b_{3} being ManySortedSet of I holds

( b_{3} is multMagma-Family of I,J iff for i being Element of I holds b_{3} . i is multMagma-Family of J . i );

for I being non empty set

for J, b

( b

definition

let I be non empty set ;

let J be ManySortedSet of I;

ex b_{1} being multMagma-Family of I,J st

for i being Element of I holds b_{1} . i is Group-Family of J . i

end;
let J be ManySortedSet of I;

mode Group-Family of I,J -> multMagma-Family of I,J means :Def5: :: GROUP_21:def 5

for i being Element of I holds it . i is Group-Family of J . i;

existence for i being Element of I holds it . i is Group-Family of J . i;

ex b

for i being Element of I holds b

proof end;

:: deftheorem Def5 defines Group-Family GROUP_21:def 5 :

for I being non empty set

for J being ManySortedSet of I

for b_{3} being multMagma-Family of I,J holds

( b_{3} is Group-Family of I,J iff for i being Element of I holds b_{3} . i is Group-Family of J . i );

for I being non empty set

for J being ManySortedSet of I

for b

( b

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;

:: original: .

redefine func N . i -> multMagma-Family of J . i;

correctness

coherence

N . i is multMagma-Family of J . i;

by Def4;

end;
let J be ManySortedSet of I;

let N be multMagma-Family of I,J;

let i be Element of I;

:: original: .

redefine func N . i -> multMagma-Family of J . i;

correctness

coherence

N . i is multMagma-Family of J . i;

by Def4;

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;

:: original: .

redefine func N . i -> Group-Family of J . i;

correctness

coherence

N . i is Group-Family of J . i;

by Def5;

end;
let J be ManySortedSet of I;

let N be Group-Family of I,J;

let i be Element of I;

:: original: .

redefine func N . i -> Group-Family of J . i;

correctness

coherence

N . i is Group-Family of J . i;

by Def5;

definition

let I be non empty set ;

let J be disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

:: original: Union

redefine func Union F -> Group-Family of Union J;

correctness

coherence

Union F is Group-Family of Union J;

end;
let J be disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

:: original: Union

redefine func Union F -> Group-Family of Union J;

correctness

coherence

Union F is Group-Family of Union J;

proof end;

theorem Th19: :: GROUP_21:21

for I being non empty set

for J being disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for j being Element of I

for i being object st i in J . j holds

(Union F) . i = (F . j) . i

for J being disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for j being Element of I

for i being object st i in J . j holds

(Union F) . i = (F . j) . i

proof end;

definition

let I be non empty set ;

let J be ManySortedSet of I;

let F be multMagma-Family of I,J;

ex b_{1} being multMagma-Family of I st

for i being Element of I holds b_{1} . i = product (F . i)

for b_{1}, b_{2} being multMagma-Family of I st ( for i being Element of I holds b_{1} . i = product (F . i) ) & ( for i being Element of I holds b_{2} . i = product (F . i) ) holds

b_{1} = b_{2}

end;
let J be ManySortedSet of I;

let F be multMagma-Family of I,J;

func prod_bundle F -> multMagma-Family of I means :Def6: :: GROUP_21:def 6

for i being Element of I holds it . i = product (F . i);

existence for i being Element of I holds it . i = product (F . i);

ex b

for i being Element of I holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines prod_bundle GROUP_21:def 6 :

for I being non empty set

for J being ManySortedSet of I

for F being multMagma-Family of I,J

for b_{4} being multMagma-Family of I holds

( b_{4} = prod_bundle F iff for i being Element of I holds b_{4} . i = product (F . i) );

for I being non empty set

for J being ManySortedSet of I

for F being multMagma-Family of I,J

for b

( b

definition

let I be non empty set ;

let J be ManySortedSet of I;

let F be Group-Family of I,J;

:: original: prod_bundle

redefine func prod_bundle F -> Group-Family of I;

correctness

coherence

prod_bundle F is Group-Family of I;

end;
let J be ManySortedSet of I;

let F be Group-Family of I,J;

:: original: prod_bundle

redefine func prod_bundle F -> Group-Family of I;

correctness

coherence

prod_bundle F is Group-Family of I;

proof end;

definition

let I be non empty set ;

let J be ManySortedSet of I;

let F be Group-Family of I,J;

ex b_{1} being Group-Family of I st

for i being Element of I holds b_{1} . i = sum (F . i)

for b_{1}, b_{2} being Group-Family of I st ( for i being Element of I holds b_{1} . i = sum (F . i) ) & ( for i being Element of I holds b_{2} . i = sum (F . i) ) holds

b_{1} = b_{2}

end;
let J be ManySortedSet of I;

let F be Group-Family of I,J;

func sum_bundle F -> Group-Family of I means :Def7: :: GROUP_21:def 7

for i being Element of I holds it . i = sum (F . i);

existence for i being Element of I holds it . i = sum (F . i);

ex b

for i being Element of I holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines sum_bundle GROUP_21:def 7 :

for I being non empty set

for J being ManySortedSet of I

for F being Group-Family of I,J

for b_{4} being Group-Family of I holds

( b_{4} = sum_bundle F iff for i being Element of I holds b_{4} . i = sum (F . i) );

for I being non empty set

for J being ManySortedSet of I

for F being Group-Family of I,J

for b

( b

definition

let I be non empty set ;

let J be ManySortedSet of I;

let F be multMagma-Family of I,J;

correctness

coherence

product (prod_bundle F) is multMagma ;

;

end;
let J be ManySortedSet of I;

let F be multMagma-Family of I,J;

correctness

coherence

product (prod_bundle F) is multMagma ;

;

:: deftheorem defines dprod GROUP_21:def 8 :

for I being non empty set

for J being ManySortedSet of I

for F being multMagma-Family of I,J holds dprod F = product (prod_bundle F);

for I being non empty set

for J being ManySortedSet of I

for F being multMagma-Family of I,J holds dprod F = product (prod_bundle F);

registration

let I be non empty set ;

let J be non-empty ManySortedSet of I;

let F be multMagma-Family of I,J;

correctness

coherence

( not dprod F is empty & dprod F is constituted-Functions );

;

end;
let J be non-empty ManySortedSet of I;

let F be multMagma-Family of I,J;

correctness

coherence

( not dprod F is empty & dprod F is constituted-Functions );

;

registration

let I be non empty set ;

let J be non-empty ManySortedSet of I;

let F be Group-Family of I,J;

coherence

( dprod F is Group-like & dprod F is associative )

end;
let J be non-empty ManySortedSet of I;

let F be Group-Family of I,J;

coherence

( dprod F is Group-like & dprod F is associative )

proof end;

definition

let I be non empty set ;

let J be non-empty ManySortedSet of I;

let F be Group-Family of I,J;

correctness

coherence

sum (sum_bundle F) is Group;

;

end;
let J be non-empty ManySortedSet of I;

let F be Group-Family of I,J;

correctness

coherence

sum (sum_bundle F) is Group;

;

:: deftheorem defines dsum GROUP_21:def 9 :

for I being non empty set

for J being non-empty ManySortedSet of I

for F being Group-Family of I,J holds dsum F = sum (sum_bundle F);

for I being non empty set

for J being non-empty ManySortedSet of I

for F being Group-Family of I,J holds dsum F = sum (sum_bundle F);

registration

let I be non empty set ;

let J be non-empty ManySortedSet of I;

let F be Group-Family of I,J;

correctness

coherence

( not dsum F is empty & dsum F is constituted-Functions );

;

end;
let J be non-empty ManySortedSet of I;

let F be Group-Family of I,J;

correctness

coherence

( not dsum F is empty & dsum F is constituted-Functions );

;

theorem Th20: :: GROUP_21:22

for I being non empty set

for F1, F2 being Group-Family of I st ( for i being Element of I holds F1 . i is Subgroup of F2 . i ) holds

product F1 is Subgroup of product F2

for F1, F2 being Group-Family of I st ( for i being Element of I holds F1 . i is Subgroup of F2 . i ) holds

product F1 is Subgroup of product F2

proof end;

theorem :: GROUP_21:23

for I being non empty set

for F1, F2 being Group-Family of I st ( for i being Element of I holds F1 . i is Subgroup of F2 . i ) holds

sum F1 is Subgroup of sum F2

for F1, F2 being Group-Family of I st ( for i being Element of I holds F1 . i is Subgroup of F2 . i ) holds

sum F1 is Subgroup of sum F2

proof end;

theorem Th22: :: GROUP_21:24

for I being non empty set

for J being non-empty ManySortedSet of I

for F being Group-Family of I,J holds dsum F is Subgroup of dprod F

for J being non-empty ManySortedSet of I

for F being Group-Family of I,J holds dsum F is Subgroup of dprod F

proof 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;

:: original: dsum

redefine func dsum F -> Subgroup of dprod F;

correctness

coherence

dsum F is Subgroup of dprod F;

by Th22;

end;
let J be non-empty disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

:: original: dsum

redefine func dsum F -> Subgroup of dprod F;

correctness

coherence

dsum F is Subgroup of dprod F;

by Th22;

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;

ex b_{1} being Homomorphism of (dprod F),(product (Union F)) st

for x being Element of (dprod F)

for i being Element of I holds x . i = (b_{1} . x) | (J . i)

for b_{1}, b_{2} being Homomorphism of (dprod F),(product (Union F)) st ( for x being Element of (dprod F)

for i being Element of I holds x . i = (b_{1} . x) | (J . i) ) & ( for x being Element of (dprod F)

for i being Element of I holds x . i = (b_{2} . x) | (J . i) ) holds

b_{1} = b_{2}

end;
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: :: GROUP_21:def 10

for x being Element of (dprod F)

for i being Element of I holds x . i = (it . x) | (J . i);

existence for x being Element of (dprod F)

for i being Element of I holds x . i = (it . x) | (J . i);

ex b

for x being Element of (dprod F)

for i being Element of I holds x . i = (b

proof end;

uniqueness for b

for i being Element of I holds x . i = (b

for i being Element of I holds x . i = (b

b

proof end;

:: deftheorem Def10 defines dprod2prod GROUP_21:def 10 :

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for b_{4} being Homomorphism of (dprod F),(product (Union F)) holds

( b_{4} = dprod2prod F iff for x being Element of (dprod F)

for i being Element of I holds x . i = (b_{4} . x) | (J . i) );

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for b

( b

for i being Element of I holds x . i = (b

theorem Th23: :: GROUP_21:25

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for y being Element of (product (Union F))

for i being Element of I holds y | (J . i) in product (F . i)

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for y being Element of (product (Union F))

for i being Element of I holds y | (J . i) in product (F . i)

proof end;

Th24: for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds dprod2prod F is bijective

proof end;

registration

let I be non empty set ;

let J be non-empty disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

coherence

dprod2prod F is bijective by Th24;

end;
let J be non-empty disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

coherence

dprod2prod F is bijective by Th24;

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;

coherence

(dprod2prod F) " is Homomorphism of (product (Union F)),(dprod F);

by GROUP_6:62;

end;
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 :: GROUP_21:def 11

(dprod2prod F) " ;

correctness (dprod2prod F) " ;

coherence

(dprod2prod F) " is Homomorphism of (product (Union F)),(dprod F);

by GROUP_6:62;

:: deftheorem defines prod2dprod GROUP_21:def 11 :

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds prod2dprod F = (dprod2prod F) " ;

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds prod2dprod F = (dprod2prod F) " ;

theorem Th25: :: GROUP_21:26

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for x being Element of (product (Union F))

for i being Element of I holds x | (J . i) = ((prod2dprod F) . x) . i

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for x being Element of (product (Union F))

for i being Element of I holds x | (J . i) = ((prod2dprod F) . x) . i

proof end;

ThXX: for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds prod2dprod F is bijective

by GROUP_6:63;

registration

let I be non empty set ;

let J be non-empty disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

coherence

prod2dprod F is bijective by ThXX;

end;
let J be non-empty disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

coherence

prod2dprod F is bijective by ThXX;

theorem :: GROUP_21:27

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds prod2dprod F = (dprod2prod F) " ;

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds prod2dprod F = (dprod2prod F) " ;

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;

let x be Function;

ex b_{1} being disjoint_valued ManySortedSet of I st

for i being Element of I holds b_{1} . i = support ((x | (J . i)),(F . i))

for b_{1}, b_{2} being disjoint_valued ManySortedSet of I st ( for i being Element of I holds b_{1} . i = support ((x | (J . i)),(F . i)) ) & ( for i being Element of I holds b_{2} . i = support ((x | (J . i)),(F . i)) ) holds

b_{1} = b_{2}

end;
let J be non-empty disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

let x be Function;

func supp_restr (x,F) -> disjoint_valued ManySortedSet of I means :Def12: :: GROUP_21:def 12

for i being Element of I holds it . i = support ((x | (J . i)),(F . i));

existence for i being Element of I holds it . i = support ((x | (J . i)),(F . i));

ex b

for i being Element of I holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines supp_restr GROUP_21:def 12 :

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for x being Function

for b_{5} being disjoint_valued ManySortedSet of I holds

( b_{5} = supp_restr (x,F) iff for i being Element of I holds b_{5} . i = support ((x | (J . i)),(F . i)) );

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for x being Function

for b

( b

theorem Th28: :: GROUP_21:28

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for x being Function holds support (x,(Union F)) = Union (supp_restr (x,F))

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for x being Function holds support (x,(Union F)) = Union (supp_restr (x,F))

proof end;

theorem Th29: :: GROUP_21:29

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for x, y, z being 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)))) )

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for x, y, z being 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 end;

theorem Th31: :: GROUP_21:30

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for y being Function st y in sum (Union F) holds

ex x being Function st

( y = (dprod2prod F) . x & x in dsum F )

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for y being Function st y in sum (Union F) holds

ex x being Function st

( y = (dprod2prod F) . x & x in dsum F )

proof end;

theorem Th32: :: GROUP_21:31

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for x, y being Function st x in dsum F & x in dsum F holds

(dprod2prod F) . x in sum (Union F)

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J

for x, y being Function st x in dsum F & x in dsum F holds

(dprod2prod F) . x in sum (Union F)

proof end;

theorem Th33: :: GROUP_21:32

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds rng ((dprod2prod F) | (dsum F)) = [#] (sum (Union F))

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds rng ((dprod2prod F) | (dsum F)) = [#] (sum (Union F))

proof 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;

coherence

(dprod2prod F) | (dsum F) is Homomorphism of (dsum F),(sum (Union F));

end;
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 :: GROUP_21:def 13

(dprod2prod F) | (dsum F);

correctness (dprod2prod F) | (dsum F);

coherence

(dprod2prod F) | (dsum F) is Homomorphism of (dsum F),(sum (Union F));

proof end;

:: deftheorem defines dsum2sum GROUP_21:def 13 :

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds dsum2sum F = (dprod2prod F) | (dsum F);

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds dsum2sum F = (dprod2prod F) | (dsum F);

Th34: for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds dsum2sum F is bijective

proof end;

registration

let I be non empty set ;

let J be non-empty disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

coherence

dsum2sum F is bijective by Th34;

end;
let J be non-empty disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

coherence

dsum2sum F is bijective by Th34;

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;

coherence

(dsum2sum F) " is Homomorphism of (sum (Union F)),(dsum F);

by GROUP_6:62;

end;
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 :: GROUP_21:def 14

(dsum2sum F) " ;

correctness (dsum2sum F) " ;

coherence

(dsum2sum F) " is Homomorphism of (sum (Union F)),(dsum F);

by GROUP_6:62;

:: deftheorem defines sum2dsum GROUP_21:def 14 :

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds sum2dsum F = (dsum2sum F) " ;

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds sum2dsum F = (dsum2sum F) " ;

theorem Th36: :: GROUP_21:33

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds sum2dsum F = (prod2dprod F) | (sum (Union F))

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds sum2dsum F = (prod2dprod F) | (sum (Union F))

proof end;

Th37: for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds sum2dsum F is bijective

by GROUP_6:63;

registration

let I be non empty set ;

let J be non-empty disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

coherence

sum2dsum F is bijective by Th37;

end;
let J be non-empty disjoint_valued ManySortedSet of I;

let F be Group-Family of I,J;

coherence

sum2dsum F is bijective by Th37;

theorem :: GROUP_21:34

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for F being Group-Family of I,J holds dsum2sum F = (sum2dsum F) " by FUNCT_1:43;

for J being non-empty disjoint_valued ManySortedSet of I

for F being 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;

ex b_{1} being Homomorphism of (sum F),G st

( b_{1} is bijective & ( for x being finite-support Function of I,G st x in sum F holds

b_{1} . x = Product x ) )
by GROUP_19:def 9;

uniqueness

for b_{1}, b_{2} being Homomorphism of (sum F),G st b_{1} is bijective & ( for x being finite-support Function of I,G st x in sum F holds

b_{1} . x = Product x ) & b_{2} is bijective & ( for x being finite-support Function of I,G st x in sum F holds

b_{2} . x = Product x ) holds

b_{1} = b_{2}

end;
let G be Group;

let F be internal DirectSumComponents of G,I;

func InterHom F -> Homomorphism of (sum F),G means :Def15: :: GROUP_21:def 15

( it is bijective & ( for x being finite-support Function of I,G st x in sum F holds

it . x = Product x ) );

existence ( it is bijective & ( for x being finite-support Function of I,G st x in sum F holds

it . x = Product x ) );

ex b

( b

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem Def15 defines InterHom GROUP_21:def 15 :

for I being non empty set

for G being Group

for F being internal DirectSumComponents of G,I

for b_{4} being Homomorphism of (sum F),G holds

( b_{4} = InterHom F iff ( b_{4} is bijective & ( for x being finite-support Function of I,G st x in sum F holds

b_{4} . x = Product x ) ) );

for I being non empty set

for G being Group

for F being internal DirectSumComponents of G,I

for b

( b

b

definition

let I be non empty set ;

let J be non-empty disjoint_valued ManySortedSet of I;

let G be Group;

let M be DirectSumComponents of G,I;

let N be Group-Family of I,J;

let h be ManySortedSet of I;

assume A2: for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st

( hi = h . i & hi is bijective ) ;

ex b_{1} being Homomorphism of (dsum N),(sum M) st

( b_{1} = SumMap ((sum_bundle N),M,h) & b_{1} is bijective )

for b_{1}, b_{2} being Homomorphism of (dsum N),(sum M) st b_{1} = SumMap ((sum_bundle N),M,h) & b_{1} is bijective & b_{2} = SumMap ((sum_bundle N),M,h) & b_{2} is bijective holds

b_{1} = b_{2}
;

end;
let J be non-empty disjoint_valued ManySortedSet of I;

let G be Group;

let M be DirectSumComponents of G,I;

let N be Group-Family of I,J;

let h be ManySortedSet of I;

assume A2: for i being Element of I ex hi being 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: :: GROUP_21:def 16

( it = SumMap ((sum_bundle N),M,h) & it is bijective );

existence ( it = SumMap ((sum_bundle N),M,h) & it is bijective );

ex b

( b

proof end;

uniqueness for b

b

:: deftheorem Def16 defines ProductHom GROUP_21:def 16 :

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for G being Group

for M being DirectSumComponents of G,I

for N being Group-Family of I,J

for h being ManySortedSet of I st ( for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st

( hi = h . i & hi is bijective ) ) holds

for b_{7} being Homomorphism of (dsum N),(sum M) holds

( b_{7} = ProductHom (G,M,N,h) iff ( b_{7} = SumMap ((sum_bundle N),M,h) & b_{7} is bijective ) );

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for G being Group

for M being DirectSumComponents of G,I

for N being Group-Family of I,J

for h being ManySortedSet of I st ( for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st

( hi = h . i & hi is bijective ) ) holds

for b

( b

theorem Th39: :: GROUP_21:35

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for G being Group

for M being DirectSumComponents of G,I

for N being Group-Family of I,J st ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds

Union N is DirectSumComponents of G, Union J

for J being non-empty disjoint_valued ManySortedSet of I

for G being Group

for M being DirectSumComponents of G,I

for N being Group-Family of I,J st ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds

Union N is DirectSumComponents of G, Union J

proof end;

theorem Th40: :: GROUP_21:36

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for G being Group

for M being internal DirectSumComponents of G,I

for N being Group-Family of I,J st ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds

Union N is internal DirectSumComponents of G, Union J

for J being non-empty disjoint_valued ManySortedSet of I

for G being Group

for M being internal DirectSumComponents of G,I

for N being Group-Family of I,J st ( for i being 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 end;

theorem Th41: :: GROUP_21:37

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for G being Group

for M being Group-Family of I

for N being Group-Family of I,J st Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds

M is DirectSumComponents of G,I

for J being non-empty disjoint_valued ManySortedSet of I

for G being Group

for M being Group-Family of I

for N being Group-Family of I,J st Union N is DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is DirectSumComponents of M . i,J . i ) holds

M is DirectSumComponents of G,I

proof end;

theorem :: GROUP_21:38

for I being non empty set

for J being non-empty disjoint_valued ManySortedSet of I

for G being Group

for M being Subgroup-Family of I,G

for N being Group-Family of I,J st Union N is internal DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds

M is internal DirectSumComponents of G,I

for J being non-empty disjoint_valued ManySortedSet of I

for G being Group

for M being Subgroup-Family of I,G

for N being Group-Family of I,J st Union N is internal DirectSumComponents of G, Union J & ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds

M is internal DirectSumComponents of G,I

proof end;

::

:: trivial groups addition preservance

::

:: Corollary of Th39

::

:: trivial groups addition preservance

::

:: Corollary of Th39

::

theorem Th43: :: GROUP_21:39

for I2 being non empty set

for F2 being Group-Family of I2 st ( for i being Element of I2 holds card (F2 . i) = 1 ) holds

card the carrier of (sum F2) = 1

for F2 being Group-Family of I2 st ( for i being Element of I2 holds card (F2 . i) = 1 ) holds

card the carrier of (sum F2) = 1

proof end;

theorem Th44: :: GROUP_21:40

for I being non empty set

for G being Group

for x being finite-support Function of I,G st ( for i being object st i in I holds

x . i = 1_ G ) holds

Product x = 1_ G

for G being Group

for x being finite-support Function of I,G st ( for i being object st i in I holds

x . i = 1_ G ) holds

Product x = 1_ G

proof end;

theorem Th45: :: GROUP_21:41

for I being non empty set

for G being Group

for x being finite-support Function of I,G

for a being Element of G st I = {1,2} & x = <*a,(1_ G)*> holds

Product x = a

for G being Group

for x being finite-support Function of I,G

for a being Element of G st I = {1,2} & x = <*a,(1_ G)*> holds

Product x = a

proof end;

theorem :: GROUP_21:42

for G being Group

for I1, I2 being non empty set

for F1 being DirectSumComponents of G,I1

for F2 being Group-Family of I2 st I1 misses I2 & ( for i being Element of I2 holds card (F2 . i) = 1 ) holds

F1 +* F2 is DirectSumComponents of G,I1 \/ I2

for I1, I2 being non empty set

for F1 being DirectSumComponents of G,I1

for F2 being Group-Family of I2 st I1 misses I2 & ( for i being Element of I2 holds card (F2 . i) = 1 ) holds

F1 +* F2 is DirectSumComponents of G,I1 \/ I2

proof end;

theorem :: GROUP_21:43

for G being Group

for I1, I2 being non empty set

for F1 being internal DirectSumComponents of G,I1

for F2 being Subgroup-Family of I2,G st I1 misses I2 & F2 = I2 --> ((1). G) holds

F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2

for I1, I2 being non empty set

for F1 being internal DirectSumComponents of G,I1

for F2 being Subgroup-Family of I2,G st I1 misses I2 & F2 = I2 --> ((1). G) holds

F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2

proof end;