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

::

:: Received February 26, 2015

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

definition

let I be set ;

let G be Group;

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

for i being object st i in I holds

b_{1} . i is Subgroup of G

end;
let G be Group;

mode Subgroup-Family of I,G -> Group-Family of I means :Def1: :: GROUP_20:def 1

for i being object st i in I holds

it . i is Subgroup of G;

existence for i being object st i in I holds

it . i is Subgroup of G;

ex b

for i being object st i in I holds

b

proof end;

:: deftheorem Def1 defines Subgroup-Family GROUP_20:def 1 :

for I being set

for G being Group

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

( b_{3} is Subgroup-Family of I,G iff for i being object st i in I holds

b_{3} . i is Subgroup of G );

for I being set

for G being Group

for b

( b

b

:: deftheorem Def2 defines component-commutative GROUP_20:def 2 :

for I being set

for G being Group

for F being Subgroup-Family of I,G holds

( F is component-commutative iff 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 I being set

for G being Group

for F being Subgroup-Family of I,G holds

( F is component-commutative iff 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 );

registration

let I be non empty set ;

let G be Group;

ex b_{1} being Subgroup-Family of I,G st b_{1} is component-commutative

end;
let G be Group;

cluster Relation-like I -defined Function-like total V180() V235() Group-like associative component-commutative for Subgroup-Family of I,G;

existence ex b

proof end;

theorem Th1: :: GROUP_20:1

for G being Group

for H being normal Subgroup of G

for x, y being Element of G st y in H holds

( (x * y) * (x ") in H & x * (y * (x ")) in H )

for H being normal Subgroup of G

for x, y being Element of G st y in H holds

( (x * y) * (x ") in H & x * (y * (x ")) in H )

proof end;

theorem Th2: :: GROUP_20:2

for I being non empty set

for G being Group

for F being Group-Family of I

for x being Function of I,G st x in product F holds

x is Function of I,(Union (Carrier F))

for G being Group

for F being Group-Family of I

for x being Function of I,G st x in product F holds

x is Function of I,(Union (Carrier F))

proof end;

theorem Th3: :: GROUP_20:3

for I being non empty set

for G being Group

for H being Subgroup of G

for x being Function of I,G

for y being Function of I,H st x = y holds

support x = support y

for G being Group

for H being Subgroup of G

for x being Function of I,G

for y being Function of I,H st x = y holds

support x = support y

proof end;

theorem Th4: :: GROUP_20:4

for I being non empty set

for G being Group

for H being Subgroup of G

for y being finite-support Function of I,H holds y is finite-support Function of I,G

for G being Group

for H being Subgroup of G

for y being finite-support Function of I,H holds y is finite-support Function of I,G

proof end;

theorem Th5: :: GROUP_20:5

for I being non empty set

for G being Group

for H being Subgroup of G

for x being finite-support Function of I,G st rng x c= [#] H holds

x is finite-support Function of I,H

for G being Group

for H being Subgroup of G

for x being finite-support Function of I,G st rng x c= [#] H holds

x is finite-support Function of I,H

proof end;

theorem Th6: :: GROUP_20:6

for I being non empty set

for G being Group

for H being Subgroup of G

for x being finite-support Function of I,G

for y being finite-support Function of I,H st x = y holds

Product x = Product y

for G being Group

for H being Subgroup of G

for x being finite-support Function of I,G

for y being finite-support Function of I,H st x = y holds

Product x = Product y

proof end;

theorem Th8: :: GROUP_20:8

for I being non empty set

for G being Group

for F being component-commutative Subgroup-Family of I,G

for x, y being finite-support Function of I,G

for i being Element of I st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

for G being Group

for F being component-commutative Subgroup-Family of I,G

for x, y being finite-support Function of I,G

for i being Element of I st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

proof end;

theorem Th9: :: GROUP_20:9

for I being non empty set

for G being Group

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G

for i being Element of I

for x, y being finite-support Function of I,(gr UF) st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

for G being Group

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G

for i being Element of I

for x, y being finite-support Function of I,(gr UF) st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

proof end;

theorem Th10: :: GROUP_20:10

for I being non empty set

for G being Group

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G

for y being finite-support Function of I,(gr UF)

for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

for G being Group

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G

for y being finite-support Function of I,(gr UF)

for i being Element of I

for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds

(Product y) * g = g * (Product y)

proof end;

theorem Th11: :: GROUP_20:11

for I being non empty set

for G being Group

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G st UF = Union (Carrier F) holds

for g being Element of G

for H being FinSequence of G

for K being FinSequence of INT st len H = len K & rng H c= UF & Product (H |^ K) = g holds

ex f being finite-support Function of I,G st

( f in product F & g = Product f )

for G being Group

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G st UF = Union (Carrier F) holds

for g being Element of G

for H being FinSequence of G

for K being FinSequence of INT st len H = len K & rng H c= UF & Product (H |^ K) = g holds

ex f being finite-support Function of I,G st

( f in product F & g = Product f )

proof end;

theorem Th12: :: GROUP_20:12

for I being non empty set

for G being Group

for F being Subgroup-Family of I,G

for h, h0 being finite-support Function of I,G

for i being Element of I

for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

for G being Group

for F being Subgroup-Family of I,G

for h, h0 being finite-support Function of I,G

for i being Element of I

for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds

Product h0 in gr UFi

proof end;

theorem Th13: :: GROUP_20:13

for I being non empty set

for G being Group

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G st UF = Union (Carrier F) holds

for g being Element of G st g in gr UF holds

ex f being finite-support Function of I,(gr UF) st

( f in sum F & g = Product f )

for G being Group

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G st UF = Union (Carrier F) holds

for g being Element of G st g in gr UF holds

ex f being finite-support Function of I,(gr UF) st

( f in sum F & g = Product f )

proof end;

theorem Th14: :: GROUP_20:14

for I being non empty set

for G being Group

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G st UF = Union (Carrier F) holds

for i being Element of I holds F . i is normal Subgroup of gr UF

for G being Group

for F being component-commutative Subgroup-Family of I,G

for UF being Subset of G st UF = Union (Carrier F) holds

for i being Element of I holds F . i is normal Subgroup of gr UF

proof end;

theorem Th15: :: GROUP_20:15

for I being non empty set

for G being Group

for F being component-commutative Subgroup-Family of I,G st ( for i being Element of I ex UFi being Subset of G st

( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) holds

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 component-commutative Subgroup-Family of I,G st ( for i being Element of I ex UFi being Subset of G st

( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) holds

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;

theorem :: GROUP_20:16

for I being non empty set

for G being strict 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 normal Subgroup of G ) & ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( for i being Element of I ex UFi being Subset of G st

( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) ) )

for G being strict 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 normal Subgroup of G ) & ex UF being Subset of G st

( UF = Union (Carrier F) & gr UF = G ) & ( for i being Element of I ex UFi being Subset of G st

( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) ) )

proof end;

theorem :: GROUP_20:17

for I being non empty set

for G being commutative 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 st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( 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 commutative 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 st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( 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;

theorem Th19: :: GROUP_20:18

for I being non empty set

for G being Group

for F being Subgroup-Family of I,G

for h being Homomorphism of (sum F),G

for a being finite-support Function of I,G st a in sum F & ( for i being Element of I

for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds

h . a = Product a

for G being Group

for F being Subgroup-Family of I,G

for h being Homomorphism of (sum F),G

for a being finite-support Function of I,G st a in sum F & ( for i being Element of I

for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds

h . a = Product a

proof end;

theorem :: GROUP_20:19

for I being non empty set

for G being Group

for M being DirectSumComponents of G,I ex f being Homomorphism of (sum M),G ex N being internal DirectSumComponents of G,I st

( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st

( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )

for G being Group

for M being DirectSumComponents of G,I ex f being Homomorphism of (sum M),G ex N being internal DirectSumComponents of G,I st

( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st

( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )

proof end;