set H = ProjGroup (F,i);
set G = product F;
A1:
for a being Element of (product F) holds (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i))
proof
let a be
Element of
(product F);
(a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i))
now for x being object st x in (a * (ProjGroup (F,i))) * (a ") holds
x in the carrier of (ProjGroup (F,i))let x be
object ;
( x in (a * (ProjGroup (F,i))) * (a ") implies x in the carrier of (ProjGroup (F,i)) )assume
x in (a * (ProjGroup (F,i))) * (a ")
;
x in the carrier of (ProjGroup (F,i))then consider h being
Element of
(product F) such that A2:
(
x = h * (a ") &
h in a * (ProjGroup (F,i)) )
by GROUP_2:28;
consider k being
Element of
(product F) such that A3:
(
h = a * k &
k in ProjGroup (
F,
i) )
by A2, GROUP_2:103;
k in the
carrier of
(ProjGroup (F,i))
by A3, STRUCT_0:def 5;
then
k in ProjSet (
F,
i)
by Def2;
then consider m being
Function,
g being
Element of
(F . i) such that A4:
(
m = k &
dom m = I &
m . i = g & ( for
j being
Element of
I st
j <> i holds
m . j = 1_ (F . j) ) )
by Th2;
set n =
(a * k) * (a ");
A5:
the
carrier of
(product F) = product (Carrier F)
by GROUP_7:def 2;
A6:
dom (Carrier F) = I
by PARTFUN1:def 2;
A7:
dom ((a * k) * (a ")) = I
by A5, PARTFUN1:def 2;
set Gi =
F . i;
consider Ri being
1-sorted such that A8:
(
Ri = F . i &
(Carrier F) . i = the
carrier of
Ri )
by PRALG_1:def 15;
set ak =
a * k;
set ad =
a " ;
reconsider xa =
a . i,
xk =
k . i as
Element of
(F . i) by A8, A5, A6, CARD_3:9;
A9:
(a * k) . i = xa * xk
by GROUP_7:1;
A10:
(a ") . i = xa "
by GROUP_7:8;
A11:
((a * k) * (a ")) . i = (xa * xk) * (xa ")
by A9, A10, GROUP_7:1;
then
(a * k) * (a ") in ProjSet (
F,
i)
by A7, A11, Th2;
hence
x in the
carrier of
(ProjGroup (F,i))
by Def2, A2, A3;
verum end;
hence
(a * (ProjGroup (F,i))) * (a ") c= the
carrier of
(ProjGroup (F,i))
by TARSKI:def 3;
verum
end;
A16:
for a being Element of (product F) holds a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a
proof
let a be
Element of
(product F);
a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a
A17:
(a * (ProjGroup (F,i))) * (a ") c= the
carrier of
(ProjGroup (F,i))
by A1;
A18:
(a ") * a = 1_ (product F)
by GROUP_1:def 5;
((a * (ProjGroup (F,i))) * (a ")) * a =
(a * ((ProjGroup (F,i)) * (a "))) * a
by GROUP_2:106
.=
a * (((ProjGroup (F,i)) * (a ")) * a)
by GROUP_2:33
.=
a * ((ProjGroup (F,i)) * ((a ") * a))
by GROUP_2:107
.=
a * (ProjGroup (F,i))
by A18, GROUP_2:109
;
hence
a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a
by A17, GROUP_3:5;
verum
end;
A19:
for a being Element of (product F) holds (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i))
proof
let a be
Element of
(product F);
(ProjGroup (F,i)) * a c= a * (ProjGroup (F,i))
A20:
((a ") * (ProjGroup (F,i))) * ((a ") ") c= the
carrier of
(ProjGroup (F,i))
by A1;
A21:
a * (a ") = 1_ (product F)
by GROUP_1:def 5;
a * (((a ") * (ProjGroup (F,i))) * a) =
a * ((a ") * ((ProjGroup (F,i)) * a))
by GROUP_2:106
.=
(a * (a ")) * ((ProjGroup (F,i)) * a)
by GROUP_2:32
.=
((a * (a ")) * (ProjGroup (F,i))) * a
by GROUP_2:106
.=
(ProjGroup (F,i)) * a
by A21, GROUP_2:109
;
hence
(ProjGroup (F,i)) * a c= a * (ProjGroup (F,i))
by A20, GROUP_3:5;
verum
end;
for a being Element of (product F) holds a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a
hence
ProjGroup (F,i) is normal
by GROUP_3:117; verum