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

::

:: Received December 31, 2014

:: Copyright (c) 2014-2018 Association of Mizar Users

definition

let D be non empty set ;

let x be Element of D;

:: original: <*

redefine func <*x*> -> FinSequence of D;

coherence

<*x*> is FinSequence of D

end;
let x be Element of D;

:: original: <*

redefine func <*x*> -> FinSequence of D;

coherence

<*x*> is FinSequence of D

proof end;

definition
end;

registration

let G be Group;

existence

ex b_{1} being Subgroup of G st b_{1} is commutative ;

end;
cluster non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V160() for Subgroup of G;

correctness existence

ex b

proof end;

definition

let I be non empty set ;

let F be Group-Family of I;

let i be Element of I;

:: original: .

redefine func F . i -> Group;

coherence

F . i is Group by Th1;

end;
let F be Group-Family of I;

let i be Element of I;

:: original: .

redefine func F . i -> Group;

coherence

F . i is Group by Th1;

registration

let I be set ;

let F be Group-Family of I;

correctness

coherence

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

end;
let F be Group-Family of I;

correctness

coherence

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

proof end;

theorem Th2: :: GROUP_19:2

for I being set

for F being Function st I = dom F & ( for i being object st i in I holds

F . i is Group ) holds

F is Group-Family of I

for F being Function st I = dom F & ( for i being object st i in I holds

F . i is Group ) holds

F is Group-Family of I

proof end;

theorem Th3: :: GROUP_19:3

for I being set

for F being multMagma-Family of I

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

for F being multMagma-Family of I

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

proof end;

theorem Th4: :: GROUP_19:4

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)

for F being multMagma-Family of I

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

proof end;

theorem Th5: :: GROUP_19:5

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

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

proof end;

theorem Th6: :: GROUP_19:6

for G, H being Group

for I being Subgroup of H

for f being Homomorphism of G,I holds f is Homomorphism of G,H

for I being Subgroup of H

for f being Homomorphism of G,I holds f is Homomorphism of G,H

proof end;

definition

let I be set ;

let F be Group-Family of I;

let a be Function;

ex b_{1} being Subset of I st

for i being object holds

( i in b_{1} iff ex G being Group st

( G = F . i & a . i <> 1_ G & i in I ) )

for b_{1}, b_{2} being Subset of I st ( for i being object holds

( i in b_{1} iff ex G being Group st

( G = F . i & a . i <> 1_ G & i in I ) ) ) & ( for i being object holds

( i in b_{2} iff ex G being Group st

( G = F . i & a . i <> 1_ G & i in I ) ) ) holds

b_{1} = b_{2}

end;
let F be Group-Family of I;

let a be Function;

func support (a,F) -> Subset of I means :Def1: :: GROUP_19:def 1

for i being object holds

( i in it iff ex G being Group st

( G = F . i & a . i <> 1_ G & i in I ) );

existence for i being object holds

( i in it iff ex G being Group st

( G = F . i & a . i <> 1_ G & i in I ) );

ex b

for i being object holds

( i in b

( G = F . i & a . i <> 1_ G & i in I ) )

proof end;

uniqueness for b

( i in b

( G = F . i & a . i <> 1_ G & i in I ) ) ) & ( for i being object holds

( i in b

( G = F . i & a . i <> 1_ G & i in I ) ) ) holds

b

proof end;

:: deftheorem Def1 defines support GROUP_19:def 1 :

for I being set

for F being Group-Family of I

for a being Function

for b_{4} being Subset of I holds

( b_{4} = support (a,F) iff for i being object holds

( i in b_{4} iff ex G being Group st

( G = F . i & a . i <> 1_ G & i in I ) ) );

for I being set

for F being Group-Family of I

for a being Function

for b

( b

( i in b

( G = F . i & a . i <> 1_ G & i in I ) ) );

theorem Th7: :: GROUP_19:7

for I being set

for F being Group-Family of I

for a being Element of (sum F) ex J being finite Subset of I ex b being ManySortedSet of J st

( J = support (a,F) & a = (1_ (product F)) +* b & ( for j being object

for G being Group st j in I \ J & G = F . j holds

a . j = 1_ G ) & ( for j being object st j in J holds

a . j = b . j ) )

for F being Group-Family of I

for a being Element of (sum F) ex J being finite Subset of I ex b being ManySortedSet of J st

( J = support (a,F) & a = (1_ (product F)) +* b & ( for j being object

for G being Group st j in I \ J & G = F . j holds

a . j = 1_ G ) & ( for j being object st j in J holds

a . j = b . j ) )

proof end;

registration

let I be set ;

let F be Group-Family of I;

let a be Element of (sum F);

correctness

coherence

support (a,F) is finite ;

end;
let F be Group-Family of I;

let a be Element of (sum F);

correctness

coherence

support (a,F) is finite ;

proof end;

definition

let I be set ;

let G be Group;

let a be Function of I,G;

ex b_{1} being Subset of I st

for i being object holds

( i in b_{1} iff ( a . i <> 1_ G & i in I ) )

for b_{1}, b_{2} being Subset of I st ( for i being object holds

( i in b_{1} iff ( a . i <> 1_ G & i in I ) ) ) & ( for i being object holds

( i in b_{2} iff ( a . i <> 1_ G & i in I ) ) ) holds

b_{1} = b_{2}

end;
let G be Group;

let a be Function of I,G;

func support a -> Subset of I means :Def2: :: GROUP_19:def 2

for i being object holds

( i in it iff ( a . i <> 1_ G & i in I ) );

existence for i being object holds

( i in it iff ( a . i <> 1_ G & i in I ) );

ex b

for i being object holds

( i in b

proof end;

uniqueness for b

( i in b

( i in b

b

proof end;

:: deftheorem Def2 defines support GROUP_19:def 2 :

for I being set

for G being Group

for a being Function of I,G

for b_{4} being Subset of I holds

( b_{4} = support a iff for i being object holds

( i in b_{4} iff ( a . i <> 1_ G & i in I ) ) );

for I being set

for G being Group

for a being Function of I,G

for b

( b

( i in b

:: deftheorem Def3 defines finite-support GROUP_19:def 3 :

for I being set

for G being Group

for a being Function of I,G holds

( a is finite-support iff support a is finite );

for I being set

for G being Group

for a being Function of I,G holds

( a is finite-support iff support a is finite );

registration

let I be set ;

let G be Group;

existence

ex b_{1} being Function of I,G st b_{1} is finite-support ;

end;
let G be Group;

cluster Relation-like I -defined the carrier of G -valued Function-like total quasi_total finite-support for Function of ,;

correctness existence

ex b

proof end;

registration

let I be set ;

let G be Group;

let a be finite-support Function of I,G;

correctness

coherence

support a is finite ;

by Def3;

end;
let G be Group;

let a be finite-support Function of I,G;

correctness

coherence

support a is finite ;

by Def3;

definition

let I be set ;

let G be Group;

let a be finite-support Function of I,G;

correctness

coherence

Product (a | (support a)) is Element of G;

;

end;
let G be Group;

let a be finite-support Function of I,G;

correctness

coherence

Product (a | (support a)) is Element of G;

;

:: deftheorem defines Product GROUP_19:def 4 :

for I being set

for G being Group

for a being finite-support Function of I,G holds Product a = Product (a | (support a));

for I being set

for G being Group

for a being finite-support Function of I,G holds Product a = Product (a | (support a));

theorem Th8: :: GROUP_19:8

for I being set

for F being Group-Family of I

for a being Element of (product F) holds

( a in sum F iff support (a,F) is finite )

for F being Group-Family of I

for a being Element of (product F) holds

( a in sum F iff support (a,F) is finite )

proof end;

theorem Th9: :: GROUP_19:9

for I being set

for G being Group

for H being Group-Family of I

for x being Function of I,G

for y being Element of (product H) st x = y & ( for i being object st i in I holds

H . i is Subgroup of G ) holds

support x = support (y,H)

for G being Group

for H being Group-Family of I

for x being Function of I,G

for y being Element of (product H) st x = y & ( for i being object st i in I holds

H . i is Subgroup of G ) holds

support x = support (y,H)

proof end;

theorem Th10: :: GROUP_19:10

for I being set

for G being Group

for F being Group-Family of I

for a being object st a in sum F & ( for i being object st i in I holds

F . i is Subgroup of G ) holds

a is finite-support Function of I,G

for G being Group

for F being Group-Family of I

for a being object st a in sum F & ( for i being object st i in I holds

F . i is Subgroup of G ) holds

a is finite-support Function of I,G

proof end;

theorem Th12: :: GROUP_19:12

for I being non empty set

for G being Group

for a being Function of I,G st a = I --> (1_ G) holds

support a is empty

for G being Group

for a being Function of I,G st a = I --> (1_ G) holds

support a is empty

proof end;

theorem Th13: :: GROUP_19:13

for I being non empty set

for G being Group

for F being Group-Family of I st ( for i being Element of I holds F . i is Subgroup of G ) holds

1_ (product F) = I --> (1_ G)

for G being Group

for F being Group-Family of I st ( for i being Element of I holds F . i is Subgroup of G ) holds

1_ (product F) = I --> (1_ G)

proof end;

theorem :: GROUP_19:14

for I being non empty set

for F being Group-Family of I

for G being Group

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

F . i is Subgroup of G ) holds

x = 1_ (product F)

for F being Group-Family of I

for G being Group

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

F . i is Subgroup of G ) holds

x = 1_ (product F)

proof end;

theorem Th15: :: GROUP_19:15

for I being set

for G being Group

for x being finite-support Function of I,G st support x = {} holds

Product x = 1_ G

for G being Group

for x being finite-support Function of I,G st support x = {} holds

Product x = 1_ G

proof end;

theorem Th16: :: GROUP_19:16

for I being non empty set

for G being Group

for a being finite-support Function of I,G st a = I --> (1_ G) holds

Product a = 1_ G

for G being Group

for a being finite-support Function of I,G st a = I --> (1_ G) holds

Product a = 1_ G

proof end;

theorem Th17: :: GROUP_19:17

for I being non empty set

for F being Group-Family of I

for x being Element of (product F)

for i being Element of I

for g being Element of (F . i) st x = (1_ (product F)) +* (i,g) holds

support (x,F) c= {i}

for F being Group-Family of I

for x being Element of (product F)

for i being Element of I

for g being Element of (F . i) st x = (1_ (product F)) +* (i,g) holds

support (x,F) c= {i}

proof end;

theorem :: GROUP_19:18

for I being non empty set

for F being Group-Family of I

for x being Element of (product F)

for i being Element of I

for g being Element of (F . i) st x = (1_ (product F)) +* (i,g) & g <> 1_ (F . i) holds

support (x,F) = {i}

for F being Group-Family of I

for x being Element of (product F)

for i being Element of I

for g being Element of (F . i) st x = (1_ (product F)) +* (i,g) & g <> 1_ (F . i) holds

support (x,F) = {i}

proof end;

theorem Th19: :: GROUP_19:19

for I being non empty set

for G being Group

for i being Element of I

for g being Element of G

for a being Function of I,G st a = (I --> (1_ G)) +* (i,g) holds

support a c= {i}

for G being Group

for i being Element of I

for g being Element of G

for a being Function of I,G st a = (I --> (1_ G)) +* (i,g) holds

support a c= {i}

proof end;

theorem Th20: :: GROUP_19:20

for I being non empty set

for G being Group

for i being Element of I

for g being Element of G

for a being Function of I,G st a = (I --> (1_ G)) +* (i,g) & g <> 1_ G holds

support a = {i}

for G being Group

for i being Element of I

for g being Element of G

for a being Function of I,G st a = (I --> (1_ G)) +* (i,g) & g <> 1_ G holds

support a = {i}

proof end;

theorem Th21: :: GROUP_19:21

for I being non empty set

for G being Group

for a being finite-support Function of I,G

for i being Element of I

for g being Element of G st a = (I --> (1_ G)) +* (i,g) holds

Product a = g

for G being Group

for a being finite-support Function of I,G

for i being Element of I

for g being Element of G st a = (I --> (1_ G)) +* (i,g) holds

Product a = g

proof end;

theorem :: GROUP_19:22

for I being non empty set

for F being Group-Family of I

for x being Function

for i being Element of I

for g being Element of (F . i) st support (x,F) is finite holds

support ((x +* (i,g)),F) is finite

for F being Group-Family of I

for x being Function

for i being Element of I

for g being Element of (F . i) st support (x,F) is finite holds

support ((x +* (i,g)),F) is finite

proof end;

theorem Th23: :: GROUP_19:23

for I being non empty set

for G being Group

for a being Function of I,G

for i being Element of I

for g being Element of G st support a is finite holds

support (a +* (i,g)) is finite

for G being Group

for a being Function of I,G

for i being Element of I

for g being Element of G st support a is finite holds

support (a +* (i,g)) is finite

proof end;

theorem Th24: :: GROUP_19:24

for I being non empty set

for F being Group-Family of I

for x being Function

for i being Element of I

for g being Element of (F . i) st x in product F holds

x +* (i,g) in product F

for F being Group-Family of I

for x being Function

for i being Element of I

for g being Element of (F . i) st x in product F holds

x +* (i,g) in product F

proof end;

theorem Th25: :: GROUP_19:25

for I being non empty set

for F being Group-Family of I

for x being Function

for i being Element of I

for g being Element of (F . i) st x in sum F holds

x +* (i,g) in sum F

for F being Group-Family of I

for x being Function

for i being Element of I

for g being Element of (F . i) st x in sum F holds

x +* (i,g) in sum F

proof end;

theorem :: GROUP_19:26

for I being non empty set

for G being Group

for a being finite-support Function of I,G

for i being Element of I

for g being Element of G holds a +* (i,g) is finite-support Function of I,G

for G being Group

for a being finite-support Function of I,G

for i being Element of I

for g being Element of G holds a +* (i,g) is finite-support Function of I,G

proof end;

theorem Th27: :: GROUP_19:27

for I being non empty set

for F being Group-Family of I

for i being Element of I

for a, b being Function st dom a = I & b = a +* (i,(1_ (F . i))) holds

support (b,F) = (support (a,F)) \ {i}

for F being Group-Family of I

for i being Element of I

for a, b being Function st dom a = I & b = a +* (i,(1_ (F . i))) holds

support (b,F) = (support (a,F)) \ {i}

proof end;

theorem Th28: :: GROUP_19:28

for I being non empty set

for G being Group

for i being object

for a, b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds

support b = (support a) \ {i}

for G being Group

for i being object

for a, b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds

support b = (support a) \ {i}

proof end;

theorem :: GROUP_19:29

for I being non empty set

for F being Group-Family of I

for i being Element of I

for a being Element of (sum F)

for b being Function st i in support (a,F) & b = a +* (i,(1_ (F . i))) holds

card (support (b,F)) = (card (support (a,F))) - 1

for F being Group-Family of I

for i being Element of I

for a being Element of (sum F)

for b being Function st i in support (a,F) & b = a +* (i,(1_ (F . i))) holds

card (support (b,F)) = (card (support (a,F))) - 1

proof end;

theorem :: GROUP_19:30

for I being non empty set

for G being Group

for i being object

for a being finite-support Function of I,G

for b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds

card (support b) = (card (support a)) - 1

for G being Group

for i being object

for a being finite-support Function of I,G

for b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds

card (support b) = (card (support a)) - 1

proof end;

theorem :: GROUP_19:31

for I being non empty set

for F being Group-Family of I

for a, b being Element of (product F) st support (a,F) misses support (b,F) holds

a +* (b | (support (b,F))) = a * b

for F being Group-Family of I

for a, b being Element of (product F) st support (a,F) misses support (b,F) holds

a +* (b | (support (b,F))) = a * b

proof end;

theorem Th32: :: GROUP_19:32

for I being non empty set

for F being Group-Family of I

for a, b being Element of (product F) st support (a,F) misses support (b,F) holds

a * b = b * a

for F being Group-Family of I

for a, b being Element of (product F) st support (a,F) misses support (b,F) holds

a * b = b * a

proof end;

theorem Th33: :: GROUP_19:33

for I being non empty set

for F being Group-Family of I

for i being Element of I holds ProjGroup (F,i) is Subgroup of sum F

for F being Group-Family of I

for i being Element of I holds ProjGroup (F,i) is Subgroup of sum F

proof end;

theorem Th34: :: GROUP_19:34

for I being non empty set

for F, G being Group-Family of I

for x, y being Function st ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st y . i = hi . (x . i) ) holds

support (y,G) c= support (x,F)

for F, G being Group-Family of I

for x, y being Function st ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st y . i = hi . (x . i) ) holds

support (y,G) c= support (x,F)

proof end;

definition

let F, G be non-empty non empty Function;

let h be non empty Function;

assume A1: ( dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds

h . i is Function of (F . i),(G . i) ) ) ;

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

for x being Element of product F

for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & (b_{1} . x) . i = hi . (x . i) )

for b_{1}, b_{2} being Function of (product F),(product G) st ( for x being Element of product F

for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & (b_{1} . x) . i = hi . (x . i) ) ) & ( for x being Element of product F

for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & (b_{2} . x) . i = hi . (x . i) ) ) holds

b_{1} = b_{2}

end;
let h be non empty Function;

assume A1: ( dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds

h . i is Function of (F . i),(G . i) ) ) ;

func ProductMap (F,G,h) -> Function of (product F),(product G) means :Def5: :: GROUP_19:def 5

for x being Element of product F

for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & (it . x) . i = hi . (x . i) );

existence for x being Element of product F

for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & (it . x) . i = hi . (x . i) );

ex b

for x being Element of product F

for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & (b

proof end;

uniqueness for b

for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & (b

for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & (b

b

proof end;

:: deftheorem Def5 defines ProductMap GROUP_19:def 5 :

for F, G being non-empty non empty Function

for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds

h . i is Function of (F . i),(G . i) ) holds

for b_{4} being Function of (product F),(product G) holds

( b_{4} = ProductMap (F,G,h) iff for x being Element of product F

for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & (b_{4} . x) . i = hi . (x . i) ) );

for F, G being non-empty non empty Function

for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds

h . i is Function of (F . i),(G . i) ) holds

for b

( b

for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & (b

theorem Th35: :: GROUP_19:35

for F, G being non-empty non empty Function

for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

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

ProductMap (F,G,h) is onto

for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

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

ProductMap (F,G,h) is onto

proof end;

theorem Th36: :: GROUP_19:36

for F, G being non-empty non empty Function

for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & hi is one-to-one ) ) holds

ProductMap (F,G,h) is one-to-one

for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

( hi = h . i & hi is one-to-one ) ) holds

ProductMap (F,G,h) is one-to-one

proof end;

theorem Th37: :: GROUP_19:37

for F, G being non-empty non empty Function

for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

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

ProductMap (F,G,h) is bijective

for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds

ex hi being Function of (F . i),(G . i) st

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

ProductMap (F,G,h) is bijective

proof end;

theorem Th38: :: GROUP_19:38

for I being non empty set

for F, G being Group-Family of I

for h being non empty Function

for x being Element of (product F)

for y being Element of (product G) st I = dom h & y = (ProductMap ((Carrier F),(Carrier G),h)) . x & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st

( hi = h . i & y . i = hi . (x . i) )

for F, G being Group-Family of I

for h being non empty Function

for x being Element of (product F)

for y being Element of (product G) st I = dom h & y = (ProductMap ((Carrier F),(Carrier G),h)) . x & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st

( hi = h . i & y . i = hi . (x . i) )

proof end;

definition

let I be non empty set ;

let F, G be Group-Family of I;

let h be non empty Function;

assume A1: ( I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) ) ;

ProductMap ((Carrier F),(Carrier G),h) is Homomorphism of (product F),(product G)

end;
let F, G be Group-Family of I;

let h be non empty Function;

assume A1: ( I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) ) ;

func ProductMap (F,G,h) -> Homomorphism of (product F),(product G) equals :Def6: :: GROUP_19:def 6

ProductMap ((Carrier F),(Carrier G),h);

coherence ProductMap ((Carrier F),(Carrier G),h);

ProductMap ((Carrier F),(Carrier G),h) is Homomorphism of (product F),(product G)

proof end;

:: deftheorem Def6 defines ProductMap GROUP_19:def 6 :

for I being non empty set

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

ProductMap (F,G,h) = ProductMap ((Carrier F),(Carrier G),h);

for I being non empty set

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

ProductMap (F,G,h) = ProductMap ((Carrier F),(Carrier G),h);

theorem Th39: :: GROUP_19:39

for I being non empty set

for F, G being Group-Family of I

for h being non empty Function

for x being Element of (product F)

for y being Element of (product G) st I = dom h & y = (ProductMap (F,G,h)) . x & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st

( hi = h . i & y . i = hi . (x . i) )

for F, G being Group-Family of I

for h being non empty Function

for x being Element of (product F)

for y being Element of (product G) st I = dom h & y = (ProductMap (F,G,h)) . x & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st

( hi = h . i & y . i = hi . (x . i) )

proof end;

theorem Th40: :: GROUP_19:40

for I being non empty set

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st

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

ProductMap (F,G,h) is bijective

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st

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

ProductMap (F,G,h) is bijective

proof end;

definition

let I be non empty set ;

let F be Group-Family of I;

let i be Element of I;

:: original: ProjGroup

redefine func ProjGroup (F,i) -> strict Subgroup of sum F;

correctness

coherence

ProjGroup (F,i) is strict Subgroup of sum F;

by Th33;

end;
let F be Group-Family of I;

let i be Element of I;

:: original: ProjGroup

redefine func ProjGroup (F,i) -> strict Subgroup of sum F;

correctness

coherence

ProjGroup (F,i) is strict Subgroup of sum F;

by Th33;

definition

let I be non empty set ;

let F, G be Group-Family of I;

let h be non empty Function;

assume A1: ( I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) ) ;

coherence

(ProductMap (F,G,h)) | (sum F) is Homomorphism of (sum F),(sum G);

end;
let F, G be Group-Family of I;

let h be non empty Function;

assume A1: ( I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) ) ;

func SumMap (F,G,h) -> Homomorphism of (sum F),(sum G) equals :Def7: :: GROUP_19:def 7

(ProductMap (F,G,h)) | (sum F);

correctness (ProductMap (F,G,h)) | (sum F);

coherence

(ProductMap (F,G,h)) | (sum F) is Homomorphism of (sum F),(sum G);

proof end;

:: deftheorem Def7 defines SumMap GROUP_19:def 7 :

for I being non empty set

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

SumMap (F,G,h) = (ProductMap (F,G,h)) | (sum F);

for I being non empty set

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

SumMap (F,G,h) = (ProductMap (F,G,h)) | (sum F);

theorem :: GROUP_19:41

for I being non empty set

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st

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

SumMap (F,G,h) is bijective

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st

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

SumMap (F,G,h) is bijective

proof end;

theorem :: GROUP_19:42

for I being non empty set

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

for i being Element of I

for f being Element of (F . i)

for hi being Homomorphism of (F . i),(G . i) st hi = h . i holds

(SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f)

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

for i being Element of I

for f being Element of (F . i)

for hi being Homomorphism of (F . i),(G . i) st hi = h . i holds

(SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f)

proof end;

theorem Th43: :: GROUP_19:43

for I being non empty set

for G being Group

for i being object st i in I holds

ex F being Group-Family of I ex h being Homomorphism of (sum F),G st

( h is bijective & F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st

( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds

x . j = 1_ (F . j) ) & ( for j being object st j in J holds

x . j = a . j ) ) ) )

for G being Group

for i being object st i in I holds

ex F being Group-Family of I ex h being Homomorphism of (sum F),G st

( h is bijective & F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st

( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds

x . j = 1_ (F . j) ) & ( for j being object st j in J holds

x . j = a . j ) ) ) )

proof end;

definition

let I be non empty set ;

let G be Group;

ex b_{1} being Group-Family of I ex h being Homomorphism of (sum b_{1}),G st h is bijective

end;
let G be Group;

mode DirectSumComponents of G,I -> Group-Family of I means :Def8: :: GROUP_19:def 8

ex h being Homomorphism of (sum it),G st h is bijective ;

existence ex h being Homomorphism of (sum it),G st h is bijective ;

ex b

proof end;

:: deftheorem Def8 defines DirectSumComponents GROUP_19:def 8 :

for I being non empty set

for G being Group

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

( b_{3} is DirectSumComponents of G,I iff ex h being Homomorphism of (sum b_{3}),G st h is bijective );

for I being non empty set

for G being Group

for b

( b

:: deftheorem Def9 defines internal GROUP_19:def 9 :

for I being non empty set

for G being Group

for F being DirectSumComponents of G,I holds

( F is internal iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ex h being Homomorphism of (sum F),G st

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

h . x = Product x ) ) ) );

for I being non empty set

for G being Group

for F being DirectSumComponents of G,I holds

( F is internal iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ex h being Homomorphism of (sum F),G st

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

h . x = Product x ) ) ) );

registration

let I be non empty set ;

let G be Group;

ex b_{1} being DirectSumComponents of G,I st b_{1} is internal

end;
let G be Group;

cluster Relation-like I -defined Function-like non empty total V180() multMagma-yielding Group-like associative internal for DirectSumComponents of G,I;

existence ex b

proof end;

theorem Th44: :: GROUP_19:44

for G being Group

for A being non empty Subset of G st ( for x, y being Element of G st x in A & y in A holds

x * y = y * x ) holds

gr A is commutative

for A being non empty Subset of G st ( for x, y being Element of G st x in A & y in A holds

x * y = y * x ) holds

gr A is commutative

proof end;

theorem Th45: :: GROUP_19:45

for G being Group

for H being Subgroup of G

for a being FinSequence of G

for b being FinSequence of H st a = b holds

Product a = Product b

for H being Subgroup of G

for a being FinSequence of G

for b being FinSequence of H st a = b holds

Product a = Product b

proof end;

theorem Th46: :: GROUP_19:46

for G being Group

for h being Element of G

for F being FinSequence of G st ( for k being Nat st k in dom F holds

h * (F /. k) = (F /. k) * h ) holds

h * (Product F) = (Product F) * h

for h being Element of G

for F being FinSequence of G st ( for k being Nat st k in dom F holds

h * (F /. k) = (F /. k) * h ) holds

h * (Product F) = (Product F) * h

proof end;

theorem Th47: :: GROUP_19:47

for G being Group

for F, F1, F2 being FinSequence of G st len F = len F1 & len F = len F2 & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds

(F1 /. i) * (F2 /. j) = (F2 /. j) * (F1 /. i) ) & ( for k being Nat st k in dom F holds

F . k = (F1 /. k) * (F2 /. k) ) holds

Product F = (Product F1) * (Product F2)

for F, F1, F2 being FinSequence of G st len F = len F1 & len F = len F2 & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds

(F1 /. i) * (F2 /. j) = (F2 /. j) * (F1 /. i) ) & ( for k being Nat st k in dom F holds

F . k = (F1 /. k) * (F2 /. k) ) holds

Product F = (Product F1) * (Product F2)

proof end;

theorem Th48: :: GROUP_19:48

for G being Group

for a being FinSequence of G st ( for i being object st i in dom a holds

a . i = 1_ G ) holds

Product a = 1_ G

for a being FinSequence of G st ( for i being object st i in dom a holds

a . i = 1_ G ) holds

Product a = 1_ G

proof end;

theorem Th49: :: GROUP_19:49

for I being finite set

for G being Group

for a being b_{1} -defined the carrier of b_{2} -valued total Function st ( for i being object st i in I holds

a . i = 1_ G ) holds

Product a = 1_ G

for G being Group

for a being b

a . i = 1_ G ) holds

Product a = 1_ G

proof end;

theorem Th50: :: GROUP_19:50

for A being finite set

for B being non empty set

for f being b_{1} -defined b_{2} -valued total Function holds f * (canFS A) is FinSequence of B

for B being non empty set

for f being b

proof end;

theorem Th51: :: GROUP_19:51

for I being non empty set

for G being Group

for a being finite-support Function of I,G

for W being finite Subset of I st support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) holds

Product a = Product (a | W)

for G being Group

for a being finite-support Function of I,G

for W being finite Subset of I st support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) holds

Product a = Product (a | W)

proof end;

theorem :: GROUP_19:52

for I being non empty set

for G being Group

for a being finite-support Function of I,G

for W being finite Subset of I st support a c= W holds

ex aW being finite-support Function of W,G st

( aW = a | W & support a = support aW & Product a = Product aW )

for G being Group

for a being finite-support Function of I,G

for W being finite Subset of I st support a c= W holds

ex aW being finite-support Function of W,G st

( aW = a | W & support a = support aW & Product a = Product aW )

proof end;

theorem Th53: :: GROUP_19:53

for I being non empty set

for G being Group

for F being Group-Family of I

for sx, sy being Element of (sum F)

for x, y, xy being finite-support Function of I,G st ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I

for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds

gi * gj = gj * gi ) & sx = x & sy = y & sx * sy = xy holds

Product xy = (Product x) * (Product y)

for G being Group

for F being Group-Family of I

for sx, sy being Element of (sum F)

for x, y, xy being finite-support Function of I,G st ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I

for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds

gi * gj = gj * gi ) & sx = x & sy = y & sx * sy = xy holds

Product xy = (Product x) * (Product y)

proof end;

theorem :: GROUP_19:54

for I being non empty set

for G being Group

for F being Group-Family of I holds

( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I

for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds

gi * gj = gj * gi ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds

x1 = x2 ) ) )

for G being Group

for F being Group-Family of I holds

( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I

for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds

gi * gj = gj * gi ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds

x1 = x2 ) ) )

proof end;