begin
:: deftheorem Def1 defines id MSUALG_3:def 1 :
:: deftheorem Def2 defines "1-1" MSUALG_3:def 2 :
theorem Th1:
:: deftheorem Def3 defines "onto" MSUALG_3:def 3 :
theorem Th2:
theorem
theorem Th4:
:: deftheorem MSUALG_3:def 4 :
canceled;
:: deftheorem Def5 defines "" MSUALG_3:def 5 :
theorem Th5:
begin
theorem Th6:
:: deftheorem MSUALG_3:def 6 :
canceled;
:: deftheorem Def7 defines # MSUALG_3:def 7 :
Lm1:
now
let S be non
empty non
void ManySortedSign ;
for U1, U2 being MSAlgebra of S
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1
for f, u being Function st x = f & x in Args o,U1 & u in Args o,U2 holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )let U1,
U2 be
MSAlgebra of
S;
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1
for f, u being Function st x = f & x in Args o,U1 & u in Args o,U2 holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )let o be
OperSymbol of
S;
for F being ManySortedFunction of U1,U2
for x being Element of Args o,U1
for f, u being Function st x = f & x in Args o,U1 & u in Args o,U2 holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )let F be
ManySortedFunction of
U1,
U2;
for x being Element of Args o,U1
for f, u being Function st x = f & x in Args o,U1 & u in Args o,U2 holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )let x be
Element of
Args o,
U1;
for f, u being Function st x = f & x in Args o,U1 & u in Args o,U2 holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )let f,
u be
Function;
( x = f & x in Args o,U1 & u in Args o,U2 implies ( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) )assume that A1:
x = f
and A2:
x in Args o,
U1
and A3:
u in Args o,
U2
;
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )A4:
rng (the_arity_of o) c= the
carrier of
S
by FINSEQ_1:def 4;
then A5:
rng (the_arity_of o) c= dom the
Sorts of
U1
by PARTFUN1:def 4;
A6:
F # x = (Frege (F * (the_arity_of o))) . x
by A2, A3, Def7;
A7:
dom (the Sorts of U1 * (the_arity_of o)) = (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))
A12:
Args o,
U2 = product (the Sorts of U2 * (the_arity_of o))
by PRALG_2:10;
then A13:
dom u = dom (the Sorts of U2 * (the_arity_of o))
by A3, CARD_3:18;
A14:
Args o,
U1 = product (the Sorts of U1 * (the_arity_of o))
by PRALG_2:10;
then A15:
dom f =
dom (the Sorts of U1 * (the_arity_of o))
by A1, A2, CARD_3:18
.=
dom (the_arity_of o)
by A5, RELAT_1:46
;
rng (the_arity_of o) c= dom the
Sorts of
U2
by A4, PARTFUN1:def 4;
then A16:
dom u = dom (the_arity_of o)
by A13, RELAT_1:46;
now
let e be
set ;
( e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) implies (the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e) )assume
e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))
;
(the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e)then
e in dom (F * (the_arity_of o))
by FUNCT_6:28;
then A17:
e in dom (the_arity_of o)
by FUNCT_1:21;
then reconsider Foe =
F . ((the_arity_of o) . e) as
Function of
(the Sorts of U1 . ((the_arity_of o) . e)),
(the Sorts of U2 . ((the_arity_of o) . e)) by FINSEQ_2:13, PBOOLE:def 18;
(the Sorts of U2 * (the_arity_of o)) . e in rng (the Sorts of U2 * (the_arity_of o))
by A13, A16, A17, FUNCT_1:def 5;
then A18:
(the Sorts of U2 * (the_arity_of o)) . e <> {}
by A3, A12, CARD_3:37;
(
(the Sorts of U1 * (the_arity_of o)) . e = the
Sorts of
U1 . ((the_arity_of o) . e) &
(the Sorts of U2 * (the_arity_of o)) . e = the
Sorts of
U2 . ((the_arity_of o) . e) )
by A17, FUNCT_1:23;
hence (the Sorts of U1 * (the_arity_of o)) . e =
dom Foe
by A18, FUNCT_2:def 1
.=
proj1 Foe
.=
proj1 ((F * (the_arity_of o)) . e)
by A17, FUNCT_1:23
;
verumreconsider f =
e as
Element of
NAT by A17;
end;
then A19:
the
Sorts of
U1 * (the_arity_of o) = doms (F * (the_arity_of o))
by A7, FUNCT_6:def 2;
hereby ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x )
assume
u = F # x
;
for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n)then A20:
u = (Frege (F * (the_arity_of o))) . x
by A2, A3, Def7;
let n be
Nat;
( n in dom f implies u . n = (F . ((the_arity_of o) /. n)) . (f . n) )assume A21:
n in dom f
;
u . n = (F . ((the_arity_of o) /. n)) . (f . n)then
(the_arity_of o) . n in the
carrier of
S
by A15, FINSEQ_2:13;
then
(the_arity_of o) . n in dom F
by PARTFUN1:def 4;
then A22:
n in dom (F * (the_arity_of o))
by A15, A21, FUNCT_1:21;
then A23:
(F * (the_arity_of o)) . n =
F . ((the_arity_of o) . n)
by FUNCT_1:22
.=
F . ((the_arity_of o) /. n)
by A15, A21, PARTFUN1:def 8
;
thus u . n =
((F * (the_arity_of o)) .. f) . n
by A1, A2, A14, A19, A20, PRALG_2:def 8
.=
(F . ((the_arity_of o) /. n)) . (f . n)
by A22, A23, PRALG_1:def 17
;
verum
end;
F # x is
Element of
product (the Sorts of U2 * (the_arity_of o))
by PRALG_2:10;
then reconsider g =
F # x as
Function ;
A24:
rng (the_arity_of o) c= dom F
by A4, PARTFUN1:def 4;
assume A25:
for
n being
Nat st
n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n)
;
u = F # x
A26:
now
let e be
set ;
( e in dom f implies u . e = g . e )assume A27:
e in dom f
;
u . e = g . ethen reconsider n =
e as
Nat by A15;
(the_arity_of o) . n in the
carrier of
S
by A15, A27, FINSEQ_2:13;
then
(the_arity_of o) . n in dom F
by PARTFUN1:def 4;
then A28:
n in dom (F * (the_arity_of o))
by A15, A27, FUNCT_1:21;
then A29:
(F * (the_arity_of o)) . n =
F . ((the_arity_of o) . n)
by FUNCT_1:22
.=
F . ((the_arity_of o) /. n)
by A15, A27, PARTFUN1:def 8
;
thus u . e =
(F . ((the_arity_of o) /. n)) . (f . n)
by A25, A27
.=
((F * (the_arity_of o)) .. f) . n
by A28, A29, PRALG_1:def 17
.=
g . e
by A1, A2, A14, A19, A6, PRALG_2:def 8
;
verum
end;
F # x = (F * (the_arity_of o)) .. f
by A1, A2, A14, A19, A6, PRALG_2:def 8;
then dom g =
dom (F * (the_arity_of o))
by PRALG_1:def 17
.=
dom f
by A15, A24, RELAT_1:46
;
hence
u = F # x
by A15, A16, A26, FUNCT_1:9;
verum
end;
:: deftheorem Def8 defines # MSUALG_3:def 8 :
theorem Th7:
theorem Th8:
:: deftheorem Def9 defines is_homomorphism MSUALG_3:def 9 :
theorem Th9:
theorem Th10:
:: deftheorem Def10 defines is_epimorphism MSUALG_3:def 10 :
theorem Th11:
:: deftheorem Def11 defines is_monomorphism MSUALG_3:def 11 :
theorem Th12:
:: deftheorem Def12 defines is_isomorphism MSUALG_3:def 12 :
theorem Th13:
Lm2:
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds
H "" is_homomorphism U2,U1
theorem Th14:
theorem Th15:
:: deftheorem Def13 defines are_isomorphic MSUALG_3:def 13 :
theorem Th16:
theorem
theorem
:: deftheorem Def14 defines Image MSUALG_3:def 14 :
theorem
Lm3:
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
F is ManySortedFunction of U1,(Image F)
theorem Th20:
theorem
Lm4:
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for U3 being non-empty MSSubAlgebra of U2
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds
F is_homomorphism U1,U2
theorem Th22:
theorem
theorem