let U1, U2 be Universal_Algebra; :: thesis: ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies for B being non empty Subset of U2 st B = the carrier of U1 holds
B is opers_closed )
set MU1 = MSAlg U1;
set MU2 = MSAlg U2;
assume A1:
MSAlg U1 is MSSubAlgebra of MSAlg U2
; :: thesis: for B being non empty Subset of U2 st B = the carrier of U1 holds
B is opers_closed
then reconsider MU1 = MSAlg U1 as MSAlgebra of MSSign U2 ;
A2:
MU1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #)
by MSUALG_1:def 16;
A3:
MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #)
by MSUALG_1:def 16;
set gg1 = (*--> 0 ) * (signature U2);
set gg2 = (dom (signature U2)) --> z;
reconsider gg1 = (*--> 0 ) * (signature U2) as Function of (dom (signature U2)),({0 } * ) by MSUALG_1:7;
A4:
MSSign U2 = ManySortedSign(# {0 },(dom (signature U2)),gg1,((dom (signature U2)) --> z) #)
by MSUALG_1:16;
reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A1, MSUALG_2:def 10;
let B be non empty Subset of U2; :: thesis: ( B = the carrier of U1 implies B is opers_closed )
assume A5:
B = the carrier of U1
; :: thesis: B is opers_closed
A6:
( C is opers_closed & the Charact of MU1 = Opers (MSAlg U2),C )
by A1, MSUALG_2:def 10;
let o be operation of U2; :: according to UNIALG_2:def 5 :: thesis: B is_closed_on o
thus
B is_closed_on o
:: thesis: verumproof
let s be
FinSequence of
B;
:: according to UNIALG_2:def 4 :: thesis: ( not len s = arity o or o . s in B )
assume A7:
len s = arity o
;
:: thesis: o . s in B
consider n being
set such that A8:
(
n in dom the
charact of
U2 &
o = the
charact of
U2 . n )
by FUNCT_1:def 5;
A9:
(
dom the
charact of
U2 = Seg (len the charact of U2) &
dom (signature U2) = Seg (len (signature U2)) )
by FINSEQ_1:def 3;
then A10:
n in dom (signature U2)
by A8, UNIALG_1:def 11;
reconsider n =
n as
OperSymbol of
(MSSign U2) by A4, A8, A9, UNIALG_1:def 11;
C is_closed_on n
by A6, MSUALG_2:def 7;
then A12:
rng ((Den n,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . n)) c= (C * the ResultSort of (MSSign U2)) . n
by MSUALG_2:def 6;
A13:
o . s in rng ((Den n,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . n))
proof
ex
y being
set st
(
y in dom ((Den n,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . n)) &
((Den n,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . n)) . y = o . s )
proof
take
s
;
:: thesis: ( s in dom ((Den n,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . n)) & ((Den n,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . n)) . s = o . s )
thus
s in dom ((Den n,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . n))
:: thesis: ((Den n,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . n)) . s = o . sproof
A14:
dom the
Arity of
(MSSign U2) = the
carrier' of
(MSSign U2)
by FUNCT_2:def 1;
dom (Den n,(MSAlg U2)) = Args n,
(MSAlg U2)
by FUNCT_2:def 1;
then A15:
dom (Den n,(MSAlg U2)) =
((the Sorts of (MSAlg U2) # ) * the Arity of (MSSign U2)) . n
by MSUALG_1:def 9
.=
(the Sorts of (MSAlg U2) # ) . (((*--> 0 ) * (signature U2)) . n)
by A4, A14, FUNCT_1:23
.=
(the Sorts of (MSAlg U2) # ) . ((*--> 0 ) . ((signature U2) . n))
by A10, FUNCT_1:23
.=
(the Sorts of (MSAlg U2) # ) . ((*--> 0 ) . (arity o))
by A8, A10, UNIALG_1:def 11
.=
(the Sorts of (MSAlg U2) # ) . ((arity o) |-> 0 )
by PBOOLE:def 20
;
(
Seg (arity o) <> {} implies (
dom ((arity o) |-> 0 ) = Seg (arity o) &
rng ((arity o) |-> 0 ) c= the
carrier of
(MSSign U2) ) )
by A4, FUNCOP_1:19;
then
(arity o) |-> 0 is
FinSequence of the
carrier of
(MSSign U2)
by A16, FINSEQ_1:def 4;
then reconsider aro =
(arity o) |-> 0 as
Element of the
carrier of
(MSSign U2) * by FINSEQ_1:def 11;
A17:
dom (Den n,(MSAlg U2)) = product (the Sorts of (MSAlg U2) * aro)
by A15, PBOOLE:def 19;
A18:
dom s = dom (the Sorts of (MSAlg U2) * aro)
for
x being
set st
x in dom (the Sorts of (MSAlg U2) * aro) holds
s . x in (the Sorts of (MSAlg U2) * aro) . x
then A25:
s in dom (Den n,(MSAlg U2))
by A17, A18, CARD_3:def 5;
A26:
(
s is
Element of
(len s) -tuples_on B & not
(len s) -tuples_on B is
empty )
by FINSEQ_2:110;
A27:
(
n in dom (signature U2) &
(signature U2) . n in dom (*--> 0 ) )
then A29:
n in dom ((*--> 0 ) * (signature U2))
by FUNCT_1:21;
then A30:
((C # ) * the Arity of (MSSign U2)) . n =
(C # ) . (((*--> 0 ) * (signature U2)) . n)
by A4, FUNCT_1:23
.=
(C # ) . ((*--> 0 ) . ((signature U2) . n))
by A29, FUNCT_1:22
.=
(C # ) . ((*--> 0 ) . (arity o))
by A8, A27, UNIALG_1:def 11
.=
(C # ) . ((arity o) |-> 0 )
by PBOOLE:def 20
;
(arity o) |-> 0 is
FinSequence of the
carrier of
(MSSign U2)
by A4, FINSEQ_2:77;
then reconsider ao0 =
(arity o) |-> 0 as
Element of the
carrier of
(MSSign U2) * by FINSEQ_1:def 11;
A31:
C = 0 .--> the
carrier of
U1
by A2, MSUALG_1:def 14;
then
dom C = {0 }
by FUNCOP_1:19;
then A32:
0 in dom C
by TARSKI:def 1;
A33:
0 in {0 }
by TARSKI:def 1;
((C # ) * the Arity of (MSSign U2)) . n =
product (C * ao0)
by A30, PBOOLE:def 19
.=
product ((Seg (arity o)) --> (C . 0 ))
by A32, FUNCOP_1:23
.=
product ((Seg (arity o)) --> B)
by A5, A31, A33, FUNCOP_1:13
.=
Funcs (Seg (arity o)),
B
by CARD_3:20
.=
(arity o) -tuples_on B
by FINSEQ_2:111
;
then
s in (dom (Den n,(MSAlg U2))) /\ (((C # ) * the Arity of (MSSign U2)) . n)
by A7, A25, A26, XBOOLE_0:def 4;
hence
s in dom ((Den n,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . n))
by RELAT_1:90;
:: thesis: verum
end;
hence ((Den n,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . n)) . s =
(Den n,(MSAlg U2)) . s
by FUNCT_1:70
.=
((MSCharact U2) . n) . s
by A3, MSUALG_1:def 11
.=
o . s
by A8, MSUALG_1:def 15
;
:: thesis: verum
end;
hence
o . s in rng ((Den n,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . n))
by FUNCT_1:def 5;
:: thesis: verum
end;
A34:
0 in {0 }
by TARSKI:def 1;
n in dom ((dom (signature U2)) --> 0 )
by A10, FUNCOP_1:19;
then (C * the ResultSort of (MSSign U2)) . n =
C . (((dom (signature U2)) --> 0 ) . n)
by A4, FUNCT_1:23
.=
the
Sorts of
MU1 . 0
by A10, FUNCOP_1:13
.=
(0 .--> the carrier of U1) . 0
by A2, MSUALG_1:def 14
.=
B
by A5, A34, FUNCOP_1:13
;
hence
o . s in B
by A12, A13;
:: thesis: verum
end;