let I be 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
let G be 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
let F be 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
let UF be Subset of G; ( UF = Union (Carrier F) implies for i being Element of I holds F . i is normal Subgroup of gr UF )
assume A1:
UF = Union (Carrier F)
; for i being Element of I holds F . i is normal Subgroup of gr UF
let i be Element of I; F . i is normal Subgroup of gr UF
A2:
dom (Carrier F) = I
by PARTFUN1:def 2;
A3:
F . i is Subgroup of G
by Def1;
(Carrier F) . i in rng (Carrier F)
by A2, FUNCT_1:3;
then
[#] (F . i) in rng (Carrier F)
by PENCIL_3:7;
then
[#] (F . i) c= union (rng (Carrier F))
by ZFMISC_1:74;
then A4:
[#] (F . i) c= UF
by A1, CARD_3:def 4;
UF c= [#] (gr UF)
by GROUP_4:def 4;
then
[#] (F . i) c= [#] (gr UF)
by A4;
then reconsider Fi = F . i as Subgroup of gr UF by A3, GROUP_2:57;
for a being Element of (gr UF) holds a * Fi c= Fi * a
proof
let a be
Element of
(gr UF);
a * Fi c= Fi * a
for
x being
object st
x in a * Fi holds
x in Fi * a
proof
let x be
object ;
( x in a * Fi implies x in Fi * a )
assume
x in a * Fi
;
x in Fi * a
then consider g being
Element of
(gr UF) such that A5:
(
x = a * g &
g in Fi )
by GROUP_2:103;
reconsider a1 =
a as
Element of
G by GROUP_2:42;
a1 in gr UF
;
then consider h being
finite-support Function of
I,
(gr UF) such that A6:
(
h in sum F &
a = Product h )
by A1, Th13;
reconsider m =
h . i as
Element of
(gr UF) ;
A7:
h in product F
by A6, GROUP_2:40;
A8:
h . i in F . i
by A6, GROUP_19:5, GROUP_2:40;
reconsider I0 =
I \ {i} as
Subset of
I ;
1_ (F . i) in gr UF
by A3, GROUP_2:47;
then reconsider h0 =
h +* (
i,
(1_ (F . i))) as
finite-support Function of
I,
(gr UF) by GROUP_19:26;
A9:
h0 in product F
by A6, GROUP_19:24, GROUP_2:40;
dom h = I
by FUNCT_2:def 1;
then A10:
h0 . i = 1_ (F . i)
by FUNCT_7:31;
A11:
a * g =
((Product h0) * m) * g
by A6, A7, Th9
.=
(Product h0) * (m * g)
by GROUP_1:def 3
;
A12:
a * g =
(m * g) * (Product h0)
by A5, A8, A9, A10, A11, GROUP_2:50, Th10
.=
((m * g) * (1_ (gr UF))) * (Product h0)
by GROUP_1:def 4
.=
((m * g) * ((m ") * m)) * (Product h0)
by GROUP_1:def 5
.=
(((m * g) * (m ")) * m) * (Product h0)
by GROUP_1:def 3
.=
((m * g) * (m ")) * (m * (Product h0))
by GROUP_1:def 3
.=
((m * g) * (m ")) * ((Product h0) * m)
by A7, Th9
.=
((m * g) * (m ")) * a
by A6, A7, Th9
;
m " in Fi
by A8, GROUP_2:51;
then
g * (m ") in Fi
by A5, GROUP_2:50;
then
m * (g * (m ")) in Fi
by A8, GROUP_2:50;
then
(m * g) * (m ") in Fi
by GROUP_1:def 3;
hence
x in Fi * a
by A5, A12, GROUP_2:104;
verum
end;
hence
a * Fi c= Fi * a
;
verum
end;
hence
F . i is normal Subgroup of gr UF
by GROUP_3:118; verum