morph_01.miz
begin
definition
let E be non
empty
RLSStruct;
mode
binary-image of E is
Subset of E;
end
reserve E for
RealLinearSpace;
reserve A,B,C for
binary-image of E;
reserve a,b,v for
Element of E;
definition
let E be
RealLinearSpace;
let A,B be
binary-image of E;
::
MORPH_01:def1
func A
(-) B ->
binary-image of E equals { z where z be
Element of E : for b be
Element of E st b
in B holds (z
- b)
in A };
correctness
proof
now
let x be
object;
assume x
in { z where z be
Element of E : for b be
Element of E st b
in B holds (z
- b)
in A };
then ex z be
Element of E st x
= z & for b be
Element of E st b
in B holds (z
- b)
in A;
hence x
in the
carrier of E;
end;
hence thesis by
TARSKI:def 3;
end;
end
notation
let a be
Real, E be
RealLinearSpace, A be
Subset of E;
synonym a
* A for a
(.) A;
end
theorem ::
MORPH_01:1
Th1: for E be
RealLinearSpace, A,B be
Subset of E st B
=
{} holds (A
(+) B)
= B & (B
(+) A)
= B & (A
(-) B)
= the
carrier of E
proof
let E be
RealLinearSpace, A,B be
Subset of E;
assume
A1: B
=
{} ;
hence (A
(+) B)
= B & (B
(+) A)
= B by
RUSUB_5: 5;
now
let x be
object;
assume x
in the
carrier of E;
then
reconsider z = x as
Element of E;
for b be
Element of E st b
in B holds (z
- b)
in A by
A1;
hence x
in (A
(-) B);
end;
then the
carrier of E
c= (A
(-) B);
hence the
carrier of E
= (A
(-) B);
end;
theorem ::
MORPH_01:2
Th2: for E be
RealLinearSpace, A,B be
Subset of E st A
<>
{} & B
=
{} holds (B
(-) A)
= B
proof
let E be
RealLinearSpace, A,B be
Subset of E;
assume
A1: A
<>
{} & B
=
{} ;
then
consider a be
object such that
A2: a
in A by
XBOOLE_0:def 1;
reconsider a as
Element of E by
A2;
assume (B
(-) A)
<> B;
then
consider ba be
object such that
A3: ba
in (B
(-) A) by
A1,
XBOOLE_0:def 1;
consider z be
Element of E such that
A4: ba
= z & for a be
Element of E st a
in A holds (z
- a)
in B by
A3;
thus contradiction by
A1,
A2,
A4;
end;
theorem ::
MORPH_01:3
Th3: for E be
RealLinearSpace, A,B be
Subset of E st B
= the
carrier of E & A
<>
{} holds (A
(+) B)
= B & (B
(+) A)
= B
proof
let E be
RealLinearSpace, A,B be
Subset of E;
assume
A1: B
= the
carrier of E & A
<>
{} ;
then
consider a be
object such that
A2: a
in A by
XBOOLE_0:def 1;
reconsider a as
Element of E by
A2;
now
let x be
object;
assume x
in the
carrier of E;
then
reconsider z = x as
Element of E;
(a
+ (z
- a))
= z by
RLVECT_4: 1;
hence x
in (A
(+) B) by
A1,
A2;
end;
then
A3: the
carrier of E
c= (A
(+) B);
hence B
= (A
(+) B) by
A1;
thus (B
(+) A)
= (A
+ B)
.= B by
A3,
A1;
end;
theorem ::
MORPH_01:4
Th4: for E be
RealLinearSpace, A,B be
Subset of E st B
= the
carrier of E holds (B
(-) A)
= B
proof
let E be
RealLinearSpace, A,B be
Subset of E;
assume
A1: B
= the
carrier of E;
now
let x be
object;
assume x
in the
carrier of E;
then
reconsider z = x as
Element of E;
for a be
Element of E st a
in A holds (z
- a)
in B by
A1;
hence x
in (B
(-) A);
end;
then the
carrier of E
c= (B
(-) A);
hence B
= (B
(-) A) by
A1;
end;
theorem ::
MORPH_01:5
(A
(+) B)
= (
union { (b
+ A) where b be
Element of E : b
in B })
proof
now
let x be
object;
assume
A1: x
in (A
(+) B);
consider a0,b0 be
Element of E such that
A2: x
= (a0
+ b0) & a0
in A & b0
in B by
A1;
A3: x
in (b0
+ A) by
A2;
(b0
+ A)
in { (b
+ A) where b be
Element of E : b
in B } by
A2;
hence x
in (
union { (b
+ A) where b be
Element of E : b
in B }) by
A3,
TARSKI:def 4;
end;
hence (A
(+) B)
c= (
union { (b
+ A) where b be
Element of E : b
in B });
now
let x be
object;
assume x
in (
union { (b
+ A) where b be
Element of E : b
in B });
then
consider y be
set such that
A4: x
in y & y
in { (b
+ A) where b be
Element of E : b
in B } by
TARSKI:def 4;
consider b be
Element of E such that
A5: y
= (b
+ A) & b
in B by
A4;
consider a be
Element of E such that
A6: x
= (b
+ a) & a
in A by
A5,
A4;
thus x
in (A
(+) B) by
A5,
A6;
end;
hence thesis;
end;
definition
let E be non
empty
RLSStruct;
mode
binary-image-family of E is
Subset-Family of the
carrier of E;
end
reserve F,G for
binary-image-family of E;
reserve A,B,C for non
empty
binary-image of E;
theorem ::
MORPH_01:6
(A
(-) B)
= (
meet { (b
+ A) where b be
Element of E : b
in B })
proof
consider g be
object such that
A1: g
in B by
XBOOLE_0:def 1;
reconsider g as
Element of E by
A1;
A2: (g
+ A)
in { (b
+ A) where b be
Element of E : b
in B } by
A1;
now
let x be
object;
assume x
in (A
(-) B);
then
consider z be
Element of E such that
A3: x
= z & for b be
Element of E st b
in B holds (z
- b)
in A;
for Y be
set st Y
in { (b
+ A) where b be
Element of E : b
in B } holds z
in Y
proof
let Y be
set;
assume Y
in { (b
+ A) where b be
Element of E : b
in B };
then
consider b be
Element of E such that
A4: Y
= (b
+ A) & b
in B;
A5: (z
- b)
in A by
A3,
A4;
z
= (b
+ (z
- b)) by
RLVECT_4: 1;
hence z
in Y by
A5,
A4;
end;
hence x
in (
meet { (b
+ A) where b be
Element of E : b
in B }) by
A3,
A2,
SETFAM_1:def 1;
end;
hence (A
(-) B)
c= (
meet { (b
+ A) where b be
Element of E : b
in B });
now
let x be
object;
assume
A6: x
in (
meet { (b
+ A) where b be
Element of E : b
in B });
consider S be
set such that
A7: S
in { (b
+ A) where b be
Element of E : b
in B } by
A2;
consider d be
Element of E such that
A8: S
= (d
+ A) & d
in B by
A7;
x
in S by
A6,
A7,
SETFAM_1:def 1;
then
reconsider x0 = x as
Element of E by
A8;
for b be
Element of E st b
in B holds (x0
- b)
in A
proof
let b be
Element of E;
assume b
in B;
then (b
+ A)
in { (f
+ A) where f be
Element of E : f
in B };
then x
in (b
+ A) by
A6,
SETFAM_1:def 1;
then
consider a be
Element of E such that
A9: x0
= (b
+ a) & a
in A;
thus thesis by
A9,
RLVECT_4: 1;
end;
hence x
in (A
(-) B);
end;
hence (
meet { (b
+ A) where b be
Element of E : b
in B })
c= (A
(-) B);
end;
theorem ::
MORPH_01:7
Th7: (A
(+) B)
= { v where v be
Element of E : ((v
+ ((
- 1)
* B))
/\ A)
<>
{} }
proof
thus (A
(+) B)
c= { v where v be
Element of E : ((v
+ ((
- 1)
* B))
/\ A)
<>
{} }
proof
let x be
object;
assume
A1: x
in (A
(+) B);
consider a0,b0 be
Element of E such that
A2: x
= (a0
+ b0) & a0
in A & b0
in B by
A1;
reconsider v = x as
Element of E by
A1;
A3: (v
- b0)
= a0 by
A2,
RLVECT_4: 1;
((
- 1)
* b0)
in ((
- 1)
* B) by
A2;
then (v
+ ((
- 1)
* b0))
in (v
+ ((
- 1)
* B));
then (v
- b0)
in (v
+ ((
- 1)
* B)) by
RLVECT_1: 16;
then ((v
+ ((
- 1)
* B))
/\ A)
<>
{} by
A2,
A3,
XBOOLE_0:def 4;
hence x
in { w where w be
Element of E : ((w
+ ((
- 1)
* B))
/\ A)
<>
{} };
end;
let x be
object;
assume x
in { v where v be
Element of E : ((v
+ ((
- 1)
* B))
/\ A)
<>
{} };
then
consider v be
Element of E such that
A4: x
= v & ((v
+ ((
- 1)
* B))
/\ A)
<>
{} ;
consider y be
object such that
A5: y
in ((v
+ ((
- 1)
* B))
/\ A) by
A4,
XBOOLE_0:def 1;
A6: y
in (v
+ ((
- 1)
* B)) & y
in A by
A5,
XBOOLE_0:def 4;
then
consider nb be
Element of E such that
A7: y
= (v
+ nb) & nb
in ((
- 1)
* B);
consider b be
Element of E such that
A8: nb
= ((
- 1)
* b) & b
in B by
A7;
reconsider a = y as
Element of E by
A7;
(a
+ b)
= ((v
- b)
+ b) by
A7,
A8,
RLVECT_1: 16
.= v by
RLVECT_4: 1;
hence x
in (A
(+) B) by
A4,
A8,
A6;
end;
theorem ::
MORPH_01:8
Th8: (A
(-) B)
= { v where v be
Element of E : (v
+ ((
- 1)
* B))
c= A }
proof
thus (A
(-) B)
c= { v where v be
Element of E : (v
+ ((
- 1)
* B))
c= A }
proof
let x be
object;
assume x
in (A
(-) B);
then
consider z be
Element of E such that
A1: x
= z & for b be
Element of E st b
in B holds (z
- b)
in A;
(z
+ ((
- 1)
* B))
c= A
proof
let y be
object;
assume y
in (z
+ ((
- 1)
* B));
then
consider nb be
Element of E such that
A2: y
= (z
+ nb) & nb
in ((
- 1)
* B);
consider b be
Element of E such that
A3: nb
= ((
- 1)
* b) & b
in B by
A2;
(z
- b)
in A by
A3,
A1;
hence y
in A by
A2,
A3,
RLVECT_1: 16;
end;
hence x
in { v where v be
Element of E : (v
+ ((
- 1)
* B))
c= A } by
A1;
end;
let x be
object;
assume x
in { v where v be
Element of E : (v
+ ((
- 1)
* B))
c= A };
then
consider v be
Element of E such that
A4: x
= v & (v
+ ((
- 1)
* B))
c= A;
for b be
Element of E st b
in B holds (v
- b)
in A
proof
let b be
Element of E;
assume b
in B;
then ((
- 1)
* b)
in ((
- 1)
* B);
then (v
+ ((
- 1)
* b))
in (v
+ ((
- 1)
* B));
then (v
- b)
in (v
+ ((
- 1)
* B)) by
RLVECT_1: 16;
hence thesis by
A4;
end;
hence x
in (A
(-) B) by
A4;
end;
theorem ::
MORPH_01:9
Th9: ((the
carrier of E
\ A)
(+) B)
= (the
carrier of E
\ (A
(-) B)) & ((the
carrier of E
\ A)
(-) B)
= (the
carrier of E
\ (A
(+) B))
proof
per cases ;
suppose
A1: A
= the
carrier of E;
reconsider X =
{} as
Subset of E by
XBOOLE_1: 2;
thus ((the
carrier of E
\ A)
(+) B)
= (X
(+) B) by
A1,
XBOOLE_1: 37
.=
{} by
Th1
.= (the
carrier of E
\ the
carrier of E) by
XBOOLE_1: 37
.= (the
carrier of E
\ (A
(-) B)) by
A1,
Th4;
thus ((the
carrier of E
\ A)
(-) B)
= (X
(-) B) by
A1,
XBOOLE_1: 37
.=
{} by
Th2
.= (the
carrier of E
\ the
carrier of E) by
XBOOLE_1: 37
.= (the
carrier of E
\ (A
(+) B)) by
A1,
Th3;
end;
suppose
A2: A
<> the
carrier of E;
A3: (the
carrier of E
\ A) is non
empty by
XBOOLE_1: 37,
A2;
A4: for x be
object holds x
in { v where v be
Element of E : ((v
+ ((
- 1)
* B))
/\ (the
carrier of E
\ A))
<>
{} } iff x
in the
carrier of E & not x
in { v where v be
Element of E : (v
+ ((
- 1)
* B))
c= A }
proof
let x be
object;
hereby
assume x
in { v where v be
Element of E : ((v
+ ((
- 1)
* B))
/\ (the
carrier of E
\ A))
<>
{} };
then
consider v be
Element of E such that
A5: x
= v & ((v
+ ((
- 1)
* B))
/\ (the
carrier of E
\ A))
<>
{} ;
thus x
in the
carrier of E by
A5;
thus not x
in { w where w be
Element of E : (w
+ ((
- 1)
* B))
c= A }
proof
assume x
in { w where w be
Element of E : (w
+ ((
- 1)
* B))
c= A };
then
consider w be
Element of E such that
A6: w
= x & (w
+ ((
- 1)
* B))
c= A;
(v
+ ((
- 1)
* B))
misses (the
carrier of E
\ A) by
A5,
A6,
XBOOLE_1: 85;
hence contradiction by
A5;
end;
end;
assume
A7: x
in the
carrier of E & not x
in { v where v be
Element of E : (v
+ ((
- 1)
* B))
c= A };
then
reconsider w = x as
Element of E;
now
assume ((w
+ ((
- 1)
* B))
/\ (the
carrier of E
\ A))
=
{} ;
then
{}
= (((w
+ ((
- 1)
* B))
/\ the
carrier of E)
\ A) by
XBOOLE_1: 49
.= ((w
+ ((
- 1)
* B))
\ A) by
XBOOLE_1: 28;
then (w
+ ((
- 1)
* B))
c= A by
XBOOLE_1: 37;
hence contradiction by
A7;
end;
hence x
in { v where v be
Element of E : ((v
+ ((
- 1)
* B))
/\ (the
carrier of E
\ A))
<>
{} };
end;
A8: for x be
object holds x
in { v where v be
Element of E : (v
+ ((
- 1)
* B))
c= (the
carrier of E
\ A) } iff x
in the
carrier of E & not x
in { v where v be
Element of E : ((v
+ ((
- 1)
* B))
/\ A)
<>
{} }
proof
let x be
object;
hereby
assume x
in { v where v be
Element of E : (v
+ ((
- 1)
* B))
c= (the
carrier of E
\ A) };
then
consider v be
Element of E such that
A9: x
= v & (v
+ ((
- 1)
* B))
c= (the
carrier of E
\ A);
thus x
in the
carrier of E by
A9;
thus not x
in { w where w be
Element of E : ((w
+ ((
- 1)
* B))
/\ A)
<>
{} }
proof
assume x
in { w where w be
Element of E : ((w
+ ((
- 1)
* B))
/\ A)
<>
{} };
then
consider w be
Element of E such that
A10: w
= x & ((w
+ ((
- 1)
* B))
/\ A)
<>
{} ;
(w
+ ((
- 1)
* B))
misses (the
carrier of E
\ (the
carrier of E
\ A)) by
A9,
A10,
XBOOLE_1: 85;
then (w
+ ((
- 1)
* B))
misses (the
carrier of E
/\ A) by
XBOOLE_1: 48;
then (w
+ ((
- 1)
* B))
misses A by
XBOOLE_1: 28;
hence contradiction by
A10;
end;
end;
assume
A11: x
in the
carrier of E & not x
in { v where v be
Element of E : ((v
+ ((
- 1)
* B))
/\ A)
<>
{} };
then
reconsider w = x as
Element of E;
reconsider w = x as
Element of E by
A11;
((w
+ ((
- 1)
* B))
\ (the
carrier of E
\ A))
= (((w
+ ((
- 1)
* B))
\ the
carrier of E)
\/ ((w
+ ((
- 1)
* B))
/\ A)) by
XBOOLE_1: 52
.= (
{}
\/ ((w
+ ((
- 1)
* B))
/\ A)) by
XBOOLE_1: 37
.=
{} by
A11;
then (w
+ ((
- 1)
* B))
c= (the
carrier of E
\ A) by
XBOOLE_1: 37;
hence x
in { v where v be
Element of E : (v
+ ((
- 1)
* B))
c= (the
carrier of E
\ A) };
end;
thus ((the
carrier of E
\ A)
(+) B)
= { v where v be
Element of E : ((v
+ ((
- 1)
* B))
/\ (the
carrier of E
\ A))
<>
{} } by
Th7,
A3
.= (the
carrier of E
\ { v where v be
Element of E : (v
+ ((
- 1)
* B))
c= A }) by
A4,
XBOOLE_0:def 5
.= (the
carrier of E
\ (A
(-) B)) by
Th8;
thus ((the
carrier of E
\ A)
(-) B)
= { v where v be
Element of E : (v
+ ((
- 1)
* B))
c= (the
carrier of E
\ A) } by
Th8,
A3
.= (the
carrier of E
\ { v where v be
Element of E : ((v
+ ((
- 1)
* B))
/\ A)
<>
{} }) by
A8,
XBOOLE_0:def 5
.= (the
carrier of E
\ (A
(+) B)) by
Th7;
end;
end;
Lm1: for E be non
empty
Abelian
addLoopStr, A,B be
Subset of E holds (A
(+) B)
= (B
(+) A)
proof
let E be non
empty
Abelian
addLoopStr, A,B be
Subset of E;
thus (A
(+) B)
= (B
+ A)
.= (B
(+) A);
end;
definition
let E be non
empty
Abelian
addLoopStr, A,B be
Subset of E;
:: original:
(+)
redefine
func A
(+) B;
commutativity by
Lm1;
end
theorem ::
MORPH_01:10
Th10: for E be non
empty
add-associative
addLoopStr, A,B,C be
Subset of E holds ((A
+ B)
+ C)
= (A
+ (B
+ C))
proof
let E be non
empty
add-associative
addLoopStr, A,B,C be
Subset of E;
for x be
Element of E holds x
in ((A
+ B)
+ C) iff x
in (A
+ (B
+ C))
proof
let x be
Element of E;
hereby
assume x
in ((A
+ B)
+ C);
then
consider ab,c be
Element of E such that
A1: x
= (ab
+ c) & ab
in (A
+ B) & c
in C;
consider a,b be
Element of E such that
A2: ab
= (a
+ b) & a
in A & b
in B by
A1;
A3: x
= (a
+ (b
+ c)) by
A1,
A2,
RLVECT_1:def 3;
(b
+ c)
in (B
+ C) by
A1,
A2;
hence x
in (A
+ (B
+ C)) by
A2,
A3;
end;
assume x
in (A
+ (B
+ C));
then
consider a,bc be
Element of E such that
A4: x
= (a
+ bc) & a
in A & bc
in (B
+ C);
consider b,c be
Element of E such that
A5: bc
= (b
+ c) & b
in B & c
in C by
A4;
A6: x
= ((a
+ b)
+ c) by
A4,
A5,
RLVECT_1:def 3;
(a
+ b)
in (A
+ B) by
A4,
A5;
hence x
in ((A
+ B)
+ C) by
A5,
A6;
end;
hence thesis by
SUBSET_1: 3;
end;
theorem ::
MORPH_01:11
((A
(+) B)
(+) C)
= (A
(+) (B
(+) C)) by
Th10;
theorem ::
MORPH_01:12
Th12: ((
union F)
(+) B)
= (
union { (X
(+) B) where X be
binary-image of E : X
in F })
proof
for x be
object holds x
in ((
union F)
(+) B) iff x
in (
union { (X
(+) B) where X be
binary-image of E : X
in F })
proof
let x be
object;
hereby
assume x
in ((
union F)
(+) B);
then
consider f,b be
Element of E such that
A1: x
= (f
+ b) & f
in (
union F) & b
in B;
consider Y be
set such that
A2: f
in Y & Y
in F by
A1,
TARSKI:def 4;
reconsider X = Y as
binary-image of E by
A2;
A3: x
in (X
(+) B) by
A1,
A2;
(X
(+) B)
in { (W
(+) B) where W be
binary-image of E : W
in F } by
A2;
hence x
in (
union { (W
(+) B) where W be
binary-image of E : W
in F }) by
A3,
TARSKI:def 4;
end;
assume x
in (
union { (X
(+) B) where X be
binary-image of E : X
in F });
then
consider Y be
set such that
A4: x
in Y & Y
in { (X
(+) B) where X be
binary-image of E : X
in F } by
TARSKI:def 4;
consider W be
binary-image of E such that
A5: Y
= (W
(+) B) & W
in F by
A4;
consider f,b be
Element of E such that
A6: x
= (f
+ b) & f
in W & b
in B by
A4,
A5;
W
c= (
union F) by
A5,
ZFMISC_1: 74;
hence x
in ((
union F)
(+) B) by
A6;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
MORPH_01:13
(A
(+) (
union F))
= (
union { (A
(+) X) where X be
binary-image of E : X
in F })
proof
A1: for x be
object holds x
in { (X
(+) A) where X be
binary-image of E : X
in F } iff x
in { (A
(+) X) where X be
binary-image of E : X
in F }
proof
let x be
object;
hereby
assume x
in { (X
(+) A) where X be
binary-image of E : X
in F };
then
consider W be
binary-image of E such that
A2: x
= (W
(+) A) & W
in F;
x
= (A
(+) W) & W
in F by
A2;
hence x
in { (A
(+) X) where X be
binary-image of E : X
in F };
end;
assume x
in { (A
(+) X) where X be
binary-image of E : X
in F };
then
consider W be
binary-image of E such that
A3: x
= (A
(+) W) & W
in F;
x
= (W
(+) A) & W
in F by
A3;
hence x
in { (X
(+) A) where X be
binary-image of E : X
in F };
end;
thus (A
(+) (
union F))
= ((
union F)
(+) A)
.= (
union { (X
(+) A) where X be
binary-image of E : X
in F }) by
Th12
.= (
union { (A
(+) X) where X be
binary-image of E : X
in F }) by
A1,
TARSKI: 2;
end;
theorem ::
MORPH_01:14
Th14: ((
meet F)
(+) B)
c= (
meet { (X
(+) B) where X be
binary-image of E : X
in F })
proof
per cases ;
suppose
A1: F
=
{} ;
reconsider Z = (
meet F) as
Subset of E;
(
meet F)
=
{} by
A1,
SETFAM_1:def 1;
then (Z
(+) B)
=
{} by
Th1;
hence ((
meet F)
(+) B)
c= (
meet { (X
(+) B) where X be
binary-image of E : X
in F });
end;
suppose F
<>
{} ;
then
consider W0 be
object such that
A2: W0
in F by
XBOOLE_0:def 1;
reconsider W0 as
binary-image of E by
A2;
A3: (W0
(+) B)
in { (W
(+) B) where W be
binary-image of E : W
in F } by
A2;
let x be
object;
assume x
in ((
meet F)
(+) B);
then
consider f,b be
Element of E such that
A4: x
= (f
+ b) & f
in (
meet F) & b
in B;
now
let Y be
set;
assume Y
in { (X
(+) B) where X be
binary-image of E : X
in F };
then
consider X be
binary-image of E such that
A5: Y
= (X
(+) B) & X
in F;
(
meet F)
c= X by
A5,
SETFAM_1: 3;
hence x
in Y by
A4,
A5;
end;
hence x
in (
meet { (W
(+) B) where W be
binary-image of E : W
in F }) by
A3,
SETFAM_1:def 1;
end;
end;
theorem ::
MORPH_01:15
(A
(+) (
meet F))
c= (
meet { (A
(+) X) where X be
binary-image of E : X
in F })
proof
A1: for x be
object holds x
in { (X
(+) A) where X be
binary-image of E : X
in F } iff x
in { (A
(+) X) where X be
binary-image of E : X
in F }
proof
let x be
object;
hereby
assume x
in { (X
(+) A) where X be
binary-image of E : X
in F };
then
consider W be
binary-image of E such that
A2: x
= (W
(+) A) & W
in F;
x
= (A
(+) W) & W
in F by
A2;
hence x
in { (A
(+) X) where X be
binary-image of E : X
in F };
end;
assume x
in { (A
(+) X) where X be
binary-image of E : X
in F };
then
consider W be
binary-image of E such that
A3: x
= (A
(+) W) & W
in F;
x
= (W
(+) A) & W
in F by
A3;
hence x
in { (X
(+) A) where X be
binary-image of E : X
in F };
end;
(A
(+) (
meet F))
c= (
meet { (X
(+) A) where X be
binary-image of E : X
in F }) by
Th14;
hence (A
(+) (
meet F))
c= (
meet { (A
(+) X) where X be
binary-image of E : X
in F }) by
A1,
TARSKI: 2;
end;
theorem ::
MORPH_01:16
Th16: for E be non
empty
addLoopStr, A,B,C be
Subset of E holds B
c= C implies (A
+ B)
c= (A
+ C)
proof
let E be non
empty
addLoopStr, A,B,C be
Subset of E;
assume
A1: B
c= C;
let x be
object;
assume x
in (A
+ B);
then
consider a,b be
Element of E such that
A2: x
= (a
+ b) & a
in A & b
in B;
thus x
in (A
+ C) by
A1,
A2;
end;
theorem ::
MORPH_01:17
Th17: ((v
+ A)
(+) B)
= (A
(+) (v
+ B)) & ((v
+ A)
(+) B)
= (v
+ (A
(+) B))
proof
for x be
object holds x
in ((v
+ A)
(+) B) iff x
in (A
(+) (v
+ B))
proof
let x be
object;
hereby
assume x
in ((v
+ A)
(+) B);
then
consider f,b be
Element of E such that
A1: x
= (f
+ b) & f
in (v
+ A) & b
in B;
consider a be
Element of E such that
A2: f
= (v
+ a) & a
in A by
A1;
A3: x
= (a
+ (v
+ b)) by
A1,
A2,
RLVECT_1:def 3;
(v
+ b)
in (v
+ B) by
A1;
hence x
in (A
(+) (v
+ B)) by
A3,
A2;
end;
assume x
in (A
(+) (v
+ B));
then
consider a,f be
Element of E such that
A4: x
= (a
+ f) & a
in A & f
in (v
+ B);
consider b be
Element of E such that
A5: f
= (v
+ b) & b
in B by
A4;
A6: x
= ((v
+ a)
+ b) by
A4,
A5,
RLVECT_1:def 3;
(v
+ a)
in (v
+ A) by
A4;
hence x
in ((v
+ A)
(+) B) by
A6,
A5;
end;
hence ((v
+ A)
(+) B)
= (A
(+) (v
+ B)) by
TARSKI: 2;
for x be
object holds x
in ((v
+ A)
(+) B) iff x
in (v
+ (A
(+) B))
proof
let x be
object;
hereby
assume x
in ((v
+ A)
(+) B);
then
consider f,b be
Element of E such that
A7: x
= (f
+ b) & f
in (v
+ A) & b
in B;
consider a be
Element of E such that
A8: f
= (v
+ a) & a
in A by
A7;
A9: x
= (v
+ (a
+ b)) by
A7,
A8,
RLVECT_1:def 3;
(a
+ b)
in (A
+ B) by
A7,
A8;
hence x
in (v
+ (A
(+) B)) by
A9;
end;
assume x
in (v
+ (A
(+) B));
then
consider ab be
Element of E such that
A10: x
= (v
+ ab) & ab
in (A
(+) B);
consider a,b be
Element of E such that
A11: ab
= (a
+ b) & a
in A & b
in B by
A10;
A12: x
= ((v
+ a)
+ b) by
A10,
A11,
RLVECT_1:def 3;
(v
+ a)
in (v
+ A) by
A11;
hence x
in ((v
+ A)
(+) B) by
A12,
A11;
end;
hence ((v
+ A)
(+) B)
= (v
+ (A
(+) B)) by
TARSKI: 2;
end;
theorem ::
MORPH_01:18
Th18: ((
meet F)
(-) B)
= (
meet { (X
(-) B) where X be
binary-image of E : X
in F })
proof
per cases ;
suppose
A1: F
=
{} ;
reconsider Z = (
meet F) as
Subset of E;
A2: (
meet F)
=
{} by
A1,
SETFAM_1:def 1;
{ (X
(-) B) where X be
binary-image of E : X
in F }
=
{}
proof
assume { (X
(-) B) where X be
binary-image of E : X
in F }
<>
{} ;
then
consider x be
object such that
A3: x
in { (X
(-) B) where X be
binary-image of E : X
in F } by
XBOOLE_0:def 1;
ex X be
binary-image of E st x
= (X
(-) B) & X
in F by
A3;
hence contradiction by
A1;
end;
then
{}
= (
meet { (X
(-) B) where X be
binary-image of E : X
in F }) by
SETFAM_1:def 1;
hence ((
meet F)
(-) B)
= (
meet { (X
(-) B) where X be
binary-image of E : X
in F }) by
A2,
Th2;
end;
suppose
A4: F
<>
{} ;
then
consider W0 be
object such that
A5: W0
in F by
XBOOLE_0:def 1;
reconsider W0 as
binary-image of E by
A5;
A6: (W0
(-) B)
in { (W
(-) B) where W be
binary-image of E : W
in F } by
A5;
for x be
object holds x
in ((
meet F)
(-) B) iff x
in (
meet { (W
(-) B) where W be
binary-image of E : W
in F })
proof
let x be
object;
hereby
assume x
in ((
meet F)
(-) B);
then
consider z be
Element of E such that
A7: x
= z & for b be
Element of E st b
in B holds (z
- b)
in (
meet F);
now
let Y be
set;
assume Y
in { (X
(-) B) where X be
binary-image of E : X
in F };
then
consider X be
binary-image of E such that
A8: Y
= (X
(-) B) & X
in F;
now
let b be
Element of E;
assume b
in B;
then
A9: (z
- b)
in (
meet F) by
A7;
(
meet F)
c= X by
A8,
SETFAM_1: 3;
hence (z
- b)
in X by
A9;
end;
hence x
in Y by
A8,
A7;
end;
hence x
in (
meet { (W
(-) B) where W be
binary-image of E : W
in F }) by
A6,
SETFAM_1:def 1;
end;
assume
A10: x
in (
meet { (W
(-) B) where W be
binary-image of E : W
in F });
A11: for W be
binary-image of E st W
in F holds x
in (W
(-) B)
proof
let W be
binary-image of E;
assume W
in F;
then (W
(-) B)
in { (D
(-) B) where D be
binary-image of E : D
in F };
hence x
in (W
(-) B) by
A10,
SETFAM_1:def 1;
end;
x
in (W0
(-) B) by
A5,
A11;
then
reconsider z = x as
Element of E;
for b be
Element of E st b
in B holds (z
- b)
in (
meet F)
proof
assume not for b be
Element of E st b
in B holds (z
- b)
in (
meet F);
then
consider b be
Element of E such that
A12: b
in B & not (z
- b)
in (
meet F);
consider X be
set such that
A13: X
in F & not (z
- b)
in X by
A4,
A12,
SETFAM_1:def 1;
reconsider X as
binary-image of E by
A13;
z
in (X
(-) B) by
A13,
A11;
then
consider zz be
Element of E such that
A14: z
= zz & for b be
Element of E st b
in B holds (zz
- b)
in X;
thus contradiction by
A14,
A12,
A13;
end;
hence x
in ((
meet F)
(-) B);
end;
hence ((
meet F)
(-) B)
= (
meet { (X
(-) B) where X be
binary-image of E : X
in F }) by
TARSKI: 2;
end;
end;
theorem ::
MORPH_01:19
(
meet { (B
(-) X) where X be
binary-image of E : X
in F })
c= (B
(-) (
meet F))
proof
per cases ;
suppose
A1: F
=
{} ;
reconsider Z = (
meet F) as
Subset of E;
{ (B
(-) X) where X be
binary-image of E : X
in F }
=
{}
proof
assume { (B
(-) X) where X be
binary-image of E : X
in F }
<>
{} ;
then
consider x be
object such that
A2: x
in { (B
(-) X) where X be
binary-image of E : X
in F } by
XBOOLE_0:def 1;
ex X be
binary-image of E st x
= (B
(-) X) & X
in F by
A2;
hence contradiction by
A1;
end;
then
{}
= (
meet { (B
(-) X) where X be
binary-image of E : X
in F }) by
SETFAM_1:def 1;
hence (
meet { (B
(-) X) where X be
binary-image of E : X
in F })
c= (B
(-) (
meet F));
end;
suppose F
<>
{} ;
then
consider W0 be
object such that
A3: W0
in F by
XBOOLE_0:def 1;
reconsider W0 as
binary-image of E by
A3;
let x be
object;
assume
A4: x
in (
meet { (B
(-) W) where W be
binary-image of E : W
in F });
A5: for W be
binary-image of E st W
in F holds x
in (B
(-) W)
proof
let W be
binary-image of E;
assume W
in F;
then (B
(-) W)
in { (B
(-) D) where D be
binary-image of E : D
in F };
hence x
in (B
(-) W) by
A4,
SETFAM_1:def 1;
end;
A6: x
in (B
(-) W0) by
A3,
A5;
then
reconsider z = x as
Element of E;
for f be
Element of E st f
in (
meet F) holds (z
- f)
in B
proof
let f be
Element of E;
assume
A7: f
in (
meet F);
A8: (
meet F)
c= W0 by
A3,
SETFAM_1: 3;
consider zz be
Element of E such that
A9: z
= zz & for w be
Element of E st w
in W0 holds (zz
- w)
in B by
A6;
thus (z
- f)
in B by
A9,
A7,
A8;
end;
hence x
in (B
(-) (
meet F));
end;
end;
theorem ::
MORPH_01:20
(
union { (X
(-) B) where X be
binary-image of E : X
in F })
c= ((
union F)
(-) B)
proof
let x be
object;
assume x
in (
union { (X
(-) B) where X be
binary-image of E : X
in F });
then
consider Y be
set such that
A1: x
in Y & Y
in { (X
(-) B) where X be
binary-image of E : X
in F } by
TARSKI:def 4;
consider W be
binary-image of E such that
A2: Y
= (W
(-) B) & W
in F by
A1;
consider z be
Element of E such that
A3: x
= z & for b be
Element of E st b
in B holds (z
- b)
in W by
A1,
A2;
now
let b be
Element of E;
assume b
in B;
then
A4: (z
- b)
in W by
A3;
W
c= (
union F) by
A2,
ZFMISC_1: 74;
hence (z
- b)
in (
union F) by
A4;
end;
hence x
in ((
union F)
(-) B) by
A3;
end;
theorem ::
MORPH_01:21
F
<>
{} implies (B
(-) (
union F))
= (
meet { (B
(-) X) where X be
binary-image of E : X
in F })
proof
assume F
<>
{} ;
then
consider W0 be
object such that
A1: W0
in F by
XBOOLE_0:def 1;
reconsider W0 as
binary-image of E by
A1;
A2: (B
(-) W0)
in { (B
(-) X) where X be
binary-image of E : X
in F } by
A1;
for x be
object holds x
in (B
(-) (
union F)) iff x
in (
meet { (B
(-) X) where X be
binary-image of E : X
in F })
proof
let x be
object;
hereby
assume x
in (B
(-) (
union F));
then
consider z be
Element of E such that
A3: x
= z & for f be
Element of E st f
in (
union F) holds (z
- f)
in B;
now
let Y be
set;
assume Y
in { (B
(-) X) where X be
binary-image of E : X
in F };
then
consider X be
binary-image of E such that
A4: Y
= (B
(-) X) & X
in F;
now
let f be
Element of E;
assume f
in X;
then f
in (
union F) by
A4,
TARSKI:def 4;
hence (z
- f)
in B by
A3;
end;
hence x
in Y by
A3,
A4;
end;
hence x
in (
meet { (B
(-) W) where W be
binary-image of E : W
in F }) by
A2,
SETFAM_1:def 1;
end;
assume
A5: x
in (
meet { (B
(-) W) where W be
binary-image of E : W
in F });
A6: for W be
binary-image of E st W
in F holds x
in (B
(-) W)
proof
let W be
binary-image of E;
assume W
in F;
then (B
(-) W)
in { (B
(-) D) where D be
binary-image of E : D
in F };
hence x
in (B
(-) W) by
A5,
SETFAM_1:def 1;
end;
x
in (B
(-) W0) by
A1,
A6;
then
reconsider z = x as
Element of E;
for f be
Element of E st f
in (
union F) holds (z
- f)
in B
proof
let f be
Element of E;
assume f
in (
union F);
then
consider W be
set such that
A7: f
in W & W
in F by
TARSKI:def 4;
reconsider W as
binary-image of E by
A7;
z
in (B
(-) W) by
A6,
A7;
then
consider w be
Element of E such that
A8: z
= w & for f be
Element of E st f
in W holds (w
- f)
in B;
thus (z
- f)
in B by
A7,
A8;
end;
hence x
in (B
(-) (
union F));
end;
hence (B
(-) (
union F))
= (
meet { (B
(-) X) where X be
binary-image of E : X
in F }) by
TARSKI: 2;
end;
theorem ::
MORPH_01:22
Th22: A
c= B implies (A
(-) C)
c= (B
(-) C)
proof
assume
A1: A
c= B;
let x be
object;
assume x
in (A
(-) C);
then
consider w be
Element of E such that
A2: x
= w & for c be
Element of E st c
in C holds (w
- c)
in A;
for c be
Element of E st c
in C holds (w
- c)
in B by
A1,
A2;
hence x
in (B
(-) C) by
A2;
end;
theorem ::
MORPH_01:23
A
c= B implies (C
(-) B)
c= (C
(-) A)
proof
assume
A1: A
c= B;
let x be
object;
assume x
in (C
(-) B);
then
consider w be
Element of E such that
A2: x
= w & for b be
Element of E st b
in B holds (w
- b)
in C;
for a be
Element of E st a
in A holds (w
- a)
in C by
A1,
A2;
hence x
in (C
(-) A) by
A2;
end;
theorem ::
MORPH_01:24
Th24: ((v
+ A)
(-) B)
= (A
(-) (v
+ B)) & ((v
+ A)
(-) B)
= (v
+ (A
(-) B))
proof
for x be
object holds x
in ((v
+ A)
(-) B) iff x
in (A
(-) (v
+ B))
proof
let x be
object;
hereby
assume x
in ((v
+ A)
(-) B);
then
consider w be
Element of E such that
A1: x
= w & for b be
Element of E st b
in B holds (w
- b)
in (v
+ A);
now
let vb be
Element of E;
assume vb
in (v
+ B);
then
consider b be
Element of E such that
A2: vb
= (v
+ b) & b
in B;
(w
- b)
in (v
+ A) by
A2,
A1;
then
consider a be
Element of E such that
A3: (w
- b)
= (v
+ a) & a
in A;
(w
- vb)
= ((w
- b)
- v) by
A2,
RLVECT_1: 27
.= a by
A3,
RLVECT_4: 1;
hence (w
- vb)
in A by
A3;
end;
hence x
in (A
(-) (v
+ B)) by
A1;
end;
assume x
in (A
(-) (v
+ B));
then
consider w be
Element of E such that
A4: x
= w & for vb be
Element of E st vb
in (v
+ B) holds (w
- vb)
in A;
now
let b be
Element of E;
assume b
in B;
then (v
+ b)
in (v
+ B);
then (w
- (v
+ b))
in A by
A4;
then
A5: (v
+ (w
- (v
+ b)))
in (v
+ A);
(v
+ (w
- (v
+ b)))
= ((v
+ w)
- (v
+ b)) by
RLVECT_1: 28
.= (w
+ (v
- (v
+ b))) by
RLVECT_1: 28
.= (w
+ ((v
- v)
- b)) by
RLVECT_1: 27
.= (w
+ ((
0. E)
- b)) by
RLVECT_1: 15;
hence (w
- b)
in (v
+ A) by
A5;
end;
hence x
in ((v
+ A)
(-) B) by
A4;
end;
hence ((v
+ A)
(-) B)
= (A
(-) (v
+ B)) by
TARSKI: 2;
for x be
object holds x
in ((v
+ A)
(-) B) iff x
in (v
+ (A
(-) B))
proof
let x be
object;
hereby
assume x
in ((v
+ A)
(-) B);
then
consider w be
Element of E such that
A6: x
= w & for b be
Element of E st b
in B holds (w
- b)
in (v
+ A);
now
let b be
Element of E;
assume b
in B;
then
A7: (w
- b)
in (v
+ A) by
A6;
consider a be
Element of E such that
A8: (w
- b)
= (v
+ a) & a
in A by
A7;
((w
- v)
- b)
= (w
- (v
+ b)) by
RLVECT_1: 27
.= ((v
+ a)
- v) by
A8,
RLVECT_1: 27
.= a by
RLVECT_4: 1;
hence ((w
- v)
- b)
in A by
A8;
end;
then
A9: (w
- v)
in (A
(-) B);
(v
+ (w
- v))
= w by
RLVECT_4: 1;
hence x
in (v
+ (A
(-) B)) by
A6,
A9;
end;
assume x
in (v
+ (A
(-) B));
then
consider ab be
Element of E such that
A10: x
= (v
+ ab) & ab
in (A
(-) B);
reconsider w = x as
Element of E by
A10;
consider d be
Element of E such that
A11: ab
= d & for b be
Element of E st b
in B holds (d
- b)
in A by
A10;
now
let b be
Element of E;
assume b
in B;
then
A12: (ab
- b)
in A by
A11;
((v
+ ab)
- b)
= (v
+ (ab
- b)) by
RLVECT_1: 28;
hence ((v
+ ab)
- b)
in (v
+ A) by
A12;
end;
hence x
in ((v
+ A)
(-) B) by
A10;
end;
hence ((v
+ A)
(-) B)
= (v
+ (A
(-) B)) by
TARSKI: 2;
end;
theorem ::
MORPH_01:25
Th25: ((A
(-) B)
(-) C)
= (A
(-) (B
(+) C))
proof
for x be
object holds x
in ((A
(-) B)
(-) C) iff x
in (A
(-) (B
(+) C))
proof
let x be
object;
hereby
assume x
in ((A
(-) B)
(-) C);
then
consider w be
Element of E such that
A1: x
= w & for c be
Element of E st c
in C holds (w
- c)
in (A
(-) B);
now
let bc be
Element of E;
assume bc
in (B
(+) C);
then
consider b,c be
Element of E such that
A2: bc
= (b
+ c) & b
in B & c
in C;
(w
- c)
in (A
(-) B) by
A1,
A2;
then
consider g be
Element of E such that
A3: (w
- c)
= g & for b be
Element of E st b
in B holds (g
- b)
in A;
(w
- bc)
= (g
- b) by
A2,
A3,
RLVECT_1: 27;
hence (w
- bc)
in A by
A3,
A2;
end;
hence x
in (A
(-) (B
(+) C)) by
A1;
end;
assume x
in (A
(-) (B
(+) C));
then
consider w be
Element of E such that
A4: x
= w & for bc be
Element of E st bc
in (B
(+) C) holds (w
- bc)
in A;
now
let c be
Element of E;
assume
A5: c
in C;
now
let b be
Element of E;
assume
A6: b
in B;
(b
+ c)
in (B
(+) C) by
A5,
A6;
then (w
- (b
+ c))
in A by
A4;
hence ((w
- c)
- b)
in A by
RLVECT_1: 27;
end;
hence (w
- c)
in (A
(-) B);
end;
hence x
in ((A
(-) B)
(-) C) by
A4;
end;
hence ((A
(-) B)
(-) C)
= (A
(-) (B
(+) C)) by
TARSKI: 2;
end;
begin
definition
let E be
RealLinearSpace;
let B be
binary-image of E;
::
MORPH_01:def2
func
dilation (B) ->
Function of (
bool the
carrier of E), (
bool the
carrier of E) means
:
Def2: for A be
binary-image of E holds (it
. A)
= (A
(+) B);
existence
proof
defpred
P[
object,
object] means ex A be
binary-image of E st $1
= A & $2
= (A
(+) B);
A1:
now
let x be
object;
assume x
in (
bool the
carrier of E);
then
reconsider A = x as
binary-image of E;
set y = (A
(+) B);
(A
(+) B)
c= the
carrier of E;
hence ex y be
object st y
in (
bool the
carrier of E) &
P[x, y];
end;
consider f be
Function of (
bool the
carrier of E), (
bool the
carrier of E) such that
A2: for x be
object st x
in (
bool the
carrier of E) holds
P[x, (f
. x)] from
FUNCT_2:sch 1(
A1);
take f;
now
let A be
binary-image of E;
ex X be
binary-image of E st A
= X & (f
. A)
= (X
(+) B) by
A2;
hence (f
. A)
= (A
(+) B);
end;
hence thesis;
end;
uniqueness
proof
let f,g be
Function of (
bool the
carrier of E), (
bool the
carrier of E);
assume
A3: for A be
binary-image of E holds (f
. A)
= (A
(+) B);
assume
A4: for A be
binary-image of E holds (g
. A)
= (A
(+) B);
now
let x be
object;
assume x
in (
bool the
carrier of E);
then
reconsider A = x as
binary-image of E;
thus (f
. x)
= (A
(+) B) by
A3
.= (g
. x) by
A4;
end;
hence f
= g by
FUNCT_2: 12;
end;
end
definition
let E be
RealLinearSpace;
let B be
binary-image of E;
::
MORPH_01:def3
func
erosion (B) ->
Function of (
bool the
carrier of E), (
bool the
carrier of E) means
:
Def3: for A be
binary-image of E holds (it
. A)
= (A
(-) B);
existence
proof
defpred
P[
object,
object] means ex A be
binary-image of E st $1
= A & $2
= (A
(-) B);
A1:
now
let x be
object;
assume x
in (
bool the
carrier of E);
then
reconsider A = x as
binary-image of E;
set y = (A
(-) B);
(A
(-) B)
c= the
carrier of E;
hence ex y be
object st y
in (
bool the
carrier of E) &
P[x, y];
end;
consider f be
Function of (
bool the
carrier of E), (
bool the
carrier of E) such that
A2: for x be
object st x
in (
bool the
carrier of E) holds
P[x, (f
. x)] from
FUNCT_2:sch 1(
A1);
take f;
now
let A be
binary-image of E;
ex X be
binary-image of E st A
= X & (f
. A)
= (X
(-) B) by
A2;
hence (f
. A)
= (A
(-) B);
end;
hence thesis;
end;
uniqueness
proof
let f,g be
Function of (
bool the
carrier of E), (
bool the
carrier of E);
assume that
A3: for A be
binary-image of E holds (f
. A)
= (A
(-) B) and
A4: for A be
binary-image of E holds (g
. A)
= (A
(-) B);
now
let x be
object;
assume x
in (
bool the
carrier of E);
then
reconsider A = x as
binary-image of E;
thus (f
. x)
= (A
(-) B) by
A3
.= (g
. x) by
A4;
end;
hence f
= g by
FUNCT_2: 12;
end;
end
theorem ::
MORPH_01:26
((
dilation B)
. (
union F))
= (
union { ((
dilation B)
. X) where X be
binary-image of E : X
in F })
proof
A1: for x be
object holds x
in { (X
(+) B) where X be
binary-image of E : X
in F } iff x
in { ((
dilation B)
. X) where X be
binary-image of E : X
in F }
proof
let x be
object;
hereby
assume x
in { (X
(+) B) where X be
binary-image of E : X
in F };
then
consider X be
binary-image of E such that
A2: x
= (X
(+) B) & X
in F;
x
= ((
dilation B)
. X) & X
in F by
A2,
Def2;
hence x
in { ((
dilation B)
. W) where W be
binary-image of E : W
in F };
end;
assume x
in { ((
dilation B)
. X) where X be
binary-image of E : X
in F };
then
consider X be
binary-image of E such that
A3: x
= ((
dilation B)
. X) & X
in F;
x
= (X
(+) B) & X
in F by
A3,
Def2;
hence x
in { (W
(+) B) where W be
binary-image of E : W
in F };
end;
thus ((
dilation B)
. (
union F))
= ((
union F)
(+) B) by
Def2
.= (
union { (X
(+) B) where X be
binary-image of E : X
in F }) by
Th12
.= (
union { ((
dilation B)
. X) where X be
binary-image of E : X
in F }) by
A1,
TARSKI: 2;
end;
theorem ::
MORPH_01:27
A
c= B implies ((
dilation C)
. A)
c= ((
dilation C)
. B)
proof
assume
A1: A
c= B;
A2: ((
dilation C)
. A)
= (C
+ A) by
Def2;
((
dilation C)
. B)
= (C
+ B) by
Def2;
hence thesis by
A2,
A1,
Th16;
end;
theorem ::
MORPH_01:28
((
dilation C)
. (v
+ A))
= (v
+ ((
dilation C)
. A))
proof
A1: ((
dilation C)
. (v
+ A))
= ((v
+ A)
(+) C) by
Def2;
(v
+ ((
dilation C)
. A))
= (v
+ (A
(+) C)) by
Def2;
hence thesis by
Th17,
A1;
end;
theorem ::
MORPH_01:29
((
erosion B)
. (
meet F))
= (
meet { ((
erosion B)
. X) where X be
binary-image of E : X
in F })
proof
A1: for x be
object holds x
in { (X
(-) B) where X be
binary-image of E : X
in F } iff x
in { ((
erosion B)
. X) where X be
binary-image of E : X
in F }
proof
let x be
object;
hereby
assume x
in { (X
(-) B) where X be
binary-image of E : X
in F };
then
consider X be
binary-image of E such that
A2: x
= (X
(-) B) & X
in F;
x
= ((
erosion B)
. X) & X
in F by
A2,
Def3;
hence x
in { ((
erosion B)
. W) where W be
binary-image of E : W
in F };
end;
assume x
in { ((
erosion B)
. X) where X be
binary-image of E : X
in F };
then
consider X be
binary-image of E such that
A3: x
= ((
erosion B)
. X) & X
in F;
x
= (X
(-) B) & X
in F by
A3,
Def3;
hence x
in { (W
(-) B) where W be
binary-image of E : W
in F };
end;
thus ((
erosion B)
. (
meet F))
= ((
meet F)
(-) B) by
Def3
.= (
meet { (X
(-) B) where X be
binary-image of E : X
in F }) by
Th18
.= (
meet { ((
erosion B)
. X) where X be
binary-image of E : X
in F }) by
A1,
TARSKI: 2;
end;
theorem ::
MORPH_01:30
A
c= B implies ((
erosion C)
. A)
c= ((
erosion C)
. B)
proof
assume
A1: A
c= B;
A2: ((
erosion C)
. A)
= (A
(-) C) by
Def3;
((
erosion C)
. B)
= (B
(-) C) by
Def3;
hence thesis by
A2,
A1,
Th22;
end;
theorem ::
MORPH_01:31
((
erosion C)
. (v
+ A))
= (v
+ ((
erosion C)
. A))
proof
A1: ((
erosion C)
. (v
+ A))
= ((v
+ A)
(-) C) by
Def3;
(v
+ ((
erosion C)
. A))
= (v
+ (A
(-) C)) by
Def3;
hence thesis by
Th24,
A1;
end;
theorem ::
MORPH_01:32
((
dilation C)
. (the
carrier of E
\ A))
= (the
carrier of E
\ ((
erosion C)
. A)) & ((
erosion C)
. (the
carrier of E
\ A))
= (the
carrier of E
\ ((
dilation C)
. A))
proof
thus ((
dilation C)
. (the
carrier of E
\ A))
= ((the
carrier of E
\ A)
(+) C) by
Def2
.= (the
carrier of E
\ (A
(-) C)) by
Th9
.= (the
carrier of E
\ ((
erosion C)
. A)) by
Def3;
thus ((
erosion C)
. (the
carrier of E
\ A))
= ((the
carrier of E
\ A)
(-) C) by
Def3
.= (the
carrier of E
\ (A
(+) C)) by
Th9
.= (the
carrier of E
\ ((
dilation C)
. A)) by
Def2;
end;
theorem ::
MORPH_01:33
((
dilation C)
. ((
dilation B)
. A))
= ((
dilation ((
dilation C)
. B))
. A) & ((
erosion C)
. ((
erosion B)
. A))
= ((
erosion ((
dilation C)
. B))
. A)
proof
thus ((
dilation C)
. ((
dilation B)
. A))
= ((
dilation C)
. (A
(+) B)) by
Def2
.= ((A
(+) B)
(+) C) by
Def2
.= (A
(+) (B
(+) C)) by
Th10
.= (A
(+) ((
dilation C)
. B)) by
Def2
.= ((
dilation ((
dilation C)
. B))
. A) by
Def2;
thus ((
erosion C)
. ((
erosion B)
. A))
= ((
erosion C)
. (A
(-) B)) by
Def3
.= ((A
(-) B)
(-) C) by
Def3
.= (A
(-) (B
(+) C)) by
Th25
.= (A
(-) ((
dilation C)
. B)) by
Def2
.= ((
erosion ((
dilation C)
. B))
. A) by
Def3;
end;