let I0, I be non empty finite set ; for F0 being Group-like associative multMagma-Family of I0
for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),(product F)
let F0 be Group-like associative multMagma-Family of I0; for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),(product F)
let F be Group-like associative multMagma-Family of I; for H, K being Group
for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),(product F)
let H, K be Group; for q being Element of I
for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),(product F)
let q be Element of I; for G0 being Function of H,(product F0) st G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),(product F)
let G0 be Function of H,(product F0); ( G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) implies for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),(product F) )
assume A1:
( G0 is Homomorphism of H,(product F0) & G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) )
; for G being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),(product F)
let G be Function of (product <*H,K*>),(product F); ( ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) implies G is Homomorphism of (product <*H,K*>),(product F) )
assume A2:
for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) )
; G is Homomorphism of (product <*H,K*>),(product F)
set HK = <*H,K*>;
A3:
dom (Carrier F) = I
by PARTFUN1:def 2;
now for a, b being Element of (product <*H,K*>) holds G . (a * b) = (G . a) * (G . b)let a,
b be
Element of
(product <*H,K*>);
G . (a * b) = (G . a) * (G . b)consider h1 being
Element of
H,
k1 being
Element of
K such that A4:
a = <*h1,k1*>
by TOPALG_4:1;
consider h2 being
Element of
H,
k2 being
Element of
K such that A5:
b = <*h2,k2*>
by TOPALG_4:1;
consider g1 being
Function such that A6:
(
g1 = G0 . h1 &
G . <*h1,k1*> = g1 +* (q .--> k1) )
by A2;
consider g2 being
Function such that A7:
(
g2 = G0 . h2 &
G . <*h2,k2*> = g2 +* (q .--> k2) )
by A2;
reconsider g1 =
g1 as
I0 -defined total Function by A6, Lm6;
reconsider g2 =
g2 as
I0 -defined total Function by A7, Lm6;
reconsider g12 =
G0 . (h1 * h2) as
I0 -defined total Function by Lm6;
A12:
ex
g12 being
Function st
(
g12 = G0 . (h1 * h2) &
G . <*(h1 * h2),(k1 * k2)*> = g12 +* (q .--> (k1 * k2)) )
by A2;
reconsider Ga =
G . a,
Gb =
G . b as
Element of
(product F) ;
reconsider ga =
g1 +* (q .--> k1) as
I -defined total Function by Lm6, A6;
reconsider gb =
g2 +* (q .--> k2) as
I -defined total Function by Lm6, A7;
reconsider pab =
Ga * Gb as
I -defined total Function by Lm6;
A13:
dom pab = dom (Carrier F)
by PARTFUN1:def 2, A3;
A14:
g12 = (G0 . h1) * (G0 . h2)
by A1, GROUP_6:def 6;
reconsider gab =
G . (a * b) as
I -defined total Function by Lm6;
A15:
gab = g12 +* (q .--> (k1 * k2))
by A4, A5, GROUP_7:29, A12;
A16:
for
i being
set st
i in I0 holds
(
ga . i = g1 . i &
gb . i = g2 . i &
gab . i = g12 . i &
F . i = F0 . i )
proof
let i be
set ;
( i in I0 implies ( ga . i = g1 . i & gb . i = g2 . i & gab . i = g12 . i & F . i = F0 . i ) )
assume A17:
i in I0
;
( ga . i = g1 . i & gb . i = g2 . i & gab . i = g12 . i & F . i = F0 . i )
A18:
dom g1 = I0
by PARTFUN1:def 2;
A19:
dom g2 = I0
by PARTFUN1:def 2;
A20:
dom g12 = I0
by PARTFUN1:def 2;
A21:
dom F0 = I0
by PARTFUN1:def 2;
A22:
i in (dom g1) \/ (dom (q .--> k1))
by A18, A17, XBOOLE_0:def 3;
A23:
i in (dom g2) \/ (dom (q .--> k2))
by A19, A17, XBOOLE_0:def 3;
A24:
i in (dom g12) \/ (dom (q .--> (k1 * k2)))
by A20, A17, XBOOLE_0:def 3;
A25:
i in (dom F0) \/ (dom (q .--> K))
by A21, A17, XBOOLE_0:def 3;
not
i in dom (q .--> K)
by A1, A17, FUNCOP_1:75;
hence
(
ga . i = g1 . i &
gb . i = g2 . i &
gab . i = g12 . i &
F . i = F0 . i )
by A25, FUNCT_4:def 1, A1, A22, A23, A24, A15;
verum
end; A29:
(
ga . q = k1 &
gb . q = k2 &
gab . q = k1 * k2 &
F . q = K )
proof
A30:
q in {q}
by TARSKI:def 1;
A31:
q in dom (q .--> k1)
by TARSKI:def 1;
A32:
q in dom (q .--> k2)
by TARSKI:def 1;
A33:
q in dom (q .--> (k1 * k2))
by TARSKI:def 1;
A34:
q in dom (q .--> K)
by TARSKI:def 1;
A35:
q in (dom g1) \/ (dom (q .--> k1))
by A30, XBOOLE_0:def 3;
A36:
q in (dom g2) \/ (dom (q .--> k2))
by A30, XBOOLE_0:def 3;
A37:
q in (dom g12) \/ (dom (q .--> (k1 * k2)))
by A30, XBOOLE_0:def 3;
A38:
q in (dom F0) \/ (dom (q .--> K))
by A30, XBOOLE_0:def 3;
A39:
ga . q =
(q .--> k1) . q
by A31, A35, FUNCT_4:def 1
.=
k1
by FUNCOP_1:7, A30
;
A40:
gb . q =
(q .--> k2) . q
by A32, A36, FUNCT_4:def 1
.=
k2
by FUNCOP_1:7, A30
;
A41:
gab . q =
(q .--> (k1 * k2)) . q
by A33, A37, A15, FUNCT_4:def 1
.=
k1 * k2
by FUNCOP_1:7, A30
;
F . q =
(q .--> K) . q
by A34, A38, A1, FUNCT_4:def 1
.=
K
by FUNCOP_1:7, A30
;
hence
(
ga . q = k1 &
gb . q = k2 &
gab . q = k1 * k2 &
F . q = K )
by A39, A40, A41;
verum
end; A42:
for
x being
set st
x in I0 holds
pab . x = gab . x
proof
let x be
set ;
( x in I0 implies pab . x = gab . x )
assume A43:
x in I0
;
pab . x = gab . x
then A44:
x in I
by A1, XBOOLE_0:def 3;
consider S being non
empty multMagma such that A45:
(
S = F0 . x &
g1 . x in the
carrier of
S )
by A43, Lm7, A6;
reconsider x0 =
g1 . x as
Element of
S by A45;
ex
R being non
empty multMagma st
(
R = F0 . x &
g2 . x in the
carrier of
R )
by Lm7, A43, A7;
then reconsider y0 =
g2 . x as
Element of
S by A45;
A46:
S = F . x
by A45, A16, A43;
(
x0 = ga . x &
y0 = gb . x )
by A16, A43;
hence pab . x =
x0 * y0
by A44, A46, GROUP_7:1, A6, A4, A7, A5
.=
g12 . x
by A14, A6, A7, GROUP_7:1, A43, A45
.=
gab . x
by A16, A43
;
verum
end;
for
x being
object st
x in dom gab holds
gab . x = pab . x
hence
G . (a * b) = (G . a) * (G . b)
by A13, PARTFUN1:def 2, A3, FUNCT_1:2;
verum end;
hence
G is Homomorphism of (product <*H,K*>),(product F)
by GROUP_6:def 6; verum