:: ALTCAT_1 semantic presentation
theorem Th1: :: ALTCAT_1:1
canceled;
theorem Th2: :: ALTCAT_1:2
theorem Th3: :: ALTCAT_1:3
theorem Th4: :: ALTCAT_1:4
theorem Th5: :: ALTCAT_1:5
proof
let c
1, c
2, c
3 be
set ;
assume that E5:
Funcs c
1,c
2 <> {}
and E6:
Funcs c
2,c
3 <> {}
;
consider c
4 being
set such that E7:
c
4 in Funcs c
1,c
2
by E5, XBOOLE_0:def 1;
consider c
5 being
set such that E8:
c
5 in Funcs c
2,c
3
by E6, XBOOLE_0:def 1;
reconsider c
6 = c
4 as
Function of c
1,c
2 by E7, FUNCT_2:121;
reconsider c
7 = c
5 as
Function of c
2,c
3 by E8, FUNCT_2:121;
c
7 * c
6 in Funcs c
1,c
3
by E7, E8, Th4;
hence
Funcs c
1,c
3 <> {}
;
end;
theorem Th6: :: ALTCAT_1:6
canceled;
theorem Th7: :: ALTCAT_1:7
proof
let c
1, c
2 be
set ;
let c
3 be
ManySortedSet of
[:c2,c1:];
let c
4 be
Subset of c
1;
let c
5 be
Subset of c
2;
let c
6, c
7 be
set ;
assume
( c
6 in c
4 & c
7 in c
5 )
;
then E5:
[c7,c6] in [:c5,c4:]
by ZFMISC_1:106;
thus c
3 . c
7,c
6 =
c
3 . [c7,c6]
.=
(c3 | [:c5,c4:]) . [c7,c6]
by E5, FUNCT_1:72
.=
(c3 | [:c5,c4:]) . c
7,c
6
;
end;
scheme :: ALTCAT_1:sch 1
s1{ F
1()
-> set , F
2()
-> set , F
3(
set ,
set )
-> set } :
ex b
1 being
ManySortedSet of
[:F1(),F2():] st
for b
2, b
3 being
set holds
( b
2 in F
1() & b
3 in F
2() implies b
1 . b
2,b
3 = F
3(b
2,b
3) )
proof
deffunc H
1(
set )
-> set = F
3(
(a1 `1 ),
(a1 `2 ));
consider c
1 being
Function such that E5:
dom c
1 = [:F1(),F2():]
and E6:
for b
1 being
set holds
( b
1 in [:F1(),F2():] implies c
1 . b
1 = H
1(b
1) )
from FUNCT_1:sch 3();
reconsider c
2 = c
1 as
ManySortedSet of
[:F1(),F2():] by E5, PBOOLE:def 3;
take
c
2
;
let c
3, c
4 be
set ;
assume
( c
3 in F
1() & c
4 in F
2() )
;
then E7:
[c3,c4] in [:F1(),F2():]
by ZFMISC_1:106;
E8:
(
[c3,c4] `1 = c
3 &
[c3,c4] `2 = c
4 )
by MCART_1:7;
thus c
2 . c
3,c
4 =
c
2 . [c3,c4]
.=
F
3(c
3,c
4)
by E6, E7, E8
;
end;
scheme :: ALTCAT_1:sch 3
s3{ F
1()
-> set , F
2()
-> set , F
3()
-> set , F
4(
set ,
set ,
set )
-> set } :
ex b
1 being
ManySortedSet of
[:F1(),F2(),F3():] st
for b
2, b
3, b
4 being
set holds
( b
2 in F
1() & b
3 in F
2() & b
4 in F
3() implies b
1 . b
2,b
3,b
4 = F
4(b
2,b
3,b
4) )
proof
deffunc H
1(
set )
-> set = F
4(
((a1 `1 ) `1 ),
((a1 `1 ) `2 ),
(a1 `2 ));
consider c
1 being
Function such that E5:
dom c
1 = [:F1(),F2(),F3():]
and E6:
for b
1 being
set holds
( b
1 in [:F1(),F2(),F3():] implies c
1 . b
1 = H
1(b
1) )
from FUNCT_1:sch 3();
reconsider c
2 = c
1 as
ManySortedSet of
[:F1(),F2(),F3():] by E5, PBOOLE:def 3;
take
c
2
;
let c
3, c
4, c
5 be
set ;
assume
( c
3 in F
1() & c
4 in F
2() & c
5 in F
3() )
;
then E7:
[c3,c4,c5] in [:F1(),F2(),F3():]
by MCART_1:73;
(
[c3,c4] `1 = c
3 &
[c3,c4] `2 = c
4 )
by MCART_1:7;
then E8:
(
([[c3,c4],c5] `1 ) `1 = c
3 &
([[c3,c4],c5] `1 ) `2 = c
4 &
[[c3,c4],c5] `2 = c
5 )
by MCART_1:7;
E9:
[c3,c4,c5] = [[c3,c4],c5]
by MCART_1:def 3;
thus c
2 . c
3,c
4,c
5 =
c
2 . [c3,c4,c5]
by MULTOP_1:def 1
.=
F
4(c
3,c
4,c
5)
by E6, E7, E8, E9
;
end;
scheme :: ALTCAT_1:sch 4
s4{ F
1()
-> non
empty set , F
2()
-> non
empty set , F
3()
-> non
empty set , F
4(
set ,
set ,
set )
-> set } :
proof
consider c
1 being
ManySortedSet of
[:F1(),F2(),F3():] such that E5:
for b
1, b
2, b
3 being
set holds
( b
1 in F
1() & b
2 in F
2() & b
3 in F
3() implies c
1 . b
1,b
2,b
3 = F
4(b
1,b
2,b
3) )
from ALTCAT_1:sch 3();
take
c
1
;
thus
for b
1 being
Element of F
1()
for b
2 being
Element of F
2()
for b
3 being
Element of F
3() holds c
1 . b
1,b
2,b
3 = F
4(b
1,b
2,b
3)
by E5;
end;
theorem Th8: :: ALTCAT_1:8
for b
1, b
2 being
set for b
3, b
4 being
ManySortedSet of
[:b1,b2:] holds
( ( for b
5, b
6 being
set holds
( b
5 in b
1 & b
6 in b
2 implies b
3 . b
5,b
6 = b
4 . b
5,b
6 ) ) implies b
4 = b
3 )
theorem Th9: :: ALTCAT_1:9
theorem Th10: :: ALTCAT_1:10
for b
1 being
set for b
2, b
3 being
ManySortedSet of
[:b1,b1,b1:] holds
( ( for b
4, b
5, b
6 being
set holds
( b
4 in b
1 & b
5 in b
1 & b
6 in b
1 implies b
2 . b
4,b
5,b
6 = b
3 . b
4,b
5,b
6 ) ) implies b
3 = b
2 )
proof
let c
1 be
set ;
let c
2, c
3 be
ManySortedSet of
[:c1,c1,c1:];
assume E8:
for b
1, b
2, b
3 being
set holds
( b
1 in c
1 & b
2 in c
1 & b
3 in c
1 implies c
2 . b
1,b
2,b
3 = c
3 . b
1,b
2,b
3 )
;
E9:
(
dom c
3 = [:c1,c1,c1:] &
dom c
2 = [:c1,c1,c1:] )
by PBOOLE:def 3;
now
let c
4 be
set ;
assume E10:
c
4 in [:c1,c1,c1:]
;
then reconsider c
5 = c
1 as non
empty set by MCART_1:35;
consider c
6, c
7, c
8 being
Element of c
5 such that E11:
c
4 = [c6,c7,c8]
by E10, DOMAIN_1:15;
thus c
3 . c
4 =
c
3 . c
6,c
7,c
8
by E11, MULTOP_1:def 1
.=
c
2 . c
6,c
7,c
8
by E8
.=
c
2 . c
4
by E11, MULTOP_1:def 1
;
end;
hence
c
3 = c
2
by E9, FUNCT_1:9;
end;
theorem Th11: :: ALTCAT_1:11
proof
let c
1, c
2, c
3 be
set ;
E9:
{[c1,c2]} = [:{c1},{c2}:]
by ZFMISC_1:35;
(
dom ([c1,c2] .--> c3) = {[c1,c2]} &
rng ([c1,c2] .--> c3) = {c3} )
by CQC_LANG:5;
then
[c1,c2] .--> c
3 is
Function of
[:{c1},{c2}:],
{c3}
by E9, FUNCT_2:def 1, RELSET_1:11;
hence
c
1,c
2 :-> c
3 = [c1,c2] .--> c
3
by FUNCT_2:def 5;
end;
theorem Th12: :: ALTCAT_1:12
for b
1, b
2, b
3 being
set holds
(b1,b2 :-> b3) . b
1,b
2 = b
3
:: deftheorem Def1 ALTCAT_1:def 1 :
canceled;
:: deftheorem Def2 defines <^ ALTCAT_1:def 2 :
:: deftheorem Def3 ALTCAT_1:def 3 :
canceled;
:: deftheorem Def4 defines transitive ALTCAT_1:def 4 :
definition
let c
1 be
set ;
let c
2 be
ManySortedSet of
[:c1,c1:];
func {|c2|} -> ManySortedSet of
[:a1,a1,a1:] means :
Def5:
:: ALTCAT_1:def 5
for b
1, b
2, b
3 being
set holds
( b
1 in a
1 & b
2 in a
1 & b
3 in a
1 implies a
3 . b
1,b
2,b
3 = a
2 . b
1,b
3 );
existence
ex b1 being ManySortedSet of [:c1,c1,c1:] st
for b2, b3, b4 being set holds
( b2 in c1 & b3 in c1 & b4 in c1 implies b1 . b2,b3,b4 = c2 . b2,b4 )
proof
deffunc H
1(
set ,
set ,
set )
-> set = c
2 . a
1,a
3;
ex b
1 being
ManySortedSet of
[:c1,c1,c1:] st
for b
2, b
3, b
4 being
set holds
( b
2 in c
1 & b
3 in c
1 & b
4 in c
1 implies b
1 . b
2,b
3,b
4 = H
1(b
2,b
3,b
4) )
from ALTCAT_1:sch 3();
hence
ex b
1 being
ManySortedSet of
[:c1,c1,c1:] st
for b
2, b
3, b
4 being
set holds
( b
2 in c
1 & b
3 in c
1 & b
4 in c
1 implies b
1 . b
2,b
3,b
4 = c
2 . b
2,b
4 )
;
end;
uniqueness
for b1, b2 being ManySortedSet of [:c1,c1,c1:] holds
( ( for b3, b4, b5 being set holds
( b3 in c1 & b4 in c1 & b5 in c1 implies b1 . b3,b4,b5 = c2 . b3,b5 ) ) & ( for b3, b4, b5 being set holds
( b3 in c1 & b4 in c1 & b5 in c1 implies b2 . b3,b4,b5 = c2 . b3,b5 ) ) implies b1 = b2 )
proof
let c
3, c
4 be
ManySortedSet of
[:c1,c1,c1:];
assume that E11:
for b
1, b
2, b
3 being
set holds
( b
1 in c
1 & b
2 in c
1 & b
3 in c
1 implies c
3 . b
1,b
2,b
3 = c
2 . b
1,b
3 )
and E12:
for b
1, b
2, b
3 being
set holds
( b
1 in c
1 & b
2 in c
1 & b
3 in c
1 implies c
4 . b
1,b
2,b
3 = c
2 . b
1,b
3 )
;
now
let c
5, c
6, c
7 be
set ;
assume E13:
( c
5 in c
1 & c
6 in c
1 & c
7 in c
1 )
;
hence c
3 . c
5,c
6,c
7 =
c
2 . c
5,c
7
by E11
.=
c
4 . c
5,c
6,c
7
by E12, E13
;
end;
hence
c
3 = c
4
by Th10;
end;
let c
3 be
ManySortedSet of
[:c1,c1:];
func {|c2,c3|} -> ManySortedSet of
[:a1,a1,a1:] means :
Def6:
:: ALTCAT_1:def 6
for b
1, b
2, b
3 being
set holds
( b
1 in a
1 & b
2 in a
1 & b
3 in a
1 implies a
4 . b
1,b
2,b
3 = [:(a3 . b2,b3),(a2 . b1,b2):] );
existence
ex b1 being ManySortedSet of [:c1,c1,c1:] st
for b2, b3, b4 being set holds
( b2 in c1 & b3 in c1 & b4 in c1 implies b1 . b2,b3,b4 = [:(c3 . b3,b4),(c2 . b2,b3):] )
proof
deffunc H
1(
set ,
set ,
set )
-> set =
[:(c3 . a2,a3),(c2 . a1,a2):];
ex b
1 being
ManySortedSet of
[:c1,c1,c1:] st
for b
2, b
3, b
4 being
set holds
( b
2 in c
1 & b
3 in c
1 & b
4 in c
1 implies b
1 . b
2,b
3,b
4 = H
1(b
2,b
3,b
4) )
from ALTCAT_1:sch 3();
hence
ex b
1 being
ManySortedSet of
[:c1,c1,c1:] st
for b
2, b
3, b
4 being
set holds
( b
2 in c
1 & b
3 in c
1 & b
4 in c
1 implies b
1 . b
2,b
3,b
4 = [:(c3 . b3,b4),(c2 . b2,b3):] )
;
end;
uniqueness
for b1, b2 being ManySortedSet of [:c1,c1,c1:] holds
( ( for b3, b4, b5 being set holds
( b3 in c1 & b4 in c1 & b5 in c1 implies b1 . b3,b4,b5 = [:(c3 . b4,b5),(c2 . b3,b4):] ) ) & ( for b3, b4, b5 being set holds
( b3 in c1 & b4 in c1 & b5 in c1 implies b2 . b3,b4,b5 = [:(c3 . b4,b5),(c2 . b3,b4):] ) ) implies b1 = b2 )
proof
let c
4, c
5 be
ManySortedSet of
[:c1,c1,c1:];
assume that E11:
for b
1, b
2, b
3 being
set holds
( b
1 in c
1 & b
2 in c
1 & b
3 in c
1 implies c
4 . b
1,b
2,b
3 = [:(c3 . b2,b3),(c2 . b1,b2):] )
and E12:
for b
1, b
2, b
3 being
set holds
( b
1 in c
1 & b
2 in c
1 & b
3 in c
1 implies c
5 . b
1,b
2,b
3 = [:(c3 . b2,b3),(c2 . b1,b2):] )
;
now
let c
6, c
7, c
8 be
set ;
assume E13:
( c
6 in c
1 & c
7 in c
1 & c
8 in c
1 )
;
hence c
4 . c
6,c
7,c
8 =
[:(c3 . c7,c8),(c2 . c6,c7):]
by E11
.=
c
5 . c
6,c
7,c
8
by E12, E13
;
end;
hence
c
4 = c
5
by Th10;
end;
end;
:: deftheorem Def5 defines {| ALTCAT_1:def 5 :
:: deftheorem Def6 defines {| ALTCAT_1:def 6 :
for b
1 being
set for b
2, b
3 being
ManySortedSet of
[:b1,b1:]for b
4 being
ManySortedSet of
[:b1,b1,b1:] holds
( b
4 = {|b2,b3|} iff for b
5, b
6, b
7 being
set holds
( b
5 in b
1 & b
6 in b
1 & b
7 in b
1 implies b
4 . b
5,b
6,b
7 = [:(b3 . b6,b7),(b2 . b5,b6):] ) );
definition
let c
1 be non
empty set ;
let c
2 be
ManySortedSet of
[:c1,c1:];
let c
3 be
BinComp of c
2;
let c
4, c
5, c
6 be
Element of c
1;
redefine func . as c
3 . c
4,c
5,c
6 -> Function of
[:(a2 . a5,a6),(a2 . a4,a5):],a
2 . a
4,a
6;
coherence
c3 . c4,c5,c6 is Function of [:(c2 . c5,c6),(c2 . c4,c5):],c2 . c4,c6
proof
E13:
c
3 . [c4,c5,c6] = c
3 . c
4,c
5,c
6
by MULTOP_1:def 1;
E14:
{|c2,c2|} . [c4,c5,c6] =
{|c2,c2|} . c
4,c
5,c
6
by MULTOP_1:def 1
.=
[:(c2 . c5,c6),(c2 . c4,c5):]
by Def6
;
{|c2|} . [c4,c5,c6] =
{|c2|} . c
4,c
5,c
6
by MULTOP_1:def 1
.=
c
2 . c
4,c
6
by Def5
;
hence
c
3 . c
4,c
5,c
6 is
Function of
[:(c2 . c5,c6),(c2 . c4,c5):],c
2 . c
4,c
6
by E13, E14, PBOOLE:def 18;
end;
end;
definition
let c
1 be non
empty set ;
let c
2 be
ManySortedSet of
[:c1,c1:];
let c
3 be
BinComp of c
2;
attr a
3 is
associative means :
Def7:
:: ALTCAT_1:def 7
for b
1, b
2, b
3, b
4 being
Element of a
1for b
5, b
6, b
7 being
set holds
( b
5 in a
2 . b
1,b
2 & b
6 in a
2 . b
2,b
3 & b
7 in a
2 . b
3,b
4 implies
(a3 . b1,b3,b4) . b
7,
((a3 . b1,b2,b3) . b6,b5) = (a3 . b1,b2,b4) . ((a3 . b2,b3,b4) . b7,b6),b
5 );
attr a
3 is
with_right_units means :
Def8:
:: ALTCAT_1:def 8
for b
1 being
Element of a
1 holds
ex b
2 being
set st
( b
2 in a
2 . b
1,b
1 & ( for b
3 being
Element of a
1for b
4 being
set holds
( b
4 in a
2 . b
1,b
3 implies
(a3 . b1,b1,b3) . b
4,b
2 = b
4 ) ) );
attr a
3 is
with_left_units means :
Def9:
:: ALTCAT_1:def 9
for b
1 being
Element of a
1 holds
ex b
2 being
set st
( b
2 in a
2 . b
1,b
1 & ( for b
3 being
Element of a
1for b
4 being
set holds
( b
4 in a
2 . b
3,b
1 implies
(a3 . b3,b1,b1) . b
2,b
4 = b
4 ) ) );
end;
:: deftheorem Def7 defines associative ALTCAT_1:def 7 :
for b
1 being non
empty set for b
2 being
ManySortedSet of
[:b1,b1:]for b
3 being
BinComp of b
2 holds
( b
3 is
associative iff for b
4, b
5, b
6, b
7 being
Element of b
1for b
8, b
9, b
10 being
set holds
( b
8 in b
2 . b
4,b
5 & b
9 in b
2 . b
5,b
6 & b
10 in b
2 . b
6,b
7 implies
(b3 . b4,b6,b7) . b
10,
((b3 . b4,b5,b6) . b9,b8) = (b3 . b4,b5,b7) . ((b3 . b5,b6,b7) . b10,b9),b
8 ) );
:: deftheorem Def8 defines with_right_units ALTCAT_1:def 8 :
:: deftheorem Def9 defines with_left_units ALTCAT_1:def 9 :
definition
let c
1 be non
empty AltCatStr ;
let c
2, c
3, c
4 be
object of c
1;
assume E16:
(
<^c2,c3^> <> {} &
<^c3,c4^> <> {} )
;
let c
5 be
Morphism of c
2,c
3;
let c
6 be
Morphism of c
3,c
4;
func c
6 * c
5 -> Morphism of a
2,a
4 equals :
Def10:
:: ALTCAT_1:def 10
(the Comp of a1 . a2,a3,a4) . a
6,a
5;
coherence
(the Comp of c1 . c2,c3,c4) . c6,c5 is Morphism of c2,c4
proof
reconsider c
7 =
<^c2,c3^>, c
8 =
<^c3,c4^> as non
empty set by E16;
reconsider c
9 = the
Comp of c
1 . c
2,c
3,c
4 as
Function of
[:c8,c7:],
<^c2,c4^> ;
reconsider c
10 = c
6 as
Element of c
8 ;
reconsider c
11 = c
5 as
Element of c
7 ;
c
9 . c
10,c
11 is
Element of
<^c2,c4^>
;
hence
(the Comp of c1 . c2,c3,c4) . c
6,c
5 is
Morphism of c
2,c
4
;
end;
correctness
;
end;
:: deftheorem Def10 defines * ALTCAT_1:def 10 :
:: deftheorem Def11 defines compositional ALTCAT_1:def 11 :
registration
let c
1, c
2 be
functional set ;
cluster compositional ManySortedSet of
[:a1,a2:];
existence
ex b1 being ManySortedFunction of [:c1,c2:] st b1 is compositional
proof
per cases
not ( not c1 = {} & not c2 = {} & not ( c1 <> {} & c2 <> {} ) )
;
suppose E18:
( c
1 = {} or c
2 = {} )
;
set c
3 =
[0] [:c1,c2:];
E19:
dom ([0] [:c1,c2:]) = [:c1,c2:]
by PBOOLE:def 3;
[0] [:c1,c2:] is
Function-yielding
then reconsider c
4 =
[0] [:c1,c2:] as
ManySortedFunction of
[:c1,c2:] ;
take
c
4
;
let c
5 be
set ;
:: according to ALTCAT_1:def 11thus
not ( c
5 in dom c
4 & ( for b
1, b
2 being
Function holds
not ( c
5 = [b2,b1] & c
4 . c
5 = b
2 * b
1 ) ) )
by E18, E19, ZFMISC_1:113;
end;
suppose
( c
1 <> {} & c
2 <> {} )
;
then reconsider c
3 = c
1, c
4 = c
2 as non
empty functional set ;
deffunc H
1(
Element of c
3,
Element of c
4)
-> set = a
1 * a
2;
consider c
5 being
ManySortedSet of
[:c3,c4:] such that E18:
for b
1 being
Element of c
3for b
2 being
Element of c
4 holds c
5 . b
1,b
2 = H
1(b
1,b
2)
from ALTCAT_1:sch 2();
c
5 is
Function-yielding
then reconsider c
6 = c
5 as
ManySortedFunction of
[:c1,c2:] ;
take
c
6
;
let c
7 be
set ;
:: according to ALTCAT_1:def 11assume
c
7 in dom c
6
;
then E19:
c
7 in [:c3,c4:]
by PBOOLE:def 3;
then E20:
( c
7 `1 in c
3 & c
7 `2 in c
4 )
by MCART_1:10;
then reconsider c
8 = c
7 `1 , c
9 = c
7 `2 as
Function by FRAENKEL:def 1;
take
c
9
;
take
c
8
;
thus
c
7 = [c8,c9]
by E19, MCART_1:24;
c
7 = [c8,c9]
by E19, MCART_1:24;
hence c
6 . c
7 =
c
6 . c
8,c
9
.=
c
8 * c
9
by E18, E20
;
end;
end;
end;
end;
theorem Th13: :: ALTCAT_1:13
proof
let c
1, c
2 be
functional set ;
let c
3 be
compositional ManySortedSet of
[:c1,c2:];
let c
4, c
5 be
Function;
assume E19:
( c
4 in c
1 & c
5 in c
2 )
;
dom c
3 = [:c1,c2:]
by PBOOLE:def 3;
then
[c4,c5] in dom c
3
by E19, ZFMISC_1:106;
then consider c
6, c
7 being
Function such that E20:
[c4,c5] = [c7,c6]
and E21:
c
3 . [c4,c5] = c
7 * c
6
by Def11;
( c
4 = c
7 & c
5 = c
6 )
by E20, ZFMISC_1:33;
hence
c
3 . c
4,c
5 = c
4 * c
5
by E21;
end;