:: MATHMORP semantic presentation
begin
definition
let T be non empty addMagma ;
let p be Element of T;
let X be Subset of T;
funcX + p -> Subset of T equals :: MATHMORP:def 1
{ (q + p) where q is Element of T : q in X } ;
coherence
{ (q + p) where q is Element of T : q in X } is Subset of T
proof
now__::_thesis:_for_x_being_set_st_x_in__{__(q_+_p)_where_q_is_Point_of_T_:_q_in_X__}__holds_
x_in_the_carrier_of_T
let x be set ; ::_thesis: ( x in { (q + p) where q is Point of T : q in X } implies x in the carrier of T )
assume x in { (q + p) where q is Point of T : q in X } ; ::_thesis: x in the carrier of T
then ex q being Point of T st
( x = q + p & q in X ) ;
hence x in the carrier of T ; ::_thesis: verum
end;
hence { (q + p) where q is Element of T : q in X } is Subset of T by TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines + MATHMORP:def_1_:_
for T being non empty addMagma
for p being Element of T
for X being Subset of T holds X + p = { (q + p) where q is Element of T : q in X } ;
definition
let T be non empty addLoopStr ;
let X be Subset of T;
funcX ! -> Subset of T equals :: MATHMORP:def 2
{ (- q) where q is Point of T : q in X } ;
coherence
{ (- q) where q is Point of T : q in X } is Subset of T
proof
now__::_thesis:_for_x_being_set_st_x_in__{__(-_q)_where_q_is_Point_of_T_:_q_in_X__}__holds_
x_in_the_carrier_of_T
let x be set ; ::_thesis: ( x in { (- q) where q is Point of T : q in X } implies x in the carrier of T )
assume x in { (- q) where q is Point of T : q in X } ; ::_thesis: x in the carrier of T
then ex q being Point of T st
( x = - q & q in X ) ;
hence x in the carrier of T ; ::_thesis: verum
end;
hence { (- q) where q is Point of T : q in X } is Subset of T by TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines ! MATHMORP:def_2_:_
for T being non empty addLoopStr
for X being Subset of T holds X ! = { (- q) where q is Point of T : q in X } ;
definition
let T be non empty addMagma ;
let X, B be Subset of T;
funcX (-) B -> Subset of T equals :: MATHMORP:def 3
{ y where y is Point of T : B + y c= X } ;
coherence
{ y where y is Point of T : B + y c= X } is Subset of T
proof
now__::_thesis:_for_x_being_set_st_x_in__{__y_where_y_is_Point_of_T_:_B_+_y_c=_X__}__holds_
x_in_the_carrier_of_T
let x be set ; ::_thesis: ( x in { y where y is Point of T : B + y c= X } implies x in the carrier of T )
assume x in { y where y is Point of T : B + y c= X } ; ::_thesis: x in the carrier of T
then ex q being Point of T st
( x = q & B + q c= X ) ;
hence x in the carrier of T ; ::_thesis: verum
end;
hence { y where y is Point of T : B + y c= X } is Subset of T by TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines (-) MATHMORP:def_3_:_
for T being non empty addMagma
for X, B being Subset of T holds X (-) B = { y where y is Point of T : B + y c= X } ;
notation
let T be non empty addLoopStr ;
let A, B be Subset of T;
synonym A (+) B for A + B;
end;
theorem Th1: :: MATHMORP:1
for T being non empty right_complementable add-associative right_zeroed RLSStruct
for B being Subset of T holds (B !) ! = B
proof
let T be non empty right_complementable add-associative right_zeroed RLSStruct ; ::_thesis: for B being Subset of T holds (B !) ! = B
let B be Subset of T; ::_thesis: (B !) ! = B
thus (B !) ! c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= (B !) !
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B !) ! or x in B )
assume x in (B !) ! ; ::_thesis: x in B
then consider q being Element of T such that
A1: x = - q and
A2: q in B ! ;
ex q1 being Element of T st
( q = - q1 & q1 in B ) by A2;
hence x in B by A1, RLVECT_1:17; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in (B !) ! )
assume A3: x in B ; ::_thesis: x in (B !) !
then reconsider xx = x as Point of T ;
- xx in { (- q) where q is Point of T : q in B } by A3;
then - (- xx) in { (- q) where q is Point of T : q in B ! } ;
hence x in (B !) ! by RLVECT_1:17; ::_thesis: verum
end;
theorem Th2: :: MATHMORP:2
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x being Point of T holds {(0. T)} + x = {x}
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for x being Point of T holds {(0. T)} + x = {x}
let x be Point of T; ::_thesis: {(0. T)} + x = {x}
thus {(0. T)} + x c= {x} :: according to XBOOLE_0:def_10 ::_thesis: {x} c= {(0. T)} + x
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {(0. T)} + x or a in {x} )
assume a in {(0. T)} + x ; ::_thesis: a in {x}
then consider q being Point of T such that
A1: a = q + x and
A2: q in {(0. T)} ;
{q} c= {(0. T)} by A2, ZFMISC_1:31;
then q = 0. T by ZFMISC_1:18;
then {a} c= {x} by A1, RLVECT_1:4;
hence a in {x} by ZFMISC_1:31; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x} or a in {(0. T)} + x )
assume a in {x} ; ::_thesis: a in {(0. T)} + x
then {a} c= {x} by ZFMISC_1:31;
then a = x by ZFMISC_1:18;
then A3: a = (0. T) + x by RLVECT_1:4;
0. T in {(0. T)} by ZFMISC_1:31;
hence a in {(0. T)} + x by A3; ::_thesis: verum
end;
theorem Th3: :: MATHMORP:3
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B1, B2 being Subset of T
for p being Point of T st B1 c= B2 holds
B1 + p c= B2 + p
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B1, B2 being Subset of T
for p being Point of T st B1 c= B2 holds
B1 + p c= B2 + p
let B1, B2 be Subset of T; ::_thesis: for p being Point of T st B1 c= B2 holds
B1 + p c= B2 + p
let p be Point of T; ::_thesis: ( B1 c= B2 implies B1 + p c= B2 + p )
assume A1: B1 c= B2 ; ::_thesis: B1 + p c= B2 + p
let p1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not p1 in B1 + p or p1 in B2 + p )
assume p1 in B1 + p ; ::_thesis: p1 in B2 + p
then ex p2 being Point of T st
( p1 = p2 + p & p2 in B1 ) ;
hence p1 in B2 + p by A1; ::_thesis: verum
end;
theorem Th4: :: MATHMORP:4
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x being Point of T
for X being Subset of T st X = {} holds
X + x = {}
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for x being Point of T
for X being Subset of T st X = {} holds
X + x = {}
let x be Point of T; ::_thesis: for X being Subset of T st X = {} holds
X + x = {}
let X be Subset of T; ::_thesis: ( X = {} implies X + x = {} )
assume A1: X = {} ; ::_thesis: X + x = {}
now__::_thesis:_for_y_being_set_holds_not_y_in_X_+_x
given y being set such that A2: y in X + x ; ::_thesis: contradiction
ex y1 being Point of T st
( y = y1 + x & y1 in X ) by A2;
hence contradiction by A1; ::_thesis: verum
end;
hence X + x = {} by XBOOLE_0:def_1; ::_thesis: verum
end;
theorem :: MATHMORP:5
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T holds X (-) {(0. T)} = X
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T holds X (-) {(0. T)} = X
let X be Subset of T; ::_thesis: X (-) {(0. T)} = X
thus X (-) {(0. T)} c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X (-) {(0. T)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (-) {(0. T)} or x in X )
assume x in X (-) {(0. T)} ; ::_thesis: x in X
then ex y being Point of T st
( x = y & {(0. T)} + y c= X ) ;
then {x} c= X by Th2;
hence x in X by ZFMISC_1:31; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X (-) {(0. T)} )
assume A1: x in X ; ::_thesis: x in X (-) {(0. T)}
then reconsider xx = x as Point of T ;
{x} c= X by A1, ZFMISC_1:31;
then {(0. T)} + xx c= X by Th2;
hence x in X (-) {(0. T)} ; ::_thesis: verum
end;
Lm1: for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x, y being Point of T holds {x} + y = {y} + x
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for x, y being Point of T holds {x} + y = {y} + x
let x, y be Point of T; ::_thesis: {x} + y = {y} + x
thus {x} + y c= {y} + x :: according to XBOOLE_0:def_10 ::_thesis: {y} + x c= {x} + y
proof
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in {x} + y or x1 in {y} + x )
assume x1 in {x} + y ; ::_thesis: x1 in {y} + x
then consider p1 being Point of T such that
A1: x1 = p1 + y and
A2: p1 in {x} ;
{p1} c= {x} by A2, ZFMISC_1:31;
then A3: x1 = x + y by A1, ZFMISC_1:18;
y in {y} by TARSKI:def_1;
hence x1 in {y} + x by A3; ::_thesis: verum
end;
let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in {y} + x or x1 in {x} + y )
assume x1 in {y} + x ; ::_thesis: x1 in {x} + y
then consider p1 being Point of T such that
A4: x1 = p1 + x and
A5: p1 in {y} ;
{p1} c= {y} by A5, ZFMISC_1:31;
then A6: x1 = x + y by A4, ZFMISC_1:18;
x in {x} by TARSKI:def_1;
hence x1 in {x} + y by A6; ::_thesis: verum
end;
theorem :: MATHMORP:6
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T holds X (+) {(0. T)} = X
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T holds X (+) {(0. T)} = X
let X be Subset of T; ::_thesis: X (+) {(0. T)} = X
thus X (+) {(0. T)} c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X (+) {(0. T)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (+) {(0. T)} or x in X )
assume x in X (+) {(0. T)} ; ::_thesis: x in X
then consider y, z being Point of T such that
A1: ( x = y + z & y in X ) and
A2: z in {(0. T)} ;
{z} c= {(0. T)} by A2, ZFMISC_1:31;
then z = 0. T by ZFMISC_1:18;
hence x in X by A1, RLVECT_1:4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X (+) {(0. T)} )
assume A3: x in X ; ::_thesis: x in X (+) {(0. T)}
then reconsider x = x as Point of T ;
0. T in {(0. T)} by TARSKI:def_1;
then x + (0. T) in { (y + z) where y, z is Point of T : ( y in X & z in {(0. T)} ) } by A3;
hence x in X (+) {(0. T)} by RLVECT_1:4; ::_thesis: verum
end;
theorem :: MATHMORP:7
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T
for x being Point of T holds X (+) {x} = X + x
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T
for x being Point of T holds X (+) {x} = X + x
let X be Subset of T; ::_thesis: for x being Point of T holds X (+) {x} = X + x
let x be Point of T; ::_thesis: X (+) {x} = X + x
thus X (+) {x} c= X + x :: according to XBOOLE_0:def_10 ::_thesis: X + x c= X (+) {x}
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (+) {x} or p in X + x )
assume p in X (+) {x} ; ::_thesis: p in X + x
then consider y, z being Point of T such that
A1: p = y + z and
A2: y in X and
A3: z in {x} ;
{z} c= {x} by A3, ZFMISC_1:31;
then p = y + x by A1, ZFMISC_1:18;
hence p in X + x by A2; ::_thesis: verum
end;
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X + x or p in X (+) {x} )
assume p in X + x ; ::_thesis: p in X (+) {x}
then A4: ex q being Point of T st
( p = q + x & q in X ) ;
x in {x} by TARSKI:def_1;
hence p in X (+) {x} by A4; ::_thesis: verum
end;
theorem Th8: :: MATHMORP:8
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T st Y = {} holds
X (-) Y = the carrier of T
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T st Y = {} holds
X (-) Y = the carrier of T
let X, Y be Subset of T; ::_thesis: ( Y = {} implies X (-) Y = the carrier of T )
assume A1: Y = {} ; ::_thesis: X (-) Y = the carrier of T
{ y where y is Point of T : Y + y c= X } = the carrier of T
proof
thus { y where y is Point of T : Y + y c= X } c= the carrier of T :: according to XBOOLE_0:def_10 ::_thesis: the carrier of T c= { y where y is Point of T : Y + y c= X }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Point of T : Y + y c= X } or x in the carrier of T )
assume x in { y where y is Point of T : Y + y c= X } ; ::_thesis: x in the carrier of T
then ex y being Point of T st
( x = y & Y + y c= X ) ;
hence x in the carrier of T ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of T or x in { y where y is Point of T : Y + y c= X } )
assume x in the carrier of T ; ::_thesis: x in { y where y is Point of T : Y + y c= X }
then reconsider a = x as Point of T ;
Y + a = {} by A1, Th4;
then Y + a c= X by XBOOLE_1:2;
hence x in { y where y is Point of T : Y + y c= X } ; ::_thesis: verum
end;
hence X (-) Y = the carrier of T ; ::_thesis: verum
end;
theorem Th9: :: MATHMORP:9
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, B being Subset of T st X c= Y holds
( X (-) B c= Y (-) B & X (+) B c= Y (+) B )
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, B being Subset of T st X c= Y holds
( X (-) B c= Y (-) B & X (+) B c= Y (+) B )
let X, Y, B be Subset of T; ::_thesis: ( X c= Y implies ( X (-) B c= Y (-) B & X (+) B c= Y (+) B ) )
assume A1: X c= Y ; ::_thesis: ( X (-) B c= Y (-) B & X (+) B c= Y (+) B )
thus X (-) B c= Y (-) B ::_thesis: X (+) B c= Y (+) B
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (-) B or p in Y (-) B )
assume p in X (-) B ; ::_thesis: p in Y (-) B
then consider p1 being Point of T such that
A2: p = p1 and
A3: B + p1 c= X ;
B + p1 c= Y by A1, A3, XBOOLE_1:1;
hence p in Y (-) B by A2; ::_thesis: verum
end;
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (+) B or p in Y (+) B )
assume p in X (+) B ; ::_thesis: p in Y (+) B
then ex p1, p2 being Point of T st
( p = p1 + p2 & p1 in X & p2 in B ) ;
hence p in Y (+) B by A1; ::_thesis: verum
end;
theorem Th10: :: MATHMORP:10
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B1, B2, X being Subset of T st B1 c= B2 holds
( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 )
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B1, B2, X being Subset of T st B1 c= B2 holds
( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 )
let B1, B2, X be Subset of T; ::_thesis: ( B1 c= B2 implies ( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 ) )
assume A1: B1 c= B2 ; ::_thesis: ( X (-) B2 c= X (-) B1 & X (+) B1 c= X (+) B2 )
thus X (-) B2 c= X (-) B1 ::_thesis: X (+) B1 c= X (+) B2
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (-) B2 or p in X (-) B1 )
assume p in X (-) B2 ; ::_thesis: p in X (-) B1
then consider p1 being Point of T such that
A2: p = p1 and
A3: B2 + p1 c= X ;
B1 + p1 c= B2 + p1 by A1, Th3;
then B1 + p1 c= X by A3, XBOOLE_1:1;
hence p in X (-) B1 by A2; ::_thesis: verum
end;
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (+) B1 or p in X (+) B2 )
assume p in X (+) B1 ; ::_thesis: p in X (+) B2
then ex x, b being Point of T st
( p = x + b & x in X & b in B1 ) ;
hence p in X (+) B2 by A1; ::_thesis: verum
end;
theorem :: MATHMORP:11
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, X being Subset of T st 0. T in B holds
( X (-) B c= X & X c= X (+) B )
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, X being Subset of T st 0. T in B holds
( X (-) B c= X & X c= X (+) B )
let B, X be Subset of T; ::_thesis: ( 0. T in B implies ( X (-) B c= X & X c= X (+) B ) )
assume A1: 0. T in B ; ::_thesis: ( X (-) B c= X & X c= X (+) B )
thus X (-) B c= X ::_thesis: X c= X (+) B
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (-) B or p in X )
assume p in X (-) B ; ::_thesis: p in X
then consider p1 being Point of T such that
A2: p = p1 and
A3: B + p1 c= X ;
(0. T) + p1 in { (q + p1) where q is Point of T : q in B } by A1;
then (0. T) + p1 in X by A3;
hence p in X by A2, RLVECT_1:4; ::_thesis: verum
end;
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X or p in X (+) B )
assume A4: p in X ; ::_thesis: p in X (+) B
then reconsider p = p as Point of T ;
p + (0. T) in { (x + b) where x, b is Point of T : ( x in X & b in B ) } by A1, A4;
hence p in X (+) B by RLVECT_1:4; ::_thesis: verum
end;
theorem Th12: :: MATHMORP:12
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T holds X (+) Y = Y (+) X
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T holds X (+) Y = Y (+) X
let X, Y be Subset of T; ::_thesis: X (+) Y = Y (+) X
thus X (+) Y c= Y (+) X :: according to XBOOLE_0:def_10 ::_thesis: Y (+) X c= X (+) Y
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (+) Y or p in Y (+) X )
assume p in X (+) Y ; ::_thesis: p in Y (+) X
then ex p1, p2 being Point of T st
( p = p1 + p2 & p1 in X & p2 in Y ) ;
hence p in Y (+) X ; ::_thesis: verum
end;
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Y (+) X or p in X (+) Y )
assume p in Y (+) X ; ::_thesis: p in X (+) Y
then ex p1, p2 being Point of T st
( p = p1 + p2 & p1 in Y & p2 in X ) ;
hence p in X (+) Y ; ::_thesis: verum
end;
Lm2: for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for p, x being Point of T holds
( (p - x) + x = p & (p + x) - x = p )
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for p, x being Point of T holds
( (p - x) + x = p & (p + x) - x = p )
let p, x be Point of T; ::_thesis: ( (p - x) + x = p & (p + x) - x = p )
(p + x) - x = p + (x - x) by RLVECT_1:def_3
.= p + (0. T) by RLVECT_1:15
.= p by RLVECT_1:4 ;
hence ( (p - x) + x = p & (p + x) - x = p ) by RLVECT_1:28; ::_thesis: verum
end;
theorem Th13: :: MATHMORP:13
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for Y, X being Subset of T
for y, x being Point of T holds
( Y + y c= X + x iff Y + (y - x) c= X )
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for Y, X being Subset of T
for y, x being Point of T holds
( Y + y c= X + x iff Y + (y - x) c= X )
let Y, X be Subset of T; ::_thesis: for y, x being Point of T holds
( Y + y c= X + x iff Y + (y - x) c= X )
let y, x be Point of T; ::_thesis: ( Y + y c= X + x iff Y + (y - x) c= X )
thus ( Y + y c= X + x implies Y + (y - x) c= X ) ::_thesis: ( Y + (y - x) c= X implies Y + y c= X + x )
proof
assume A1: Y + y c= X + x ; ::_thesis: Y + (y - x) c= X
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Y + (y - x) or p in X )
assume p in Y + (y - x) ; ::_thesis: p in X
then consider q1 being Point of T such that
A2: p = q1 + (y - x) and
A3: q1 in Y ;
reconsider p = p as Point of T by A2;
p = (q1 + y) - x by A2, RLVECT_1:28;
then A4: p + x = q1 + y by Lm2;
q1 + y in { (q + y) where q is Point of T : q in Y } by A3;
then p + x in X + x by A1, A4;
then consider p1 being Point of T such that
A5: p + x = p1 + x and
A6: p1 in X ;
(p + x) - x = p1 by A5, Lm2;
hence p in X by A6, Lm2; ::_thesis: verum
end;
assume A7: Y + (y - x) c= X ; ::_thesis: Y + y c= X + x
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Y + y or p in X + x )
assume p in Y + y ; ::_thesis: p in X + x
then consider q1 being Point of T such that
A8: p = q1 + y and
A9: q1 in Y ;
reconsider p = p as Point of T by A8;
( p - x = q1 + (y - x) & q1 + (y - x) in { (q + (y - x)) where q is Point of T : q in Y } ) by A8, A9, RLVECT_1:28;
then (p - x) + x in { (q + x) where q is Point of T : q in X } by A7;
hence p in X + x by Lm2; ::_thesis: verum
end;
theorem Th14: :: MATHMORP:14
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds (X + p) (-) Y = (X (-) Y) + p
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T
for p being Point of T holds (X + p) (-) Y = (X (-) Y) + p
let X, Y be Subset of T; ::_thesis: for p being Point of T holds (X + p) (-) Y = (X (-) Y) + p
let p be Point of T; ::_thesis: (X + p) (-) Y = (X (-) Y) + p
thus (X + p) (-) Y c= (X (-) Y) + p :: according to XBOOLE_0:def_10 ::_thesis: (X (-) Y) + p c= (X + p) (-) Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X + p) (-) Y or x in (X (-) Y) + p )
assume x in (X + p) (-) Y ; ::_thesis: x in (X (-) Y) + p
then consider y being Point of T such that
A1: x = y and
A2: Y + y c= X + p ;
Y + (y - p) c= X by A2, Th13;
then y - p in { y1 where y1 is Point of T : Y + y1 c= X } ;
then (y - p) + p in { (q + p) where q is Point of T : q in X (-) Y } ;
hence x in (X (-) Y) + p by A1, Lm2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) Y) + p or x in (X + p) (-) Y )
assume x in (X (-) Y) + p ; ::_thesis: x in (X + p) (-) Y
then consider y being Point of T such that
A3: x = y + p and
A4: y in X (-) Y ;
reconsider x = x as Point of T by A3;
( x - p = y & ex y2 being Point of T st
( y = y2 & Y + y2 c= X ) ) by A3, A4, Lm2;
then Y + x c= X + p by Th13;
hence x in (X + p) (-) Y ; ::_thesis: verum
end;
theorem Th15: :: MATHMORP:15
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds (X + p) (+) Y = (X (+) Y) + p
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T
for p being Point of T holds (X + p) (+) Y = (X (+) Y) + p
let X, Y be Subset of T; ::_thesis: for p being Point of T holds (X + p) (+) Y = (X (+) Y) + p
let p be Point of T; ::_thesis: (X + p) (+) Y = (X (+) Y) + p
thus (X + p) (+) Y c= (X (+) Y) + p :: according to XBOOLE_0:def_10 ::_thesis: (X (+) Y) + p c= (X + p) (+) Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X + p) (+) Y or x in (X (+) Y) + p )
assume x in (X + p) (+) Y ; ::_thesis: x in (X (+) Y) + p
then consider x2, y2 being Point of T such that
A1: x = x2 + y2 and
A2: x2 in X + p and
A3: y2 in Y ;
consider x3 being Point of T such that
A4: ( x2 = x3 + p & x3 in X ) by A2;
( x = (x3 + y2) + p & x3 + y2 in X (+) Y ) by A1, A3, A4, RLVECT_1:def_3;
hence x in (X (+) Y) + p ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (+) Y) + p or x in (X + p) (+) Y )
assume x in (X (+) Y) + p ; ::_thesis: x in (X + p) (+) Y
then consider x2 being Point of T such that
A5: x = x2 + p and
A6: x2 in X (+) Y ;
consider x3, y3 being Point of T such that
A7: x2 = x3 + y3 and
A8: x3 in X and
A9: y3 in Y by A6;
A10: x3 + p in X + p by A8;
x = (x3 + p) + y3 by A5, A7, RLVECT_1:def_3;
hence x in (X + p) (+) Y by A9, A10; ::_thesis: verum
end;
theorem Th16: :: MATHMORP:16
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T
for x, y being Point of T holds (X + x) + y = X + (x + y)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T
for x, y being Point of T holds (X + x) + y = X + (x + y)
let X be Subset of T; ::_thesis: for x, y being Point of T holds (X + x) + y = X + (x + y)
let x, y be Point of T; ::_thesis: (X + x) + y = X + (x + y)
thus (X + x) + y c= X + (x + y) :: according to XBOOLE_0:def_10 ::_thesis: X + (x + y) c= (X + x) + y
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in (X + x) + y or p in X + (x + y) )
assume p in (X + x) + y ; ::_thesis: p in X + (x + y)
then consider x2 being Point of T such that
A1: p = x2 + y and
A2: x2 in X + x ;
consider x3 being Point of T such that
A3: x2 = x3 + x and
A4: x3 in X by A2;
p = x3 + (x + y) by A1, A3, RLVECT_1:def_3;
hence p in X + (x + y) by A4; ::_thesis: verum
end;
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X + (x + y) or p in (X + x) + y )
assume p in X + (x + y) ; ::_thesis: p in (X + x) + y
then consider x2 being Point of T such that
A5: ( p = x2 + (x + y) & x2 in X ) ;
( p = (x2 + x) + y & x2 + x in X + x ) by A5, RLVECT_1:def_3;
hence p in (X + x) + y ; ::_thesis: verum
end;
theorem Th17: :: MATHMORP:17
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds X (-) (Y + p) = (X (-) Y) + (- p)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T
for p being Point of T holds X (-) (Y + p) = (X (-) Y) + (- p)
let X, Y be Subset of T; ::_thesis: for p being Point of T holds X (-) (Y + p) = (X (-) Y) + (- p)
let p be Point of T; ::_thesis: X (-) (Y + p) = (X (-) Y) + (- p)
thus X (-) (Y + p) c= (X (-) Y) + (- p) :: according to XBOOLE_0:def_10 ::_thesis: (X (-) Y) + (- p) c= X (-) (Y + p)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (-) (Y + p) or x in (X (-) Y) + (- p) )
assume x in X (-) (Y + p) ; ::_thesis: x in (X (-) Y) + (- p)
then consider y being Point of T such that
A1: x = y and
A2: (Y + p) + y c= X ;
Y + (y + p) c= X by A2, Th16;
then y + p in { y1 where y1 is Point of T : Y + y1 c= X } ;
then (y + p) - p in (X (-) Y) + (- p) ;
hence x in (X (-) Y) + (- p) by A1, Lm2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) Y) + (- p) or x in X (-) (Y + p) )
assume x in (X (-) Y) + (- p) ; ::_thesis: x in X (-) (Y + p)
then consider y being Point of T such that
A3: x = y + (- p) and
A4: y in X (-) Y ;
reconsider x = x as Point of T by A3;
x + p = (y - p) + p by A3;
then A5: x + p = y by Lm2;
ex y2 being Point of T st
( y = y2 & Y + y2 c= X ) by A4;
then (Y + p) + x c= X by A5, Th16;
hence x in X (-) (Y + p) ; ::_thesis: verum
end;
theorem :: MATHMORP:18
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds X (+) (Y + p) = (X (+) Y) + p
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T
for p being Point of T holds X (+) (Y + p) = (X (+) Y) + p
let X, Y be Subset of T; ::_thesis: for p being Point of T holds X (+) (Y + p) = (X (+) Y) + p
let p be Point of T; ::_thesis: X (+) (Y + p) = (X (+) Y) + p
thus X (+) (Y + p) c= (X (+) Y) + p :: according to XBOOLE_0:def_10 ::_thesis: (X (+) Y) + p c= X (+) (Y + p)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (+) (Y + p) or x in (X (+) Y) + p )
assume x in X (+) (Y + p) ; ::_thesis: x in (X (+) Y) + p
then consider x2, y2 being Point of T such that
A1: ( x = x2 + y2 & x2 in X ) and
A2: y2 in Y + p ;
consider y3 being Point of T such that
A3: ( y2 = y3 + p & y3 in Y ) by A2;
( x = (x2 + y3) + p & x2 + y3 in X (+) Y ) by A1, A3, RLVECT_1:def_3;
hence x in (X (+) Y) + p ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (+) Y) + p or x in X (+) (Y + p) )
assume x in (X (+) Y) + p ; ::_thesis: x in X (+) (Y + p)
then consider x2 being Point of T such that
A4: x = x2 + p and
A5: x2 in X (+) Y ;
consider x3, y3 being Point of T such that
A6: x2 = x3 + y3 and
A7: x3 in X and
A8: y3 in Y by A5;
A9: y3 + p in Y + p by A8;
x = x3 + (y3 + p) by A4, A6, RLVECT_1:def_3;
hence x in X (+) (Y + p) by A7, A9; ::_thesis: verum
end;
theorem Th19: :: MATHMORP:19
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T
for x being Point of T st x in X holds
B + x c= B (+) X
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T
for x being Point of T st x in X holds
B + x c= B (+) X
let X, B be Subset of T; ::_thesis: for x being Point of T st x in X holds
B + x c= B (+) X
let x be Point of T; ::_thesis: ( x in X implies B + x c= B (+) X )
assume A1: x in X ; ::_thesis: B + x c= B (+) X
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B + x or y in B (+) X )
assume y in B + x ; ::_thesis: y in B (+) X
then ex y1 being Point of T st
( y = y1 + x & y1 in B ) ;
hence y in B (+) X by A1; ::_thesis: verum
end;
theorem Th20: :: MATHMORP:20
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds X c= (X (+) B) (-) B
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds X c= (X (+) B) (-) B
let X, B be Subset of T; ::_thesis: X c= (X (+) B) (-) B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (X (+) B) (-) B )
assume A1: x in X ; ::_thesis: x in (X (+) B) (-) B
then consider x1 being Point of T such that
A2: x1 = x ;
B + x1 c= B (+) X by A1, A2, Th19;
then x in (B (+) X) (-) B by A2;
hence x in (X (+) B) (-) B by Th12; ::_thesis: verum
end;
theorem Th21: :: MATHMORP:21
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T holds X + (0. T) = X
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T holds X + (0. T) = X
let X be Subset of T; ::_thesis: X + (0. T) = X
thus X + (0. T) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X + (0. T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X + (0. T) or x in X )
assume x in X + (0. T) ; ::_thesis: x in X
then ex q being Point of T st
( x = q + (0. T) & q in X ) ;
hence x in X by RLVECT_1:4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X + (0. T) )
assume A1: x in X ; ::_thesis: x in X + (0. T)
then reconsider x1 = x as Point of T ;
x1 = x1 + (0. T) by RLVECT_1:4;
hence x in X + (0. T) by A1; ::_thesis: verum
end;
theorem :: MATHMORP:22
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T
for x being Point of T holds X (-) {x} = X + (- x)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T
for x being Point of T holds X (-) {x} = X + (- x)
let X be Subset of T; ::_thesis: for x being Point of T holds X (-) {x} = X + (- x)
let x be Point of T; ::_thesis: X (-) {x} = X + (- x)
thus X (-) {x} c= X + (- x) :: according to XBOOLE_0:def_10 ::_thesis: X + (- x) c= X (-) {x}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X (-) {x} or y in X + (- x) )
assume y in X (-) {x} ; ::_thesis: y in X + (- x)
then consider p being Point of T such that
A1: p = y and
A2: {x} + p c= X ;
{p} + x c= X by A2, Lm1;
then ({p} + x) + (- x) c= X + (- x) by Th3;
then {p} + (x + (- x)) c= X + (- x) by Th16;
then {p} + (0. T) c= X + (- x) by RLVECT_1:5;
then {p} c= X + (- x) by Th21;
hence y in X + (- x) by A1, ZFMISC_1:31; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X + (- x) or y in X (-) {x} )
assume y in X + (- x) ; ::_thesis: y in X (-) {x}
then consider p being Point of T such that
A3: y = p + (- x) and
A4: p in X ;
reconsider y = y as Point of T by A3;
y = p - x by A3;
then A5: y + x = p by Lm2;
{x} + y c= X
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in {x} + y or q in X )
assume q in {x} + y ; ::_thesis: q in X
then consider qq being Point of T such that
A6: q = qq + y and
A7: qq in {x} ;
{qq} c= {x} by A7, ZFMISC_1:31;
hence q in X by A4, A5, A6, ZFMISC_1:18; ::_thesis: verum
end;
hence y in X (-) {x} ; ::_thesis: verum
end;
Lm3: for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds (X (-) B) (+) B c= X
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds (X (-) B) (+) B c= X
let X, B be Subset of T; ::_thesis: (X (-) B) (+) B c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) B) (+) B or x in X )
assume x in (X (-) B) (+) B ; ::_thesis: x in X
then consider y1, y2 being Point of T such that
A1: x = y1 + y2 and
A2: y1 in X (-) B and
A3: y2 in B ;
consider y being Point of T such that
A4: y1 = y and
A5: B + y c= X by A2;
x in B + y by A1, A3, A4;
hence x in X by A5; ::_thesis: verum
end;
theorem Th23: :: MATHMORP:23
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Y) (-) Z
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Y) (-) Z
let X, Y, Z be Subset of T; ::_thesis: X (-) (Y (+) Z) = (X (-) Y) (-) Z
A1: (X (-) Y) (+) Y c= X by Lm3;
thus X (-) (Y (+) Z) c= (X (-) Y) (-) Z :: according to XBOOLE_0:def_10 ::_thesis: (X (-) Y) (-) Z c= X (-) (Y (+) Z)
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (-) (Y (+) Z) or p in (X (-) Y) (-) Z )
assume p in X (-) (Y (+) Z) ; ::_thesis: p in (X (-) Y) (-) Z
then consider x being Point of T such that
A2: p = x and
A3: (Y (+) Z) + x c= X ;
(Y + x) (+) Z c= X by A3, Th15;
then Z (+) (Y + x) c= X by Th12;
then A4: (Z (+) (Y + x)) (-) (Y + x) c= X (-) (Y + x) by Th9;
Z c= (Z (+) (Y + x)) (-) (Y + x) by Th20;
then Z c= X (-) (Y + x) by A4, XBOOLE_1:1;
then Z c= (X (-) Y) + (- x) by Th17;
then Z + x c= ((X (-) Y) + (- x)) + x by Th3;
then Z + x c= (X (-) Y) + ((- x) + x) by Th16;
then Z + x c= (X (-) Y) + (x - x) ;
then Z + x c= (X (-) Y) + (0. T) by RLVECT_1:15;
then Z + x c= X (-) Y by Th21;
hence p in (X (-) Y) (-) Z by A2; ::_thesis: verum
end;
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in (X (-) Y) (-) Z or p in X (-) (Y (+) Z) )
assume p in (X (-) Y) (-) Z ; ::_thesis: p in X (-) (Y (+) Z)
then consider y being Point of T such that
A5: p = y and
A6: Z + y c= X (-) Y ;
(Z + y) (+) Y c= (X (-) Y) (+) Y by A6, Th9;
then (Z + y) (+) Y c= X by A1, XBOOLE_1:1;
then (Z (+) Y) + y c= X by Th15;
then p in X (-) (Z (+) Y) by A5;
hence p in X (-) (Y (+) Z) by Th12; ::_thesis: verum
end;
theorem :: MATHMORP:24
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Z) (-) Y
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, Z being Subset of T holds X (-) (Y (+) Z) = (X (-) Z) (-) Y
let X, Y, Z be Subset of T; ::_thesis: X (-) (Y (+) Z) = (X (-) Z) (-) Y
X (-) (Y (+) Z) = X (-) (Z (+) Y) by Th12
.= (X (-) Z) (-) Y by Th23 ;
hence X (-) (Y (+) Z) = (X (-) Z) (-) Y ; ::_thesis: verum
end;
theorem :: MATHMORP:25
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, Z being Subset of T holds X (+) (Y (-) Z) c= (X (+) Y) (-) Z
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, Z being Subset of T holds X (+) (Y (-) Z) c= (X (+) Y) (-) Z
let X, Y, Z be Subset of T; ::_thesis: X (+) (Y (-) Z) c= (X (+) Y) (-) Z
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (+) (Y (-) Z) or x in (X (+) Y) (-) Z )
assume x in X (+) (Y (-) Z) ; ::_thesis: x in (X (+) Y) (-) Z
then consider a, b being Point of T such that
A1: x = a + b and
A2: a in X and
A3: b in Y (-) Z ;
ex c being Point of T st
( b = c & Z + c c= Y ) by A3;
then (Z + b) + a c= Y + a by Th3;
then A4: Z + (b + a) c= Y + a by Th16;
Y + a c= Y (+) X by A2, Th19;
then Z + (b + a) c= Y (+) X by A4, XBOOLE_1:1;
then x in (Y (+) X) (-) Z by A1;
hence x in (X (+) Y) (-) Z by Th12; ::_thesis: verum
end;
theorem :: MATHMORP:26
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, Z being Subset of T holds X (+) (Y (+) Z) = (X (+) Y) (+) Z
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, Z being Subset of T holds X (+) (Y (+) Z) = (X (+) Y) (+) Z
let X, Y, Z be Subset of T; ::_thesis: X (+) (Y (+) Z) = (X (+) Y) (+) Z
thus X (+) (Y (+) Z) c= (X (+) Y) (+) Z :: according to XBOOLE_0:def_10 ::_thesis: (X (+) Y) (+) Z c= X (+) (Y (+) Z)
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in X (+) (Y (+) Z) or p in (X (+) Y) (+) Z )
assume p in X (+) (Y (+) Z) ; ::_thesis: p in (X (+) Y) (+) Z
then consider x1, p2 being Point of T such that
A1: ( p = x1 + p2 & x1 in X ) and
A2: p2 in Y (+) Z ;
consider y, z being Point of T such that
A3: ( p2 = y + z & y in Y ) and
A4: z in Z by A2;
set p3 = x1 + y;
( p = (x1 + y) + z & x1 + y in X (+) Y ) by A1, A3, RLVECT_1:def_3;
hence p in (X (+) Y) (+) Z by A4; ::_thesis: verum
end;
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in (X (+) Y) (+) Z or p in X (+) (Y (+) Z) )
assume p in (X (+) Y) (+) Z ; ::_thesis: p in X (+) (Y (+) Z)
then consider x1, p2 being Point of T such that
A5: p = x1 + p2 and
A6: x1 in X (+) Y and
A7: p2 in Z ;
consider y, z being Point of T such that
A8: x1 = y + z and
A9: y in X and
A10: z in Y by A6;
set p3 = z + p2;
( p = y + (z + p2) & z + p2 in Y (+) Z ) by A5, A7, A8, A10, RLVECT_1:def_3;
hence p in X (+) (Y (+) Z) by A9; ::_thesis: verum
end;
theorem Th27: :: MATHMORP:27
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, C being Subset of T
for y being Point of T holds (B \/ C) + y = (B + y) \/ (C + y)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, C being Subset of T
for y being Point of T holds (B \/ C) + y = (B + y) \/ (C + y)
let B, C be Subset of T; ::_thesis: for y being Point of T holds (B \/ C) + y = (B + y) \/ (C + y)
let y be Point of T; ::_thesis: (B \/ C) + y = (B + y) \/ (C + y)
thus (B \/ C) + y c= (B + y) \/ (C + y) :: according to XBOOLE_0:def_10 ::_thesis: (B + y) \/ (C + y) c= (B \/ C) + y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B \/ C) + y or x in (B + y) \/ (C + y) )
assume x in (B \/ C) + y ; ::_thesis: x in (B + y) \/ (C + y)
then consider y2 being Point of T such that
A1: x = y2 + y and
A2: y2 in B \/ C ;
( y2 in B or y2 in C ) by A2, XBOOLE_0:def_3;
then ( x in { (y1 + y) where y1 is Point of T : y1 in B } or x in { (y1 + y) where y1 is Point of T : y1 in C } ) by A1;
hence x in (B + y) \/ (C + y) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B + y) \/ (C + y) or x in (B \/ C) + y )
assume x in (B + y) \/ (C + y) ; ::_thesis: x in (B \/ C) + y
then ( x in B + y or x in C + y ) by XBOOLE_0:def_3;
then consider y2 being Point of T such that
A3: ( ( x = y2 + y & y2 in B ) or ( x = y2 + y & y2 in C ) ) ;
y2 in B \/ C by A3, XBOOLE_0:def_3;
hence x in (B \/ C) + y by A3; ::_thesis: verum
end;
theorem Th28: :: MATHMORP:28
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, C being Subset of T
for y being Point of T holds (B /\ C) + y = (B + y) /\ (C + y)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, C being Subset of T
for y being Point of T holds (B /\ C) + y = (B + y) /\ (C + y)
let B, C be Subset of T; ::_thesis: for y being Point of T holds (B /\ C) + y = (B + y) /\ (C + y)
let y be Point of T; ::_thesis: (B /\ C) + y = (B + y) /\ (C + y)
thus (B /\ C) + y c= (B + y) /\ (C + y) :: according to XBOOLE_0:def_10 ::_thesis: (B + y) /\ (C + y) c= (B /\ C) + y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B /\ C) + y or x in (B + y) /\ (C + y) )
assume x in (B /\ C) + y ; ::_thesis: x in (B + y) /\ (C + y)
then consider y2 being Point of T such that
A1: x = y2 + y and
A2: y2 in B /\ C ;
y2 in C by A2, XBOOLE_0:def_4;
then A3: x in { (y1 + y) where y1 is Point of T : y1 in C } by A1;
y2 in B by A2, XBOOLE_0:def_4;
then x in { (y1 + y) where y1 is Point of T : y1 in B } by A1;
hence x in (B + y) /\ (C + y) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B + y) /\ (C + y) or x in (B /\ C) + y )
assume A4: x in (B + y) /\ (C + y) ; ::_thesis: x in (B /\ C) + y
then x in B + y by XBOOLE_0:def_4;
then consider y3 being Point of T such that
A5: x = y3 + y and
A6: y3 in B ;
x in C + y by A4, XBOOLE_0:def_4;
then consider y2 being Point of T such that
A7: x = y2 + y and
A8: y2 in C ;
(y2 + y) - y = y3 by A5, A7, Lm2;
then A9: y2 = y3 by Lm2;
then y2 in B /\ C by A6, A8, XBOOLE_0:def_4;
hence x in (B /\ C) + y by A5, A9; ::_thesis: verum
end;
theorem :: MATHMORP:29
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B, C being Subset of T holds X (-) (B \/ C) = (X (-) B) /\ (X (-) C)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B, C being Subset of T holds X (-) (B \/ C) = (X (-) B) /\ (X (-) C)
let X, B, C be Subset of T; ::_thesis: X (-) (B \/ C) = (X (-) B) /\ (X (-) C)
thus X (-) (B \/ C) c= (X (-) B) /\ (X (-) C) :: according to XBOOLE_0:def_10 ::_thesis: (X (-) B) /\ (X (-) C) c= X (-) (B \/ C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (-) (B \/ C) or x in (X (-) B) /\ (X (-) C) )
assume x in X (-) (B \/ C) ; ::_thesis: x in (X (-) B) /\ (X (-) C)
then consider y being Point of T such that
A1: x = y and
A2: (B \/ C) + y c= X ;
A3: (B + y) \/ (C + y) c= X by A2, Th27;
then C + y c= X by XBOOLE_1:11;
then A4: x in { y1 where y1 is Point of T : C + y1 c= X } by A1;
B + y c= X by A3, XBOOLE_1:11;
then x in { y1 where y1 is Point of T : B + y1 c= X } by A1;
hence x in (X (-) B) /\ (X (-) C) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) B) /\ (X (-) C) or x in X (-) (B \/ C) )
assume A5: x in (X (-) B) /\ (X (-) C) ; ::_thesis: x in X (-) (B \/ C)
then x in X (-) B by XBOOLE_0:def_4;
then consider y being Point of T such that
A6: x = y and
A7: B + y c= X ;
x in X (-) C by A5, XBOOLE_0:def_4;
then ex y2 being Point of T st
( x = y2 & C + y2 c= X ) ;
then (B + y) \/ (C + y) c= X by A6, A7, XBOOLE_1:8;
then (B \/ C) + y c= X by Th27;
hence x in X (-) (B \/ C) by A6; ::_thesis: verum
end;
theorem :: MATHMORP:30
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B, C being Subset of T holds X (+) (B \/ C) = (X (+) B) \/ (X (+) C)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B, C being Subset of T holds X (+) (B \/ C) = (X (+) B) \/ (X (+) C)
let X, B, C be Subset of T; ::_thesis: X (+) (B \/ C) = (X (+) B) \/ (X (+) C)
thus X (+) (B \/ C) c= (X (+) B) \/ (X (+) C) :: according to XBOOLE_0:def_10 ::_thesis: (X (+) B) \/ (X (+) C) c= X (+) (B \/ C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (+) (B \/ C) or x in (X (+) B) \/ (X (+) C) )
assume x in X (+) (B \/ C) ; ::_thesis: x in (X (+) B) \/ (X (+) C)
then consider y3, y4 being Point of T such that
A1: ( x = y3 + y4 & y3 in X ) and
A2: y4 in B \/ C ;
( y4 in B or y4 in C ) by A2, XBOOLE_0:def_3;
then ( x in { (y1 + y2) where y1, y2 is Point of T : ( y1 in X & y2 in B ) } or x in { (y1 + y2) where y1, y2 is Point of T : ( y1 in X & y2 in C ) } ) by A1;
hence x in (X (+) B) \/ (X (+) C) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (+) B) \/ (X (+) C) or x in X (+) (B \/ C) )
assume x in (X (+) B) \/ (X (+) C) ; ::_thesis: x in X (+) (B \/ C)
then ( x in X (+) B or x in X (+) C ) by XBOOLE_0:def_3;
then consider y3, y4 being Point of T such that
A3: ( ( x = y3 + y4 & y3 in X & y4 in B ) or ( x = y3 + y4 & y3 in X & y4 in C ) ) ;
y4 in B \/ C by A3, XBOOLE_0:def_3;
hence x in X (+) (B \/ C) by A3; ::_thesis: verum
end;
theorem :: MATHMORP:31
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B, Y being Subset of T holds (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B, Y being Subset of T holds (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B
let X, B, Y be Subset of T; ::_thesis: (X (-) B) \/ (Y (-) B) c= (X \/ Y) (-) B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) B) \/ (Y (-) B) or x in (X \/ Y) (-) B )
assume x in (X (-) B) \/ (Y (-) B) ; ::_thesis: x in (X \/ Y) (-) B
then ( x in X (-) B or x in Y (-) B ) by XBOOLE_0:def_3;
then consider y being Point of T such that
A1: ( ( x = y & B + y c= X ) or ( x = y & B + y c= Y ) ) ;
B + y c= X \/ Y
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in B + y or z in X \/ Y )
assume z in B + y ; ::_thesis: z in X \/ Y
hence z in X \/ Y by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
hence x in (X \/ Y) (-) B by A1; ::_thesis: verum
end;
theorem :: MATHMORP:32
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, B being Subset of T holds (X \/ Y) (+) B = (X (+) B) \/ (Y (+) B)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, B being Subset of T holds (X \/ Y) (+) B = (X (+) B) \/ (Y (+) B)
let X, Y, B be Subset of T; ::_thesis: (X \/ Y) (+) B = (X (+) B) \/ (Y (+) B)
thus (X \/ Y) (+) B c= (X (+) B) \/ (Y (+) B) :: according to XBOOLE_0:def_10 ::_thesis: (X (+) B) \/ (Y (+) B) c= (X \/ Y) (+) B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X \/ Y) (+) B or x in (X (+) B) \/ (Y (+) B) )
assume x in (X \/ Y) (+) B ; ::_thesis: x in (X (+) B) \/ (Y (+) B)
then consider y1, y2 being Point of T such that
A1: x = y1 + y2 and
A2: y1 in X \/ Y and
A3: y2 in B ;
( y1 in X or y1 in Y ) by A2, XBOOLE_0:def_3;
then ( x in { (y3 + y4) where y3, y4 is Point of T : ( y3 in X & y4 in B ) } or x in { (y3 + y4) where y3, y4 is Point of T : ( y3 in Y & y4 in B ) } ) by A1, A3;
hence x in (X (+) B) \/ (Y (+) B) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (+) B) \/ (Y (+) B) or x in (X \/ Y) (+) B )
assume x in (X (+) B) \/ (Y (+) B) ; ::_thesis: x in (X \/ Y) (+) B
then ( x in X (+) B or x in Y (+) B ) by XBOOLE_0:def_3;
then consider y1, y2 being Point of T such that
A4: ( ( x = y1 + y2 & y1 in X & y2 in B ) or ( x = y1 + y2 & y1 in Y & y2 in B ) ) ;
y1 in X \/ Y by A4, XBOOLE_0:def_3;
hence x in (X \/ Y) (+) B by A4; ::_thesis: verum
end;
theorem :: MATHMORP:33
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, B being Subset of T holds (X /\ Y) (-) B = (X (-) B) /\ (Y (-) B)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, B being Subset of T holds (X /\ Y) (-) B = (X (-) B) /\ (Y (-) B)
let X, Y, B be Subset of T; ::_thesis: (X /\ Y) (-) B = (X (-) B) /\ (Y (-) B)
thus (X /\ Y) (-) B c= (X (-) B) /\ (Y (-) B) :: according to XBOOLE_0:def_10 ::_thesis: (X (-) B) /\ (Y (-) B) c= (X /\ Y) (-) B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X /\ Y) (-) B or x in (X (-) B) /\ (Y (-) B) )
assume x in (X /\ Y) (-) B ; ::_thesis: x in (X (-) B) /\ (Y (-) B)
then consider y being Point of T such that
A1: x = y and
A2: B + y c= X /\ Y ;
B + y c= Y by A2, XBOOLE_1:18;
then A3: x in { y1 where y1 is Point of T : B + y1 c= Y } by A1;
B + y c= X by A2, XBOOLE_1:18;
then x in { y1 where y1 is Point of T : B + y1 c= X } by A1;
hence x in (X (-) B) /\ (Y (-) B) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) B) /\ (Y (-) B) or x in (X /\ Y) (-) B )
assume A4: x in (X (-) B) /\ (Y (-) B) ; ::_thesis: x in (X /\ Y) (-) B
then x in X (-) B by XBOOLE_0:def_4;
then consider y being Point of T such that
A5: x = y and
A6: B + y c= X ;
x in Y (-) B by A4, XBOOLE_0:def_4;
then A7: ex y2 being Point of T st
( x = y2 & B + y2 c= Y ) ;
B + y c= X /\ Y
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in B + y or z in X /\ Y )
assume z in B + y ; ::_thesis: z in X /\ Y
hence z in X /\ Y by A5, A6, A7, XBOOLE_0:def_4; ::_thesis: verum
end;
hence x in (X /\ Y) (-) B by A5; ::_thesis: verum
end;
theorem Th34: :: MATHMORP:34
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, B being Subset of T holds (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, B being Subset of T holds (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B)
let X, Y, B be Subset of T; ::_thesis: (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X /\ Y) (+) B or x in (X (+) B) /\ (Y (+) B) )
assume x in (X /\ Y) (+) B ; ::_thesis: x in (X (+) B) /\ (Y (+) B)
then consider y1, y2 being Point of T such that
A1: x = y1 + y2 and
A2: y1 in X /\ Y and
A3: y2 in B ;
y1 in Y by A2, XBOOLE_0:def_4;
then A4: x in { (y3 + y4) where y3, y4 is Point of T : ( y3 in Y & y4 in B ) } by A1, A3;
y1 in X by A2, XBOOLE_0:def_4;
then x in { (y3 + y4) where y3, y4 is Point of T : ( y3 in X & y4 in B ) } by A1, A3;
hence x in (X (+) B) /\ (Y (+) B) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: MATHMORP:35
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, X, Y being Subset of T holds B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, X, Y being Subset of T holds B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)
let B, X, Y be Subset of T; ::_thesis: B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)
B (+) (X /\ Y) = (X /\ Y) (+) B by Th12;
then B (+) (X /\ Y) c= (X (+) B) /\ (Y (+) B) by Th34;
then B (+) (X /\ Y) c= (B (+) X) /\ (Y (+) B) by Th12;
hence B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y) by Th12; ::_thesis: verum
end;
theorem :: MATHMORP:36
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, X, Y being Subset of T holds (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, X, Y being Subset of T holds (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y)
let B, X, Y be Subset of T; ::_thesis: (B (-) X) \/ (B (-) Y) c= B (-) (X /\ Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B (-) X) \/ (B (-) Y) or x in B (-) (X /\ Y) )
assume x in (B (-) X) \/ (B (-) Y) ; ::_thesis: x in B (-) (X /\ Y)
then ( x in B (-) X or x in B (-) Y ) by XBOOLE_0:def_3;
then consider y being Point of T such that
A1: ( ( x = y & X + y c= B ) or ( x = y & Y + y c= B ) ) ;
(X + y) /\ (Y + y) c= B
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (X + y) /\ (Y + y) or a in B )
assume A2: a in (X + y) /\ (Y + y) ; ::_thesis: a in B
then A3: a in X + y by XBOOLE_0:def_4;
A4: a in Y + y by A2, XBOOLE_0:def_4;
percases ( X + y c= B or Y + y c= B ) by A1;
suppose X + y c= B ; ::_thesis: a in B
hence a in B by A3; ::_thesis: verum
end;
suppose Y + y c= B ; ::_thesis: a in B
hence a in B by A4; ::_thesis: verum
end;
end;
end;
then (X /\ Y) + y c= B by Th28;
hence x in B (-) (X /\ Y) by A1; ::_thesis: verum
end;
theorem Th37: :: MATHMORP:37
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds ((X `) (-) B) ` = X (+) (B !)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds ((X `) (-) B) ` = X (+) (B !)
let X, B be Subset of T; ::_thesis: ((X `) (-) B) ` = X (+) (B !)
thus ((X `) (-) B) ` c= X (+) (B !) :: according to XBOOLE_0:def_10 ::_thesis: X (+) (B !) c= ((X `) (-) B) `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((X `) (-) B) ` or x in X (+) (B !) )
assume A1: x in ((X `) (-) B) ` ; ::_thesis: x in X (+) (B !)
then reconsider x1 = x as Point of T ;
not x in (X `) (-) B by A1, XBOOLE_0:def_5;
then not B + x1 c= X ` ;
then B + x1 meets X by SUBSET_1:23;
then consider y being set such that
A2: y in B + x1 and
A3: y in X by XBOOLE_0:3;
reconsider y1 = y as Point of T by A2;
consider b1 being Point of T such that
A4: ( y = b1 + x1 & b1 in B ) by A2;
( x1 = y1 - b1 & - b1 in B ! ) by A4, Lm2;
hence x in X (+) (B !) by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (+) (B !) or x in ((X `) (-) B) ` )
assume x in X (+) (B !) ; ::_thesis: x in ((X `) (-) B) `
then consider x1, b1 being Point of T such that
A5: x = x1 + b1 and
A6: x1 in X and
A7: b1 in B ! ;
reconsider xx = x as Point of T by A5;
consider b2 being Point of T such that
A8: b1 = - b2 and
A9: b2 in B by A7;
x = x1 - b2 by A5, A8;
then A10: xx + b2 = x1 by Lm2;
b2 + xx in { (pb + xx) where pb is Point of T : pb in B } by A9;
then A11: B + xx meets X by A6, A10, XBOOLE_0:3;
not xx in (X `) (-) B
proof
assume xx in (X `) (-) B ; ::_thesis: contradiction
then ex yy being Point of T st
( xx = yy & B + yy c= X ` ) ;
hence contradiction by A11, SUBSET_1:23; ::_thesis: verum
end;
hence x in ((X `) (-) B) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th38: :: MATHMORP:38
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds (X (-) B) ` = (X `) (+) (B !)
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds (X (-) B) ` = (X `) (+) (B !)
let X, B be Subset of T; ::_thesis: (X (-) B) ` = (X `) (+) (B !)
thus (X (-) B) ` c= (X `) (+) (B !) :: according to XBOOLE_0:def_10 ::_thesis: (X `) (+) (B !) c= (X (-) B) `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X (-) B) ` or x in (X `) (+) (B !) )
assume A1: x in (X (-) B) ` ; ::_thesis: x in (X `) (+) (B !)
then reconsider x1 = x as Point of T ;
not x in X (-) B by A1, XBOOLE_0:def_5;
then not B + x1 c= X ;
then B + x1 meets X ` by SUBSET_1:24;
then consider y being set such that
A2: y in B + x1 and
A3: y in X ` by XBOOLE_0:3;
reconsider y1 = y as Point of T by A2;
consider b1 being Point of T such that
A4: ( y = b1 + x1 & b1 in B ) by A2;
( x1 = y1 - b1 & - b1 in B ! ) by A4, Lm2;
hence x in (X `) (+) (B !) by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X `) (+) (B !) or x in (X (-) B) ` )
assume x in (X `) (+) (B !) ; ::_thesis: x in (X (-) B) `
then consider x1, b1 being Point of T such that
A5: x = x1 + b1 and
A6: x1 in X ` and
A7: b1 in B ! ;
reconsider xx = x as Point of T by A5;
consider q being Point of T such that
A8: b1 = - q and
A9: q in B by A7;
xx = x1 - q by A5, A8;
then A10: xx + q = x1 by Lm2;
q + xx in { (q1 + xx) where q1 is Point of T : q1 in B } by A9;
then A11: B + xx meets X ` by A6, A10, XBOOLE_0:3;
not xx in X (-) B
proof
assume xx in X (-) B ; ::_thesis: contradiction
then ex yy being Point of T st
( xx = yy & B + yy c= X ) ;
hence contradiction by A11, SUBSET_1:24; ::_thesis: verum
end;
hence x in (X (-) B) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
begin
definition
let T be non empty addLoopStr ;
let X, B be Subset of T;
funcX (O) B -> Subset of T equals :: MATHMORP:def 4
(X (-) B) (+) B;
coherence
(X (-) B) (+) B is Subset of T ;
end;
:: deftheorem defines (O) MATHMORP:def_4_:_
for T being non empty addLoopStr
for X, B being Subset of T holds X (O) B = (X (-) B) (+) B;
definition
let T be non empty addLoopStr ;
let X, B be Subset of T;
funcX (o) B -> Subset of T equals :: MATHMORP:def 5
(X (+) B) (-) B;
coherence
(X (+) B) (-) B is Subset of T ;
end;
:: deftheorem defines (o) MATHMORP:def_5_:_
for T being non empty addLoopStr
for X, B being Subset of T holds X (o) B = (X (+) B) (-) B;
theorem :: MATHMORP:39
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds ((X `) (O) (B !)) ` = X (o) B
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds ((X `) (O) (B !)) ` = X (o) B
let X, B be Subset of T; ::_thesis: ((X `) (O) (B !)) ` = X (o) B
((X `) (O) (B !)) ` = (((((X `) (-) (B !)) `) (-) B) `) ` by Th37
.= (X (+) ((B !) !)) (-) B by Th37
.= (X (+) B) (-) B by Th1 ;
hence ((X `) (O) (B !)) ` = X (o) B ; ::_thesis: verum
end;
theorem :: MATHMORP:40
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds ((X `) (o) (B !)) ` = X (O) B
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds ((X `) (o) (B !)) ` = X (O) B
let X, B be Subset of T; ::_thesis: ((X `) (o) (B !)) ` = X (O) B
((X `) (o) (B !)) ` = (((X `) (+) (B !)) `) (+) ((B !) !) by Th38
.= (((X `) (+) (B !)) `) (+) B by Th1
.= (((X (-) B) `) `) (+) B by Th38 ;
hence ((X `) (o) (B !)) ` = X (O) B ; ::_thesis: verum
end;
theorem Th41: :: MATHMORP:41
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds
( X (O) B c= X & X c= X (o) B )
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds
( X (O) B c= X & X c= X (o) B )
let X, B be Subset of T; ::_thesis: ( X (O) B c= X & X c= X (o) B )
thus X (O) B c= X ::_thesis: X c= X (o) B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (O) B or x in X )
assume x in X (O) B ; ::_thesis: x in X
then consider y1, y2 being Point of T such that
A1: x = y1 + y2 and
A2: y1 in X (-) B and
A3: y2 in B ;
consider y being Point of T such that
A4: y1 = y and
A5: B + y c= X by A2;
x in B + y by A1, A3, A4;
hence x in X by A5; ::_thesis: verum
end;
thus X c= X (o) B by Th20; ::_thesis: verum
end;
theorem Th42: :: MATHMORP:42
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T holds X (O) X = X
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T holds X (O) X = X
let X be Subset of T; ::_thesis: X (O) X = X
thus X (O) X c= X by Th41; :: according to XBOOLE_0:def_10 ::_thesis: X c= X (O) X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X (O) X )
assume A1: x in X ; ::_thesis: x in X (O) X
then reconsider x1 = x as Point of T ;
X + (0. T) c= X by Th21;
then 0. T in X (-) X ;
then x1 + (0. T) in (X (-) X) (+) X by A1;
hence x in X (O) X by RLVECT_1:4; ::_thesis: verum
end;
theorem :: MATHMORP:43
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds
( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B )
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds
( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B )
let X, B be Subset of T; ::_thesis: ( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B )
X (O) B c= X by Th41;
hence ( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B ) by Th9; ::_thesis: verum
end;
theorem :: MATHMORP:44
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds
( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B )
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds
( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B )
let X, B be Subset of T; ::_thesis: ( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B )
X c= X (o) B by Th41;
hence ( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B ) by Th9; ::_thesis: verum
end;
theorem Th45: :: MATHMORP:45
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, B being Subset of T st X c= Y holds
( X (O) B c= Y (O) B & X (o) B c= Y (o) B )
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y, B being Subset of T st X c= Y holds
( X (O) B c= Y (O) B & X (o) B c= Y (o) B )
let X, Y, B be Subset of T; ::_thesis: ( X c= Y implies ( X (O) B c= Y (O) B & X (o) B c= Y (o) B ) )
assume A1: X c= Y ; ::_thesis: ( X (O) B c= Y (O) B & X (o) B c= Y (o) B )
thus X (O) B c= Y (O) B ::_thesis: X (o) B c= Y (o) B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (O) B or x in Y (O) B )
assume x in X (O) B ; ::_thesis: x in Y (O) B
then consider x2, b2 being Point of T such that
A2: x = x2 + b2 and
A3: x2 in X (-) B and
A4: b2 in B ;
consider y being Point of T such that
A5: x2 = y and
A6: B + y c= X by A3;
B + y c= Y by A1, A6, XBOOLE_1:1;
then x2 in { y1 where y1 is Point of T : B + y1 c= Y } by A5;
hence x in Y (O) B by A2, A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (o) B or x in Y (o) B )
assume x in X (o) B ; ::_thesis: x in Y (o) B
then consider x2 being Point of T such that
A7: x = x2 and
A8: B + x2 c= X (+) B ;
X (+) B c= Y (+) B by A1, Th9;
then B + x2 c= Y (+) B by A8, XBOOLE_1:1;
hence x in Y (o) B by A7; ::_thesis: verum
end;
theorem Th46: :: MATHMORP:46
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds (X + p) (O) Y = (X (O) Y) + p
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T
for p being Point of T holds (X + p) (O) Y = (X (O) Y) + p
let X, Y be Subset of T; ::_thesis: for p being Point of T holds (X + p) (O) Y = (X (O) Y) + p
let p be Point of T; ::_thesis: (X + p) (O) Y = (X (O) Y) + p
thus (X + p) (O) Y = ((X (-) Y) + p) (+) Y by Th14
.= (X (O) Y) + p by Th15 ; ::_thesis: verum
end;
theorem :: MATHMORP:47
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds (X + p) (o) Y = (X (o) Y) + p
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T
for p being Point of T holds (X + p) (o) Y = (X (o) Y) + p
let X, Y be Subset of T; ::_thesis: for p being Point of T holds (X + p) (o) Y = (X (o) Y) + p
let p be Point of T; ::_thesis: (X + p) (o) Y = (X (o) Y) + p
thus (X + p) (o) Y = ((X (+) Y) + p) (-) Y by Th15
.= (X (o) Y) + p by Th14 ; ::_thesis: verum
end;
theorem :: MATHMORP:48
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for C, B, X being Subset of T st C c= B holds
X (O) B c= (X (-) C) (+) B
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for C, B, X being Subset of T st C c= B holds
X (O) B c= (X (-) C) (+) B
let C, B, X be Subset of T; ::_thesis: ( C c= B implies X (O) B c= (X (-) C) (+) B )
assume A1: C c= B ; ::_thesis: X (O) B c= (X (-) C) (+) B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (O) B or x in (X (-) C) (+) B )
assume x in X (O) B ; ::_thesis: x in (X (-) C) (+) B
then consider x1, b1 being Point of T such that
A2: x = x1 + b1 and
A3: x1 in X (-) B and
A4: b1 in B ;
consider x2 being Point of T such that
A5: x1 = x2 and
A6: B + x2 c= X by A3;
C + x2 c= B + x2 by A1, Th3;
then C + x2 c= X by A6, XBOOLE_1:1;
then x1 in X (-) C by A5;
hence x in (X (-) C) (+) B by A2, A4; ::_thesis: verum
end;
theorem :: MATHMORP:49
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, C, X being Subset of T st B c= C holds
X (o) B c= (X (+) C) (-) B
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, C, X being Subset of T st B c= C holds
X (o) B c= (X (+) C) (-) B
let B, C, X be Subset of T; ::_thesis: ( B c= C implies X (o) B c= (X (+) C) (-) B )
assume B c= C ; ::_thesis: X (o) B c= (X (+) C) (-) B
then A1: X (+) B c= X (+) C by Th10;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (o) B or x in (X (+) C) (-) B )
assume x in X (o) B ; ::_thesis: x in (X (+) C) (-) B
then consider x2 being Point of T such that
A2: x = x2 and
A3: B + x2 c= X (+) B ;
B + x2 c= X (+) C by A3, A1, XBOOLE_1:1;
hence x in (X (+) C) (-) B by A2; ::_thesis: verum
end;
theorem Th50: :: MATHMORP:50
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T holds
( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y )
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T holds
( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y )
let X, Y be Subset of T; ::_thesis: ( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y )
(X (o) Y) (+) Y = (X (+) Y) (O) Y ;
then A1: (X (o) Y) (+) Y c= X (+) Y by Th41;
X c= X (o) Y by Th41;
then X (+) Y c= (X (o) Y) (+) Y by Th9;
hence X (+) Y = (X (o) Y) (+) Y by A1, XBOOLE_0:def_10; ::_thesis: X (-) Y = (X (O) Y) (-) Y
(X (O) Y) (-) Y = (X (-) Y) (o) Y ;
hence X (-) Y c= (X (O) Y) (-) Y by Th41; :: according to XBOOLE_0:def_10 ::_thesis: (X (O) Y) (-) Y c= X (-) Y
X (O) Y c= X by Th41;
hence (X (O) Y) (-) Y c= X (-) Y by Th9; ::_thesis: verum
end;
theorem :: MATHMORP:51
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T holds
( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y )
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, Y being Subset of T holds
( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y )
let X, Y be Subset of T; ::_thesis: ( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y )
(X (+) Y) (O) Y = (X (o) Y) (+) Y ;
hence X (+) Y = (X (+) Y) (O) Y by Th50; ::_thesis: X (-) Y = (X (-) Y) (o) Y
(X (-) Y) (o) Y = (X (O) Y) (-) Y ;
hence X (-) Y = (X (-) Y) (o) Y by Th50; ::_thesis: verum
end;
theorem :: MATHMORP:52
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds (X (O) B) (O) B = X (O) B
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B being Subset of T holds (X (O) B) (O) B = X (O) B
let X, B be Subset of T; ::_thesis: (X (O) B) (O) B = X (O) B
thus (X (O) B) (O) B c= X (O) B by Th41; :: according to XBOOLE_0:def_10 ::_thesis: X (O) B c= (X (O) B) (O) B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (O) B or x in (X (O) B) (O) B )
assume x in X (O) B ; ::_thesis: x in (X (O) B) (O) B
then consider x1, b1 being Point of T such that
A1: x = x1 + b1 and
A2: x1 in X (-) B and
A3: b1 in B ;
consider x2 being Point of T such that
A4: x1 = x2 and
A5: B + x2 c= X by A2;
(B + x2) (O) B c= X (O) B by A5, Th45;
then (B (O) B) + x2 c= X (O) B by Th46;
then B + x2 c= X (O) B by Th42;
then x1 in { x4 where x4 is Point of T : B + x4 c= X (O) B } by A4;
hence x in (X (O) B) (O) B by A1, A3; ::_thesis: verum
end;
theorem :: MATHMORP:53
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds (X (o) B) (o) B = X (o) B by Th50;
theorem :: MATHMORP:54
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B, Y being Subset of T holds X (O) B c= (X \/ Y) (O) B
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X, B, Y being Subset of T holds X (O) B c= (X \/ Y) (O) B
let X, B, Y be Subset of T; ::_thesis: X (O) B c= (X \/ Y) (O) B
X c= X \/ Y by XBOOLE_1:7;
hence X (O) B c= (X \/ Y) (O) B by Th45; ::_thesis: verum
end;
theorem :: MATHMORP:55
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, B1, X being Subset of T st B = B (O) B1 holds
X (O) B c= X (O) B1
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for B, B1, X being Subset of T st B = B (O) B1 holds
X (O) B c= X (O) B1
let B, B1, X be Subset of T; ::_thesis: ( B = B (O) B1 implies X (O) B c= X (O) B1 )
assume A1: B = B (O) B1 ; ::_thesis: X (O) B c= X (O) B1
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (O) B or x in X (O) B1 )
assume x in X (O) B ; ::_thesis: x in X (O) B1
then consider x1, b1 being Point of T such that
A2: x = x1 + b1 and
A3: x1 in X (-) B and
A4: b1 in B ;
consider x2 being Point of T such that
A5: ( x1 = x2 & B + x2 c= X ) by A3;
consider x3, b2 being Point of T such that
A6: b1 = x3 + b2 and
A7: x3 in B (-) B1 and
A8: b2 in B1 by A1, A4;
consider x4 being Point of T such that
A9: x3 = x4 and
A10: B1 + x4 c= B by A7;
(B1 + x4) + x2 c= B + x2 by A10, Th3;
then (B1 + x3) + x1 c= X by A5, A9, XBOOLE_1:1;
then B1 + (x3 + x1) c= X by Th16;
then x1 + x3 in X (-) B1 ;
then (x1 + x3) + b2 in (X (-) B1) (+) B1 by A8;
hence x in X (O) B1 by A2, A6, RLVECT_1:def_3; ::_thesis: verum
end;
begin
definition
let t be real number ;
let T be non empty RLSStruct ;
let A be Subset of T;
funct (.) A -> Subset of T equals :: MATHMORP:def 6
{ (t * a) where a is Point of T : a in A } ;
coherence
{ (t * a) where a is Point of T : a in A } is Subset of T
proof
now__::_thesis:_for_x_being_set_st_x_in__{__(t_*_a)_where_a_is_Point_of_T_:_a_in_A__}__holds_
x_in_the_carrier_of_T
let x be set ; ::_thesis: ( x in { (t * a) where a is Point of T : a in A } implies x in the carrier of T )
assume x in { (t * a) where a is Point of T : a in A } ; ::_thesis: x in the carrier of T
then ex q being Point of T st
( x = t * q & q in A ) ;
hence x in the carrier of T ; ::_thesis: verum
end;
hence { (t * a) where a is Point of T : a in A } is Subset of T by TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines (.) MATHMORP:def_6_:_
for t being real number
for T being non empty RLSStruct
for A being Subset of T holds t (.) A = { (t * a) where a is Point of T : a in A } ;
theorem :: MATHMORP:56
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T st X = {} holds
0 (.) X = {}
proof
let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; ::_thesis: for X being Subset of T st X = {} holds
0 (.) X = {}
let X be Subset of T; ::_thesis: ( X = {} implies 0 (.) X = {} )
assume A1: X = {} ; ::_thesis: 0 (.) X = {}
now__::_thesis:_for_x_being_set_holds_not_x_in_0_(.)_X
given x being set such that A2: x in 0 (.) X ; ::_thesis: contradiction
ex a being Point of T st
( x = 0 * a & a in X ) by A2;
hence contradiction by A1; ::_thesis: verum
end;
hence 0 (.) X = {} by XBOOLE_0:def_1; ::_thesis: verum
end;
theorem :: MATHMORP:57
for n being Element of NAT
for X being non empty Subset of (TOP-REAL n) holds 0 (.) X = {(0. (TOP-REAL n))}
proof
let n be Element of NAT ; ::_thesis: for X being non empty Subset of (TOP-REAL n) holds 0 (.) X = {(0. (TOP-REAL n))}
set T = TOP-REAL n;
let X be non empty Subset of (TOP-REAL n); ::_thesis: 0 (.) X = {(0. (TOP-REAL n))}
thus 0 (.) X c= {(0. (TOP-REAL n))} :: according to XBOOLE_0:def_10 ::_thesis: {(0. (TOP-REAL n))} c= 0 (.) X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in 0 (.) X or x in {(0. (TOP-REAL n))} )
assume x in 0 (.) X ; ::_thesis: x in {(0. (TOP-REAL n))}
then ex a being Point of (TOP-REAL n) st
( x = 0 * a & a in X ) ;
then x = 0. (TOP-REAL n) by EUCLID:29;
hence x in {(0. (TOP-REAL n))} by ZFMISC_1:31; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. (TOP-REAL n))} or x in 0 (.) X )
set d = the Element of X;
reconsider d1 = the Element of X as Point of (TOP-REAL n) ;
assume x in {(0. (TOP-REAL n))} ; ::_thesis: x in 0 (.) X
then {x} c= {(0. (TOP-REAL n))} by ZFMISC_1:31;
then x = 0. (TOP-REAL n) by ZFMISC_1:18;
then x = 0 * d1 by EUCLID:29;
hence x in 0 (.) X ; ::_thesis: verum
end;
theorem Th58: :: MATHMORP:58
for n being Element of NAT
for X being Subset of (TOP-REAL n) holds 1 (.) X = X
proof
let n be Element of NAT ; ::_thesis: for X being Subset of (TOP-REAL n) holds 1 (.) X = X
let X be Subset of (TOP-REAL n); ::_thesis: 1 (.) X = X
thus 1 (.) X c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= 1 (.) X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in 1 (.) X or x in X )
assume x in 1 (.) X ; ::_thesis: x in X
then ex z being Point of (TOP-REAL n) st
( x = 1 * z & z in X ) ;
hence x in X by EUCLID:29; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in 1 (.) X )
assume A1: x in X ; ::_thesis: x in 1 (.) X
then reconsider x1 = x as Point of (TOP-REAL n) ;
x1 = 1 * x1 by EUCLID:29;
hence x in 1 (.) X by A1; ::_thesis: verum
end;
theorem :: MATHMORP:59
for n being Element of NAT
for X being Subset of (TOP-REAL n) holds 2 (.) X c= X (+) X
proof
let n be Element of NAT ; ::_thesis: for X being Subset of (TOP-REAL n) holds 2 (.) X c= X (+) X
let X be Subset of (TOP-REAL n); ::_thesis: 2 (.) X c= X (+) X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in 2 (.) X or x in X (+) X )
assume x in 2 (.) X ; ::_thesis: x in X (+) X
then consider z being Point of (TOP-REAL n) such that
A1: x = 2 * z and
A2: z in X ;
x = (1 + 1) * z by A1
.= (1 * z) + (1 * z) by EUCLID:33
.= z + (1 * z) by EUCLID:29
.= z + z by EUCLID:29 ;
hence x in X (+) X by A2; ::_thesis: verum
end;
theorem Th60: :: MATHMORP:60
for t, s being real number
for n being Element of NAT
for X being Subset of (TOP-REAL n) holds (t * s) (.) X = t (.) (s (.) X)
proof
let t, s be real number ; ::_thesis: for n being Element of NAT
for X being Subset of (TOP-REAL n) holds (t * s) (.) X = t (.) (s (.) X)
let n be Element of NAT ; ::_thesis: for X being Subset of (TOP-REAL n) holds (t * s) (.) X = t (.) (s (.) X)
let X be Subset of (TOP-REAL n); ::_thesis: (t * s) (.) X = t (.) (s (.) X)
thus (t * s) (.) X c= t (.) (s (.) X) :: according to XBOOLE_0:def_10 ::_thesis: t (.) (s (.) X) c= (t * s) (.) X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (t * s) (.) X or x in t (.) (s (.) X) )
assume x in (t * s) (.) X ; ::_thesis: x in t (.) (s (.) X)
then consider z being Point of (TOP-REAL n) such that
A1: ( x = (t * s) * z & z in X ) ;
( x = t * (s * z) & s * z in s (.) X ) by A1, EUCLID:30;
hence x in t (.) (s (.) X) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in t (.) (s (.) X) or x in (t * s) (.) X )
assume x in t (.) (s (.) X) ; ::_thesis: x in (t * s) (.) X
then consider z being Point of (TOP-REAL n) such that
A2: x = t * z and
A3: z in s (.) X ;
consider z1 being Point of (TOP-REAL n) such that
A4: z = s * z1 and
A5: z1 in X by A3;
x = (t * s) * z1 by A2, A4, EUCLID:30;
hence x in (t * s) (.) X by A5; ::_thesis: verum
end;
theorem Th61: :: MATHMORP:61
for t being real number
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st X c= Y holds
t (.) X c= t (.) Y
proof
let t be real number ; ::_thesis: for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st X c= Y holds
t (.) X c= t (.) Y
let n be Element of NAT ; ::_thesis: for X, Y being Subset of (TOP-REAL n) st X c= Y holds
t (.) X c= t (.) Y
let X, Y be Subset of (TOP-REAL n); ::_thesis: ( X c= Y implies t (.) X c= t (.) Y )
assume A1: X c= Y ; ::_thesis: t (.) X c= t (.) Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in t (.) X or x in t (.) Y )
assume x in t (.) X ; ::_thesis: x in t (.) Y
then ex a being Point of (TOP-REAL n) st
( x = t * a & a in X ) ;
hence x in t (.) Y by A1; ::_thesis: verum
end;
theorem Th62: :: MATHMORP:62
for t being real number
for n being Element of NAT
for X being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x)
proof
let t be real number ; ::_thesis: for n being Element of NAT
for X being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x)
let n be Element of NAT ; ::_thesis: for X being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x)
let X be Subset of (TOP-REAL n); ::_thesis: for x being Point of (TOP-REAL n) holds t (.) (X + x) = (t (.) X) + (t * x)
let x be Point of (TOP-REAL n); ::_thesis: t (.) (X + x) = (t (.) X) + (t * x)
thus t (.) (X + x) c= (t (.) X) + (t * x) :: according to XBOOLE_0:def_10 ::_thesis: (t (.) X) + (t * x) c= t (.) (X + x)
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in t (.) (X + x) or b in (t (.) X) + (t * x) )
assume b in t (.) (X + x) ; ::_thesis: b in (t (.) X) + (t * x)
then consider a being Point of (TOP-REAL n) such that
A1: b = t * a and
A2: a in X + x ;
consider x1 being Point of (TOP-REAL n) such that
A3: a = x1 + x and
A4: x1 in X by A2;
A5: t * x1 in t (.) X by A4;
b = (t * x1) + (t * x) by A1, A3, EUCLID:32;
hence b in (t (.) X) + (t * x) by A5; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (t (.) X) + (t * x) or b in t (.) (X + x) )
assume b in (t (.) X) + (t * x) ; ::_thesis: b in t (.) (X + x)
then consider x1 being Point of (TOP-REAL n) such that
A6: b = x1 + (t * x) and
A7: x1 in t (.) X ;
consider a being Point of (TOP-REAL n) such that
A8: x1 = t * a and
A9: a in X by A7;
A10: a + x in X + x by A9;
b = t * (a + x) by A6, A8, EUCLID:32;
hence b in t (.) (X + x) by A10; ::_thesis: verum
end;
theorem Th63: :: MATHMORP:63
for t being real number
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) holds t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y)
proof
let t be real number ; ::_thesis: for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) holds t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y)
let n be Element of NAT ; ::_thesis: for X, Y being Subset of (TOP-REAL n) holds t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y)
let X, Y be Subset of (TOP-REAL n); ::_thesis: t (.) (X (+) Y) = (t (.) X) (+) (t (.) Y)
thus t (.) (X (+) Y) c= (t (.) X) (+) (t (.) Y) :: according to XBOOLE_0:def_10 ::_thesis: (t (.) X) (+) (t (.) Y) c= t (.) (X (+) Y)
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in t (.) (X (+) Y) or b in (t (.) X) (+) (t (.) Y) )
assume b in t (.) (X (+) Y) ; ::_thesis: b in (t (.) X) (+) (t (.) Y)
then consider a being Point of (TOP-REAL n) such that
A1: b = t * a and
A2: a in X (+) Y ;
consider x, y being Point of (TOP-REAL n) such that
A3: a = x + y and
A4: ( x in X & y in Y ) by A2;
A5: ( t * x in t (.) X & t * y in t (.) Y ) by A4;
b = (t * x) + (t * y) by A1, A3, EUCLID:32;
hence b in (t (.) X) (+) (t (.) Y) by A5; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (t (.) X) (+) (t (.) Y) or b in t (.) (X (+) Y) )
assume b in (t (.) X) (+) (t (.) Y) ; ::_thesis: b in t (.) (X (+) Y)
then consider x, y being Point of (TOP-REAL n) such that
A6: b = x + y and
A7: x in t (.) X and
A8: y in t (.) Y ;
consider y1 being Point of (TOP-REAL n) such that
A9: y = t * y1 and
A10: y1 in Y by A8;
consider x1 being Point of (TOP-REAL n) such that
A11: x = t * x1 and
A12: x1 in X by A7;
A13: x1 + y1 in X (+) Y by A12, A10;
b = t * (x1 + y1) by A6, A11, A9, EUCLID:32;
hence b in t (.) (X (+) Y) by A13; ::_thesis: verum
end;
theorem Th64: :: MATHMORP:64
for t being real number
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y)
proof
let t be real number ; ::_thesis: for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y)
let n be Element of NAT ; ::_thesis: for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y)
let X, Y be Subset of (TOP-REAL n); ::_thesis: ( t <> 0 implies t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y) )
assume A1: t <> 0 ; ::_thesis: t (.) (X (-) Y) = (t (.) X) (-) (t (.) Y)
thus t (.) (X (-) Y) c= (t (.) X) (-) (t (.) Y) :: according to XBOOLE_0:def_10 ::_thesis: (t (.) X) (-) (t (.) Y) c= t (.) (X (-) Y)
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in t (.) (X (-) Y) or b in (t (.) X) (-) (t (.) Y) )
assume b in t (.) (X (-) Y) ; ::_thesis: b in (t (.) X) (-) (t (.) Y)
then consider a being Point of (TOP-REAL n) such that
A2: b = t * a and
A3: a in X (-) Y ;
consider x being Point of (TOP-REAL n) such that
A4: a = x and
A5: Y + x c= X by A3;
t (.) (Y + x) c= t (.) X by A5, Th61;
then (t (.) Y) + (t * x) c= t (.) X by Th62;
hence b in (t (.) X) (-) (t (.) Y) by A2, A4; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (t (.) X) (-) (t (.) Y) or b in t (.) (X (-) Y) )
assume b in (t (.) X) (-) (t (.) Y) ; ::_thesis: b in t (.) (X (-) Y)
then consider x being Point of (TOP-REAL n) such that
A6: b = x and
A7: (t (.) Y) + x c= t (.) X ;
(1 / t) (.) ((t (.) Y) + x) c= (1 / t) (.) (t (.) X) by A7, Th61;
then (1 / t) (.) ((t (.) Y) + x) c= ((1 / t) * t) (.) X by Th60;
then ((1 / t) (.) (t (.) Y)) + ((1 / t) * x) c= ((1 / t) * t) (.) X by Th62;
then (((1 / t) * t) (.) Y) + ((1 / t) * x) c= ((1 / t) * t) (.) X by Th60;
then (1 (.) Y) + ((1 / t) * x) c= ((1 / t) * t) (.) X by A1, XCMPLX_1:87;
then (1 (.) Y) + ((1 / t) * x) c= 1 (.) X by A1, XCMPLX_1:87;
then Y + ((1 / t) * x) c= 1 (.) X by Th58;
then Y + ((1 / t) * x) c= X by Th58;
then (1 / t) * x in { z where z is Point of (TOP-REAL n) : Y + z c= X } ;
then t * ((1 / t) * x) in { (t * a1) where a1 is Point of (TOP-REAL n) : a1 in X (-) Y } ;
then ((1 / t) * t) * x in t (.) (X (-) Y) by EUCLID:30;
then 1 * x in t (.) (X (-) Y) by A1, XCMPLX_1:87;
hence b in t (.) (X (-) Y) by A6, EUCLID:29; ::_thesis: verum
end;
theorem :: MATHMORP:65
for t being real number
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y)
proof
let t be real number ; ::_thesis: for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y)
let n be Element of NAT ; ::_thesis: for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y)
let X, Y be Subset of (TOP-REAL n); ::_thesis: ( t <> 0 implies t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y) )
assume A1: t <> 0 ; ::_thesis: t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y)
t (.) (X (O) Y) = (t (.) (X (-) Y)) (+) (t (.) Y) by Th63
.= ((t (.) X) (-) (t (.) Y)) (+) (t (.) Y) by A1, Th64 ;
hence t (.) (X (O) Y) = (t (.) X) (O) (t (.) Y) ; ::_thesis: verum
end;
theorem :: MATHMORP:66
for t being real number
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)
proof
let t be real number ; ::_thesis: for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)
let n be Element of NAT ; ::_thesis: for X, Y being Subset of (TOP-REAL n) st t <> 0 holds
t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)
let X, Y be Subset of (TOP-REAL n); ::_thesis: ( t <> 0 implies t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y) )
assume t <> 0 ; ::_thesis: t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y)
then t (.) (X (o) Y) = (t (.) (X (+) Y)) (-) (t (.) Y) by Th64
.= ((t (.) X) (+) (t (.) Y)) (-) (t (.) Y) by Th63 ;
hence t (.) (X (o) Y) = (t (.) X) (o) (t (.) Y) ; ::_thesis: verum
end;
begin
definition
let T be non empty RLSStruct ;
let X, B1, B2 be Subset of T;
funcX (*) (B1,B2) -> Subset of T equals :: MATHMORP:def 7
(X (-) B1) /\ ((X `) (-) B2);
coherence
(X (-) B1) /\ ((X `) (-) B2) is Subset of T ;
end;
:: deftheorem defines (*) MATHMORP:def_7_:_
for T being non empty RLSStruct
for X, B1, B2 being Subset of T holds X (*) (B1,B2) = (X (-) B1) /\ ((X `) (-) B2);
definition
let T be non empty RLSStruct ;
let X, B1, B2 be Subset of T;
funcX (&) (B1,B2) -> Subset of T equals :: MATHMORP:def 8
X \/ (X (*) (B1,B2));
coherence
X \/ (X (*) (B1,B2)) is Subset of T ;
end;
:: deftheorem defines (&) MATHMORP:def_8_:_
for T being non empty RLSStruct
for X, B1, B2 being Subset of T holds X (&) (B1,B2) = X \/ (X (*) (B1,B2));
definition
let T be non empty RLSStruct ;
let X, B1, B2 be Subset of T;
funcX (@) (B1,B2) -> Subset of T equals :: MATHMORP:def 9
X \ (X (*) (B1,B2));
coherence
X \ (X (*) (B1,B2)) is Subset of T ;
end;
:: deftheorem defines (@) MATHMORP:def_9_:_
for T being non empty RLSStruct
for X, B1, B2 being Subset of T holds X (@) (B1,B2) = X \ (X (*) (B1,B2));
theorem :: MATHMORP:67
for n being Element of NAT
for B1, X, B2 being Subset of (TOP-REAL n) st B1 = {} holds
X (*) (B1,B2) = (X `) (-) B2
proof
let n be Element of NAT ; ::_thesis: for B1, X, B2 being Subset of (TOP-REAL n) st B1 = {} holds
X (*) (B1,B2) = (X `) (-) B2
let B1, X, B2 be Subset of (TOP-REAL n); ::_thesis: ( B1 = {} implies X (*) (B1,B2) = (X `) (-) B2 )
assume B1 = {} ; ::_thesis: X (*) (B1,B2) = (X `) (-) B2
then X (*) (B1,B2) = ((X `) (-) B2) /\ the carrier of (TOP-REAL n) by Th8;
hence X (*) (B1,B2) = (X `) (-) B2 by XBOOLE_1:28; ::_thesis: verum
end;
theorem :: MATHMORP:68
for n being Element of NAT
for B2, X, B1 being Subset of (TOP-REAL n) st B2 = {} holds
X (*) (B1,B2) = X (-) B1
proof
let n be Element of NAT ; ::_thesis: for B2, X, B1 being Subset of (TOP-REAL n) st B2 = {} holds
X (*) (B1,B2) = X (-) B1
let B2, X, B1 be Subset of (TOP-REAL n); ::_thesis: ( B2 = {} implies X (*) (B1,B2) = X (-) B1 )
assume B2 = {} ; ::_thesis: X (*) (B1,B2) = X (-) B1
then X (*) (B1,B2) = (X (-) B1) /\ the carrier of (TOP-REAL n) by Th8;
hence X (*) (B1,B2) = X (-) B1 by XBOOLE_1:28; ::_thesis: verum
end;
theorem :: MATHMORP:69
for n being Element of NAT
for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds
X (*) (B1,B2) c= X
proof
let n be Element of NAT ; ::_thesis: for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds
X (*) (B1,B2) c= X
let B1, X, B2 be Subset of (TOP-REAL n); ::_thesis: ( 0. (TOP-REAL n) in B1 implies X (*) (B1,B2) c= X )
assume A1: 0. (TOP-REAL n) in B1 ; ::_thesis: X (*) (B1,B2) c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (*) (B1,B2) or x in X )
assume x in X (*) (B1,B2) ; ::_thesis: x in X
then x in X (-) B1 by XBOOLE_0:def_4;
then consider y being Point of (TOP-REAL n) such that
A2: x = y and
A3: B1 + y c= X ;
(0. (TOP-REAL n)) + y in { (z + y) where z is Point of (TOP-REAL n) : z in B1 } by A1;
then x in B1 + y by A2, RLVECT_1:4;
hence x in X by A3; ::_thesis: verum
end;
theorem :: MATHMORP:70
for n being Element of NAT
for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds
(X (*) (B1,B2)) /\ X = {}
proof
let n be Element of NAT ; ::_thesis: for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds
(X (*) (B1,B2)) /\ X = {}
let B2, X, B1 be Subset of (TOP-REAL n); ::_thesis: ( 0. (TOP-REAL n) in B2 implies (X (*) (B1,B2)) /\ X = {} )
assume A1: 0. (TOP-REAL n) in B2 ; ::_thesis: (X (*) (B1,B2)) /\ X = {}
now__::_thesis:_for_x_being_set_holds_not_x_in_(X_(*)_(B1,B2))_/\_X
given x being set such that A2: x in (X (*) (B1,B2)) /\ X ; ::_thesis: contradiction
A3: x in X by A2, XBOOLE_0:def_4;
x in X (*) (B1,B2) by A2, XBOOLE_0:def_4;
then x in (X `) (-) B2 by XBOOLE_0:def_4;
then consider y being Point of (TOP-REAL n) such that
A4: x = y and
A5: B2 + y c= X ` ;
(0. (TOP-REAL n)) + y in { (z + y) where z is Point of (TOP-REAL n) : z in B2 } by A1;
then x in B2 + y by A4, RLVECT_1:4;
hence contradiction by A3, A5, XBOOLE_0:def_5; ::_thesis: verum
end;
hence (X (*) (B1,B2)) /\ X = {} by XBOOLE_0:def_1; ::_thesis: verum
end;
theorem :: MATHMORP:71
for n being Element of NAT
for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds
X (&) (B1,B2) = X
proof
let n be Element of NAT ; ::_thesis: for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds
X (&) (B1,B2) = X
let B1, X, B2 be Subset of (TOP-REAL n); ::_thesis: ( 0. (TOP-REAL n) in B1 implies X (&) (B1,B2) = X )
assume A1: 0. (TOP-REAL n) in B1 ; ::_thesis: X (&) (B1,B2) = X
thus X (&) (B1,B2) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X (&) (B1,B2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (&) (B1,B2) or x in X )
assume A2: x in X (&) (B1,B2) ; ::_thesis: x in X
percases ( x in X or x in X (*) (B1,B2) ) by A2, XBOOLE_0:def_3;
suppose x in X ; ::_thesis: x in X
hence x in X ; ::_thesis: verum
end;
suppose x in X (*) (B1,B2) ; ::_thesis: x in X
then x in X (-) B1 by XBOOLE_0:def_4;
then consider y being Point of (TOP-REAL n) such that
A3: x = y and
A4: B1 + y c= X ;
(0. (TOP-REAL n)) + y in { (z + y) where z is Point of (TOP-REAL n) : z in B1 } by A1;
then x in B1 + y by A3, RLVECT_1:4;
hence x in X by A4; ::_thesis: verum
end;
end;
end;
thus X c= X (&) (B1,B2) by XBOOLE_1:7; ::_thesis: verum
end;
theorem :: MATHMORP:72
for n being Element of NAT
for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds
X (@) (B1,B2) = X
proof
let n be Element of NAT ; ::_thesis: for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds
X (@) (B1,B2) = X
let B2, X, B1 be Subset of (TOP-REAL n); ::_thesis: ( 0. (TOP-REAL n) in B2 implies X (@) (B1,B2) = X )
assume A1: 0. (TOP-REAL n) in B2 ; ::_thesis: X (@) (B1,B2) = X
thus X (@) (B1,B2) c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X (@) (B1,B2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X (@) (B1,B2) or x in X )
assume x in X (@) (B1,B2) ; ::_thesis: x in X
hence x in X by XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X (@) (B1,B2) )
assume A2: x in X ; ::_thesis: x in X (@) (B1,B2)
not x in X (*) (B1,B2)
proof
assume x in X (*) (B1,B2) ; ::_thesis: contradiction
then x in (X `) (-) B2 by XBOOLE_0:def_4;
then consider y being Point of (TOP-REAL n) such that
A3: x = y and
A4: B2 + y c= X ` ;
(0. (TOP-REAL n)) + y in { (z + y) where z is Point of (TOP-REAL n) : z in B2 } by A1;
then x in B2 + y by A3, RLVECT_1:4;
hence contradiction by A2, A4, XBOOLE_0:def_5; ::_thesis: verum
end;
hence x in X (@) (B1,B2) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: MATHMORP:73
for n being Element of NAT
for X, B2, B1 being Subset of (TOP-REAL n) holds X (@) (B2,B1) = ((X `) (&) (B1,B2)) `
proof
let n be Element of NAT ; ::_thesis: for X, B2, B1 being Subset of (TOP-REAL n) holds X (@) (B2,B1) = ((X `) (&) (B1,B2)) `
let X, B2, B1 be Subset of (TOP-REAL n); ::_thesis: X (@) (B2,B1) = ((X `) (&) (B1,B2)) `
((X `) (&) (B1,B2)) ` = ((X \ (((X `) (-) B1) /\ (((X `) `) (-) B2))) `) ` by SUBSET_1:14
.= X \ (X (*) (B2,B1)) ;
hence X (@) (B2,B1) = ((X `) (&) (B1,B2)) ` ; ::_thesis: verum
end;
begin
theorem Th74: :: MATHMORP:74
for V being RealLinearSpace
for B being Subset of V holds
( B is convex iff for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B )
proof
let V be RealLinearSpace; ::_thesis: for B being Subset of V holds
( B is convex iff for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B )
let B be Subset of V; ::_thesis: ( B is convex iff for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B )
thus ( B is convex implies for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ) ::_thesis: ( ( for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ) implies B is convex )
proof
assume A1: B is convex ; ::_thesis: for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B
for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B
proof
let x, y be Point of V; ::_thesis: for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B
let r be real number ; ::_thesis: ( 0 <= r & r <= 1 & x in B & y in B implies (r * x) + ((1 - r) * y) in B )
assume that
A2: ( 0 <= r & r <= 1 ) and
A3: ( x in B & y in B ) ; ::_thesis: (r * x) + ((1 - r) * y) in B
r is Real by XREAL_0:def_1;
then ((1 - r) * y) + (r * x) in { (((1 - r1) * y) + (r1 * x)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by A2;
then A4: ((1 - r) * y) + (r * x) in LSeg (x,y) by RLTOPSP1:def_2;
LSeg (x,y) c= B by A1, A3, JORDAN1:def_1;
hence (r * x) + ((1 - r) * y) in B by A4; ::_thesis: verum
end;
hence for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ; ::_thesis: verum
end;
( ( for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ) implies B is convex )
proof
assume A5: for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ; ::_thesis: B is convex
for x, y being Point of V st x in B & y in B holds
LSeg (x,y) c= B
proof
let x, y be Point of V; ::_thesis: ( x in B & y in B implies LSeg (x,y) c= B )
assume A6: ( x in B & y in B ) ; ::_thesis: LSeg (x,y) c= B
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in LSeg (x,y) or p in B )
assume p in LSeg (x,y) ; ::_thesis: p in B
then p in { (((1 - r1) * y) + (r1 * x)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RLTOPSP1:def_2;
then ex r1 being Real st
( p = ((1 - r1) * y) + (r1 * x) & 0 <= r1 & r1 <= 1 ) ;
hence p in B by A5, A6; ::_thesis: verum
end;
hence B is convex by RLTOPSP1:22; ::_thesis: verum
end;
hence ( ( for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ) implies B is convex ) ; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
let B be Subset of V;
redefine attr B is convex means :Def10: :: MATHMORP:def 10
for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B;
compatibility
( B is convex iff for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B ) by Th74;
end;
:: deftheorem Def10 defines convex MATHMORP:def_10_:_
for V being RealLinearSpace
for B being Subset of V holds
( B is convex iff for x, y being Point of V
for r being real number st 0 <= r & r <= 1 & x in B & y in B holds
(r * x) + ((1 - r) * y) in B );
theorem :: MATHMORP:75
for n being Element of NAT
for X being Subset of (TOP-REAL n) st X is convex holds
X ! is convex
proof
let n be Element of NAT ; ::_thesis: for X being Subset of (TOP-REAL n) st X is convex holds
X ! is convex
let X be Subset of (TOP-REAL n); ::_thesis: ( X is convex implies X ! is convex )
assume A1: X is convex ; ::_thesis: X ! is convex
for x, y being Point of (TOP-REAL n)
for r being real number st 0 <= r & r <= 1 & x in X ! & y in X ! holds
(r * x) + ((1 - r) * y) in X !
proof
let x, y be Point of (TOP-REAL n); ::_thesis: for r being real number st 0 <= r & r <= 1 & x in X ! & y in X ! holds
(r * x) + ((1 - r) * y) in X !
let r be real number ; ::_thesis: ( 0 <= r & r <= 1 & x in X ! & y in X ! implies (r * x) + ((1 - r) * y) in X ! )
assume that
A2: ( 0 <= r & r <= 1 ) and
A3: x in X ! and
A4: y in X ! ; ::_thesis: (r * x) + ((1 - r) * y) in X !
consider x2 being Point of (TOP-REAL n) such that
A5: y = - x2 and
A6: x2 in X by A4;
consider x1 being Point of (TOP-REAL n) such that
A7: x = - x1 and
A8: x1 in X by A3;
(r * x1) + ((1 - r) * x2) in X by A1, A2, A8, A6, Def10;
then - ((r * x1) + ((1 - r) * x2)) in X ! ;
then (- (r * x1)) - ((1 - r) * x2) in X ! by EUCLID:38;
then (r * (- x1)) + (- ((1 - r) * x2)) in X ! by EUCLID:40;
hence (r * x) + ((1 - r) * y) in X ! by A7, A5, EUCLID:40; ::_thesis: verum
end;
hence X ! is convex by Def10; ::_thesis: verum
end;
theorem Th76: :: MATHMORP:76
for n being Element of NAT
for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds
( X (+) B is convex & X (-) B is convex )
proof
let n be Element of NAT ; ::_thesis: for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds
( X (+) B is convex & X (-) B is convex )
let X, B be Subset of (TOP-REAL n); ::_thesis: ( X is convex & B is convex implies ( X (+) B is convex & X (-) B is convex ) )
assume that
A1: X is convex and
A2: B is convex ; ::_thesis: ( X (+) B is convex & X (-) B is convex )
for x, y being Point of (TOP-REAL n)
for r being real number st 0 <= r & r <= 1 & x in X (+) B & y in X (+) B holds
(r * x) + ((1 - r) * y) in X (+) B
proof
let x, y be Point of (TOP-REAL n); ::_thesis: for r being real number st 0 <= r & r <= 1 & x in X (+) B & y in X (+) B holds
(r * x) + ((1 - r) * y) in X (+) B
let r be real number ; ::_thesis: ( 0 <= r & r <= 1 & x in X (+) B & y in X (+) B implies (r * x) + ((1 - r) * y) in X (+) B )
assume that
A3: ( 0 <= r & r <= 1 ) and
A4: x in X (+) B and
A5: y in X (+) B ; ::_thesis: (r * x) + ((1 - r) * y) in X (+) B
consider x2, b2 being Point of (TOP-REAL n) such that
A6: y = x2 + b2 and
A7: ( x2 in X & b2 in B ) by A5;
consider x1, b1 being Point of (TOP-REAL n) such that
A8: x = x1 + b1 and
A9: ( x1 in X & b1 in B ) by A4;
( (r * x1) + ((1 - r) * x2) in X & (r * b1) + ((1 - r) * b2) in B ) by A1, A2, A3, A9, A7, Def10;
then ((r * x1) + ((1 - r) * x2)) + ((r * b1) + ((1 - r) * b2)) in { (x3 + b3) where x3, b3 is Point of (TOP-REAL n) : ( x3 in X & b3 in B ) } ;
then (((r * x1) + ((1 - r) * x2)) + (r * b1)) + ((1 - r) * b2) in X (+) B by EUCLID:26;
then (((r * x1) + (r * b1)) + ((1 - r) * x2)) + ((1 - r) * b2) in X (+) B by EUCLID:26;
then ((r * x1) + (r * b1)) + (((1 - r) * x2) + ((1 - r) * b2)) in X (+) B by EUCLID:26;
then (r * (x1 + b1)) + (((1 - r) * x2) + ((1 - r) * b2)) in X (+) B by EUCLID:32;
hence (r * x) + ((1 - r) * y) in X (+) B by A8, A6, EUCLID:32; ::_thesis: verum
end;
hence X (+) B is convex by Def10; ::_thesis: X (-) B is convex
for x, y being Point of (TOP-REAL n)
for r being real number st 0 <= r & r <= 1 & x in X (-) B & y in X (-) B holds
(r * x) + ((1 - r) * y) in X (-) B
proof
let x, y be Point of (TOP-REAL n); ::_thesis: for r being real number st 0 <= r & r <= 1 & x in X (-) B & y in X (-) B holds
(r * x) + ((1 - r) * y) in X (-) B
let r be real number ; ::_thesis: ( 0 <= r & r <= 1 & x in X (-) B & y in X (-) B implies (r * x) + ((1 - r) * y) in X (-) B )
assume that
A10: ( 0 <= r & r <= 1 ) and
A11: ( x in X (-) B & y in X (-) B ) ; ::_thesis: (r * x) + ((1 - r) * y) in X (-) B
A12: ( ex x1 being Point of (TOP-REAL n) st
( x = x1 & B + x1 c= X ) & ex y1 being Point of (TOP-REAL n) st
( y = y1 & B + y1 c= X ) ) by A11;
B + ((r * x) + ((1 - r) * y)) c= X
proof
let b1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not b1 in B + ((r * x) + ((1 - r) * y)) or b1 in X )
assume b1 in B + ((r * x) + ((1 - r) * y)) ; ::_thesis: b1 in X
then consider b being Point of (TOP-REAL n) such that
A13: b1 = b + ((r * x) + ((1 - r) * y)) and
A14: b in B ;
( b + x in B + x & b + y in { (b2 + y) where b2 is Point of (TOP-REAL n) : b2 in B } ) by A14;
then (r * (b + x)) + ((1 - r) * (b + y)) in X by A1, A10, A12, Def10;
then ((r * b) + (r * x)) + ((1 - r) * (b + y)) in X by EUCLID:32;
then ((r * b) + (r * x)) + (((1 - r) * b) + ((1 - r) * y)) in X by EUCLID:32;
then (((r * b) + (r * x)) + ((1 - r) * b)) + ((1 - r) * y) in X by EUCLID:26;
then (((r * b) + (r * x)) + ((1 * b) - (r * b))) + ((1 - r) * y) in X by EUCLID:50;
then ((((r * b) + (r * x)) + (1 * b)) - (r * b)) + ((1 - r) * y) in X by EUCLID:45;
then ((((r * x) + (1 * b)) + (r * b)) - (r * b)) + ((1 - r) * y) in X by EUCLID:26;
then ((r * x) + (1 * b)) + ((1 - r) * y) in X by EUCLID:48;
then (1 * b) + ((r * x) + ((1 - r) * y)) in X by EUCLID:26;
hence b1 in X by A13, EUCLID:29; ::_thesis: verum
end;
hence (r * x) + ((1 - r) * y) in X (-) B ; ::_thesis: verum
end;
hence X (-) B is convex by Def10; ::_thesis: verum
end;
theorem :: MATHMORP:77
for n being Element of NAT
for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds
( X (O) B is convex & X (o) B is convex )
proof
let n be Element of NAT ; ::_thesis: for X, B being Subset of (TOP-REAL n) st X is convex & B is convex holds
( X (O) B is convex & X (o) B is convex )
let X, B be Subset of (TOP-REAL n); ::_thesis: ( X is convex & B is convex implies ( X (O) B is convex & X (o) B is convex ) )
assume that
A1: X is convex and
A2: B is convex ; ::_thesis: ( X (O) B is convex & X (o) B is convex )
X (-) B is convex by A1, A2, Th76;
hence X (O) B is convex by A2, Th76; ::_thesis: X (o) B is convex
X (+) B is convex by A1, A2, Th76;
hence X (o) B is convex by A2, Th76; ::_thesis: verum
end;
theorem :: MATHMORP:78
for t, s being real number
for n being Element of NAT
for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds
(s + t) (.) B = (s (.) B) (+) (t (.) B)
proof
let t, s be real number ; ::_thesis: for n being Element of NAT
for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds
(s + t) (.) B = (s (.) B) (+) (t (.) B)
let n be Element of NAT ; ::_thesis: for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds
(s + t) (.) B = (s (.) B) (+) (t (.) B)
let B be Subset of (TOP-REAL n); ::_thesis: ( B is convex & 0 < t & 0 < s implies (s + t) (.) B = (s (.) B) (+) (t (.) B) )
assume that
A1: B is convex and
A2: ( 0 < t & 0 < s ) ; ::_thesis: (s + t) (.) B = (s (.) B) (+) (t (.) B)
thus (s + t) (.) B c= (s (.) B) (+) (t (.) B) :: according to XBOOLE_0:def_10 ::_thesis: (s (.) B) (+) (t (.) B) c= (s + t) (.) B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (s + t) (.) B or x in (s (.) B) (+) (t (.) B) )
assume x in (s + t) (.) B ; ::_thesis: x in (s (.) B) (+) (t (.) B)
then consider b being Point of (TOP-REAL n) such that
A3: x = (s + t) * b and
A4: b in B ;
A5: t * b in t (.) B by A4;
( x = (s * b) + (t * b) & s * b in s (.) B ) by A3, A4, EUCLID:33;
hence x in (s (.) B) (+) (t (.) B) by A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (s (.) B) (+) (t (.) B) or x in (s + t) (.) B )
assume x in (s (.) B) (+) (t (.) B) ; ::_thesis: x in (s + t) (.) B
then consider s1, s2 being Point of (TOP-REAL n) such that
A6: x = s1 + s2 and
A7: s1 in s (.) B and
A8: s2 in t (.) B ;
consider b2 being Point of (TOP-REAL n) such that
A9: s2 = t * b2 and
A10: b2 in B by A8;
consider b1 being Point of (TOP-REAL n) such that
A11: s1 = s * b1 and
A12: b1 in B by A7;
s / (s + t) < (s + t) / (s + t) by A2, XREAL_1:29, XREAL_1:74;
then s / (s + t) < 1 by A2, XCMPLX_1:60;
then ((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2) in B by A1, A2, A12, A10, Def10;
then (s + t) * (((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2)) in { ((s + t) * zz) where zz is Point of (TOP-REAL n) : zz in B } ;
then ((s + t) * ((s / (s + t)) * b1)) + ((s + t) * ((1 - (s / (s + t))) * b2)) in (s + t) (.) B by EUCLID:32;
then (((s + t) * (s / (s + t))) * b1) + ((s + t) * ((1 - (s / (s + t))) * b2)) in (s + t) (.) B by EUCLID:30;
then (((s + t) * (s / (s + t))) * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) in (s + t) (.) B by EUCLID:30;
then (s * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) in (s + t) (.) B by A2, XCMPLX_1:87;
then (s * b1) + (((s + t) * (((s + t) / (s + t)) - (s / (s + t)))) * b2) in (s + t) (.) B by A2, XCMPLX_1:60;
then (s * b1) + (((s + t) * (((s + t) - s) / (s + t))) * b2) in (s + t) (.) B by XCMPLX_1:120;
hence x in (s + t) (.) B by A2, A6, A11, A9, XCMPLX_1:87; ::_thesis: verum
end;