:: MSUALG_5 semantic presentation
begin
definition
let X be set ;
let R be Relation of X;
func EqCl R -> Equivalence_Relation of X means :Def1: :: MSUALG_5:def 1
( R c= it & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
it c= EqR2 ) );
existence
ex b1 being Equivalence_Relation of X st
( R c= b1 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b1 c= EqR2 ) ) by EQREL_1:12;
uniqueness
for b1, b2 being Equivalence_Relation of X st R c= b1 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b1 c= EqR2 ) & R c= b2 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b2 c= EqR2 ) holds
b1 = b2
proof
let C1, C2 be Equivalence_Relation of X; ::_thesis: ( R c= C1 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
C1 c= EqR2 ) & R c= C2 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
C2 c= EqR2 ) implies C1 = C2 )
assume that
A1: R c= C1 and
A2: for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
C1 c= EqR2 and
A3: R c= C2 and
A4: for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
C2 c= EqR2 ; ::_thesis: C1 = C2
A5: C2 c= C1 by A1, A4;
C1 c= C2 by A2, A3;
hence C1 = C2 by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines EqCl MSUALG_5:def_1_:_
for X being set
for R being Relation of X
for b3 being Equivalence_Relation of X holds
( b3 = EqCl R iff ( R c= b3 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b3 c= EqR2 ) ) );
theorem Th1: :: MSUALG_5:1
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2)
proof
let X be set ; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2)
let EqR1, EqR2 be Equivalence_Relation of X; ::_thesis: EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2)
A1: for EqR3 being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR3 holds
EqR1 "\/" EqR2 c= EqR3 by EQREL_1:def_2;
EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by EQREL_1:def_2;
hence EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2) by A1, Def1; ::_thesis: verum
end;
theorem Th2: :: MSUALG_5:2
for X being set
for EqR1 being Equivalence_Relation of X holds EqCl EqR1 = EqR1
proof
let X be set ; ::_thesis: for EqR1 being Equivalence_Relation of X holds EqCl EqR1 = EqR1
let EqR1 be Equivalence_Relation of X; ::_thesis: EqCl EqR1 = EqR1
for EqR2 being Equivalence_Relation of X st EqR1 c= EqR2 holds
EqR1 c= EqR2 ;
hence EqCl EqR1 = EqR1 by Def1; ::_thesis: verum
end;
begin
definition
let X be set ;
func EqRelLatt X -> strict Lattice means :Def2: :: MSUALG_5:def 2
( the carrier of it = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of it . (x,y) = x /\ y & the L_join of it . (x,y) = x "\/" y ) ) );
existence
ex b1 being strict Lattice st
( the carrier of b1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) )
proof
set B = { x where x is Relation of X,X : x is Equivalence_Relation of X } ;
id X in { x where x is Relation of X,X : x is Equivalence_Relation of X } ;
then reconsider B = { x where x is Relation of X,X : x is Equivalence_Relation of X } as non empty set ;
defpred S1[ Element of B, Element of B, Element of B] means ( $1 \/ $2 c= $3 & ( for x9 being Element of B st $1 \/ $2 c= x9 holds
$3 c= x9 ) );
A1: for x, y being Element of B ex z being Element of B st S1[x,y,z]
proof
let x, y be Element of B; ::_thesis: ex z being Element of B st S1[x,y,z]
y in B ;
then A2: ex y99 being Relation of X,X st
( y = y99 & y99 is Equivalence_Relation of X ) ;
x in B ;
then ex x99 being Relation of X,X st
( x = x99 & x99 is Equivalence_Relation of X ) ;
then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A2;
consider z being Equivalence_Relation of X such that
A3: x1 \/ y1 c= z and
A4: for x9 being Equivalence_Relation of X st x1 \/ y1 c= x9 holds
z c= x9 by EQREL_1:12;
z in B ;
then reconsider z9 = z as Element of B ;
take z9 ; ::_thesis: S1[x,y,z9]
thus x \/ y c= z9 by A3; ::_thesis: for x9 being Element of B st x \/ y c= x9 holds
z9 c= x9
hereby ::_thesis: verum
let x9 be Element of B; ::_thesis: ( x \/ y c= x9 implies z9 c= x9 )
assume A5: x \/ y c= x9 ; ::_thesis: z9 c= x9
x9 in B ;
then ex x99 being Relation of X,X st
( x9 = x99 & x99 is Equivalence_Relation of X ) ;
then reconsider x19 = x9 as Equivalence_Relation of X ;
x \/ y c= x19 by A5;
hence z9 c= x9 by A4; ::_thesis: verum
end;
end;
consider B1 being BinOp of B such that
A6: for x, y being Element of B holds S1[x,y,B1 . (x,y)] from BINOP_1:sch_3(A1);
defpred S2[ Element of B, Element of B, Element of B] means $3 = $1 /\ $2;
A7: for x, y being Element of B ex z being Element of B st S2[x,y,z]
proof
let x, y be Element of B; ::_thesis: ex z being Element of B st S2[x,y,z]
y in B ;
then A8: ex y1 being Relation of X,X st
( y = y1 & y1 is Equivalence_Relation of X ) ;
x in B ;
then ex x1 being Relation of X,X st
( x = x1 & x1 is Equivalence_Relation of X ) ;
then reconsider x9 = x, y9 = y as Equivalence_Relation of X by A8;
set z = x9 /\ y9;
x9 /\ y9 in B ;
then reconsider z = x9 /\ y9 as Element of B ;
take z ; ::_thesis: S2[x,y,z]
thus S2[x,y,z] ; ::_thesis: verum
end;
consider B2 being BinOp of B such that
A9: for x, y being Element of B holds S2[x,y,B2 . (x,y)] from BINOP_1:sch_3(A7);
reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;
A10: now__::_thesis:_for_x,_y_being_Equivalence_Relation_of_X_holds_B1_._(x,y)_=_x_"\/"_y
let x, y be Equivalence_Relation of X; ::_thesis: B1 . (x,y) = x "\/" y
A11: y in B ;
x in B ;
then reconsider x1 = x, y1 = y as Element of B by A11;
reconsider B19 = B1 . (x1,y1) as Element of B ;
B19 in B ;
then ex B199 being Relation of X,X st
( B19 = B199 & B199 is Equivalence_Relation of X ) ;
then reconsider B19 = B19 as Equivalence_Relation of X ;
A12: for x9 being Element of B st x1 \/ y1 c= x9 holds
B1 . (x1,y1) c= x9 by A6;
A13: now__::_thesis:_for_x9_being_Equivalence_Relation_of_X_st_x_\/_y_c=_x9_holds_
B1_._(x,y)_c=_x9
let x9 be Equivalence_Relation of X; ::_thesis: ( x \/ y c= x9 implies B1 . (x,y) c= x9 )
assume A14: x \/ y c= x9 ; ::_thesis: B1 . (x,y) c= x9
x9 in B ;
then reconsider x19 = x9 as Element of B ;
x \/ y c= x19 by A14;
hence B1 . (x,y) c= x9 by A12; ::_thesis: verum
end;
x1 \/ y1 c= B1 . (x1,y1) by A6;
then B19 = x "\/" y by A13, EQREL_1:def_2;
hence B1 . (x,y) = x "\/" y ; ::_thesis: verum
end;
A15: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B1_._(a,(B1_._(b,c)))_=_B1_._((B1_._(a,b)),c)
let a, b, c be Element of B; ::_thesis: B1 . (a,(B1 . (b,c))) = B1 . ((B1 . (a,b)),c)
b in B ;
then A16: ex x2 being Relation of X,X st
( b = x2 & x2 is Equivalence_Relation of X ) ;
c in B ;
then A17: ex x3 being Relation of X,X st
( c = x3 & x3 is Equivalence_Relation of X ) ;
a in B ;
then ex x1 being Relation of X,X st
( a = x1 & x1 is Equivalence_Relation of X ) ;
then reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of X by A16, A17;
thus B1 . (a,(B1 . (b,c))) = B1 . (a,(U2 "\/" U3)) by A10
.= U1 "\/" (U2 "\/" U3) by A10
.= (U1 "\/" U2) "\/" U3 by EQREL_1:13
.= B1 . ((U1 "\/" U2),c) by A10
.= B1 . ((B1 . (a,b)),c) by A10 ; ::_thesis: verum
end;
A18: for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider x = a, y = b, z = c as Element of B ;
A19: the L_join of L . (a,b) = a "\/" b by LATTICES:def_1;
thus a "\/" (b "\/" c) = the L_join of L . (a,(b "\/" c)) by LATTICES:def_1
.= B1 . (x,(B1 . (y,z))) by LATTICES:def_1
.= the L_join of L . (( the L_join of L . (a,b)),c) by A15
.= (a "\/" b) "\/" c by A19, LATTICES:def_1 ; ::_thesis: verum
end;
A20: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B1_._(a,b)_=_B1_._(b,a)
let a, b be Element of B; ::_thesis: B1 . (a,b) = B1 . (b,a)
b in B ;
then A21: ex x2 being Relation of X,X st
( b = x2 & x2 is Equivalence_Relation of X ) ;
a in B ;
then ex x1 being Relation of X,X st
( a = x1 & x1 is Equivalence_Relation of X ) ;
then reconsider U1 = a, U2 = b as Equivalence_Relation of X by A21;
thus B1 . (a,b) = U2 "\/" U1 by A10
.= B1 . (b,a) by A10 ; ::_thesis: verum
end;
A22: for a, b being Element of L holds a "\/" b = b "\/" a
proof
let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a
reconsider x = a, y = b as Element of B ;
thus a "\/" b = B1 . (x,y) by LATTICES:def_1
.= the L_join of L . (b,a) by A20
.= b "\/" a by LATTICES:def_1 ; ::_thesis: verum
end;
A23: now__::_thesis:_for_x,_y_being_Equivalence_Relation_of_X_holds_B2_._(x,y)_=_x_/\_y
let x, y be Equivalence_Relation of X; ::_thesis: B2 . (x,y) = x /\ y
A24: y in B ;
x in B ;
then reconsider x9 = x, y9 = y as Element of B by A24;
B2 . (x9,y9) = x9 /\ y9 by A9;
hence B2 . (x,y) = x /\ y ; ::_thesis: verum
end;
A25: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B2_._(a,(B2_._(b,c)))_=_B2_._((B2_._(a,b)),c)
let a, b, c be Element of B; ::_thesis: B2 . (a,(B2 . (b,c))) = B2 . ((B2 . (a,b)),c)
b in B ;
then A26: ex x2 being Relation of X,X st
( b = x2 & x2 is Equivalence_Relation of X ) ;
c in B ;
then A27: ex x3 being Relation of X,X st
( c = x3 & x3 is Equivalence_Relation of X ) ;
a in B ;
then ex x1 being Relation of X,X st
( a = x1 & x1 is Equivalence_Relation of X ) ;
then reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of X by A26, A27;
thus B2 . (a,(B2 . (b,c))) = B2 . (a,(U2 /\ U3)) by A23
.= U1 /\ (U2 /\ U3) by A23
.= (U1 /\ U2) /\ U3 by XBOOLE_1:16
.= B2 . ((U1 /\ U2),c) by A23
.= B2 . ((B2 . (a,b)),c) by A23 ; ::_thesis: verum
end;
A28: for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider x = a, y = b, z = c as Element of B ;
A29: the L_meet of L . (a,b) = a "/\" b by LATTICES:def_2;
thus a "/\" (b "/\" c) = the L_meet of L . (a,(b "/\" c)) by LATTICES:def_2
.= B2 . (x,(B2 . (y,z))) by LATTICES:def_2
.= the L_meet of L . (( the L_meet of L . (a,b)),c) by A25
.= (a "/\" b) "/\" c by A29, LATTICES:def_2 ; ::_thesis: verum
end;
A30: for a, b being Element of L holds a "/\" (a "\/" b) = a
proof
let a, b be Element of L; ::_thesis: a "/\" (a "\/" b) = a
reconsider x = a, y = b as Element of B ;
A31: B2 . (x,(B1 . (x,y))) = x
proof
y in B ;
then A32: ex x2 being Relation of X,X st
( y = x2 & x2 is Equivalence_Relation of X ) ;
x in B ;
then ex x1 being Relation of X,X st
( x = x1 & x1 is Equivalence_Relation of X ) ;
then reconsider U1 = x, U2 = y as Equivalence_Relation of X by A32;
B1 . (x,y) = U1 "\/" U2 by A10;
hence B2 . (x,(B1 . (x,y))) = U1 /\ (U1 "\/" U2) by A23
.= x by EQREL_1:16 ;
::_thesis: verum
end;
thus a "/\" (a "\/" b) = the L_meet of L . (a,(a "\/" b)) by LATTICES:def_2
.= a by A31, LATTICES:def_1 ; ::_thesis: verum
end;
A33: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B2_._(a,b)_=_B2_._(b,a)
let a, b be Element of B; ::_thesis: B2 . (a,b) = B2 . (b,a)
b in B ;
then A34: ex x2 being Relation of X,X st
( b = x2 & x2 is Equivalence_Relation of X ) ;
a in B ;
then ex x1 being Relation of X,X st
( a = x1 & x1 is Equivalence_Relation of X ) ;
then reconsider U1 = a, U2 = b as Equivalence_Relation of X by A34;
thus B2 . (a,b) = U2 /\ U1 by A23
.= B2 . (b,a) by A23 ; ::_thesis: verum
end;
A35: for a, b being Element of L holds a "/\" b = b "/\" a
proof
let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a
reconsider x = a, y = b as Element of B ;
thus a "/\" b = B2 . (x,y) by LATTICES:def_2
.= the L_meet of L . (b,a) by A33
.= b "/\" a by LATTICES:def_2 ; ::_thesis: verum
end;
for a, b being Element of L holds (a "/\" b) "\/" b = b
proof
let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b
reconsider x = a, y = b as Element of B ;
A36: B1 . ((B2 . (x,y)),y) = y
proof
y in B ;
then A37: ex x2 being Relation of X,X st
( y = x2 & x2 is Equivalence_Relation of X ) ;
x in B ;
then ex x1 being Relation of X,X st
( x = x1 & x1 is Equivalence_Relation of X ) ;
then reconsider U1 = x, U2 = y as Equivalence_Relation of X by A37;
B2 . (x,y) = U1 /\ U2 by A23;
hence B1 . ((B2 . (x,y)),y) = U2 "\/" (U1 /\ U2) by A10
.= y by EQREL_1:17 ;
::_thesis: verum
end;
thus (a "/\" b) "\/" b = the L_join of L . ((a "/\" b),b) by LATTICES:def_1
.= b by A36, LATTICES:def_2 ; ::_thesis: verum
end;
then ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by A22, A18, A35, A28, A30, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
then reconsider L = L as strict Lattice ;
take L ; ::_thesis: ( the carrier of L = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y ) ) )
thus the carrier of L = { x where x is Relation of X,X : x is Equivalence_Relation of X } ; ::_thesis: for x, y being Equivalence_Relation of X holds
( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y )
thus for x, y being Equivalence_Relation of X holds
( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y ) by A10, A23; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Lattice st the carrier of b1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) & the carrier of b2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) holds
b1 = b2
proof
let P1, P2 be strict Lattice; ::_thesis: ( the carrier of P1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of P1 . (x,y) = x /\ y & the L_join of P1 . (x,y) = x "\/" y ) ) & the carrier of P2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of P2 . (x,y) = x /\ y & the L_join of P2 . (x,y) = x "\/" y ) ) implies P1 = P2 )
assume that
A38: the carrier of P1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } and
A39: for x, y being Equivalence_Relation of X holds
( the L_meet of P1 . (x,y) = x /\ y & the L_join of P1 . (x,y) = x "\/" y ) and
A40: the carrier of P2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } and
A41: for x, y being Equivalence_Relation of X holds
( the L_meet of P2 . (x,y) = x /\ y & the L_join of P2 . (x,y) = x "\/" y ) ; ::_thesis: P1 = P2
reconsider Z = the carrier of P1 as non empty set ;
now__::_thesis:_for_x,_y_being_Element_of_Z_holds_the_L_meet_of_P1_._(x,y)_=_the_L_meet_of_P2_._(x,y)
let x, y be Element of Z; ::_thesis: the L_meet of P1 . (x,y) = the L_meet of P2 . (x,y)
y in Z ;
then A42: ex x3 being Relation of X,X st
( y = x3 & x3 is Equivalence_Relation of X ) by A38;
x in Z ;
then ex x2 being Relation of X,X st
( x = x2 & x2 is Equivalence_Relation of X ) by A38;
then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A42;
thus the L_meet of P1 . (x,y) = x1 /\ y1 by A39
.= the L_meet of P2 . (x,y) by A41 ; ::_thesis: verum
end;
then A43: the L_meet of P1 = the L_meet of P2 by A38, A40, BINOP_1:2;
now__::_thesis:_for_x,_y_being_Element_of_Z_holds_the_L_join_of_P1_._(x,y)_=_the_L_join_of_P2_._(x,y)
let x, y be Element of Z; ::_thesis: the L_join of P1 . (x,y) = the L_join of P2 . (x,y)
y in Z ;
then A44: ex x3 being Relation of X,X st
( y = x3 & x3 is Equivalence_Relation of X ) by A38;
x in Z ;
then ex x2 being Relation of X,X st
( x = x2 & x2 is Equivalence_Relation of X ) by A38;
then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A44;
thus the L_join of P1 . (x,y) = x1 "\/" y1 by A39
.= the L_join of P2 . (x,y) by A41 ; ::_thesis: verum
end;
hence P1 = P2 by A38, A40, A43, BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines EqRelLatt MSUALG_5:def_2_:_
for X being set
for b2 being strict Lattice holds
( b2 = EqRelLatt X iff ( the carrier of b2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) ) );
begin
registration
let I be set ;
let M be ManySortedSet of I;
cluster Relation-like I -defined Function-like total V95() MSEquivalence_Relation-like for ManySortedRelation of M,M;
existence
ex b1 being ManySortedRelation of M st b1 is MSEquivalence_Relation-like
proof
deffunc H1( set ) -> Element of bool [:(M . I),(M . I):] = id (M . I);
consider f being ManySortedSet of I such that
A1: for d being set st d in I holds
f . d = H1(d) from PBOOLE:sch_4();
for i being set st i in I holds
f . i is Relation of (M . i),(M . i)
proof
let i be set ; ::_thesis: ( i in I implies f . i is Relation of (M . i),(M . i) )
assume i in I ; ::_thesis: f . i is Relation of (M . i),(M . i)
then f . i = id (M . i) by A1;
hence f . i is Relation of (M . i),(M . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedRelation of M by MSUALG_4:def_1;
take f ; ::_thesis: f is MSEquivalence_Relation-like
for i being set
for R being Relation of (M . i) st i in I & f . i = R holds
R is Equivalence_Relation of (M . i)
proof
let i be set ; ::_thesis: for R being Relation of (M . i) st i in I & f . i = R holds
R is Equivalence_Relation of (M . i)
let R be Relation of (M . i); ::_thesis: ( i in I & f . i = R implies R is Equivalence_Relation of (M . i) )
assume that
A2: i in I and
A3: f . i = R ; ::_thesis: R is Equivalence_Relation of (M . i)
R = id (M . i) by A1, A2, A3;
hence R is Equivalence_Relation of (M . i) ; ::_thesis: verum
end;
hence f is MSEquivalence_Relation-like by MSUALG_4:def_2; ::_thesis: verum
end;
end;
definition
let I be set ;
let M be ManySortedSet of I;
mode Equivalence_Relation of M is MSEquivalence_Relation-like ManySortedRelation of M;
end;
definition
let I be non empty set ;
let M be ManySortedSet of I;
let R be ManySortedRelation of M;
func EqCl R -> Equivalence_Relation of M means :Def3: :: MSUALG_5:def 3
for i being Element of I holds it . i = EqCl (R . i);
existence
ex b1 being Equivalence_Relation of M st
for i being Element of I holds b1 . i = EqCl (R . i)
proof
deffunc H1( Element of I) -> Equivalence_Relation of (M . $1) = EqCl (R . $1);
consider EqR being ManySortedSet of I such that
A1: for i being Element of I holds EqR . i = H1(i) from PBOOLE:sch_5();
for i being set st i in I holds
EqR . i is Relation of (M . i)
proof
let i be set ; ::_thesis: ( i in I implies EqR . i is Relation of (M . i) )
assume i in I ; ::_thesis: EqR . i is Relation of (M . i)
then reconsider i9 = i as Element of I ;
EqR . i = EqCl (R . i9) by A1;
hence EqR . i is Relation of (M . i) ; ::_thesis: verum
end;
then reconsider EqR = EqR as ManySortedRelation of M by MSUALG_4:def_1;
for i being set
for R being Relation of (M . i) st i in I & EqR . i = R holds
R is Equivalence_Relation of (M . i)
proof
let i be set ; ::_thesis: for R being Relation of (M . i) st i in I & EqR . i = R holds
R is Equivalence_Relation of (M . i)
let R1 be Relation of (M . i); ::_thesis: ( i in I & EqR . i = R1 implies R1 is Equivalence_Relation of (M . i) )
assume that
A2: i in I and
A3: EqR . i = R1 ; ::_thesis: R1 is Equivalence_Relation of (M . i)
reconsider i9 = i as Element of I by A2;
R1 = EqCl (R . i9) by A1, A3;
hence R1 is Equivalence_Relation of (M . i) ; ::_thesis: verum
end;
then reconsider EqR = EqR as Equivalence_Relation of M by MSUALG_4:def_2;
take EqR ; ::_thesis: for i being Element of I holds EqR . i = EqCl (R . i)
thus for i being Element of I holds EqR . i = EqCl (R . i) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Equivalence_Relation of M st ( for i being Element of I holds b1 . i = EqCl (R . i) ) & ( for i being Element of I holds b2 . i = EqCl (R . i) ) holds
b1 = b2
proof
let C1, C2 be Equivalence_Relation of M; ::_thesis: ( ( for i being Element of I holds C1 . i = EqCl (R . i) ) & ( for i being Element of I holds C2 . i = EqCl (R . i) ) implies C1 = C2 )
assume that
A4: for i being Element of I holds C1 . i = EqCl (R . i) and
A5: for i being Element of I holds C2 . i = EqCl (R . i) ; ::_thesis: C1 = C2
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
C1_._i_=_C2_._i
let i be set ; ::_thesis: ( i in I implies C1 . i = C2 . i )
assume i in I ; ::_thesis: C1 . i = C2 . i
then reconsider i1 = i as Element of I ;
thus C1 . i = EqCl (R . i1) by A4
.= C2 . i by A5 ; ::_thesis: verum
end;
hence C1 = C2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines EqCl MSUALG_5:def_3_:_
for I being non empty set
for M being ManySortedSet of I
for R being ManySortedRelation of M
for b4 being Equivalence_Relation of M holds
( b4 = EqCl R iff for i being Element of I holds b4 . i = EqCl (R . i) );
theorem :: MSUALG_5:3
for I being non empty set
for M being ManySortedSet of I
for EqR being Equivalence_Relation of M holds EqCl EqR = EqR
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for EqR being Equivalence_Relation of M holds EqCl EqR = EqR
let M be ManySortedSet of I; ::_thesis: for EqR being Equivalence_Relation of M holds EqCl EqR = EqR
let EqR be Equivalence_Relation of M; ::_thesis: EqCl EqR = EqR
now__::_thesis:_for_i_being_Element_of_I_holds_EqR_._i_=_EqCl_(EqR_._i)
let i be Element of I; ::_thesis: EqR . i = EqCl (EqR . i)
reconsider ER = EqR . i as Equivalence_Relation of (M . i) by MSUALG_4:def_2;
thus EqR . i = EqCl ER by Th2
.= EqCl (EqR . i) ; ::_thesis: verum
end;
hence EqCl EqR = EqR by Def3; ::_thesis: verum
end;
begin
definition
let I be non empty set ;
let M be ManySortedSet of I;
let EqR1, EqR2 be Equivalence_Relation of M;
funcEqR1 "\/" EqR2 -> Equivalence_Relation of M means :Def4: :: MSUALG_5:def 4
ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & it = EqCl EqR3 );
existence
ex b1 being Equivalence_Relation of M ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 )
proof
deffunc H1( set ) -> set = (EqR1 \/ EqR2) . $1;
consider E being ManySortedSet of I such that
A1: for i being set st i in I holds
E . i = H1(i) from PBOOLE:sch_4();
for i being set st i in I holds
E . i is Relation of (M . i)
proof
let i be set ; ::_thesis: ( i in I implies E . i is Relation of (M . i) )
assume A2: i in I ; ::_thesis: E . i is Relation of (M . i)
then reconsider i9 = i as Element of I ;
E . i = (EqR1 \/ EqR2) . i by A1, A2
.= (EqR1 . i9) \/ (EqR2 . i9) by PBOOLE:def_4 ;
hence E . i is Relation of (M . i) ; ::_thesis: verum
end;
then reconsider E = E as ManySortedRelation of M by MSUALG_4:def_1;
take EqCl E ; ::_thesis: ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & EqCl E = EqCl EqR3 )
take E ; ::_thesis: ( E = EqR1 \/ EqR2 & EqCl E = EqCl E )
thus ( E = EqR1 \/ EqR2 & EqCl E = EqCl E ) by A1, PBOOLE:3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Equivalence_Relation of M st ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 ) & ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b2 = EqCl EqR3 ) holds
b1 = b2 ;
commutativity
for b1, EqR1, EqR2 being Equivalence_Relation of M st ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 ) holds
ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR2 \/ EqR1 & b1 = EqCl EqR3 ) ;
end;
:: deftheorem Def4 defines "\/" MSUALG_5:def_4_:_
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, b5 being Equivalence_Relation of M holds
( b5 = EqR1 "\/" EqR2 iff ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b5 = EqCl EqR3 ) );
theorem Th4: :: MSUALG_5:4
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 \/ EqR2 c= EqR1 "\/" EqR2
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 \/ EqR2 c= EqR1 "\/" EqR2
let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 \/ EqR2 c= EqR1 "\/" EqR2
let EqR1, EqR2 be Equivalence_Relation of M; ::_thesis: EqR1 \/ EqR2 c= EqR1 "\/" EqR2
consider EqR3 being ManySortedRelation of M such that
A1: EqR3 = EqR1 \/ EqR2 and
A2: EqR1 "\/" EqR2 = EqCl EqR3 by Def4;
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
EqR3_._i_c=_(EqR1_"\/"_EqR2)_._i
let i be set ; ::_thesis: ( i in I implies EqR3 . i c= (EqR1 "\/" EqR2) . i )
assume i in I ; ::_thesis: EqR3 . i c= (EqR1 "\/" EqR2) . i
then reconsider i9 = i as Element of I ;
EqR3 . i c= EqCl (EqR3 . i9) by Def1;
hence EqR3 . i c= (EqR1 "\/" EqR2) . i by A2, Def3; ::_thesis: verum
end;
hence EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by A1, PBOOLE:def_2; ::_thesis: verum
end;
theorem Th5: :: MSUALG_5:5
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR1 "\/" EqR2 c= EqR
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR1 "\/" EqR2 c= EqR
let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR1 "\/" EqR2 c= EqR
let EqR1, EqR2 be Equivalence_Relation of M; ::_thesis: for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR1 "\/" EqR2 c= EqR
consider EqR3 being ManySortedRelation of M such that
A1: EqR3 = EqR1 \/ EqR2 and
A2: EqR1 "\/" EqR2 = EqCl EqR3 by Def4;
let EqR be Equivalence_Relation of M; ::_thesis: ( EqR1 \/ EqR2 c= EqR implies EqR1 "\/" EqR2 c= EqR )
assume A3: EqR1 \/ EqR2 c= EqR ; ::_thesis: EqR1 "\/" EqR2 c= EqR
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(EqR1_"\/"_EqR2)_._i_c=_EqR_._i
let i be set ; ::_thesis: ( i in I implies (EqR1 "\/" EqR2) . i c= EqR . i )
assume A4: i in I ; ::_thesis: (EqR1 "\/" EqR2) . i c= EqR . i
then reconsider i9 = i as Element of I ;
EqR . i9 is Relation of (M . i) ;
then reconsider E = EqR . i as Equivalence_Relation of (M . i) by MSUALG_4:def_2;
EqR3 . i c= E by A3, A1, A4, PBOOLE:def_2;
then EqCl (EqR3 . i9) c= E by Def1;
hence (EqR1 "\/" EqR2) . i c= EqR . i by A2, Def3; ::_thesis: verum
end;
hence EqR1 "\/" EqR2 c= EqR by PBOOLE:def_2; ::_thesis: verum
end;
theorem Th6: :: MSUALG_5:6
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR3 c= EqR ) holds
EqR3 = EqR1 "\/" EqR2
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR3 c= EqR ) holds
EqR3 = EqR1 "\/" EqR2
let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR3 c= EqR ) holds
EqR3 = EqR1 "\/" EqR2
let EqR1, EqR2, EqR3 be Equivalence_Relation of M; ::_thesis: ( EqR1 \/ EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR3 c= EqR ) implies EqR3 = EqR1 "\/" EqR2 )
assume that
A1: EqR1 \/ EqR2 c= EqR3 and
A2: for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR3 c= EqR ; ::_thesis: EqR3 = EqR1 "\/" EqR2
A3: EqR1 "\/" EqR2 c= EqR3 by A1, Th5;
EqR3 c= EqR1 "\/" EqR2 by A2, Th4;
hence EqR3 = EqR1 "\/" EqR2 by A3, PBOOLE:146; ::_thesis: verum
end;
theorem :: MSUALG_5:7
for I being non empty set
for M being ManySortedSet of I
for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR
let M be ManySortedSet of I; ::_thesis: for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR
let EqR be Equivalence_Relation of M; ::_thesis: EqR "\/" EqR = EqR
for EqR3 being Equivalence_Relation of M st EqR \/ EqR c= EqR3 holds
EqR c= EqR3 ;
hence EqR "\/" EqR = EqR by Th6; ::_thesis: verum
end;
theorem Th8: :: MSUALG_5:8
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
let EqR1, EqR2, EqR3 be Equivalence_Relation of M; ::_thesis: (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
for EqR4 being Equivalence_Relation of M st EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) holds
(EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
proof
let EqR4 be Equivalence_Relation of M; ::_thesis: ( EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) implies (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 )
A1: EqR2 \/ EqR3 c= EqR2 "\/" EqR3 by Th4;
assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) ; ::_thesis: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
then A2: EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by Th4;
EqR2 "\/" EqR3 c= EqR1 \/ (EqR2 "\/" EqR3) by PBOOLE:14;
then EqR2 "\/" EqR3 c= EqR4 by A2, PBOOLE:13;
then A3: EqR2 \/ EqR3 c= EqR4 by A1, PBOOLE:13;
EqR2 c= EqR2 \/ EqR3 by PBOOLE:14;
then A4: EqR2 c= EqR4 by A3, PBOOLE:13;
EqR1 c= EqR1 \/ (EqR2 "\/" EqR3) by PBOOLE:14;
then EqR1 c= EqR4 by A2, PBOOLE:13;
then EqR1 \/ EqR2 c= EqR4 by A4, PBOOLE:16;
then A5: EqR1 "\/" EqR2 c= EqR4 by Th5;
EqR3 c= EqR2 \/ EqR3 by PBOOLE:14;
then EqR3 c= EqR4 by A3, PBOOLE:13;
then (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by A5, PBOOLE:16;
hence (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 by Th5; ::_thesis: verum
end;
then A6: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR1 "\/" (EqR2 "\/" EqR3) ;
for EqR4 being Equivalence_Relation of M st EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 holds
EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
proof
let EqR4 be Equivalence_Relation of M; ::_thesis: ( EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 implies EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 )
A7: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Th4;
assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 ; ::_thesis: EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
then A8: (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by Th4;
EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) \/ EqR3 by PBOOLE:14;
then EqR1 "\/" EqR2 c= EqR4 by A8, PBOOLE:13;
then A9: EqR1 \/ EqR2 c= EqR4 by A7, PBOOLE:13;
EqR3 c= (EqR1 "\/" EqR2) \/ EqR3 by PBOOLE:14;
then A10: EqR3 c= EqR4 by A8, PBOOLE:13;
EqR2 c= EqR1 \/ EqR2 by PBOOLE:14;
then EqR2 c= EqR4 by A9, PBOOLE:13;
then EqR2 \/ EqR3 c= EqR4 by A10, PBOOLE:16;
then A11: EqR2 "\/" EqR3 c= EqR4 by Th5;
EqR1 c= EqR1 \/ EqR2 by PBOOLE:14;
then EqR1 c= EqR4 by A9, PBOOLE:13;
then EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by A11, PBOOLE:16;
hence EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 by Th5; ::_thesis: verum
end;
then EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3 ;
hence (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) by A6, PBOOLE:146; ::_thesis: verum
end;
theorem Th9: :: MSUALG_5:9
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1
let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1
let EqR1, EqR2 be Equivalence_Relation of M; ::_thesis: EqR1 /\ (EqR1 "\/" EqR2) = EqR1
A1: EqR1 /\ (EqR1 "\/" EqR2) c= EqR1 by PBOOLE:15;
A2: EqR1 c= EqR1 \/ EqR2 by PBOOLE:14;
EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Th4;
then EqR1 c= EqR1 "\/" EqR2 by A2, PBOOLE:13;
then EqR1 c= EqR1 /\ (EqR1 "\/" EqR2) by PBOOLE:17;
hence EqR1 /\ (EqR1 "\/" EqR2) = EqR1 by A1, PBOOLE:146; ::_thesis: verum
end;
theorem Th10: :: MSUALG_5:10
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds
EqR1 "\/" EqR = EqR1
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds
EqR1 "\/" EqR = EqR1
let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds
EqR1 "\/" EqR = EqR1
let EqR1, EqR2 be Equivalence_Relation of M; ::_thesis: for EqR being Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds
EqR1 "\/" EqR = EqR1
A1: EqR1 = EqR1 \/ (EqR1 /\ EqR2) by PBOOLE:31;
A2: for EqR4 being Equivalence_Relation of M st EqR1 \/ (EqR1 /\ EqR2) c= EqR4 holds
EqR1 c= EqR4 by PBOOLE:31;
let EqR be Equivalence_Relation of M; ::_thesis: ( EqR = EqR1 /\ EqR2 implies EqR1 "\/" EqR = EqR1 )
assume EqR = EqR1 /\ EqR2 ; ::_thesis: EqR1 "\/" EqR = EqR1
hence EqR1 "\/" EqR = EqR1 by A1, A2, Th6; ::_thesis: verum
end;
theorem Th11: :: MSUALG_5:11
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M
let M be ManySortedSet of I; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M
let EqR1, EqR2 be Equivalence_Relation of M; ::_thesis: EqR1 /\ EqR2 is Equivalence_Relation of M
for i being set st i in I holds
(EqR1 /\ EqR2) . i is Relation of (M . i),(M . i)
proof
let i be set ; ::_thesis: ( i in I implies (EqR1 /\ EqR2) . i is Relation of (M . i),(M . i) )
assume A1: i in I ; ::_thesis: (EqR1 /\ EqR2) . i is Relation of (M . i),(M . i)
then reconsider U19 = EqR1 . i as Relation of (M . i),(M . i) by MSUALG_4:def_1;
reconsider U29 = EqR2 . i as Relation of (M . i),(M . i) by A1, MSUALG_4:def_1;
(EqR1 /\ EqR2) . i = U19 /\ U29 by A1, PBOOLE:def_5;
hence (EqR1 /\ EqR2) . i is Relation of (M . i),(M . i) ; ::_thesis: verum
end;
then reconsider U3 = EqR1 /\ EqR2 as ManySortedRelation of M by MSUALG_4:def_1;
for i being set
for R being Relation of (M . i) st i in I & U3 . i = R holds
R is Equivalence_Relation of (M . i)
proof
let i be set ; ::_thesis: for R being Relation of (M . i) st i in I & U3 . i = R holds
R is Equivalence_Relation of (M . i)
let R be Relation of (M . i); ::_thesis: ( i in I & U3 . i = R implies R is Equivalence_Relation of (M . i) )
assume that
A2: i in I and
A3: U3 . i = R ; ::_thesis: R is Equivalence_Relation of (M . i)
reconsider U29 = EqR2 . i as Relation of (M . i) by A2, MSUALG_4:def_1;
reconsider U29 = U29 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def_2;
reconsider U19 = EqR1 . i as Relation of (M . i) by A2, MSUALG_4:def_1;
reconsider U19 = U19 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def_2;
U19 /\ U29 is Equivalence_Relation of (M . i) ;
hence R is Equivalence_Relation of (M . i) by A2, A3, PBOOLE:def_5; ::_thesis: verum
end;
hence EqR1 /\ EqR2 is Equivalence_Relation of M by MSUALG_4:def_2; ::_thesis: verum
end;
definition
let I be non empty set ;
let M be ManySortedSet of I;
func EqRelLatt M -> strict Lattice means :Def5: :: MSUALG_5:def 5
( ( for x being set holds
( x in the carrier of it iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of it . (x,y) = x /\ y & the L_join of it . (x,y) = x "\/" y ) ) );
existence
ex b1 being strict Lattice st
( ( for x being set holds
( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) )
proof
set f = the Equivalence_Relation of M;
defpred S1[ set ] means $1 is Equivalence_Relation of M;
deffunc H1( Element of I) -> set = bool [:(M . $1),(M . $1):];
consider M2 being ManySortedSet of I such that
A1: for i being Element of I holds M2 . i = H1(i) from PBOOLE:sch_5();
consider B being set such that
A2: for x being set holds
( x in B iff ( x in product M2 & S1[x] ) ) from XBOOLE_0:sch_1();
A3: for EqR being Equivalence_Relation of M holds EqR in product M2
proof
let EqR be Equivalence_Relation of M; ::_thesis: EqR in product M2
A4: for x being set st x in dom M2 holds
EqR . x in M2 . x
proof
let x be set ; ::_thesis: ( x in dom M2 implies EqR . x in M2 . x )
assume x in dom M2 ; ::_thesis: EqR . x in M2 . x
then reconsider x9 = x as Element of I ;
A5: EqR . x9 is Subset of [:(M . x9),(M . x9):] ;
M2 . x9 = bool [:(M . x9),(M . x9):] by A1;
hence EqR . x in M2 . x by A5; ::_thesis: verum
end;
dom EqR = I by PARTFUN1:def_2
.= dom M2 by PARTFUN1:def_2 ;
hence EqR in product M2 by A4, CARD_3:9; ::_thesis: verum
end;
then the Equivalence_Relation of M in product M2 ;
then reconsider B = B as non empty set by A2;
defpred S2[ Element of B, Element of B, Element of B] means for x1, y1 being Equivalence_Relation of M st x1 = $1 & y1 = $2 holds
ex EqR3 being ManySortedRelation of M st
( EqR3 = x1 \/ y1 & $3 = EqCl EqR3 );
A6: for x, y being Element of B ex z being Element of B st S2[x,y,z]
proof
let x, y be Element of B; ::_thesis: ex z being Element of B st S2[x,y,z]
reconsider x9 = x, y9 = y as Equivalence_Relation of M by A2;
set z = x9 "\/" y9;
x9 "\/" y9 in product M2 by A3;
then reconsider z = x9 "\/" y9 as Element of B by A2;
take z ; ::_thesis: S2[x,y,z]
let x1, y1 be Equivalence_Relation of M; ::_thesis: ( x1 = x & y1 = y implies ex EqR3 being ManySortedRelation of M st
( EqR3 = x1 \/ y1 & z = EqCl EqR3 ) )
assume that
A7: x1 = x and
A8: y1 = y ; ::_thesis: ex EqR3 being ManySortedRelation of M st
( EqR3 = x1 \/ y1 & z = EqCl EqR3 )
thus ex EqR3 being ManySortedRelation of M st
( EqR3 = x1 \/ y1 & z = EqCl EqR3 ) by A7, A8, Def4; ::_thesis: verum
end;
consider B1 being BinOp of B such that
A9: for x, y being Element of B holds S2[x,y,B1 . (x,y)] from BINOP_1:sch_3(A6);
defpred S3[ Element of B, Element of B, Element of B] means for x1, y1 being Equivalence_Relation of M st x1 = $1 & y1 = $2 holds
$3 = x1 /\ y1;
A10: for x, y being Element of B ex z being Element of B st S3[x,y,z]
proof
let x, y be Element of B; ::_thesis: ex z being Element of B st S3[x,y,z]
reconsider x9 = x, y9 = y as Equivalence_Relation of M by A2;
set z = x9 /\ y9;
for i being set st i in I holds
(x9 /\ y9) . i is Relation of (M . i)
proof
let i be set ; ::_thesis: ( i in I implies (x9 /\ y9) . i is Relation of (M . i) )
assume i in I ; ::_thesis: (x9 /\ y9) . i is Relation of (M . i)
then reconsider i9 = i as Element of I ;
(x9 /\ y9) . i = (x9 . i9) /\ (y9 . i9) by PBOOLE:def_5;
hence (x9 /\ y9) . i is Relation of (M . i) ; ::_thesis: verum
end;
then reconsider z = x9 /\ y9 as ManySortedRelation of M by MSUALG_4:def_1;
for i being set
for R being Relation of (M . i) st i in I & z . i = R holds
R is Equivalence_Relation of (M . i)
proof
let i be set ; ::_thesis: for R being Relation of (M . i) st i in I & z . i = R holds
R is Equivalence_Relation of (M . i)
let R be Relation of (M . i); ::_thesis: ( i in I & z . i = R implies R is Equivalence_Relation of (M . i) )
assume that
A11: i in I and
A12: z . i = R ; ::_thesis: R is Equivalence_Relation of (M . i)
reconsider i9 = i as Element of I by A11;
reconsider x199 = x9 . i9, y199 = y9 . i9 as Relation of (M . i) ;
reconsider x99 = x199, y99 = y199 as Equivalence_Relation of (M . i) by MSUALG_4:def_2;
R = x99 /\ y99 by A12, PBOOLE:def_5;
hence R is Equivalence_Relation of (M . i) ; ::_thesis: verum
end;
then reconsider z = z as Equivalence_Relation of M by MSUALG_4:def_2;
z in product M2 by A3;
then reconsider z = z as Element of B by A2;
take z ; ::_thesis: S3[x,y,z]
thus S3[x,y,z] ; ::_thesis: verum
end;
consider B2 being BinOp of B such that
A13: for x, y being Element of B holds S3[x,y,B2 . (x,y)] from BINOP_1:sch_3(A10);
reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;
A14: now__::_thesis:_for_x,_y_being_Equivalence_Relation_of_M_holds_B1_._(x,y)_=_x_"\/"_y
let x, y be Equivalence_Relation of M; ::_thesis: B1 . (x,y) = x "\/" y
A15: y in product M2 by A3;
x in product M2 by A3;
then reconsider x9 = x, y9 = y as Element of B by A2, A15;
ex EqR3 being ManySortedRelation of M st
( EqR3 = x \/ y & B1 . (x9,y9) = EqCl EqR3 ) by A9;
hence B1 . (x,y) = x "\/" y by Def4; ::_thesis: verum
end;
A16: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B1_._(a,(B1_._(b,c)))_=_B1_._((B1_._(a,b)),c)
let a, b, c be Element of B; ::_thesis: B1 . (a,(B1 . (b,c))) = B1 . ((B1 . (a,b)),c)
reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of M by A2;
thus B1 . (a,(B1 . (b,c))) = B1 . (a,(U2 "\/" U3)) by A14
.= U1 "\/" (U2 "\/" U3) by A14
.= (U1 "\/" U2) "\/" U3 by Th8
.= B1 . ((U1 "\/" U2),c) by A14
.= B1 . ((B1 . (a,b)),c) by A14 ; ::_thesis: verum
end;
A17: for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider x = a, y = b, z = c as Element of B ;
A18: the L_join of L . (a,b) = a "\/" b by LATTICES:def_1;
thus a "\/" (b "\/" c) = the L_join of L . (a,(b "\/" c)) by LATTICES:def_1
.= B1 . (x,(B1 . (y,z))) by LATTICES:def_1
.= the L_join of L . (( the L_join of L . (a,b)),c) by A16
.= (a "\/" b) "\/" c by A18, LATTICES:def_1 ; ::_thesis: verum
end;
A19: now__::_thesis:_for_x,_y_being_Equivalence_Relation_of_M_holds_B2_._(x,y)_=_x_/\_y
let x, y be Equivalence_Relation of M; ::_thesis: B2 . (x,y) = x /\ y
A20: y in product M2 by A3;
x in product M2 by A3;
then reconsider x9 = x, y9 = y as Element of B by A2, A20;
A21: y9 = y ;
x9 = x ;
hence B2 . (x,y) = x /\ y by A13, A21; ::_thesis: verum
end;
A22: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B2_._(a,(B2_._(b,c)))_=_B2_._((B2_._(a,b)),c)
let a, b, c be Element of B; ::_thesis: B2 . (a,(B2 . (b,c))) = B2 . ((B2 . (a,b)),c)
reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of M by A2;
reconsider EQR1 = U2 /\ U3 as Equivalence_Relation of M by Th11;
reconsider EQR2 = U1 /\ U2 as Equivalence_Relation of M by Th11;
thus B2 . (a,(B2 . (b,c))) = B2 . (a,EQR1) by A19
.= U1 /\ (U2 /\ U3) by A19
.= (U1 /\ U2) /\ U3 by PBOOLE:29
.= B2 . (EQR2,c) by A19
.= B2 . ((B2 . (a,b)),c) by A19 ; ::_thesis: verum
end;
A23: for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider x = a, y = b, z = c as Element of B ;
A24: the L_meet of L . (a,b) = a "/\" b by LATTICES:def_2;
thus a "/\" (b "/\" c) = the L_meet of L . (a,(b "/\" c)) by LATTICES:def_2
.= B2 . (x,(B2 . (y,z))) by LATTICES:def_2
.= the L_meet of L . (( the L_meet of L . (a,b)),c) by A22
.= (a "/\" b) "/\" c by A24, LATTICES:def_2 ; ::_thesis: verum
end;
A25: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B1_._(a,b)_=_B1_._(b,a)
let a, b be Element of B; ::_thesis: B1 . (a,b) = B1 . (b,a)
reconsider U1 = a, U2 = b as Equivalence_Relation of M by A2;
thus B1 . (a,b) = U1 "\/" U2 by A14
.= B1 . (b,a) by A14 ; ::_thesis: verum
end;
A26: for a, b being Element of L holds a "\/" b = b "\/" a
proof
let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a
reconsider x = a, y = b as Element of B ;
thus a "\/" b = B1 . (x,y) by LATTICES:def_1
.= the L_join of L . (b,a) by A25
.= b "\/" a by LATTICES:def_1 ; ::_thesis: verum
end;
A27: for a, b being Element of L holds (a "/\" b) "\/" b = b
proof
let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b
reconsider x = a, y = b as Element of B ;
A28: B1 . ((B2 . (x,y)),y) = y
proof
reconsider U1 = x, U2 = y as Equivalence_Relation of M by A2;
reconsider EQR = U1 /\ U2 as Equivalence_Relation of M by Th11;
B2 . (x,y) = U1 /\ U2 by A19;
hence B1 . ((B2 . (x,y)),y) = EQR "\/" U2 by A14
.= y by Th10 ;
::_thesis: verum
end;
thus (a "/\" b) "\/" b = the L_join of L . ((a "/\" b),b) by LATTICES:def_1
.= b by A28, LATTICES:def_2 ; ::_thesis: verum
end;
A29: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B2_._(a,b)_=_B2_._(b,a)
let a, b be Element of B; ::_thesis: B2 . (a,b) = B2 . (b,a)
reconsider U1 = a, U2 = b as Equivalence_Relation of M by A2;
thus B2 . (a,b) = U2 /\ U1 by A19
.= B2 . (b,a) by A19 ; ::_thesis: verum
end;
A30: for a, b being Element of L holds a "/\" b = b "/\" a
proof
let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a
reconsider x = a, y = b as Element of B ;
thus a "/\" b = B2 . (x,y) by LATTICES:def_2
.= the L_meet of L . (b,a) by A29
.= b "/\" a by LATTICES:def_2 ; ::_thesis: verum
end;
for a, b being Element of L holds a "/\" (a "\/" b) = a
proof
let a, b be Element of L; ::_thesis: a "/\" (a "\/" b) = a
reconsider x = a, y = b as Element of B ;
A31: B2 . (x,(B1 . (x,y))) = x
proof
reconsider U1 = x, U2 = y as Equivalence_Relation of M by A2;
B1 . (x,y) = U1 "\/" U2 by A14;
hence B2 . (x,(B1 . (x,y))) = U1 /\ (U1 "\/" U2) by A19
.= x by Th9 ;
::_thesis: verum
end;
thus a "/\" (a "\/" b) = the L_meet of L . (a,(a "\/" b)) by LATTICES:def_2
.= a by A31, LATTICES:def_1 ; ::_thesis: verum
end;
then ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by A26, A17, A27, A30, A23, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
then reconsider L = L as strict Lattice ;
take L ; ::_thesis: ( ( for x being set holds
( x in the carrier of L iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y ) ) )
thus for x being set holds
( x in the carrier of L iff x is Equivalence_Relation of M ) ::_thesis: for x, y being Equivalence_Relation of M holds
( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y )
proof
let x be set ; ::_thesis: ( x in the carrier of L iff x is Equivalence_Relation of M )
thus ( x in the carrier of L implies x is Equivalence_Relation of M ) by A2; ::_thesis: ( x is Equivalence_Relation of M implies x in the carrier of L )
thus ( x is Equivalence_Relation of M implies x in the carrier of L ) ::_thesis: verum
proof
assume A32: x is Equivalence_Relation of M ; ::_thesis: x in the carrier of L
then x in product M2 by A3;
hence x in the carrier of L by A2, A32; ::_thesis: verum
end;
end;
thus for x, y being Equivalence_Relation of M holds
( the L_meet of L . (x,y) = x /\ y & the L_join of L . (x,y) = x "\/" y ) by A14, A19; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Lattice st ( for x being set holds
( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) & ( for x being set holds
( x in the carrier of b2 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) holds
b1 = b2
proof
let S1, S2 be strict Lattice; ::_thesis: ( ( for x being set holds
( x in the carrier of S1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of S1 . (x,y) = x /\ y & the L_join of S1 . (x,y) = x "\/" y ) ) & ( for x being set holds
( x in the carrier of S2 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of S2 . (x,y) = x /\ y & the L_join of S2 . (x,y) = x "\/" y ) ) implies S1 = S2 )
assume that
A33: for x being set holds
( x in the carrier of S1 iff x is Equivalence_Relation of M ) and
A34: for x, y being Equivalence_Relation of M holds
( the L_meet of S1 . (x,y) = x /\ y & the L_join of S1 . (x,y) = x "\/" y ) and
A35: for x being set holds
( x in the carrier of S2 iff x is Equivalence_Relation of M ) and
A36: for x, y being Equivalence_Relation of M holds
( the L_meet of S2 . (x,y) = x /\ y & the L_join of S2 . (x,y) = x "\/" y ) ; ::_thesis: S1 = S2
reconsider Z = the carrier of S1 as non empty set ;
now__::_thesis:_for_x_being_set_holds_
(_x_in_the_carrier_of_S1_iff_x_in_the_carrier_of_S2_)
let x be set ; ::_thesis: ( x in the carrier of S1 iff x in the carrier of S2 )
( x is Equivalence_Relation of M iff x in the carrier of S2 ) by A35;
hence ( x in the carrier of S1 iff x in the carrier of S2 ) by A33; ::_thesis: verum
end;
then A37: the carrier of S1 = the carrier of S2 by TARSKI:1;
A38: now__::_thesis:_for_x,_y_being_Element_of_Z_holds_
(_the_L_meet_of_S1_._(x,y)_=_the_L_meet_of_S2_._(x,y)_&_the_L_join_of_S1_._(x,y)_=_the_L_join_of_S2_._(x,y)_)
let x, y be Element of Z; ::_thesis: ( the L_meet of S1 . (x,y) = the L_meet of S2 . (x,y) & the L_join of S1 . (x,y) = the L_join of S2 . (x,y) )
reconsider x1 = x, y1 = y as Equivalence_Relation of M by A33;
thus the L_meet of S1 . (x,y) = x1 /\ y1 by A34
.= the L_meet of S2 . (x,y) by A36 ; ::_thesis: the L_join of S1 . (x,y) = the L_join of S2 . (x,y)
thus the L_join of S1 . (x,y) = x1 "\/" y1 by A34
.= the L_join of S2 . (x,y) by A36 ; ::_thesis: verum
end;
then the L_meet of S1 = the L_meet of S2 by A37, BINOP_1:2;
hence S1 = S2 by A37, A38, BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines EqRelLatt MSUALG_5:def_5_:_
for I being non empty set
for M being ManySortedSet of I
for b3 being strict Lattice holds
( b3 = EqRelLatt M iff ( ( for x being set holds
( x in the carrier of b3 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b3 . (x,y) = x /\ y & the L_join of b3 . (x,y) = x "\/" y ) ) ) );
begin
registration
let S be non empty ManySortedSign ;
let A be MSAlgebra over S;
cluster MSEquivalence-like -> MSEquivalence_Relation-like for ManySortedRelation of the Sorts of A, the Sorts of A;
coherence
for b1 being ManySortedRelation of A st b1 is MSEquivalence-like holds
b1 is MSEquivalence_Relation-like by MSUALG_4:def_3;
end;
theorem Th12: :: MSUALG_5:12
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
let A be non-empty MSAlgebra over S; ::_thesis: for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
let o be OperSymbol of S; ::_thesis: for C1, C2 being MSCongruence of A
for x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
let C1, C2 be MSCongruence of A; ::_thesis: for x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
let x1, y1 be set ; ::_thesis: for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
let a1, b1 be FinSequence; ::_thesis: ( [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) implies for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) )
assume A1: [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) ; ::_thesis: for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
let x, y be Element of Args (o,A); ::_thesis: ( x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 implies [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) )
assume that
A2: x = (a1 ^ <*x1*>) ^ b1 and
A3: y = (a1 ^ <*y1*>) ^ b1 ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
A4: y = a1 ^ (<*y1*> ^ b1) by A3, FINSEQ_1:32;
A5: x = a1 ^ (<*x1*> ^ b1) by A2, FINSEQ_1:32;
now__::_thesis:_[((Den_(o,A))_._x),((Den_(o,A))_._y)]_in_(C1_._(the_result_sort_of_o))_\/_(C2_._(the_result_sort_of_o))
percases ( [x1,y1] in C1 . ((the_arity_of o) /. ((len a1) + 1)) or [x1,y1] in C2 . ((the_arity_of o) /. ((len a1) + 1)) ) by A1, XBOOLE_0:def_3;
supposeA6: [x1,y1] in C1 . ((the_arity_of o) /. ((len a1) + 1)) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
for n being Nat st n in dom x holds
[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
proof
let n be Nat; ::_thesis: ( n in dom x implies [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) )
assume A7: n in dom x ; ::_thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
then reconsider dz = dom (the_arity_of o) as non empty set by MSUALG_3:6;
A8: n in dom (the_arity_of o) by A7, MSUALG_3:6;
then A9: n in dom ( the Sorts of A * (the_arity_of o)) by PARTFUN1:def_2;
reconsider so = the Sorts of A * (the_arity_of o) as V2() ManySortedSet of dz ;
A10: not product so is empty ;
pi ((Args (o,A)),n) = pi (((( the Sorts of A #) * the Arity of S) . o),n) by MSUALG_1:def_4
.= pi ((( the Sorts of A #) . ( the Arity of S . o)),n) by FUNCT_2:15
.= pi ((( the Sorts of A #) . (the_arity_of o)),n) by MSUALG_1:def_1
.= pi ((product ( the Sorts of A * (the_arity_of o))),n) by FINSEQ_2:def_5
.= ( the Sorts of A * (the_arity_of o)) . n by A9, A10, CARD_3:12
.= the Sorts of A . ((the_arity_of o) . n) by A8, FUNCT_1:13
.= the Sorts of A . ((the_arity_of o) /. n) by A8, PARTFUN1:def_6 ;
then A11: x . n in the Sorts of A . ((the_arity_of o) /. n) by CARD_3:def_6;
A12: ( n in dom (a1 ^ <*x1*>) or ex k being Nat st
( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ) by A2, A7, FINSEQ_1:25;
now__::_thesis:_[(x_._n),(y_._n)]_in_C1_._((the_arity_of_o)_/._n)
percases ( n in dom a1 or ex m being Nat st
( m in dom <*x1*> & n = (len a1) + m ) or ex k being Element of NAT st
( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ) by A12, FINSEQ_1:25;
supposeA13: n in dom a1 ; ::_thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
then A14: y . n = a1 . n by A4, FINSEQ_1:def_7;
x . n = a1 . n by A5, A13, FINSEQ_1:def_7;
hence [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) by A11, A14, EQREL_1:5; ::_thesis: verum
end;
suppose ex m being Nat st
( m in dom <*x1*> & n = (len a1) + m ) ; ::_thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
then consider m being Nat such that
A15: m in dom <*x1*> and
A16: n = (len a1) + m ;
A17: m in Seg 1 by A15, FINSEQ_1:38;
then A18: m = 1 by FINSEQ_1:2, TARSKI:def_1;
then A19: n in Seg ((len a1) + 1) by A16, FINSEQ_1:4;
then n in Seg ((len a1) + (len <*y1*>)) by FINSEQ_1:40;
then n in Seg (len (a1 ^ <*y1*>)) by FINSEQ_1:22;
then n in dom (a1 ^ <*y1*>) by FINSEQ_1:def_3;
then A20: y . n = (a1 ^ <*y1*>) . ((len a1) + 1) by A3, A16, A18, FINSEQ_1:def_7
.= y1 by FINSEQ_1:42 ;
n in Seg ((len a1) + (len <*x1*>)) by A19, FINSEQ_1:40;
then n in Seg (len (a1 ^ <*x1*>)) by FINSEQ_1:22;
then n in dom (a1 ^ <*x1*>) by FINSEQ_1:def_3;
then x . n = (a1 ^ <*x1*>) . ((len a1) + 1) by A2, A16, A18, FINSEQ_1:def_7
.= x1 by FINSEQ_1:42 ;
hence [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) by A6, A16, A17, A20, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
suppose ex k being Element of NAT st
( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ; ::_thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
then consider k being Element of NAT such that
A21: k in dom b1 and
A22: n = (len (a1 ^ <*x1*>)) + k ;
n = ((len a1) + (len <*x1*>)) + k by A22, FINSEQ_1:22;
then n = ((len a1) + 1) + k by FINSEQ_1:40;
then n = ((len a1) + (len <*y1*>)) + k by FINSEQ_1:40;
then n = (len (a1 ^ <*y1*>)) + k by FINSEQ_1:22;
then A23: y . n = b1 . k by A3, A21, FINSEQ_1:def_7;
x . n = b1 . k by A2, A21, A22, FINSEQ_1:def_7;
hence [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) by A11, A23, EQREL_1:5; ::_thesis: verum
end;
end;
end;
hence [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) ; ::_thesis: verum
end;
then [((Den (o,A)) . x),((Den (o,A)) . y)] in C1 . (the_result_sort_of o) by MSUALG_4:def_4;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA24: [x1,y1] in C2 . ((the_arity_of o) /. ((len a1) + 1)) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
for n being Nat st n in dom x holds
[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
proof
let n be Nat; ::_thesis: ( n in dom x implies [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) )
assume A25: n in dom x ; ::_thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
then reconsider dz = dom (the_arity_of o) as non empty set by MSUALG_3:6;
A26: n in dom (the_arity_of o) by A25, MSUALG_3:6;
then A27: n in dom ( the Sorts of A * (the_arity_of o)) by PARTFUN1:def_2;
reconsider so = the Sorts of A * (the_arity_of o) as V2() ManySortedSet of dz ;
A28: not product so is empty ;
pi ((Args (o,A)),n) = pi (((( the Sorts of A #) * the Arity of S) . o),n) by MSUALG_1:def_4
.= pi ((( the Sorts of A #) . ( the Arity of S . o)),n) by FUNCT_2:15
.= pi ((( the Sorts of A #) . (the_arity_of o)),n) by MSUALG_1:def_1
.= pi ((product ( the Sorts of A * (the_arity_of o))),n) by FINSEQ_2:def_5
.= ( the Sorts of A * (the_arity_of o)) . n by A27, A28, CARD_3:12
.= the Sorts of A . ((the_arity_of o) . n) by A26, FUNCT_1:13
.= the Sorts of A . ((the_arity_of o) /. n) by A26, PARTFUN1:def_6 ;
then A29: x . n in the Sorts of A . ((the_arity_of o) /. n) by CARD_3:def_6;
A30: ( n in dom (a1 ^ <*x1*>) or ex k being Nat st
( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ) by A2, A25, FINSEQ_1:25;
now__::_thesis:_[(x_._n),(y_._n)]_in_C2_._((the_arity_of_o)_/._n)
percases ( n in dom a1 or ex m being Nat st
( m in dom <*x1*> & n = (len a1) + m ) or ex k being Element of NAT st
( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ) by A30, FINSEQ_1:25;
supposeA31: n in dom a1 ; ::_thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
then A32: y . n = a1 . n by A4, FINSEQ_1:def_7;
x . n = a1 . n by A5, A31, FINSEQ_1:def_7;
hence [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) by A29, A32, EQREL_1:5; ::_thesis: verum
end;
suppose ex m being Nat st
( m in dom <*x1*> & n = (len a1) + m ) ; ::_thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
then consider m being Nat such that
A33: m in dom <*x1*> and
A34: n = (len a1) + m ;
A35: m in Seg 1 by A33, FINSEQ_1:38;
then A36: m = 1 by FINSEQ_1:2, TARSKI:def_1;
then A37: n in Seg ((len a1) + 1) by A34, FINSEQ_1:4;
then n in Seg ((len a1) + (len <*y1*>)) by FINSEQ_1:40;
then n in Seg (len (a1 ^ <*y1*>)) by FINSEQ_1:22;
then n in dom (a1 ^ <*y1*>) by FINSEQ_1:def_3;
then A38: y . n = (a1 ^ <*y1*>) . ((len a1) + 1) by A3, A34, A36, FINSEQ_1:def_7
.= y1 by FINSEQ_1:42 ;
n in Seg ((len a1) + (len <*x1*>)) by A37, FINSEQ_1:40;
then n in Seg (len (a1 ^ <*x1*>)) by FINSEQ_1:22;
then n in dom (a1 ^ <*x1*>) by FINSEQ_1:def_3;
then x . n = (a1 ^ <*x1*>) . ((len a1) + 1) by A2, A34, A36, FINSEQ_1:def_7
.= x1 by FINSEQ_1:42 ;
hence [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) by A24, A34, A35, A38, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
suppose ex k being Element of NAT st
( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) ; ::_thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
then consider k being Element of NAT such that
A39: k in dom b1 and
A40: n = (len (a1 ^ <*x1*>)) + k ;
n = ((len a1) + (len <*x1*>)) + k by A40, FINSEQ_1:22;
then n = ((len a1) + 1) + k by FINSEQ_1:40;
then n = ((len a1) + (len <*y1*>)) + k by FINSEQ_1:40;
then n = (len (a1 ^ <*y1*>)) + k by FINSEQ_1:22;
then A41: y . n = b1 . k by A3, A39, FINSEQ_1:def_7;
x . n = b1 . k by A2, A39, A40, FINSEQ_1:def_7;
hence [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) by A29, A41, EQREL_1:5; ::_thesis: verum
end;
end;
end;
hence [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) ; ::_thesis: verum
end;
then [((Den (o,A)) . x),((Den (o,A)) . y)] in C2 . (the_result_sort_of o) by MSUALG_4:def_4;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ; ::_thesis: verum
end;
theorem Th13: :: MSUALG_5:13
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x1, y1 being set
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x1, y1 being set
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
let A be non-empty MSAlgebra over S; ::_thesis: for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x1, y1 being set
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
let o be OperSymbol of S; ::_thesis: for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x1, y1 being set
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
let C1, C2 be MSCongruence of A; ::_thesis: for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x1, y1 being set
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
let C be MSEquivalence-like ManySortedRelation of A; ::_thesis: ( C = C1 "\/" C2 implies for x1, y1 being set
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )
assume A1: C = C1 "\/" C2 ; ::_thesis: for x1, y1 being set
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
consider C9 being ManySortedRelation of the Sorts of A such that
A2: C9 = C1 \/ C2 and
A3: C1 "\/" C2 = EqCl C9 by Def4;
A4: (C1 . (the_result_sort_of o)) "\/" (C2 . (the_result_sort_of o)) = EqCl ((C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))) by Th1
.= EqCl (C9 . (the_result_sort_of o)) by A2, PBOOLE:def_4
.= (C1 "\/" C2) . (the_result_sort_of o) by A3, Def3 ;
consider D9 being ManySortedRelation of the Sorts of A such that
A5: D9 = C1 \/ C2 and
A6: C1 "\/" C2 = EqCl D9 by Def4;
let x1, y1 be set ; ::_thesis: for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
let n be Element of NAT ; ::_thesis: for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
let a1, a2, b1 be FinSequence; ::_thesis: ( len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) implies for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )
assume that
A7: len a1 = n and
A8: len a1 = len a2 and
A9: for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ; ::_thesis: ( not [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) or not [x1,y1] in C . ((the_arity_of o) /. (n + 1)) or for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )
A10: (C1 . ((the_arity_of o) /. (n + 1))) "\/" (C2 . ((the_arity_of o) /. (n + 1))) = EqCl ((C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1)))) by Th1
.= EqCl (D9 . ((the_arity_of o) /. (n + 1))) by A5, PBOOLE:def_4
.= (C1 "\/" C2) . ((the_arity_of o) /. (n + 1)) by A6, Def3 ;
set y = (a2 ^ <*y1*>) ^ b1;
assume that
A11: [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) and
A12: [x1,y1] in C . ((the_arity_of o) /. (n + 1)) ; ::_thesis: for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
let x be Element of Args (o,A); ::_thesis: ( x = (a1 ^ <*x1*>) ^ b1 implies [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) )
assume A13: x = (a1 ^ <*x1*>) ^ b1 ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)
A14: the Sorts of A . (the_result_sort_of o) = the Sorts of A . ( the ResultSort of S . o) by MSUALG_1:def_2
.= ( the Sorts of A * the ResultSort of S) . o by FUNCT_2:15
.= Result (o,A) by MSUALG_1:def_5 ;
then (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) ;
then consider p being FinSequence such that
A15: 1 <= len p and
A16: (Den (o,A)) . ((a1 ^ <*x1*>) ^ b1) = p . 1 and
A17: (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) = p . (len p) and
A18: for i being Element of NAT st 1 <= i & i < len p holds
[(p . i),(p . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A1, A11, A13, A4, EQREL_1:28;
x1 in the Sorts of A . ((the_arity_of o) /. (n + 1)) by A12, ZFMISC_1:87;
then consider f being FinSequence such that
A19: 1 <= len f and
A20: x1 = f . 1 and
A21: y1 = f . (len f) and
A22: for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A1, A12, A10, EQREL_1:28;
deffunc H1( Nat) -> set = (Den (o,A)) . ((a2 ^ <*(f . $1)*>) ^ b1);
consider g being FinSequence such that
A23: ( len g = len f & ( for i being Nat st i in dom g holds
g . i = H1(i) ) ) from FINSEQ_1:sch_2();
A24: dom g = Seg (len f) by A23, FINSEQ_1:def_3;
A25: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def_3
.= Seg (len (a1 ^ (<*x1*> ^ b1))) by FINSEQ_1:32
.= Seg ((len a2) + (len (<*x1*> ^ b1))) by A8, FINSEQ_1:22
.= Seg (len (a2 ^ (<*x1*> ^ b1))) by FINSEQ_1:22
.= Seg (len ((a2 ^ <*x1*>) ^ b1)) by FINSEQ_1:32
.= dom ((a2 ^ <*x1*>) ^ b1) by FINSEQ_1:def_3 ;
ex q being FinSequence st
( 1 <= len q & (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Element of NAT st 1 <= i & i < len q holds
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )
proof
take q = p ^ g; ::_thesis: ( 1 <= len q & (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Element of NAT st 1 <= i & i < len q holds
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )
A26: len q = (len p) + (len g) by FINSEQ_1:22;
hence 1 <= len q by A15, NAT_1:12; ::_thesis: ( (Den (o,A)) . x = q . 1 & (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Element of NAT st 1 <= i & i < len q holds
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )
1 in dom p by A15, FINSEQ_3:25;
hence q . 1 = (Den (o,A)) . x by A13, A16, FINSEQ_1:def_7; ::_thesis: ( (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) = q . (len q) & ( for i being Element of NAT st 1 <= i & i < len q holds
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ) )
A27: len g in Seg (len f) by A19, A23, FINSEQ_1:1;
then len g in dom g by A23, FINSEQ_1:def_3;
hence q . (len q) = g . (len g) by A26, FINSEQ_1:def_7
.= (Den (o,A)) . ((a2 ^ <*y1*>) ^ b1) by A21, A23, A24, A27 ;
::_thesis: for i being Element of NAT st 1 <= i & i < len q holds
[(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
A28: len p <> 0 by A15;
hereby ::_thesis: verum
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len q implies [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) )
assume that
A29: 1 <= i and
A30: i < len q ; ::_thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
A31: ( ( 1 <= i & i < len p ) or ( (len p) + 1 <= i & i < len q ) or i = len p )
proof
assume that
A32: ( not 1 <= i or not i < len p ) and
A33: ( not (len p) + 1 <= i or not i < len q ) ; ::_thesis: i = len p
i <= len p by A30, A33, NAT_1:13;
hence i = len p by A29, A32, XXREAL_0:1; ::_thesis: verum
end;
A34: Seg (len ((a1 ^ <*x1*>) ^ b1)) = dom x by A13, FINSEQ_1:def_3
.= dom (the_arity_of o) by MSUALG_3:6
.= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ;
A35: len ((a2 ^ <*x1*>) ^ b1) = len (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32
.= (len a2) + (len (<*x1*> ^ b1)) by FINSEQ_1:22
.= len (a1 ^ (<*x1*> ^ b1)) by A8, FINSEQ_1:22
.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:32
.= len (the_arity_of o) by A34, FINSEQ_1:6 ;
A36: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_x_holds_
x_._k_in_the_Sorts_of_A_._((the_arity_of_o)_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom x implies x . k in the Sorts of A . ((the_arity_of o) /. k) )
assume k in dom x ; ::_thesis: x . k in the Sorts of A . ((the_arity_of o) /. k)
then A37: k in Seg (len (the_arity_of o)) by A25, A35, FINSEQ_1:def_3;
then A38: k in dom (the_arity_of o) by FINSEQ_1:def_3;
then A39: k in dom ( the Sorts of A * (the_arity_of o)) by PARTFUN1:def_2;
reconsider dz = dom (the_arity_of o) as non empty set by A37, FINSEQ_1:def_3;
reconsider so = the Sorts of A * (the_arity_of o) as V2() ManySortedSet of dz ;
A40: not product so is empty ;
pi ((Args (o,A)),k) = pi (((( the Sorts of A #) * the Arity of S) . o),k) by MSUALG_1:def_4
.= pi ((( the Sorts of A #) . ( the Arity of S . o)),k) by FUNCT_2:15
.= pi ((( the Sorts of A #) . (the_arity_of o)),k) by MSUALG_1:def_1
.= pi ((product ( the Sorts of A * (the_arity_of o))),k) by FINSEQ_2:def_5
.= ( the Sorts of A * (the_arity_of o)) . k by A39, A40, CARD_3:12
.= the Sorts of A . ((the_arity_of o) . k) by A38, FUNCT_1:13
.= the Sorts of A . ((the_arity_of o) /. k) by A38, PARTFUN1:def_6 ;
hence x . k in the Sorts of A . ((the_arity_of o) /. k) by CARD_3:def_6; ::_thesis: verum
end;
A41: ex i1 being Nat st len p = i1 + 1 by A28, NAT_1:6;
now__::_thesis:_[(q_._i),(q_._(i_+_1))]_in_(C1_._(the_result_sort_of_o))_\/_(C2_._(the_result_sort_of_o))
percases ( ( 1 <= i & i < len p ) or i = len p or ( (len p) + 1 <= i & i < len q ) ) by A31;
supposeA42: ( 1 <= i & i < len p ) ; ::_thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
then A43: i + 1 <= len p by NAT_1:13;
1 <= i + 1 by A42, NAT_1:13;
then i + 1 in dom p by A43, FINSEQ_3:25;
then A44: q . (i + 1) = p . (i + 1) by FINSEQ_1:def_7;
i in dom p by A42, FINSEQ_3:25;
then q . i = p . i by FINSEQ_1:def_7;
hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A18, A42, A44; ::_thesis: verum
end;
supposeA45: i = len p ; ::_thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
then i in Seg (len p) by A41, FINSEQ_1:4;
then i in dom p by FINSEQ_1:def_3;
then A46: q . i = (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) by A17, A45, FINSEQ_1:def_7;
A47: 1 in Seg (len g) by A19, A23, FINSEQ_1:1;
then 1 in dom g by FINSEQ_1:def_3;
then A48: q . (i + 1) = g . 1 by A45, FINSEQ_1:def_7
.= (Den (o,A)) . ((a2 ^ <*x1*>) ^ b1) by A20, A23, A24, A47 ;
for k being Nat st k in dom ((a2 ^ <*x1*>) ^ b1) holds
((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
proof
let k be Nat; ::_thesis: ( k in dom ((a2 ^ <*x1*>) ^ b1) implies ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) )
assume A50: k in dom ((a2 ^ <*x1*>) ^ b1) ; ::_thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then A51: k in dom (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32;
now__::_thesis:_((a2_^_<*x1*>)_^_b1)_._k_in_the_Sorts_of_A_._((the_arity_of_o)_/._k)
percases ( k in dom a2 or ex n1 being Nat st
( n1 in dom (<*x1*> ^ b1) & k = (len a2) + n1 ) ) by A51, FINSEQ_1:25;
supposeA52: k in dom a2 ; ::_thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then k in Seg (len a2) by FINSEQ_1:def_3;
then k in dom a1 by A8, FINSEQ_1:def_3;
then A53: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;
((a2 ^ <*x1*>) ^ b1) . k = (a2 ^ (<*x1*> ^ b1)) . k by FINSEQ_1:32
.= a2 . k by A52, FINSEQ_1:def_7 ;
hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A53, ZFMISC_1:87; ::_thesis: verum
end;
suppose ex n1 being Nat st
( n1 in dom (<*x1*> ^ b1) & k = (len a2) + n1 ) ; ::_thesis: ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then consider n1 being Nat such that
A54: n1 in dom (<*x1*> ^ b1) and
A55: k = (len a2) + n1 ;
((a2 ^ <*x1*>) ^ b1) . k = (a2 ^ (<*x1*> ^ b1)) . k by FINSEQ_1:32
.= (<*x1*> ^ b1) . n1 by A54, A55, FINSEQ_1:def_7
.= (a1 ^ (<*x1*> ^ b1)) . k by A8, A54, A55, FINSEQ_1:def_7
.= x . k by A13, FINSEQ_1:32 ;
hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A25, A36, A50; ::_thesis: verum
end;
end;
end;
hence ((a2 ^ <*x1*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ; ::_thesis: verum
end;
then reconsider de = (a2 ^ <*x1*>) ^ b1 as Element of Args (o,A) by A35, MSAFREE2:5;
A56: field (C2 . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by EQREL_1:9;
field (C1 . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by EQREL_1:9;
then field ((C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))) = ( the Sorts of A . (the_result_sort_of o)) \/ ( the Sorts of A . (the_result_sort_of o)) by A56, RELAT_1:18
.= the Sorts of A . (the_result_sort_of o) ;
then A57: (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) is_reflexive_in the Sorts of A . (the_result_sort_of o) by RELAT_2:def_9;
(Den (o,A)) . de in the Sorts of A . (the_result_sort_of o) by A14;
hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A46, A48, A57, RELAT_2:def_1; ::_thesis: verum
end;
supposeA58: ( (len p) + 1 <= i & i < len q ) ; ::_thesis: [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
then len p < i by NAT_1:13;
then reconsider j = i - (len p) as Element of NAT by NAT_1:21;
A59: 1 <= j + 1 by NAT_1:12;
len f = (len q) - (len p) by A23, A26, XCMPLX_1:26;
then A60: j < len f by A58, XREAL_1:9;
then j + 1 <= len f by NAT_1:13;
then j + 1 in Seg (len f) by A59, FINSEQ_1:1;
then A61: (i + 1) - (len p) in Seg (len f) by XCMPLX_1:29;
A62: 1 <= j by A58, XREAL_1:19;
then A63: [(f . j),(f . (j + 1))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A22, A60;
then A64: f . ((i - (len p)) + 1) in the Sorts of A . ((the_arity_of o) /. (n + 1)) by ZFMISC_1:87;
A65: for k being Nat st k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) holds
((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
proof
let k be Nat; ::_thesis: ( k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) implies ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) )
assume A66: k in dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) ; ::_thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then A67: ( k in dom (a2 ^ <*(f . ((i + 1) - (len p)))*>) or ex n1 being Nat st
( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ) by FINSEQ_1:25;
now__::_thesis:_((a2_^_<*(f_._((i_+_1)_-_(len_p)))*>)_^_b1)_._k_in_the_Sorts_of_A_._((the_arity_of_o)_/._k)
percases ( k in dom a2 or ex n2 being Nat st
( n2 in dom <*(f . ((i + 1) - (len p)))*> & k = (len a2) + n2 ) or ex n1 being Element of NAT st
( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ) by A67, FINSEQ_1:25;
supposeA68: k in dom a2 ; ::_thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then k in Seg (len a2) by FINSEQ_1:def_3;
then k in dom a1 by A8, FINSEQ_1:def_3;
then A69: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;
((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = (a2 ^ (<*(f . ((i + 1) - (len p)))*> ^ b1)) . k by FINSEQ_1:32
.= a2 . k by A68, FINSEQ_1:def_7 ;
hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A69, ZFMISC_1:87; ::_thesis: verum
end;
suppose ex n2 being Nat st
( n2 in dom <*(f . ((i + 1) - (len p)))*> & k = (len a2) + n2 ) ; ::_thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then consider n2 being Nat such that
A70: n2 in dom <*(f . ((i + 1) - (len p)))*> and
A71: k = (len a2) + n2 ;
n2 in Seg 1 by A70, FINSEQ_1:38;
then A72: k = (len a1) + 1 by A8, A71, FINSEQ_1:2, TARSKI:def_1;
then k in Seg ((len a2) + 1) by A8, FINSEQ_1:4;
then k in Seg ((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) by FINSEQ_1:40;
then k in Seg (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) by FINSEQ_1:22;
then k in dom (a2 ^ <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:def_3;
then ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = (a2 ^ <*(f . ((i + 1) - (len p)))*>) . k by FINSEQ_1:def_7
.= f . ((i + 1) - (len p)) by A8, A72, FINSEQ_1:42 ;
hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A7, A64, A72, XCMPLX_1:29; ::_thesis: verum
end;
supposeA73: ex n1 being Element of NAT st
( n1 in dom b1 & k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 ) ; ::_thesis: ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
A74: len (a1 ^ <*x1*>) = (len a1) + (len <*x1*>) by FINSEQ_1:22
.= (len a2) + 1 by A8, FINSEQ_1:40
.= (len a2) + (len <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:40
.= len (a2 ^ <*(f . ((i + 1) - (len p)))*>) by FINSEQ_1:22 ;
A75: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def_3
.= Seg ((len (a1 ^ <*x1*>)) + (len b1)) by FINSEQ_1:22
.= Seg (((len a1) + (len <*x1*>)) + (len b1)) by FINSEQ_1:22
.= Seg (((len a2) + 1) + (len b1)) by A8, FINSEQ_1:40
.= Seg (((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) + (len b1)) by FINSEQ_1:40
.= Seg ((len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + (len b1)) by FINSEQ_1:22
.= Seg (len ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1)) by FINSEQ_1:22
.= dom ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) by FINSEQ_1:def_3 ;
consider n1 being Element of NAT such that
A76: n1 in dom b1 and
A77: k = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + n1 by A73;
((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k = b1 . n1 by A76, A77, FINSEQ_1:def_7
.= x . k by A13, A76, A77, A74, FINSEQ_1:def_7 ;
hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A36, A66, A75; ::_thesis: verum
end;
end;
end;
hence ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ; ::_thesis: verum
end;
A78: f . (i - (len p)) in the Sorts of A . ((the_arity_of o) /. (n + 1)) by A63, ZFMISC_1:87;
A79: for k being Nat st k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) holds
((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
proof
let k be Nat; ::_thesis: ( k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) implies ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) )
assume A80: k in dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) ; ::_thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then A81: ( k in dom (a2 ^ <*(f . (i - (len p)))*>) or ex n1 being Nat st
( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ) by FINSEQ_1:25;
now__::_thesis:_((a2_^_<*(f_._(i_-_(len_p)))*>)_^_b1)_._k_in_the_Sorts_of_A_._((the_arity_of_o)_/._k)
percases ( k in dom a2 or ex n2 being Nat st
( n2 in dom <*(f . (i - (len p)))*> & k = (len a2) + n2 ) or ex n1 being Element of NAT st
( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ) by A81, FINSEQ_1:25;
supposeA82: k in dom a2 ; ::_thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then k in Seg (len a2) by FINSEQ_1:def_3;
then k in dom a1 by A8, FINSEQ_1:def_3;
then A83: [(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) by A9;
((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = (a2 ^ (<*(f . (i - (len p)))*> ^ b1)) . k by FINSEQ_1:32
.= a2 . k by A82, FINSEQ_1:def_7 ;
hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A83, ZFMISC_1:87; ::_thesis: verum
end;
suppose ex n2 being Nat st
( n2 in dom <*(f . (i - (len p)))*> & k = (len a2) + n2 ) ; ::_thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
then consider n2 being Nat such that
A84: n2 in dom <*(f . (i - (len p)))*> and
A85: k = (len a2) + n2 ;
A86: n2 in Seg 1 by A84, FINSEQ_1:38;
then A87: k = (len a1) + 1 by A8, A85, FINSEQ_1:2, TARSKI:def_1;
then k in Seg ((len a2) + 1) by A8, FINSEQ_1:4;
then k in Seg ((len a2) + (len <*(f . (i - (len p)))*>)) by FINSEQ_1:40;
then k in Seg (len (a2 ^ <*(f . (i - (len p)))*>)) by FINSEQ_1:22;
then k in dom (a2 ^ <*(f . (i - (len p)))*>) by FINSEQ_1:def_3;
then ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = (a2 ^ <*(f . (i - (len p)))*>) . k by FINSEQ_1:def_7
.= f . (i - (len p)) by A8, A87, FINSEQ_1:42 ;
hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A7, A8, A78, A85, A86, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
supposeA88: ex n1 being Element of NAT st
( n1 in dom b1 & k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 ) ; ::_thesis: ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k)
A89: len (a1 ^ <*x1*>) = (len a1) + (len <*x1*>) by FINSEQ_1:22
.= (len a2) + 1 by A8, FINSEQ_1:40
.= (len a2) + (len <*(f . (i - (len p)))*>) by FINSEQ_1:40
.= len (a2 ^ <*(f . (i - (len p)))*>) by FINSEQ_1:22 ;
A90: dom x = Seg (len ((a1 ^ <*x1*>) ^ b1)) by A13, FINSEQ_1:def_3
.= Seg ((len (a1 ^ <*x1*>)) + (len b1)) by FINSEQ_1:22
.= Seg (((len a1) + (len <*x1*>)) + (len b1)) by FINSEQ_1:22
.= Seg (((len a2) + 1) + (len b1)) by A8, FINSEQ_1:40
.= Seg (((len a2) + (len <*(f . (i - (len p)))*>)) + (len b1)) by FINSEQ_1:40
.= Seg ((len (a2 ^ <*(f . (i - (len p)))*>)) + (len b1)) by FINSEQ_1:22
.= Seg (len ((a2 ^ <*(f . (i - (len p)))*>) ^ b1)) by FINSEQ_1:22
.= dom ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) by FINSEQ_1:def_3 ;
consider n1 being Element of NAT such that
A91: n1 in dom b1 and
A92: k = (len (a2 ^ <*(f . (i - (len p)))*>)) + n1 by A88;
((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k = b1 . n1 by A91, A92, FINSEQ_1:def_7
.= x . k by A13, A91, A92, A89, FINSEQ_1:def_7 ;
hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) by A36, A80, A90; ::_thesis: verum
end;
end;
end;
hence ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) . k in the Sorts of A . ((the_arity_of o) /. k) ; ::_thesis: verum
end;
A93: 1 <= j by A58, XREAL_1:19;
j <= len f by A23, A26, A58, XREAL_1:19;
then A94: i - (len p) in Seg (len f) by A93, FINSEQ_1:1;
A95: Seg (len ((a1 ^ <*x1*>) ^ b1)) = dom x by A13, FINSEQ_1:def_3
.= dom (the_arity_of o) by MSUALG_3:6
.= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ;
A96: len ((a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1) = (len (a2 ^ <*(f . ((i + 1) - (len p)))*>)) + (len b1) by FINSEQ_1:22
.= ((len a2) + (len <*(f . ((i + 1) - (len p)))*>)) + (len b1) by FINSEQ_1:22
.= ((len a2) + 1) + (len b1) by FINSEQ_1:40
.= ((len a1) + (len <*x1*>)) + (len b1) by A8, FINSEQ_1:40
.= (len (a1 ^ <*x1*>)) + (len b1) by FINSEQ_1:22
.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:22
.= len (the_arity_of o) by A95, FINSEQ_1:6 ;
len ((a2 ^ <*(f . (i - (len p)))*>) ^ b1) = (len (a2 ^ <*(f . (i - (len p)))*>)) + (len b1) by FINSEQ_1:22
.= ((len a2) + (len <*(f . (i - (len p)))*>)) + (len b1) by FINSEQ_1:22
.= ((len a2) + 1) + (len b1) by FINSEQ_1:40
.= ((len a1) + (len <*x1*>)) + (len b1) by A8, FINSEQ_1:40
.= (len (a1 ^ <*x1*>)) + (len b1) by FINSEQ_1:22
.= len ((a1 ^ <*x1*>) ^ b1) by FINSEQ_1:22
.= len (the_arity_of o) by A95, FINSEQ_1:6 ;
then reconsider d1 = (a2 ^ <*(f . (i - (len p)))*>) ^ b1, d2 = (a2 ^ <*(f . ((i + 1) - (len p)))*>) ^ b1 as Element of Args (o,A) by A79, A65, A96, MSAFREE2:5;
A97: q . i = g . (i - (len p)) by A26, A58, FINSEQ_1:23
.= (Den (o,A)) . d1 by A23, A24, A94 ;
(i + 1) - (len p) = (i - (len p)) + 1 by XCMPLX_1:29;
then A98: [(f . (i - (len p))),(f . ((i + 1) - (len p)))] in (C1 . ((the_arity_of o) /. (n + 1))) \/ (C2 . ((the_arity_of o) /. (n + 1))) by A22, A62, A60;
A99: i + 1 <= len q by A58, NAT_1:13;
(len p) + 1 <= i + 1 by A58, NAT_1:12;
then q . (i + 1) = g . ((i + 1) - (len p)) by A26, A99, FINSEQ_1:23
.= (Den (o,A)) . d2 by A23, A24, A61 ;
hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) by A7, A8, A97, A98, Th12; ::_thesis: verum
end;
end;
end;
hence [(q . i),(q . (i + 1))] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) ; ::_thesis: verum
end;
end;
hence [((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o) by A1, A4, A14, EQREL_1:28; ::_thesis: verum
end;
theorem Th14: :: MSUALG_5:14
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
let A be non-empty MSAlgebra over S; ::_thesis: for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
set b1 = {} ;
let o be OperSymbol of S; ::_thesis: for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
let C1, C2 be MSCongruence of A; ::_thesis: for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
let C be MSEquivalence-like ManySortedRelation of A; ::_thesis: ( C = C1 "\/" C2 implies for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) )
assume A1: C = C1 "\/" C2 ; ::_thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
let x, y be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) )
defpred S1[ Element of NAT ] means for a1, a2, b1 being FinSequence st len a1 = $1 & len a1 = len a2 & x = a1 ^ b1 & ( for n being Nat st n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o);
A2: for l being Element of NAT st S1[l] holds
S1[l + 1]
proof
let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] )
assume A3: for a1, a2, b1 being FinSequence st len a1 = l & len a1 = len a2 & x = a1 ^ b1 & ( for n being Nat st n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) ; ::_thesis: S1[l + 1]
let a1, a2, b1 be FinSequence; ::_thesis: ( len a1 = l + 1 & len a1 = len a2 & x = a1 ^ b1 & ( for n being Nat st n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) )
assume that
A4: len a1 = l + 1 and
A5: len a1 = len a2 and
A6: x = a1 ^ b1 and
A7: for n being Nat st n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o)
A8: l + 1 in Seg (len a1) by A4, FINSEQ_1:4;
then A9: l + 1 in dom a2 by A5, FINSEQ_1:def_3;
set y = a2 ^ b1;
a2 <> {} by A4, A5;
then consider q2 being FinSequence, y1 being set such that
A10: a2 = q2 ^ <*y1*> by FINSEQ_1:46;
A11: l + 1 = (len q2) + (len <*y1*>) by A4, A5, A10, FINSEQ_1:22
.= (len q2) + 1 by FINSEQ_1:40 ;
then A12: y1 = a2 . (l + 1) by A10, FINSEQ_1:42
.= (a2 ^ b1) . (l + 1) by A9, FINSEQ_1:def_7 ;
a1 <> {} by A4;
then consider q1 being FinSequence, x1 being set such that
A13: a1 = q1 ^ <*x1*> by FINSEQ_1:46;
A14: l + 1 = (len q1) + (len <*x1*>) by A4, A13, FINSEQ_1:22
.= (len q1) + 1 by FINSEQ_1:40 ;
then A15: len q1 = len q2 by A11, XCMPLX_1:2;
A16: dom q1 = Seg (len q1) by FINSEQ_1:def_3
.= dom q2 by A15, FINSEQ_1:def_3 ;
A17: for n being Element of NAT st n in dom q1 holds
[(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n)
proof
let n be Element of NAT ; ::_thesis: ( n in dom q1 implies [(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n) )
len q1 <= len a1 by A4, A14, NAT_1:11;
then A18: Seg (len q1) c= Seg (len a1) by FINSEQ_1:5;
assume A19: n in dom q1 ; ::_thesis: [(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n)
then n in Seg (len q1) by FINSEQ_1:def_3;
then n in Seg (len a1) by A18;
then A20: n in dom a1 by FINSEQ_1:def_3;
then A21: x . n = a1 . n by A6, FINSEQ_1:def_7
.= q1 . n by A13, A19, FINSEQ_1:def_7 ;
dom a1 = Seg (len a1) by FINSEQ_1:def_3
.= dom a2 by A5, FINSEQ_1:def_3 ;
then (a2 ^ b1) . n = a2 . n by A20, FINSEQ_1:def_7
.= q2 . n by A10, A16, A19, FINSEQ_1:def_7 ;
hence [(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n) by A7, A20, A21; ::_thesis: verum
end;
A22: l + 1 in dom a1 by A8, FINSEQ_1:def_3;
A23: (q1 ^ <*x1*>) ^ b1 = q1 ^ (<*x1*> ^ b1) by FINSEQ_1:32;
A24: (q2 ^ <*x1*>) ^ b1 = q2 ^ (<*x1*> ^ b1) by FINSEQ_1:32;
A25: for n being Nat st n in dom q1 holds
[(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n)
proof
let n be Nat; ::_thesis: ( n in dom q1 implies [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n) )
assume A26: n in dom q1 ; ::_thesis: [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n)
then A27: ((q2 ^ <*x1*>) ^ b1) . n = q2 . n by A16, A24, FINSEQ_1:def_7;
x . n = q1 . n by A6, A13, A23, A26, FINSEQ_1:def_7;
hence [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n) by A17, A26, A27; ::_thesis: verum
end;
x1 = a1 . (l + 1) by A13, A14, FINSEQ_1:42
.= x . (l + 1) by A6, A22, FINSEQ_1:def_7 ;
then A28: [x1,y1] in C . ((the_arity_of o) /. (l + 1)) by A7, A22, A12;
len q1 = l by A14, XCMPLX_1:2;
then [((Den (o,A)) . x),((Den (o,A)) . ((q2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) by A3, A6, A13, A15, A23, A24, A25;
hence [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) by A1, A6, A13, A10, A14, A15, A17, A28, Th13; ::_thesis: verum
end;
A29: dom y = dom (the_arity_of o) by MSUALG_3:6
.= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ;
dom x = dom (the_arity_of o) by MSUALG_3:6
.= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ;
then reconsider a1 = x, a2 = y as FinSequence by A29, FINSEQ_1:def_2;
assume A30: for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
A31: Seg (len a2) = dom a2 by FINSEQ_1:def_3
.= dom (the_arity_of o) by MSUALG_3:6
.= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ;
Seg (len a1) = dom a1 by FINSEQ_1:def_3
.= dom (the_arity_of o) by MSUALG_3:6
.= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ;
then A32: len a1 = len a2 by A31, FINSEQ_1:6;
A33: x = a1 ^ {} by FINSEQ_1:34;
A34: y = a2 ^ {} by FINSEQ_1:34;
A35: S1[ 0 ]
proof
field (C . (the_result_sort_of o)) = the Sorts of A . (the_result_sort_of o) by ORDERS_1:12;
then A36: C . (the_result_sort_of o) is_reflexive_in the Sorts of A . (the_result_sort_of o) by RELAT_2:def_9;
A37: the Sorts of A . (the_result_sort_of o) = the Sorts of A . ( the ResultSort of S . o) by MSUALG_1:def_2
.= ( the Sorts of A * the ResultSort of S) . o by FUNCT_2:15
.= Result (o,A) by MSUALG_1:def_5 ;
let a1, a2, b1 be FinSequence; ::_thesis: ( len a1 = 0 & len a1 = len a2 & x = a1 ^ b1 & ( for n being Nat st n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) )
assume that
A38: len a1 = 0 and
A39: len a1 = len a2 and
A40: x = a1 ^ b1 and
for n being Nat st n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o)
A41: a1 = {} by A38;
a2 = {} by A38, A39;
hence [((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o) by A40, A41, A37, A36, RELAT_2:def_1; ::_thesis: verum
end;
for l being Element of NAT holds S1[l] from NAT_1:sch_1(A35, A2);
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) by A30, A32, A33, A34; ::_thesis: verum
end;
theorem Th15: :: MSUALG_5:15
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A
let A be non-empty MSAlgebra over S; ::_thesis: for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A
let C1, C2 be MSCongruence of A; ::_thesis: C1 "\/" C2 is MSCongruence of A
reconsider C = C1 "\/" C2 as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A ;
reconsider C = C as ManySortedRelation of A ;
reconsider C = C as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3;
for o being OperSymbol of S
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) by Th14;
hence C1 "\/" C2 is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum
end;
theorem Th16: :: MSUALG_5:16
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A holds C1 /\ C2 is MSCongruence of A
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A holds C1 /\ C2 is MSCongruence of A
let A be non-empty MSAlgebra over S; ::_thesis: for C1, C2 being MSCongruence of A holds C1 /\ C2 is MSCongruence of A
let C1, C2 be MSCongruence of A; ::_thesis: C1 /\ C2 is MSCongruence of A
reconsider C = C1 /\ C2 as Equivalence_Relation of the Sorts of A by Th11;
reconsider C = C as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A ;
reconsider C = C as ManySortedRelation of A ;
reconsider C = C as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3;
for o being OperSymbol of S
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
proof
let o be OperSymbol of S; ::_thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
let x, y be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) )
assume A1: for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
for n being Nat st n in dom x holds
[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
proof
let n be Nat; ::_thesis: ( n in dom x implies [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) )
assume n in dom x ; ::_thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
then [(x . n),(y . n)] in C . ((the_arity_of o) /. n) by A1;
then [(x . n),(y . n)] in (C1 . ((the_arity_of o) /. n)) /\ (C2 . ((the_arity_of o) /. n)) by PBOOLE:def_5;
hence [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) by XBOOLE_0:def_4; ::_thesis: verum
end;
then A2: [((Den (o,A)) . x),((Den (o,A)) . y)] in C1 . (the_result_sort_of o) by MSUALG_4:def_4;
for n being Nat st n in dom x holds
[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
proof
let n be Nat; ::_thesis: ( n in dom x implies [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) )
assume n in dom x ; ::_thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
then [(x . n),(y . n)] in C . ((the_arity_of o) /. n) by A1;
then [(x . n),(y . n)] in (C1 . ((the_arity_of o) /. n)) /\ (C2 . ((the_arity_of o) /. n)) by PBOOLE:def_5;
hence [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) by XBOOLE_0:def_4; ::_thesis: verum
end;
then A3: [((Den (o,A)) . x),((Den (o,A)) . y)] in C2 . (the_result_sort_of o) by MSUALG_4:def_4;
(C1 . (the_result_sort_of o)) /\ (C2 . (the_result_sort_of o)) = C . (the_result_sort_of o) by PBOOLE:def_5;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) by A2, A3, XBOOLE_0:def_4; ::_thesis: verum
end;
hence C1 /\ C2 is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
func CongrLatt A -> strict SubLattice of EqRelLatt the Sorts of A means :Def6: :: MSUALG_5:def 6
for x being set holds
( x in the carrier of it iff x is MSCongruence of A );
existence
ex b1 being strict SubLattice of EqRelLatt the Sorts of A st
for x being set holds
( x in the carrier of b1 iff x is MSCongruence of A )
proof
set D = the carrier of (EqRelLatt the Sorts of A);
set f = the MSCongruence of A;
defpred S1[ set ] means $1 is MSCongruence of A;
deffunc H1( Element of S) -> set = bool [:( the Sorts of A . $1),( the Sorts of A . $1):];
consider M2 being ManySortedSet of the carrier of S such that
A1: for i being Element of the carrier of S holds M2 . i = H1(i) from PBOOLE:sch_5();
consider B being set such that
A2: for x being set holds
( x in B iff ( x in product M2 & S1[x] ) ) from XBOOLE_0:sch_1();
A3: for C1 being MSCongruence of A holds C1 in product M2
proof
let C1 be MSCongruence of A; ::_thesis: C1 in product M2
A4: now__::_thesis:_for_x_being_set_st_x_in_dom_M2_holds_
C1_._x_in_M2_._x
let x be set ; ::_thesis: ( x in dom M2 implies C1 . x in M2 . x )
assume x in dom M2 ; ::_thesis: C1 . x in M2 . x
then reconsider x9 = x as Element of the carrier of S ;
A5: C1 . x9 is Subset of [:( the Sorts of A . x9),( the Sorts of A . x9):] ;
M2 . x9 = bool [:( the Sorts of A . x9),( the Sorts of A . x9):] by A1;
hence C1 . x in M2 . x by A5; ::_thesis: verum
end;
dom C1 = the carrier of S by PARTFUN1:def_2
.= dom M2 by PARTFUN1:def_2 ;
hence C1 in product M2 by A4, CARD_3:9; ::_thesis: verum
end;
A6: for x being set holds
( x in B iff x is MSCongruence of A )
proof
let x be set ; ::_thesis: ( x in B iff x is MSCongruence of A )
thus ( x in B implies x is MSCongruence of A ) by A2; ::_thesis: ( x is MSCongruence of A implies x in B )
thus ( x is MSCongruence of A implies x in B ) ::_thesis: verum
proof
assume A7: x is MSCongruence of A ; ::_thesis: x in B
then x in product M2 by A3;
hence x in B by A2, A7; ::_thesis: verum
end;
end;
then the MSCongruence of A in B ;
then reconsider B = B as non empty set ;
set B1 = the L_join of (EqRelLatt the Sorts of A) || B;
set B2 = the L_meet of (EqRelLatt the Sorts of A) || B;
now__::_thesis:_for_x_being_set_st_x_in_B_holds_
x_in_the_carrier_of_(EqRelLatt_the_Sorts_of_A)
let x be set ; ::_thesis: ( x in B implies x in the carrier of (EqRelLatt the Sorts of A) )
assume x in B ; ::_thesis: x in the carrier of (EqRelLatt the Sorts of A)
then x is MSCongruence of A by A6;
hence x in the carrier of (EqRelLatt the Sorts of A) by Def5; ::_thesis: verum
end;
then A8: B c= the carrier of (EqRelLatt the Sorts of A) by TARSKI:def_3;
then [:B,B:] c= [: the carrier of (EqRelLatt the Sorts of A), the carrier of (EqRelLatt the Sorts of A):] by ZFMISC_1:96;
then reconsider B1 = the L_join of (EqRelLatt the Sorts of A) || B, B2 = the L_meet of (EqRelLatt the Sorts of A) || B as Function of [:B,B:], the carrier of (EqRelLatt the Sorts of A) by FUNCT_2:32;
A9: dom B2 = [:B,B:] by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_[:B,B:]_holds_
B2_._x_in_B
let x be set ; ::_thesis: ( x in [:B,B:] implies B2 . x in B )
assume A10: x in [:B,B:] ; ::_thesis: B2 . x in B
then consider x1, x2 being set such that
A11: x = [x1,x2] by RELAT_1:def_1;
A12: x2 in B by A10, A11, ZFMISC_1:87;
x1 in B by A10, A11, ZFMISC_1:87;
then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A12;
A13: x29 in B by A6;
x19 in B by A6;
then [x1,x2] in [:B,B:] by A13, ZFMISC_1:87;
then B2 . x = the L_meet of (EqRelLatt the Sorts of A) . (x1,x2) by A11, FUNCT_1:49
.= x19 /\ x29 by Def5 ;
then B2 . x is MSCongruence of A by Th16;
hence B2 . x in B by A6; ::_thesis: verum
end;
then reconsider B2 = B2 as BinOp of B by A9, FUNCT_2:3;
A14: dom B1 = [:B,B:] by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_[:B,B:]_holds_
B1_._x_in_B
let x be set ; ::_thesis: ( x in [:B,B:] implies B1 . x in B )
assume A15: x in [:B,B:] ; ::_thesis: B1 . x in B
then consider x1, x2 being set such that
A16: x = [x1,x2] by RELAT_1:def_1;
A17: x2 in B by A15, A16, ZFMISC_1:87;
x1 in B by A15, A16, ZFMISC_1:87;
then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A17;
A18: x29 in B by A6;
x19 in B by A6;
then [x1,x2] in [:B,B:] by A18, ZFMISC_1:87;
then B1 . x = the L_join of (EqRelLatt the Sorts of A) . (x1,x2) by A16, FUNCT_1:49
.= x19 "\/" x29 by Def5 ;
then B1 . x is MSCongruence of A by Th15;
hence B1 . x in B by A6; ::_thesis: verum
end;
then reconsider B1 = B1 as BinOp of B by A14, FUNCT_2:3;
reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;
A19: for a, b being MSCongruence of A holds
( B1 . (a,b) = a "\/" b & B2 . (a,b) = a /\ b )
proof
let a, b be MSCongruence of A; ::_thesis: ( B1 . (a,b) = a "\/" b & B2 . (a,b) = a /\ b )
A20: b in B by A6;
a in B by A6;
then A21: [a,b] in [:B,B:] by A20, ZFMISC_1:87;
hence B1 . (a,b) = the L_join of (EqRelLatt the Sorts of A) . (a,b) by FUNCT_1:49
.= a "\/" b by Def5 ;
::_thesis: B2 . (a,b) = a /\ b
thus B2 . (a,b) = the L_meet of (EqRelLatt the Sorts of A) . (a,b) by A21, FUNCT_1:49
.= a /\ b by Def5 ; ::_thesis: verum
end;
A22: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B1_._(a,b)_=_B1_._(b,a)
let a, b be Element of B; ::_thesis: B1 . (a,b) = B1 . (b,a)
reconsider a9 = a, b9 = b as MSCongruence of A by A6;
thus B1 . (a,b) = a9 "\/" b9 by A19
.= B1 . (b,a) by A19 ; ::_thesis: verum
end;
A23: for a, b being Element of L holds a "\/" b = b "\/" a
proof
let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a
thus a "\/" b = B1 . (a,b) by LATTICES:def_1
.= the L_join of L . (b,a) by A22
.= b "\/" a by LATTICES:def_1 ; ::_thesis: verum
end;
A24: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B2_._(a,(B2_._(b,c)))_=_B2_._((B2_._(a,b)),c)
let a, b, c be Element of B; ::_thesis: B2 . (a,(B2 . (b,c))) = B2 . ((B2 . (a,b)),c)
reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;
reconsider e1 = b9 /\ c9 as MSCongruence of A by Th16;
reconsider e2 = a9 /\ b9 as MSCongruence of A by Th16;
thus B2 . (a,(B2 . (b,c))) = B2 . (a,e1) by A19
.= a9 /\ (b9 /\ c9) by A19
.= (a9 /\ b9) /\ c9 by PBOOLE:29
.= B2 . (e2,c) by A19
.= B2 . ((B2 . (a,b)),c) by A19 ; ::_thesis: verum
end;
A25: for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
thus a "/\" (b "/\" c) = the L_meet of L . (a,(b "/\" c)) by LATTICES:def_2
.= B2 . (a,(B2 . (b,c))) by LATTICES:def_2
.= the L_meet of L . (( the L_meet of L . (a,b)),c) by A24
.= the L_meet of L . ((a "/\" b),c) by LATTICES:def_2
.= (a "/\" b) "/\" c by LATTICES:def_2 ; ::_thesis: verum
end;
A26: now__::_thesis:_for_a,_b,_c_being_Element_of_B_holds_B1_._(a,(B1_._(b,c)))_=_B1_._((B1_._(a,b)),c)
let a, b, c be Element of B; ::_thesis: B1 . (a,(B1 . (b,c))) = B1 . ((B1 . (a,b)),c)
reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;
reconsider d = b9 "\/" c9 as MSCongruence of A by Th15;
reconsider e = a9 "\/" b9 as MSCongruence of A by Th15;
thus B1 . (a,(B1 . (b,c))) = B1 . (a,d) by A19
.= a9 "\/" (b9 "\/" c9) by A19
.= (a9 "\/" b9) "\/" c9 by Th8
.= B1 . (e,c) by A19
.= B1 . ((B1 . (a,b)),c) by A19 ; ::_thesis: verum
end;
A27: for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
thus a "\/" (b "\/" c) = the L_join of L . (a,(b "\/" c)) by LATTICES:def_1
.= B1 . (a,(B1 . (b,c))) by LATTICES:def_1
.= the L_join of L . (( the L_join of L . (a,b)),c) by A26
.= the L_join of L . ((a "\/" b),c) by LATTICES:def_1
.= (a "\/" b) "\/" c by LATTICES:def_1 ; ::_thesis: verum
end;
A28: now__::_thesis:_for_a,_b_being_Element_of_B_holds_B2_._(a,b)_=_B2_._(b,a)
let a, b be Element of B; ::_thesis: B2 . (a,b) = B2 . (b,a)
reconsider a9 = a, b9 = b as MSCongruence of A by A6;
thus B2 . (a,b) = b9 /\ a9 by A19
.= B2 . (b,a) by A19 ; ::_thesis: verum
end;
A29: for a, b being Element of L holds a "/\" b = b "/\" a
proof
let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a
thus a "/\" b = B2 . (a,b) by LATTICES:def_2
.= the L_meet of L . (b,a) by A28
.= b "/\" a by LATTICES:def_2 ; ::_thesis: verum
end;
A30: for a, b being Element of L holds a "/\" (a "\/" b) = a
proof
let a, b be Element of L; ::_thesis: a "/\" (a "\/" b) = a
A31: B2 . (a,(B1 . (a,b))) = a
proof
reconsider a9 = a, b9 = b as MSCongruence of A by A6;
reconsider d = a9 "\/" b9 as MSCongruence of A by Th15;
thus B2 . (a,(B1 . (a,b))) = B2 . (a,d) by A19
.= a9 /\ (a9 "\/" b9) by A19
.= a by Th9 ; ::_thesis: verum
end;
thus a "/\" (a "\/" b) = the L_meet of L . (a,(a "\/" b)) by LATTICES:def_2
.= a by A31, LATTICES:def_1 ; ::_thesis: verum
end;
for a, b being Element of L holds (a "/\" b) "\/" b = b
proof
let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b
A32: B1 . ((B2 . (a,b)),b) = b
proof
reconsider a9 = a, b9 = b as MSCongruence of A by A6;
reconsider EQR = a9 /\ b9 as MSCongruence of A by Th16;
thus B1 . ((B2 . (a,b)),b) = B1 . ((a9 /\ b9),b9) by A19
.= EQR "\/" b9 by A19
.= b by Th10 ; ::_thesis: verum
end;
thus (a "/\" b) "\/" b = the L_join of L . ((a "/\" b),b) by LATTICES:def_1
.= b by A32, LATTICES:def_2 ; ::_thesis: verum
end;
then ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by A23, A27, A29, A25, A30, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
then reconsider L = L as Lattice ;
reconsider L = L as strict SubLattice of EqRelLatt the Sorts of A by A8, NAT_LAT:def_12;
take L ; ::_thesis: for x being set holds
( x in the carrier of L iff x is MSCongruence of A )
thus for x being set holds
( x in the carrier of L iff x is MSCongruence of A ) by A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict SubLattice of EqRelLatt the Sorts of A st ( for x being set holds
( x in the carrier of b1 iff x is MSCongruence of A ) ) & ( for x being set holds
( x in the carrier of b2 iff x is MSCongruence of A ) ) holds
b1 = b2
proof
let C1, C2 be strict SubLattice of EqRelLatt the Sorts of A; ::_thesis: ( ( for x being set holds
( x in the carrier of C1 iff x is MSCongruence of A ) ) & ( for x being set holds
( x in the carrier of C2 iff x is MSCongruence of A ) ) implies C1 = C2 )
assume that
A33: for x being set holds
( x in the carrier of C1 iff x is MSCongruence of A ) and
A34: for x being set holds
( x in the carrier of C2 iff x is MSCongruence of A ) ; ::_thesis: C1 = C2
A35: now__::_thesis:_for_x_being_set_holds_
(_x_in_the_carrier_of_C1_iff_x_in_the_carrier_of_C2_)
let x be set ; ::_thesis: ( x in the carrier of C1 iff x in the carrier of C2 )
( x in the carrier of C2 iff x is MSCongruence of A ) by A34;
hence ( x in the carrier of C1 iff x in the carrier of C2 ) by A33; ::_thesis: verum
end;
then A36: the carrier of C1 = the carrier of C2 by TARSKI:1;
then A37: the L_join of C1 = the L_join of (EqRelLatt the Sorts of A) || the carrier of C2 by NAT_LAT:def_12
.= the L_join of C2 by NAT_LAT:def_12 ;
the L_meet of C1 = the L_meet of (EqRelLatt the Sorts of A) || the carrier of C2 by A36, NAT_LAT:def_12
.= the L_meet of C2 by NAT_LAT:def_12 ;
hence C1 = C2 by A35, A37, TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines CongrLatt MSUALG_5:def_6_:_
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for b3 being strict SubLattice of EqRelLatt the Sorts of A holds
( b3 = CongrLatt A iff for x being set holds
( x in the carrier of b3 iff x is MSCongruence of A ) );
theorem Th17: :: MSUALG_5:17
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S holds id the Sorts of A is MSCongruence of A
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds id the Sorts of A is MSCongruence of A
let A be non-empty MSAlgebra over S; ::_thesis: id the Sorts of A is MSCongruence of A
set J = id the Sorts of A;
for i being set st i in the carrier of S holds
(id the Sorts of A) . i is Relation of ( the Sorts of A . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies (id the Sorts of A) . i is Relation of ( the Sorts of A . i) )
assume i in the carrier of S ; ::_thesis: (id the Sorts of A) . i is Relation of ( the Sorts of A . i)
then (id the Sorts of A) . i = id ( the Sorts of A . i) by MSUALG_3:def_1;
hence (id the Sorts of A) . i is Relation of ( the Sorts of A . i) ; ::_thesis: verum
end;
then reconsider J = id the Sorts of A as ManySortedRelation of the Sorts of A by MSUALG_4:def_1;
for i being set
for R being Relation of ( the Sorts of A . i) st i in the carrier of S & J . i = R holds
R is Equivalence_Relation of ( the Sorts of A . i)
proof
let i be set ; ::_thesis: for R being Relation of ( the Sorts of A . i) st i in the carrier of S & J . i = R holds
R is Equivalence_Relation of ( the Sorts of A . i)
let R be Relation of ( the Sorts of A . i); ::_thesis: ( i in the carrier of S & J . i = R implies R is Equivalence_Relation of ( the Sorts of A . i) )
assume that
A1: i in the carrier of S and
A2: J . i = R ; ::_thesis: R is Equivalence_Relation of ( the Sorts of A . i)
J . i = id ( the Sorts of A . i) by A1, MSUALG_3:def_1;
hence R is Equivalence_Relation of ( the Sorts of A . i) by A2; ::_thesis: verum
end;
then reconsider J = J as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A by MSUALG_4:def_2;
reconsider J = J as ManySortedRelation of A ;
reconsider J = J as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3;
for o being OperSymbol of S
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o)
proof
let o be OperSymbol of S; ::_thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o)
let x, y be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) )
assume A3: for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o)
A4: dom y = dom (the_arity_of o) by MSUALG_3:6
.= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ;
A5: dom x = dom (the_arity_of o) by MSUALG_3:6
.= Seg (len (the_arity_of o)) by FINSEQ_1:def_3 ;
then reconsider x9 = x, y9 = y as FinSequence by A4, FINSEQ_1:def_2;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_x_holds_
x9_._n_=_y9_._n
let n be Nat; ::_thesis: ( n in dom x implies x9 . n = y9 . n )
assume A6: n in dom x ; ::_thesis: x9 . n = y9 . n
J . ((the_arity_of o) /. n) = id ( the Sorts of A . ((the_arity_of o) /. n)) by MSUALG_3:def_1;
then [(x . n),(y . n)] in id ( the Sorts of A . ((the_arity_of o) /. n)) by A3, A6;
hence x9 . n = y9 . n by RELAT_1:def_10; ::_thesis: verum
end;
then A7: x = y by A5, A4, FINSEQ_1:13;
(Den (o,A)) . x in Result (o,A) ;
then A8: (Den (o,A)) . x in ( the Sorts of A * the ResultSort of S) . o by MSUALG_1:def_5;
o in the carrier' of S ;
then o in dom the ResultSort of S by FUNCT_2:def_1;
then (Den (o,A)) . x in the Sorts of A . ( the ResultSort of S . o) by A8, FUNCT_1:13;
then A9: (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2;
J . (the_result_sort_of o) = id ( the Sorts of A . (the_result_sort_of o)) by MSUALG_3:def_1;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) by A7, A9, RELAT_1:def_10; ::_thesis: verum
end;
hence id the Sorts of A is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum
end;
theorem Th18: :: MSUALG_5:18
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S holds [| the Sorts of A, the Sorts of A|] is MSCongruence of A
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds [| the Sorts of A, the Sorts of A|] is MSCongruence of A
let A be non-empty MSAlgebra over S; ::_thesis: [| the Sorts of A, the Sorts of A|] is MSCongruence of A
set J = [| the Sorts of A, the Sorts of A|];
for i being set st i in the carrier of S holds
[| the Sorts of A, the Sorts of A|] . i is Relation of ( the Sorts of A . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies [| the Sorts of A, the Sorts of A|] . i is Relation of ( the Sorts of A . i) )
assume i in the carrier of S ; ::_thesis: [| the Sorts of A, the Sorts of A|] . i is Relation of ( the Sorts of A . i)
then [| the Sorts of A, the Sorts of A|] . i c= [:( the Sorts of A . i),( the Sorts of A . i):] by PBOOLE:def_16;
hence [| the Sorts of A, the Sorts of A|] . i is Relation of ( the Sorts of A . i) ; ::_thesis: verum
end;
then reconsider J = [| the Sorts of A, the Sorts of A|] as ManySortedRelation of the Sorts of A by MSUALG_4:def_1;
for i being set
for R being Relation of ( the Sorts of A . i) st i in the carrier of S & J . i = R holds
R is Equivalence_Relation of ( the Sorts of A . i)
proof
let i be set ; ::_thesis: for R being Relation of ( the Sorts of A . i) st i in the carrier of S & J . i = R holds
R is Equivalence_Relation of ( the Sorts of A . i)
let R be Relation of ( the Sorts of A . i); ::_thesis: ( i in the carrier of S & J . i = R implies R is Equivalence_Relation of ( the Sorts of A . i) )
assume that
A1: i in the carrier of S and
A2: J . i = R ; ::_thesis: R is Equivalence_Relation of ( the Sorts of A . i)
J . i = nabla ( the Sorts of A . i) by A1, PBOOLE:def_16;
hence R is Equivalence_Relation of ( the Sorts of A . i) by A2; ::_thesis: verum
end;
then reconsider J = J as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A by MSUALG_4:def_2;
reconsider J = J as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def_3;
for o being OperSymbol of S
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o)
proof
let o be OperSymbol of S; ::_thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o)
let x, y be Element of Args (o,A); ::_thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) )
assume for n being Nat st n in dom x holds
[(x . n),(y . n)] in J . ((the_arity_of o) /. n) ; ::_thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o)
o in the carrier' of S ;
then A3: o in dom the ResultSort of S by FUNCT_2:def_1;
(Den (o,A)) . y in Result (o,A) ;
then (Den (o,A)) . y in ( the Sorts of A * the ResultSort of S) . o by MSUALG_1:def_5;
then (Den (o,A)) . y in the Sorts of A . ( the ResultSort of S . o) by A3, FUNCT_1:13;
then A4: (Den (o,A)) . y in the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2;
(Den (o,A)) . x in Result (o,A) ;
then (Den (o,A)) . x in ( the Sorts of A * the ResultSort of S) . o by MSUALG_1:def_5;
then (Den (o,A)) . x in the Sorts of A . ( the ResultSort of S . o) by A3, FUNCT_1:13;
then A5: (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o) by MSUALG_1:def_2;
J . (the_result_sort_of o) = [:( the Sorts of A . (the_result_sort_of o)),( the Sorts of A . (the_result_sort_of o)):] by PBOOLE:def_16;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in J . (the_result_sort_of o) by A5, A4, ZFMISC_1:87; ::_thesis: verum
end;
hence [| the Sorts of A, the Sorts of A|] is MSCongruence of A by MSUALG_4:def_4; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster CongrLatt A -> strict bounded ;
coherence
CongrLatt A is bounded
proof
ex c being Element of (CongrLatt A) st
for a being Element of (CongrLatt A) holds
( c "\/" a = c & a "\/" c = c )
proof
reconsider c9 = [| the Sorts of A, the Sorts of A|] as MSCongruence of A by Th18;
A1: the L_join of (CongrLatt A) = the L_join of (EqRelLatt the Sorts of A) || the carrier of (CongrLatt A) by NAT_LAT:def_12;
reconsider c = c9 as Element of (CongrLatt A) by Def6;
take c ; ::_thesis: for a being Element of (CongrLatt A) holds
( c "\/" a = c & a "\/" c = c )
let a be Element of (CongrLatt A); ::_thesis: ( c "\/" a = c & a "\/" c = c )
A2: [c,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] by ZFMISC_1:87;
reconsider a9 = a as MSCongruence of A by Def6;
A3: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
(c9_"\/"_a9)_._i_=_c9_._i
let i be set ; ::_thesis: ( i in the carrier of S implies (c9 "\/" a9) . i = c9 . i )
assume A4: i in the carrier of S ; ::_thesis: (c9 "\/" a9) . i = c9 . i
then reconsider i9 = i as Element of S ;
A5: ex K1 being ManySortedRelation of the Sorts of A st
( K1 = c9 \/ a9 & c9 "\/" a9 = EqCl K1 ) by Def4;
reconsider K2 = c9 . i9, a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) ;
(c9 \/ a9) . i = (c9 . i) \/ (a9 . i) by A4, PBOOLE:def_4
.= (nabla ( the Sorts of A . i)) \/ a2 by PBOOLE:def_16
.= nabla ( the Sorts of A . i) by EQREL_1:1
.= c9 . i by A4, PBOOLE:def_16 ;
hence (c9 "\/" a9) . i = EqCl K2 by A5, Def3
.= c9 . i by Th2 ;
::_thesis: verum
end;
thus c "\/" a = the L_join of (CongrLatt A) . (c,a) by LATTICES:def_1
.= the L_join of (EqRelLatt the Sorts of A) . (c,a) by A1, A2, FUNCT_1:49
.= c9 "\/" a9 by Def5
.= c by A3, PBOOLE:3 ; ::_thesis: a "\/" c = c
hence a "\/" c = c ; ::_thesis: verum
end;
then A6: CongrLatt A is upper-bounded by LATTICES:def_14;
ex c being Element of (CongrLatt A) st
for a being Element of (CongrLatt A) holds
( c "/\" a = c & a "/\" c = c )
proof
reconsider c9 = id the Sorts of A as MSCongruence of A by Th17;
A7: the L_meet of (CongrLatt A) = the L_meet of (EqRelLatt the Sorts of A) || the carrier of (CongrLatt A) by NAT_LAT:def_12;
reconsider c = c9 as Element of (CongrLatt A) by Def6;
take c ; ::_thesis: for a being Element of (CongrLatt A) holds
( c "/\" a = c & a "/\" c = c )
let a be Element of (CongrLatt A); ::_thesis: ( c "/\" a = c & a "/\" c = c )
A8: [c,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] by ZFMISC_1:87;
reconsider a9 = a as MSCongruence of A by Def6;
A9: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
(c9_/\_a9)_._i_=_c9_._i
let i be set ; ::_thesis: ( i in the carrier of S implies (c9 /\ a9) . i = c9 . i )
assume A10: i in the carrier of S ; ::_thesis: (c9 /\ a9) . i = c9 . i
then reconsider i9 = i as Element of S ;
reconsider a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) ;
thus (c9 /\ a9) . i = (c9 . i) /\ (a9 . i) by A10, PBOOLE:def_5
.= (id ( the Sorts of A . i)) /\ a2 by MSUALG_3:def_1
.= id ( the Sorts of A . i) by EQREL_1:10
.= c9 . i by A10, MSUALG_3:def_1 ; ::_thesis: verum
end;
thus c "/\" a = the L_meet of (CongrLatt A) . (c,a) by LATTICES:def_2
.= the L_meet of (EqRelLatt the Sorts of A) . (c,a) by A7, A8, FUNCT_1:49
.= c9 /\ a9 by Def5
.= c by A9, PBOOLE:3 ; ::_thesis: a "/\" c = c
hence a "/\" c = c ; ::_thesis: verum
end;
then CongrLatt A is lower-bounded by LATTICES:def_13;
hence CongrLatt A is bounded by A6; ::_thesis: verum
end;
end;
theorem :: MSUALG_5:19
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S holds Bottom (CongrLatt A) = id the Sorts of A
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds Bottom (CongrLatt A) = id the Sorts of A
let A be non-empty MSAlgebra over S; ::_thesis: Bottom (CongrLatt A) = id the Sorts of A
set K = id the Sorts of A;
id the Sorts of A is MSCongruence of A by Th17;
then reconsider K = id the Sorts of A as Element of (CongrLatt A) by Def6;
A1: the L_meet of (CongrLatt A) = the L_meet of (EqRelLatt the Sorts of A) || the carrier of (CongrLatt A) by NAT_LAT:def_12;
now__::_thesis:_for_a_being_Element_of_(CongrLatt_A)_holds_
(_K_"/\"_a_=_K_&_a_"/\"_K_=_K_)
let a be Element of (CongrLatt A); ::_thesis: ( K "/\" a = K & a "/\" K = K )
reconsider K9 = K, a9 = a as Equivalence_Relation of the Sorts of A by Def6;
A2: [K,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] by ZFMISC_1:87;
A3: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
(K9_/\_a9)_._i_=_K9_._i
let i be set ; ::_thesis: ( i in the carrier of S implies (K9 /\ a9) . i = K9 . i )
assume A4: i in the carrier of S ; ::_thesis: (K9 /\ a9) . i = K9 . i
then reconsider i9 = i as Element of S ;
reconsider a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_4:def_2;
thus (K9 /\ a9) . i = (K9 . i) /\ (a9 . i) by A4, PBOOLE:def_5
.= (id ( the Sorts of A . i)) /\ a2 by MSUALG_3:def_1
.= id ( the Sorts of A . i) by EQREL_1:10
.= K9 . i by A4, MSUALG_3:def_1 ; ::_thesis: verum
end;
thus K "/\" a = the L_meet of (CongrLatt A) . (K,a) by LATTICES:def_2
.= the L_meet of (EqRelLatt the Sorts of A) . (K,a) by A1, A2, FUNCT_1:49
.= K9 /\ a9 by Def5
.= K by A3, PBOOLE:3 ; ::_thesis: a "/\" K = K
hence a "/\" K = K ; ::_thesis: verum
end;
hence Bottom (CongrLatt A) = id the Sorts of A by LATTICES:def_16; ::_thesis: verum
end;
theorem :: MSUALG_5:20
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S holds Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|]
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S holds Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|]
let A be non-empty MSAlgebra over S; ::_thesis: Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|]
set K = [| the Sorts of A, the Sorts of A|];
[| the Sorts of A, the Sorts of A|] is MSCongruence of A by Th18;
then reconsider K = [| the Sorts of A, the Sorts of A|] as Element of (CongrLatt A) by Def6;
A1: the L_join of (CongrLatt A) = the L_join of (EqRelLatt the Sorts of A) || the carrier of (CongrLatt A) by NAT_LAT:def_12;
now__::_thesis:_for_a_being_Element_of_(CongrLatt_A)_holds_
(_K_"\/"_a_=_K_&_a_"\/"_K_=_K_)
let a be Element of (CongrLatt A); ::_thesis: ( K "\/" a = K & a "\/" K = K )
reconsider K9 = K, a9 = a as Equivalence_Relation of the Sorts of A by Def6;
A2: [K,a] in [: the carrier of (CongrLatt A), the carrier of (CongrLatt A):] by ZFMISC_1:87;
A3: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
(K9_"\/"_a9)_._i_=_K9_._i
let i be set ; ::_thesis: ( i in the carrier of S implies (K9 "\/" a9) . i = K9 . i )
assume A4: i in the carrier of S ; ::_thesis: (K9 "\/" a9) . i = K9 . i
then reconsider i9 = i as Element of S ;
A5: ex K1 being ManySortedRelation of the Sorts of A st
( K1 = K9 \/ a9 & K9 "\/" a9 = EqCl K1 ) by Def4;
reconsider K2 = K9 . i9, a2 = a9 . i9 as Equivalence_Relation of ( the Sorts of A . i) by MSUALG_4:def_2;
(K9 \/ a9) . i = (K9 . i) \/ (a9 . i) by A4, PBOOLE:def_4
.= (nabla ( the Sorts of A . i)) \/ a2 by PBOOLE:def_16
.= nabla ( the Sorts of A . i) by EQREL_1:1
.= K9 . i by A4, PBOOLE:def_16 ;
hence (K9 "\/" a9) . i = EqCl K2 by A5, Def3
.= K9 . i by Th2 ;
::_thesis: verum
end;
thus K "\/" a = the L_join of (CongrLatt A) . (K,a) by LATTICES:def_1
.= the L_join of (EqRelLatt the Sorts of A) . (K,a) by A1, A2, FUNCT_1:49
.= K9 "\/" a9 by Def5
.= K by A3, PBOOLE:3 ; ::_thesis: a "\/" K = K
hence a "\/" K = K ; ::_thesis: verum
end;
hence Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|] by LATTICES:def_17; ::_thesis: verum
end;
theorem :: MSUALG_5:21
for x, X being set holds
( x in the carrier of (EqRelLatt X) iff x is Equivalence_Relation of X )
proof
let x, X be set ; ::_thesis: ( x in the carrier of (EqRelLatt X) iff x is Equivalence_Relation of X )
A1: the carrier of (EqRelLatt X) = { x1 where x1 is Relation of X,X : x1 is Equivalence_Relation of X } by Def2;
thus ( x in the carrier of (EqRelLatt X) implies x is Equivalence_Relation of X ) ::_thesis: ( x is Equivalence_Relation of X implies x in the carrier of (EqRelLatt X) )
proof
assume x in the carrier of (EqRelLatt X) ; ::_thesis: x is Equivalence_Relation of X
then ex x1 being Relation of X,X st
( x = x1 & x1 is Equivalence_Relation of X ) by A1;
hence x is Equivalence_Relation of X ; ::_thesis: verum
end;
thus ( x is Equivalence_Relation of X implies x in the carrier of (EqRelLatt X) ) by A1; ::_thesis: verum
end;