let U1, U2 be Universal_Algebra; for h being Function of U1,U2
for h1 being Function of U2,U1 st h is_isomorphism & h1 = h " holds
h1 is_homomorphism
let h be Function of U1,U2; for h1 being Function of U2,U1 st h is_isomorphism & h1 = h " holds
h1 is_homomorphism
let h1 be Function of U2,U1; ( h is_isomorphism & h1 = h " implies h1 is_homomorphism )
assume that
A1:
h is_isomorphism
and
A2:
h1 = h "
; h1 is_homomorphism
A3:
h is one-to-one
by A1, Th7;
A4:
h is_homomorphism
by A1, Th7;
then A5:
U1,U2 are_similar
;
then A6:
signature U1 = signature U2
;
A7:
( len (signature U1) = len the charact of U1 & dom the charact of U1 = Seg (len the charact of U1) )
by FINSEQ_1:def 3, UNIALG_1:def 4;
A8:
dom (signature U2) = Seg (len (signature U2))
by FINSEQ_1:def 3;
A9:
( len (signature U2) = len the charact of U2 & dom the charact of U2 = Seg (len the charact of U2) )
by FINSEQ_1:def 3, UNIALG_1:def 4;
A10:
rng h = the carrier of U2
by A1, Th7;
now for n being Nat st n in dom the charact of U2 holds
for o2 being operation of U2
for o1 being operation of U1 st o2 = the charact of U2 . n & o1 = the charact of U1 . n holds
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x)let n be
Nat;
( n in dom the charact of U2 implies for o2 being operation of U2
for o1 being operation of U1 st o2 = the charact of U2 . n & o1 = the charact of U1 . n holds
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x) )assume A11:
n in dom the
charact of
U2
;
for o2 being operation of U2
for o1 being operation of U1 st o2 = the charact of U2 . n & o1 = the charact of U1 . n holds
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x)let o2 be
operation of
U2;
for o1 being operation of U1 st o2 = the charact of U2 . n & o1 = the charact of U1 . n holds
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x)let o1 be
operation of
U1;
( o2 = the charact of U2 . n & o1 = the charact of U1 . n implies for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x) )assume A12:
(
o2 = the
charact of
U2 . n &
o1 = the
charact of
U1 . n )
;
for x being FinSequence of U2 st x in dom o2 holds
h1 . (o2 . x) = o1 . (h1 * x)let x be
FinSequence of
U2;
( x in dom o2 implies h1 . (o2 . x) = o1 . (h1 * x) )defpred S1[
set ,
set ]
means h . $2
= x . $1;
A13:
dom x = Seg (len x)
by FINSEQ_1:def 3;
A14:
for
m being
Nat st
m in Seg (len x) holds
ex
a being
Element of
U1 st
S1[
m,
a]
consider p being
FinSequence of
U1 such that A17:
(
dom p = Seg (len x) & ( for
m being
Nat st
m in Seg (len x) holds
S1[
m,
p . m] ) )
from FINSEQ_1:sch 5(A14);
A18:
dom (h * p) = dom p
by FINSEQ_3:120;
then A20:
x = h * p
by A17, A13, A18;
A21:
len p = len x
by A17, FINSEQ_1:def 3;
assume
x in dom o2
;
h1 . (o2 . x) = o1 . (h1 * x)then
x in (arity o2) -tuples_on the
carrier of
U2
by MARGREL1:22;
then
x in { s where s is Element of the carrier of U2 * : len s = arity o2 }
by FINSEQ_2:def 4;
then A22:
ex
s being
Element of the
carrier of
U2 * st
(
x = s &
len s = arity o2 )
;
A23:
h1 * h =
id (dom h)
by A2, A3, FUNCT_1:39
.=
id the
carrier of
U1
by FUNCT_2:def 1
;
then A24:
h1 * x =
(id the carrier of U1) * p
by A20, Th4
.=
p
by Th3
;
reconsider p =
p as
Element of the
carrier of
U1 * by FINSEQ_1:def 11;
(
(signature U1) . n = arity o1 &
(signature U2) . n = arity o2 )
by A6, A8, A9, A11, A12, UNIALG_1:def 4;
then
p in { w where w is Element of the carrier of U1 * : len w = arity o1 }
by A6, A22, A21;
then
p in (arity o1) -tuples_on the
carrier of
U1
by FINSEQ_2:def 4;
then A25:
p in dom o1
by MARGREL1:22;
then A26:
h1 . (o2 . x) = h1 . (h . (o1 . p))
by A4, A6, A7, A9, A11, A12, A20;
A27:
o1 . p in the
carrier of
U1
by A25, PARTFUN1:4;
then
o1 . p in dom h
by FUNCT_2:def 1;
hence h1 . (o2 . x) =
(id the carrier of U1) . (o1 . p)
by A23, A26, FUNCT_1:13
.=
o1 . (h1 * x)
by A24, A27, FUNCT_1:17
;
verum end;
hence
h1 is_homomorphism
by A5; verum