:: NORMFORM semantic presentation
begin
definition
let A, B be non empty preBoolean set ;
let x, y be Element of [:A,B:];
predx c= y means :: NORMFORM:def 1
( x `1 c= y `1 & x `2 c= y `2 );
reflexivity
for x being Element of [:A,B:] holds
( x `1 c= x `1 & x `2 c= x `2 ) ;
funcx \/ y -> Element of [:A,B:] equals :: NORMFORM:def 2
[((x `1) \/ (y `1)),((x `2) \/ (y `2))];
correctness
coherence
[((x `1) \/ (y `1)),((x `2) \/ (y `2))] is Element of [:A,B:];
;
commutativity
for b1, x, y being Element of [:A,B:] st b1 = [((x `1) \/ (y `1)),((x `2) \/ (y `2))] holds
b1 = [((y `1) \/ (x `1)),((y `2) \/ (x `2))] ;
idempotence
for x being Element of [:A,B:] holds x = [((x `1) \/ (x `1)),((x `2) \/ (x `2))] by MCART_1:21;
funcx /\ y -> Element of [:A,B:] equals :: NORMFORM:def 3
[((x `1) /\ (y `1)),((x `2) /\ (y `2))];
correctness
coherence
[((x `1) /\ (y `1)),((x `2) /\ (y `2))] is Element of [:A,B:];
;
commutativity
for b1, x, y being Element of [:A,B:] st b1 = [((x `1) /\ (y `1)),((x `2) /\ (y `2))] holds
b1 = [((y `1) /\ (x `1)),((y `2) /\ (x `2))] ;
idempotence
for x being Element of [:A,B:] holds x = [((x `1) /\ (x `1)),((x `2) /\ (x `2))] by MCART_1:21;
funcx \ y -> Element of [:A,B:] equals :: NORMFORM:def 4
[((x `1) \ (y `1)),((x `2) \ (y `2))];
correctness
coherence
[((x `1) \ (y `1)),((x `2) \ (y `2))] is Element of [:A,B:];
;
funcx \+\ y -> Element of [:A,B:] equals :: NORMFORM:def 5
[((x `1) \+\ (y `1)),((x `2) \+\ (y `2))];
correctness
coherence
[((x `1) \+\ (y `1)),((x `2) \+\ (y `2))] is Element of [:A,B:];
;
commutativity
for b1, x, y being Element of [:A,B:] st b1 = [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))] holds
b1 = [((y `1) \+\ (x `1)),((y `2) \+\ (x `2))] ;
end;
:: deftheorem defines c= NORMFORM:def_1_:_
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds
( x c= y iff ( x `1 c= y `1 & x `2 c= y `2 ) );
:: deftheorem defines \/ NORMFORM:def_2_:_
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds x \/ y = [((x `1) \/ (y `1)),((x `2) \/ (y `2))];
:: deftheorem defines /\ NORMFORM:def_3_:_
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds x /\ y = [((x `1) /\ (y `1)),((x `2) /\ (y `2))];
:: deftheorem defines \ NORMFORM:def_4_:_
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds x \ y = [((x `1) \ (y `1)),((x `2) \ (y `2))];
:: deftheorem defines \+\ NORMFORM:def_5_:_
for A, B being non empty preBoolean set
for x, y being Element of [:A,B:] holds x \+\ y = [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))];
theorem Th1: :: NORMFORM:1
for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] st a c= b & b c= a holds
a = b
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b being Element of [:A,B:] st a c= b & b c= a holds
a = b
let a, b be Element of [:A,B:]; ::_thesis: ( a c= b & b c= a implies a = b )
assume ( a `1 c= b `1 & a `2 c= b `2 & b `1 c= a `1 & b `2 c= a `2 ) ; :: according to NORMFORM:def_1 ::_thesis: a = b
then ( a `1 = b `1 & a `2 = b `2 ) by XBOOLE_0:def_10;
hence a = b by DOMAIN_1:2; ::_thesis: verum
end;
theorem Th2: :: NORMFORM:2
for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] st a c= b & b c= c holds
a c= c
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] st a c= b & b c= c holds
a c= c
let a, b, c be Element of [:A,B:]; ::_thesis: ( a c= b & b c= c implies a c= c )
assume ( a `1 c= b `1 & a `2 c= b `2 & b `1 c= c `1 & b `2 c= c `2 ) ; :: according to NORMFORM:def_1 ::_thesis: a c= c
hence ( a `1 c= c `1 & a `2 c= c `2 ) by XBOOLE_1:1; :: according to NORMFORM:def_1 ::_thesis: verum
end;
theorem Th3: :: NORMFORM:3
for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] holds (a \/ b) \/ c = a \/ (b \/ c)
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] holds (a \/ b) \/ c = a \/ (b \/ c)
let a, b, c be Element of [:A,B:]; ::_thesis: (a \/ b) \/ c = a \/ (b \/ c)
A1: ((a \/ b) \/ c) `2 = ((a \/ b) `2) \/ (c `2) by MCART_1:7
.= ((a `2) \/ (b `2)) \/ (c `2) by MCART_1:7
.= (a `2) \/ ((b `2) \/ (c `2)) by XBOOLE_1:4
.= (a `2) \/ ((b \/ c) `2) by MCART_1:7
.= (a \/ (b \/ c)) `2 by MCART_1:7 ;
((a \/ b) \/ c) `1 = ((a \/ b) `1) \/ (c `1) by MCART_1:7
.= ((a `1) \/ (b `1)) \/ (c `1) by MCART_1:7
.= (a `1) \/ ((b `1) \/ (c `1)) by XBOOLE_1:4
.= (a `1) \/ ((b \/ c) `1) by MCART_1:7
.= (a \/ (b \/ c)) `1 by MCART_1:7 ;
hence (a \/ b) \/ c = a \/ (b \/ c) by A1, DOMAIN_1:2; ::_thesis: verum
end;
theorem :: NORMFORM:4
for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] holds (a /\ b) /\ c = a /\ (b /\ c)
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] holds (a /\ b) /\ c = a /\ (b /\ c)
let a, b, c be Element of [:A,B:]; ::_thesis: (a /\ b) /\ c = a /\ (b /\ c)
A1: ((a /\ b) /\ c) `2 = ((a /\ b) `2) /\ (c `2) by MCART_1:7
.= ((a `2) /\ (b `2)) /\ (c `2) by MCART_1:7
.= (a `2) /\ ((b `2) /\ (c `2)) by XBOOLE_1:16
.= (a `2) /\ ((b /\ c) `2) by MCART_1:7
.= (a /\ (b /\ c)) `2 by MCART_1:7 ;
((a /\ b) /\ c) `1 = ((a /\ b) `1) /\ (c `1) by MCART_1:7
.= ((a `1) /\ (b `1)) /\ (c `1) by MCART_1:7
.= (a `1) /\ ((b `1) /\ (c `1)) by XBOOLE_1:16
.= (a `1) /\ ((b /\ c) `1) by MCART_1:7
.= (a /\ (b /\ c)) `1 by MCART_1:7 ;
hence (a /\ b) /\ c = a /\ (b /\ c) by A1, DOMAIN_1:2; ::_thesis: verum
end;
theorem Th5: :: NORMFORM:5
for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] holds a /\ (b \/ c) = (a /\ b) \/ (a /\ c)
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] holds a /\ (b \/ c) = (a /\ b) \/ (a /\ c)
let a, b, c be Element of [:A,B:]; ::_thesis: a /\ (b \/ c) = (a /\ b) \/ (a /\ c)
A1: (a /\ (b \/ c)) `2 = (a `2) /\ ((b \/ c) `2) by MCART_1:7
.= (a `2) /\ ((b `2) \/ (c `2)) by MCART_1:7
.= ((a `2) /\ (b `2)) \/ ((a `2) /\ (c `2)) by XBOOLE_1:23
.= ((a `2) /\ (b `2)) \/ ((a /\ c) `2) by MCART_1:7
.= ((a /\ b) `2) \/ ((a /\ c) `2) by MCART_1:7
.= ((a /\ b) \/ (a /\ c)) `2 by MCART_1:7 ;
(a /\ (b \/ c)) `1 = (a `1) /\ ((b \/ c) `1) by MCART_1:7
.= (a `1) /\ ((b `1) \/ (c `1)) by MCART_1:7
.= ((a `1) /\ (b `1)) \/ ((a `1) /\ (c `1)) by XBOOLE_1:23
.= ((a `1) /\ (b `1)) \/ ((a /\ c) `1) by MCART_1:7
.= ((a /\ b) `1) \/ ((a /\ c) `1) by MCART_1:7
.= ((a /\ b) \/ (a /\ c)) `1 by MCART_1:7 ;
hence a /\ (b \/ c) = (a /\ b) \/ (a /\ c) by A1, DOMAIN_1:2; ::_thesis: verum
end;
theorem Th6: :: NORMFORM:6
for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] holds a \/ (b /\ a) = a
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b being Element of [:A,B:] holds a \/ (b /\ a) = a
let a, b be Element of [:A,B:]; ::_thesis: a \/ (b /\ a) = a
A1: (a \/ (b /\ a)) `2 = (a `2) \/ ((b /\ a) `2) by MCART_1:7
.= (a `2) \/ ((b `2) /\ (a `2)) by MCART_1:7
.= a `2 by XBOOLE_1:22 ;
(a \/ (b /\ a)) `1 = (a `1) \/ ((b /\ a) `1) by MCART_1:7
.= (a `1) \/ ((b `1) /\ (a `1)) by MCART_1:7
.= a `1 by XBOOLE_1:22 ;
hence a \/ (b /\ a) = a by A1, DOMAIN_1:2; ::_thesis: verum
end;
theorem Th7: :: NORMFORM:7
for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] holds a /\ (b \/ a) = a
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b being Element of [:A,B:] holds a /\ (b \/ a) = a
let a, b be Element of [:A,B:]; ::_thesis: a /\ (b \/ a) = a
thus a /\ (b \/ a) = (a /\ b) \/ (a /\ a) by Th5
.= a by Th6 ; ::_thesis: verum
end;
theorem :: NORMFORM:8
for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] holds a \/ (b /\ c) = (a \/ b) /\ (a \/ c)
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] holds a \/ (b /\ c) = (a \/ b) /\ (a \/ c)
let a, b, c be Element of [:A,B:]; ::_thesis: a \/ (b /\ c) = (a \/ b) /\ (a \/ c)
thus a \/ (b /\ c) = (a \/ (c /\ a)) \/ (c /\ b) by Th6
.= a \/ ((c /\ a) \/ (c /\ b)) by Th3
.= a \/ (c /\ (a \/ b)) by Th5
.= ((a \/ b) /\ a) \/ ((a \/ b) /\ c) by Th7
.= (a \/ b) /\ (a \/ c) by Th5 ; ::_thesis: verum
end;
theorem Th9: :: NORMFORM:9
for A, B being non empty preBoolean set
for a, c, b being Element of [:A,B:] st a c= c & b c= c holds
a \/ b c= c
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, c, b being Element of [:A,B:] st a c= c & b c= c holds
a \/ b c= c
let a, c, b be Element of [:A,B:]; ::_thesis: ( a c= c & b c= c implies a \/ b c= c )
assume ( a `1 c= c `1 & a `2 c= c `2 & b `1 c= c `1 & b `2 c= c `2 ) ; :: according to NORMFORM:def_1 ::_thesis: a \/ b c= c
then ( (a `1) \/ (b `1) c= c `1 & (a `2) \/ (b `2) c= c `2 ) by XBOOLE_1:8;
hence ( (a \/ b) `1 c= c `1 & (a \/ b) `2 c= c `2 ) by MCART_1:7; :: according to NORMFORM:def_1 ::_thesis: verum
end;
theorem Th10: :: NORMFORM:10
for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] holds
( a c= a \/ b & b c= a \/ b )
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b being Element of [:A,B:] holds
( a c= a \/ b & b c= a \/ b )
let a, b be Element of [:A,B:]; ::_thesis: ( a c= a \/ b & b c= a \/ b )
( (a \/ b) `1 = (a `1) \/ (b `1) & (a \/ b) `2 = (a `2) \/ (b `2) ) by MCART_1:7;
hence ( a `1 c= (a \/ b) `1 & a `2 c= (a \/ b) `2 & b `1 c= (a \/ b) `1 & b `2 c= (a \/ b) `2 ) by XBOOLE_1:7; :: according to NORMFORM:def_1 ::_thesis: verum
end;
theorem :: NORMFORM:11
for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] st a = a \/ b holds
b c= a by Th10;
theorem Th12: :: NORMFORM:12
for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] st a c= b holds
( c \/ a c= c \/ b & a \/ c c= b \/ c )
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] st a c= b holds
( c \/ a c= c \/ b & a \/ c c= b \/ c )
let a, b, c be Element of [:A,B:]; ::_thesis: ( a c= b implies ( c \/ a c= c \/ b & a \/ c c= b \/ c ) )
assume A1: ( a `1 c= b `1 & a `2 c= b `2 ) ; :: according to NORMFORM:def_1 ::_thesis: ( c \/ a c= c \/ b & a \/ c c= b \/ c )
A2: ( (c \/ b) `1 = (c `1) \/ (b `1) & (c \/ b) `2 = (c `2) \/ (b `2) ) by MCART_1:7;
( (c \/ a) `1 = (c `1) \/ (a `1) & (c \/ a) `2 = (c `2) \/ (a `2) ) by MCART_1:7;
hence ( (c \/ a) `1 c= (c \/ b) `1 & (c \/ a) `2 c= (c \/ b) `2 ) by A1, A2, XBOOLE_1:9; :: according to NORMFORM:def_1 ::_thesis: a \/ c c= b \/ c
A3: ( (b \/ c) `1 = (b `1) \/ (c `1) & (b \/ c) `2 = (b `2) \/ (c `2) ) by MCART_1:7;
( (a \/ c) `1 = (a `1) \/ (c `1) & (a \/ c) `2 = (a `2) \/ (c `2) ) by MCART_1:7;
hence ( (a \/ c) `1 c= (b \/ c) `1 & (a \/ c) `2 c= (b \/ c) `2 ) by A1, A3, XBOOLE_1:9; :: according to NORMFORM:def_1 ::_thesis: verum
end;
theorem :: NORMFORM:13
for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] holds (a \ b) \/ b = a \/ b
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b being Element of [:A,B:] holds (a \ b) \/ b = a \/ b
let a, b be Element of [:A,B:]; ::_thesis: (a \ b) \/ b = a \/ b
A1: (a \ b) `1 = (a `1) \ (b `1) by MCART_1:7;
( ((a `1) \ (b `1)) \/ (b `1) = (a `1) \/ (b `1) & ((a `2) \ (b `2)) \/ (b `2) = (a `2) \/ (b `2) ) by XBOOLE_1:39;
hence (a \ b) \/ b = a \/ b by A1, MCART_1:7; ::_thesis: verum
end;
theorem :: NORMFORM:14
for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] st a \ b c= c holds
a c= b \/ c
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] st a \ b c= c holds
a c= b \/ c
let a, b, c be Element of [:A,B:]; ::_thesis: ( a \ b c= c implies a c= b \/ c )
assume that
A1: (a \ b) `1 c= c `1 and
A2: (a \ b) `2 c= c `2 ; :: according to NORMFORM:def_1 ::_thesis: a c= b \/ c
(a `2) \ (b `2) c= c `2 by A2, MCART_1:7;
then A3: a `2 c= (b `2) \/ (c `2) by XBOOLE_1:44;
(a `1) \ (b `1) c= c `1 by A1, MCART_1:7;
then a `1 c= (b `1) \/ (c `1) by XBOOLE_1:44;
hence ( a `1 c= (b \/ c) `1 & a `2 c= (b \/ c) `2 ) by A3, MCART_1:7; :: according to NORMFORM:def_1 ::_thesis: verum
end;
theorem :: NORMFORM:15
for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] st a c= b \/ c holds
a \ c c= b
proof
let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] st a c= b \/ c holds
a \ c c= b
let a, b, c be Element of [:A,B:]; ::_thesis: ( a c= b \/ c implies a \ c c= b )
A1: ( (b \/ c) `1 = (b `1) \/ (c `1) & (b \/ c) `2 = (b `2) \/ (c `2) ) by MCART_1:7;
A2: ( (a \ c) `1 = (a `1) \ (c `1) & (a \ c) `2 = (a `2) \ (c `2) ) by MCART_1:7;
assume ( a `1 c= (b \/ c) `1 & a `2 c= (b \/ c) `2 ) ; :: according to NORMFORM:def_1 ::_thesis: a \ c c= b
hence ( (a \ c) `1 c= b `1 & (a \ c) `2 c= b `2 ) by A1, A2, XBOOLE_1:43; :: according to NORMFORM:def_1 ::_thesis: verum
end;
definition
let A be set ;
func FinPairUnion A -> BinOp of [:(Fin A),(Fin A):] means :Def6: :: NORMFORM:def 6
for x, y being Element of [:(Fin A),(Fin A):] holds it . (x,y) = x \/ y;
existence
ex b1 being BinOp of [:(Fin A),(Fin A):] st
for x, y being Element of [:(Fin A),(Fin A):] holds b1 . (x,y) = x \/ y
proof
deffunc H1( Element of [:(Fin A),(Fin A):], Element of [:(Fin A),(Fin A):]) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2;
ex IT being BinOp of [:(Fin A),(Fin A):] st
for x, y being Element of [:(Fin A),(Fin A):] holds IT . (x,y) = H1(x,y) from BINOP_1:sch_4();
hence ex b1 being BinOp of [:(Fin A),(Fin A):] st
for x, y being Element of [:(Fin A),(Fin A):] holds b1 . (x,y) = x \/ y ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of [:(Fin A),(Fin A):] st ( for x, y being Element of [:(Fin A),(Fin A):] holds b1 . (x,y) = x \/ y ) & ( for x, y being Element of [:(Fin A),(Fin A):] holds b2 . (x,y) = x \/ y ) holds
b1 = b2
proof
let IT, IT9 be BinOp of [:(Fin A),(Fin A):]; ::_thesis: ( ( for x, y being Element of [:(Fin A),(Fin A):] holds IT . (x,y) = x \/ y ) & ( for x, y being Element of [:(Fin A),(Fin A):] holds IT9 . (x,y) = x \/ y ) implies IT = IT9 )
assume that
A1: for x, y being Element of [:(Fin A),(Fin A):] holds IT . (x,y) = x \/ y and
A2: for x, y being Element of [:(Fin A),(Fin A):] holds IT9 . (x,y) = x \/ y ; ::_thesis: IT = IT9
now__::_thesis:_for_x,_y_being_Element_of_[:(Fin_A),(Fin_A):]_holds_IT_._(x,y)_=_IT9_._(x,y)
let x, y be Element of [:(Fin A),(Fin A):]; ::_thesis: IT . (x,y) = IT9 . (x,y)
thus IT . (x,y) = x \/ y by A1
.= IT9 . (x,y) by A2 ; ::_thesis: verum
end;
hence IT = IT9 by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines FinPairUnion NORMFORM:def_6_:_
for A being set
for b2 being BinOp of [:(Fin A),(Fin A):] holds
( b2 = FinPairUnion A iff for x, y being Element of [:(Fin A),(Fin A):] holds b2 . (x,y) = x \/ y );
definition
let X be non empty set ;
let A be set ;
let B be Element of Fin X;
let f be Function of X,[:(Fin A),(Fin A):];
func FinPairUnion (B,f) -> Element of [:(Fin A),(Fin A):] equals :: NORMFORM:def 7
(FinPairUnion A) $$ (B,f);
correctness
coherence
(FinPairUnion A) $$ (B,f) is Element of [:(Fin A),(Fin A):];
;
end;
:: deftheorem defines FinPairUnion NORMFORM:def_7_:_
for X being non empty set
for A being set
for B being Element of Fin X
for f being Function of X,[:(Fin A),(Fin A):] holds FinPairUnion (B,f) = (FinPairUnion A) $$ (B,f);
Lm1: for A being set holds FinPairUnion A is idempotent
proof
let A be set ; ::_thesis: FinPairUnion A is idempotent
let a be Element of [:(Fin A),(Fin A):]; :: according to BINOP_1:def_4 ::_thesis: (FinPairUnion A) . (a,a) = a
thus (FinPairUnion A) . (a,a) = a \/ a by Def6
.= a ; ::_thesis: verum
end;
Lm2: for A being set holds FinPairUnion A is commutative
proof
let A be set ; ::_thesis: FinPairUnion A is commutative
let a, b be Element of [:(Fin A),(Fin A):]; :: according to BINOP_1:def_2 ::_thesis: (FinPairUnion A) . (a,b) = (FinPairUnion A) . (b,a)
thus (FinPairUnion A) . (a,b) = b \/ a by Def6
.= (FinPairUnion A) . (b,a) by Def6 ; ::_thesis: verum
end;
Lm3: for A being set holds FinPairUnion A is associative
proof
let A be set ; ::_thesis: FinPairUnion A is associative
let a, b, c be Element of [:(Fin A),(Fin A):]; :: according to BINOP_1:def_3 ::_thesis: (FinPairUnion A) . (a,((FinPairUnion A) . (b,c))) = (FinPairUnion A) . (((FinPairUnion A) . (a,b)),c)
thus (FinPairUnion A) . (a,((FinPairUnion A) . (b,c))) = a \/ ((FinPairUnion A) . (b,c)) by Def6
.= a \/ (b \/ c) by Def6
.= (a \/ b) \/ c by Th3
.= ((FinPairUnion A) . (a,b)) \/ c by Def6
.= (FinPairUnion A) . (((FinPairUnion A) . (a,b)),c) by Def6 ; ::_thesis: verum
end;
registration
let A be set ;
cluster FinPairUnion A -> commutative associative idempotent ;
coherence
( FinPairUnion A is commutative & FinPairUnion A is idempotent & FinPairUnion A is associative ) by Lm1, Lm2, Lm3;
end;
theorem :: NORMFORM:16
for A being set
for X being non empty set
for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for x being Element of X st x in B holds
f . x c= FinPairUnion (B,f)
proof
let A be set ; ::_thesis: for X being non empty set
for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for x being Element of X st x in B holds
f . x c= FinPairUnion (B,f)
let X be non empty set ; ::_thesis: for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for x being Element of X st x in B holds
f . x c= FinPairUnion (B,f)
let f be Function of X,[:(Fin A),(Fin A):]; ::_thesis: for B being Element of Fin X
for x being Element of X st x in B holds
f . x c= FinPairUnion (B,f)
let B be Element of Fin X; ::_thesis: for x being Element of X st x in B holds
f . x c= FinPairUnion (B,f)
let x be Element of X; ::_thesis: ( x in B implies f . x c= FinPairUnion (B,f) )
assume A1: x in B ; ::_thesis: f . x c= FinPairUnion (B,f)
then (FinPairUnion A) $$ (B,f) = (FinPairUnion A) $$ ((B \/ {.x.}),f) by ZFMISC_1:40
.= (FinPairUnion A) . (((FinPairUnion A) $$ (B,f)),(f . x)) by A1, SETWISEO:20
.= ((FinPairUnion A) $$ (B,f)) \/ (f . x) by Def6 ;
hence f . x c= FinPairUnion (B,f) by Th10; ::_thesis: verum
end;
theorem Th17: :: NORMFORM:17
for A being set holds [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A
proof
let A be set ; ::_thesis: [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A
now__::_thesis:_for_x_being_Element_of_[:(Fin_A),(Fin_A):]_holds_(FinPairUnion_A)_._([({}._A),({}._A)],x)_=_x
let x be Element of [:(Fin A),(Fin A):]; ::_thesis: (FinPairUnion A) . ([({}. A),({}. A)],x) = x
thus (FinPairUnion A) . ([({}. A),({}. A)],x) = [({}. A),({}. A)] \/ x by Def6
.= x by MCART_1:21 ; ::_thesis: verum
end;
hence [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by BINOP_1:4; ::_thesis: verum
end;
theorem Th18: :: NORMFORM:18
for A being set holds FinPairUnion A is having_a_unity
proof
let A be set ; ::_thesis: FinPairUnion A is having_a_unity
[({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by Th17;
hence FinPairUnion A is having_a_unity by SETWISEO:def_2; ::_thesis: verum
end;
theorem Th19: :: NORMFORM:19
for A being set holds the_unity_wrt (FinPairUnion A) = [({}. A),({}. A)]
proof
let A be set ; ::_thesis: the_unity_wrt (FinPairUnion A) = [({}. A),({}. A)]
[({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by Th17;
hence the_unity_wrt (FinPairUnion A) = [({}. A),({}. A)] by BINOP_1:def_8; ::_thesis: verum
end;
theorem Th20: :: NORMFORM:20
for A being set
for x being Element of [:(Fin A),(Fin A):] holds the_unity_wrt (FinPairUnion A) c= x
proof
let A be set ; ::_thesis: for x being Element of [:(Fin A),(Fin A):] holds the_unity_wrt (FinPairUnion A) c= x
let x be Element of [:(Fin A),(Fin A):]; ::_thesis: the_unity_wrt (FinPairUnion A) c= x
[({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by Th17;
then the_unity_wrt (FinPairUnion A) = [{},{}] by BINOP_1:def_8;
then ( (the_unity_wrt (FinPairUnion A)) `1 = {} & (the_unity_wrt (FinPairUnion A)) `2 = {} ) by MCART_1:7;
hence ( (the_unity_wrt (FinPairUnion A)) `1 c= x `1 & (the_unity_wrt (FinPairUnion A)) `2 c= x `2 ) by XBOOLE_1:2; :: according to NORMFORM:def_1 ::_thesis: verum
end;
theorem :: NORMFORM:21
for A being set
for X being non empty set
for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds
f . x c= c ) holds
FinPairUnion (B,f) c= c
proof
let A be set ; ::_thesis: for X being non empty set
for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds
f . x c= c ) holds
FinPairUnion (B,f) c= c
let X be non empty set ; ::_thesis: for f being Function of X,[:(Fin A),(Fin A):]
for B being Element of Fin X
for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds
f . x c= c ) holds
FinPairUnion (B,f) c= c
let f be Function of X,[:(Fin A),(Fin A):]; ::_thesis: for B being Element of Fin X
for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds
f . x c= c ) holds
FinPairUnion (B,f) c= c
let B be Element of Fin X; ::_thesis: for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds
f . x c= c ) holds
FinPairUnion (B,f) c= c
let c be Element of [:(Fin A),(Fin A):]; ::_thesis: ( ( for x being Element of X st x in B holds
f . x c= c ) implies FinPairUnion (B,f) c= c )
defpred S1[ Element of Fin X] means ( $1 c= B implies (FinPairUnion A) $$ ($1,f) c= c );
assume A1: for x being Element of X st x in B holds
f . x c= c ; ::_thesis: FinPairUnion (B,f) c= c
A2: now__::_thesis:_for_C_being_Element_of_Fin_X
for_b_being_Element_of_X_st_S1[C]_holds_
S1[C_\/_{.b.}]
let C be Element of Fin X; ::_thesis: for b being Element of X st S1[C] holds
S1[C \/ {.b.}]
let b be Element of X; ::_thesis: ( S1[C] implies S1[C \/ {.b.}] )
assume A3: S1[C] ; ::_thesis: S1[C \/ {.b.}]
now__::_thesis:_(_C_\/_{b}_c=_B_implies_(FinPairUnion_A)_$$_((C_\/_{.b.}),f)_c=_c_)
assume A4: C \/ {b} c= B ; ::_thesis: (FinPairUnion A) $$ ((C \/ {.b.}),f) c= c
then {b} c= B by XBOOLE_1:11;
then b in B by ZFMISC_1:31;
then A5: f . b c= c by A1;
(FinPairUnion A) $$ ((C \/ {.b.}),f) = (FinPairUnion A) . (((FinPairUnion A) $$ (C,f)),(f . b)) by Th18, SETWISEO:32
.= ((FinPairUnion A) $$ (C,f)) \/ (f . b) by Def6 ;
hence (FinPairUnion A) $$ ((C \/ {.b.}),f) c= c by A3, A4, A5, Th9, XBOOLE_1:11; ::_thesis: verum
end;
hence S1[C \/ {.b.}] ; ::_thesis: verum
end;
A6: S1[ {}. X]
proof
assume {}. X c= B ; ::_thesis: (FinPairUnion A) $$ (({}. X),f) c= c
(FinPairUnion A) $$ (({}. X),f) = the_unity_wrt (FinPairUnion A) by Th18, SETWISEO:31;
hence (FinPairUnion A) $$ (({}. X),f) c= c by Th20; ::_thesis: verum
end;
for C being Element of Fin X holds S1[C] from SETWISEO:sch_4(A6, A2);
hence FinPairUnion (B,f) c= c ; ::_thesis: verum
end;
theorem :: NORMFORM:22
for A being set
for X being non empty set
for B being Element of Fin X
for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds
FinPairUnion (B,f) = FinPairUnion (B,g)
proof
let A be set ; ::_thesis: for X being non empty set
for B being Element of Fin X
for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds
FinPairUnion (B,f) = FinPairUnion (B,g)
let X be non empty set ; ::_thesis: for B being Element of Fin X
for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds
FinPairUnion (B,f) = FinPairUnion (B,g)
let B be Element of Fin X; ::_thesis: for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds
FinPairUnion (B,f) = FinPairUnion (B,g)
let f, g be Function of X,[:(Fin A),(Fin A):]; ::_thesis: ( f | B = g | B implies FinPairUnion (B,f) = FinPairUnion (B,g) )
set J = FinPairUnion A;
A1: [({}. A),({}. A)] = the_unity_wrt (FinPairUnion A) by Th19;
assume A2: f | B = g | B ; ::_thesis: FinPairUnion (B,f) = FinPairUnion (B,g)
now__::_thesis:_FinPairUnion_(B,f)_=_FinPairUnion_(B,g)
percases ( B = {} or B <> {} ) ;
supposeA3: B = {} ; ::_thesis: FinPairUnion (B,f) = FinPairUnion (B,g)
hence FinPairUnion (B,f) = (FinPairUnion A) $$ (({}. X),f)
.= [({}. A),({}. A)] by A1, Th18, SETWISEO:31
.= (FinPairUnion A) $$ (({}. X),g) by A1, Th18, SETWISEO:31
.= FinPairUnion (B,g) by A3 ;
::_thesis: verum
end;
supposeA4: B <> {} ; ::_thesis: FinPairUnion (B,f) = FinPairUnion (B,g)
f .: B = g .: B by A2, RELAT_1:166;
hence FinPairUnion (B,f) = FinPairUnion (B,g) by A4, SETWISEO:26; ::_thesis: verum
end;
end;
end;
hence FinPairUnion (B,f) = FinPairUnion (B,g) ; ::_thesis: verum
end;
definition
let X be set ;
func DISJOINT_PAIRS X -> Subset of [:(Fin X),(Fin X):] equals :: NORMFORM:def 8
{ a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;
coherence
{ a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } is Subset of [:(Fin X),(Fin X):]
proof
set D = { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;
{ a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } c= [:(Fin X),(Fin X):]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } or x in [:(Fin X),(Fin X):] )
assume x in { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ; ::_thesis: x in [:(Fin X),(Fin X):]
then ex a being Element of [:(Fin X),(Fin X):] st
( x = a & a `1 misses a `2 ) ;
hence x in [:(Fin X),(Fin X):] ; ::_thesis: verum
end;
hence { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } is Subset of [:(Fin X),(Fin X):] ; ::_thesis: verum
end;
end;
:: deftheorem defines DISJOINT_PAIRS NORMFORM:def_8_:_
for X being set holds DISJOINT_PAIRS X = { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;
registration
let X be set ;
cluster DISJOINT_PAIRS X -> non empty ;
coherence
not DISJOINT_PAIRS X is empty
proof
{} is Element of Fin X by FINSUB_1:7;
then reconsider b = [{},{}] as Element of [:(Fin X),(Fin X):] by ZFMISC_1:def_2;
b `1 = {} by MCART_1:7;
then b `1 misses b `2 by XBOOLE_1:65;
then b in { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;
hence not DISJOINT_PAIRS X is empty ; ::_thesis: verum
end;
end;
theorem Th23: :: NORMFORM:23
for X being set
for y being Element of [:(Fin X),(Fin X):] holds
( y in DISJOINT_PAIRS X iff y `1 misses y `2 )
proof
let X be set ; ::_thesis: for y being Element of [:(Fin X),(Fin X):] holds
( y in DISJOINT_PAIRS X iff y `1 misses y `2 )
let y be Element of [:(Fin X),(Fin X):]; ::_thesis: ( y in DISJOINT_PAIRS X iff y `1 misses y `2 )
( y in DISJOINT_PAIRS X iff ex a being Element of [:(Fin X),(Fin X):] st
( y = a & a `1 misses a `2 ) ) ;
hence ( y in DISJOINT_PAIRS X iff y `1 misses y `2 ) ; ::_thesis: verum
end;
theorem :: NORMFORM:24
for X being set
for y, x being Element of [:(Fin X),(Fin X):] st y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X holds
( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} )
proof
let X be set ; ::_thesis: for y, x being Element of [:(Fin X),(Fin X):] st y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X holds
( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} )
let y, x be Element of [:(Fin X),(Fin X):]; ::_thesis: ( y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X implies ( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} ) )
assume that
A1: y in DISJOINT_PAIRS X and
A2: x in DISJOINT_PAIRS X ; ::_thesis: ( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} )
A3: ( ((y `1) \/ (x `1)) /\ ((y `2) \/ (x `2)) = (((y `1) \/ (x `1)) /\ (y `2)) \/ (((y `1) \/ (x `1)) /\ (x `2)) & ((y `1) \/ (x `1)) /\ (y `2) = ((y `1) /\ (y `2)) \/ ((x `1) /\ (y `2)) ) by XBOOLE_1:23;
x `1 misses x `2 by A2, Th23;
then A4: (x `1) /\ (x `2) = {} by XBOOLE_0:def_7;
y `1 misses y `2 by A1, Th23;
then A5: (y `1) /\ (y `2) = {} by XBOOLE_0:def_7;
A6: ((y `1) \/ (x `1)) /\ (x `2) = ((y `1) /\ (x `2)) \/ ((x `1) /\ (x `2)) by XBOOLE_1:23;
A7: ( (y \/ x) `1 = (y `1) \/ (x `1) & (y \/ x) `2 = (y `2) \/ (x `2) ) by MCART_1:7;
hereby ::_thesis: ( ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} implies y \/ x in DISJOINT_PAIRS X )
assume y \/ x in DISJOINT_PAIRS X ; ::_thesis: ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {}
then (y \/ x) `1 misses (y \/ x) `2 by Th23;
hence ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} by A5, A4, A7, A3, A6, XBOOLE_0:def_7; ::_thesis: verum
end;
assume ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} ; ::_thesis: y \/ x in DISJOINT_PAIRS X
then (y \/ x) `1 misses (y \/ x) `2 by A5, A4, A7, A3, A6, XBOOLE_0:def_7;
hence y \/ x in DISJOINT_PAIRS X ; ::_thesis: verum
end;
theorem :: NORMFORM:25
for X being set
for a being Element of DISJOINT_PAIRS X holds a `1 misses a `2 by Th23;
theorem Th26: :: NORMFORM:26
for X being set
for x being Element of [:(Fin X),(Fin X):]
for b being Element of DISJOINT_PAIRS X st x c= b holds
x is Element of DISJOINT_PAIRS X
proof
let X be set ; ::_thesis: for x being Element of [:(Fin X),(Fin X):]
for b being Element of DISJOINT_PAIRS X st x c= b holds
x is Element of DISJOINT_PAIRS X
let x be Element of [:(Fin X),(Fin X):]; ::_thesis: for b being Element of DISJOINT_PAIRS X st x c= b holds
x is Element of DISJOINT_PAIRS X
let b be Element of DISJOINT_PAIRS X; ::_thesis: ( x c= b implies x is Element of DISJOINT_PAIRS X )
assume A1: ( x `1 c= b `1 & x `2 c= b `2 ) ; :: according to NORMFORM:def_1 ::_thesis: x is Element of DISJOINT_PAIRS X
b `1 misses b `2 by Th23;
then x `1 misses x `2 by A1, XBOOLE_1:64;
hence x is Element of DISJOINT_PAIRS X by Th23; ::_thesis: verum
end;
theorem Th27: :: NORMFORM:27
for X being set
for a being Element of DISJOINT_PAIRS X
for x being set holds
( not x in a `1 or not x in a `2 )
proof
let X be set ; ::_thesis: for a being Element of DISJOINT_PAIRS X
for x being set holds
( not x in a `1 or not x in a `2 )
let a be Element of DISJOINT_PAIRS X; ::_thesis: for x being set holds
( not x in a `1 or not x in a `2 )
a `1 misses a `2 by Th23;
hence for x being set holds
( not x in a `1 or not x in a `2 ) by XBOOLE_0:3; ::_thesis: verum
end;
theorem :: NORMFORM:28
for X being set
for a, b being Element of DISJOINT_PAIRS X st not a \/ b in DISJOINT_PAIRS X holds
ex p being Element of X st
( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) )
proof
let X be set ; ::_thesis: for a, b being Element of DISJOINT_PAIRS X st not a \/ b in DISJOINT_PAIRS X holds
ex p being Element of X st
( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) )
let a, b be Element of DISJOINT_PAIRS X; ::_thesis: ( not a \/ b in DISJOINT_PAIRS X implies ex p being Element of X st
( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) ) )
set p = the Element of ((a \/ b) `1) /\ ((a \/ b) `2);
assume not a \/ b in DISJOINT_PAIRS X ; ::_thesis: ex p being Element of X st
( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) )
then (a \/ b) `1 meets (a \/ b) `2 ;
then A1: ((a \/ b) `1) /\ ((a \/ b) `2) <> {} by XBOOLE_0:def_7;
((a \/ b) `1) /\ ((a \/ b) `2) is Subset of X by FINSUB_1:17;
then reconsider p = the Element of ((a \/ b) `1) /\ ((a \/ b) `2) as Element of X by A1, TARSKI:def_3;
p in (a \/ b) `2 by A1, XBOOLE_0:def_4;
then p in (a `2) \/ (b `2) by MCART_1:7;
then A2: ( p in b `2 or p in a `2 ) by XBOOLE_0:def_3;
take p ; ::_thesis: ( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) )
p in (a \/ b) `1 by A1, XBOOLE_0:def_4;
then p in (a `1) \/ (b `1) by MCART_1:7;
then ( p in a `1 or p in b `1 ) by XBOOLE_0:def_3;
hence ( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) ) by A2, Th27; ::_thesis: verum
end;
theorem :: NORMFORM:29
for X being set
for x being Element of [:(Fin X),(Fin X):] st x `1 misses x `2 holds
x is Element of DISJOINT_PAIRS X by Th23;
theorem :: NORMFORM:30
for X being set
for a being Element of DISJOINT_PAIRS X
for V, W being set st V c= a `1 & W c= a `2 holds
[V,W] is Element of DISJOINT_PAIRS X
proof
let X be set ; ::_thesis: for a being Element of DISJOINT_PAIRS X
for V, W being set st V c= a `1 & W c= a `2 holds
[V,W] is Element of DISJOINT_PAIRS X
let a be Element of DISJOINT_PAIRS X; ::_thesis: for V, W being set st V c= a `1 & W c= a `2 holds
[V,W] is Element of DISJOINT_PAIRS X
let V, W be set ; ::_thesis: ( V c= a `1 & W c= a `2 implies [V,W] is Element of DISJOINT_PAIRS X )
A1: [V,W] `2 = W ;
assume A2: ( V c= a `1 & W c= a `2 ) ; ::_thesis: [V,W] is Element of DISJOINT_PAIRS X
then ( V is Element of Fin X & W is Element of Fin X ) by SETWISEO:11;
then reconsider x = [V,W] as Element of [:(Fin X),(Fin X):] by ZFMISC_1:def_2;
( a `1 misses a `2 & [V,W] `1 = V ) by Th23;
then x `1 misses x `2 by A1, A2, XBOOLE_1:64;
hence [V,W] is Element of DISJOINT_PAIRS X by Th23; ::_thesis: verum
end;
Lm4: for A being set holds {} in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b }
proof
let A be set ; ::_thesis: {} in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b }
( {} is Element of Fin (DISJOINT_PAIRS A) & ( for a, b being Element of DISJOINT_PAIRS A st a in {} & b in {} & a c= b holds
a = b ) ) by FINSUB_1:7;
hence {} in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } ; ::_thesis: verum
end;
definition
let A be set ;
func Normal_forms_on A -> Subset of (Fin (DISJOINT_PAIRS A)) equals :: NORMFORM:def 9
{ B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } ;
coherence
{ B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } is Subset of (Fin (DISJOINT_PAIRS A))
proof
set IT = { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } ;
{ B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } c= Fin (DISJOINT_PAIRS A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } or x in Fin (DISJOINT_PAIRS A) )
assume x in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } ; ::_thesis: x in Fin (DISJOINT_PAIRS A)
then ex B being Element of Fin (DISJOINT_PAIRS A) st
( x = B & ( for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b ) ) ;
hence x in Fin (DISJOINT_PAIRS A) ; ::_thesis: verum
end;
hence { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } is Subset of (Fin (DISJOINT_PAIRS A)) ; ::_thesis: verum
end;
end;
:: deftheorem defines Normal_forms_on NORMFORM:def_9_:_
for A being set holds Normal_forms_on A = { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } ;
registration
let A be set ;
cluster Normal_forms_on A -> non empty ;
coherence
not Normal_forms_on A is empty by Lm4;
end;
theorem :: NORMFORM:31
for A being set holds {} in Normal_forms_on A by Lm4;
theorem Th32: :: NORMFORM:32
for A being set
for a, b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds
a = b
proof
let A be set ; ::_thesis: for a, b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds
a = b
let a, b be Element of DISJOINT_PAIRS A; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds
a = b
let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( B in Normal_forms_on A & a in B & b in B & a c= b implies a = b )
assume B in Normal_forms_on A ; ::_thesis: ( not a in B or not b in B or not a c= b or a = b )
then ex C being Element of Fin (DISJOINT_PAIRS A) st
( B = C & ( for a, b being Element of DISJOINT_PAIRS A st a in C & b in C & a c= b holds
a = b ) ) ;
hence ( not a in B or not b in B or not a c= b or a = b ) ; ::_thesis: verum
end;
theorem Th33: :: NORMFORM:33
for A being set
for B being Element of Fin (DISJOINT_PAIRS A) st ( for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b ) holds
B in Normal_forms_on A ;
definition
let A be set ;
let B be Element of Fin (DISJOINT_PAIRS A);
func mi B -> Element of Normal_forms_on A equals :: NORMFORM:def 10
{ t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } ;
coherence
{ t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } is Element of Normal_forms_on A
proof
set M = { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } ;
now__::_thesis:_for_x_being_set_st_x_in__{__t_where_t_is_Element_of_DISJOINT_PAIRS_A_:_for_s_being_Element_of_DISJOINT_PAIRS_A_holds_
(_(_s_in_B_&_s_c=_t_)_iff_s_=_t_)__}__holds_
x_in_B
let x be set ; ::_thesis: ( x in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } implies x in B )
assume x in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } ; ::_thesis: x in B
then ex t being Element of DISJOINT_PAIRS A st
( x = t & ( for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) ) ) ;
hence x in B ; ::_thesis: verum
end;
then A1: { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } c= B by TARSKI:def_3;
then A2: { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } is finite by FINSET_1:1;
B c= DISJOINT_PAIRS A by FINSUB_1:def_5;
then { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } c= DISJOINT_PAIRS A by A1, XBOOLE_1:1;
then reconsider M9 = { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } as Element of Fin (DISJOINT_PAIRS A) by A2, FINSUB_1:def_5;
now__::_thesis:_for_c,_d_being_Element_of_DISJOINT_PAIRS_A_st_c_in__{__t_where_t_is_Element_of_DISJOINT_PAIRS_A_:_for_s_being_Element_of_DISJOINT_PAIRS_A_holds_
(_(_s_in_B_&_s_c=_t_)_iff_s_=_t_)__}__&_d_in__{__t_where_t_is_Element_of_DISJOINT_PAIRS_A_:_for_s_being_Element_of_DISJOINT_PAIRS_A_holds_
(_(_s_in_B_&_s_c=_t_)_iff_s_=_t_)__}__&_c_c=_d_holds_
c_=_d
let c, d be Element of DISJOINT_PAIRS A; ::_thesis: ( c in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } & d in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } & c c= d implies c = d )
assume c in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } ; ::_thesis: ( d in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } & c c= d implies c = d )
then ex t being Element of DISJOINT_PAIRS A st
( c = t & ( for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) ) ) ;
then A3: c in B ;
assume d in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } ; ::_thesis: ( c c= d implies c = d )
then ex t being Element of DISJOINT_PAIRS A st
( d = t & ( for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) ) ) ;
hence ( c c= d implies c = d ) by A3; ::_thesis: verum
end;
then M9 is Element of Normal_forms_on A by Th33;
hence { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } is Element of Normal_forms_on A ; ::_thesis: verum
end;
correctness
;
let C be Element of Fin (DISJOINT_PAIRS A);
funcB ^ C -> Element of Fin (DISJOINT_PAIRS A) equals :: NORMFORM:def 11
(DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;
coherence
(DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is Element of Fin (DISJOINT_PAIRS A)
proof
deffunc H1( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2;
set M = (DISJOINT_PAIRS A) /\ { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;
A4: C is finite ;
A5: B is finite ;
{ H1(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is finite from FRAENKEL:sch_22(A5, A4);
then ( (DISJOINT_PAIRS A) /\ { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } c= DISJOINT_PAIRS A & (DISJOINT_PAIRS A) /\ { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is finite ) by FINSET_1:1, XBOOLE_1:17;
hence (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is Element of Fin (DISJOINT_PAIRS A) by FINSUB_1:def_5; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem defines mi NORMFORM:def_10_:_
for A being set
for B being Element of Fin (DISJOINT_PAIRS A) holds mi B = { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } ;
:: deftheorem defines ^ NORMFORM:def_11_:_
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;
theorem Th34: :: NORMFORM:34
for A being set
for x being Element of [:(Fin A),(Fin A):]
for B, C being Element of Fin (DISJOINT_PAIRS A) st x in B ^ C holds
ex b, c being Element of DISJOINT_PAIRS A st
( b in B & c in C & x = b \/ c )
proof
let A be set ; ::_thesis: for x being Element of [:(Fin A),(Fin A):]
for B, C being Element of Fin (DISJOINT_PAIRS A) st x in B ^ C holds
ex b, c being Element of DISJOINT_PAIRS A st
( b in B & c in C & x = b \/ c )
let x be Element of [:(Fin A),(Fin A):]; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st x in B ^ C holds
ex b, c being Element of DISJOINT_PAIRS A st
( b in B & c in C & x = b \/ c )
let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( x in B ^ C implies ex b, c being Element of DISJOINT_PAIRS A st
( b in B & c in C & x = b \/ c ) )
assume x in B ^ C ; ::_thesis: ex b, c being Element of DISJOINT_PAIRS A st
( b in B & c in C & x = b \/ c )
then x in { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } by XBOOLE_0:def_4;
then ex s, t being Element of DISJOINT_PAIRS A st
( x = s \/ t & s in B & t in C ) ;
hence ex b, c being Element of DISJOINT_PAIRS A st
( b in B & c in C & x = b \/ c ) ; ::_thesis: verum
end;
theorem Th35: :: NORMFORM:35
for A being set
for b, c being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st b in B & c in C & b \/ c in DISJOINT_PAIRS A holds
b \/ c in B ^ C
proof
let A be set ; ::_thesis: for b, c being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st b in B & c in C & b \/ c in DISJOINT_PAIRS A holds
b \/ c in B ^ C
let b, c be Element of DISJOINT_PAIRS A; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st b in B & c in C & b \/ c in DISJOINT_PAIRS A holds
b \/ c in B ^ C
let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( b in B & c in C & b \/ c in DISJOINT_PAIRS A implies b \/ c in B ^ C )
assume ( b in B & c in C ) ; ::_thesis: ( not b \/ c in DISJOINT_PAIRS A or b \/ c in B ^ C )
then A1: b \/ c in { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ;
assume b \/ c in DISJOINT_PAIRS A ; ::_thesis: b \/ c in B ^ C
hence b \/ c in B ^ C by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th36: :: NORMFORM:36
for A being set
for a, b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds
( a in B & ( b in B & b c= a implies b = a ) )
proof
let A be set ; ::_thesis: for a, b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds
( a in B & ( b in B & b c= a implies b = a ) )
let a, b be Element of DISJOINT_PAIRS A; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds
( a in B & ( b in B & b c= a implies b = a ) )
let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( a in mi B implies ( a in B & ( b in B & b c= a implies b = a ) ) )
assume a in mi B ; ::_thesis: ( a in B & ( b in B & b c= a implies b = a ) )
then ex t being Element of DISJOINT_PAIRS A st
( a = t & ( for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) ) ) ;
hence ( a in B & ( b in B & b c= a implies b = a ) ) ; ::_thesis: verum
end;
theorem :: NORMFORM:37
for A being set
for a being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds
a in B by Th36;
theorem :: NORMFORM:38
for A being set
for a, b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B & b in B & b c= a holds
b = a by Th36;
theorem Th39: :: NORMFORM:39
for A being set
for a being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds
b = a ) holds
a in mi B
proof
let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds
b = a ) holds
a in mi B
let a be Element of DISJOINT_PAIRS A; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) st a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds
b = a ) holds
a in mi B
let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds
b = a ) implies a in mi B )
assume ( a in B & ( for s being Element of DISJOINT_PAIRS A st s in B & s c= a holds
s = a ) ) ; ::_thesis: a in mi B
then for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= a ) iff s = a ) ;
hence a in mi B ; ::_thesis: verum
end;
definition
let A be non empty set ;
let B be non empty Subset of A;
let O be BinOp of B;
let a, b be Element of B;
:: original: .
redefine funcO . (a,b) -> Element of B;
coherence
O . (a,b) is Element of B
proof
thus O . (a,b) is Element of B ; ::_thesis: verum
end;
end;
Lm5: for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) st ( for a being Element of DISJOINT_PAIRS A st a in B holds
a in C ) holds
B c= C
proof
let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st ( for a being Element of DISJOINT_PAIRS A st a in B holds
a in C ) holds
B c= C
let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( ( for a being Element of DISJOINT_PAIRS A st a in B holds
a in C ) implies B c= C )
assume A1: for a being Element of DISJOINT_PAIRS A st a in B holds
a in C ; ::_thesis: B c= C
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in C )
assume A2: x in B ; ::_thesis: x in C
then x is Element of DISJOINT_PAIRS A by SETWISEO:9;
hence x in C by A1, A2; ::_thesis: verum
end;
theorem Th40: :: NORMFORM:40
for A being set
for B being Element of Fin (DISJOINT_PAIRS A) holds mi B c= B
proof
let A be set ; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) holds mi B c= B
let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi B c= B
for a being Element of DISJOINT_PAIRS A st a in mi B holds
a in B by Th36;
hence mi B c= B by Lm5; ::_thesis: verum
end;
theorem Th41: :: NORMFORM:41
for A being set
for b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st b in B holds
ex c being Element of DISJOINT_PAIRS A st
( c c= b & c in mi B )
proof
let A be set ; ::_thesis: for b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st b in B holds
ex c being Element of DISJOINT_PAIRS A st
( c c= b & c in mi B )
let b be Element of DISJOINT_PAIRS A; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) st b in B holds
ex c being Element of DISJOINT_PAIRS A st
( c c= b & c in mi B )
let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( b in B implies ex c being Element of DISJOINT_PAIRS A st
( c c= b & c in mi B ) )
assume A1: b in B ; ::_thesis: ex c being Element of DISJOINT_PAIRS A st
( c c= b & c in mi B )
defpred S1[ Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A] means $1 c= $2;
A2: for a being Element of DISJOINT_PAIRS A holds S1[a,a] ;
A3: for a, b, c being Element of DISJOINT_PAIRS A st S1[a,b] & S1[b,c] holds
S1[a,c] by Th2;
for a being Element of DISJOINT_PAIRS A st a in B holds
ex b being Element of DISJOINT_PAIRS A st
( b in B & S1[b,a] & ( for c being Element of DISJOINT_PAIRS A st c in B & S1[c,b] holds
S1[b,c] ) ) from FRAENKEL:sch_23(A2, A3);
then consider c being Element of DISJOINT_PAIRS A such that
A4: c in B and
A5: c c= b and
A6: for a being Element of DISJOINT_PAIRS A st a in B & a c= c holds
c c= a by A1;
take c ; ::_thesis: ( c c= b & c in mi B )
thus c c= b by A5; ::_thesis: c in mi B
now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_B_&_b_c=_c_holds_
b_=_c
let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in B & b c= c implies b = c )
assume that
A7: b in B and
A8: b c= c ; ::_thesis: b = c
c c= b by A6, A7, A8;
hence b = c by A8, Th1; ::_thesis: verum
end;
hence c in mi B by A4, Th39; ::_thesis: verum
end;
theorem Th42: :: NORMFORM:42
for A being set
for K being Element of Normal_forms_on A holds mi K = K
proof
let A be set ; ::_thesis: for K being Element of Normal_forms_on A holds mi K = K
let K be Element of Normal_forms_on A; ::_thesis: mi K = K
thus mi K c= K by Th40; :: according to XBOOLE_0:def_10 ::_thesis: K c= mi K
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_K_holds_
a_in_mi_K
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in K implies a in mi K )
assume A1: a in K ; ::_thesis: a in mi K
then for b being Element of DISJOINT_PAIRS A st b in K & b c= a holds
b = a by Th32;
hence a in mi K by A1, Th39; ::_thesis: verum
end;
hence K c= mi K by Lm5; ::_thesis: verum
end;
theorem Th43: :: NORMFORM:43
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B \/ C) c= (mi B) \/ C
proof
let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B \/ C) c= (mi B) \/ C
let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi (B \/ C) c= (mi B) \/ C
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_(B_\/_C)_holds_
a_in_(mi_B)_\/_C
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi (B \/ C) implies a in (mi B) \/ C )
assume A1: a in mi (B \/ C) ; ::_thesis: a in (mi B) \/ C
then A2: a in B \/ C by Th36;
now__::_thesis:_a_in_(mi_B)_\/_C
percases ( a in B or a in C ) by A2, XBOOLE_0:def_3;
supposeA3: a in B ; ::_thesis: a in (mi B) \/ C
now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_B_&_b_c=_a_holds_
b_=_a
let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in B & b c= a implies b = a )
assume b in B ; ::_thesis: ( b c= a implies b = a )
then b in B \/ C by XBOOLE_0:def_3;
hence ( b c= a implies b = a ) by A1, Th36; ::_thesis: verum
end;
then a in mi B by A3, Th39;
hence a in (mi B) \/ C by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose a in C ; ::_thesis: a in (mi B) \/ C
hence a in (mi B) \/ C by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence a in (mi B) \/ C ; ::_thesis: verum
end;
hence mi (B \/ C) c= (mi B) \/ C by Lm5; ::_thesis: verum
end;
theorem Th44: :: NORMFORM:44
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) \/ C) = mi (B \/ C)
proof
let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) \/ C) = mi (B \/ C)
let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi ((mi B) \/ C) = mi (B \/ C)
A1: (mi B) \/ C c= B \/ C by Th40, XBOOLE_1:9;
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_((mi_B)_\/_C)_holds_
a_in_mi_(B_\/_C)
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi ((mi B) \/ C) implies a in mi (B \/ C) )
assume A2: a in mi ((mi B) \/ C) ; ::_thesis: a in mi (B \/ C)
A3: now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_B_\/_C_&_b_c=_a_holds_
b_=_a
let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in B \/ C & b c= a implies b = a )
assume that
A4: b in B \/ C and
A5: b c= a ; ::_thesis: b = a
now__::_thesis:_b_=_a
percases ( b in B or b in C ) by A4, XBOOLE_0:def_3;
suppose b in B ; ::_thesis: b = a
then consider c being Element of DISJOINT_PAIRS A such that
A6: c c= b and
A7: c in mi B by Th41;
( c in (mi B) \/ C & c c= a ) by A5, A6, A7, Th2, XBOOLE_0:def_3;
then c = a by A2, Th36;
hence b = a by A5, A6, Th1; ::_thesis: verum
end;
suppose b in C ; ::_thesis: b = a
then b in (mi B) \/ C by XBOOLE_0:def_3;
hence b = a by A2, A5, Th36; ::_thesis: verum
end;
end;
end;
hence b = a ; ::_thesis: verum
end;
a in (mi B) \/ C by A2, Th36;
hence a in mi (B \/ C) by A1, A3, Th39; ::_thesis: verum
end;
hence mi ((mi B) \/ C) c= mi (B \/ C) by Lm5; :: according to XBOOLE_0:def_10 ::_thesis: mi (B \/ C) c= mi ((mi B) \/ C)
A8: mi (B \/ C) c= (mi B) \/ C by Th43;
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_(B_\/_C)_holds_
a_in_mi_((mi_B)_\/_C)
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi (B \/ C) implies a in mi ((mi B) \/ C) )
assume A9: a in mi (B \/ C) ; ::_thesis: a in mi ((mi B) \/ C)
then for b being Element of DISJOINT_PAIRS A st b in (mi B) \/ C & b c= a holds
b = a by A1, Th36;
hence a in mi ((mi B) \/ C) by A8, A9, Th39; ::_thesis: verum
end;
hence mi (B \/ C) c= mi ((mi B) \/ C) by Lm5; ::_thesis: verum
end;
theorem :: NORMFORM:45
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B \/ (mi C)) = mi (B \/ C) by Th44;
theorem Th46: :: NORMFORM:46
for A being set
for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds
B ^ D c= C ^ D
proof
let A be set ; ::_thesis: for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds
B ^ D c= C ^ D
let B, C, D be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( B c= C implies B ^ D c= C ^ D )
deffunc H1( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2;
defpred S1[ set , set ] means ( $1 in B & $2 in D );
defpred S2[ set , set ] means ( $1 in C & $2 in D );
set X1 = { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } ;
set X2 = { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } ;
assume B c= C ; ::_thesis: B ^ D c= C ^ D
then A1: for s, t being Element of DISJOINT_PAIRS A st S1[s,t] holds
S2[s,t] ;
{ H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } c= { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } from FRAENKEL:sch_2(A1);
hence B ^ D c= C ^ D by XBOOLE_1:26; ::_thesis: verum
end;
Lm6: for A being set
for a being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds
ex b being Element of DISJOINT_PAIRS A st
( b c= a & b in (mi B) ^ C )
proof
let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds
ex b being Element of DISJOINT_PAIRS A st
( b c= a & b in (mi B) ^ C )
let a be Element of DISJOINT_PAIRS A; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds
ex b being Element of DISJOINT_PAIRS A st
( b c= a & b in (mi B) ^ C )
let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( a in B ^ C implies ex b being Element of DISJOINT_PAIRS A st
( b c= a & b in (mi B) ^ C ) )
assume a in B ^ C ; ::_thesis: ex b being Element of DISJOINT_PAIRS A st
( b c= a & b in (mi B) ^ C )
then consider b, c being Element of DISJOINT_PAIRS A such that
A1: b in B and
A2: c in C and
A3: a = b \/ c by Th34;
consider d being Element of DISJOINT_PAIRS A such that
A4: d c= b and
A5: d in mi B by A1, Th41;
d \/ c c= a by A3, A4, Th12;
then reconsider e = d \/ c as Element of DISJOINT_PAIRS A by Th26;
take e ; ::_thesis: ( e c= a & e in (mi B) ^ C )
thus e c= a by A3, A4, Th12; ::_thesis: e in (mi B) ^ C
thus e in (mi B) ^ C by A2, A5, Th35; ::_thesis: verum
end;
theorem Th47: :: NORMFORM:47
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ C) c= (mi B) ^ C
proof
let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ C) c= (mi B) ^ C
let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi (B ^ C) c= (mi B) ^ C
A1: (mi B) ^ C c= B ^ C by Th40, Th46;
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_(B_^_C)_holds_
a_in_(mi_B)_^_C
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi (B ^ C) implies a in (mi B) ^ C )
assume A2: a in mi (B ^ C) ; ::_thesis: a in (mi B) ^ C
then a in B ^ C by Th36;
then ex b being Element of DISJOINT_PAIRS A st
( b c= a & b in (mi B) ^ C ) by Lm6;
hence a in (mi B) ^ C by A1, A2, Th36; ::_thesis: verum
end;
hence mi (B ^ C) c= (mi B) ^ C by Lm5; ::_thesis: verum
end;
theorem Th48: :: NORMFORM:48
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = C ^ B
proof
let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = C ^ B
let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: B ^ C = C ^ B
deffunc H1( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2;
defpred S1[ set , set ] means ( $1 in B & $2 in C );
defpred S2[ set , set ] means ( $2 in C & $1 in B );
set X1 = { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } ;
set X2 = { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } ;
A1: for s, t being Element of DISJOINT_PAIRS A holds H1(s,t) = H1(t,s) ;
A2: now__::_thesis:_for_x_being_set_holds_
(_x_in__{__H1(t,s)_where_s,_t_is_Element_of_DISJOINT_PAIRS_A_:_S2[s,t]__}__iff_x_in__{__(t_\/_s)_where_t,_s_is_Element_of_DISJOINT_PAIRS_A_:_(_t_in_C_&_s_in_B_)__}__)
let x be set ; ::_thesis: ( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } )
( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff ex s, t being Element of DISJOINT_PAIRS A st
( x = t \/ s & t in C & s in B ) ) ;
then ( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff ex t, s being Element of DISJOINT_PAIRS A st
( x = t \/ s & t in C & s in B ) ) ;
hence ( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } ) ; ::_thesis: verum
end;
A3: for s, t being Element of DISJOINT_PAIRS A holds
( S1[s,t] iff S2[s,t] ) ;
{ H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } = { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } from FRAENKEL:sch_8(A3, A1);
hence B ^ C = C ^ B by A2, TARSKI:1; ::_thesis: verum
end;
theorem Th49: :: NORMFORM:49
for A being set
for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds
D ^ B c= D ^ C
proof
let A be set ; ::_thesis: for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds
D ^ B c= D ^ C
let B, C, D be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( B c= C implies D ^ B c= D ^ C )
( D ^ C = C ^ D & D ^ B = B ^ D ) by Th48;
hence ( B c= C implies D ^ B c= D ^ C ) by Th46; ::_thesis: verum
end;
theorem Th50: :: NORMFORM:50
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) ^ C) = mi (B ^ C)
proof
let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) ^ C) = mi (B ^ C)
let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi ((mi B) ^ C) = mi (B ^ C)
A1: (mi B) ^ C c= B ^ C by Th40, Th46;
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_((mi_B)_^_C)_holds_
a_in_mi_(B_^_C)
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi ((mi B) ^ C) implies a in mi (B ^ C) )
assume A2: a in mi ((mi B) ^ C) ; ::_thesis: a in mi (B ^ C)
A3: now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_B_^_C_&_b_c=_a_holds_
b_=_a
let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in B ^ C & b c= a implies b = a )
assume b in B ^ C ; ::_thesis: ( b c= a implies b = a )
then consider c being Element of DISJOINT_PAIRS A such that
A4: c c= b and
A5: c in (mi B) ^ C by Lm6;
assume A6: b c= a ; ::_thesis: b = a
then c c= a by A4, Th2;
then c = a by A2, A5, Th36;
hence b = a by A4, A6, Th1; ::_thesis: verum
end;
a in (mi B) ^ C by A2, Th36;
hence a in mi (B ^ C) by A1, A3, Th39; ::_thesis: verum
end;
hence mi ((mi B) ^ C) c= mi (B ^ C) by Lm5; :: according to XBOOLE_0:def_10 ::_thesis: mi (B ^ C) c= mi ((mi B) ^ C)
A7: mi (B ^ C) c= (mi B) ^ C by Th47;
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_(B_^_C)_holds_
a_in_mi_((mi_B)_^_C)
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi (B ^ C) implies a in mi ((mi B) ^ C) )
assume A8: a in mi (B ^ C) ; ::_thesis: a in mi ((mi B) ^ C)
then for b being Element of DISJOINT_PAIRS A st b in (mi B) ^ C & b c= a holds
b = a by A1, Th36;
hence a in mi ((mi B) ^ C) by A7, A8, Th39; ::_thesis: verum
end;
hence mi (B ^ C) c= mi ((mi B) ^ C) by Lm5; ::_thesis: verum
end;
theorem Th51: :: NORMFORM:51
for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ (mi C)) = mi (B ^ C)
proof
let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ (mi C)) = mi (B ^ C)
let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi (B ^ (mi C)) = mi (B ^ C)
( B ^ (mi C) = (mi C) ^ B & B ^ C = C ^ B ) by Th48;
hence mi (B ^ (mi C)) = mi (B ^ C) by Th50; ::_thesis: verum
end;
theorem Th52: :: NORMFORM:52
for A being set
for K, L, M being Element of Normal_forms_on A holds K ^ (L ^ M) = (K ^ L) ^ M
proof
let A be set ; ::_thesis: for K, L, M being Element of Normal_forms_on A holds K ^ (L ^ M) = (K ^ L) ^ M
let K, L, M be Element of Normal_forms_on A; ::_thesis: K ^ (L ^ M) = (K ^ L) ^ M
A1: ( L ^ M = M ^ L & K ^ L = L ^ K ) by Th48;
A2: now__::_thesis:_for_K,_L,_M_being_Element_of_Normal_forms_on_A_holds_K_^_(L_^_M)_c=_(K_^_L)_^_M
let K, L, M be Element of Normal_forms_on A; ::_thesis: K ^ (L ^ M) c= (K ^ L) ^ M
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_K_^_(L_^_M)_holds_
a_in_(K_^_L)_^_M
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in K ^ (L ^ M) implies a in (K ^ L) ^ M )
assume a in K ^ (L ^ M) ; ::_thesis: a in (K ^ L) ^ M
then consider b, c being Element of DISJOINT_PAIRS A such that
A3: b in K and
A4: c in L ^ M and
A5: a = b \/ c by Th34;
consider b1, c1 being Element of DISJOINT_PAIRS A such that
A6: b1 in L and
A7: c1 in M and
A8: c = b1 \/ c1 by A4, Th34;
reconsider d = b \/ (b1 \/ c1) as Element of DISJOINT_PAIRS A by A5, A8;
A9: b \/ (b1 \/ c1) = (b \/ b1) \/ c1 by Th3;
then b \/ b1 c= d by Th10;
then reconsider c2 = b \/ b1 as Element of DISJOINT_PAIRS A by Th26;
c2 in K ^ L by A3, A6, Th35;
hence a in (K ^ L) ^ M by A5, A7, A8, A9, Th35; ::_thesis: verum
end;
hence K ^ (L ^ M) c= (K ^ L) ^ M by Lm5; ::_thesis: verum
end;
then A10: K ^ (L ^ M) c= (K ^ L) ^ M ;
( (K ^ L) ^ M = M ^ (K ^ L) & K ^ (L ^ M) = (L ^ M) ^ K ) by Th48;
then (K ^ L) ^ M c= K ^ (L ^ M) by A1, A2;
hence K ^ (L ^ M) = (K ^ L) ^ M by A10, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th53: :: NORMFORM:53
for A being set
for K, L, M being Element of Normal_forms_on A holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
proof
let A be set ; ::_thesis: for K, L, M being Element of Normal_forms_on A holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
let K, L, M be Element of Normal_forms_on A; ::_thesis: K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_K_^_(L_\/_M)_holds_
a_in_(K_^_L)_\/_(K_^_M)
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in K ^ (L \/ M) implies a in (K ^ L) \/ (K ^ M) )
assume a in K ^ (L \/ M) ; ::_thesis: a in (K ^ L) \/ (K ^ M)
then consider b, c being Element of DISJOINT_PAIRS A such that
A1: b in K and
A2: c in L \/ M and
A3: a = b \/ c by Th34;
( c in L or c in M ) by A2, XBOOLE_0:def_3;
then ( a in K ^ L or a in K ^ M ) by A1, A3, Th35;
hence a in (K ^ L) \/ (K ^ M) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence K ^ (L \/ M) c= (K ^ L) \/ (K ^ M) by Lm5; :: according to XBOOLE_0:def_10 ::_thesis: (K ^ L) \/ (K ^ M) c= K ^ (L \/ M)
( K ^ L c= K ^ (L \/ M) & K ^ M c= K ^ (L \/ M) ) by Th49, XBOOLE_1:7;
hence (K ^ L) \/ (K ^ M) c= K ^ (L \/ M) by XBOOLE_1:8; ::_thesis: verum
end;
Lm7: for A being set
for a being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds
ex c being Element of DISJOINT_PAIRS A st
( c in C & c c= a )
proof
let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A
for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds
ex c being Element of DISJOINT_PAIRS A st
( c in C & c c= a )
let a be Element of DISJOINT_PAIRS A; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds
ex c being Element of DISJOINT_PAIRS A st
( c in C & c c= a )
let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( a in B ^ C implies ex c being Element of DISJOINT_PAIRS A st
( c in C & c c= a ) )
assume a in B ^ C ; ::_thesis: ex c being Element of DISJOINT_PAIRS A st
( c in C & c c= a )
then consider b, c being Element of DISJOINT_PAIRS A such that
b in B and
A1: c in C and
A2: a = b \/ c by Th34;
take c ; ::_thesis: ( c in C & c c= a )
thus c in C by A1; ::_thesis: c c= a
thus c c= a by A2, Th10; ::_thesis: verum
end;
Lm8: for A being set
for K, L being Element of Normal_forms_on A holds mi ((K ^ L) \/ L) = mi L
proof
let A be set ; ::_thesis: for K, L being Element of Normal_forms_on A holds mi ((K ^ L) \/ L) = mi L
let K, L be Element of Normal_forms_on A; ::_thesis: mi ((K ^ L) \/ L) = mi L
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_((K_^_L)_\/_L)_holds_
a_in_mi_L
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi ((K ^ L) \/ L) implies a in mi L )
assume A1: a in mi ((K ^ L) \/ L) ; ::_thesis: a in mi L
A2: now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_L_&_b_c=_a_holds_
b_=_a
let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in L & b c= a implies b = a )
assume b in L ; ::_thesis: ( b c= a implies b = a )
then b in (K ^ L) \/ L by XBOOLE_0:def_3;
hence ( b c= a implies b = a ) by A1, Th36; ::_thesis: verum
end;
A3: now__::_thesis:_(_a_in_K_^_L_implies_a_in_L_)
assume a in K ^ L ; ::_thesis: a in L
then consider b being Element of DISJOINT_PAIRS A such that
A4: b in L and
A5: b c= a by Lm7;
b in (K ^ L) \/ L by A4, XBOOLE_0:def_3;
hence a in L by A1, A4, A5, Th36; ::_thesis: verum
end;
a in (K ^ L) \/ L by A1, Th36;
then ( a in K ^ L or a in L ) by XBOOLE_0:def_3;
hence a in mi L by A3, A2, Th39; ::_thesis: verum
end;
hence mi ((K ^ L) \/ L) c= mi L by Lm5; :: according to XBOOLE_0:def_10 ::_thesis: mi L c= mi ((K ^ L) \/ L)
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_L_holds_
a_in_mi_((K_^_L)_\/_L)
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi L implies a in mi ((K ^ L) \/ L) )
assume A6: a in mi L ; ::_thesis: a in mi ((K ^ L) \/ L)
then A7: a in L by Th36;
A8: now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_(K_^_L)_\/_L_&_b_c=_a_holds_
b_=_a
let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in (K ^ L) \/ L & b c= a implies b = a )
assume b in (K ^ L) \/ L ; ::_thesis: ( b c= a implies b = a )
then A9: ( b in K ^ L or b in L ) by XBOOLE_0:def_3;
assume A10: b c= a ; ::_thesis: b = a
now__::_thesis:_(_b_in_K_^_L_implies_b_in_L_)
assume b in K ^ L ; ::_thesis: b in L
then consider c being Element of DISJOINT_PAIRS A such that
A11: c in L and
A12: c c= b by Lm7;
c c= a by A10, A12, Th2;
then c = a by A6, A11, Th36;
hence b in L by A7, A10, A12, Th1; ::_thesis: verum
end;
hence b = a by A6, A9, A10, Th36; ::_thesis: verum
end;
a in (K ^ L) \/ L by A7, XBOOLE_0:def_3;
hence a in mi ((K ^ L) \/ L) by A8, Th39; ::_thesis: verum
end;
hence mi L c= mi ((K ^ L) \/ L) by Lm5; ::_thesis: verum
end;
theorem Th54: :: NORMFORM:54
for A being set
for B being Element of Fin (DISJOINT_PAIRS A) holds B c= B ^ B
proof
let A be set ; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) holds B c= B ^ B
let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: B c= B ^ B
now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_B_holds_
a_in_B_^_B
let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in B implies a in B ^ B )
a = a \/ a ;
hence ( a in B implies a in B ^ B ) by Th35; ::_thesis: verum
end;
hence B c= B ^ B by Lm5; ::_thesis: verum
end;
theorem Th55: :: NORMFORM:55
for A being set
for K being Element of Normal_forms_on A holds mi (K ^ K) = mi K
proof
let A be set ; ::_thesis: for K being Element of Normal_forms_on A holds mi (K ^ K) = mi K
let K be Element of Normal_forms_on A; ::_thesis: mi (K ^ K) = mi K
thus mi (K ^ K) = mi ((K ^ K) \/ K) by Th54, XBOOLE_1:12
.= mi K by Lm8 ; ::_thesis: verum
end;
definition
let A be set ;
func NormForm A -> strict LattStr means :Def12: :: NORMFORM:def 12
( the carrier of it = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of it . (B,C) = mi (B \/ C) & the L_meet of it . (B,C) = mi (B ^ C) ) ) );
existence
ex b1 being strict LattStr st
( the carrier of b1 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b1 . (B,C) = mi (B \/ C) & the L_meet of b1 . (B,C) = mi (B ^ C) ) ) )
proof
set L = Normal_forms_on A;
deffunc H1( Element of Normal_forms_on A, Element of Normal_forms_on A) -> Element of Normal_forms_on A = mi ($1 \/ $2);
consider j being BinOp of (Normal_forms_on A) such that
A1: for x, y being Element of Normal_forms_on A holds j . (x,y) = H1(x,y) from BINOP_1:sch_4();
deffunc H2( Element of Normal_forms_on A, Element of Normal_forms_on A) -> Element of Normal_forms_on A = mi ($1 ^ $2);
consider m being BinOp of (Normal_forms_on A) such that
A2: for x, y being Element of Normal_forms_on A holds m . (x,y) = H2(x,y) from BINOP_1:sch_4();
take LattStr(# (Normal_forms_on A),j,m #) ; ::_thesis: ( the carrier of LattStr(# (Normal_forms_on A),j,m #) = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of LattStr(# (Normal_forms_on A),j,m #) . (B,C) = mi (B \/ C) & the L_meet of LattStr(# (Normal_forms_on A),j,m #) . (B,C) = mi (B ^ C) ) ) )
thus ( the carrier of LattStr(# (Normal_forms_on A),j,m #) = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of LattStr(# (Normal_forms_on A),j,m #) . (B,C) = mi (B \/ C) & the L_meet of LattStr(# (Normal_forms_on A),j,m #) . (B,C) = mi (B ^ C) ) ) ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict LattStr st the carrier of b1 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b1 . (B,C) = mi (B \/ C) & the L_meet of b1 . (B,C) = mi (B ^ C) ) ) & the carrier of b2 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b2 . (B,C) = mi (B \/ C) & the L_meet of b2 . (B,C) = mi (B ^ C) ) ) holds
b1 = b2
proof
set L = Normal_forms_on A;
let A1, A2 be strict LattStr ; ::_thesis: ( the carrier of A1 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of A1 . (B,C) = mi (B \/ C) & the L_meet of A1 . (B,C) = mi (B ^ C) ) ) & the carrier of A2 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of A2 . (B,C) = mi (B \/ C) & the L_meet of A2 . (B,C) = mi (B ^ C) ) ) implies A1 = A2 )
assume that
A3: the carrier of A1 = Normal_forms_on A and
A4: for A, B being Element of Normal_forms_on A holds
( the L_join of A1 . (A,B) = mi (A \/ B) & the L_meet of A1 . (A,B) = mi (A ^ B) ) and
A5: the carrier of A2 = Normal_forms_on A and
A6: for A, B being Element of Normal_forms_on A holds
( the L_join of A2 . (A,B) = mi (A \/ B) & the L_meet of A2 . (A,B) = mi (A ^ B) ) ; ::_thesis: A1 = A2
reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of (Normal_forms_on A) by A3, A5;
now__::_thesis:_for_x,_y_being_Element_of_Normal_forms_on_A_holds_a1_._(x,y)_=_a2_._(x,y)
let x, y be Element of Normal_forms_on A; ::_thesis: a1 . (x,y) = a2 . (x,y)
thus a1 . (x,y) = mi (x \/ y) by A4
.= a2 . (x,y) by A6 ; ::_thesis: verum
end;
then A7: a1 = a2 by BINOP_1:2;
now__::_thesis:_for_x,_y_being_Element_of_Normal_forms_on_A_holds_a3_._(x,y)_=_a4_._(x,y)
let x, y be Element of Normal_forms_on A; ::_thesis: a3 . (x,y) = a4 . (x,y)
thus a3 . (x,y) = mi (x ^ y) by A4
.= a4 . (x,y) by A6 ; ::_thesis: verum
end;
hence A1 = A2 by A3, A5, A7, BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines NormForm NORMFORM:def_12_:_
for A being set
for b2 being strict LattStr holds
( b2 = NormForm A iff ( the carrier of b2 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds
( the L_join of b2 . (B,C) = mi (B \/ C) & the L_meet of b2 . (B,C) = mi (B ^ C) ) ) ) );
registration
let A be set ;
cluster NormForm A -> non empty strict ;
coherence
not NormForm A is empty
proof
the carrier of (NormForm A) = Normal_forms_on A by Def12;
hence not NormForm A is empty ; ::_thesis: verum
end;
end;
Lm9: for A being set
for a, b being Element of (NormForm A) holds a "\/" b = b "\/" a
proof
let A be set ; ::_thesis: for a, b being Element of (NormForm A) holds a "\/" b = b "\/" a
set G = NormForm A;
let a, b be Element of (NormForm A); ::_thesis: a "\/" b = b "\/" a
reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12;
a "\/" b = mi (b9 \/ a9) by Def12
.= b "\/" a by Def12 ;
hence a "\/" b = b "\/" a ; ::_thesis: verum
end;
Lm10: for A being set
for a, b, c being Element of (NormForm A) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let A be set ; ::_thesis: for a, b, c being Element of (NormForm A) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
set G = NormForm A;
let a, b, c be Element of (NormForm A); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider a9 = a, b9 = b, c9 = c as Element of Normal_forms_on A by Def12;
a "\/" (b "\/" c) = the L_join of (NormForm A) . (a,(mi (b9 \/ c9))) by Def12
.= mi ((mi (b9 \/ c9)) \/ a9) by Def12
.= mi (a9 \/ (b9 \/ c9)) by Th44
.= mi ((a9 \/ b9) \/ c9) by XBOOLE_1:4
.= mi ((mi (a9 \/ b9)) \/ c9) by Th44
.= the L_join of (NormForm A) . ((mi (a9 \/ b9)),c9) by Def12
.= (a "\/" b) "\/" c by Def12 ;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; ::_thesis: verum
end;
Lm11: for A being set
for K, L being Element of Normal_forms_on A holds the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),L) = L
proof
let A be set ; ::_thesis: for K, L being Element of Normal_forms_on A holds the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),L) = L
let K, L be Element of Normal_forms_on A; ::_thesis: the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),L) = L
thus the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),L) = the L_join of (NormForm A) . ((mi (K ^ L)),L) by Def12
.= mi ((mi (K ^ L)) \/ L) by Def12
.= mi ((K ^ L) \/ L) by Th44
.= mi L by Lm8
.= L by Th42 ; ::_thesis: verum
end;
Lm12: for A being set
for a, b being Element of (NormForm A) holds (a "/\" b) "\/" b = b
proof
let A be set ; ::_thesis: for a, b being Element of (NormForm A) holds (a "/\" b) "\/" b = b
let a, b be Element of (NormForm A); ::_thesis: (a "/\" b) "\/" b = b
reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12;
set G = NormForm A;
thus (a "/\" b) "\/" b = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (a9,b9)),b9)
.= b by Lm11 ; ::_thesis: verum
end;
Lm13: for A being set
for a, b being Element of (NormForm A) holds a "/\" b = b "/\" a
proof
let A be set ; ::_thesis: for a, b being Element of (NormForm A) holds a "/\" b = b "/\" a
set G = NormForm A;
let a, b be Element of (NormForm A); ::_thesis: a "/\" b = b "/\" a
reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12;
a "/\" b = mi (a9 ^ b9) by Def12
.= mi (b9 ^ a9) by Th48
.= b "/\" a by Def12 ;
hence a "/\" b = b "/\" a ; ::_thesis: verum
end;
Lm14: for A being set
for a, b, c being Element of (NormForm A) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let A be set ; ::_thesis: for a, b, c being Element of (NormForm A) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
set G = NormForm A;
let a, b, c be Element of (NormForm A); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider a9 = a, b9 = b, c9 = c as Element of Normal_forms_on A by Def12;
a "/\" (b "/\" c) = the L_meet of (NormForm A) . (a,(mi (b9 ^ c9))) by Def12
.= mi (a9 ^ (mi (b9 ^ c9))) by Def12
.= mi (a9 ^ (b9 ^ c9)) by Th51
.= mi ((a9 ^ b9) ^ c9) by Th52
.= mi ((mi (a9 ^ b9)) ^ c9) by Th50
.= the L_meet of (NormForm A) . ((mi (a9 ^ b9)),c9) by Def12
.= (a "/\" b) "/\" c by Def12 ;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; ::_thesis: verum
end;
Lm15: for A being set
for K, L, M being Element of Normal_forms_on A holds the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),( the L_meet of (NormForm A) . (K,M)))
proof
let A be set ; ::_thesis: for K, L, M being Element of Normal_forms_on A holds the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),( the L_meet of (NormForm A) . (K,M)))
let K, L, M be Element of Normal_forms_on A; ::_thesis: the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),( the L_meet of (NormForm A) . (K,M)))
A1: the L_meet of (NormForm A) . (K,M) = mi (K ^ M) by Def12;
( the L_join of (NormForm A) . (L,M) = mi (L \/ M) & the L_meet of (NormForm A) . (K,L) = mi (K ^ L) ) by Def12;
then reconsider La = the L_join of (NormForm A) . (L,M), Lb = the L_meet of (NormForm A) . (K,L), Lc = the L_meet of (NormForm A) . (K,M) as Element of Normal_forms_on A by A1;
the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = mi (K ^ La) by Def12
.= mi (K ^ (mi (L \/ M))) by Def12
.= mi (K ^ (L \/ M)) by Th51
.= mi ((K ^ L) \/ (K ^ M)) by Th53
.= mi ((mi (K ^ L)) \/ (K ^ M)) by Th44
.= mi ((mi (K ^ L)) \/ (mi (K ^ M))) by Th44
.= mi (Lb \/ (mi (K ^ M))) by Def12
.= mi (Lb \/ Lc) by Def12 ;
hence the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),( the L_meet of (NormForm A) . (K,M))) by Def12; ::_thesis: verum
end;
Lm16: for A being set
for a, b being Element of (NormForm A) holds a "/\" (a "\/" b) = a
proof
let A be set ; ::_thesis: for a, b being Element of (NormForm A) holds a "/\" (a "\/" b) = a
set G = NormForm A;
let a, b be Element of (NormForm A); ::_thesis: a "/\" (a "\/" b) = a
reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12;
thus a "/\" (a "\/" b) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (a9,a9)),( the L_meet of (NormForm A) . (a9,b9))) by Lm15
.= the L_join of (NormForm A) . ((mi (a9 ^ a9)),( the L_meet of (NormForm A) . (a9,b9))) by Def12
.= the L_join of (NormForm A) . ((mi a9),( the L_meet of (NormForm A) . (a9,b9))) by Th55
.= a "\/" (a "/\" b) by Th42
.= (a "/\" b) "\/" a by Lm9
.= (b "/\" a) "\/" a by Lm13
.= a by Lm12 ; ::_thesis: verum
end;
registration
let A be set ;
cluster NormForm A -> strict Lattice-like ;
coherence
NormForm A is Lattice-like
proof
set G = NormForm A;
thus for u, v being Element of (NormForm A) holds u "\/" v = v "\/" u by Lm9; :: according to LATTICES:def_4,LATTICES:def_10 ::_thesis: ( NormForm A is join-associative & NormForm A is meet-absorbing & NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing )
thus for u, v, w being Element of (NormForm A) holds u "\/" (v "\/" w) = (u "\/" v) "\/" w by Lm10; :: according to LATTICES:def_5 ::_thesis: ( NormForm A is meet-absorbing & NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing )
thus for u, v being Element of (NormForm A) holds (u "/\" v) "\/" v = v by Lm12; :: according to LATTICES:def_8 ::_thesis: ( NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing )
thus for u, v being Element of (NormForm A) holds u "/\" v = v "/\" u by Lm13; :: according to LATTICES:def_6 ::_thesis: ( NormForm A is meet-associative & NormForm A is join-absorbing )
thus for u, v, w being Element of (NormForm A) holds u "/\" (v "/\" w) = (u "/\" v) "/\" w by Lm14; :: according to LATTICES:def_7 ::_thesis: NormForm A is join-absorbing
let u, v be Element of (NormForm A); :: according to LATTICES:def_9 ::_thesis: u "/\" (u "\/" v) = u
thus u "/\" (u "\/" v) = u by Lm16; ::_thesis: verum
end;
end;
registration
let A be set ;
cluster NormForm A -> strict distributive lower-bounded ;
coherence
( NormForm A is distributive & NormForm A is lower-bounded )
proof
set G = NormForm A;
thus NormForm A is distributive ::_thesis: NormForm A is lower-bounded
proof
let u, v, w be Element of (NormForm A); :: according to LATTICES:def_11 ::_thesis: u "/\" (v "\/" w) = (u "/\" v) "\/" (u "/\" w)
reconsider K = u, L = v, M = w as Element of Normal_forms_on A by Def12;
thus u "/\" (v "\/" w) = the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M)))
.= (u "/\" v) "\/" (u "/\" w) by Lm15 ; ::_thesis: verum
end;
thus NormForm A is lower-bounded ::_thesis: verum
proof
reconsider E = {} as Element of Normal_forms_on A by Lm4;
reconsider e = E as Element of (NormForm A) by Def12;
take e ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (NormForm A) holds
( e "/\" b1 = e & b1 "/\" e = e )
let u be Element of (NormForm A); ::_thesis: ( e "/\" u = e & u "/\" e = e )
reconsider K = u as Element of Normal_forms_on A by Def12;
A1: e "\/" u = mi (E \/ K) by Def12
.= u by Th42 ;
then u "/\" e = e by LATTICES:def_9;
hence ( e "/\" u = e & u "/\" e = e ) by A1, LATTICES:def_9; ::_thesis: verum
end;
end;
end;
theorem :: NORMFORM:56
for A being set holds {} is Element of (NormForm A)
proof
let A be set ; ::_thesis: {} is Element of (NormForm A)
the carrier of (NormForm A) = Normal_forms_on A by Def12;
hence {} is Element of (NormForm A) by Lm4; ::_thesis: verum
end;
theorem :: NORMFORM:57
for A being set holds Bottom (NormForm A) = {}
proof
let A be set ; ::_thesis: Bottom (NormForm A) = {}
{} in Normal_forms_on A by Lm4;
then reconsider Z = {} as Element of (NormForm A) by Def12;
now__::_thesis:_for_u_being_Element_of_(NormForm_A)_holds_Z_"\/"_u_=_u
let u be Element of (NormForm A); ::_thesis: Z "\/" u = u
reconsider z = Z, u9 = u as Element of Normal_forms_on A by Def12;
thus Z "\/" u = mi (z \/ u9) by Def12
.= u by Th42 ; ::_thesis: verum
end;
hence Bottom (NormForm A) = {} by LATTICE2:14; ::_thesis: verum
end;