:: Internal Direct Products and the Universal Property of Direct Product Groups
:: by Alexander M. Nelson
::
:: Received June 30, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

theorem LmEqRng: :: GROUP_23:1

for X, Y, Z, W being set st Z <> {} & W <> {} holds
for f being Function of [:X,Y:],Z
for g being Function of [:X,Y:],W st ( for a being Element of X
for b being Element of Y holds f . (a,b) = g . (a,b) ) holds
f = g

proof end;

ThCoim: for f being Function
for X being non empty set
for x, x0 being Element of X holds
( f . x = f . x0 iff x in { x1 where x1 is Element of X : f . x0 = f . x1 } )

proof end;

theorem ThCanFSIsMss: :: GROUP_23:2

for A being finite set holds canFS A is ManySortedSet of Seg (card A)

proof end;

theorem :: GROUP_23:3

for X, Y being non empty set
for f being Function of X,Y st f is onto holds
ex g being Function of Y,X st f * g = id Y

proof end;

:: This probably belongs in PBOOLE

definition

let I be non empty set ;
let A, B be ManySortedSet of I;
let f be ManySortedFunction of A,B;
let i be Element of I;
:: original: .
redefine func f . i -> Function of (A . i),(B . i);
coherence
f . i is Function of (A . i),(B . i) by PBOOLE:def 15;

end;

:: This probably belongs in PRALG_1

definition

let I be non empty set ;
let F1, F2 be 1-sorted-yielding ManySortedSet of I;
mode ManySortedFunction of F1,F2 is ManySortedFunction of Carrier F1, Carrier F2;

end;

:: This probably belongs in PRALG_1

definition

let I be non empty set ;
let F1, F2 be 1-sorted-yielding ManySortedSet of I;
let phi be ManySortedFunction of F1,F2;
let i be Element of I;
:: original: .
redefine func phi . i -> Function of (F1 . i),(F2 . i);
correctness
coherence
phi . i is Function of (F1 . i),(F2 . i);

proof end;

end;

theorem Th25: :: GROUP_23:4

for I being non empty set
for A, B, f being ManySortedSet of I holds
( f is ManySortedFunction of A,B iff for i being Element of I holds f . i is Function of (A . i),(B . i) )

proof end;

registration

let I, X be set ;

cluster Relation-like I -defined bool X -valued Function-like total for set ;

existence
ex b₁ being ManySortedSet of I st b₁ is bool X -valued

proof end;

end;

definition

let I, X be set ;
let M be bool X -valued ManySortedSet of I;
:: original: Union
redefine func Union M -> Subset of X;
correctness
coherence
Union M is Subset of X;

proof end;

end;

registration

let I be set ;
let J be Subset of I;
let F be ManySortedSet of I;

cluster F | J -> J -defined total ;

coherence
( F | J is J -defined & F | J is total )

proof end;

end;

registration

let I be set ;
let J be Subset of I;
let F be 1-sorted-yielding ManySortedSet of I;

cluster F | J -> J -defined total 1-sorted-yielding ;

coherence
( F | J is 1-sorted-yielding & F | J is J -defined & F | J is total )

proof end;

end;

theorem MssRng: :: GROUP_23:5

for I being non empty set
for M being ManySortedSet of I
for y being object holds
( y in rng M iff ex i being Element of I st y = M . i )

proof end;

theorem ThMappingFrobProdProperty: :: GROUP_23:6

for G1, G2 being Group
for phi being Homomorphism of G1,G2
for F1 being FinSequence of the carrier of G1
for F2 being FinSequence of the carrier of G2 st F2 = phi * F1 holds
Product F2 = phi . (Product F1)

proof end;

theorem ThMappingFrobProd: :: GROUP_23:7

for G1, G2 being Group
for phi being Homomorphism of G1,G2
for F1 being FinSequence of the carrier of G1 ex F2 being FinSequence of the carrier of G2 st
( len F1 = len F2 & F2 = phi * F1 & Product F2 = phi . (Product F1) )

proof end;

theorem ThMappingFrobProd2: :: GROUP_23:8

for G1, G2 being Group
for phi being Homomorphism of G1,G2
for F1 being FinSequence of the carrier of G1
for ks being FinSequence of INT ex F2 being FinSequence of the carrier of G2 st
( len F1 = len F2 & F2 = phi * F1 & Product (F2 |^ ks) = phi . (Product (F1 |^ ks)) )

proof end;

definition

let IT be Relation;

attr IT is Group-yielding means :Def1: :: GROUP_23:def 1
for G being object st G in rng IT holds
G is Group;

end;

:: deftheorem Def1 defines Group-yielding GROUP_23:def 1 :
for IT being Relation holds
( IT is Group-yielding iff for G being object st G in rng IT holds
G is Group );

registration

cluster Relation-like Function-like Group-yielding -> 1-sorted-yielding for set ;

coherence
for b₁ being Function st b₁ is Group-yielding holds
b₁ is 1-sorted-yielding

proof end;

cluster Relation-like Function-like Group-yielding -> multMagma-yielding for set ;

coherence
for b₁ being Function st b₁ is Group-yielding holds
b₁ is multMagma-yielding

proof end;

end;

theorem Th4: :: GROUP_23:9

for I being set
for F being Group-like associative multMagma-Family of I holds F is Group-yielding

proof end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total Group-yielding for set ;

existence
ex b₁ being ManySortedSet of I st b₁ is Group-yielding

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total multMagma-yielding Group-like associative -> Group-yielding for set ;

coherence
for b₁ being multMagma-Family of I st b₁ is associative & b₁ is Group-like holds
b₁ is Group-yielding by Th4;

end;

registration

cluster Relation-like Function-like Group-yielding for set ;

existence
ex b₁ being Function st b₁ is Group-yielding

proof end;

end;

theorem Th5: :: GROUP_23:10

for I being non empty set
for F being Group-yielding ManySortedSet of I
for i being Element of I holds F . i is Group

proof end;

registration

let I be non empty set ;
let i be Element of I;
let F be Group-yielding ManySortedSet of I;

cluster F . i -> non empty unital Group-like associative for multMagma ;

correctness
coherence
for b₁ being multMagma st b₁ = F . i holds
( b₁ is Group-like & b₁ is associative & b₁ is unital & not b₁ is empty );
by Th5;

end;

theorem :: GROUP_23:11

for I being set
for F being ManySortedSet of I holds
( F is Group-yielding iff for i being object st i in I holds
F . i is Group )

proof end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total multMagma-yielding Group-yielding -> Group-like associative for set ;

correctness
coherence
for b₁ being multMagma-Family of I st b₁ is Group-yielding holds
( b₁ is Group-like & b₁ is associative );

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total multMagma-yielding Group-like associative -> Group-like associative Group-yielding for set ;

coherence
for b₁ being Group-like associative multMagma-Family of I holds b₁ is Group-yielding ;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total Group-yielding -> multMagma-yielding Group-like associative Group-yielding for set ;

coherence
for b₁ being Group-yielding ManySortedSet of I holds
( b₁ is Group-like & b₁ is associative & b₁ is multMagma-yielding ) ;

end;

theorem :: GROUP_23:12

for G being Group holds {} --> G is Group-Family of {} ;

theorem :: GROUP_23:13

for G being Group
for n being Nat holds (Seg n) --> G is Group-Family of Seg n ;

registration

let G be Group;
let n be Nat;

cluster (Seg n) --> G -> Group-yielding ;

correctness
coherence
(Seg n) --> G is Group-yielding ;
;

end;

theorem Th9: :: GROUP_23:14

for I being non empty set
for i being Element of I
for F being Group-Family of I holds (Carrier F) . i = the carrier of (F . i)

proof end;

scheme :: GROUP_23:sch 1
GrFamSch{ F₁() -> non empty set , F₂( Element of F₁()) -> Group } :

ex Fam being Group-Family of F₁() st
for i being Element of F₁() holds Fam . i = F₂(i)

proof end;

definition

let I be set ;
let F, IT be Group-Family of I;

attr IT is F -Subgroup-yielding means :Def2: :: GROUP_23:def 2
for i being Element of I
for G being Group st G = F . i holds
IT . i is Subgroup of G;

end;

:: deftheorem Def2 defines -Subgroup-yielding GROUP_23:def 2 :
for I being set
for F, IT being Group-Family of I holds
( IT is F -Subgroup-yielding iff for i being Element of I
for G being Group st G = F . i holds
IT . i is Subgroup of G );

theorem :: GROUP_23:15

for I being non empty set
for F, S being Group-Family of I holds
( S is F -Subgroup-yielding iff for i being Element of I holds S . i is Subgroup of F . i ) ;

theorem ThSubYieldRefl: :: GROUP_23:16

for I being set
for F being Group-Family of I holds F is F -Subgroup-yielding by GROUP_2:54;

registration

let I be set ;
let F be Group-Family of I;

cluster Relation-like I -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative Group-yielding F -Subgroup-yielding for set ;

existence
ex b₁ being Group-Family of I st b₁ is F -Subgroup-yielding by ThSubYieldRefl;

end;

definition

let I be set ;
let F be Group-Family of I;
mode Subgroup-Family of F is F -Subgroup-yielding Group-Family of I;

end;

definition

let I be non empty set ;
let F be Group-Family of I;
let S be Subgroup-Family of F;
let i be Element of I;
:: original: .
redefine func S . i -> Subgroup of F . i;
correctness
coherence
S . i is Subgroup of F . i;
by Def2;

end;

theorem :: GROUP_23:17

for I being non empty set
for F, S being Group-Family of I holds
( S is Subgroup-Family of F iff for i being Element of I holds S . i is Subgroup of F . i )

proof end;

scheme :: GROUP_23:sch 2
SubFamSch{ F₁() -> non empty set , F₂() -> Group-Family of F₁(), F₃( Group) -> Group } :

ex S being Subgroup-Family of F₂() st
for i being Element of F₁() holds S . i = F₃((F₂() . i))

provided

A1: for G being Group holds F₃(G) is Subgroup of G

proof end;

:: Re-defining "strict" for Subgroup-Family seemed like a risky move,
:: so I opted to introduce an adjective which captured what was needed.

definition

let I be non empty set ;
let IT be Group-Family of I;

attr IT is componentwise_strict means :Def3: :: GROUP_23:def 3
for i being Element of I holds IT . i is strict ;

end;

:: deftheorem Def3 defines componentwise_strict GROUP_23:def 3 :
for I being non empty set
for IT being Group-Family of I holds
( IT is componentwise_strict iff for i being Element of I holds IT . i is strict );

registration

let I be non empty set ;

cluster Relation-like I -defined Function-like non empty total 1-sorted-yielding multMagma-yielding Group-like associative Group-yielding componentwise_strict for set ;

existence
ex b₁ being Group-Family of I st b₁ is componentwise_strict

proof end;

end;

theorem Def4: :: GROUP_23:18

for I being non empty set
for F being Group-Family of I
for IT being Subgroup-Family of F holds
( IT is componentwise_strict iff for i being Element of I holds IT . i is strict Subgroup of F . i ) ;

registration

let I be non empty set ;
let F be Group-Family of I;

cluster Relation-like I -defined Function-like non empty total 1-sorted-yielding multMagma-yielding Group-like associative Group-yielding F -Subgroup-yielding componentwise_strict for set ;

existence
ex b₁ being Subgroup-Family of F st b₁ is componentwise_strict

proof end;

end;

registration

let I be non empty set ;
let F be Group-Family of I;
let S be componentwise_strict Subgroup-Family of F;
let i be Element of I;

cluster S . i -> strict for Subgroup of F . i;

correctness
coherence
for b₁ being Subgroup of F . i st b₁ = S . i holds
b₁ is strict ;
by Def3;

end;

scheme :: GROUP_23:sch 3
StrSubFamSch{ F₁() -> non empty set , F₂() -> Group-Family of F₁(), F₃( Group) -> Group } :

ex S being componentwise_strict Subgroup-Family of F₂() st
for i being Element of F₁() holds S . i = F₃((F₂() . i))

provided

A1: for G being Group holds F₃(G) is strict Subgroup of G

proof end;

theorem ThStrSubEq: :: GROUP_23:19

for I being non empty set
for F being Group-Family of I
for A, B being Subgroup-Family of F st ( for i being Element of I holds A . i = B . i ) holds
A = B

proof end;

definition

let I be non empty set ;
let F be Group-Family of I;

func (1). F -> componentwise_strict Subgroup-Family of F means :Def5: :: GROUP_23:def 4
for i being Element of I holds it . i = (1). (F . i);

existence
ex b₁ being componentwise_strict Subgroup-Family of F st
for i being Element of I holds b₁ . i = (1). (F . i)

proof end;

uniqueness
for b₁, b₂ being componentwise_strict Subgroup-Family of F st ( for i being Element of I holds b₁ . i = (1). (F . i) ) & ( for i being Element of I holds b₂ . i = (1). (F . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines (1). GROUP_23:def 4 :
for I being non empty set
for F being Group-Family of I
for b₃ being componentwise_strict Subgroup-Family of F holds
( b₃ = (1). F iff for i being Element of I holds b₃ . i = (1). (F . i) );

definition

let I be non empty set ;
let F be Group-Family of I;

func (Omega). F -> componentwise_strict Subgroup-Family of F means :Def6: :: GROUP_23:def 5
for i being Element of I holds it . i = (Omega). (F . i);

existence
ex b₁ being componentwise_strict Subgroup-Family of F st
for i being Element of I holds b₁ . i = (Omega). (F . i)

proof end;

uniqueness
for b₁, b₂ being componentwise_strict Subgroup-Family of F st ( for i being Element of I holds b₁ . i = (Omega). (F . i) ) & ( for i being Element of I holds b₂ . i = (Omega). (F . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines (Omega). GROUP_23:def 5 :
for I being non empty set
for F being Group-Family of I
for b₃ being componentwise_strict Subgroup-Family of F holds
( b₃ = (Omega). F iff for i being Element of I holds b₃ . i = (Omega). (F . i) );

definition

let I be non empty set ;
let F be Group-Family of I;
let IT be Subgroup-Family of F;

attr IT is normal means :Def7: :: GROUP_23:def 6
for i being Element of I holds IT . i is normal Subgroup of F . i;

end;

:: deftheorem Def7 defines normal GROUP_23:def 6 :
for I being non empty set
for F being Group-Family of I
for IT being Subgroup-Family of F holds
( IT is normal iff for i being Element of I holds IT . i is normal Subgroup of F . i );

registration

let I be non empty set ;
let F be Group-Family of I;

cluster Relation-like I -defined Function-like non empty total 1-sorted-yielding multMagma-yielding Group-like associative Group-yielding F -Subgroup-yielding componentwise_strict normal for set ;

existence
ex b₁ being Subgroup-Family of F st
( b₁ is componentwise_strict & b₁ is normal )

proof end;

end;

registration

let I be non empty set ;
let F be Group-Family of I;
let S be normal Subgroup-Family of F;
let i be Element of I;

cluster S . i -> normal for Subgroup of F . i;

correctness
coherence
for b₁ being Subgroup of F . i st b₁ = S . i holds
b₁ is normal ;
by Def7;

end;

registration

let I be non empty set ;
let F be Group-Family of I;
let S be componentwise_strict Subgroup-Family of F;
let i be Element of I;

cluster S . i -> strict for Subgroup of F . i;

correctness
coherence
for b₁ being Subgroup of F . i st b₁ = S . i holds
b₁ is strict ;
;

end;

registration

let I be non empty set ;
let F be Group-Family of I;

cluster (1). F -> componentwise_strict normal ;

correctness
coherence
(1). F is normal ;

proof end;

cluster (Omega). F -> componentwise_strict normal ;

correctness
coherence
(Omega). F is normal ;

proof end;

end;

definition

let I be non empty set ;
let F be Group-Family of I;
let N be normal Subgroup-Family of F;

func F ./. N -> Group-Family of I means :Def8: :: GROUP_23:def 7
for i being Element of I holds it . i = (F . i) ./. (N . i);

existence
ex b₁ being Group-Family of I st
for i being Element of I holds b₁ . i = (F . i) ./. (N . i)

proof end;

uniqueness
for b₁, b₂ being Group-Family of I st ( for i being Element of I holds b₁ . i = (F . i) ./. (N . i) ) & ( for i being Element of I holds b₂ . i = (F . i) ./. (N . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines ./. GROUP_23:def 7 :
for I being non empty set
for F being Group-Family of I
for N being normal Subgroup-Family of F
for b₄ being Group-Family of I holds
( b₄ = F ./. N iff for i being Element of I holds b₄ . i = (F . i) ./. (N . i) );

registration

let I be non empty set ;
let F be Group-Family of I;
let N be normal Subgroup-Family of F;

cluster F ./. N -> componentwise_strict ;

correctness
coherence
F ./. N is componentwise_strict ;

proof end;

end;

theorem :: GROUP_23:20

for I being non empty set
for F being Group-Family of I ex S being componentwise_strict normal Subgroup-Family of F st
for i being Element of I holds S . i = (F . i) `

proof end;

theorem LmTriv: :: GROUP_23:21

for M being strict multMagma st ex x being object st the carrier of M = {x} holds
ex G being trivial strict Group st M = G

proof end;

theorem :: GROUP_23:22

for I being empty set
for F being multMagma-Family of I holds product F is trivial Group

proof end;

definition

let G, H be Group;
assume A1: H is Subgroup of G ;

func incl (H,G) -> Homomorphism of H,G equals :Def9: :: GROUP_23:def 8
id the carrier of H;

coherence
id the carrier of H is Homomorphism of H,G

proof end;

end;

:: deftheorem Def9 defines incl GROUP_23:def 8 :
for G, H being Group st H is Subgroup of G holds
incl (H,G) = id the carrier of H;

definition

let G be Group;
let H be Subgroup of G;

func incl H -> Homomorphism of H,G equals :: GROUP_23:def 9
incl (H,G);

coherence
incl (H,G) is Homomorphism of H,G ;

end;

:: deftheorem defines incl GROUP_23:def 9 :
for G being Group
for H being Subgroup of G holds incl H = incl (H,G);

theorem Th18: :: GROUP_23:23

for G, H being Group
for h being Element of H st H is Subgroup of G holds
(incl (H,G)) . h = h

proof end;

theorem Th19: :: GROUP_23:24

for G being Group
for H being Subgroup of G holds
( incl (H,G) is one-to-one & Image (incl (H,G)) = multMagma(# the carrier of H, the multF of H #) )

proof end;

registration

let G be Group;
let H be Subgroup of G;

cluster incl (H,G) -> one-to-one ;

correctness
coherence
incl (H,G) is one-to-one ;
by Th19;

end;

theorem :: GROUP_23:25

for G, H, K being Group st H is Subgroup of G holds
for phi being Homomorphism of G,K holds phi | the carrier of H = phi * (incl (H,G))

proof end;

theorem :: GROUP_23:26

for G, K being Group
for H being Subgroup of G
for phi being Homomorphism of G,K holds phi | H = phi * (incl H)

proof end;

theorem :: GROUP_23:27

for G being Group
for H being strict Subgroup of G holds Image (incl H) = H

proof end;

definition

let G be Group;
let I be non empty set ;
let F be Group-Family of I;

mode Homomorphism-Family of G,F -> ManySortedFunction of I means :Def10: :: GROUP_23:def 10
for i being Element of I holds it . i is Homomorphism of G,(F . i);

existence
ex b₁ being ManySortedFunction of I st
for i being Element of I holds b₁ . i is Homomorphism of G,(F . i)

proof end;

end;

:: deftheorem Def10 defines Homomorphism-Family GROUP_23:def 10 :
for G being Group
for I being non empty set
for F being Group-Family of I
for b₄ being ManySortedFunction of I holds
( b₄ is Homomorphism-Family of G,F iff for i being Element of I holds b₄ . i is Homomorphism of G,(F . i) );

:: I hate this, but have no better alternative

definition

let G be Group;
let I be non empty set ;
let F be Group-Family of I;
let f be Homomorphism-Family of G,F;
let i be Element of I;
:: original: .
redefine func f . i -> Homomorphism of G,(F . i);
coherence
f . i is Homomorphism of G,(F . i) by Def10;

end;

theorem :: GROUP_23:28

for I being non empty set
for i being Element of I
for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F holds [i,(f . i)] in f

proof end;

definition

let I be non empty set ;
let F1, F2 be Group-Family of I;

mode Homomorphism-Family of F1,F2 -> ManySortedFunction of F1,F2 means :Def11: :: GROUP_23:def 11
for i being Element of I holds it . i is Homomorphism of (F1 . i),(F2 . i);

existence
ex b₁ being ManySortedFunction of F1,F2 st
for i being Element of I holds b₁ . i is Homomorphism of (F1 . i),(F2 . i)

proof end;

end;

:: deftheorem Def11 defines Homomorphism-Family GROUP_23:def 11 :
for I being non empty set
for F1, F2 being Group-Family of I
for b₄ being ManySortedFunction of F1,F2 holds
( b₄ is Homomorphism-Family of F1,F2 iff for i being Element of I holds b₄ . i is Homomorphism of (F1 . i),(F2 . i) );

registration

let I be non empty set ;
let F1, F2 be Group-Family of I;
let i be Element of I;
let phi be Homomorphism-Family of F1,F2;

cluster phi . i -> multiplicative for Function of (F1 . i),(F2 . i);

correctness
coherence
for b₁ being Function of (F1 . i),(F2 . i) st b₁ = phi . i holds
b₁ is multiplicative ;
by Def11;

end;

theorem ThHom: :: GROUP_23:29

for I being non empty set
for A, B being Group-Family of I
for f being ManySortedSet of I holds
( f is Homomorphism-Family of A,B iff for i being Element of I holds f . i is Homomorphism of (A . i),(B . i) )

proof end;

scheme :: GROUP_23:sch 4
HomFamSch{ F₁() -> non empty set , F₂() -> Group-Family of F₁(), F₃() -> Group-Family of F₁(), F₄( Element of F₁()) -> Function } :

ex H being Homomorphism-Family of F₂(),F₃() st
for i being Element of F₁() holds H . i = F₄(i)

provided

A1: for i being Element of F₁() holds F₄(i) is Homomorphism of (F₂() . i),(F₃() . i)

proof end;

theorem ThRHom: :: GROUP_23:30

for G being Group
for I being non empty set
for F being Group-Family of I
for f being ManySortedSet of I holds
( f is Homomorphism-Family of G,F iff for i being Element of I holds f . i is Homomorphism of G,(F . i) )

proof end;

scheme :: GROUP_23:sch 5
RHomFamSch{ F₁() -> non empty set , F₂() -> Group, F₃() -> Group-Family of F₁(), F₄( Element of F₁()) -> Function } :

ex H being Homomorphism-Family of F₂(),F₃() st
for i being Element of F₁() holds H . i = F₄(i)

provided

A1: for i being Element of F₁() holds F₄(i) is Homomorphism of F₂(),(F₃() . i)

proof end;

theorem :: GROUP_23:31

for I being non empty set
for A, B being Group-Family of I
for f being ManySortedSet of I holds
( f is Homomorphism-Family of A,B iff for i being Element of I holds f . i is Homomorphism of (A . i),(B . i) )

proof end;

theorem Th29: :: GROUP_23:32

for I being non empty set
for i being Element of I
for F being Group-Family of I
for g being Element of (product F) holds g . i is Element of (F . i)

proof end;

definition

let I be non empty set ;
let F be Group-Family of I;
let g be Element of (product F);
let i be Element of I;

func g /. i -> Element of (F . i) equals :: GROUP_23:def 12
g . i;

correctness
coherence
g . i is Element of (F . i);
by Th29;

end;

:: deftheorem defines /. GROUP_23:def 12 :
for I being non empty set
for F being Group-Family of I
for g being Element of (product F)
for i being Element of I holds g /. i = g . i;

registration

let I be non empty set ;
let F be Group-Family of I;
let g be Element of (product F);
let i be Element of I;

identify g /. i with g . i;

correctness
compatibility
g /. i = g . i;
;

end;

definition

let I be non empty set ;
let i be Element of I;
let F be Group-Family of I;

func proj (F,i) -> Homomorphism of (product F),(F . i) means :Def13: :: GROUP_23:def 13
for h being Element of (product F) holds it . h = h . i;

existence
ex b₁ being Homomorphism of (product F),(F . i) st
for h being Element of (product F) holds b₁ . h = h . i

proof end;

uniqueness
for b₁, b₂ being Homomorphism of (product F),(F . i) st ( for h being Element of (product F) holds b₁ . h = h . i ) & ( for h being Element of (product F) holds b₂ . h = h . i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines proj GROUP_23:def 13 :
for I being non empty set
for i being Element of I
for F being Group-Family of I
for b₄ being Homomorphism of (product F),(F . i) holds
( b₄ = proj (F,i) iff for h being Element of (product F) holds b₄ . h = h . i );

theorem Th30: :: GROUP_23:33

for I being non empty set
for i being Element of I
for F being Group-Family of I holds proj (F,i) is onto

proof end;

registration

let I be non empty set ;
let F be Group-Family of I;
let i be Element of I;

cluster proj (F,i) -> onto ;

correctness
coherence
proj (F,i) is onto ;
by Th30;

end;

theorem Th31: :: GROUP_23:34

for I being non empty set
for i being Element of I
for F being Group-Family of I holds proj ((Carrier F),i) is Function of (product (Carrier F)), the carrier of (F . i)

proof end;

theorem Th32: :: GROUP_23:35

for I being non empty set
for i being Element of I
for F being Group-Family of I
for g being Element of (product F) holds (proj (F,i)) . g = (proj ((Carrier F),i)) . g

proof end;

theorem :: GROUP_23:36

for I being non empty set
for i being Element of I
for F being Group-Family of I holds proj (F,i) = proj ((Carrier F),i)

proof end;

theorem Th34: :: GROUP_23:37

for I being non empty set
for i being Element of I
for F being Group-Family of I
for g being Element of (product F)
for h being Element of (F . i) holds g +* (i,h) in product F

proof end;

theorem :: GROUP_23:38

for I being non empty set
for F being Group-Family of I
for i being Element of I
for g being Element of (product F) holds g +* (i,(1_ (F . i))) in Ker (proj (F,i))

proof end;

theorem InclByAnyOtherName: :: GROUP_23:39

for G1, G2 being Group
for f being Homomorphism of G1,G2 st ( for g being Element of G1 holds f . g = g ) holds
G1 is Subgroup of G2

proof end;

theorem Th37: :: GROUP_23:40

for I being non empty set
for F being Group-Family of I
for i, j being Element of I st i <> j holds
(proj (F,j)) * (1ProdHom (F,i)) = 1: ((F . i),(F . j))

proof end;

theorem Th38: :: GROUP_23:41

for I being non empty set
for i being Element of I
for F being Group-Family of I holds (proj (F,i)) * (1ProdHom (F,i)) = id the carrier of (F . i)

proof end;

:: Universal property of group product, explicit version.

theorem Th39: :: GROUP_23:42

for I being non empty set
for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F ex phi being Homomorphism of G,(product F) st
for g being Element of G
for j being Element of I holds (f . j) . g = (proj (F,j)) . (phi . g)

proof end;

:: Universal property of group product, as most people would recognize it.

theorem :: GROUP_23:43

for I being non empty set
for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F ex phi being Homomorphism of G,(product F) st
for i being Element of I holds f . i = (proj (F,i)) * phi

proof end;

theorem :: GROUP_23:44

for I being non empty set
for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F
for phi1, phi2 being Homomorphism of G,(product F) st ( for i being Element of I holds f . i = (proj (F,i)) * phi1 ) & ( for i being Element of I holds f . i = (proj (F,i)) * phi2 ) holds
phi1 = phi2

proof end;

definition

let G be Group;
let I be non empty set ;
let F be Group-Family of I;
let f be Homomorphism-Family of G,F;

func product f -> Homomorphism of G,(product F) means :Def14: :: GROUP_23:def 14
for g being Element of G
for i being Element of I holds (f . i) . g = (it . g) . i;

existence
ex b₁ being Homomorphism of G,(product F) st
for g being Element of G
for i being Element of I holds (f . i) . g = (b₁ . g) . i

proof end;

uniqueness
for b₁, b₂ being Homomorphism of G,(product F) st ( for g being Element of G
for i being Element of I holds (f . i) . g = (b₁ . g) . i ) & ( for g being Element of G
for i being Element of I holds (f . i) . g = (b₂ . g) . i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines product GROUP_23:def 14 :
for G being Group
for I being non empty set
for F being Group-Family of I
for f being Homomorphism-Family of G,F
for b₅ being Homomorphism of G,(product F) holds
( b₅ = product f iff for g being Element of G
for i being Element of I holds (f . i) . g = (b₅ . g) . i );

theorem Th42: :: GROUP_23:45

for I being non empty set
for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F
for g being Element of G holds
( ( for i being Element of I holds ((product f) . g) . i = 1_ (F . i) ) iff (product f) . g = 1_ (product F) )

proof end;

theorem Th43: :: GROUP_23:46

for I being non empty set
for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F
for g being Element of G holds
( g in Ker (product f) iff for i being Element of I holds g in Ker (f . i) )

proof end;

theorem Th44: :: GROUP_23:47

for G1, G2, G3 being Group
for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G2,G3
for g being Element of G1 holds
( g in Ker (f2 * f1) iff f1 . g in Ker f2 )

proof end;

theorem :: GROUP_23:48

for G1, G2, G3 being Group
for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G2,G3 holds the carrier of (Ker (f2 * f1)) = f1 " the carrier of (Ker f2)

proof end;

theorem :: GROUP_23:49

for I being non empty set
for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F holds the carrier of (Ker (product f)) = meet { the carrier of (Ker (f . i)) where i is Element of I : verum }

proof end;

theorem Th47: :: GROUP_23:50

for f being Function
for I being non empty set
for F being Group-Family of I st dom f = I & ( for i being Element of I holds f . i in F . i ) holds
f in product F

proof end;

theorem :: GROUP_23:51

for I being non empty set
for F, S being Group-Family of I
for g being Element of (product F) holds
( g in product S iff for i being Element of I holds (proj (F,i)) . g in S . i )

proof end;

theorem Th49: :: GROUP_23:52

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

proof end;

definition

let I be non empty set ;
let F be Group-Family of I;
let S be Subgroup-Family of F;

func product S -> strict Subgroup of product F equals :: GROUP_23:def 15
product S;

coherence
product S is strict Subgroup of product F

proof end;

end;

:: deftheorem defines product GROUP_23:def 15 :
for I being non empty set
for F being Group-Family of I
for S being Subgroup-Family of F holds product S = product S;

theorem Th50: :: GROUP_23:53

for I being non empty set
for i being Element of I
for F being Group-Family of I holds Image (proj (F,i)) = multMagma(# the carrier of (F . i), the multF of (F . i) #)

proof end;

theorem :: GROUP_23:54

for I being non empty set
for F being Group-Family of I
for F1, F2 being componentwise_strict Subgroup-Family of F st ( for i being Element of I holds Image (proj (F1,i)) is Subgroup of Image (proj (F2,i)) ) holds
product F1 is strict Subgroup of product F2

proof end;

theorem :: GROUP_23:55

for I being non empty set
for F being Group-Family of I
for G being strict Subgroup of product F
for S being Subgroup-Family of F st ( for i being Element of I holds S . i = Image ((proj (F,i)) * (incl G)) ) holds
for f being Homomorphism-Family of G,S st ( for i being Element of I holds f . i = (proj (F,i)) * (incl G) ) holds
product f = id the carrier of G

proof end;

theorem ThMorphismOfCommutators: :: GROUP_23:56

for G1, G2 being Group
for phi being Homomorphism of G1,G2
for x being Element of G1 st x in commutators G1 holds
phi . x in commutators G2

proof end;

theorem :: GROUP_23:57

for G1, G2, G3 being Group
for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G2,G3
for g being Element of G1 holds (f2 * f1) . g = f2 . (f1 . g)

proof end;

theorem :: GROUP_23:58

for G1, G2 being Group
for H being Subgroup of G2
for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G1,H st f1 = f2 holds
Image f1 = Image f2

proof end;

theorem Th57: :: GROUP_23:59

for I being non empty set
for F being Group-Family of I
for a, b being Element of (product F)
for i being Element of I holds [.a,b.] . i = [.(a /. i),(b /. i).]

proof end;

scheme :: GROUP_23:sch 6
SubFamEx{ F₁() -> non empty set , F₂() -> Group-Family of F₁(), P₁[ object , object ] } :

ex S being Subgroup-Family of F₂() st
for i being Element of F₁() holds P₁[i,S . i]

provided

A1: for i being Element of F₁() ex j being Subgroup of F₂() . i st P₁[i,j]

proof end;

theorem :: GROUP_23:60

for I being non empty set
for F being Group-Family of I
for A being ManySortedSet of I st ( for i being Element of I holds A . i is Subset of (F . i) ) holds
product A is Subset of (product F)

proof end;

theorem Th59: :: GROUP_23:61

for I being non empty set
for F being Group-Family of I
for S being normal Subgroup-Family of F holds product S is normal Subgroup of product F

proof end;

registration

let I be non empty set ;
let F be Group-Family of I;
let S be normal Subgroup-Family of F;

cluster product S -> normal for Subgroup of product F;

correctness
coherence
for b₁ being Subgroup of product F st b₁ = product S holds
b₁ is normal ;
by Th59;

end;

:: Kurosh, Theory of Groups, volume I, result VI about Direct Products

theorem :: GROUP_23:62

for I being non empty set
for F, Z being Group-Family of I st ( for i being Element of I holds Z . i = center (F . i) ) holds
center (product F) = product Z

proof end;

theorem Th61: :: GROUP_23:63

for I being non empty set
for F being Group-Family of I
for D being Subgroup-Family of F st ( for i being Element of I holds D . i = (F . i) ` ) holds
(product F) ` is strict Subgroup of product D

proof end;

LmHeartOf62: for I being non empty set
for F being Group-Family of I
for D being Subgroup-Family of F st ( for i being Element of I holds D . i = (F . i) ` ) holds
for g being Element of (product F) st g in sum D holds
for J being finite Subset of I
for b being ManySortedSet of J st ( for j being object st j in J holds
g . j = b . j ) holds
for x, B being set st x in J & B c= J & not x in B & ex FS0 being FinSequence of the carrier of (product F) ex ks being FinSequence of INT st
( len FS0 = len ks & rng FS0 c= commutators (product F) & (1_ (product F)) +* (b | B) = Product (FS0 |^ ks) ) holds
ex FS being FinSequence of the carrier of (product F) ex ks being FinSequence of INT st
( len FS = len ks & rng FS c= commutators (product F) & (1_ (product F)) +* (b | (B \/ {x})) = Product (FS |^ ks) )

proof end;

theorem Th62: :: GROUP_23:64

for I being non empty set
for F being Group-Family of I
for D being Subgroup-Family of F st ( for i being Element of I holds D . i = (F . i) ` ) holds
sum D is strict Subgroup of (product F) `

proof end;

theorem :: GROUP_23:65

for I being non empty finite set
for F being Group-Family of I
for D being Subgroup-Family of F st ( for i being Element of I holds D . i = (F . i) ` ) holds
(product F) ` = product D

proof end;

definition

let I be non empty set ;
let F1, F2 be Group-Family of I;
let f be Homomorphism-Family of F1,F2;

func product f -> Homomorphism of (product F1),(product F2) means :Def15: :: GROUP_23:def 16
for i being Element of I holds (proj (F2,i)) * it = (f . i) * (proj (F1,i));

existence
ex b₁ being Homomorphism of (product F1),(product F2) st
for i being Element of I holds (proj (F2,i)) * b₁ = (f . i) * (proj (F1,i))

proof end;

uniqueness
for b₁, b₂ being Homomorphism of (product F1),(product F2) st ( for i being Element of I holds (proj (F2,i)) * b₁ = (f . i) * (proj (F1,i)) ) & ( for i being Element of I holds (proj (F2,i)) * b₂ = (f . i) * (proj (F1,i)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines product GROUP_23:def 16 :
for I being non empty set
for F1, F2 being Group-Family of I
for f being Homomorphism-Family of F1,F2
for b₅ being Homomorphism of (product F1),(product F2) holds
( b₅ = product f iff for i being Element of I holds (proj (F2,i)) * b₅ = (f . i) * (proj (F1,i)) );

definition

let I be non empty set ;
let F1, F2 be Group-Family of I;
let f be Homomorphism-Family of F1,F2;

func Ker f -> componentwise_strict normal Subgroup-Family of F1 means :Def16: :: GROUP_23:def 17
for i being Element of I holds it . i = Ker (f . i);

existence
ex b₁ being componentwise_strict normal Subgroup-Family of F1 st
for i being Element of I holds b₁ . i = Ker (f . i)

proof end;

uniqueness
for b₁, b₂ being componentwise_strict normal Subgroup-Family of F1 st ( for i being Element of I holds b₁ . i = Ker (f . i) ) & ( for i being Element of I holds b₂ . i = Ker (f . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines Ker GROUP_23:def 17 :
for I being non empty set
for F1, F2 being Group-Family of I
for f being Homomorphism-Family of F1,F2
for b₅ being componentwise_strict normal Subgroup-Family of F1 holds
( b₅ = Ker f iff for i being Element of I holds b₅ . i = Ker (f . i) );

definition

let I be non empty set ;
let F1, F2 be Group-Family of I;
let f be Homomorphism-Family of F1,F2;

func Image f -> componentwise_strict Subgroup-Family of F2 means :Def17: :: GROUP_23:def 18
for i being Element of I holds it . i = Image (f . i);

existence
ex b₁ being componentwise_strict Subgroup-Family of F2 st
for i being Element of I holds b₁ . i = Image (f . i)

proof end;

uniqueness
for b₁, b₂ being componentwise_strict Subgroup-Family of F2 st ( for i being Element of I holds b₁ . i = Image (f . i) ) & ( for i being Element of I holds b₂ . i = Image (f . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines Image GROUP_23:def 18 :
for I being non empty set
for F1, F2 being Group-Family of I
for f being Homomorphism-Family of F1,F2
for b₅ being componentwise_strict Subgroup-Family of F2 holds
( b₅ = Image f iff for i being Element of I holds b₅ . i = Image (f . i) );

:: Hungerford, Algebra, Chapter I, Section 8, Theorem 8.10

theorem Th64: :: GROUP_23:66

for I being non empty set
for F1, F2 being Group-Family of I
for f being Homomorphism-Family of F1,F2 holds Ker (product f) = product (Ker f)

proof end;

:: Hungerford, Algebra, Chapter I, Section 8, Theorem 8.10

theorem Th65: :: GROUP_23:67

for I being non empty set
for F1, F2 being Group-Family of I
for f being Homomorphism-Family of F1,F2 holds Image (product f) = product (Image f)

proof end;

theorem :: GROUP_23:68

for I being non empty set
for F being Group-Family of I
for S being componentwise_strict normal Subgroup-Family of F holds (product F) ./. (product S), product (F ./. S) are_isomorphic

proof end;

definition

let I be set ;
let G be Group;
let IT be Subgroup-Family of I,G;

attr IT is normal means :Def18: :: GROUP_23:def 19
for i being object st i in I holds
IT . i is normal Subgroup of G;

attr IT is componentwise_strict means :Def19: :: GROUP_23:def 20
for i being object st i in I holds
IT . i is strict Subgroup of G;

end;

:: deftheorem Def18 defines normal GROUP_23:def 19 :
for I being set
for G being Group
for IT being Subgroup-Family of I,G holds
( IT is normal iff for i being object st i in I holds
IT . i is normal Subgroup of G );

:: deftheorem Def19 defines componentwise_strict GROUP_23:def 20 :
for I being set
for G being Group
for IT being Subgroup-Family of I,G holds
( IT is componentwise_strict iff for i being object st i in I holds
IT . i is strict Subgroup of G );

theorem ThS1: :: GROUP_23:69

for I being non empty set
for G being Group
for F being Subgroup-Family of I,G holds
( F is normal iff for i being Element of I holds F . i is normal Subgroup of G ) ;

theorem ThS2: :: GROUP_23:70

for I being non empty set
for G being Group
for F being Subgroup-Family of I,G holds
( F is componentwise_strict iff for i being Element of I holds F . i is strict Subgroup of G ) ;

registration

let I be set ;
let G be Group;

cluster Relation-like I -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative Group-yielding normal componentwise_strict for Subgroup-Family of I,G;

existence
ex b₁ being Subgroup-Family of I,G st
( b₁ is componentwise_strict & b₁ is normal )

proof end;

end;

definition

let I be non empty set ;
let G be Group;
let F be Subgroup-Family of I,G;
let i be Element of I;
:: original: .
redefine func F . i -> Subgroup of G;
coherence
F . i is Subgroup of G by GROUP_20:def 1;

end;

registration

let I be non empty set ;
let G be Group;
let F be normal Subgroup-Family of I,G;
let i be Element of I;

cluster F . i -> normal for Subgroup of G;

correctness
coherence
for b₁ being Subgroup of G st b₁ = F . i holds
b₁ is normal ;
by ThS1;

end;

theorem :: GROUP_23:71

for G being Group
for H1, H2 being Subgroup of G st [.H1,H2.] = (1). G holds
for a, b being Element of G st a in H1 & b in H2 holds
a * b = b * a

proof end;

:: Weaker form of GROUP_5:3, we don't really need N to be "strict"
::: Generalize GROUP_5:3

theorem ThNorm: :: GROUP_23:72

for G being Group
for N being normal Subgroup of G
for a, b being Element of G st a in N holds
a |^ b in N

proof end;

theorem :: GROUP_23:73

for G being Group
for H, K being normal Subgroup of G st H /\ K = (1). G holds
for h, k being Element of G st h in H & k in K holds
h * k = k * h

proof end;

theorem ThJoinNorm: :: GROUP_23:74

for I being non empty set
for G being Group
for F being normal Subgroup-Family of I,G
for A being Subset of G st A = union { the carrier of (F . i) where i is Element of I : verum } holds
ex N being strict normal Subgroup of G st N = gr A

proof end;

registration

let I be set ;
let J be Subset of I;
let F be Group-yielding ManySortedSet of I;

cluster F | J -> J -defined total Group-yielding ;

correctness
coherence
( F | J is Group-yielding & F | J is J -defined & F | J is total );

proof end;

end;

theorem ThSubFamRes: :: GROUP_23:75

for G being Group
for I being set
for F being Subgroup-Family of I,G
for J being set st J c= I holds
F | J is Subgroup-Family of J,G

proof end;

definition

let I be set ;
let G be Group;
let F be Subgroup-Family of I,G;
let J be Subset of I;
:: original: |
redefine func F | J -> Subgroup-Family of J,G;
correctness
coherence
F | J is Subgroup-Family of J,G;
by ThSubFamRes;

end;

registration

let I be set ;
let G be Group;
let F be Subgroup-Family of I,G;
let J be Subset of I;

cluster F | J -> Group-yielding ;

correctness
coherence
F | J is Group-yielding ;
;

end;

theorem :: GROUP_23:76

for I being non empty set
for G being Group
for F being normal Subgroup-Family of I,G
for A being Subset of G
for i being Element of I st A = union { the carrier of (F . j) where j is Element of I : i <> j } holds
ex N being strict normal Subgroup of G st N = gr A

proof end;

theorem :: GROUP_23:77

for I being non empty set
for G being Group
for J being non empty Subset of I
for F being normal Subgroup-Family of I,G holds F | J is normal Subgroup-Family of J,G

proof end;

theorem ThNormSubFamResIsNorm: :: GROUP_23:78

for G being Group
for I being set
for J being Subset of I
for F being normal Subgroup-Family of I,G holds F | J is normal Subgroup-Family of J,G

proof end;

registration

let I be set ;
let J be Subset of I;
let G be Group;
let F be normal Subgroup-Family of I,G;

cluster F | J -> normal for Subgroup-Family of J,G;

correctness
coherence
for b₁ being Subgroup-Family of J,G st b₁ = F | J holds
b₁ is normal ;
by ThNormSubFamResIsNorm;

end;

theorem ThStrSubFamResIsStr: :: GROUP_23:79

for G being Group
for I being set
for J being Subset of I
for F being componentwise_strict Subgroup-Family of I,G holds F | J is componentwise_strict Subgroup-Family of J,G

proof end;

registration

let I be set ;
let J be Subset of I;
let G be Group;
let F be componentwise_strict Subgroup-Family of I,G;

cluster F | J -> componentwise_strict for Subgroup-Family of J,G;

correctness
coherence
for b₁ being Subgroup-Family of J,G st b₁ = F | J holds
b₁ is componentwise_strict ;
by ThStrSubFamResIsStr;

end;

LmJoinNormUnionRes: for I being non empty set
for G being Group
for J being non empty Subset of I
for F being normal Subgroup-Family of I,G
for A being Subset of G st A = Union (Carrier (F | J)) holds
ex N being strict normal Subgroup of G st N = gr A

proof end;

theorem :: GROUP_23:80

for G being Group
for I being set
for J being Subset of I st J is empty holds
for F being normal Subgroup-Family of I,G holds Carrier (F | J) = {} --> (bool the carrier of G) ;

theorem ThJoinNormUnionRes: :: GROUP_23:81

for G being Group
for I being set
for J being Subset of I
for F being normal Subgroup-Family of I,G
for A being Subset of G st A = Union (Carrier (F | J)) holds
ex N being strict normal Subgroup of G st N = gr A

proof end;

theorem :: GROUP_23:82

for G being Group
for I being set
for F being normal Subgroup-Family of I,G
for A being Subset of G st A = Union (Carrier F) holds
ex N being strict normal Subgroup of G st N = gr A

proof end;

theorem CSSubFam: :: GROUP_23:83

for I being non empty set
for G being Group
for F being componentwise_strict Subgroup-Family of I,G holds F is Subgroups G -valued

proof end;

registration

let I be non empty set ;
let G be Group;

cluster componentwise_strict -> Subgroups G -valued componentwise_strict for Subgroup-Family of I,G;

correctness
coherence
for b₁ being componentwise_strict Subgroup-Family of I,G holds b₁ is Subgroups G -valued ;
by CSSubFam;

end;

definition

let I be set ;
let F be 1-sorted-yielding ManySortedSet of I;
mode Element of F is Element of Carrier F;

end;

theorem EltGF: :: GROUP_23:84

for I being non empty set
for F being Group-Family of I
for g being Element of F
for i being Element of I holds g . i is Element of (F . i)

proof end;

registration

let I be non empty set ;
let G be Group;
let F be Subgroup-Family of I,G;

cluster -> the carrier of G -valued for Element of Carrier F;

correctness
coherence
for b₁ being Element of F holds b₁ is the carrier of G -valued ;

proof end;

end;

registration

let I be non empty set ;
let G be Group;
let F be Subgroup-Family of I,G;

cluster -> Relation-like I -defined Function-like for Element of the carrier of (product F);

coherence
for b₁ being Element of (product F) holds
( b₁ is I -defined & b₁ is Relation-like & b₁ is Function-like )

proof end;

end;

registration

let I be non empty set ;
let G be Group;
let F be Subgroup-Family of I,G;

cluster -> I -defined the carrier of G -valued total for Element of the carrier of (product F);

correctness
coherence
for b₁ being Element of (product F) holds
( b₁ is I -defined & b₁ is the carrier of G -valued & b₁ is total );

proof end;

end;

theorem ThSubFamIsBoolValued: :: GROUP_23:85

for I being set
for G being Group
for F being Subgroup-Family of I,G holds Carrier F is bool the carrier of G -valued

proof end;

registration

let I be set ;
let G be Group;
let F be Subgroup-Family of I,G;

cluster Carrier F -> bool the carrier of G -valued ;

correctness
coherence
Carrier F is bool the carrier of G -valued ;
by ThSubFamIsBoolValued;

end;

theorem ThCanSubgrFam: :: GROUP_23:86

for G being Group
for S being finite Subset of (Subgroups G)
for n being Nat st n = card S holds
canFS S is Subgroup-Family of Seg n,G

proof end;

theorem :: GROUP_23:87

for G being Group
for N being finite Subset of (the_normal_subgroups_of G)
for n being Nat st n = card N holds
canFS N is normal Subgroup-Family of Seg n,G

proof end;

theorem ThJoinEmptyGr: :: GROUP_23:88

for G being Group
for I being empty set
for F being Subgroup-Family of I,G holds gr (Union (Carrier F)) = (1). G

proof end;

definition

let G be Group;
let I be set ;
let F be Subgroup-Family of I,G;
let i be object ;
assume A1: i in I ;

func F /. i -> Subgroup of G equals :Def20: :: GROUP_23:def 21
F . i;

coherence
F . i is Subgroup of G by A1, GROUP_20:def 1;

end;

:: deftheorem Def20 defines /. GROUP_23:def 21 :
for G being Group
for I being set
for F being Subgroup-Family of I,G
for i being object st i in I holds
F /. i = F . i;

definition

let G be Group;
let I be set ;
let F be Subgroup-Family of I,G;

pred G is_internal_product_of F means :: GROUP_23:def 22
( ( for i being object st i in I holds
F . i is normal Subgroup of G ) & multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being object st i in I holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | (I \ { j where j is Element of I : F . i = F . j } )))) holds
(F /. i) /\ N = (1). G ) );

end;

:: deftheorem defines is_internal_product_of GROUP_23:def 22 :
for G being Group
for I being set
for F being Subgroup-Family of I,G holds
( G is_internal_product_of F iff ( ( for i being object st i in I holds
F . i is normal Subgroup of G ) & multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being object st i in I holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | (I \ { j where j is Element of I : F . i = F . j } )))) holds
(F /. i) /\ N = (1). G ) ) );

theorem :: GROUP_23:89

for G being Group
for I being empty set
for F being Subgroup-Family of I,G holds
( G is_internal_product_of F iff G is trivial )

proof end;

theorem ThIPOa: :: GROUP_23:90

for G being Group
for I being non empty set
for F being Subgroup-Family of I,G holds
( G is_internal_product_of F iff ( ( for i being Element of I holds F . i is normal Subgroup of G ) & multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ) ) )

proof end;

definition

let G be Group;
let I be set ;
let F be normal Subgroup-Family of I,G;

redefine pred G is_internal_product_of F means :: GROUP_23:def 23
( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being object st i in I holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | (I \ { j where j is Element of I : F . i = F . j } )))) holds
(F /. i) /\ N = (1). G ) );

correctness
compatibility
( G is_internal_product_of F iff ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being object st i in I holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | (I \ { j where j is Element of I : F . i = F . j } )))) holds
(F /. i) /\ N = (1). G ) ) );
by Def18;

end;

:: deftheorem defines is_internal_product_of GROUP_23:def 23 :
for G being Group
for I being set
for F being normal Subgroup-Family of I,G holds
( G is_internal_product_of F iff ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being object st i in I holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | (I \ { j where j is Element of I : F . i = F . j } )))) holds
(F /. i) /\ N = (1). G ) ) );

theorem ThIPO: :: GROUP_23:91

for G being Group
for I being non empty set
for F being normal Subgroup-Family of I,G holds
( G is_internal_product_of F iff ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being Element of I
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ) ) )

proof end;

theorem ThInjectiveIPO: :: GROUP_23:92

for G being Group
for I being non empty set
for F being normal Subgroup-Family of I,G st F is one-to-one holds
( G is_internal_product_of F iff ( multMagma(# the carrier of G, the multF of G #) = gr (Union (Carrier F)) & ( for i being Element of I
for J being Subset of I st J = I \ {i} holds
for N being strict normal Subgroup of G st N = gr (Union (Carrier (F | J))) holds
(F . i) /\ N = (1). G ) ) )

proof end;

:: Aschbacher, Finite Group Theory, Theorem (1.9)
:: Hungerford, Algebra, Ch. 1, section 8, Theorem 8.6
:: Robinson, Theory of Groups, Ch 1, section 4, Theorem 1.4.7 (ii)

theorem :: GROUP_23:93

for G being strict Group
for I being non empty set
for F being normal Subgroup-Family of I,G st F is one-to-one holds
( G is_internal_product_of F iff F is internal DirectSumComponents of G,I )

proof end;

definition

let G be Group;
let Fam be Subset of (Subgroups G);

pred G is_internal_product_of Fam means :: GROUP_23:def 24
( ( for H being strict Subgroup of G st H in Fam holds
H is normal Subgroup of G ) & ex A being Subset of G st
( A = union { UH where UH is Subset of G : ex H being strict Subgroup of G st
( H in Fam & UH = the carrier of H ) } & multMagma(# the carrier of G, the multF of G #) = gr A ) & ( for H being strict Subgroup of G st H in Fam holds
for A being Subset of G st A = union { UK where UK is Subset of G : ex K being strict Subgroup of G st
( K in Fam & UK = the carrier of K & K <> H ) } holds
H /\ (gr A) = (1). G ) );

end;

:: deftheorem defines is_internal_product_of GROUP_23:def 24 :
for G being Group
for Fam being Subset of (Subgroups G) holds
( G is_internal_product_of Fam iff ( ( for H being strict Subgroup of G st H in Fam holds
H is normal Subgroup of G ) & ex A being Subset of G st
( A = union { UH where UH is Subset of G : ex H being strict Subgroup of G st
( H in Fam & UH = the carrier of H ) } & multMagma(# the carrier of G, the multF of G #) = gr A ) & ( for H being strict Subgroup of G st H in Fam holds
for A being Subset of G st A = union { UK where UK is Subset of G : ex K being strict Subgroup of G st
( K in Fam & UK = the carrier of K & K <> H ) } holds
H /\ (gr A) = (1). G ) ) );

:: We eventually want to prove a proposition along the lines of
:: "FittingSubgroup G is_internal_product_of Sylow_subgroups G"
:: *without* having to construct a family of subgroups.

definition

let G be Group;
let H be strict Subgroup of G;
let Fam be Subset of (Subgroups G);

pred H is_internal_product_of Fam means :: GROUP_23:def 25
( ( for H1 being strict Subgroup of G st H1 in Fam holds
H1 is normal Subgroup of H ) & ex A being Subset of G st
( A = union { UH where UH is Subset of G : ex H being strict Subgroup of G st
( H in Fam & UH = the carrier of H ) } & H = gr A ) & ( for H1 being strict Subgroup of G st H1 in Fam holds
for A being Subset of G st A = union { UK where UK is Subset of G : ex K being strict Subgroup of G st
( K in Fam & UK = the carrier of K & K <> H1 ) } holds
H1 /\ (gr A) = (1). G ) );

end;

:: deftheorem defines is_internal_product_of GROUP_23:def 25 :
for G being Group
for H being strict Subgroup of G
for Fam being Subset of (Subgroups G) holds
( H is_internal_product_of Fam iff ( ( for H1 being strict Subgroup of G st H1 in Fam holds
H1 is normal Subgroup of H ) & ex A being Subset of G st
( A = union { UH where UH is Subset of G : ex H being strict Subgroup of G st
( H in Fam & UH = the carrier of H ) } & H = gr A ) & ( for H1 being strict Subgroup of G st H1 in Fam holds
for A being Subset of G st A = union { UK where UK is Subset of G : ex K being strict Subgroup of G st
( K in Fam & UK = the carrier of K & K <> H1 ) } holds
H1 /\ (gr A) = (1). G ) ) );

theorem ThGSubOmega: :: GROUP_23:94

for G being Group holds G is Subgroup of (Omega). G

proof end;

theorem ThMinorAnnoyance: :: GROUP_23:95

for G being Group
for H being Subgroup of G st H is normal Subgroup of (Omega). G holds
H is normal Subgroup of G

proof end;

theorem :: GROUP_23:96

for G being Group
for Fam being Subset of (Subgroups G) holds
( G is_internal_product_of Fam iff (Omega). G is_internal_product_of Fam )

proof end;

theorem ThCarrG: :: GROUP_23:97

for G being Group
for I being non empty set
for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of (Subgroups G) st Fam = rng F holds
union { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } = Union (Carrier F)

proof end;

theorem ThUnionFam: :: GROUP_23:98

for G being Group
for I being non empty set
for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of (Subgroups G) st Fam = rng F holds
for H being strict Subgroup of G
for i being Element of I st H = F . i holds
for J being Subset of I st J = I \ { j where j is Element of I : F . i = F . j } holds
union { A where A is Subset of G : ex K being strict Subgroup of G st
( K in Fam & A = the carrier of K & K <> H ) } = Union (Carrier (F | J))

proof end;

theorem :: GROUP_23:99

for G being Group
for I being non empty set
for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of (Subgroups G) st Fam = rng F holds
( G is_internal_product_of F iff G is_internal_product_of Fam )

proof end;