let G be Group; for q being set
for F being Group-like associative multMagma-Family of {q}
for f being Function of G,(product F) st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is Homomorphism of G,(product F)
let q be set ; for F being Group-like associative multMagma-Family of {q}
for f being Function of G,(product F) st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is Homomorphism of G,(product F)
let F be Group-like associative multMagma-Family of {q}; for f being Function of G,(product F) st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is Homomorphism of G,(product F)
let f be Function of G,(product F); ( F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) implies f is Homomorphism of G,(product F) )
assume A1:
F = q .--> G
; ( ex x being Element of G st not f . x = q .--> x or f is Homomorphism of G,(product F) )
assume A2:
for x being Element of G holds f . x = q .--> x
; f is Homomorphism of G,(product F)
A3:
the carrier of (product F) = product (Carrier F)
by GROUP_7:def 2;
now for a, b being Element of G holds f . (a * b) = (f . a) * (f . b)let a,
b be
Element of
G;
f . (a * b) = (f . a) * (f . b)A4:
f . a = q .--> a
by A2;
A5:
f . b = q .--> b
by A2;
reconsider fa =
f . a,
fb =
f . b as
Element of
(product F) ;
set ga =
q .--> a;
set gb =
q .--> b;
consider gab being
Function such that A6:
(
fa * fb = gab &
dom gab = dom (Carrier F) & ( for
y being
object st
y in dom (Carrier F) holds
gab . y in (Carrier F) . y ) )
by CARD_3:def 5, A3;
A7:
for
z being
object st
z in dom gab holds
gab . z = a * b
proof
let z be
object ;
( z in dom gab implies gab . z = a * b )
assume A8:
z in dom gab
;
gab . z = a * b
A9:
G = F . z
by A1, FUNCOP_1:7, A8, A6;
A10:
(q .--> a) . z = a
by FUNCOP_1:7, A8, A6;
(q .--> b) . z = b
by FUNCOP_1:7, A8, A6;
hence
gab . z = a * b
by A4, A5, A6, A8, A9, A10, GROUP_7:1;
verum
end; gab =
(dom gab) --> (a * b)
by A7, FUNCOP_1:11
.=
q .--> (a * b)
by A6, PARTFUN1:def 2
.=
f . (a * b)
by A2
;
hence
f . (a * b) = (f . a) * (f . b)
by A6;
verum end;
hence
f is Homomorphism of G,(product F)
by GROUP_6:def 6; verum