:: MEMBER_1 semantic presentation
begin
definition
let w be Element of ExtREAL ;
:: original: -
redefine func - w -> Element of ExtREAL ;
coherence
- w is Element of ExtREAL by XXREAL_0:def_1;
:: original: "
redefine funcw " -> Element of ExtREAL ;
coherence
w " is Element of ExtREAL by XXREAL_0:def_1;
let w1 be Element of ExtREAL ;
:: original: *
redefine funcw * w1 -> Element of ExtREAL ;
coherence
w * w1 is Element of ExtREAL by XXREAL_0:def_1;
end;
registration
let a, b, c, d be complex number ;
cluster{a,b,c,d} -> complex-membered ;
coherence
{a,b,c,d} is complex-membered
proof
let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( not e in {a,b,c,d} or e is complex )
thus ( not e in {a,b,c,d} or e is complex ) by ENUMSET1:def_2; ::_thesis: verum
end;
end;
registration
let a, b, c, d be ext-real number ;
cluster{a,b,c,d} -> ext-real-membered ;
coherence
{a,b,c,d} is ext-real-membered
proof
let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( not e in {a,b,c,d} or e is ext-real )
thus ( not e in {a,b,c,d} or e is ext-real ) by ENUMSET1:def_2; ::_thesis: verum
end;
end;
definition
let F be ext-real-membered set ;
func -- F -> ext-real-membered set equals :: MEMBER_1:def 1
{ (- w) where w is Element of ExtREAL : w in F } ;
coherence
{ (- w) where w is Element of ExtREAL : w in F } is ext-real-membered set
proof
{ (- w) where w is Element of ExtREAL : w in F } is ext-real-membered
proof
let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( not e in { (- w) where w is Element of ExtREAL : w in F } or e is ext-real )
assume e in { (- w) where w is Element of ExtREAL : w in F } ; ::_thesis: e is ext-real
then ex w being Element of ExtREAL st
( e = - w & w in F ) ;
hence e is ext-real ; ::_thesis: verum
end;
hence { (- w) where w is Element of ExtREAL : w in F } is ext-real-membered set ; ::_thesis: verum
end;
involutiveness
for b1, b2 being ext-real-membered set st b1 = { (- w) where w is Element of ExtREAL : w in b2 } holds
b2 = { (- w) where w is Element of ExtREAL : w in b1 }
proof
let A, B be ext-real-membered set ; ::_thesis: ( A = { (- w) where w is Element of ExtREAL : w in B } implies B = { (- w) where w is Element of ExtREAL : w in A } )
assume A1: A = { (- w) where w is Element of ExtREAL : w in B } ; ::_thesis: B = { (- w) where w is Element of ExtREAL : w in A }
thus B c= { (- w) where w is Element of ExtREAL : w in A } :: according to XBOOLE_0:def_10 ::_thesis: { (- w) where w is Element of ExtREAL : w in A } c= B
proof
let z be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not z in B or z in { (- w) where w is Element of ExtREAL : w in A } )
A2: z in ExtREAL by XXREAL_0:def_1;
A3: ( - z in ExtREAL & z = - (- z) ) by XXREAL_0:def_1;
assume z in B ; ::_thesis: z in { (- w) where w is Element of ExtREAL : w in A }
then - z in A by A1, A2;
hence z in { (- w) where w is Element of ExtREAL : w in A } by A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (- w) where w is Element of ExtREAL : w in A } or e in B )
assume e in { (- w) where w is Element of ExtREAL : w in A } ; ::_thesis: e in B
then consider w1 being Element of ExtREAL such that
A4: - w1 = e and
A5: w1 in A ;
ex w being Element of ExtREAL st
( - w = w1 & w in B ) by A1, A5;
hence e in B by A4; ::_thesis: verum
end;
end;
:: deftheorem defines -- MEMBER_1:def_1_:_
for F being ext-real-membered set holds -- F = { (- w) where w is Element of ExtREAL : w in F } ;
theorem Th1: :: MEMBER_1:1
for F being ext-real-membered set
for f being ext-real number holds
( f in F iff - f in -- F )
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds
( f in F iff - f in -- F )
let f be ext-real number ; ::_thesis: ( f in F iff - f in -- F )
f in ExtREAL by XXREAL_0:def_1;
hence ( f in F implies - f in -- F ) ; ::_thesis: ( - f in -- F implies f in F )
assume - f in -- F ; ::_thesis: f in F
then A1: ex w being Element of ExtREAL st
( - w = - f & w in F ) ;
- (- f) = f ;
hence f in F by A1; ::_thesis: verum
end;
theorem Th2: :: MEMBER_1:2
for F being ext-real-membered set
for f being ext-real number holds
( - f in F iff f in -- F )
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds
( - f in F iff f in -- F )
let f be ext-real number ; ::_thesis: ( - f in F iff f in -- F )
- (- f) = f ;
hence ( - f in F iff f in -- F ) by Th1; ::_thesis: verum
end;
registration
let F be empty set ;
cluster -- F -> empty ext-real-membered ;
coherence
-- F is empty
proof
assume not -- F is empty ; ::_thesis: contradiction
then the Element of -- F in -- F ;
then ex w being Element of ExtREAL st
( the Element of -- F = - w & w in F ) ;
hence contradiction ; ::_thesis: verum
end;
end;
registration
let F be non empty ext-real-membered set ;
cluster -- F -> non empty ext-real-membered ;
coherence
not -- F is empty
proof
- the Element of F in -- F by Th1;
hence not -- F is empty ; ::_thesis: verum
end;
end;
Lm1: for F, G being ext-real-membered set st F c= G holds
-- F c= -- G
proof
let F, G be ext-real-membered set ; ::_thesis: ( F c= G implies -- F c= -- G )
assume A1: F c= G ; ::_thesis: -- F c= -- G
let j be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not j in -- F or j in -- G )
assume j in -- F ; ::_thesis: j in -- G
then - j in F by Th2;
hence j in -- G by A1, Th2; ::_thesis: verum
end;
theorem Th3: :: MEMBER_1:3
for F, G being ext-real-membered set holds
( F c= G iff -- F c= -- G )
proof
let F, G be ext-real-membered set ; ::_thesis: ( F c= G iff -- F c= -- G )
( -- (-- F) = F & -- (-- G) = G ) ;
hence ( F c= G iff -- F c= -- G ) by Lm1; ::_thesis: verum
end;
theorem :: MEMBER_1:4
for F, G being ext-real-membered set st -- F = -- G holds
F = G
proof
let F, G be ext-real-membered set ; ::_thesis: ( -- F = -- G implies F = G )
assume -- F = -- G ; ::_thesis: F = G
then ( F c= G & G c= F ) by Th3;
hence F = G by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th5: :: MEMBER_1:5
for F, G being ext-real-membered set holds -- (F \/ G) = (-- F) \/ (-- G)
proof
let F, G be ext-real-membered set ; ::_thesis: -- (F \/ G) = (-- F) \/ (-- G)
let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in -- (F \/ G) or i in (-- F) \/ (-- G) ) & ( not i in (-- F) \/ (-- G) or i in -- (F \/ G) ) )
hereby ::_thesis: ( not i in (-- F) \/ (-- G) or i in -- (F \/ G) )
assume i in -- (F \/ G) ; ::_thesis: i in (-- F) \/ (-- G)
then - i in F \/ G by Th2;
then ( - i in F or - i in G ) by XBOOLE_0:def_3;
then ( i in -- F or i in -- G ) by Th2;
hence i in (-- F) \/ (-- G) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume i in (-- F) \/ (-- G) ; ::_thesis: i in -- (F \/ G)
then ( i in -- F or i in -- G ) by XBOOLE_0:def_3;
then ( - i in F or - i in G ) by Th2;
then - i in F \/ G by XBOOLE_0:def_3;
hence i in -- (F \/ G) by Th2; ::_thesis: verum
end;
theorem Th6: :: MEMBER_1:6
for F, G being ext-real-membered set holds -- (F /\ G) = (-- F) /\ (-- G)
proof
let F, G be ext-real-membered set ; ::_thesis: -- (F /\ G) = (-- F) /\ (-- G)
let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in -- (F /\ G) or i in (-- F) /\ (-- G) ) & ( not i in (-- F) /\ (-- G) or i in -- (F /\ G) ) )
hereby ::_thesis: ( not i in (-- F) /\ (-- G) or i in -- (F /\ G) )
assume i in -- (F /\ G) ; ::_thesis: i in (-- F) /\ (-- G)
then A1: - i in F /\ G by Th2;
then - i in G by XBOOLE_0:def_4;
then A2: i in -- G by Th2;
- i in F by A1, XBOOLE_0:def_4;
then i in -- F by Th2;
hence i in (-- F) /\ (-- G) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A3: i in (-- F) /\ (-- G) ; ::_thesis: i in -- (F /\ G)
then i in -- G by XBOOLE_0:def_4;
then A4: - i in G by Th2;
i in -- F by A3, XBOOLE_0:def_4;
then - i in F by Th2;
then - i in F /\ G by A4, XBOOLE_0:def_4;
hence i in -- (F /\ G) by Th2; ::_thesis: verum
end;
theorem Th7: :: MEMBER_1:7
for F, G being ext-real-membered set holds -- (F \ G) = (-- F) \ (-- G)
proof
let F, G be ext-real-membered set ; ::_thesis: -- (F \ G) = (-- F) \ (-- G)
let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in -- (F \ G) or i in (-- F) \ (-- G) ) & ( not i in (-- F) \ (-- G) or i in -- (F \ G) ) )
hereby ::_thesis: ( not i in (-- F) \ (-- G) or i in -- (F \ G) )
assume i in -- (F \ G) ; ::_thesis: i in (-- F) \ (-- G)
then A1: - i in F \ G by Th2;
then not - i in G by XBOOLE_0:def_5;
then A2: not i in -- G by Th2;
i in -- F by A1, Th2;
hence i in (-- F) \ (-- G) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A3: i in (-- F) \ (-- G) ; ::_thesis: i in -- (F \ G)
then not i in -- G by XBOOLE_0:def_5;
then A4: not - i in G by Th2;
- i in F by A3, Th2;
then - i in F \ G by A4, XBOOLE_0:def_5;
hence i in -- (F \ G) by Th2; ::_thesis: verum
end;
theorem Th8: :: MEMBER_1:8
for F, G being ext-real-membered set holds -- (F \+\ G) = (-- F) \+\ (-- G)
proof
let F, G be ext-real-membered set ; ::_thesis: -- (F \+\ G) = (-- F) \+\ (-- G)
thus -- (F \+\ G) = (-- (F \ G)) \/ (-- (G \ F)) by Th5
.= ((-- F) \ (-- G)) \/ (-- (G \ F)) by Th7
.= (-- F) \+\ (-- G) by Th7 ; ::_thesis: verum
end;
theorem Th9: :: MEMBER_1:9
for f being ext-real number holds -- {f} = {(- f)}
proof
let f be ext-real number ; ::_thesis: -- {f} = {(- f)}
let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in -- {f} or i in {(- f)} ) & ( not i in {(- f)} or i in -- {f} ) )
hereby ::_thesis: ( not i in {(- f)} or i in -- {f} )
assume i in -- {f} ; ::_thesis: i in {(- f)}
then consider w being Element of ExtREAL such that
A1: i = - w and
A2: w in {f} ;
w = f by A2, TARSKI:def_1;
hence i in {(- f)} by A1, TARSKI:def_1; ::_thesis: verum
end;
assume i in {(- f)} ; ::_thesis: i in -- {f}
then A3: i = - f by TARSKI:def_1;
( f in ExtREAL & f in {f} ) by TARSKI:def_1, XXREAL_0:def_1;
hence i in -- {f} by A3; ::_thesis: verum
end;
theorem Th10: :: MEMBER_1:10
for f, g being ext-real number holds -- {f,g} = {(- f),(- g)}
proof
let f, g be ext-real number ; ::_thesis: -- {f,g} = {(- f),(- g)}
thus -- {f,g} = -- ({f} \/ {g}) by ENUMSET1:1
.= (-- {f}) \/ (-- {g}) by Th5
.= {(- f)} \/ (-- {g}) by Th9
.= {(- f)} \/ {(- g)} by Th9
.= {(- f),(- g)} by ENUMSET1:1 ; ::_thesis: verum
end;
definition
let A be complex-membered set ;
func -- A -> complex-membered set equals :: MEMBER_1:def 2
{ (- c) where c is Element of COMPLEX : c in A } ;
coherence
{ (- c) where c is Element of COMPLEX : c in A } is complex-membered set
proof
{ (- c) where c is Element of COMPLEX : c in A } is complex-membered
proof
let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( not e in { (- c) where c is Element of COMPLEX : c in A } or e is complex )
assume e in { (- c) where c is Element of COMPLEX : c in A } ; ::_thesis: e is complex
then ex c being Element of COMPLEX st
( e = - c & c in A ) ;
hence e is complex ; ::_thesis: verum
end;
hence { (- c) where c is Element of COMPLEX : c in A } is complex-membered set ; ::_thesis: verum
end;
involutiveness
for b1, b2 being complex-membered set st b1 = { (- c) where c is Element of COMPLEX : c in b2 } holds
b2 = { (- c) where c is Element of COMPLEX : c in b1 }
proof
let A, B be complex-membered set ; ::_thesis: ( A = { (- c) where c is Element of COMPLEX : c in B } implies B = { (- c) where c is Element of COMPLEX : c in A } )
assume A1: A = { (- c) where c is Element of COMPLEX : c in B } ; ::_thesis: B = { (- c) where c is Element of COMPLEX : c in A }
thus B c= { (- c) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (- c) where c is Element of COMPLEX : c in A } c= B
proof
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in B or z in { (- c) where c is Element of COMPLEX : c in A } )
A2: z in COMPLEX by XCMPLX_0:def_2;
A3: ( - z in COMPLEX & z = - (- z) ) by XCMPLX_0:def_2;
assume z in B ; ::_thesis: z in { (- c) where c is Element of COMPLEX : c in A }
then - z in A by A1, A2;
hence z in { (- c) where c is Element of COMPLEX : c in A } by A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (- c) where c is Element of COMPLEX : c in A } or e in B )
assume e in { (- c) where c is Element of COMPLEX : c in A } ; ::_thesis: e in B
then consider r0 being Element of COMPLEX such that
A4: - r0 = e and
A5: r0 in A ;
ex c being Element of COMPLEX st
( - c = r0 & c in B ) by A1, A5;
hence e in B by A4; ::_thesis: verum
end;
end;
:: deftheorem defines -- MEMBER_1:def_2_:_
for A being complex-membered set holds -- A = { (- c) where c is Element of COMPLEX : c in A } ;
theorem Th11: :: MEMBER_1:11
for A being complex-membered set
for a being complex number holds
( a in A iff - a in -- A )
proof
let A be complex-membered set ; ::_thesis: for a being complex number holds
( a in A iff - a in -- A )
let a be complex number ; ::_thesis: ( a in A iff - a in -- A )
a in COMPLEX by XCMPLX_0:def_2;
hence ( a in A implies - a in -- A ) ; ::_thesis: ( - a in -- A implies a in A )
assume - a in -- A ; ::_thesis: a in A
then ex c being Element of COMPLEX st
( - c = - a & c in A ) ;
hence a in A ; ::_thesis: verum
end;
theorem Th12: :: MEMBER_1:12
for A being complex-membered set
for a being complex number holds
( - a in A iff a in -- A )
proof
let A be complex-membered set ; ::_thesis: for a being complex number holds
( - a in A iff a in -- A )
let a be complex number ; ::_thesis: ( - a in A iff a in -- A )
- (- a) = a ;
hence ( - a in A iff a in -- A ) by Th11; ::_thesis: verum
end;
registration
let A be empty set ;
cluster -- A -> empty complex-membered ;
coherence
-- A is empty
proof
assume not -- A is empty ; ::_thesis: contradiction
then the Element of -- A in -- A ;
then ex c being Element of COMPLEX st
( the Element of -- A = - c & c in A ) ;
hence contradiction ; ::_thesis: verum
end;
end;
registration
let A be non empty complex-membered set ;
cluster -- A -> non empty complex-membered ;
coherence
not -- A is empty
proof
- the Element of A in -- A by Th11;
hence not -- A is empty ; ::_thesis: verum
end;
end;
registration
let A be real-membered set ;
cluster -- A -> complex-membered real-membered ;
coherence
-- A is real-membered
proof
let e be set ; :: according to MEMBERED:def_3 ::_thesis: ( not e in -- A or e is real )
assume e in -- A ; ::_thesis: e is real
then ex c being Element of COMPLEX st
( e = - c & c in A ) ;
hence e is real ; ::_thesis: verum
end;
end;
registration
let A be rational-membered set ;
cluster -- A -> complex-membered rational-membered ;
coherence
-- A is rational-membered
proof
let e be set ; :: according to MEMBERED:def_4 ::_thesis: ( not e in -- A or e is rational )
assume e in -- A ; ::_thesis: e is rational
then ex c being Element of COMPLEX st
( e = - c & c in A ) ;
hence e is rational ; ::_thesis: verum
end;
end;
registration
let A be integer-membered set ;
cluster -- A -> complex-membered integer-membered ;
coherence
-- A is integer-membered
proof
let e be set ; :: according to MEMBERED:def_5 ::_thesis: ( not e in -- A or e is integer )
assume e in -- A ; ::_thesis: e is integer
then ex c being Element of COMPLEX st
( e = - c & c in A ) ;
hence e is integer ; ::_thesis: verum
end;
end;
registration
let A be real-membered set ;
let F be ext-real-membered set ;
identify -- A with -- F when A = F;
compatibility
( A = F implies -- A = -- F )
proof
assume A1: A = F ; ::_thesis: -- A = -- F
let a be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not a in -- A or a in -- F ) & ( not a in -- F or a in -- A ) )
hereby ::_thesis: ( not a in -- F or a in -- A )
assume A2: a in -- A ; ::_thesis: a in -- F
then reconsider b = a as real number ;
- b in A by A2, Th12;
hence a in -- F by A1, Th2; ::_thesis: verum
end;
assume a in -- F ; ::_thesis: a in -- A
then consider w being Element of ExtREAL such that
A3: a = - w and
A4: w in F ;
reconsider b = w as real number by A1, A4;
- b in COMPLEX by XCMPLX_0:def_2;
then - a in COMPLEX by A3, XCMPLX_0:def_2;
then - b in -- A by A1, A3, A4;
hence a in -- A by A3; ::_thesis: verum
end;
end;
Lm2: for A, B being complex-membered set st A c= B holds
-- A c= -- B
proof
let A, B be complex-membered set ; ::_thesis: ( A c= B implies -- A c= -- B )
assume A1: A c= B ; ::_thesis: -- A c= -- B
let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in -- A or a in -- B )
assume a in -- A ; ::_thesis: a in -- B
then - a in A by Th12;
hence a in -- B by A1, Th12; ::_thesis: verum
end;
theorem Th13: :: MEMBER_1:13
for A, B being complex-membered set holds
( A c= B iff -- A c= -- B )
proof
let A, B be complex-membered set ; ::_thesis: ( A c= B iff -- A c= -- B )
( -- (-- A) = A & -- (-- B) = B ) ;
hence ( A c= B iff -- A c= -- B ) by Lm2; ::_thesis: verum
end;
theorem :: MEMBER_1:14
for A, B being complex-membered set st -- A = -- B holds
A = B
proof
let A, B be complex-membered set ; ::_thesis: ( -- A = -- B implies A = B )
assume -- A = -- B ; ::_thesis: A = B
then ( A c= B & B c= A ) by Th13;
hence A = B by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th15: :: MEMBER_1:15
for A, B being complex-membered set holds -- (A \/ B) = (-- A) \/ (-- B)
proof
let A, B be complex-membered set ; ::_thesis: -- (A \/ B) = (-- A) \/ (-- B)
let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in -- (A \/ B) or z in (-- A) \/ (-- B) ) & ( not z in (-- A) \/ (-- B) or z in -- (A \/ B) ) )
hereby ::_thesis: ( not z in (-- A) \/ (-- B) or z in -- (A \/ B) )
assume z in -- (A \/ B) ; ::_thesis: z in (-- A) \/ (-- B)
then - z in A \/ B by Th12;
then ( - z in A or - z in B ) by XBOOLE_0:def_3;
then ( z in -- A or z in -- B ) by Th12;
hence z in (-- A) \/ (-- B) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume z in (-- A) \/ (-- B) ; ::_thesis: z in -- (A \/ B)
then ( z in -- A or z in -- B ) by XBOOLE_0:def_3;
then ( - z in A or - z in B ) by Th12;
then - z in A \/ B by XBOOLE_0:def_3;
hence z in -- (A \/ B) by Th12; ::_thesis: verum
end;
theorem Th16: :: MEMBER_1:16
for A, B being complex-membered set holds -- (A /\ B) = (-- A) /\ (-- B)
proof
let A, B be complex-membered set ; ::_thesis: -- (A /\ B) = (-- A) /\ (-- B)
let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in -- (A /\ B) or z in (-- A) /\ (-- B) ) & ( not z in (-- A) /\ (-- B) or z in -- (A /\ B) ) )
hereby ::_thesis: ( not z in (-- A) /\ (-- B) or z in -- (A /\ B) )
assume z in -- (A /\ B) ; ::_thesis: z in (-- A) /\ (-- B)
then A1: - z in A /\ B by Th12;
then - z in B by XBOOLE_0:def_4;
then A2: z in -- B by Th12;
- z in A by A1, XBOOLE_0:def_4;
then z in -- A by Th12;
hence z in (-- A) /\ (-- B) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A3: z in (-- A) /\ (-- B) ; ::_thesis: z in -- (A /\ B)
then z in -- B by XBOOLE_0:def_4;
then A4: - z in B by Th12;
z in -- A by A3, XBOOLE_0:def_4;
then - z in A by Th12;
then - z in A /\ B by A4, XBOOLE_0:def_4;
hence z in -- (A /\ B) by Th12; ::_thesis: verum
end;
theorem Th17: :: MEMBER_1:17
for A, B being complex-membered set holds -- (A \ B) = (-- A) \ (-- B)
proof
let A, B be complex-membered set ; ::_thesis: -- (A \ B) = (-- A) \ (-- B)
let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in -- (A \ B) or z in (-- A) \ (-- B) ) & ( not z in (-- A) \ (-- B) or z in -- (A \ B) ) )
hereby ::_thesis: ( not z in (-- A) \ (-- B) or z in -- (A \ B) )
assume z in -- (A \ B) ; ::_thesis: z in (-- A) \ (-- B)
then A1: - z in A \ B by Th12;
then not - z in B by XBOOLE_0:def_5;
then A2: not z in -- B by Th12;
z in -- A by A1, Th12;
hence z in (-- A) \ (-- B) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A3: z in (-- A) \ (-- B) ; ::_thesis: z in -- (A \ B)
then not z in -- B by XBOOLE_0:def_5;
then A4: not - z in B by Th12;
- z in A by A3, Th12;
then - z in A \ B by A4, XBOOLE_0:def_5;
hence z in -- (A \ B) by Th12; ::_thesis: verum
end;
theorem Th18: :: MEMBER_1:18
for A, B being complex-membered set holds -- (A \+\ B) = (-- A) \+\ (-- B)
proof
let A, B be complex-membered set ; ::_thesis: -- (A \+\ B) = (-- A) \+\ (-- B)
thus -- (A \+\ B) = (-- (A \ B)) \/ (-- (B \ A)) by Th15
.= ((-- A) \ (-- B)) \/ (-- (B \ A)) by Th17
.= (-- A) \+\ (-- B) by Th17 ; ::_thesis: verum
end;
theorem Th19: :: MEMBER_1:19
for a being complex number holds -- {a} = {(- a)}
proof
let a be complex number ; ::_thesis: -- {a} = {(- a)}
let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in -- {a} or z in {(- a)} ) & ( not z in {(- a)} or z in -- {a} ) )
hereby ::_thesis: ( not z in {(- a)} or z in -- {a} )
assume z in -- {a} ; ::_thesis: z in {(- a)}
then consider c being Element of COMPLEX such that
A1: z = - c and
A2: c in {a} ;
c = a by A2, TARSKI:def_1;
hence z in {(- a)} by A1, TARSKI:def_1; ::_thesis: verum
end;
assume z in {(- a)} ; ::_thesis: z in -- {a}
then A3: z = - a by TARSKI:def_1;
( a in COMPLEX & a in {a} ) by TARSKI:def_1, XCMPLX_0:def_2;
hence z in -- {a} by A3; ::_thesis: verum
end;
theorem Th20: :: MEMBER_1:20
for a, b being complex number holds -- {a,b} = {(- a),(- b)}
proof
let a, b be complex number ; ::_thesis: -- {a,b} = {(- a),(- b)}
thus -- {a,b} = -- ({a} \/ {b}) by ENUMSET1:1
.= (-- {a}) \/ (-- {b}) by Th15
.= {(- a)} \/ (-- {b}) by Th19
.= {(- a)} \/ {(- b)} by Th19
.= {(- a),(- b)} by ENUMSET1:1 ; ::_thesis: verum
end;
definition
let F be ext-real-membered set ;
funcF "" -> ext-real-membered set equals :: MEMBER_1:def 3
{ (w ") where w is Element of ExtREAL : w in F } ;
coherence
{ (w ") where w is Element of ExtREAL : w in F } is ext-real-membered set
proof
{ (w ") where w is Element of ExtREAL : w in F } is ext-real-membered
proof
let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( not e in { (w ") where w is Element of ExtREAL : w in F } or e is ext-real )
assume e in { (w ") where w is Element of ExtREAL : w in F } ; ::_thesis: e is ext-real
then ex w being Element of ExtREAL st
( e = w " & w in F ) ;
hence e is ext-real ; ::_thesis: verum
end;
hence { (w ") where w is Element of ExtREAL : w in F } is ext-real-membered set ; ::_thesis: verum
end;
end;
:: deftheorem defines "" MEMBER_1:def_3_:_
for F being ext-real-membered set holds F "" = { (w ") where w is Element of ExtREAL : w in F } ;
theorem Th21: :: MEMBER_1:21
for F being ext-real-membered set
for f being ext-real number st f in F holds
f " in F ""
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number st f in F holds
f " in F ""
let f be ext-real number ; ::_thesis: ( f in F implies f " in F "" )
f in ExtREAL by XXREAL_0:def_1;
hence ( f in F implies f " in F "" ) ; ::_thesis: verum
end;
registration
let F be empty set ;
clusterF "" -> empty ext-real-membered ;
coherence
F "" is empty
proof
assume not F "" is empty ; ::_thesis: contradiction
then the Element of F "" in F "" ;
then ex w being Element of ExtREAL st
( the Element of F "" = w " & w in F ) ;
hence contradiction ; ::_thesis: verum
end;
end;
registration
let F be non empty ext-real-membered set ;
clusterF "" -> non empty ext-real-membered ;
coherence
not F "" is empty
proof
the Element of F " in F "" by Th21;
hence not F "" is empty ; ::_thesis: verum
end;
end;
theorem :: MEMBER_1:22
for F, G being ext-real-membered set st F c= G holds
F "" c= G ""
proof
let F, G be ext-real-membered set ; ::_thesis: ( F c= G implies F "" c= G "" )
assume A1: F c= G ; ::_thesis: F "" c= G ""
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F "" or i in G "" )
assume i in F "" ; ::_thesis: i in G ""
then ex w being Element of ExtREAL st
( i = w " & w in F ) ;
hence i in G "" by A1; ::_thesis: verum
end;
theorem Th23: :: MEMBER_1:23
for F, G being ext-real-membered set holds (F \/ G) "" = (F "") \/ (G "")
proof
let F, G be ext-real-membered set ; ::_thesis: (F \/ G) "" = (F "") \/ (G "")
let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in (F \/ G) "" or i in (F "") \/ (G "") ) & ( not i in (F "") \/ (G "") or i in (F \/ G) "" ) )
hereby ::_thesis: ( not i in (F "") \/ (G "") or i in (F \/ G) "" )
assume i in (F \/ G) "" ; ::_thesis: i in (F "") \/ (G "")
then consider w being Element of ExtREAL such that
A1: i = w " and
A2: w in F \/ G ;
( w in F or w in G ) by A2, XBOOLE_0:def_3;
then ( w " in F "" or w " in G "" ) ;
hence i in (F "") \/ (G "") by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A3: i in (F "") \/ (G "") ; ::_thesis: i in (F \/ G) ""
percases ( i in F "" or i in G "" ) by A3, XBOOLE_0:def_3;
suppose i in F "" ; ::_thesis: i in (F \/ G) ""
then consider w being Element of ExtREAL such that
A4: i = w " and
A5: w in F ;
w in F \/ G by A5, XBOOLE_0:def_3;
hence i in (F \/ G) "" by A4; ::_thesis: verum
end;
suppose i in G "" ; ::_thesis: i in (F \/ G) ""
then consider w being Element of ExtREAL such that
A6: i = w " and
A7: w in G ;
w in F \/ G by A7, XBOOLE_0:def_3;
hence i in (F \/ G) "" by A6; ::_thesis: verum
end;
end;
end;
theorem Th24: :: MEMBER_1:24
for F, G being ext-real-membered set holds (F /\ G) "" c= (F "") /\ (G "")
proof
let F, G be ext-real-membered set ; ::_thesis: (F /\ G) "" c= (F "") /\ (G "")
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in (F /\ G) "" or i in (F "") /\ (G "") )
assume i in (F /\ G) "" ; ::_thesis: i in (F "") /\ (G "")
then consider w being Element of ExtREAL such that
A1: i = w " and
A2: w in F /\ G ;
w in G by A2, XBOOLE_0:def_4;
then A3: w " in G "" ;
w in F by A2, XBOOLE_0:def_4;
then w " in F "" ;
hence i in (F "") /\ (G "") by A1, A3, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: MEMBER_1:25
for F being ext-real-membered set holds -- (F "") = (-- F) ""
proof
let F be ext-real-membered set ; ::_thesis: -- (F "") = (-- F) ""
let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in -- (F "") or i in (-- F) "" ) & ( not i in (-- F) "" or i in -- (F "") ) )
hereby ::_thesis: ( not i in (-- F) "" or i in -- (F "") )
assume i in -- (F "") ; ::_thesis: i in (-- F) ""
then - i in F "" by Th2;
then consider w being Element of ExtREAL such that
A1: - i = w " and
A2: w in F ;
( (- w) " = - (w ") & - w in -- F ) by A2, XXREAL_3:99;
hence i in (-- F) "" by A1; ::_thesis: verum
end;
assume i in (-- F) "" ; ::_thesis: i in -- (F "")
then consider w being Element of ExtREAL such that
A3: i = w " and
A4: w in -- F ;
( (- w) " = - (w ") & - w in F ) by A4, Th2, XXREAL_3:99;
then - i in F "" by A3;
hence i in -- (F "") by Th2; ::_thesis: verum
end;
theorem Th26: :: MEMBER_1:26
for f being ext-real number holds {f} "" = {(f ")}
proof
let f be ext-real number ; ::_thesis: {f} "" = {(f ")}
let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in {f} "" or i in {(f ")} ) & ( not i in {(f ")} or i in {f} "" ) )
hereby ::_thesis: ( not i in {(f ")} or i in {f} "" )
assume i in {f} "" ; ::_thesis: i in {(f ")}
then consider w being Element of ExtREAL such that
A1: i = w " and
A2: w in {f} ;
w = f by A2, TARSKI:def_1;
hence i in {(f ")} by A1, TARSKI:def_1; ::_thesis: verum
end;
assume i in {(f ")} ; ::_thesis: i in {f} ""
then A3: i = f " by TARSKI:def_1;
( f in ExtREAL & f in {f} ) by TARSKI:def_1, XXREAL_0:def_1;
hence i in {f} "" by A3; ::_thesis: verum
end;
theorem Th27: :: MEMBER_1:27
for f, g being ext-real number holds {f,g} "" = {(f "),(g ")}
proof
let f, g be ext-real number ; ::_thesis: {f,g} "" = {(f "),(g ")}
thus {f,g} "" = ({f} \/ {g}) "" by ENUMSET1:1
.= ({f} "") \/ ({g} "") by Th23
.= {(f ")} \/ ({g} "") by Th26
.= {(f ")} \/ {(g ")} by Th26
.= {(f "),(g ")} by ENUMSET1:1 ; ::_thesis: verum
end;
definition
let A be complex-membered set ;
funcA "" -> complex-membered set equals :: MEMBER_1:def 4
{ (c ") where c is Element of COMPLEX : c in A } ;
coherence
{ (c ") where c is Element of COMPLEX : c in A } is complex-membered set
proof
{ (c ") where c is Element of COMPLEX : c in A } is complex-membered
proof
let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( not e in { (c ") where c is Element of COMPLEX : c in A } or e is complex )
assume e in { (c ") where c is Element of COMPLEX : c in A } ; ::_thesis: e is complex
then ex c being Element of COMPLEX st
( e = c " & c in A ) ;
hence e is complex ; ::_thesis: verum
end;
hence { (c ") where c is Element of COMPLEX : c in A } is complex-membered set ; ::_thesis: verum
end;
involutiveness
for b1, b2 being complex-membered set st b1 = { (c ") where c is Element of COMPLEX : c in b2 } holds
b2 = { (c ") where c is Element of COMPLEX : c in b1 }
proof
let A, B be complex-membered set ; ::_thesis: ( A = { (c ") where c is Element of COMPLEX : c in B } implies B = { (c ") where c is Element of COMPLEX : c in A } )
assume A1: A = { (c ") where c is Element of COMPLEX : c in B } ; ::_thesis: B = { (c ") where c is Element of COMPLEX : c in A }
thus B c= { (c ") where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (c ") where c is Element of COMPLEX : c in A } c= B
proof
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in B or z in { (c ") where c is Element of COMPLEX : c in A } )
A2: z in COMPLEX by XCMPLX_0:def_2;
A3: ( z " in COMPLEX & z = (z ") " ) by XCMPLX_0:def_2;
assume z in B ; ::_thesis: z in { (c ") where c is Element of COMPLEX : c in A }
then z " in A by A1, A2;
hence z in { (c ") where c is Element of COMPLEX : c in A } by A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c ") where c is Element of COMPLEX : c in A } or e in B )
assume e in { (c ") where c is Element of COMPLEX : c in A } ; ::_thesis: e in B
then consider r0 being Element of COMPLEX such that
A4: r0 " = e and
A5: r0 in A ;
ex c being Element of COMPLEX st
( c " = r0 & c in B ) by A1, A5;
hence e in B by A4; ::_thesis: verum
end;
end;
:: deftheorem defines "" MEMBER_1:def_4_:_
for A being complex-membered set holds A "" = { (c ") where c is Element of COMPLEX : c in A } ;
theorem Th28: :: MEMBER_1:28
for A being complex-membered set
for a being complex number holds
( a in A iff a " in A "" )
proof
let A be complex-membered set ; ::_thesis: for a being complex number holds
( a in A iff a " in A "" )
let a be complex number ; ::_thesis: ( a in A iff a " in A "" )
a in COMPLEX by XCMPLX_0:def_2;
hence ( a in A implies a " in A "" ) ; ::_thesis: ( a " in A "" implies a in A )
assume a " in A "" ; ::_thesis: a in A
then ex c being Element of COMPLEX st
( c " = a " & c in A ) ;
hence a in A by XCMPLX_1:201; ::_thesis: verum
end;
theorem Th29: :: MEMBER_1:29
for A being complex-membered set
for a being complex number holds
( a " in A iff a in A "" )
proof
let A be complex-membered set ; ::_thesis: for a being complex number holds
( a " in A iff a in A "" )
let a be complex number ; ::_thesis: ( a " in A iff a in A "" )
(a ") " = a ;
hence ( a " in A iff a in A "" ) by Th28; ::_thesis: verum
end;
registration
let A be empty set ;
clusterA "" -> empty complex-membered ;
coherence
A "" is empty
proof
assume not A "" is empty ; ::_thesis: contradiction
then the Element of A "" in A "" ;
then ex c being Element of COMPLEX st
( the Element of A "" = c " & c in A ) ;
hence contradiction ; ::_thesis: verum
end;
end;
registration
let A be non empty complex-membered set ;
clusterA "" -> non empty complex-membered ;
coherence
not A "" is empty
proof
the Element of A " in A "" by Th28;
hence not A "" is empty ; ::_thesis: verum
end;
end;
registration
let A be real-membered set ;
clusterA "" -> complex-membered real-membered ;
coherence
A "" is real-membered
proof
let e be set ; :: according to MEMBERED:def_3 ::_thesis: ( not e in A "" or e is real )
assume e in A "" ; ::_thesis: e is real
then ex c being Element of COMPLEX st
( e = c " & c in A ) ;
hence e is real ; ::_thesis: verum
end;
end;
registration
let A be rational-membered set ;
clusterA "" -> complex-membered rational-membered ;
coherence
A "" is rational-membered
proof
let e be set ; :: according to MEMBERED:def_4 ::_thesis: ( not e in A "" or e is rational )
assume e in A "" ; ::_thesis: e is rational
then ex c being Element of COMPLEX st
( e = c " & c in A ) ;
hence e is rational ; ::_thesis: verum
end;
end;
registration
let A be real-membered set ;
let F be ext-real-membered set ;
identifyA "" with F "" when A = F;
compatibility
( A = F implies A "" = F "" )
proof
assume A1: A = F ; ::_thesis: A "" = F ""
let a be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not a in A "" or a in F "" ) & ( not a in F "" or a in A "" ) )
hereby ::_thesis: ( not a in F "" or a in A "" )
assume a in A "" ; ::_thesis: a in F ""
then consider c being Element of COMPLEX such that
A2: a = c " and
A3: c in A ;
reconsider w = c as Element of ExtREAL by A3, XXREAL_0:def_1;
ex m being complex number st
( w = m & w " = m " ) by A3, XXREAL_3:def_6;
hence a in F "" by A1, A2, A3; ::_thesis: verum
end;
assume a in F "" ; ::_thesis: a in A ""
then consider w being Element of ExtREAL such that
A4: a = w " and
A5: w in F ;
reconsider c = w as Element of COMPLEX by A1, A5, XCMPLX_0:def_2;
w " = c " by A1, A5, XXREAL_3:def_6;
hence a in A "" by A1, A4, A5; ::_thesis: verum
end;
end;
Lm3: for A, B being complex-membered set st A c= B holds
A "" c= B ""
proof
let A, B be complex-membered set ; ::_thesis: ( A c= B implies A "" c= B "" )
assume A1: A c= B ; ::_thesis: A "" c= B ""
let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A "" or a in B "" )
assume a in A "" ; ::_thesis: a in B ""
then a " in A by Th29;
hence a in B "" by A1, Th29; ::_thesis: verum
end;
theorem Th30: :: MEMBER_1:30
for A, B being complex-membered set holds
( A c= B iff A "" c= B "" )
proof
let A, B be complex-membered set ; ::_thesis: ( A c= B iff A "" c= B "" )
( (A "") "" = A & (B "") "" = B ) ;
hence ( A c= B iff A "" c= B "" ) by Lm3; ::_thesis: verum
end;
theorem :: MEMBER_1:31
for A, B being complex-membered set st A "" = B "" holds
A = B
proof
let A, B be complex-membered set ; ::_thesis: ( A "" = B "" implies A = B )
assume A "" = B "" ; ::_thesis: A = B
then ( A c= B & B c= A ) by Th30;
hence A = B by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th32: :: MEMBER_1:32
for A, B being complex-membered set holds (A \/ B) "" = (A "") \/ (B "")
proof
let A, B be complex-membered set ; ::_thesis: (A \/ B) "" = (A "") \/ (B "")
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A \/ B) "" or a in (A "") \/ (B "") ) & ( not a in (A "") \/ (B "") or a in (A \/ B) "" ) )
hereby ::_thesis: ( not a in (A "") \/ (B "") or a in (A \/ B) "" )
assume a in (A \/ B) "" ; ::_thesis: a in (A "") \/ (B "")
then a " in A \/ B by Th29;
then ( a " in A or a " in B ) by XBOOLE_0:def_3;
then ( a in A "" or a in B "" ) by Th29;
hence a in (A "") \/ (B "") by XBOOLE_0:def_3; ::_thesis: verum
end;
assume a in (A "") \/ (B "") ; ::_thesis: a in (A \/ B) ""
then ( a in A "" or a in B "" ) by XBOOLE_0:def_3;
then ( a " in A or a " in B ) by Th29;
then a " in A \/ B by XBOOLE_0:def_3;
hence a in (A \/ B) "" by Th29; ::_thesis: verum
end;
theorem Th33: :: MEMBER_1:33
for A, B being complex-membered set holds (A /\ B) "" = (A "") /\ (B "")
proof
let A, B be complex-membered set ; ::_thesis: (A /\ B) "" = (A "") /\ (B "")
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A /\ B) "" or a in (A "") /\ (B "") ) & ( not a in (A "") /\ (B "") or a in (A /\ B) "" ) )
hereby ::_thesis: ( not a in (A "") /\ (B "") or a in (A /\ B) "" )
assume a in (A /\ B) "" ; ::_thesis: a in (A "") /\ (B "")
then A1: a " in A /\ B by Th29;
then a " in B by XBOOLE_0:def_4;
then A2: a in B "" by Th29;
a " in A by A1, XBOOLE_0:def_4;
then a in A "" by Th29;
hence a in (A "") /\ (B "") by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A3: a in (A "") /\ (B "") ; ::_thesis: a in (A /\ B) ""
then a in B "" by XBOOLE_0:def_4;
then A4: a " in B by Th29;
a in A "" by A3, XBOOLE_0:def_4;
then a " in A by Th29;
then a " in A /\ B by A4, XBOOLE_0:def_4;
hence a in (A /\ B) "" by Th29; ::_thesis: verum
end;
theorem Th34: :: MEMBER_1:34
for A, B being complex-membered set holds (A \ B) "" = (A "") \ (B "")
proof
let A, B be complex-membered set ; ::_thesis: (A \ B) "" = (A "") \ (B "")
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A \ B) "" or a in (A "") \ (B "") ) & ( not a in (A "") \ (B "") or a in (A \ B) "" ) )
hereby ::_thesis: ( not a in (A "") \ (B "") or a in (A \ B) "" )
assume a in (A \ B) "" ; ::_thesis: a in (A "") \ (B "")
then A1: a " in A \ B by Th29;
then not a " in B by XBOOLE_0:def_5;
then A2: not a in B "" by Th29;
a in A "" by A1, Th29;
hence a in (A "") \ (B "") by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A3: a in (A "") \ (B "") ; ::_thesis: a in (A \ B) ""
then not a in B "" by XBOOLE_0:def_5;
then A4: not a " in B by Th29;
a " in A by A3, Th29;
then a " in A \ B by A4, XBOOLE_0:def_5;
hence a in (A \ B) "" by Th29; ::_thesis: verum
end;
theorem Th35: :: MEMBER_1:35
for A, B being complex-membered set holds (A \+\ B) "" = (A "") \+\ (B "")
proof
let A, B be complex-membered set ; ::_thesis: (A \+\ B) "" = (A "") \+\ (B "")
thus (A \+\ B) "" = ((A \ B) "") \/ ((B \ A) "") by Th32
.= ((A "") \ (B "")) \/ ((B \ A) "") by Th34
.= (A "") \+\ (B "") by Th34 ; ::_thesis: verum
end;
theorem Th36: :: MEMBER_1:36
for A being complex-membered set holds -- (A "") = (-- A) ""
proof
let A be complex-membered set ; ::_thesis: -- (A "") = (-- A) ""
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in -- (A "") or a in (-- A) "" ) & ( not a in (-- A) "" or a in -- (A "") ) )
A1: (- a) " = - (a ") by XCMPLX_1:222;
hereby ::_thesis: ( not a in (-- A) "" or a in -- (A "") )
assume a in -- (A "") ; ::_thesis: a in (-- A) ""
then - a in A "" by Th12;
then (- a) " in A by Th29;
then a " in -- A by A1, Th12;
hence a in (-- A) "" by Th29; ::_thesis: verum
end;
assume a in (-- A) "" ; ::_thesis: a in -- (A "")
then a " in -- A by Th29;
then - (a ") in A by Th12;
then - a in A "" by A1, Th29;
hence a in -- (A "") by Th12; ::_thesis: verum
end;
theorem Th37: :: MEMBER_1:37
for a being complex number holds {a} "" = {(a ")}
proof
let a be complex number ; ::_thesis: {a} "" = {(a ")}
let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in {a} "" or z in {(a ")} ) & ( not z in {(a ")} or z in {a} "" ) )
hereby ::_thesis: ( not z in {(a ")} or z in {a} "" )
assume z in {a} "" ; ::_thesis: z in {(a ")}
then consider c being Element of COMPLEX such that
A1: z = c " and
A2: c in {a} ;
c = a by A2, TARSKI:def_1;
hence z in {(a ")} by A1, TARSKI:def_1; ::_thesis: verum
end;
assume z in {(a ")} ; ::_thesis: z in {a} ""
then A3: z = a " by TARSKI:def_1;
( a in COMPLEX & a in {a} ) by TARSKI:def_1, XCMPLX_0:def_2;
hence z in {a} "" by A3; ::_thesis: verum
end;
theorem Th38: :: MEMBER_1:38
for a, b being complex number holds {a,b} "" = {(a "),(b ")}
proof
let a, b be complex number ; ::_thesis: {a,b} "" = {(a "),(b ")}
let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in {a,b} "" or z in {(a "),(b ")} ) & ( not z in {(a "),(b ")} or z in {a,b} "" ) )
hereby ::_thesis: ( not z in {(a "),(b ")} or z in {a,b} "" )
assume z in {a,b} "" ; ::_thesis: z in {(a "),(b ")}
then consider c being Element of COMPLEX such that
A1: z = c " and
A2: c in {a,b} ;
( c = a or c = b ) by A2, TARSKI:def_2;
hence z in {(a "),(b ")} by A1, TARSKI:def_2; ::_thesis: verum
end;
A3: ( a in {a,b} & b in {a,b} ) by TARSKI:def_2;
assume z in {(a "),(b ")} ; ::_thesis: z in {a,b} ""
then A4: ( z = a " or z = b " ) by TARSKI:def_2;
( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2;
hence z in {a,b} "" by A4, A3; ::_thesis: verum
end;
definition
let F, G be ext-real-membered set ;
funcF ++ G -> set equals :: MEMBER_1:def 5
{ (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ;
coherence
{ (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } is set ;
commutativity
for b1 being set
for F, G being ext-real-membered set st b1 = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds
b1 = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }
proof
let X be set ; ::_thesis: for F, G being ext-real-membered set st X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds
X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }
let F, G be ext-real-membered set ; ::_thesis: ( X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } implies X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } )
assume A1: X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; ::_thesis: X = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }
thus X c= { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } :: according to XBOOLE_0:def_10 ::_thesis: { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } )
assume e in X ; ::_thesis: e in { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }
then ex w1, w2 being Element of ExtREAL st
( e = w1 + w2 & w1 in F & w2 in G ) by A1;
hence e in { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } or e in X )
assume e in { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ; ::_thesis: e in X
then ex w1, w2 being Element of ExtREAL st
( e = w1 + w2 & w1 in G & w2 in F ) ;
hence e in X by A1; ::_thesis: verum
end;
end;
:: deftheorem defines ++ MEMBER_1:def_5_:_
for F, G being ext-real-membered set holds F ++ G = { (w1 + w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ;
theorem Th39: :: MEMBER_1:39
for F, G being ext-real-membered set
for f, g being ext-real number st f in F & g in G holds
f + g in F ++ G
proof
let F, G be ext-real-membered set ; ::_thesis: for f, g being ext-real number st f in F & g in G holds
f + g in F ++ G
let f, g be ext-real number ; ::_thesis: ( f in F & g in G implies f + g in F ++ G )
( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1;
hence ( f in F & g in G implies f + g in F ++ G ) ; ::_thesis: verum
end;
registration
let F be empty set ;
let G be ext-real-membered set ;
clusterF ++ G -> empty ;
coherence
F ++ G is empty
proof
assume not F ++ G is empty ; ::_thesis: contradiction
then the Element of F ++ G in F ++ G ;
then ex w1, w2 being Element of ExtREAL st
( the Element of F ++ G = w1 + w2 & w1 in F & w2 in G ) ;
hence contradiction ; ::_thesis: verum
end;
clusterG ++ F -> empty ;
coherence
G ++ F is empty ;
end;
registration
let F, G be non empty ext-real-membered set ;
clusterF ++ G -> non empty ;
coherence
not F ++ G is empty
proof
the Element of F + the Element of G in F ++ G by Th39;
hence not F ++ G is empty ; ::_thesis: verum
end;
end;
registration
let F, G be ext-real-membered set ;
clusterF ++ G -> ext-real-membered ;
coherence
F ++ G is ext-real-membered
proof
let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( not e in F ++ G or e is ext-real )
assume e in F ++ G ; ::_thesis: e is ext-real
then ex w1, w2 being Element of ExtREAL st
( e = w1 + w2 & w1 in F & w2 in G ) ;
hence e is ext-real ; ::_thesis: verum
end;
end;
theorem :: MEMBER_1:40
for F, G, H, I being ext-real-membered set st F c= G & H c= I holds
F ++ H c= G ++ I
proof
let F, G, H, I be ext-real-membered set ; ::_thesis: ( F c= G & H c= I implies F ++ H c= G ++ I )
assume A1: ( F c= G & H c= I ) ; ::_thesis: F ++ H c= G ++ I
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F ++ H or i in G ++ I )
assume i in F ++ H ; ::_thesis: i in G ++ I
then ex w, w1 being Element of ExtREAL st
( i = w + w1 & w in F & w1 in H ) ;
hence i in G ++ I by A1; ::_thesis: verum
end;
theorem Th41: :: MEMBER_1:41
for F, G, H being ext-real-membered set holds F ++ (G \/ H) = (F ++ G) \/ (F ++ H)
proof
let F, G, H be ext-real-membered set ; ::_thesis: F ++ (G \/ H) = (F ++ G) \/ (F ++ H)
let j be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not j in F ++ (G \/ H) or j in (F ++ G) \/ (F ++ H) ) & ( not j in (F ++ G) \/ (F ++ H) or j in F ++ (G \/ H) ) )
hereby ::_thesis: ( not j in (F ++ G) \/ (F ++ H) or j in F ++ (G \/ H) )
assume j in F ++ (G \/ H) ; ::_thesis: j in (F ++ G) \/ (F ++ H)
then consider w, w1 being Element of ExtREAL such that
A1: j = w + w1 and
A2: w in F and
A3: w1 in G \/ H ;
( w1 in G or w1 in H ) by A3, XBOOLE_0:def_3;
then ( w + w1 in F ++ G or w + w1 in F ++ H ) by A2;
hence j in (F ++ G) \/ (F ++ H) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A4: j in (F ++ G) \/ (F ++ H) ; ::_thesis: j in F ++ (G \/ H)
percases ( j in F ++ G or j in F ++ H ) by A4, XBOOLE_0:def_3;
suppose j in F ++ G ; ::_thesis: j in F ++ (G \/ H)
then consider w, w1 being Element of ExtREAL such that
A5: ( j = w + w1 & w in F ) and
A6: w1 in G ;
w1 in G \/ H by A6, XBOOLE_0:def_3;
hence j in F ++ (G \/ H) by A5; ::_thesis: verum
end;
suppose j in F ++ H ; ::_thesis: j in F ++ (G \/ H)
then consider w, w1 being Element of ExtREAL such that
A7: ( j = w + w1 & w in F ) and
A8: w1 in H ;
w1 in G \/ H by A8, XBOOLE_0:def_3;
hence j in F ++ (G \/ H) by A7; ::_thesis: verum
end;
end;
end;
theorem Th42: :: MEMBER_1:42
for F, G, H being ext-real-membered set holds F ++ (G /\ H) c= (F ++ G) /\ (F ++ H)
proof
let F, G, H be ext-real-membered set ; ::_thesis: F ++ (G /\ H) c= (F ++ G) /\ (F ++ H)
let j be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not j in F ++ (G /\ H) or j in (F ++ G) /\ (F ++ H) )
assume j in F ++ (G /\ H) ; ::_thesis: j in (F ++ G) /\ (F ++ H)
then consider w, w1 being Element of ExtREAL such that
A1: j = w + w1 and
A2: w in F and
A3: w1 in G /\ H ;
w1 in H by A3, XBOOLE_0:def_4;
then A4: w + w1 in F ++ H by A2;
w1 in G by A3, XBOOLE_0:def_4;
then w + w1 in F ++ G by A2;
hence j in (F ++ G) /\ (F ++ H) by A1, A4, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th43: :: MEMBER_1:43
for f, g being ext-real number holds {f} ++ {g} = {(f + g)}
proof
let f, g be ext-real number ; ::_thesis: {f} ++ {g} = {(f + g)}
let j be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not j in {f} ++ {g} or j in {(f + g)} ) & ( not j in {(f + g)} or j in {f} ++ {g} ) )
hereby ::_thesis: ( not j in {(f + g)} or j in {f} ++ {g} )
assume j in {f} ++ {g} ; ::_thesis: j in {(f + g)}
then consider w1, w2 being Element of ExtREAL such that
A1: j = w1 + w2 and
A2: ( w1 in {f} & w2 in {g} ) ;
( w1 = f & w2 = g ) by A2, TARSKI:def_1;
hence j in {(f + g)} by A1, TARSKI:def_1; ::_thesis: verum
end;
A3: ( f in {f} & g in {g} ) by TARSKI:def_1;
assume j in {(f + g)} ; ::_thesis: j in {f} ++ {g}
then A4: j = f + g by TARSKI:def_1;
( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1;
hence j in {f} ++ {g} by A4, A3; ::_thesis: verum
end;
theorem Th44: :: MEMBER_1:44
for f, g, h being ext-real number holds {f} ++ {g,h} = {(f + g),(f + h)}
proof
let f, g, h be ext-real number ; ::_thesis: {f} ++ {g,h} = {(f + g),(f + h)}
thus {f} ++ {g,h} = {f} ++ ({g} \/ {h}) by ENUMSET1:1
.= ({f} ++ {g}) \/ ({f} ++ {h}) by Th41
.= {(f + g)} \/ ({f} ++ {h}) by Th43
.= {(f + g)} \/ {(f + h)} by Th43
.= {(f + g),(f + h)} by ENUMSET1:1 ; ::_thesis: verum
end;
theorem Th45: :: MEMBER_1:45
for f, g, h, i being ext-real number holds {f,g} ++ {h,i} = {(f + h),(f + i),(g + h),(g + i)}
proof
let f, g, h, i be ext-real number ; ::_thesis: {f,g} ++ {h,i} = {(f + h),(f + i),(g + h),(g + i)}
thus {f,g} ++ {h,i} = ({f} \/ {g}) ++ {h,i} by ENUMSET1:1
.= ({f} ++ {h,i}) \/ ({g} ++ {h,i}) by Th41
.= {(f + h),(f + i)} \/ ({g} ++ {h,i}) by Th44
.= {(f + h),(f + i)} \/ {(g + h),(g + i)} by Th44
.= {(f + h),(f + i),(g + h),(g + i)} by ENUMSET1:5 ; ::_thesis: verum
end;
definition
let A, B be complex-membered set ;
funcA ++ B -> set equals :: MEMBER_1:def 6
{ (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ;
coherence
{ (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } is set ;
commutativity
for b1 being set
for A, B being complex-membered set st b1 = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } holds
b1 = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) }
proof
let X be set ; ::_thesis: for A, B being complex-membered set st X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } holds
X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) }
let A, B be complex-membered set ; ::_thesis: ( X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } implies X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } )
assume A1: X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; ::_thesis: X = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) }
thus X c= { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } :: according to XBOOLE_0:def_10 ::_thesis: { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } )
assume e in X ; ::_thesis: e in { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) }
then ex c1, c2 being Element of COMPLEX st
( e = c1 + c2 & c1 in A & c2 in B ) by A1;
hence e in { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } or e in X )
assume e in { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ; ::_thesis: e in X
then ex c1, c2 being Element of COMPLEX st
( e = c1 + c2 & c1 in B & c2 in A ) ;
hence e in X by A1; ::_thesis: verum
end;
end;
:: deftheorem defines ++ MEMBER_1:def_6_:_
for A, B being complex-membered set holds A ++ B = { (c1 + c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ;
theorem Th46: :: MEMBER_1:46
for A, B being complex-membered set
for a, b being complex number st a in A & b in B holds
a + b in A ++ B
proof
let A, B be complex-membered set ; ::_thesis: for a, b being complex number st a in A & b in B holds
a + b in A ++ B
let a, b be complex number ; ::_thesis: ( a in A & b in B implies a + b in A ++ B )
( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2;
hence ( a in A & b in B implies a + b in A ++ B ) ; ::_thesis: verum
end;
registration
let A be empty set ;
let B be complex-membered set ;
clusterA ++ B -> empty ;
coherence
A ++ B is empty
proof
assume not A ++ B is empty ; ::_thesis: contradiction
then the Element of A ++ B in A ++ B ;
then ex c1, c2 being Element of COMPLEX st
( the Element of A ++ B = c1 + c2 & c1 in A & c2 in B ) ;
hence contradiction ; ::_thesis: verum
end;
clusterB ++ A -> empty ;
coherence
B ++ A is empty ;
end;
registration
let A, B be non empty complex-membered set ;
clusterA ++ B -> non empty ;
coherence
not A ++ B is empty
proof
the Element of A + the Element of B in A ++ B by Th46;
hence not A ++ B is empty ; ::_thesis: verum
end;
end;
registration
let A, B be complex-membered set ;
clusterA ++ B -> complex-membered ;
coherence
A ++ B is complex-membered
proof
let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( not e in A ++ B or e is complex )
assume e in A ++ B ; ::_thesis: e is complex
then ex c1, c2 being Element of COMPLEX st
( e = c1 + c2 & c1 in A & c2 in B ) ;
hence e is complex ; ::_thesis: verum
end;
end;
registration
let A, B be real-membered set ;
clusterA ++ B -> real-membered ;
coherence
A ++ B is real-membered
proof
let e be set ; :: according to MEMBERED:def_3 ::_thesis: ( not e in A ++ B or e is real )
assume e in A ++ B ; ::_thesis: e is real
then ex c1, c2 being Element of COMPLEX st
( e = c1 + c2 & c1 in A & c2 in B ) ;
hence e is real ; ::_thesis: verum
end;
end;
registration
let A, B be rational-membered set ;
clusterA ++ B -> rational-membered ;
coherence
A ++ B is rational-membered
proof
let e be set ; :: according to MEMBERED:def_4 ::_thesis: ( not e in A ++ B or e is rational )
assume e in A ++ B ; ::_thesis: e is rational
then ex c1, c2 being Element of COMPLEX st
( e = c1 + c2 & c1 in A & c2 in B ) ;
hence e is rational ; ::_thesis: verum
end;
end;
registration
let A, B be integer-membered set ;
clusterA ++ B -> integer-membered ;
coherence
A ++ B is integer-membered
proof
let e be set ; :: according to MEMBERED:def_5 ::_thesis: ( not e in A ++ B or e is integer )
assume e in A ++ B ; ::_thesis: e is integer
then ex c1, c2 being Element of COMPLEX st
( e = c1 + c2 & c1 in A & c2 in B ) ;
hence e is integer ; ::_thesis: verum
end;
end;
registration
let A, B be natural-membered set ;
clusterA ++ B -> natural-membered ;
coherence
A ++ B is natural-membered
proof
let e be set ; :: according to MEMBERED:def_6 ::_thesis: ( not e in A ++ B or e is natural )
assume e in A ++ B ; ::_thesis: e is natural
then ex c1, c2 being Element of COMPLEX st
( e = c1 + c2 & c1 in A & c2 in B ) ;
hence e is natural ; ::_thesis: verum
end;
end;
registration
let A, B be real-membered set ;
let F, G be ext-real-membered set ;
identifyA ++ B with F ++ G when A = F, B = G;
compatibility
( A = F & B = G implies A ++ B = F ++ G )
proof
assume A1: ( A = F & B = G ) ; ::_thesis: A ++ B = F ++ G
let a be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not a in A ++ B or a in F ++ G ) & ( not a in F ++ G or a in A ++ B ) )
hereby ::_thesis: ( not a in F ++ G or a in A ++ B )
assume a in A ++ B ; ::_thesis: a in F ++ G
then consider c, c1 being Element of COMPLEX such that
A2: a = c + c1 and
A3: ( c in A & c1 in B ) ;
reconsider d1 = c, d2 = c1 as Element of ExtREAL by A3, XXREAL_0:def_1;
a = d1 + d2 by A2, A3, XXREAL_3:def_2;
hence a in F ++ G by A1, A3; ::_thesis: verum
end;
assume a in F ++ G ; ::_thesis: a in A ++ B
then consider w, w1 being Element of ExtREAL such that
A4: a = w + w1 and
A5: ( w in F & w1 in G ) ;
reconsider d1 = w, d2 = w1 as Element of COMPLEX by A1, A5, XCMPLX_0:def_2;
a = d1 + d2 by A1, A4, A5, XXREAL_3:def_2;
hence a in A ++ B by A1, A5; ::_thesis: verum
end;
end;
theorem Th47: :: MEMBER_1:47
for A, B, C, D being complex-membered set st A c= B & C c= D holds
A ++ C c= B ++ D
proof
let A, B, C, D be complex-membered set ; ::_thesis: ( A c= B & C c= D implies A ++ C c= B ++ D )
assume A1: ( A c= B & C c= D ) ; ::_thesis: A ++ C c= B ++ D
let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A ++ C or a in B ++ D )
assume a in A ++ C ; ::_thesis: a in B ++ D
then ex c, c1 being Element of COMPLEX st
( a = c + c1 & c in A & c1 in C ) ;
hence a in B ++ D by A1; ::_thesis: verum
end;
theorem Th48: :: MEMBER_1:48
for A, B, C being complex-membered set holds A ++ (B \/ C) = (A ++ B) \/ (A ++ C)
proof
let A, B, C be complex-membered set ; ::_thesis: A ++ (B \/ C) = (A ++ B) \/ (A ++ C)
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in A ++ (B \/ C) or a in (A ++ B) \/ (A ++ C) ) & ( not a in (A ++ B) \/ (A ++ C) or a in A ++ (B \/ C) ) )
hereby ::_thesis: ( not a in (A ++ B) \/ (A ++ C) or a in A ++ (B \/ C) )
assume a in A ++ (B \/ C) ; ::_thesis: a in (A ++ B) \/ (A ++ C)
then consider c, c1 being Element of COMPLEX such that
A1: a = c + c1 and
A2: c in A and
A3: c1 in B \/ C ;
( c1 in B or c1 in C ) by A3, XBOOLE_0:def_3;
then ( c + c1 in A ++ B or c + c1 in A ++ C ) by A2;
hence a in (A ++ B) \/ (A ++ C) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A4: a in (A ++ B) \/ (A ++ C) ; ::_thesis: a in A ++ (B \/ C)
percases ( a in A ++ B or a in A ++ C ) by A4, XBOOLE_0:def_3;
suppose a in A ++ B ; ::_thesis: a in A ++ (B \/ C)
then consider c, c1 being Element of COMPLEX such that
A5: ( a = c + c1 & c in A ) and
A6: c1 in B ;
c1 in B \/ C by A6, XBOOLE_0:def_3;
hence a in A ++ (B \/ C) by A5; ::_thesis: verum
end;
suppose a in A ++ C ; ::_thesis: a in A ++ (B \/ C)
then consider c, c1 being Element of COMPLEX such that
A7: ( a = c + c1 & c in A ) and
A8: c1 in C ;
c1 in B \/ C by A8, XBOOLE_0:def_3;
hence a in A ++ (B \/ C) by A7; ::_thesis: verum
end;
end;
end;
theorem Th49: :: MEMBER_1:49
for A, B, C being complex-membered set holds A ++ (B /\ C) c= (A ++ B) /\ (A ++ C)
proof
let A, B, C be complex-membered set ; ::_thesis: A ++ (B /\ C) c= (A ++ B) /\ (A ++ C)
let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A ++ (B /\ C) or a in (A ++ B) /\ (A ++ C) )
assume a in A ++ (B /\ C) ; ::_thesis: a in (A ++ B) /\ (A ++ C)
then consider c, c1 being Element of COMPLEX such that
A1: a = c + c1 and
A2: c in A and
A3: c1 in B /\ C ;
c1 in C by A3, XBOOLE_0:def_4;
then A4: c + c1 in A ++ C by A2;
c1 in B by A3, XBOOLE_0:def_4;
then c + c1 in A ++ B by A2;
hence a in (A ++ B) /\ (A ++ C) by A1, A4, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th50: :: MEMBER_1:50
for A, B, C being complex-membered set holds (A ++ B) ++ C = A ++ (B ++ C)
proof
let A, B, C be complex-membered set ; ::_thesis: (A ++ B) ++ C = A ++ (B ++ C)
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A ++ B) ++ C or a in A ++ (B ++ C) ) & ( not a in A ++ (B ++ C) or a in (A ++ B) ++ C ) )
hereby ::_thesis: ( not a in A ++ (B ++ C) or a in (A ++ B) ++ C )
assume a in (A ++ B) ++ C ; ::_thesis: a in A ++ (B ++ C)
then consider c, c1 being Element of COMPLEX such that
A1: a = c + c1 and
A2: c in A ++ B and
A3: c1 in C ;
consider c2, c3 being Element of COMPLEX such that
A4: c = c2 + c3 and
A5: c2 in A and
A6: c3 in B by A2;
( a = c2 + (c3 + c1) & c3 + c1 in B ++ C ) by A1, A3, A4, A6;
hence a in A ++ (B ++ C) by A5; ::_thesis: verum
end;
assume a in A ++ (B ++ C) ; ::_thesis: a in (A ++ B) ++ C
then consider c, c1 being Element of COMPLEX such that
A7: ( a = c + c1 & c in A ) and
A8: c1 in B ++ C ;
consider c2, c3 being Element of COMPLEX such that
A9: ( c1 = c2 + c3 & c2 in B ) and
A10: c3 in C by A8;
( a = (c + c2) + c3 & c + c2 in A ++ B ) by A7, A9;
hence a in (A ++ B) ++ C by A10; ::_thesis: verum
end;
theorem Th51: :: MEMBER_1:51
for a, b being complex number holds {a} ++ {b} = {(a + b)}
proof
let a, b be complex number ; ::_thesis: {a} ++ {b} = {(a + b)}
let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in {a} ++ {b} or z in {(a + b)} ) & ( not z in {(a + b)} or z in {a} ++ {b} ) )
hereby ::_thesis: ( not z in {(a + b)} or z in {a} ++ {b} )
assume z in {a} ++ {b} ; ::_thesis: z in {(a + b)}
then consider c1, c2 being Element of COMPLEX such that
A1: z = c1 + c2 and
A2: ( c1 in {a} & c2 in {b} ) ;
( c1 = a & c2 = b ) by A2, TARSKI:def_1;
hence z in {(a + b)} by A1, TARSKI:def_1; ::_thesis: verum
end;
A3: ( a in {a} & b in {b} ) by TARSKI:def_1;
assume z in {(a + b)} ; ::_thesis: z in {a} ++ {b}
then A4: z = a + b by TARSKI:def_1;
( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2;
hence z in {a} ++ {b} by A4, A3; ::_thesis: verum
end;
theorem Th52: :: MEMBER_1:52
for a, s, t being complex number holds {a} ++ {s,t} = {(a + s),(a + t)}
proof
let a, s, t be complex number ; ::_thesis: {a} ++ {s,t} = {(a + s),(a + t)}
thus {a} ++ {s,t} = {a} ++ ({s} \/ {t}) by ENUMSET1:1
.= ({a} ++ {s}) \/ ({a} ++ {t}) by Th48
.= {(a + s)} \/ ({a} ++ {t}) by Th51
.= {(a + s)} \/ {(a + t)} by Th51
.= {(a + s),(a + t)} by ENUMSET1:1 ; ::_thesis: verum
end;
theorem Th53: :: MEMBER_1:53
for a, b, s, t being complex number holds {a,b} ++ {s,t} = {(a + s),(a + t),(b + s),(b + t)}
proof
let a, b, s, t be complex number ; ::_thesis: {a,b} ++ {s,t} = {(a + s),(a + t),(b + s),(b + t)}
thus {a,b} ++ {s,t} = ({a} \/ {b}) ++ {s,t} by ENUMSET1:1
.= ({a} ++ {s,t}) \/ ({b} ++ {s,t}) by Th48
.= {(a + s),(a + t)} \/ ({b} ++ {s,t}) by Th52
.= {(a + s),(a + t)} \/ {(b + s),(b + t)} by Th52
.= {(a + s),(a + t),(b + s),(b + t)} by ENUMSET1:5 ; ::_thesis: verum
end;
definition
let F, G be ext-real-membered set ;
funcF -- G -> set equals :: MEMBER_1:def 7
F ++ (-- G);
coherence
F ++ (-- G) is set ;
end;
:: deftheorem defines -- MEMBER_1:def_7_:_
for F, G being ext-real-membered set holds F -- G = F ++ (-- G);
theorem Th54: :: MEMBER_1:54
for F, G being ext-real-membered set holds F -- G = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) }
proof
let F, G be ext-real-membered set ; ::_thesis: F -- G = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) }
thus F -- G c= { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } :: according to XBOOLE_0:def_10 ::_thesis: { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } c= F -- G
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F -- G or e in { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } )
assume e in F -- G ; ::_thesis: e in { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) }
then consider w1, w2 being Element of ExtREAL such that
A1: e = w1 + w2 and
A2: w1 in F and
A3: w2 in -- G ;
( e = w1 - (- w2) & - w2 in G ) by A1, A3, Th2;
hence e in { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } by A2; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } or e in F -- G )
assume e in { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; ::_thesis: e in F -- G
then consider w1, w2 being Element of ExtREAL such that
A4: ( e = w1 - w2 & w1 in F ) and
A5: w2 in G ;
- w2 in -- G by A5;
hence e in F -- G by A4; ::_thesis: verum
end;
theorem Th55: :: MEMBER_1:55
for F, G being ext-real-membered set
for f, g being ext-real number st f in F & g in G holds
f - g in F -- G
proof
let F, G be ext-real-membered set ; ::_thesis: for f, g being ext-real number st f in F & g in G holds
f - g in F -- G
let f, g be ext-real number ; ::_thesis: ( f in F & g in G implies f - g in F -- G )
A1: ( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1;
F -- G = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } by Th54;
hence ( f in F & g in G implies f - g in F -- G ) by A1; ::_thesis: verum
end;
registration
let F be empty set ;
let G be ext-real-membered set ;
clusterF -- G -> empty ;
coherence
F -- G is empty ;
clusterG -- F -> empty ;
coherence
G -- F is empty ;
end;
registration
let F, G be non empty ext-real-membered set ;
clusterF -- G -> non empty ;
coherence
not F -- G is empty ;
end;
registration
let F, G be ext-real-membered set ;
clusterF -- G -> ext-real-membered ;
coherence
F -- G is ext-real-membered ;
end;
theorem :: MEMBER_1:56
for F, G, H, I being ext-real-membered set st F c= G & H c= I holds
F -- H c= G -- I
proof
let F, G, H, I be ext-real-membered set ; ::_thesis: ( F c= G & H c= I implies F -- H c= G -- I )
assume A1: ( F c= G & H c= I ) ; ::_thesis: F -- H c= G -- I
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F -- H or i in G -- I )
A2: F -- H = { (w1 - w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in H ) } by Th54;
assume i in F -- H ; ::_thesis: i in G -- I
then ex w, w1 being Element of ExtREAL st
( i = w - w1 & w in F & w1 in H ) by A2;
hence i in G -- I by A1, Th55; ::_thesis: verum
end;
theorem :: MEMBER_1:57
for F, G, H being ext-real-membered set holds F -- (G \/ H) = (F -- G) \/ (F -- H)
proof
let F, G, H be ext-real-membered set ; ::_thesis: F -- (G \/ H) = (F -- G) \/ (F -- H)
thus F -- (G \/ H) = F ++ ((-- G) \/ (-- H)) by Th5
.= (F -- G) \/ (F -- H) by Th41 ; ::_thesis: verum
end;
theorem :: MEMBER_1:58
for F, G, H being ext-real-membered set holds F -- (G /\ H) c= (F -- G) /\ (F -- H)
proof
let F, G, H be ext-real-membered set ; ::_thesis: F -- (G /\ H) c= (F -- G) /\ (F -- H)
F -- (G /\ H) = F ++ ((-- G) /\ (-- H)) by Th6;
hence F -- (G /\ H) c= (F -- G) /\ (F -- H) by Th42; ::_thesis: verum
end;
Lm4: for F, G being ext-real-membered set holds -- (F ++ G) = (-- F) ++ (-- G)
proof
let F, G be ext-real-membered set ; ::_thesis: -- (F ++ G) = (-- F) ++ (-- G)
let j be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not j in -- (F ++ G) or j in (-- F) ++ (-- G) ) & ( not j in (-- F) ++ (-- G) or j in -- (F ++ G) ) )
hereby ::_thesis: ( not j in (-- F) ++ (-- G) or j in -- (F ++ G) )
assume j in -- (F ++ G) ; ::_thesis: j in (-- F) ++ (-- G)
then consider w being Element of ExtREAL such that
A1: j = - w and
A2: w in F ++ G ;
consider w1, w2 being Element of ExtREAL such that
A3: w = w1 + w2 and
A4: ( w1 in F & w2 in G ) by A2;
A5: - (w1 + w2) = (- w1) - w2 by XXREAL_3:9;
( - w1 in -- F & - w2 in -- G ) by A4;
hence j in (-- F) ++ (-- G) by A1, A3, A5; ::_thesis: verum
end;
assume j in (-- F) ++ (-- G) ; ::_thesis: j in -- (F ++ G)
then consider w1, w2 being Element of ExtREAL such that
A6: j = w1 + w2 and
A7: ( w1 in -- F & w2 in -- G ) ;
( - w1 in F & - w2 in G ) by A7, Th2;
then ( - (w1 + w2) = (- w1) - w2 & (- w1) + (- w2) in F ++ G ) by XXREAL_3:9;
hence j in -- (F ++ G) by A6, Th2; ::_thesis: verum
end;
theorem :: MEMBER_1:59
for F, G being ext-real-membered set holds -- (F ++ G) = (-- F) -- G by Lm4;
theorem Th60: :: MEMBER_1:60
for F, G being ext-real-membered set holds -- (F -- G) = (-- F) ++ G
proof
let F, G be ext-real-membered set ; ::_thesis: -- (F -- G) = (-- F) ++ G
thus -- (F -- G) = (-- F) -- (-- G) by Lm4
.= (-- F) ++ G ; ::_thesis: verum
end;
theorem :: MEMBER_1:61
for f, g being ext-real number holds {f} -- {g} = {(f - g)}
proof
let f, g be ext-real number ; ::_thesis: {f} -- {g} = {(f - g)}
thus {f} -- {g} = {f} ++ {(- g)} by Th9
.= {(f - g)} by Th43 ; ::_thesis: verum
end;
theorem :: MEMBER_1:62
for f, h, i being ext-real number holds {f} -- {h,i} = {(f - h),(f - i)}
proof
let f, h, i be ext-real number ; ::_thesis: {f} -- {h,i} = {(f - h),(f - i)}
thus {f} -- {h,i} = {f} ++ {(- h),(- i)} by Th10
.= {(f - h),(f - i)} by Th44 ; ::_thesis: verum
end;
theorem :: MEMBER_1:63
for f, g, h being ext-real number holds {f,g} -- {h} = {(f - h),(g - h)}
proof
let f, g, h be ext-real number ; ::_thesis: {f,g} -- {h} = {(f - h),(g - h)}
thus {f,g} -- {h} = {f,g} ++ {(- h)} by Th9
.= {(f - h),(g - h)} by Th44 ; ::_thesis: verum
end;
theorem :: MEMBER_1:64
for f, g, h, i being ext-real number holds {f,g} -- {h,i} = {(f - h),(f - i),(g - h),(g - i)}
proof
let f, g, h, i be ext-real number ; ::_thesis: {f,g} -- {h,i} = {(f - h),(f - i),(g - h),(g - i)}
thus {f,g} -- {h,i} = {f,g} ++ {(- h),(- i)} by Th10
.= {(f - h),(f - i),(g - h),(g - i)} by Th45 ; ::_thesis: verum
end;
definition
let A, B be complex-membered set ;
funcA -- B -> set equals :: MEMBER_1:def 8
A ++ (-- B);
coherence
A ++ (-- B) is set ;
end;
:: deftheorem defines -- MEMBER_1:def_8_:_
for A, B being complex-membered set holds A -- B = A ++ (-- B);
theorem Th65: :: MEMBER_1:65
for A, B being complex-membered set holds A -- B = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) }
proof
let A, B be complex-membered set ; ::_thesis: A -- B = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) }
thus A -- B c= { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } :: according to XBOOLE_0:def_10 ::_thesis: { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } c= A -- B
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A -- B or e in { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } )
assume e in A -- B ; ::_thesis: e in { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) }
then consider c1, c2 being Element of COMPLEX such that
A1: e = c1 + c2 and
A2: c1 in A and
A3: c2 in -- B ;
( e = c1 - (- c2) & - c2 in B ) by A1, A3, Th12;
hence e in { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } by A2; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } or e in A -- B )
assume e in { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; ::_thesis: e in A -- B
then consider c1, c2 being Element of COMPLEX such that
A4: ( e = c1 - c2 & c1 in A ) and
A5: c2 in B ;
- c2 in -- B by A5;
hence e in A -- B by A4; ::_thesis: verum
end;
theorem Th66: :: MEMBER_1:66
for A, B being complex-membered set
for a, b being complex number st a in A & b in B holds
a - b in A -- B
proof
let A, B be complex-membered set ; ::_thesis: for a, b being complex number st a in A & b in B holds
a - b in A -- B
let a, b be complex number ; ::_thesis: ( a in A & b in B implies a - b in A -- B )
A1: ( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2;
A -- B = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } by Th65;
hence ( a in A & b in B implies a - b in A -- B ) by A1; ::_thesis: verum
end;
registration
let A be empty set ;
let B be complex-membered set ;
clusterA -- B -> empty ;
coherence
A -- B is empty ;
clusterB -- A -> empty ;
coherence
B -- A is empty ;
end;
registration
let A, B be non empty complex-membered set ;
clusterA -- B -> non empty ;
coherence
not A -- B is empty ;
end;
registration
let A, B be complex-membered set ;
clusterA -- B -> complex-membered ;
coherence
A -- B is complex-membered ;
end;
registration
let A, B be real-membered set ;
clusterA -- B -> real-membered ;
coherence
A -- B is real-membered ;
end;
registration
let A, B be rational-membered set ;
clusterA -- B -> rational-membered ;
coherence
A -- B is rational-membered ;
end;
registration
let A, B be integer-membered set ;
clusterA -- B -> integer-membered ;
coherence
A -- B is integer-membered ;
end;
registration
let A, B be real-membered set ;
let F, G be ext-real-membered set ;
identifyA -- B with F -- G when A = F, B = G;
compatibility
( A = F & B = G implies A -- B = F -- G ) ;
end;
theorem Th67: :: MEMBER_1:67
for A, B, C, D being complex-membered set st A c= B & C c= D holds
A -- C c= B -- D
proof
let A, B, C, D be complex-membered set ; ::_thesis: ( A c= B & C c= D implies A -- C c= B -- D )
assume A1: ( A c= B & C c= D ) ; ::_thesis: A -- C c= B -- D
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A -- C or z in B -- D )
A2: A -- C = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in C ) } by Th65;
assume z in A -- C ; ::_thesis: z in B -- D
then ex c, c1 being Element of COMPLEX st
( z = c - c1 & c in A & c1 in C ) by A2;
hence z in B -- D by A1, Th66; ::_thesis: verum
end;
Lm5: for A, B being complex-membered set holds -- (A ++ B) = (-- A) ++ (-- B)
proof
let A, B be complex-membered set ; ::_thesis: -- (A ++ B) = (-- A) ++ (-- B)
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in -- (A ++ B) or a in (-- A) ++ (-- B) ) & ( not a in (-- A) ++ (-- B) or a in -- (A ++ B) ) )
hereby ::_thesis: ( not a in (-- A) ++ (-- B) or a in -- (A ++ B) )
assume a in -- (A ++ B) ; ::_thesis: a in (-- A) ++ (-- B)
then consider c being Element of COMPLEX such that
A1: a = - c and
A2: c in A ++ B ;
consider c1, c2 being Element of COMPLEX such that
A3: c = c1 + c2 and
A4: ( c1 in A & c2 in B ) by A2;
A5: ( - c1 in -- A & - c2 in -- B ) by A4;
a = (- c1) + (- c2) by A1, A3;
hence a in (-- A) ++ (-- B) by A5; ::_thesis: verum
end;
assume a in (-- A) ++ (-- B) ; ::_thesis: a in -- (A ++ B)
then consider c1, c2 being Element of COMPLEX such that
A6: a = c1 + c2 and
A7: ( c1 in -- A & c2 in -- B ) ;
( - c1 in A & - c2 in B ) by A7, Th12;
then (- c1) + (- c2) in A ++ B ;
then - a in A ++ B by A6;
hence a in -- (A ++ B) by Th12; ::_thesis: verum
end;
theorem :: MEMBER_1:68
for A, B, C being complex-membered set holds A -- (B \/ C) = (A -- B) \/ (A -- C)
proof
let A, B, C be complex-membered set ; ::_thesis: A -- (B \/ C) = (A -- B) \/ (A -- C)
thus A -- (B \/ C) = A ++ ((-- B) \/ (-- C)) by Th15
.= (A -- B) \/ (A -- C) by Th48 ; ::_thesis: verum
end;
theorem :: MEMBER_1:69
for A, B, C being complex-membered set holds A -- (B /\ C) c= (A -- B) /\ (A -- C)
proof
let A, B, C be complex-membered set ; ::_thesis: A -- (B /\ C) c= (A -- B) /\ (A -- C)
A -- (B /\ C) = A ++ ((-- B) /\ (-- C)) by Th16;
hence A -- (B /\ C) c= (A -- B) /\ (A -- C) by Th49; ::_thesis: verum
end;
theorem :: MEMBER_1:70
for A, B being complex-membered set holds -- (A ++ B) = (-- A) -- B by Lm5;
theorem Th71: :: MEMBER_1:71
for A, B being complex-membered set holds -- (A -- B) = (-- A) ++ B
proof
let A, B be complex-membered set ; ::_thesis: -- (A -- B) = (-- A) ++ B
thus -- (A -- B) = (-- A) -- (-- B) by Lm5
.= (-- A) ++ B ; ::_thesis: verum
end;
theorem :: MEMBER_1:72
for A, B, C being complex-membered set holds A ++ (B -- C) = (A ++ B) -- C by Th50;
theorem :: MEMBER_1:73
for A, B, C being complex-membered set holds A -- (B ++ C) = (A -- B) -- C
proof
let A, B, C be complex-membered set ; ::_thesis: A -- (B ++ C) = (A -- B) -- C
thus A -- (B ++ C) = A ++ ((-- B) -- C) by Lm5
.= (A -- B) -- C by Th50 ; ::_thesis: verum
end;
theorem :: MEMBER_1:74
for A, B, C being complex-membered set holds A -- (B -- C) = (A -- B) ++ C
proof
let A, B, C be complex-membered set ; ::_thesis: A -- (B -- C) = (A -- B) ++ C
thus A -- (B -- C) = A ++ ((-- B) ++ C) by Th71
.= (A -- B) ++ C by Th50 ; ::_thesis: verum
end;
theorem Th75: :: MEMBER_1:75
for a, b being complex number holds {a} -- {b} = {(a - b)}
proof
let a, b be complex number ; ::_thesis: {a} -- {b} = {(a - b)}
thus {a} -- {b} = {a} ++ {(- b)} by Th19
.= {(a - b)} by Th51 ; ::_thesis: verum
end;
theorem :: MEMBER_1:76
for a, s, t being complex number holds {a} -- {s,t} = {(a - s),(a - t)}
proof
let a, s, t be complex number ; ::_thesis: {a} -- {s,t} = {(a - s),(a - t)}
thus {a} -- {s,t} = {a} ++ {(- s),(- t)} by Th20
.= {(a - s),(a - t)} by Th52 ; ::_thesis: verum
end;
theorem :: MEMBER_1:77
for a, b, s being complex number holds {a,b} -- {s} = {(a - s),(b - s)}
proof
let a, b, s be complex number ; ::_thesis: {a,b} -- {s} = {(a - s),(b - s)}
thus {a,b} -- {s} = {a,b} ++ {(- s)} by Th19
.= {(a - s),(b - s)} by Th52 ; ::_thesis: verum
end;
theorem :: MEMBER_1:78
for a, b, s, t being complex number holds {a,b} -- {s,t} = {(a - s),(a - t),(b - s),(b - t)}
proof
let a, b, s, t be complex number ; ::_thesis: {a,b} -- {s,t} = {(a - s),(a - t),(b - s),(b - t)}
thus {a,b} -- {s,t} = {a,b} ++ {(- s),(- t)} by Th20
.= {(a - s),(a - t),(b - s),(b - t)} by Th53 ; ::_thesis: verum
end;
definition
let F, G be ext-real-membered set ;
funcF ** G -> set equals :: MEMBER_1:def 9
{ (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ;
coherence
{ (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } is set ;
commutativity
for b1 being set
for F, G being ext-real-membered set st b1 = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds
b1 = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }
proof
let X be set ; ::_thesis: for F, G being ext-real-membered set st X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } holds
X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }
let F, G be ext-real-membered set ; ::_thesis: ( X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } implies X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } )
assume A1: X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; ::_thesis: X = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }
thus X c= { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } :: according to XBOOLE_0:def_10 ::_thesis: { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } )
assume e in X ; ::_thesis: e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) }
then ex w1, w2 being Element of ExtREAL st
( e = w1 * w2 & w1 in F & w2 in G ) by A1;
hence e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } or e in X )
assume e in { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in G & w2 in F ) } ; ::_thesis: e in X
then ex w1, w2 being Element of ExtREAL st
( e = w1 * w2 & w1 in G & w2 in F ) ;
hence e in X by A1; ::_thesis: verum
end;
end;
:: deftheorem defines ** MEMBER_1:def_9_:_
for F, G being ext-real-membered set holds F ** G = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ;
registration
let F be empty set ;
let G be ext-real-membered set ;
clusterF ** G -> empty ;
coherence
F ** G is empty
proof
assume not F ** G is empty ; ::_thesis: contradiction
then the Element of F ** G in F ** G ;
then ex w1, w2 being Element of ExtREAL st
( the Element of F ** G = w1 * w2 & w1 in F & w2 in G ) ;
hence contradiction ; ::_thesis: verum
end;
clusterG ** F -> empty ;
coherence
G ** F is empty ;
end;
registration
let F, G be ext-real-membered set ;
clusterF ** G -> ext-real-membered ;
coherence
F ** G is ext-real-membered
proof
let e be set ; :: according to MEMBERED:def_2 ::_thesis: ( not e in F ** G or e is ext-real )
assume e in F ** G ; ::_thesis: e is ext-real
then ex w1, w2 being Element of ExtREAL st
( e = w1 * w2 & w1 in F & w2 in G ) ;
hence e is ext-real ; ::_thesis: verum
end;
end;
theorem Th79: :: MEMBER_1:79
for F, G being ext-real-membered set
for f, g being ext-real number st f in F & g in G holds
f * g in F ** G
proof
let F, G be ext-real-membered set ; ::_thesis: for f, g being ext-real number st f in F & g in G holds
f * g in F ** G
let f, g be ext-real number ; ::_thesis: ( f in F & g in G implies f * g in F ** G )
( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1;
hence ( f in F & g in G implies f * g in F ** G ) ; ::_thesis: verum
end;
registration
let F, G be non empty ext-real-membered set ;
clusterF ** G -> non empty ;
coherence
not F ** G is empty
proof
the Element of F * the Element of G in F ** G by Th79;
hence not F ** G is empty ; ::_thesis: verum
end;
end;
theorem Th80: :: MEMBER_1:80
for F, G, H being ext-real-membered set holds (F ** G) ** H = F ** (G ** H)
proof
let F, G, H be ext-real-membered set ; ::_thesis: (F ** G) ** H = F ** (G ** H)
let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in (F ** G) ** H or i in F ** (G ** H) ) & ( not i in F ** (G ** H) or i in (F ** G) ** H ) )
hereby ::_thesis: ( not i in F ** (G ** H) or i in (F ** G) ** H )
assume i in (F ** G) ** H ; ::_thesis: i in F ** (G ** H)
then consider w, w1 being Element of ExtREAL such that
A1: i = w * w1 and
A2: w in F ** G and
A3: w1 in H ;
consider w2, w3 being Element of ExtREAL such that
A4: w = w2 * w3 and
A5: w2 in F and
A6: w3 in G by A2;
( i = w2 * (w3 * w1) & w3 * w1 in G ** H ) by A1, A3, A4, A6, XXREAL_3:66;
hence i in F ** (G ** H) by A5; ::_thesis: verum
end;
assume i in F ** (G ** H) ; ::_thesis: i in (F ** G) ** H
then consider w, w1 being Element of ExtREAL such that
A7: ( i = w * w1 & w in F ) and
A8: w1 in G ** H ;
consider w2, w3 being Element of ExtREAL such that
A9: ( w1 = w2 * w3 & w2 in G ) and
A10: w3 in H by A8;
( i = (w * w2) * w3 & w * w2 in F ** G ) by A7, A9, XXREAL_3:66;
hence i in (F ** G) ** H by A10; ::_thesis: verum
end;
theorem Th81: :: MEMBER_1:81
for F, G, H, I being ext-real-membered set st F c= G & H c= I holds
F ** H c= G ** I
proof
let F, G, H, I be ext-real-membered set ; ::_thesis: ( F c= G & H c= I implies F ** H c= G ** I )
assume A1: ( F c= G & H c= I ) ; ::_thesis: F ** H c= G ** I
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F ** H or i in G ** I )
assume i in F ** H ; ::_thesis: i in G ** I
then ex w, w1 being Element of ExtREAL st
( i = w * w1 & w in F & w1 in H ) ;
hence i in G ** I by A1; ::_thesis: verum
end;
theorem Th82: :: MEMBER_1:82
for F, G, H being ext-real-membered set holds F ** (G \/ H) = (F ** G) \/ (F ** H)
proof
let F, G, H be ext-real-membered set ; ::_thesis: F ** (G \/ H) = (F ** G) \/ (F ** H)
let j be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not j in F ** (G \/ H) or j in (F ** G) \/ (F ** H) ) & ( not j in (F ** G) \/ (F ** H) or j in F ** (G \/ H) ) )
hereby ::_thesis: ( not j in (F ** G) \/ (F ** H) or j in F ** (G \/ H) )
assume j in F ** (G \/ H) ; ::_thesis: j in (F ** G) \/ (F ** H)
then consider w, w1 being Element of ExtREAL such that
A1: j = w * w1 and
A2: w in F and
A3: w1 in G \/ H ;
( w1 in G or w1 in H ) by A3, XBOOLE_0:def_3;
then ( w * w1 in F ** G or w * w1 in F ** H ) by A2;
hence j in (F ** G) \/ (F ** H) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A4: j in (F ** G) \/ (F ** H) ; ::_thesis: j in F ** (G \/ H)
percases ( j in F ** G or j in F ** H ) by A4, XBOOLE_0:def_3;
suppose j in F ** G ; ::_thesis: j in F ** (G \/ H)
then consider w, w1 being Element of ExtREAL such that
A5: ( j = w * w1 & w in F ) and
A6: w1 in G ;
w1 in G \/ H by A6, XBOOLE_0:def_3;
hence j in F ** (G \/ H) by A5; ::_thesis: verum
end;
suppose j in F ** H ; ::_thesis: j in F ** (G \/ H)
then consider w, w1 being Element of ExtREAL such that
A7: ( j = w * w1 & w in F ) and
A8: w1 in H ;
w1 in G \/ H by A8, XBOOLE_0:def_3;
hence j in F ** (G \/ H) by A7; ::_thesis: verum
end;
end;
end;
theorem Th83: :: MEMBER_1:83
for F, G, H being ext-real-membered set holds F ** (G /\ H) c= (F ** G) /\ (F ** H)
proof
let F, G, H be ext-real-membered set ; ::_thesis: F ** (G /\ H) c= (F ** G) /\ (F ** H)
let j be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not j in F ** (G /\ H) or j in (F ** G) /\ (F ** H) )
assume j in F ** (G /\ H) ; ::_thesis: j in (F ** G) /\ (F ** H)
then consider w, w1 being Element of ExtREAL such that
A1: j = w * w1 and
A2: w in F and
A3: w1 in G /\ H ;
w1 in H by A3, XBOOLE_0:def_4;
then A4: w * w1 in F ** H by A2;
w1 in G by A3, XBOOLE_0:def_4;
then w * w1 in F ** G by A2;
hence j in (F ** G) /\ (F ** H) by A1, A4, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: MEMBER_1:84
for F, G being ext-real-membered set holds F ** (-- G) = -- (F ** G)
proof
let F, G be ext-real-membered set ; ::_thesis: F ** (-- G) = -- (F ** G)
let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in F ** (-- G) or i in -- (F ** G) ) & ( not i in -- (F ** G) or i in F ** (-- G) ) )
hereby ::_thesis: ( not i in -- (F ** G) or i in F ** (-- G) )
assume i in F ** (-- G) ; ::_thesis: i in -- (F ** G)
then consider w, w1 being Element of ExtREAL such that
A1: i = w * w1 and
A2: w in F and
A3: w1 in -- G ;
w * (- w1) = - (w * w1) by XXREAL_3:92;
then A4: i = - (w * (- w1)) by A1;
- w1 in G by A3, Th2;
then w * (- w1) in F ** G by A2;
hence i in -- (F ** G) by A4; ::_thesis: verum
end;
assume i in -- (F ** G) ; ::_thesis: i in F ** (-- G)
then - i in F ** G by Th2;
then consider w, w1 being Element of ExtREAL such that
A5: ( - i = w * w1 & w in F ) and
A6: w1 in G ;
( w * (- w1) = - (w * w1) & - w1 in -- G ) by A6, XXREAL_3:92;
hence i in F ** (-- G) by A5; ::_thesis: verum
end;
theorem Th85: :: MEMBER_1:85
for F, G being ext-real-membered set holds (F ** G) "" = (F "") ** (G "")
proof
let F, G be ext-real-membered set ; ::_thesis: (F ** G) "" = (F "") ** (G "")
let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in (F ** G) "" or i in (F "") ** (G "") ) & ( not i in (F "") ** (G "") or i in (F ** G) "" ) )
hereby ::_thesis: ( not i in (F "") ** (G "") or i in (F ** G) "" )
assume i in (F ** G) "" ; ::_thesis: i in (F "") ** (G "")
then consider w being Element of ExtREAL such that
A1: i = w " and
A2: w in F ** G ;
consider w1, w2 being Element of ExtREAL such that
A3: w = w1 * w2 and
A4: ( w1 in F & w2 in G ) by A2;
A5: ( w1 " in F "" & w2 " in G "" ) by A4;
i = (w1 ") * (w2 ") by A1, A3, XXREAL_3:67;
hence i in (F "") ** (G "") by A5; ::_thesis: verum
end;
assume i in (F "") ** (G "") ; ::_thesis: i in (F ** G) ""
then consider w, w1 being Element of ExtREAL such that
A6: i = w * w1 and
A7: w in F "" and
A8: w1 in G "" ;
consider w3 being Element of ExtREAL such that
A9: w1 = w3 " and
A10: w3 in G by A8;
consider w2 being Element of ExtREAL such that
A11: w = w2 " and
A12: w2 in F by A7;
A13: w2 * w3 in F ** G by A12, A10;
i = (w2 * w3) " by A6, A11, A9, XXREAL_3:67;
hence i in (F ** G) "" by A13; ::_thesis: verum
end;
theorem Th86: :: MEMBER_1:86
for f, g being ext-real number holds {f} ** {g} = {(f * g)}
proof
let f, g be ext-real number ; ::_thesis: {f} ** {g} = {(f * g)}
let i be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not i in {f} ** {g} or i in {(f * g)} ) & ( not i in {(f * g)} or i in {f} ** {g} ) )
hereby ::_thesis: ( not i in {(f * g)} or i in {f} ** {g} )
assume i in {f} ** {g} ; ::_thesis: i in {(f * g)}
then consider w1, w2 being Element of ExtREAL such that
A1: i = w1 * w2 and
A2: ( w1 in {f} & w2 in {g} ) ;
( w1 = f & w2 = g ) by A2, TARSKI:def_1;
hence i in {(f * g)} by A1, TARSKI:def_1; ::_thesis: verum
end;
A3: ( f in {f} & g in {g} ) by TARSKI:def_1;
assume i in {(f * g)} ; ::_thesis: i in {f} ** {g}
then A4: i = f * g by TARSKI:def_1;
( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1;
hence i in {f} ** {g} by A4, A3; ::_thesis: verum
end;
theorem Th87: :: MEMBER_1:87
for f, h, i being ext-real number holds {f} ** {h,i} = {(f * h),(f * i)}
proof
let f, h, i be ext-real number ; ::_thesis: {f} ** {h,i} = {(f * h),(f * i)}
thus {f} ** {h,i} = {f} ** ({h} \/ {i}) by ENUMSET1:1
.= ({f} ** {h}) \/ ({f} ** {i}) by Th82
.= {(f * h)} \/ ({f} ** {i}) by Th86
.= {(f * h)} \/ {(f * i)} by Th86
.= {(f * h),(f * i)} by ENUMSET1:1 ; ::_thesis: verum
end;
theorem Th88: :: MEMBER_1:88
for f, g, h, i being ext-real number holds {f,g} ** {h,i} = {(f * h),(f * i),(g * h),(g * i)}
proof
let f, g, h, i be ext-real number ; ::_thesis: {f,g} ** {h,i} = {(f * h),(f * i),(g * h),(g * i)}
thus {f,g} ** {h,i} = ({f} \/ {g}) ** {h,i} by ENUMSET1:1
.= ({f} ** {h,i}) \/ ({g} ** {h,i}) by Th82
.= {(f * h),(f * i)} \/ ({g} ** {h,i}) by Th87
.= {(f * h),(f * i)} \/ {(g * h),(g * i)} by Th87
.= {(f * h),(f * i),(g * h),(g * i)} by ENUMSET1:5 ; ::_thesis: verum
end;
definition
let A, B be complex-membered set ;
funcA ** B -> set equals :: MEMBER_1:def 10
{ (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ;
coherence
{ (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } is set ;
commutativity
for b1 being set
for A, B being complex-membered set st b1 = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } holds
b1 = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) }
proof
let X be set ; ::_thesis: for A, B being complex-membered set st X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } holds
X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) }
let A, B be complex-membered set ; ::_thesis: ( X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } implies X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } )
assume A1: X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; ::_thesis: X = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) }
thus X c= { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } :: according to XBOOLE_0:def_10 ::_thesis: { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } )
assume e in X ; ::_thesis: e in { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) }
then ex c1, c2 being Element of COMPLEX st
( e = c1 * c2 & c1 in A & c2 in B ) by A1;
hence e in { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } or e in X )
assume e in { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in B & c2 in A ) } ; ::_thesis: e in X
then ex c1, c2 being Element of COMPLEX st
( e = c1 * c2 & c1 in B & c2 in A ) ;
hence e in X by A1; ::_thesis: verum
end;
end;
:: deftheorem defines ** MEMBER_1:def_10_:_
for A, B being complex-membered set holds A ** B = { (c1 * c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ;
theorem Th89: :: MEMBER_1:89
for A, B being complex-membered set
for a, b being complex number st a in A & b in B holds
a * b in A ** B
proof
let A, B be complex-membered set ; ::_thesis: for a, b being complex number st a in A & b in B holds
a * b in A ** B
let a, b be complex number ; ::_thesis: ( a in A & b in B implies a * b in A ** B )
( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2;
hence ( a in A & b in B implies a * b in A ** B ) ; ::_thesis: verum
end;
registration
let A be empty set ;
let B be complex-membered set ;
clusterA ** B -> empty ;
coherence
A ** B is empty
proof
assume not A ** B is empty ; ::_thesis: contradiction
then the Element of A ** B in A ** B ;
then ex c1, c2 being Element of COMPLEX st
( the Element of A ** B = c1 * c2 & c1 in A & c2 in B ) ;
hence contradiction ; ::_thesis: verum
end;
clusterB ** A -> empty ;
coherence
B ** A is empty ;
end;
registration
let A, B be non empty complex-membered set ;
clusterA ** B -> non empty ;
coherence
not A ** B is empty
proof
the Element of A * the Element of B in A ** B by Th89;
hence not A ** B is empty ; ::_thesis: verum
end;
end;
registration
let A, B be complex-membered set ;
clusterA ** B -> complex-membered ;
coherence
A ** B is complex-membered
proof
let e be set ; :: according to MEMBERED:def_1 ::_thesis: ( not e in A ** B or e is complex )
assume e in A ** B ; ::_thesis: e is complex
then ex c1, c2 being Element of COMPLEX st
( e = c1 * c2 & c1 in A & c2 in B ) ;
hence e is complex ; ::_thesis: verum
end;
end;
registration
let A, B be real-membered set ;
clusterA ** B -> real-membered ;
coherence
A ** B is real-membered
proof
let e be set ; :: according to MEMBERED:def_3 ::_thesis: ( not e in A ** B or e is real )
assume e in A ** B ; ::_thesis: e is real
then ex c1, c2 being Element of COMPLEX st
( e = c1 * c2 & c1 in A & c2 in B ) ;
hence e is real ; ::_thesis: verum
end;
end;
registration
let A, B be rational-membered set ;
clusterA ** B -> rational-membered ;
coherence
A ** B is rational-membered
proof
let e be set ; :: according to MEMBERED:def_4 ::_thesis: ( not e in A ** B or e is rational )
assume e in A ** B ; ::_thesis: e is rational
then ex c1, c2 being Element of COMPLEX st
( e = c1 * c2 & c1 in A & c2 in B ) ;
hence e is rational ; ::_thesis: verum
end;
end;
registration
let A, B be integer-membered set ;
clusterA ** B -> integer-membered ;
coherence
A ** B is integer-membered
proof
let e be set ; :: according to MEMBERED:def_5 ::_thesis: ( not e in A ** B or e is integer )
assume e in A ** B ; ::_thesis: e is integer
then ex c1, c2 being Element of COMPLEX st
( e = c1 * c2 & c1 in A & c2 in B ) ;
hence e is integer ; ::_thesis: verum
end;
end;
registration
let A, B be natural-membered set ;
clusterA ** B -> natural-membered ;
coherence
A ** B is natural-membered
proof
let e be set ; :: according to MEMBERED:def_6 ::_thesis: ( not e in A ** B or e is natural )
assume e in A ** B ; ::_thesis: e is natural
then ex c1, c2 being Element of COMPLEX st
( e = c1 * c2 & c1 in A & c2 in B ) ;
hence e is natural ; ::_thesis: verum
end;
end;
registration
let A, B be real-membered set ;
let F, G be ext-real-membered set ;
identifyA ** B with F ** G when A = F, B = G;
compatibility
( A = F & B = G implies A ** B = F ** G )
proof
assume A1: ( A = F & B = G ) ; ::_thesis: A ** B = F ** G
let a be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not a in A ** B or a in F ** G ) & ( not a in F ** G or a in A ** B ) )
hereby ::_thesis: ( not a in F ** G or a in A ** B )
assume a in A ** B ; ::_thesis: a in F ** G
then consider c, c1 being Element of COMPLEX such that
A2: a = c * c1 and
A3: ( c in A & c1 in B ) ;
reconsider d1 = c, d2 = c1 as Element of ExtREAL by A3, XXREAL_0:def_1;
a = d1 * d2 by A2, A3, XXREAL_3:def_5;
hence a in F ** G by A1, A3; ::_thesis: verum
end;
assume a in F ** G ; ::_thesis: a in A ** B
then consider w, w1 being Element of ExtREAL such that
A4: a = w * w1 and
A5: ( w in F & w1 in G ) ;
reconsider d1 = w, d2 = w1 as Element of COMPLEX by A1, A5, XCMPLX_0:def_2;
a = d1 * d2 by A1, A4, A5, XXREAL_3:def_5;
hence a in A ** B by A1, A5; ::_thesis: verum
end;
end;
theorem Th90: :: MEMBER_1:90
for A, B, C being complex-membered set holds (A ** B) ** C = A ** (B ** C)
proof
let A, B, C be complex-membered set ; ::_thesis: (A ** B) ** C = A ** (B ** C)
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A ** B) ** C or a in A ** (B ** C) ) & ( not a in A ** (B ** C) or a in (A ** B) ** C ) )
hereby ::_thesis: ( not a in A ** (B ** C) or a in (A ** B) ** C )
assume a in (A ** B) ** C ; ::_thesis: a in A ** (B ** C)
then consider c, c1 being Element of COMPLEX such that
A1: a = c * c1 and
A2: c in A ** B and
A3: c1 in C ;
consider c2, c3 being Element of COMPLEX such that
A4: c = c2 * c3 and
A5: c2 in A and
A6: c3 in B by A2;
( a = c2 * (c3 * c1) & c3 * c1 in B ** C ) by A1, A3, A4, A6;
hence a in A ** (B ** C) by A5; ::_thesis: verum
end;
assume a in A ** (B ** C) ; ::_thesis: a in (A ** B) ** C
then consider c, c1 being Element of COMPLEX such that
A7: ( a = c * c1 & c in A ) and
A8: c1 in B ** C ;
consider c2, c3 being Element of COMPLEX such that
A9: ( c1 = c2 * c3 & c2 in B ) and
A10: c3 in C by A8;
( a = (c * c2) * c3 & c * c2 in A ** B ) by A7, A9;
hence a in (A ** B) ** C by A10; ::_thesis: verum
end;
theorem :: MEMBER_1:91
for A, B, C, D being complex-membered set st A c= B & C c= D holds
A ** C c= B ** D
proof
let A, B, C, D be complex-membered set ; ::_thesis: ( A c= B & C c= D implies A ** C c= B ** D )
assume A1: ( A c= B & C c= D ) ; ::_thesis: A ** C c= B ** D
let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A ** C or a in B ** D )
assume a in A ** C ; ::_thesis: a in B ** D
then ex c, c1 being Element of COMPLEX st
( a = c * c1 & c in A & c1 in C ) ;
hence a in B ** D by A1; ::_thesis: verum
end;
theorem Th92: :: MEMBER_1:92
for A, B, C being complex-membered set holds A ** (B \/ C) = (A ** B) \/ (A ** C)
proof
let A, B, C be complex-membered set ; ::_thesis: A ** (B \/ C) = (A ** B) \/ (A ** C)
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in A ** (B \/ C) or a in (A ** B) \/ (A ** C) ) & ( not a in (A ** B) \/ (A ** C) or a in A ** (B \/ C) ) )
hereby ::_thesis: ( not a in (A ** B) \/ (A ** C) or a in A ** (B \/ C) )
assume a in A ** (B \/ C) ; ::_thesis: a in (A ** B) \/ (A ** C)
then consider c, c1 being Element of COMPLEX such that
A1: a = c * c1 and
A2: c in A and
A3: c1 in B \/ C ;
( c1 in B or c1 in C ) by A3, XBOOLE_0:def_3;
then ( c * c1 in A ** B or c * c1 in A ** C ) by A2;
hence a in (A ** B) \/ (A ** C) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A4: a in (A ** B) \/ (A ** C) ; ::_thesis: a in A ** (B \/ C)
percases ( a in A ** B or a in A ** C ) by A4, XBOOLE_0:def_3;
suppose a in A ** B ; ::_thesis: a in A ** (B \/ C)
then consider c, c1 being Element of COMPLEX such that
A5: ( a = c * c1 & c in A ) and
A6: c1 in B ;
c1 in B \/ C by A6, XBOOLE_0:def_3;
hence a in A ** (B \/ C) by A5; ::_thesis: verum
end;
suppose a in A ** C ; ::_thesis: a in A ** (B \/ C)
then consider c, c1 being Element of COMPLEX such that
A7: ( a = c * c1 & c in A ) and
A8: c1 in C ;
c1 in B \/ C by A8, XBOOLE_0:def_3;
hence a in A ** (B \/ C) by A7; ::_thesis: verum
end;
end;
end;
theorem Th93: :: MEMBER_1:93
for A, B, C being complex-membered set holds A ** (B /\ C) c= (A ** B) /\ (A ** C)
proof
let A, B, C be complex-membered set ; ::_thesis: A ** (B /\ C) c= (A ** B) /\ (A ** C)
let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A ** (B /\ C) or a in (A ** B) /\ (A ** C) )
assume a in A ** (B /\ C) ; ::_thesis: a in (A ** B) /\ (A ** C)
then consider c, c1 being Element of COMPLEX such that
A1: a = c * c1 and
A2: c in A and
A3: c1 in B /\ C ;
c1 in C by A3, XBOOLE_0:def_4;
then A4: c * c1 in A ** C by A2;
c1 in B by A3, XBOOLE_0:def_4;
then c * c1 in A ** B by A2;
hence a in (A ** B) /\ (A ** C) by A1, A4, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th94: :: MEMBER_1:94
for A, B being complex-membered set holds A ** (-- B) = -- (A ** B)
proof
let A, B be complex-membered set ; ::_thesis: A ** (-- B) = -- (A ** B)
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in A ** (-- B) or a in -- (A ** B) ) & ( not a in -- (A ** B) or a in A ** (-- B) ) )
hereby ::_thesis: ( not a in -- (A ** B) or a in A ** (-- B) )
assume a in A ** (-- B) ; ::_thesis: a in -- (A ** B)
then consider c, c1 being Element of COMPLEX such that
A1: a = c * c1 and
A2: c in A and
A3: c1 in -- B ;
- c1 in B by A3, Th12;
then A4: c * (- c1) in A ** B by A2;
a = - (c * (- c1)) by A1;
hence a in -- (A ** B) by A4; ::_thesis: verum
end;
assume a in -- (A ** B) ; ::_thesis: a in A ** (-- B)
then - a in A ** B by Th12;
then consider c, c1 being Element of COMPLEX such that
A5: - a = c * c1 and
A6: c in A and
A7: c1 in B ;
( a = c * (- c1) & - c1 in -- B ) by A5, A7;
hence a in A ** (-- B) by A6; ::_thesis: verum
end;
theorem Th95: :: MEMBER_1:95
for A, B, C being complex-membered set holds A ** (B ++ C) c= (A ** B) ++ (A ** C)
proof
let A, B, C be complex-membered set ; ::_thesis: A ** (B ++ C) c= (A ** B) ++ (A ** C)
let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in A ** (B ++ C) or a in (A ** B) ++ (A ** C) )
assume a in A ** (B ++ C) ; ::_thesis: a in (A ** B) ++ (A ** C)
then consider c, c1 being Element of COMPLEX such that
A1: a = c * c1 and
A2: c in A and
A3: c1 in B ++ C ;
consider c2, c3 being Element of COMPLEX such that
A4: ( c1 = c2 + c3 & c2 in B ) and
A5: c3 in C by A3;
A6: c * c3 in A ** C by A2, A5;
( a = (c * c2) + (c * c3) & c * c2 in A ** B ) by A1, A2, A4;
hence a in (A ** B) ++ (A ** C) by A6; ::_thesis: verum
end;
theorem Th96: :: MEMBER_1:96
for A, B, C being complex-membered set holds A ** (B -- C) c= (A ** B) -- (A ** C)
proof
let A, B, C be complex-membered set ; ::_thesis: A ** (B -- C) c= (A ** B) -- (A ** C)
A ** (B ++ (-- C)) c= (A ** B) ++ (A ** (-- C)) by Th95;
hence A ** (B -- C) c= (A ** B) -- (A ** C) by Th94; ::_thesis: verum
end;
theorem Th97: :: MEMBER_1:97
for A, B being complex-membered set holds (A ** B) "" = (A "") ** (B "")
proof
let A, B be complex-membered set ; ::_thesis: (A ** B) "" = (A "") ** (B "")
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in (A ** B) "" or a in (A "") ** (B "") ) & ( not a in (A "") ** (B "") or a in (A ** B) "" ) )
hereby ::_thesis: ( not a in (A "") ** (B "") or a in (A ** B) "" )
assume a in (A ** B) "" ; ::_thesis: a in (A "") ** (B "")
then consider c being Element of COMPLEX such that
A1: a = c " and
A2: c in A ** B ;
consider c1, c2 being Element of COMPLEX such that
A3: c = c1 * c2 and
A4: ( c1 in A & c2 in B ) by A2;
A5: ( c1 " in A "" & c2 " in B "" ) by A4;
a = (c1 ") * (c2 ") by A1, A3, XCMPLX_1:204;
hence a in (A "") ** (B "") by A5; ::_thesis: verum
end;
assume a in (A "") ** (B "") ; ::_thesis: a in (A ** B) ""
then consider c, c1 being Element of COMPLEX such that
A6: a = c * c1 and
A7: c in A "" and
A8: c1 in B "" ;
consider c3 being Element of COMPLEX such that
A9: c1 = c3 " and
A10: c3 in B by A8;
consider c2 being Element of COMPLEX such that
A11: c = c2 " and
A12: c2 in A by A7;
A13: c2 * c3 in A ** B by A12, A10;
a = (c2 * c3) " by A6, A11, A9, XCMPLX_1:204;
hence a in (A ** B) "" by A13; ::_thesis: verum
end;
theorem Th98: :: MEMBER_1:98
for a, b being complex number holds {a} ** {b} = {(a * b)}
proof
let a, b be complex number ; ::_thesis: {a} ** {b} = {(a * b)}
let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in {a} ** {b} or z in {(a * b)} ) & ( not z in {(a * b)} or z in {a} ** {b} ) )
hereby ::_thesis: ( not z in {(a * b)} or z in {a} ** {b} )
assume z in {a} ** {b} ; ::_thesis: z in {(a * b)}
then consider c1, c2 being Element of COMPLEX such that
A1: z = c1 * c2 and
A2: ( c1 in {a} & c2 in {b} ) ;
( c1 = a & c2 = b ) by A2, TARSKI:def_1;
hence z in {(a * b)} by A1, TARSKI:def_1; ::_thesis: verum
end;
A3: ( a in {a} & b in {b} ) by TARSKI:def_1;
assume z in {(a * b)} ; ::_thesis: z in {a} ** {b}
then A4: z = a * b by TARSKI:def_1;
( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2;
hence z in {a} ** {b} by A4, A3; ::_thesis: verum
end;
theorem Th99: :: MEMBER_1:99
for a, s, t being complex number holds {a} ** {s,t} = {(a * s),(a * t)}
proof
let a, s, t be complex number ; ::_thesis: {a} ** {s,t} = {(a * s),(a * t)}
thus {a} ** {s,t} = {a} ** ({s} \/ {t}) by ENUMSET1:1
.= ({a} ** {s}) \/ ({a} ** {t}) by Th92
.= {(a * s)} \/ ({a} ** {t}) by Th98
.= {(a * s)} \/ {(a * t)} by Th98
.= {(a * s),(a * t)} by ENUMSET1:1 ; ::_thesis: verum
end;
theorem Th100: :: MEMBER_1:100
for a, b, s, t being complex number holds {a,b} ** {s,t} = {(a * s),(a * t),(b * s),(b * t)}
proof
let a, b, s, t be complex number ; ::_thesis: {a,b} ** {s,t} = {(a * s),(a * t),(b * s),(b * t)}
thus {a,b} ** {s,t} = ({a} \/ {b}) ** {s,t} by ENUMSET1:1
.= ({a} ** {s,t}) \/ ({b} ** {s,t}) by Th92
.= {(a * s),(a * t)} \/ ({b} ** {s,t}) by Th99
.= {(a * s),(a * t)} \/ {(b * s),(b * t)} by Th99
.= {(a * s),(a * t),(b * s),(b * t)} by ENUMSET1:5 ; ::_thesis: verum
end;
definition
let F, G be ext-real-membered set ;
funcF /// G -> set equals :: MEMBER_1:def 11
F ** (G "");
coherence
F ** (G "") is set ;
end;
:: deftheorem defines /// MEMBER_1:def_11_:_
for F, G being ext-real-membered set holds F /// G = F ** (G "");
theorem Th101: :: MEMBER_1:101
for F, G being ext-real-membered set holds F /// G = { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) }
proof
let F, G be ext-real-membered set ; ::_thesis: F /// G = { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) }
thus F /// G c= { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } :: according to XBOOLE_0:def_10 ::_thesis: { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } c= F /// G
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F /// G or e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } )
assume e in F /// G ; ::_thesis: e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) }
then consider w1, w2 being Element of ExtREAL such that
A1: e = w1 * w2 and
A2: w1 in F and
A3: w2 in G "" ;
consider w being Element of ExtREAL such that
A4: w2 = w " and
A5: w in G by A3;
e = w1 / w by A1, A4;
hence e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } by A2, A5; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } or e in F /// G )
assume e in { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ; ::_thesis: e in F /// G
then consider w1, w2 being Element of ExtREAL such that
A6: ( e = w1 / w2 & w1 in F ) and
A7: w2 in G ;
w2 " in G "" by A7;
hence e in F /// G by A6; ::_thesis: verum
end;
theorem Th102: :: MEMBER_1:102
for F, G being ext-real-membered set
for f, g being ext-real number st f in F & g in G holds
f / g in F /// G
proof
let F, G be ext-real-membered set ; ::_thesis: for f, g being ext-real number st f in F & g in G holds
f / g in F /// G
let f, g be ext-real number ; ::_thesis: ( f in F & g in G implies f / g in F /// G )
A1: ( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def_1;
F /// G = { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } by Th101;
hence ( f in F & g in G implies f / g in F /// G ) by A1; ::_thesis: verum
end;
registration
let F be empty set ;
let G be ext-real-membered set ;
clusterF /// G -> empty ;
coherence
F /// G is empty ;
clusterG /// F -> empty ;
coherence
G /// F is empty ;
end;
registration
let F, G be non empty ext-real-membered set ;
clusterF /// G -> non empty ;
coherence
not F /// G is empty ;
end;
registration
let F, G be ext-real-membered set ;
clusterF /// G -> ext-real-membered ;
coherence
F /// G is ext-real-membered ;
end;
theorem :: MEMBER_1:103
for F, G, H, I being ext-real-membered set st F c= G & H c= I holds
F /// H c= G /// I
proof
let F, G, H, I be ext-real-membered set ; ::_thesis: ( F c= G & H c= I implies F /// H c= G /// I )
assume A1: ( F c= G & H c= I ) ; ::_thesis: F /// H c= G /// I
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F /// H or i in G /// I )
A2: F /// H = { (w1 / w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in H ) } by Th101;
assume i in F /// H ; ::_thesis: i in G /// I
then ex w, w1 being Element of ExtREAL st
( i = w / w1 & w in F & w1 in H ) by A2;
hence i in G /// I by A1, Th102; ::_thesis: verum
end;
theorem :: MEMBER_1:104
for F, G, H being ext-real-membered set holds (F \/ G) /// H = (F /// H) \/ (G /// H) by Th82;
theorem :: MEMBER_1:105
for F, G, H being ext-real-membered set holds (F /\ G) /// H c= (F /// H) /\ (G /// H) by Th83;
theorem :: MEMBER_1:106
for F, G, H being ext-real-membered set holds F /// (G \/ H) = (F /// G) \/ (F /// H)
proof
let F, G, H be ext-real-membered set ; ::_thesis: F /// (G \/ H) = (F /// G) \/ (F /// H)
thus F /// (G \/ H) = F ** ((G "") \/ (H "")) by Th23
.= (F /// G) \/ (F /// H) by Th82 ; ::_thesis: verum
end;
theorem :: MEMBER_1:107
for F, G, H being ext-real-membered set holds F /// (G /\ H) c= (F /// G) /\ (F /// H)
proof
let F, G, H be ext-real-membered set ; ::_thesis: F /// (G /\ H) c= (F /// G) /\ (F /// H)
(G /\ H) "" c= (G "") /\ (H "") by Th24;
then A1: F ** ((G /\ H) "") c= F ** ((G "") /\ (H "")) by Th81;
F ** ((G "") /\ (H "")) c= (F ** (G "")) /\ (F ** (H "")) by Th83;
hence F /// (G /\ H) c= (F /// G) /\ (F /// H) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: MEMBER_1:108
for F, G, H being ext-real-membered set holds (F ** G) /// H = F ** (G /// H) by Th80;
theorem :: MEMBER_1:109
for F, G, H being ext-real-membered set holds (F /// G) ** H = (F ** H) /// G by Th80;
theorem :: MEMBER_1:110
for F, G, H being ext-real-membered set holds (F /// G) /// H = F /// (G ** H)
proof
let F, G, H be ext-real-membered set ; ::_thesis: (F /// G) /// H = F /// (G ** H)
thus (F /// G) /// H = F ** ((G "") ** (H "")) by Th80
.= F /// (G ** H) by Th85 ; ::_thesis: verum
end;
theorem :: MEMBER_1:111
for f, g being ext-real number holds {f} /// {g} = {(f / g)}
proof
let f, g be ext-real number ; ::_thesis: {f} /// {g} = {(f / g)}
thus {f} /// {g} = {f} ** {(g ")} by Th26
.= {(f / g)} by Th86 ; ::_thesis: verum
end;
theorem :: MEMBER_1:112
for f, h, i being ext-real number holds {f} /// {h,i} = {(f / h),(f / i)}
proof
let f, h, i be ext-real number ; ::_thesis: {f} /// {h,i} = {(f / h),(f / i)}
thus {f} /// {h,i} = {f} ** {(h "),(i ")} by Th27
.= {(f / h),(f / i)} by Th87 ; ::_thesis: verum
end;
theorem :: MEMBER_1:113
for f, g, h being ext-real number holds {f,g} /// {h} = {(f / h),(g / h)}
proof
let f, g, h be ext-real number ; ::_thesis: {f,g} /// {h} = {(f / h),(g / h)}
thus {f,g} /// {h} = {f,g} ** {(h ")} by Th26
.= {(f / h),(g / h)} by Th87 ; ::_thesis: verum
end;
theorem :: MEMBER_1:114
for f, g, h, i being ext-real number holds {f,g} /// {h,i} = {(f / h),(f / i),(g / h),(g / i)}
proof
let f, g, h, i be ext-real number ; ::_thesis: {f,g} /// {h,i} = {(f / h),(f / i),(g / h),(g / i)}
thus {f,g} /// {h,i} = {f,g} ** {(h "),(i ")} by Th27
.= {(f / h),(f / i),(g / h),(g / i)} by Th88 ; ::_thesis: verum
end;
definition
let A, B be complex-membered set ;
funcA /// B -> set equals :: MEMBER_1:def 12
A ** (B "");
coherence
A ** (B "") is set ;
end;
:: deftheorem defines /// MEMBER_1:def_12_:_
for A, B being complex-membered set holds A /// B = A ** (B "");
theorem Th115: :: MEMBER_1:115
for A, B being complex-membered set holds A /// B = { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) }
proof
let A, B be complex-membered set ; ::_thesis: A /// B = { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) }
thus A /// B c= { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } :: according to XBOOLE_0:def_10 ::_thesis: { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } c= A /// B
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A /// B or e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } )
assume e in A /// B ; ::_thesis: e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) }
then consider c1, c2 being Element of COMPLEX such that
A1: e = c1 * c2 and
A2: c1 in A and
A3: c2 in B "" ;
( e = c1 / (c2 ") & c2 " in B ) by A1, A3, Th29;
hence e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } by A2; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } or e in A /// B )
assume e in { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } ; ::_thesis: e in A /// B
then consider c1, c2 being Element of COMPLEX such that
A4: ( e = c1 / c2 & c1 in A ) and
A5: c2 in B ;
c2 " in B "" by A5;
hence e in A /// B by A4; ::_thesis: verum
end;
theorem Th116: :: MEMBER_1:116
for A, B being complex-membered set
for a, b being complex number st a in A & b in B holds
a / b in A /// B
proof
let A, B be complex-membered set ; ::_thesis: for a, b being complex number st a in A & b in B holds
a / b in A /// B
let a, b be complex number ; ::_thesis: ( a in A & b in B implies a / b in A /// B )
A1: ( a in COMPLEX & b in COMPLEX ) by XCMPLX_0:def_2;
A /// B = { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in B ) } by Th115;
hence ( a in A & b in B implies a / b in A /// B ) by A1; ::_thesis: verum
end;
registration
let A be empty set ;
let B be complex-membered set ;
clusterA /// B -> empty ;
coherence
A /// B is empty ;
clusterB /// A -> empty ;
coherence
B /// A is empty ;
end;
registration
let A, B be non empty complex-membered set ;
clusterA /// B -> non empty ;
coherence
not A /// B is empty ;
end;
registration
let A, B be complex-membered set ;
clusterA /// B -> complex-membered ;
coherence
A /// B is complex-membered ;
end;
registration
let A, B be real-membered set ;
clusterA /// B -> real-membered ;
coherence
A /// B is real-membered ;
end;
registration
let A, B be rational-membered set ;
clusterA /// B -> rational-membered ;
coherence
A /// B is rational-membered ;
end;
registration
let A, B be real-membered set ;
let F, G be ext-real-membered set ;
identifyA /// B with F /// G when A = F, B = G;
compatibility
( A = F & B = G implies A /// B = F /// G ) ;
end;
theorem :: MEMBER_1:117
for A, B, C, D being complex-membered set st A c= B & C c= D holds
A /// C c= B /// D
proof
let A, B, C, D be complex-membered set ; ::_thesis: ( A c= B & C c= D implies A /// C c= B /// D )
assume A1: ( A c= B & C c= D ) ; ::_thesis: A /// C c= B /// D
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A /// C or z in B /// D )
A2: A /// C = { (c1 / c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in C ) } by Th115;
assume z in A /// C ; ::_thesis: z in B /// D
then ex c, c1 being Element of COMPLEX st
( z = c / c1 & c in A & c1 in C ) by A2;
hence z in B /// D by A1, Th116; ::_thesis: verum
end;
theorem :: MEMBER_1:118
for A, B, C being complex-membered set holds A /// (B \/ C) = (A /// B) \/ (A /// C)
proof
let A, B, C be complex-membered set ; ::_thesis: A /// (B \/ C) = (A /// B) \/ (A /// C)
thus A /// (B \/ C) = A ** ((B "") \/ (C "")) by Th32
.= (A /// B) \/ (A /// C) by Th92 ; ::_thesis: verum
end;
theorem :: MEMBER_1:119
for A, B, C being complex-membered set holds A /// (B /\ C) c= (A /// B) /\ (A /// C)
proof
let A, B, C be complex-membered set ; ::_thesis: A /// (B /\ C) c= (A /// B) /\ (A /// C)
A /// (B /\ C) = A ** ((B "") /\ (C "")) by Th33;
hence A /// (B /\ C) c= (A /// B) /\ (A /// C) by Th93; ::_thesis: verum
end;
theorem :: MEMBER_1:120
for A, B being complex-membered set holds A /// (-- B) = -- (A /// B)
proof
let A, B be complex-membered set ; ::_thesis: A /// (-- B) = -- (A /// B)
thus A /// (-- B) = A ** (-- (B "")) by Th36
.= -- (A /// B) by Th94 ; ::_thesis: verum
end;
theorem :: MEMBER_1:121
for A, B being complex-membered set holds (-- A) /// B = -- (A /// B) by Th94;
theorem :: MEMBER_1:122
for A, B, C being complex-membered set holds (A ++ B) /// C c= (A /// C) ++ (B /// C) by Th95;
theorem :: MEMBER_1:123
for A, B, C being complex-membered set holds (A -- B) /// C c= (A /// C) -- (B /// C)
proof
let A, B, C be complex-membered set ; ::_thesis: (A -- B) /// C c= (A /// C) -- (B /// C)
(A ++ (-- B)) /// C c= (A /// C) ++ ((-- B) /// C) by Th95;
hence (A -- B) /// C c= (A /// C) -- (B /// C) by Th94; ::_thesis: verum
end;
theorem :: MEMBER_1:124
for A, B, C being complex-membered set holds (A ** B) /// C = A ** (B /// C) by Th90;
theorem :: MEMBER_1:125
for A, B, C being complex-membered set holds (A /// B) ** C = (A ** C) /// B by Th90;
theorem :: MEMBER_1:126
for A, B, C being complex-membered set holds (A /// B) /// C = A /// (B ** C)
proof
let A, B, C be complex-membered set ; ::_thesis: (A /// B) /// C = A /// (B ** C)
thus (A /// B) /// C = A ** ((B "") ** (C "")) by Th90
.= A /// (B ** C) by Th97 ; ::_thesis: verum
end;
theorem :: MEMBER_1:127
for A, B, C being complex-membered set holds A /// (B /// C) = (A ** C) /// B
proof
let A, B, C be complex-membered set ; ::_thesis: A /// (B /// C) = (A ** C) /// B
thus A /// (B /// C) = A ** ((B "") ** ((C "") "")) by Th97
.= (A ** C) /// B by Th90 ; ::_thesis: verum
end;
theorem :: MEMBER_1:128
for a, b being complex number holds {a} /// {b} = {(a / b)}
proof
let a, b be complex number ; ::_thesis: {a} /// {b} = {(a / b)}
thus {a} /// {b} = {a} ** {(b ")} by Th37
.= {(a / b)} by Th98 ; ::_thesis: verum
end;
theorem :: MEMBER_1:129
for a, s, t being complex number holds {a} /// {s,t} = {(a / s),(a / t)}
proof
let a, s, t be complex number ; ::_thesis: {a} /// {s,t} = {(a / s),(a / t)}
thus {a} /// {s,t} = {a} ** {(s "),(t ")} by Th38
.= {(a / s),(a / t)} by Th99 ; ::_thesis: verum
end;
theorem :: MEMBER_1:130
for a, b, s being complex number holds {a,b} /// {s} = {(a / s),(b / s)}
proof
let a, b, s be complex number ; ::_thesis: {a,b} /// {s} = {(a / s),(b / s)}
thus {a,b} /// {s} = {a,b} ** {(s ")} by Th37
.= {(a / s),(b / s)} by Th99 ; ::_thesis: verum
end;
theorem :: MEMBER_1:131
for a, b, s, t being complex number holds {a,b} /// {s,t} = {(a / s),(a / t),(b / s),(b / t)}
proof
let a, b, s, t be complex number ; ::_thesis: {a,b} /// {s,t} = {(a / s),(a / t),(b / s),(b / t)}
thus {a,b} /// {s,t} = {a,b} ** {(s "),(t ")} by Th38
.= {(a / s),(a / t),(b / s),(b / t)} by Th100 ; ::_thesis: verum
end;
definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcf ++ F -> set equals :: MEMBER_1:def 13
{f} ++ F;
coherence
{f} ++ F is set ;
end;
:: deftheorem defines ++ MEMBER_1:def_13_:_
for F being ext-real-membered set
for f being ext-real number holds f ++ F = {f} ++ F;
theorem Th132: :: MEMBER_1:132
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
f + g in f ++ G
proof
let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds
f + g in f ++ G
let g, f be ext-real number ; ::_thesis: ( g in G implies f + g in f ++ G )
f in {f} by TARSKI:def_1;
hence ( g in G implies f + g in f ++ G ) by Th39; ::_thesis: verum
end;
theorem Th133: :: MEMBER_1:133
for F being ext-real-membered set
for f being ext-real number holds f ++ F = { (f + w) where w is Element of ExtREAL : w in F }
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds f ++ F = { (f + w) where w is Element of ExtREAL : w in F }
let f be ext-real number ; ::_thesis: f ++ F = { (f + w) where w is Element of ExtREAL : w in F }
thus f ++ F c= { (f + w) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f + w) where w is Element of ExtREAL : w in F } c= f ++ F
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f ++ F or e in { (f + w) where w is Element of ExtREAL : w in F } )
assume e in f ++ F ; ::_thesis: e in { (f + w) where w is Element of ExtREAL : w in F }
then consider w1, w2 being Element of ExtREAL such that
A1: e = w1 + w2 and
A2: w1 in {f} and
A3: w2 in F ;
w1 = f by A2, TARSKI:def_1;
hence e in { (f + w) where w is Element of ExtREAL : w in F } by A1, A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (f + w) where w is Element of ExtREAL : w in F } or e in f ++ F )
assume e in { (f + w) where w is Element of ExtREAL : w in F } ; ::_thesis: e in f ++ F
then ex w being Element of ExtREAL st
( e = f + w & w in F ) ;
hence e in f ++ F by Th132; ::_thesis: verum
end;
theorem Th134: :: MEMBER_1:134
for F being ext-real-membered set
for f being ext-real number
for e being set st e in f ++ F holds
ex w being Element of ExtREAL st
( e = f + w & w in F )
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number
for e being set st e in f ++ F holds
ex w being Element of ExtREAL st
( e = f + w & w in F )
let f be ext-real number ; ::_thesis: for e being set st e in f ++ F holds
ex w being Element of ExtREAL st
( e = f + w & w in F )
let e be set ; ::_thesis: ( e in f ++ F implies ex w being Element of ExtREAL st
( e = f + w & w in F ) )
f ++ F = { (f + w) where w is Element of ExtREAL : w in F } by Th133;
hence ( e in f ++ F implies ex w being Element of ExtREAL st
( e = f + w & w in F ) ) ; ::_thesis: verum
end;
registration
let F be empty set ;
let f be ext-real number ;
clusterf ++ F -> empty ;
coherence
f ++ F is empty ;
end;
registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterf ++ F -> non empty ;
coherence
not f ++ F is empty ;
end;
registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterf ++ F -> ext-real-membered ;
coherence
f ++ F is ext-real-membered ;
end;
theorem Th135: :: MEMBER_1:135
for F, G being ext-real-membered set
for r being real number st r ++ F c= r ++ G holds
F c= G
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number st r ++ F c= r ++ G holds
F c= G
let r be real number ; ::_thesis: ( r ++ F c= r ++ G implies F c= G )
assume A1: r ++ F c= r ++ G ; ::_thesis: F c= G
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F or i in G )
assume i in F ; ::_thesis: i in G
then r + i in r ++ F by Th132;
then ex w being Element of ExtREAL st
( r + i = r + w & w in G ) by A1, Th134;
hence i in G by XXREAL_3:11; ::_thesis: verum
end;
theorem :: MEMBER_1:136
for F, G being ext-real-membered set
for r being real number st r ++ F = r ++ G holds
F = G
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number st r ++ F = r ++ G holds
F = G
let r be real number ; ::_thesis: ( r ++ F = r ++ G implies F = G )
assume r ++ F = r ++ G ; ::_thesis: F = G
then ( F c= G & G c= F ) by Th135;
hence F = G by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th137: :: MEMBER_1:137
for F, G being ext-real-membered set
for r being real number holds r ++ (F /\ G) = (r ++ F) /\ (r ++ G)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r ++ (F /\ G) = (r ++ F) /\ (r ++ G)
let r be real number ; ::_thesis: r ++ (F /\ G) = (r ++ F) /\ (r ++ G)
A1: (r ++ F) /\ (r ++ G) c= r ++ (F /\ G)
proof
let j be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not j in (r ++ F) /\ (r ++ G) or j in r ++ (F /\ G) )
assume A2: j in (r ++ F) /\ (r ++ G) ; ::_thesis: j in r ++ (F /\ G)
then j in r ++ F by XBOOLE_0:def_4;
then consider w being Element of ExtREAL such that
A3: j = r + w and
A4: w in F by Th134;
j in r ++ G by A2, XBOOLE_0:def_4;
then consider w1 being Element of ExtREAL such that
A5: j = r + w1 and
A6: w1 in G by Th134;
w = w1 by A3, A5, XXREAL_3:11;
then w in F /\ G by A4, A6, XBOOLE_0:def_4;
hence j in r ++ (F /\ G) by A3, Th132; ::_thesis: verum
end;
r ++ (F /\ G) c= (r ++ F) /\ (r ++ G) by Th42;
hence r ++ (F /\ G) = (r ++ F) /\ (r ++ G) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th138: :: MEMBER_1:138
for F, G being ext-real-membered set
for f being ext-real number holds (f ++ F) \ (f ++ G) c= f ++ (F \ G)
proof
let F, G be ext-real-membered set ; ::_thesis: for f being ext-real number holds (f ++ F) \ (f ++ G) c= f ++ (F \ G)
let f be ext-real number ; ::_thesis: (f ++ F) \ (f ++ G) c= f ++ (F \ G)
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in (f ++ F) \ (f ++ G) or i in f ++ (F \ G) )
assume A1: i in (f ++ F) \ (f ++ G) ; ::_thesis: i in f ++ (F \ G)
then consider w being Element of ExtREAL such that
A2: i = f + w and
A3: w in F by Th134;
now__::_thesis:_w_in_F_\_G
assume not w in F \ G ; ::_thesis: contradiction
then w in G by A3, XBOOLE_0:def_5;
then f + w in f ++ G by Th132;
hence contradiction by A1, A2, XBOOLE_0:def_5; ::_thesis: verum
end;
hence i in f ++ (F \ G) by A2, Th132; ::_thesis: verum
end;
theorem Th139: :: MEMBER_1:139
for F, G being ext-real-membered set
for r being real number holds r ++ (F \ G) = (r ++ F) \ (r ++ G)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r ++ (F \ G) = (r ++ F) \ (r ++ G)
let r be real number ; ::_thesis: r ++ (F \ G) = (r ++ F) \ (r ++ G)
A1: r ++ (F \ G) c= (r ++ F) \ (r ++ G)
proof
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in r ++ (F \ G) or i in (r ++ F) \ (r ++ G) )
assume i in r ++ (F \ G) ; ::_thesis: i in (r ++ F) \ (r ++ G)
then consider w being Element of ExtREAL such that
A2: i = r + w and
A3: w in F \ G by Th134;
A4: now__::_thesis:_not_r_+_w_in_r_++_G
assume r + w in r ++ G ; ::_thesis: contradiction
then consider w1 being Element of ExtREAL such that
A5: r + w = r + w1 and
A6: w1 in G by Th134;
w = w1 by A5, XXREAL_3:11;
hence contradiction by A3, A6, XBOOLE_0:def_5; ::_thesis: verum
end;
r + w in r ++ F by A3, Th132;
hence i in (r ++ F) \ (r ++ G) by A2, A4, XBOOLE_0:def_5; ::_thesis: verum
end;
(r ++ F) \ (r ++ G) c= r ++ (F \ G) by Th138;
hence r ++ (F \ G) = (r ++ F) \ (r ++ G) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th140: :: MEMBER_1:140
for F, G being ext-real-membered set
for r being real number holds r ++ (F \+\ G) = (r ++ F) \+\ (r ++ G)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r ++ (F \+\ G) = (r ++ F) \+\ (r ++ G)
let r be real number ; ::_thesis: r ++ (F \+\ G) = (r ++ F) \+\ (r ++ G)
thus r ++ (F \+\ G) = (r ++ (F \ G)) \/ (r ++ (G \ F)) by Th41
.= ((r ++ F) \ (r ++ G)) \/ (r ++ (G \ F)) by Th139
.= (r ++ F) \+\ (r ++ G) by Th139 ; ::_thesis: verum
end;
definition
let A be complex-membered set ;
let a be complex number ;
funca ++ A -> set equals :: MEMBER_1:def 14
{a} ++ A;
coherence
{a} ++ A is set ;
end;
:: deftheorem defines ++ MEMBER_1:def_14_:_
for A being complex-membered set
for a being complex number holds a ++ A = {a} ++ A;
theorem Th141: :: MEMBER_1:141
for A being complex-membered set
for b, a being complex number st b in A holds
a + b in a ++ A
proof
let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds
a + b in a ++ A
let b, a be complex number ; ::_thesis: ( b in A implies a + b in a ++ A )
a in {a} by TARSKI:def_1;
hence ( b in A implies a + b in a ++ A ) by Th46; ::_thesis: verum
end;
theorem Th142: :: MEMBER_1:142
for A being complex-membered set
for a being complex number holds a ++ A = { (a + c) where c is Element of COMPLEX : c in A }
proof
let A be complex-membered set ; ::_thesis: for a being complex number holds a ++ A = { (a + c) where c is Element of COMPLEX : c in A }
let a be complex number ; ::_thesis: a ++ A = { (a + c) where c is Element of COMPLEX : c in A }
thus a ++ A c= { (a + c) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (a + c) where c is Element of COMPLEX : c in A } c= a ++ A
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in a ++ A or e in { (a + c) where c is Element of COMPLEX : c in A } )
assume e in a ++ A ; ::_thesis: e in { (a + c) where c is Element of COMPLEX : c in A }
then consider c1, c2 being Element of COMPLEX such that
A1: e = c1 + c2 and
A2: c1 in {a} and
A3: c2 in A ;
c1 = a by A2, TARSKI:def_1;
hence e in { (a + c) where c is Element of COMPLEX : c in A } by A1, A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (a + c) where c is Element of COMPLEX : c in A } or e in a ++ A )
assume e in { (a + c) where c is Element of COMPLEX : c in A } ; ::_thesis: e in a ++ A
then ex c being Element of COMPLEX st
( e = a + c & c in A ) ;
hence e in a ++ A by Th141; ::_thesis: verum
end;
theorem Th143: :: MEMBER_1:143
for A being complex-membered set
for a being complex number
for e being set st e in a ++ A holds
ex c being Element of COMPLEX st
( e = a + c & c in A )
proof
let A be complex-membered set ; ::_thesis: for a being complex number
for e being set st e in a ++ A holds
ex c being Element of COMPLEX st
( e = a + c & c in A )
let a be complex number ; ::_thesis: for e being set st e in a ++ A holds
ex c being Element of COMPLEX st
( e = a + c & c in A )
let e be set ; ::_thesis: ( e in a ++ A implies ex c being Element of COMPLEX st
( e = a + c & c in A ) )
a ++ A = { (a + c) where c is Element of COMPLEX : c in A } by Th142;
hence ( e in a ++ A implies ex c being Element of COMPLEX st
( e = a + c & c in A ) ) ; ::_thesis: verum
end;
registration
let A be empty set ;
let a be complex number ;
clustera ++ A -> empty ;
coherence
a ++ A is empty ;
end;
registration
let A be non empty complex-membered set ;
let a be complex number ;
clustera ++ A -> non empty ;
coherence
not a ++ A is empty ;
end;
registration
let A be complex-membered set ;
let a be complex number ;
clustera ++ A -> complex-membered ;
coherence
a ++ A is complex-membered ;
end;
registration
let A be real-membered set ;
let a be real number ;
clustera ++ A -> real-membered ;
coherence
a ++ A is real-membered ;
end;
registration
let A be rational-membered set ;
let a be rational number ;
clustera ++ A -> rational-membered ;
coherence
a ++ A is rational-membered ;
end;
registration
let A be integer-membered set ;
let a be integer number ;
clustera ++ A -> integer-membered ;
coherence
a ++ A is integer-membered ;
end;
registration
let A be natural-membered set ;
let a be Nat;
clustera ++ A -> natural-membered ;
coherence
a ++ A is natural-membered ;
end;
registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifya ++ A with f ++ F when A = F, a = f;
compatibility
( A = F & a = f implies a ++ A = f ++ F ) ;
end;
theorem Th144: :: MEMBER_1:144
for A, B being complex-membered set
for a being complex number holds
( A c= B iff a ++ A c= a ++ B )
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds
( A c= B iff a ++ A c= a ++ B )
let a be complex number ; ::_thesis: ( A c= B iff a ++ A c= a ++ B )
thus ( A c= B implies a ++ A c= a ++ B ) by Th47; ::_thesis: ( a ++ A c= a ++ B implies A c= B )
assume A1: a ++ A c= a ++ B ; ::_thesis: A c= B
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B )
assume z in A ; ::_thesis: z in B
then a + z in a ++ A by Th141;
then ex c being Element of COMPLEX st
( a + z = a + c & c in B ) by A1, Th143;
hence z in B ; ::_thesis: verum
end;
theorem :: MEMBER_1:145
for A, B being complex-membered set
for a being complex number st a ++ A = a ++ B holds
A = B
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a ++ A = a ++ B holds
A = B
let a be complex number ; ::_thesis: ( a ++ A = a ++ B implies A = B )
assume a ++ A = a ++ B ; ::_thesis: A = B
then ( A c= B & B c= A ) by Th144;
hence A = B by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MEMBER_1:146
for A being complex-membered set holds 0 ++ A = A
proof
let A be complex-membered set ; ::_thesis: 0 ++ A = A
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in 0 ++ A or a in A ) & ( not a in A or a in 0 ++ A ) )
hereby ::_thesis: ( not a in A or a in 0 ++ A )
assume a in 0 ++ A ; ::_thesis: a in A
then consider c1, c2 being Element of COMPLEX such that
A1: a = c1 + c2 and
A2: c1 in {0} and
A3: c2 in A ;
c1 = 0 by A2, TARSKI:def_1;
hence a in A by A1, A3; ::_thesis: verum
end;
assume a in A ; ::_thesis: a in 0 ++ A
then 0 + a in { (0 + c) where c is Element of COMPLEX : c in A } ;
hence a in 0 ++ A by Th142; ::_thesis: verum
end;
theorem :: MEMBER_1:147
for A being complex-membered set
for a, b being complex number holds (a + b) ++ A = a ++ (b ++ A)
proof
let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a + b) ++ A = a ++ (b ++ A)
let a, b be complex number ; ::_thesis: (a + b) ++ A = a ++ (b ++ A)
thus (a + b) ++ A = ({a} ++ {b}) ++ A by Th51
.= a ++ (b ++ A) by Th50 ; ::_thesis: verum
end;
theorem :: MEMBER_1:148
for A, B being complex-membered set
for a being complex number holds a ++ (A ++ B) = (a ++ A) ++ B by Th50;
theorem Th149: :: MEMBER_1:149
for A, B being complex-membered set
for a being complex number holds a ++ (A /\ B) = (a ++ A) /\ (a ++ B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds a ++ (A /\ B) = (a ++ A) /\ (a ++ B)
let a be complex number ; ::_thesis: a ++ (A /\ B) = (a ++ A) /\ (a ++ B)
A1: (a ++ A) /\ (a ++ B) c= a ++ (A /\ B)
proof
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in (a ++ A) /\ (a ++ B) or z in a ++ (A /\ B) )
assume A2: z in (a ++ A) /\ (a ++ B) ; ::_thesis: z in a ++ (A /\ B)
then z in a ++ A by XBOOLE_0:def_4;
then consider c being Element of COMPLEX such that
A3: z = a + c and
A4: c in A by Th143;
z in a ++ B by A2, XBOOLE_0:def_4;
then ex c1 being Element of COMPLEX st
( z = a + c1 & c1 in B ) by Th143;
then c in A /\ B by A3, A4, XBOOLE_0:def_4;
hence z in a ++ (A /\ B) by A3, Th141; ::_thesis: verum
end;
a ++ (A /\ B) c= (a ++ A) /\ (a ++ B) by Th49;
hence a ++ (A /\ B) = (a ++ A) /\ (a ++ B) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th150: :: MEMBER_1:150
for A, B being complex-membered set
for a being complex number holds a ++ (A \ B) = (a ++ A) \ (a ++ B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds a ++ (A \ B) = (a ++ A) \ (a ++ B)
let a be complex number ; ::_thesis: a ++ (A \ B) = (a ++ A) \ (a ++ B)
let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in a ++ (A \ B) or z in (a ++ A) \ (a ++ B) ) & ( not z in (a ++ A) \ (a ++ B) or z in a ++ (A \ B) ) )
hereby ::_thesis: ( not z in (a ++ A) \ (a ++ B) or z in a ++ (A \ B) )
assume z in a ++ (A \ B) ; ::_thesis: z in (a ++ A) \ (a ++ B)
then consider c being Element of COMPLEX such that
A1: z = a + c and
A2: c in A \ B by Th143;
A3: now__::_thesis:_not_a_+_c_in_a_++_B
assume a + c in a ++ B ; ::_thesis: contradiction
then ex c1 being Element of COMPLEX st
( a + c = a + c1 & c1 in B ) by Th143;
hence contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
a + c in a ++ A by A2, Th141;
hence z in (a ++ A) \ (a ++ B) by A1, A3, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A4: z in (a ++ A) \ (a ++ B) ; ::_thesis: z in a ++ (A \ B)
then consider c being Element of COMPLEX such that
A5: z = a + c and
A6: c in A by Th143;
now__::_thesis:_c_in_A_\_B
assume not c in A \ B ; ::_thesis: contradiction
then c in B by A6, XBOOLE_0:def_5;
then a + c in a ++ B by Th141;
hence contradiction by A4, A5, XBOOLE_0:def_5; ::_thesis: verum
end;
hence z in a ++ (A \ B) by A5, Th141; ::_thesis: verum
end;
theorem Th151: :: MEMBER_1:151
for A, B being complex-membered set
for a being complex number holds a ++ (A \+\ B) = (a ++ A) \+\ (a ++ B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds a ++ (A \+\ B) = (a ++ A) \+\ (a ++ B)
let a be complex number ; ::_thesis: a ++ (A \+\ B) = (a ++ A) \+\ (a ++ B)
thus a ++ (A \+\ B) = (a ++ (A \ B)) \/ (a ++ (B \ A)) by Th48
.= ((a ++ A) \ (a ++ B)) \/ (a ++ (B \ A)) by Th150
.= (a ++ A) \+\ (a ++ B) by Th150 ; ::_thesis: verum
end;
definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcf -- F -> set equals :: MEMBER_1:def 15
{f} -- F;
coherence
{f} -- F is set ;
end;
:: deftheorem defines -- MEMBER_1:def_15_:_
for F being ext-real-membered set
for f being ext-real number holds f -- F = {f} -- F;
theorem Th152: :: MEMBER_1:152
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
f - g in f -- G
proof
let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds
f - g in f -- G
let g, f be ext-real number ; ::_thesis: ( g in G implies f - g in f -- G )
f in {f} by TARSKI:def_1;
hence ( g in G implies f - g in f -- G ) by Th55; ::_thesis: verum
end;
theorem Th153: :: MEMBER_1:153
for F being ext-real-membered set
for f being ext-real number holds f -- F = { (f - w) where w is Element of ExtREAL : w in F }
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds f -- F = { (f - w) where w is Element of ExtREAL : w in F }
let f be ext-real number ; ::_thesis: f -- F = { (f - w) where w is Element of ExtREAL : w in F }
thus f -- F c= { (f - w) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f - w) where w is Element of ExtREAL : w in F } c= f -- F
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f -- F or e in { (f - w) where w is Element of ExtREAL : w in F } )
assume e in f -- F ; ::_thesis: e in { (f - w) where w is Element of ExtREAL : w in F }
then consider w1, w2 being Element of ExtREAL such that
A1: e = w1 + w2 and
A2: ( w1 in {f} & w2 in -- F ) ;
A3: w1 - (- w2) = w1 + w2 ;
( - w2 in F & w1 = f ) by A2, Th2, TARSKI:def_1;
hence e in { (f - w) where w is Element of ExtREAL : w in F } by A1, A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (f - w) where w is Element of ExtREAL : w in F } or e in f -- F )
assume e in { (f - w) where w is Element of ExtREAL : w in F } ; ::_thesis: e in f -- F
then ex w being Element of ExtREAL st
( e = f - w & w in F ) ;
hence e in f -- F by Th152; ::_thesis: verum
end;
theorem Th154: :: MEMBER_1:154
for F being ext-real-membered set
for f being ext-real number
for e being set st e in f -- F holds
ex w being Element of ExtREAL st
( e = f - w & w in F )
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number
for e being set st e in f -- F holds
ex w being Element of ExtREAL st
( e = f - w & w in F )
let f be ext-real number ; ::_thesis: for e being set st e in f -- F holds
ex w being Element of ExtREAL st
( e = f - w & w in F )
let e be set ; ::_thesis: ( e in f -- F implies ex w being Element of ExtREAL st
( e = f - w & w in F ) )
f -- F = { (f - w) where w is Element of ExtREAL : w in F } by Th153;
hence ( e in f -- F implies ex w being Element of ExtREAL st
( e = f - w & w in F ) ) ; ::_thesis: verum
end;
registration
let F be empty set ;
let f be ext-real number ;
clusterf -- F -> empty ;
coherence
f -- F is empty ;
end;
registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterf -- F -> non empty ;
coherence
not f -- F is empty ;
end;
registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterf -- F -> ext-real-membered ;
coherence
f -- F is ext-real-membered ;
end;
theorem Th155: :: MEMBER_1:155
for F, G being ext-real-membered set
for r being real number st r -- F c= r -- G holds
F c= G
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number st r -- F c= r -- G holds
F c= G
let r be real number ; ::_thesis: ( r -- F c= r -- G implies F c= G )
assume A1: r -- F c= r -- G ; ::_thesis: F c= G
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in F or i in G )
assume i in F ; ::_thesis: i in G
then r - i in r -- F by Th152;
then ex w being Element of ExtREAL st
( r - i = r - w & w in G ) by A1, Th154;
hence i in G by XXREAL_3:12; ::_thesis: verum
end;
theorem :: MEMBER_1:156
for F, G being ext-real-membered set
for r being real number st r -- F = r -- G holds
F = G
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number st r -- F = r -- G holds
F = G
let r be real number ; ::_thesis: ( r -- F = r -- G implies F = G )
assume r -- F = r -- G ; ::_thesis: F = G
then ( F c= G & G c= F ) by Th155;
hence F = G by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th157: :: MEMBER_1:157
for F, G being ext-real-membered set
for r being real number holds r -- (F /\ G) = (r -- F) /\ (r -- G)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r -- (F /\ G) = (r -- F) /\ (r -- G)
let r be real number ; ::_thesis: r -- (F /\ G) = (r -- F) /\ (r -- G)
thus r -- (F /\ G) = r ++ ((-- F) /\ (-- G)) by Th6
.= (r ++ (-- F)) /\ (r ++ (-- G)) by Th137
.= (r -- F) /\ (r -- G) ; ::_thesis: verum
end;
theorem Th158: :: MEMBER_1:158
for F, G being ext-real-membered set
for r being real number holds r -- (F \ G) = (r -- F) \ (r -- G)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r -- (F \ G) = (r -- F) \ (r -- G)
let r be real number ; ::_thesis: r -- (F \ G) = (r -- F) \ (r -- G)
thus r -- (F \ G) = r ++ ((-- F) \ (-- G)) by Th7
.= (r ++ (-- F)) \ (r ++ (-- G)) by Th139
.= (r -- F) \ (r -- G) ; ::_thesis: verum
end;
theorem Th159: :: MEMBER_1:159
for F, G being ext-real-membered set
for r being real number holds r -- (F \+\ G) = (r -- F) \+\ (r -- G)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number holds r -- (F \+\ G) = (r -- F) \+\ (r -- G)
let r be real number ; ::_thesis: r -- (F \+\ G) = (r -- F) \+\ (r -- G)
thus r -- (F \+\ G) = r ++ ((-- F) \+\ (-- G)) by Th8
.= (r ++ (-- F)) \+\ (r ++ (-- G)) by Th140
.= (r -- F) \+\ (r -- G) ; ::_thesis: verum
end;
definition
let A be complex-membered set ;
let a be complex number ;
funca -- A -> set equals :: MEMBER_1:def 16
{a} -- A;
coherence
{a} -- A is set ;
end;
:: deftheorem defines -- MEMBER_1:def_16_:_
for A being complex-membered set
for a being complex number holds a -- A = {a} -- A;
theorem Th160: :: MEMBER_1:160
for A being complex-membered set
for b, a being complex number st b in A holds
a - b in a -- A
proof
let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds
a - b in a -- A
let b, a be complex number ; ::_thesis: ( b in A implies a - b in a -- A )
a in {a} by TARSKI:def_1;
hence ( b in A implies a - b in a -- A ) by Th66; ::_thesis: verum
end;
theorem Th161: :: MEMBER_1:161
for A being complex-membered set
for a being complex number holds a -- A = { (a - c) where c is Element of COMPLEX : c in A }
proof
let A be complex-membered set ; ::_thesis: for a being complex number holds a -- A = { (a - c) where c is Element of COMPLEX : c in A }
let a be complex number ; ::_thesis: a -- A = { (a - c) where c is Element of COMPLEX : c in A }
A1: a -- A = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in {a} & c2 in A ) } by Th65;
thus a -- A c= { (a - c) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (a - c) where c is Element of COMPLEX : c in A } c= a -- A
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in a -- A or e in { (a - c) where c is Element of COMPLEX : c in A } )
assume e in a -- A ; ::_thesis: e in { (a - c) where c is Element of COMPLEX : c in A }
then consider c1, c2 being Element of COMPLEX such that
A2: e = c1 - c2 and
A3: c1 in {a} and
A4: c2 in A by A1;
c1 = a by A3, TARSKI:def_1;
hence e in { (a - c) where c is Element of COMPLEX : c in A } by A2, A4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (a - c) where c is Element of COMPLEX : c in A } or e in a -- A )
assume e in { (a - c) where c is Element of COMPLEX : c in A } ; ::_thesis: e in a -- A
then ex c being Element of COMPLEX st
( e = a - c & c in A ) ;
hence e in a -- A by Th160; ::_thesis: verum
end;
theorem Th162: :: MEMBER_1:162
for A being complex-membered set
for a being complex number
for e being set st e in a -- A holds
ex c being Element of COMPLEX st
( e = a - c & c in A )
proof
let A be complex-membered set ; ::_thesis: for a being complex number
for e being set st e in a -- A holds
ex c being Element of COMPLEX st
( e = a - c & c in A )
let a be complex number ; ::_thesis: for e being set st e in a -- A holds
ex c being Element of COMPLEX st
( e = a - c & c in A )
let e be set ; ::_thesis: ( e in a -- A implies ex c being Element of COMPLEX st
( e = a - c & c in A ) )
a -- A = { (a - c) where c is Element of COMPLEX : c in A } by Th161;
hence ( e in a -- A implies ex c being Element of COMPLEX st
( e = a - c & c in A ) ) ; ::_thesis: verum
end;
registration
let A be empty set ;
let a be complex number ;
clustera -- A -> empty ;
coherence
a -- A is empty ;
end;
registration
let A be non empty complex-membered set ;
let a be complex number ;
clustera -- A -> non empty ;
coherence
not a -- A is empty ;
end;
registration
let A be complex-membered set ;
let a be complex number ;
clustera -- A -> complex-membered ;
coherence
a -- A is complex-membered ;
end;
registration
let A be real-membered set ;
let a be real number ;
clustera -- A -> real-membered ;
coherence
a -- A is real-membered ;
end;
registration
let A be rational-membered set ;
let a be rational number ;
clustera -- A -> rational-membered ;
coherence
a -- A is rational-membered ;
end;
registration
let A be integer-membered set ;
let a be integer number ;
clustera -- A -> integer-membered ;
coherence
a -- A is integer-membered ;
end;
registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifya -- A with f -- F when A = F, a = f;
compatibility
( A = F & a = f implies a -- A = f -- F ) ;
end;
theorem Th163: :: MEMBER_1:163
for A, B being complex-membered set
for a being complex number holds
( A c= B iff a -- A c= a -- B )
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds
( A c= B iff a -- A c= a -- B )
let a be complex number ; ::_thesis: ( A c= B iff a -- A c= a -- B )
thus ( A c= B implies a -- A c= a -- B ) by Th67; ::_thesis: ( a -- A c= a -- B implies A c= B )
assume A1: a -- A c= a -- B ; ::_thesis: A c= B
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B )
assume z in A ; ::_thesis: z in B
then a - z in a -- A by Th160;
then ex c being Element of COMPLEX st
( a - z = a - c & c in B ) by A1, Th162;
hence z in B ; ::_thesis: verum
end;
theorem :: MEMBER_1:164
for A, B being complex-membered set
for a being complex number st a -- A = a -- B holds
A = B
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a -- A = a -- B holds
A = B
let a be complex number ; ::_thesis: ( a -- A = a -- B implies A = B )
assume a -- A = a -- B ; ::_thesis: A = B
then ( A c= B & B c= A ) by Th163;
hence A = B by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th165: :: MEMBER_1:165
for A, B being complex-membered set
for a being complex number holds a -- (A /\ B) = (a -- A) /\ (a -- B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds a -- (A /\ B) = (a -- A) /\ (a -- B)
let a be complex number ; ::_thesis: a -- (A /\ B) = (a -- A) /\ (a -- B)
thus a -- (A /\ B) = a ++ ((-- A) /\ (-- B)) by Th16
.= (a ++ (-- A)) /\ (a ++ (-- B)) by Th149
.= (a -- A) /\ (a -- B) ; ::_thesis: verum
end;
theorem Th166: :: MEMBER_1:166
for A, B being complex-membered set
for a being complex number holds a -- (A \ B) = (a -- A) \ (a -- B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds a -- (A \ B) = (a -- A) \ (a -- B)
let a be complex number ; ::_thesis: a -- (A \ B) = (a -- A) \ (a -- B)
thus a -- (A \ B) = a ++ ((-- A) \ (-- B)) by Th17
.= (a ++ (-- A)) \ (a ++ (-- B)) by Th150
.= (a -- A) \ (a -- B) ; ::_thesis: verum
end;
theorem Th167: :: MEMBER_1:167
for A, B being complex-membered set
for a being complex number holds a -- (A \+\ B) = (a -- A) \+\ (a -- B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds a -- (A \+\ B) = (a -- A) \+\ (a -- B)
let a be complex number ; ::_thesis: a -- (A \+\ B) = (a -- A) \+\ (a -- B)
thus a -- (A \+\ B) = a ++ ((-- A) \+\ (-- B)) by Th18
.= (a ++ (-- A)) \+\ (a ++ (-- B)) by Th151
.= (a -- A) \+\ (a -- B) ; ::_thesis: verum
end;
definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcF -- f -> set equals :: MEMBER_1:def 17
F -- {f};
coherence
F -- {f} is set ;
end;
:: deftheorem defines -- MEMBER_1:def_17_:_
for F being ext-real-membered set
for f being ext-real number holds F -- f = F -- {f};
theorem Th168: :: MEMBER_1:168
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
g - f in G -- f
proof
let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds
g - f in G -- f
let g, f be ext-real number ; ::_thesis: ( g in G implies g - f in G -- f )
f in {f} by TARSKI:def_1;
hence ( g in G implies g - f in G -- f ) by Th55; ::_thesis: verum
end;
theorem Th169: :: MEMBER_1:169
for F being ext-real-membered set
for f being ext-real number holds F -- f = { (w - f) where w is Element of ExtREAL : w in F }
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds F -- f = { (w - f) where w is Element of ExtREAL : w in F }
let f be ext-real number ; ::_thesis: F -- f = { (w - f) where w is Element of ExtREAL : w in F }
thus F -- f c= { (w - f) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (w - f) where w is Element of ExtREAL : w in F } c= F -- f
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F -- f or e in { (w - f) where w is Element of ExtREAL : w in F } )
assume e in F -- f ; ::_thesis: e in { (w - f) where w is Element of ExtREAL : w in F }
then consider w1, w2 being Element of ExtREAL such that
A1: ( e = w1 + w2 & w1 in F ) and
A2: w2 in -- {f} ;
- w2 in {f} by A2, Th2;
then ( w1 - (- w2) = w1 + w2 & - w2 = f ) by TARSKI:def_1;
hence e in { (w - f) where w is Element of ExtREAL : w in F } by A1; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w - f) where w is Element of ExtREAL : w in F } or e in F -- f )
assume e in { (w - f) where w is Element of ExtREAL : w in F } ; ::_thesis: e in F -- f
then ex w being Element of ExtREAL st
( e = w - f & w in F ) ;
hence e in F -- f by Th168; ::_thesis: verum
end;
theorem :: MEMBER_1:170
for F being ext-real-membered set
for f being ext-real number
for e being set st e in F -- f holds
ex w being Element of ExtREAL st
( e = w - f & w in F )
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number
for e being set st e in F -- f holds
ex w being Element of ExtREAL st
( e = w - f & w in F )
let f be ext-real number ; ::_thesis: for e being set st e in F -- f holds
ex w being Element of ExtREAL st
( e = w - f & w in F )
let e be set ; ::_thesis: ( e in F -- f implies ex w being Element of ExtREAL st
( e = w - f & w in F ) )
F -- f = { (w - f) where w is Element of ExtREAL : w in F } by Th169;
hence ( e in F -- f implies ex w being Element of ExtREAL st
( e = w - f & w in F ) ) ; ::_thesis: verum
end;
registration
let F be empty set ;
let f be ext-real number ;
clusterF -- f -> empty ;
coherence
F -- f is empty ;
end;
registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterF -- f -> non empty ;
coherence
not F -- f is empty ;
end;
registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterF -- f -> ext-real-membered ;
coherence
F -- f is ext-real-membered ;
end;
theorem :: MEMBER_1:171
for F being ext-real-membered set
for f being ext-real number holds F -- f = -- (f -- F) by Th60;
theorem :: MEMBER_1:172
for F being ext-real-membered set
for f being ext-real number holds f -- F = -- (F -- f) by Th60;
theorem :: MEMBER_1:173
for F, G being ext-real-membered set
for r being real number holds (F /\ G) -- r = (F -- r) /\ (G -- r)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number holds (F /\ G) -- r = (F -- r) /\ (G -- r)
let r be real number ; ::_thesis: (F /\ G) -- r = (F -- r) /\ (G -- r)
thus (F /\ G) -- r = -- (r -- (F /\ G)) by Th60
.= -- ((r -- F) /\ (r -- G)) by Th157
.= (-- (r -- F)) /\ (-- (r -- G)) by Th6
.= (-- (r -- F)) /\ (G -- r) by Th60
.= (F -- r) /\ (G -- r) by Th60 ; ::_thesis: verum
end;
theorem :: MEMBER_1:174
for F, G being ext-real-membered set
for r being real number holds (F \ G) -- r = (F -- r) \ (G -- r)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number holds (F \ G) -- r = (F -- r) \ (G -- r)
let r be real number ; ::_thesis: (F \ G) -- r = (F -- r) \ (G -- r)
thus (F \ G) -- r = -- (r -- (F \ G)) by Th60
.= -- ((r -- F) \ (r -- G)) by Th158
.= (-- (r -- F)) \ (-- (r -- G)) by Th7
.= (-- (r -- F)) \ (G -- r) by Th60
.= (F -- r) \ (G -- r) by Th60 ; ::_thesis: verum
end;
theorem :: MEMBER_1:175
for F, G being ext-real-membered set
for r being real number holds (F \+\ G) -- r = (F -- r) \+\ (G -- r)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number holds (F \+\ G) -- r = (F -- r) \+\ (G -- r)
let r be real number ; ::_thesis: (F \+\ G) -- r = (F -- r) \+\ (G -- r)
thus (F \+\ G) -- r = -- (r -- (F \+\ G)) by Th60
.= -- ((r -- F) \+\ (r -- G)) by Th159
.= (-- (r -- F)) \+\ (-- (r -- G)) by Th8
.= (-- (r -- F)) \+\ (G -- r) by Th60
.= (F -- r) \+\ (G -- r) by Th60 ; ::_thesis: verum
end;
definition
let A be complex-membered set ;
let a be complex number ;
funcA -- a -> set equals :: MEMBER_1:def 18
A -- {a};
coherence
A -- {a} is set ;
end;
:: deftheorem defines -- MEMBER_1:def_18_:_
for A being complex-membered set
for a being complex number holds A -- a = A -- {a};
theorem Th176: :: MEMBER_1:176
for A being complex-membered set
for b, a being complex number st b in A holds
b - a in A -- a
proof
let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds
b - a in A -- a
let b, a be complex number ; ::_thesis: ( b in A implies b - a in A -- a )
a in {a} by TARSKI:def_1;
hence ( b in A implies b - a in A -- a ) by Th66; ::_thesis: verum
end;
theorem Th177: :: MEMBER_1:177
for A being complex-membered set
for a being complex number holds A -- a = { (c - a) where c is Element of COMPLEX : c in A }
proof
let A be complex-membered set ; ::_thesis: for a being complex number holds A -- a = { (c - a) where c is Element of COMPLEX : c in A }
let a be complex number ; ::_thesis: A -- a = { (c - a) where c is Element of COMPLEX : c in A }
A1: A -- a = { (c1 - c2) where c1, c2 is Element of COMPLEX : ( c1 in A & c2 in {a} ) } by Th65;
thus A -- a c= { (c - a) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (c - a) where c is Element of COMPLEX : c in A } c= A -- a
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A -- a or e in { (c - a) where c is Element of COMPLEX : c in A } )
assume e in A -- a ; ::_thesis: e in { (c - a) where c is Element of COMPLEX : c in A }
then consider c1, c2 being Element of COMPLEX such that
A2: ( e = c1 - c2 & c1 in A ) and
A3: c2 in {a} by A1;
c2 = a by A3, TARSKI:def_1;
hence e in { (c - a) where c is Element of COMPLEX : c in A } by A2; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c - a) where c is Element of COMPLEX : c in A } or e in A -- a )
assume e in { (c - a) where c is Element of COMPLEX : c in A } ; ::_thesis: e in A -- a
then ex c being Element of COMPLEX st
( e = c - a & c in A ) ;
hence e in A -- a by Th176; ::_thesis: verum
end;
theorem Th178: :: MEMBER_1:178
for A being complex-membered set
for a being complex number
for e being set st e in A -- a holds
ex c being Element of COMPLEX st
( e = c - a & c in A )
proof
let A be complex-membered set ; ::_thesis: for a being complex number
for e being set st e in A -- a holds
ex c being Element of COMPLEX st
( e = c - a & c in A )
let a be complex number ; ::_thesis: for e being set st e in A -- a holds
ex c being Element of COMPLEX st
( e = c - a & c in A )
let e be set ; ::_thesis: ( e in A -- a implies ex c being Element of COMPLEX st
( e = c - a & c in A ) )
A -- a = { (c - a) where c is Element of COMPLEX : c in A } by Th177;
hence ( e in A -- a implies ex c being Element of COMPLEX st
( e = c - a & c in A ) ) ; ::_thesis: verum
end;
registration
let A be empty set ;
let a be complex number ;
clusterA -- a -> empty ;
coherence
A -- a is empty ;
end;
registration
let A be non empty complex-membered set ;
let a be complex number ;
clusterA -- a -> non empty ;
coherence
not A -- a is empty ;
end;
registration
let A be complex-membered set ;
let a be complex number ;
clusterA -- a -> complex-membered ;
coherence
A -- a is complex-membered ;
end;
registration
let A be real-membered set ;
let a be real number ;
clusterA -- a -> real-membered ;
coherence
A -- a is real-membered ;
end;
registration
let A be rational-membered set ;
let a be rational number ;
clusterA -- a -> rational-membered ;
coherence
A -- a is rational-membered ;
end;
registration
let A be integer-membered set ;
let a be integer number ;
clusterA -- a -> integer-membered ;
coherence
A -- a is integer-membered ;
end;
registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifyA -- a with F -- f when A = F, a = f;
compatibility
( A = F & a = f implies A -- a = F -- f ) ;
end;
theorem Th179: :: MEMBER_1:179
for A, B being complex-membered set
for a being complex number holds
( A c= B iff A -- a c= B -- a )
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds
( A c= B iff A -- a c= B -- a )
let a be complex number ; ::_thesis: ( A c= B iff A -- a c= B -- a )
thus ( A c= B implies A -- a c= B -- a ) by Th67; ::_thesis: ( A -- a c= B -- a implies A c= B )
assume A1: A -- a c= B -- a ; ::_thesis: A c= B
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B )
assume z in A ; ::_thesis: z in B
then z - a in A -- a by Th176;
then ex c being Element of COMPLEX st
( z - a = c - a & c in B ) by A1, Th178;
hence z in B ; ::_thesis: verum
end;
theorem :: MEMBER_1:180
for A, B being complex-membered set
for a being complex number st A -- a = B -- a holds
A = B
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st A -- a = B -- a holds
A = B
let a be complex number ; ::_thesis: ( A -- a = B -- a implies A = B )
assume A -- a = B -- a ; ::_thesis: A = B
then ( A c= B & B c= A ) by Th179;
hence A = B by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MEMBER_1:181
for A being complex-membered set
for a being complex number holds A -- a = -- (a -- A) by Th71;
theorem :: MEMBER_1:182
for A being complex-membered set
for a being complex number holds a -- A = -- (A -- a) by Th71;
theorem :: MEMBER_1:183
for A, B being complex-membered set
for a being complex number holds (A /\ B) -- a = (A -- a) /\ (B -- a)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds (A /\ B) -- a = (A -- a) /\ (B -- a)
let a be complex number ; ::_thesis: (A /\ B) -- a = (A -- a) /\ (B -- a)
thus (A /\ B) -- a = -- (a -- (A /\ B)) by Th71
.= -- ((a -- A) /\ (a -- B)) by Th165
.= (-- (a -- A)) /\ (-- (a -- B)) by Th16
.= (-- (a -- A)) /\ (B -- a) by Th71
.= (A -- a) /\ (B -- a) by Th71 ; ::_thesis: verum
end;
theorem :: MEMBER_1:184
for A, B being complex-membered set
for a being complex number holds (A \ B) -- a = (A -- a) \ (B -- a)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds (A \ B) -- a = (A -- a) \ (B -- a)
let a be complex number ; ::_thesis: (A \ B) -- a = (A -- a) \ (B -- a)
thus (A \ B) -- a = -- (a -- (A \ B)) by Th71
.= -- ((a -- A) \ (a -- B)) by Th166
.= (-- (a -- A)) \ (-- (a -- B)) by Th17
.= (-- (a -- A)) \ (B -- a) by Th71
.= (A -- a) \ (B -- a) by Th71 ; ::_thesis: verum
end;
theorem :: MEMBER_1:185
for A, B being complex-membered set
for a being complex number holds (A \+\ B) -- a = (A -- a) \+\ (B -- a)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds (A \+\ B) -- a = (A -- a) \+\ (B -- a)
let a be complex number ; ::_thesis: (A \+\ B) -- a = (A -- a) \+\ (B -- a)
thus (A \+\ B) -- a = -- (a -- (A \+\ B)) by Th71
.= -- ((a -- A) \+\ (a -- B)) by Th167
.= (-- (a -- A)) \+\ (-- (a -- B)) by Th18
.= (-- (a -- A)) \+\ (B -- a) by Th71
.= (A -- a) \+\ (B -- a) by Th71 ; ::_thesis: verum
end;
definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcf ** F -> set equals :: MEMBER_1:def 19
{f} ** F;
coherence
{f} ** F is set ;
end;
:: deftheorem defines ** MEMBER_1:def_19_:_
for F being ext-real-membered set
for f being ext-real number holds f ** F = {f} ** F;
theorem Th186: :: MEMBER_1:186
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
f * g in f ** G
proof
let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds
f * g in f ** G
let g, f be ext-real number ; ::_thesis: ( g in G implies f * g in f ** G )
f in {f} by TARSKI:def_1;
hence ( g in G implies f * g in f ** G ) by Th79; ::_thesis: verum
end;
theorem Th187: :: MEMBER_1:187
for F being ext-real-membered set
for f being ext-real number holds f ** F = { (f * w) where w is Element of ExtREAL : w in F }
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds f ** F = { (f * w) where w is Element of ExtREAL : w in F }
let f be ext-real number ; ::_thesis: f ** F = { (f * w) where w is Element of ExtREAL : w in F }
thus f ** F c= { (f * w) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f * w) where w is Element of ExtREAL : w in F } c= f ** F
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f ** F or e in { (f * w) where w is Element of ExtREAL : w in F } )
assume e in f ** F ; ::_thesis: e in { (f * w) where w is Element of ExtREAL : w in F }
then consider w1, w2 being Element of ExtREAL such that
A1: e = w1 * w2 and
A2: w1 in {f} and
A3: w2 in F ;
w1 = f by A2, TARSKI:def_1;
hence e in { (f * w) where w is Element of ExtREAL : w in F } by A1, A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (f * w) where w is Element of ExtREAL : w in F } or e in f ** F )
assume e in { (f * w) where w is Element of ExtREAL : w in F } ; ::_thesis: e in f ** F
then ex w being Element of ExtREAL st
( e = f * w & w in F ) ;
hence e in f ** F by Th186; ::_thesis: verum
end;
theorem Th188: :: MEMBER_1:188
for F being ext-real-membered set
for f being ext-real number
for e being set st e in f ** F holds
ex w being Element of ExtREAL st
( e = f * w & w in F )
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number
for e being set st e in f ** F holds
ex w being Element of ExtREAL st
( e = f * w & w in F )
let f be ext-real number ; ::_thesis: for e being set st e in f ** F holds
ex w being Element of ExtREAL st
( e = f * w & w in F )
let e be set ; ::_thesis: ( e in f ** F implies ex w being Element of ExtREAL st
( e = f * w & w in F ) )
f ** F = { (f * w) where w is Element of ExtREAL : w in F } by Th187;
hence ( e in f ** F implies ex w being Element of ExtREAL st
( e = f * w & w in F ) ) ; ::_thesis: verum
end;
registration
let F be empty set ;
let f be ext-real number ;
clusterf ** F -> empty ;
coherence
f ** F is empty ;
end;
registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterf ** F -> non empty ;
coherence
not f ** F is empty ;
end;
registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterf ** F -> ext-real-membered ;
coherence
f ** F is ext-real-membered ;
end;
theorem :: MEMBER_1:189
for F, G being ext-real-membered set
for r being real number st r <> 0 holds
r ** (F /\ G) = (r ** F) /\ (r ** G)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number st r <> 0 holds
r ** (F /\ G) = (r ** F) /\ (r ** G)
let r be real number ; ::_thesis: ( r <> 0 implies r ** (F /\ G) = (r ** F) /\ (r ** G) )
assume A1: r <> 0 ; ::_thesis: r ** (F /\ G) = (r ** F) /\ (r ** G)
A2: (r ** F) /\ (r ** G) c= r ** (F /\ G)
proof
let j be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not j in (r ** F) /\ (r ** G) or j in r ** (F /\ G) )
assume A3: j in (r ** F) /\ (r ** G) ; ::_thesis: j in r ** (F /\ G)
then j in r ** F by XBOOLE_0:def_4;
then consider w being Element of ExtREAL such that
A4: j = r * w and
A5: w in F by Th188;
j in r ** G by A3, XBOOLE_0:def_4;
then consider w1 being Element of ExtREAL such that
A6: j = r * w1 and
A7: w1 in G by Th188;
w = w1 by A1, A4, A6, XXREAL_3:68;
then w in F /\ G by A5, A7, XBOOLE_0:def_4;
hence j in r ** (F /\ G) by A4, Th186; ::_thesis: verum
end;
r ** (F /\ G) c= (r ** F) /\ (r ** G) by Th83;
hence r ** (F /\ G) = (r ** F) /\ (r ** G) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th190: :: MEMBER_1:190
for F, G being ext-real-membered set
for f being ext-real number holds (f ** F) \ (f ** G) c= f ** (F \ G)
proof
let F, G be ext-real-membered set ; ::_thesis: for f being ext-real number holds (f ** F) \ (f ** G) c= f ** (F \ G)
let f be ext-real number ; ::_thesis: (f ** F) \ (f ** G) c= f ** (F \ G)
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in (f ** F) \ (f ** G) or i in f ** (F \ G) )
assume A1: i in (f ** F) \ (f ** G) ; ::_thesis: i in f ** (F \ G)
then consider w being Element of ExtREAL such that
A2: i = f * w and
A3: w in F by Th188;
now__::_thesis:_w_in_F_\_G
assume not w in F \ G ; ::_thesis: contradiction
then w in G by A3, XBOOLE_0:def_5;
then f * w in f ** G by Th186;
hence contradiction by A1, A2, XBOOLE_0:def_5; ::_thesis: verum
end;
hence i in f ** (F \ G) by A2, Th186; ::_thesis: verum
end;
theorem Th191: :: MEMBER_1:191
for F, G being ext-real-membered set
for r being real number st r <> 0 holds
r ** (F \ G) = (r ** F) \ (r ** G)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number st r <> 0 holds
r ** (F \ G) = (r ** F) \ (r ** G)
let r be real number ; ::_thesis: ( r <> 0 implies r ** (F \ G) = (r ** F) \ (r ** G) )
assume A1: r <> 0 ; ::_thesis: r ** (F \ G) = (r ** F) \ (r ** G)
A2: r ** (F \ G) c= (r ** F) \ (r ** G)
proof
let i be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not i in r ** (F \ G) or i in (r ** F) \ (r ** G) )
assume i in r ** (F \ G) ; ::_thesis: i in (r ** F) \ (r ** G)
then consider w being Element of ExtREAL such that
A3: i = r * w and
A4: w in F \ G by Th188;
A5: now__::_thesis:_not_r_*_w_in_r_**_G
assume r * w in r ** G ; ::_thesis: contradiction
then consider w1 being Element of ExtREAL such that
A6: r * w = r * w1 and
A7: w1 in G by Th188;
w = w1 by A1, A6, XXREAL_3:68;
hence contradiction by A4, A7, XBOOLE_0:def_5; ::_thesis: verum
end;
r * w in r ** F by A4, Th186;
hence i in (r ** F) \ (r ** G) by A3, A5, XBOOLE_0:def_5; ::_thesis: verum
end;
(r ** F) \ (r ** G) c= r ** (F \ G) by Th190;
hence r ** (F \ G) = (r ** F) \ (r ** G) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MEMBER_1:192
for F, G being ext-real-membered set
for r being real number st r <> 0 holds
r ** (F \+\ G) = (r ** F) \+\ (r ** G)
proof
let F, G be ext-real-membered set ; ::_thesis: for r being real number st r <> 0 holds
r ** (F \+\ G) = (r ** F) \+\ (r ** G)
let r be real number ; ::_thesis: ( r <> 0 implies r ** (F \+\ G) = (r ** F) \+\ (r ** G) )
assume A1: r <> 0 ; ::_thesis: r ** (F \+\ G) = (r ** F) \+\ (r ** G)
thus r ** (F \+\ G) = (r ** (F \ G)) \/ (r ** (G \ F)) by Th82
.= ((r ** F) \ (r ** G)) \/ (r ** (G \ F)) by A1, Th191
.= (r ** F) \+\ (r ** G) by A1, Th191 ; ::_thesis: verum
end;
definition
let A be complex-membered set ;
let a be complex number ;
funca ** A -> set equals :: MEMBER_1:def 20
{a} ** A;
coherence
{a} ** A is set ;
end;
:: deftheorem defines ** MEMBER_1:def_20_:_
for A being complex-membered set
for a being complex number holds a ** A = {a} ** A;
theorem Th193: :: MEMBER_1:193
for A being complex-membered set
for b, a being complex number st b in A holds
a * b in a ** A
proof
let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds
a * b in a ** A
let b, a be complex number ; ::_thesis: ( b in A implies a * b in a ** A )
a in {a} by TARSKI:def_1;
hence ( b in A implies a * b in a ** A ) by Th89; ::_thesis: verum
end;
theorem Th194: :: MEMBER_1:194
for A being complex-membered set
for a being complex number holds a ** A = { (a * c) where c is Element of COMPLEX : c in A }
proof
let A be complex-membered set ; ::_thesis: for a being complex number holds a ** A = { (a * c) where c is Element of COMPLEX : c in A }
let a be complex number ; ::_thesis: a ** A = { (a * c) where c is Element of COMPLEX : c in A }
thus a ** A c= { (a * c) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (a * c) where c is Element of COMPLEX : c in A } c= a ** A
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in a ** A or e in { (a * c) where c is Element of COMPLEX : c in A } )
assume e in a ** A ; ::_thesis: e in { (a * c) where c is Element of COMPLEX : c in A }
then consider c1, c2 being Element of COMPLEX such that
A1: e = c1 * c2 and
A2: c1 in {a} and
A3: c2 in A ;
c1 = a by A2, TARSKI:def_1;
hence e in { (a * c) where c is Element of COMPLEX : c in A } by A1, A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (a * c) where c is Element of COMPLEX : c in A } or e in a ** A )
assume e in { (a * c) where c is Element of COMPLEX : c in A } ; ::_thesis: e in a ** A
then ex c being Element of COMPLEX st
( e = a * c & c in A ) ;
hence e in a ** A by Th193; ::_thesis: verum
end;
theorem Th195: :: MEMBER_1:195
for A being complex-membered set
for a being complex number
for e being set st e in a ** A holds
ex c being Element of COMPLEX st
( e = a * c & c in A )
proof
let A be complex-membered set ; ::_thesis: for a being complex number
for e being set st e in a ** A holds
ex c being Element of COMPLEX st
( e = a * c & c in A )
let a be complex number ; ::_thesis: for e being set st e in a ** A holds
ex c being Element of COMPLEX st
( e = a * c & c in A )
let e be set ; ::_thesis: ( e in a ** A implies ex c being Element of COMPLEX st
( e = a * c & c in A ) )
a ** A = { (a * c) where c is Element of COMPLEX : c in A } by Th194;
hence ( e in a ** A implies ex c being Element of COMPLEX st
( e = a * c & c in A ) ) ; ::_thesis: verum
end;
registration
let A be empty set ;
let a be complex number ;
clustera ** A -> empty ;
coherence
a ** A is empty ;
end;
registration
let A be non empty complex-membered set ;
let a be complex number ;
clustera ** A -> non empty ;
coherence
not a ** A is empty ;
end;
registration
let A be complex-membered set ;
let a be complex number ;
clustera ** A -> complex-membered ;
coherence
a ** A is complex-membered ;
end;
registration
let A be real-membered set ;
let a be real number ;
clustera ** A -> real-membered ;
coherence
a ** A is real-membered ;
end;
registration
let A be rational-membered set ;
let a be rational number ;
clustera ** A -> rational-membered ;
coherence
a ** A is rational-membered ;
end;
registration
let A be integer-membered set ;
let a be integer number ;
clustera ** A -> integer-membered ;
coherence
a ** A is integer-membered ;
end;
registration
let A be natural-membered set ;
let a be Nat;
clustera ** A -> natural-membered ;
coherence
a ** A is natural-membered ;
end;
registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifya ** A with f ** F when A = F, a = f;
compatibility
( A = F & a = f implies a ** A = f ** F ) ;
end;
theorem Th196: :: MEMBER_1:196
for A, B being complex-membered set
for a being complex number st a <> 0 & a ** A c= a ** B holds
A c= B
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & a ** A c= a ** B holds
A c= B
let a be complex number ; ::_thesis: ( a <> 0 & a ** A c= a ** B implies A c= B )
assume that
A1: a <> 0 and
A2: a ** A c= a ** B ; ::_thesis: A c= B
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B )
assume z in A ; ::_thesis: z in B
then a * z in a ** A by Th193;
then ex c being Element of COMPLEX st
( a * z = a * c & c in B ) by A2, Th195;
hence z in B by A1, XCMPLX_1:5; ::_thesis: verum
end;
theorem :: MEMBER_1:197
for A, B being complex-membered set
for a being complex number st a <> 0 & a ** A = a ** B holds
A = B
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & a ** A = a ** B holds
A = B
let a be complex number ; ::_thesis: ( a <> 0 & a ** A = a ** B implies A = B )
assume ( a <> 0 & a ** A = a ** B ) ; ::_thesis: A = B
then ( A c= B & B c= A ) by Th196;
hence A = B by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th198: :: MEMBER_1:198
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a ** (A /\ B) = (a ** A) /\ (a ** B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds
a ** (A /\ B) = (a ** A) /\ (a ** B)
let a be complex number ; ::_thesis: ( a <> 0 implies a ** (A /\ B) = (a ** A) /\ (a ** B) )
assume A1: a <> 0 ; ::_thesis: a ** (A /\ B) = (a ** A) /\ (a ** B)
A2: (a ** A) /\ (a ** B) c= a ** (A /\ B)
proof
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in (a ** A) /\ (a ** B) or z in a ** (A /\ B) )
assume A3: z in (a ** A) /\ (a ** B) ; ::_thesis: z in a ** (A /\ B)
then z in a ** A by XBOOLE_0:def_4;
then consider c being Element of COMPLEX such that
A4: z = a * c and
A5: c in A by Th195;
z in a ** B by A3, XBOOLE_0:def_4;
then consider c1 being Element of COMPLEX such that
A6: z = a * c1 and
A7: c1 in B by Th195;
c = c1 by A1, A4, A6, XCMPLX_1:5;
then c in A /\ B by A5, A7, XBOOLE_0:def_4;
hence z in a ** (A /\ B) by A4, Th193; ::_thesis: verum
end;
a ** (A /\ B) c= (a ** A) /\ (a ** B) by Th93;
hence a ** (A /\ B) = (a ** A) /\ (a ** B) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th199: :: MEMBER_1:199
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a ** (A \ B) = (a ** A) \ (a ** B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds
a ** (A \ B) = (a ** A) \ (a ** B)
let a be complex number ; ::_thesis: ( a <> 0 implies a ** (A \ B) = (a ** A) \ (a ** B) )
assume A1: a <> 0 ; ::_thesis: a ** (A \ B) = (a ** A) \ (a ** B)
let z be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not z in a ** (A \ B) or z in (a ** A) \ (a ** B) ) & ( not z in (a ** A) \ (a ** B) or z in a ** (A \ B) ) )
hereby ::_thesis: ( not z in (a ** A) \ (a ** B) or z in a ** (A \ B) )
assume z in a ** (A \ B) ; ::_thesis: z in (a ** A) \ (a ** B)
then consider c being Element of COMPLEX such that
A2: z = a * c and
A3: c in A \ B by Th195;
A4: now__::_thesis:_not_a_*_c_in_a_**_B
assume a * c in a ** B ; ::_thesis: contradiction
then consider c1 being Element of COMPLEX such that
A5: a * c = a * c1 and
A6: c1 in B by Th195;
c = c1 by A1, A5, XCMPLX_1:5;
hence contradiction by A3, A6, XBOOLE_0:def_5; ::_thesis: verum
end;
a * c in a ** A by A3, Th193;
hence z in (a ** A) \ (a ** B) by A2, A4, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A7: z in (a ** A) \ (a ** B) ; ::_thesis: z in a ** (A \ B)
then consider c being Element of COMPLEX such that
A8: z = a * c and
A9: c in A by Th195;
now__::_thesis:_c_in_A_\_B
assume not c in A \ B ; ::_thesis: contradiction
then c in B by A9, XBOOLE_0:def_5;
then a * c in a ** B by Th193;
hence contradiction by A7, A8, XBOOLE_0:def_5; ::_thesis: verum
end;
hence z in a ** (A \ B) by A8, Th193; ::_thesis: verum
end;
theorem Th200: :: MEMBER_1:200
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a ** (A \+\ B) = (a ** A) \+\ (a ** B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds
a ** (A \+\ B) = (a ** A) \+\ (a ** B)
let a be complex number ; ::_thesis: ( a <> 0 implies a ** (A \+\ B) = (a ** A) \+\ (a ** B) )
assume A1: a <> 0 ; ::_thesis: a ** (A \+\ B) = (a ** A) \+\ (a ** B)
thus a ** (A \+\ B) = (a ** (A \ B)) \/ (a ** (B \ A)) by Th92
.= ((a ** A) \ (a ** B)) \/ (a ** (B \ A)) by A1, Th199
.= (a ** A) \+\ (a ** B) by A1, Th199 ; ::_thesis: verum
end;
theorem Th201: :: MEMBER_1:201
for A being complex-membered set holds 0 ** A c= {0}
proof
let A be complex-membered set ; ::_thesis: 0 ** A c= {0}
let a be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not a in 0 ** A or a in {0} )
assume a in 0 ** A ; ::_thesis: a in {0}
then consider c1, c2 being Element of COMPLEX such that
A1: a = c1 * c2 and
A2: c1 in {0} and
c2 in A ;
c1 = 0 by A2, TARSKI:def_1;
hence a in {0} by A1, TARSKI:def_1; ::_thesis: verum
end;
theorem :: MEMBER_1:202
for A being complex-membered set st A <> {} holds
0 ** A = {0}
proof
let A be complex-membered set ; ::_thesis: ( A <> {} implies 0 ** A = {0} )
assume A1: A <> {} ; ::_thesis: 0 ** A = {0}
A2: {0} c= 0 ** A
proof
set x = the Element of A;
let a be Nat; :: according to MEMBERED:def_12 ::_thesis: ( not a in {0} or a in 0 ** A )
assume A3: a in {0} ; ::_thesis: a in 0 ** A
the Element of A in COMPLEX by XCMPLX_0:def_2;
then A4: 0 * the Element of A in { (0 * c) where c is Element of COMPLEX : c in A } by A1;
0 ** A = { (0 * c) where c is Element of COMPLEX : c in A } by Th194;
hence a in 0 ** A by A3, A4, TARSKI:def_1; ::_thesis: verum
end;
0 ** A c= {0} by Th201;
hence 0 ** A = {0} by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MEMBER_1:203
for A being complex-membered set holds 1 ** A = A
proof
let A be complex-membered set ; ::_thesis: 1 ** A = A
let a be complex number ; :: according to MEMBERED:def_13 ::_thesis: ( ( not a in 1 ** A or a in A ) & ( not a in A or a in 1 ** A ) )
hereby ::_thesis: ( not a in A or a in 1 ** A )
assume a in 1 ** A ; ::_thesis: a in A
then consider c1, c2 being Element of COMPLEX such that
A1: a = c1 * c2 and
A2: c1 in {1} and
A3: c2 in A ;
c1 = 1 by A2, TARSKI:def_1;
hence a in A by A1, A3; ::_thesis: verum
end;
assume a in A ; ::_thesis: a in 1 ** A
then 1 * a in { (1 * c) where c is Element of COMPLEX : c in A } ;
hence a in 1 ** A by Th194; ::_thesis: verum
end;
theorem :: MEMBER_1:204
for A being complex-membered set
for a, b being complex number holds (a * b) ** A = a ** (b ** A)
proof
let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a * b) ** A = a ** (b ** A)
let a, b be complex number ; ::_thesis: (a * b) ** A = a ** (b ** A)
thus (a * b) ** A = ({a} ** {b}) ** A by Th98
.= a ** (b ** A) by Th90 ; ::_thesis: verum
end;
theorem :: MEMBER_1:205
for A, B being complex-membered set
for a being complex number holds a ** (A ** B) = (a ** A) ** B by Th90;
theorem :: MEMBER_1:206
for A being complex-membered set
for a, b being complex number holds (a + b) ** A c= (a ** A) ++ (b ** A)
proof
let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a + b) ** A c= (a ** A) ++ (b ** A)
let a, b be complex number ; ::_thesis: (a + b) ** A c= (a ** A) ++ (b ** A)
{a} ++ {b} = {(a + b)} by Th51;
hence (a + b) ** A c= (a ** A) ++ (b ** A) by Th95; ::_thesis: verum
end;
theorem :: MEMBER_1:207
for A being complex-membered set
for a, b being complex number holds (a - b) ** A c= (a ** A) -- (b ** A)
proof
let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a - b) ** A c= (a ** A) -- (b ** A)
let a, b be complex number ; ::_thesis: (a - b) ** A c= (a ** A) -- (b ** A)
{a} -- {b} = {(a - b)} by Th75;
hence (a - b) ** A c= (a ** A) -- (b ** A) by Th96; ::_thesis: verum
end;
theorem Th208: :: MEMBER_1:208
for B, C being complex-membered set
for a being complex number holds a ** (B ++ C) = (a ** B) ++ (a ** C)
proof
let B, C be complex-membered set ; ::_thesis: for a being complex number holds a ** (B ++ C) = (a ** B) ++ (a ** C)
let a be complex number ; ::_thesis: a ** (B ++ C) = (a ** B) ++ (a ** C)
A1: (a ** B) ++ (a ** C) c= a ** (B ++ C)
proof
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in (a ** B) ++ (a ** C) or z in a ** (B ++ C) )
assume z in (a ** B) ++ (a ** C) ; ::_thesis: z in a ** (B ++ C)
then consider c, c1 being Element of COMPLEX such that
A2: z = c + c1 and
A3: c in a ** B and
A4: c1 in a ** C ;
consider c3 being Element of COMPLEX such that
A5: c1 = a * c3 and
A6: c3 in C by A4, Th195;
consider c2 being Element of COMPLEX such that
A7: c = a * c2 and
A8: c2 in B by A3, Th195;
A9: c2 + c3 in B ++ C by A8, A6;
z = a * (c2 + c3) by A2, A7, A5;
hence z in a ** (B ++ C) by A9, Th193; ::_thesis: verum
end;
a ** (B ++ C) c= (a ** B) ++ (a ** C) by Th95;
hence a ** (B ++ C) = (a ** B) ++ (a ** C) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MEMBER_1:209
for B, C being complex-membered set
for a being complex number holds a ** (B -- C) = (a ** B) -- (a ** C)
proof
let B, C be complex-membered set ; ::_thesis: for a being complex number holds a ** (B -- C) = (a ** B) -- (a ** C)
let a be complex number ; ::_thesis: a ** (B -- C) = (a ** B) -- (a ** C)
thus a ** (B -- C) = (a ** B) ++ (a ** (-- C)) by Th208
.= (a ** B) -- (a ** C) by Th94 ; ::_thesis: verum
end;
definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcf /// F -> set equals :: MEMBER_1:def 21
{f} /// F;
coherence
{f} /// F is set ;
end;
:: deftheorem defines /// MEMBER_1:def_21_:_
for F being ext-real-membered set
for f being ext-real number holds f /// F = {f} /// F;
theorem Th210: :: MEMBER_1:210
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
f / g in f /// G
proof
let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds
f / g in f /// G
let g, f be ext-real number ; ::_thesis: ( g in G implies f / g in f /// G )
f in {f} by TARSKI:def_1;
hence ( g in G implies f / g in f /// G ) by Th102; ::_thesis: verum
end;
theorem Th211: :: MEMBER_1:211
for F being ext-real-membered set
for f being ext-real number holds f /// F = { (f / w) where w is Element of ExtREAL : w in F }
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds f /// F = { (f / w) where w is Element of ExtREAL : w in F }
let f be ext-real number ; ::_thesis: f /// F = { (f / w) where w is Element of ExtREAL : w in F }
thus f /// F c= { (f / w) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f / w) where w is Element of ExtREAL : w in F } c= f /// F
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f /// F or e in { (f / w) where w is Element of ExtREAL : w in F } )
assume e in f /// F ; ::_thesis: e in { (f / w) where w is Element of ExtREAL : w in F }
then consider w1, w2 being Element of ExtREAL such that
A1: e = w1 * w2 and
A2: w1 in {f} and
A3: w2 in F "" ;
consider w3 being Element of ExtREAL such that
A4: ( w2 = w3 " & w3 in F ) by A3;
( w1 * (w3 ") = w1 / w3 & w1 = f ) by A2, TARSKI:def_1;
hence e in { (f / w) where w is Element of ExtREAL : w in F } by A1, A4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (f / w) where w is Element of ExtREAL : w in F } or e in f /// F )
assume e in { (f / w) where w is Element of ExtREAL : w in F } ; ::_thesis: e in f /// F
then ex w being Element of ExtREAL st
( e = f / w & w in F ) ;
hence e in f /// F by Th210; ::_thesis: verum
end;
theorem :: MEMBER_1:212
for F being ext-real-membered set
for f being ext-real number
for e being set st e in f /// F holds
ex w being Element of ExtREAL st
( e = f / w & w in F )
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number
for e being set st e in f /// F holds
ex w being Element of ExtREAL st
( e = f / w & w in F )
let f be ext-real number ; ::_thesis: for e being set st e in f /// F holds
ex w being Element of ExtREAL st
( e = f / w & w in F )
let e be set ; ::_thesis: ( e in f /// F implies ex w being Element of ExtREAL st
( e = f / w & w in F ) )
f /// F = { (f / w) where w is Element of ExtREAL : w in F } by Th211;
hence ( e in f /// F implies ex w being Element of ExtREAL st
( e = f / w & w in F ) ) ; ::_thesis: verum
end;
registration
let F be empty set ;
let f be ext-real number ;
clusterf /// F -> empty ;
coherence
f /// F is empty ;
end;
registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterf /// F -> non empty ;
coherence
not f /// F is empty ;
end;
registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterf /// F -> ext-real-membered ;
coherence
f /// F is ext-real-membered ;
end;
definition
let A be complex-membered set ;
let a be complex number ;
funca /// A -> set equals :: MEMBER_1:def 22
{a} /// A;
coherence
{a} /// A is set ;
end;
:: deftheorem defines /// MEMBER_1:def_22_:_
for A being complex-membered set
for a being complex number holds a /// A = {a} /// A;
theorem Th213: :: MEMBER_1:213
for A being complex-membered set
for b, a being complex number st b in A holds
a / b in a /// A
proof
let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds
a / b in a /// A
let b, a be complex number ; ::_thesis: ( b in A implies a / b in a /// A )
a in {a} by TARSKI:def_1;
hence ( b in A implies a / b in a /// A ) by Th116; ::_thesis: verum
end;
theorem Th214: :: MEMBER_1:214
for A being complex-membered set
for a being complex number holds a /// A = { (a / c) where c is Element of COMPLEX : c in A }
proof
let A be complex-membered set ; ::_thesis: for a being complex number holds a /// A = { (a / c) where c is Element of COMPLEX : c in A }
let a be complex number ; ::_thesis: a /// A = { (a / c) where c is Element of COMPLEX : c in A }
thus a /// A c= { (a / c) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (a / c) where c is Element of COMPLEX : c in A } c= a /// A
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in a /// A or e in { (a / c) where c is Element of COMPLEX : c in A } )
assume e in a /// A ; ::_thesis: e in { (a / c) where c is Element of COMPLEX : c in A }
then consider c1, c2 being Element of COMPLEX such that
A1: e = c1 * c2 and
A2: ( c1 in {a} & c2 in A "" ) ;
A3: c1 * c2 = c1 / (c2 ") ;
( c2 " in A & c1 = a ) by A2, Th29, TARSKI:def_1;
hence e in { (a / c) where c is Element of COMPLEX : c in A } by A1, A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (a / c) where c is Element of COMPLEX : c in A } or e in a /// A )
assume e in { (a / c) where c is Element of COMPLEX : c in A } ; ::_thesis: e in a /// A
then ex c being Element of COMPLEX st
( e = a / c & c in A ) ;
hence e in a /// A by Th213; ::_thesis: verum
end;
theorem Th215: :: MEMBER_1:215
for A being complex-membered set
for a being complex number
for e being set st e in a /// A holds
ex c being Element of COMPLEX st
( e = a / c & c in A )
proof
let A be complex-membered set ; ::_thesis: for a being complex number
for e being set st e in a /// A holds
ex c being Element of COMPLEX st
( e = a / c & c in A )
let a be complex number ; ::_thesis: for e being set st e in a /// A holds
ex c being Element of COMPLEX st
( e = a / c & c in A )
let e be set ; ::_thesis: ( e in a /// A implies ex c being Element of COMPLEX st
( e = a / c & c in A ) )
a /// A = { (a / c) where c is Element of COMPLEX : c in A } by Th214;
hence ( e in a /// A implies ex c being Element of COMPLEX st
( e = a / c & c in A ) ) ; ::_thesis: verum
end;
registration
let A be empty set ;
let a be complex number ;
clustera /// A -> empty ;
coherence
a /// A is empty ;
end;
registration
let A be non empty complex-membered set ;
let a be complex number ;
clustera /// A -> non empty ;
coherence
not a /// A is empty ;
end;
registration
let A be complex-membered set ;
let a be complex number ;
clustera /// A -> complex-membered ;
coherence
a /// A is complex-membered ;
end;
registration
let A be real-membered set ;
let a be real number ;
clustera /// A -> real-membered ;
coherence
a /// A is real-membered ;
end;
registration
let A be rational-membered set ;
let a be rational number ;
clustera /// A -> rational-membered ;
coherence
a /// A is rational-membered ;
end;
registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifya /// A with f /// F when A = F, a = f;
compatibility
( A = F & a = f implies a /// A = f /// F ) ;
end;
theorem Th216: :: MEMBER_1:216
for A, B being complex-membered set
for a being complex number st a <> 0 & a /// A c= a /// B holds
A c= B
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & a /// A c= a /// B holds
A c= B
let a be complex number ; ::_thesis: ( a <> 0 & a /// A c= a /// B implies A c= B )
assume that
A1: a <> 0 and
A2: a /// A c= a /// B ; ::_thesis: A c= B
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B )
assume z in A ; ::_thesis: z in B
then a / z in a /// A by Th213;
then consider c being Element of COMPLEX such that
A3: a / z = a / c and
A4: c in B by A2, Th215;
z " = c " by A1, A3, XCMPLX_1:5;
hence z in B by A4, XCMPLX_1:201; ::_thesis: verum
end;
theorem :: MEMBER_1:217
for A, B being complex-membered set
for a being complex number st a <> 0 & a /// A = a /// B holds
A = B
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & a /// A = a /// B holds
A = B
let a be complex number ; ::_thesis: ( a <> 0 & a /// A = a /// B implies A = B )
assume ( a <> 0 & a /// A = a /// B ) ; ::_thesis: A = B
then ( A c= B & B c= A ) by Th216;
hence A = B by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MEMBER_1:218
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a /// (A /\ B) = (a /// A) /\ (a /// B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds
a /// (A /\ B) = (a /// A) /\ (a /// B)
let a be complex number ; ::_thesis: ( a <> 0 implies a /// (A /\ B) = (a /// A) /\ (a /// B) )
assume A1: a <> 0 ; ::_thesis: a /// (A /\ B) = (a /// A) /\ (a /// B)
thus a /// (A /\ B) = a ** ((A "") /\ (B "")) by Th33
.= (a ** (A "")) /\ (a ** (B "")) by A1, Th198
.= (a /// A) /\ (a /// B) ; ::_thesis: verum
end;
theorem :: MEMBER_1:219
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a /// (A \ B) = (a /// A) \ (a /// B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds
a /// (A \ B) = (a /// A) \ (a /// B)
let a be complex number ; ::_thesis: ( a <> 0 implies a /// (A \ B) = (a /// A) \ (a /// B) )
assume A1: a <> 0 ; ::_thesis: a /// (A \ B) = (a /// A) \ (a /// B)
thus a /// (A \ B) = a ** ((A "") \ (B "")) by Th34
.= (a ** (A "")) \ (a ** (B "")) by A1, Th199
.= (a /// A) \ (a /// B) ; ::_thesis: verum
end;
theorem :: MEMBER_1:220
for A, B being complex-membered set
for a being complex number st a <> 0 holds
a /// (A \+\ B) = (a /// A) \+\ (a /// B)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds
a /// (A \+\ B) = (a /// A) \+\ (a /// B)
let a be complex number ; ::_thesis: ( a <> 0 implies a /// (A \+\ B) = (a /// A) \+\ (a /// B) )
assume A1: a <> 0 ; ::_thesis: a /// (A \+\ B) = (a /// A) \+\ (a /// B)
thus a /// (A \+\ B) = a ** ((A "") \+\ (B "")) by Th35
.= (a ** (A "")) \+\ (a ** (B "")) by A1, Th200
.= (a /// A) \+\ (a /// B) ; ::_thesis: verum
end;
theorem :: MEMBER_1:221
for A being complex-membered set
for a, b being complex number holds (a + b) /// A c= (a /// A) ++ (b /// A)
proof
let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a + b) /// A c= (a /// A) ++ (b /// A)
let a, b be complex number ; ::_thesis: (a + b) /// A c= (a /// A) ++ (b /// A)
{a} ++ {b} = {(a + b)} by Th51;
hence (a + b) /// A c= (a /// A) ++ (b /// A) by Th95; ::_thesis: verum
end;
theorem :: MEMBER_1:222
for A being complex-membered set
for a, b being complex number holds (a - b) /// A c= (a /// A) -- (b /// A)
proof
let A be complex-membered set ; ::_thesis: for a, b being complex number holds (a - b) /// A c= (a /// A) -- (b /// A)
let a, b be complex number ; ::_thesis: (a - b) /// A c= (a /// A) -- (b /// A)
{a} -- {b} = {(a - b)} by Th75;
hence (a - b) /// A c= (a /// A) -- (b /// A) by Th96; ::_thesis: verum
end;
definition
let F be ext-real-membered set ;
let f be ext-real number ;
funcF /// f -> set equals :: MEMBER_1:def 23
F /// {f};
coherence
F /// {f} is set ;
end;
:: deftheorem defines /// MEMBER_1:def_23_:_
for F being ext-real-membered set
for f being ext-real number holds F /// f = F /// {f};
theorem Th223: :: MEMBER_1:223
for G being ext-real-membered set
for g, f being ext-real number st g in G holds
g / f in G /// f
proof
let G be ext-real-membered set ; ::_thesis: for g, f being ext-real number st g in G holds
g / f in G /// f
let g, f be ext-real number ; ::_thesis: ( g in G implies g / f in G /// f )
f in {f} by TARSKI:def_1;
hence ( g in G implies g / f in G /// f ) by Th102; ::_thesis: verum
end;
theorem Th224: :: MEMBER_1:224
for F being ext-real-membered set
for f being ext-real number holds F /// f = { (w / f) where w is Element of ExtREAL : w in F }
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number holds F /// f = { (w / f) where w is Element of ExtREAL : w in F }
let f be ext-real number ; ::_thesis: F /// f = { (w / f) where w is Element of ExtREAL : w in F }
thus F /// f c= { (w / f) where w is Element of ExtREAL : w in F } :: according to XBOOLE_0:def_10 ::_thesis: { (w / f) where w is Element of ExtREAL : w in F } c= F /// f
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F /// f or e in { (w / f) where w is Element of ExtREAL : w in F } )
assume e in F /// f ; ::_thesis: e in { (w / f) where w is Element of ExtREAL : w in F }
then consider w1, w2 being Element of ExtREAL such that
A1: ( e = w1 * w2 & w1 in F ) and
A2: w2 in {f} "" ;
consider w3 being Element of ExtREAL such that
A3: w2 = w3 " and
A4: w3 in {f} by A2;
( w1 * (w3 ") = w1 / w3 & w3 = f ) by A4, TARSKI:def_1;
hence e in { (w / f) where w is Element of ExtREAL : w in F } by A1, A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (w / f) where w is Element of ExtREAL : w in F } or e in F /// f )
assume e in { (w / f) where w is Element of ExtREAL : w in F } ; ::_thesis: e in F /// f
then ex w being Element of ExtREAL st
( e = w / f & w in F ) ;
hence e in F /// f by Th223; ::_thesis: verum
end;
theorem :: MEMBER_1:225
for F being ext-real-membered set
for f being ext-real number
for e being set st e in F /// f holds
ex w being Element of ExtREAL st
( e = w / f & w in F )
proof
let F be ext-real-membered set ; ::_thesis: for f being ext-real number
for e being set st e in F /// f holds
ex w being Element of ExtREAL st
( e = w / f & w in F )
let f be ext-real number ; ::_thesis: for e being set st e in F /// f holds
ex w being Element of ExtREAL st
( e = w / f & w in F )
let e be set ; ::_thesis: ( e in F /// f implies ex w being Element of ExtREAL st
( e = w / f & w in F ) )
F /// f = { (w / f) where w is Element of ExtREAL : w in F } by Th224;
hence ( e in F /// f implies ex w being Element of ExtREAL st
( e = w / f & w in F ) ) ; ::_thesis: verum
end;
registration
let F be empty set ;
let f be ext-real number ;
clusterF /// f -> empty ;
coherence
F /// f is empty ;
end;
registration
let F be non empty ext-real-membered set ;
let f be ext-real number ;
clusterF /// f -> non empty ;
coherence
not F /// f is empty ;
end;
registration
let F be ext-real-membered set ;
let f be ext-real number ;
clusterF /// f -> ext-real-membered ;
coherence
F /// f is ext-real-membered ;
end;
definition
let A be complex-membered set ;
let a be complex number ;
funcA /// a -> set equals :: MEMBER_1:def 24
A /// {a};
coherence
A /// {a} is set ;
end;
:: deftheorem defines /// MEMBER_1:def_24_:_
for A being complex-membered set
for a being complex number holds A /// a = A /// {a};
theorem Th226: :: MEMBER_1:226
for A being complex-membered set
for b, a being complex number st b in A holds
b / a in A /// a
proof
let A be complex-membered set ; ::_thesis: for b, a being complex number st b in A holds
b / a in A /// a
let b, a be complex number ; ::_thesis: ( b in A implies b / a in A /// a )
a in {a} by TARSKI:def_1;
hence ( b in A implies b / a in A /// a ) by Th116; ::_thesis: verum
end;
theorem Th227: :: MEMBER_1:227
for A being complex-membered set
for a being complex number holds A /// a = { (c / a) where c is Element of COMPLEX : c in A }
proof
let A be complex-membered set ; ::_thesis: for a being complex number holds A /// a = { (c / a) where c is Element of COMPLEX : c in A }
let a be complex number ; ::_thesis: A /// a = { (c / a) where c is Element of COMPLEX : c in A }
thus A /// a c= { (c / a) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def_10 ::_thesis: { (c / a) where c is Element of COMPLEX : c in A } c= A /// a
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A /// a or e in { (c / a) where c is Element of COMPLEX : c in A } )
assume e in A /// a ; ::_thesis: e in { (c / a) where c is Element of COMPLEX : c in A }
then consider c1, c2 being Element of COMPLEX such that
A1: ( e = c1 * c2 & c1 in A ) and
A2: c2 in {a} "" ;
{a} "" = {(a ")} by Th37;
then ( c1 * c2 = c1 / (c2 ") & c2 = a " ) by A2, TARSKI:def_1;
hence e in { (c / a) where c is Element of COMPLEX : c in A } by A1; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (c / a) where c is Element of COMPLEX : c in A } or e in A /// a )
assume e in { (c / a) where c is Element of COMPLEX : c in A } ; ::_thesis: e in A /// a
then ex c being Element of COMPLEX st
( e = c / a & c in A ) ;
hence e in A /// a by Th226; ::_thesis: verum
end;
theorem Th228: :: MEMBER_1:228
for A being complex-membered set
for a being complex number
for e being set st e in A /// a holds
ex c being Element of COMPLEX st
( e = c / a & c in A )
proof
let A be complex-membered set ; ::_thesis: for a being complex number
for e being set st e in A /// a holds
ex c being Element of COMPLEX st
( e = c / a & c in A )
let a be complex number ; ::_thesis: for e being set st e in A /// a holds
ex c being Element of COMPLEX st
( e = c / a & c in A )
let e be set ; ::_thesis: ( e in A /// a implies ex c being Element of COMPLEX st
( e = c / a & c in A ) )
A /// a = { (c / a) where c is Element of COMPLEX : c in A } by Th227;
hence ( e in A /// a implies ex c being Element of COMPLEX st
( e = c / a & c in A ) ) ; ::_thesis: verum
end;
registration
let A be empty set ;
let a be complex number ;
clusterA /// a -> empty ;
coherence
A /// a is empty ;
end;
registration
let A be non empty complex-membered set ;
let a be complex number ;
clusterA /// a -> non empty ;
coherence
not A /// a is empty ;
end;
registration
let A be complex-membered set ;
let a be complex number ;
clusterA /// a -> complex-membered ;
coherence
A /// a is complex-membered ;
end;
registration
let A be real-membered set ;
let a be real number ;
clusterA /// a -> real-membered ;
coherence
A /// a is real-membered ;
end;
registration
let A be rational-membered set ;
let a be rational number ;
clusterA /// a -> rational-membered ;
coherence
A /// a is rational-membered ;
end;
registration
let A be real-membered set ;
let F be ext-real-membered set ;
let a be real number ;
let f be ext-real number ;
identifyA /// a with F /// f when A = F, a = f;
compatibility
( A = F & a = f implies A /// a = F /// f ) ;
end;
theorem Th229: :: MEMBER_1:229
for A, B being complex-membered set
for a being complex number st a <> 0 & A /// a c= B /// a holds
A c= B
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & A /// a c= B /// a holds
A c= B
let a be complex number ; ::_thesis: ( a <> 0 & A /// a c= B /// a implies A c= B )
assume that
A1: a <> 0 and
A2: A /// a c= B /// a ; ::_thesis: A c= B
let z be complex number ; :: according to MEMBERED:def_7 ::_thesis: ( not z in A or z in B )
assume z in A ; ::_thesis: z in B
then z / a in A /// a by Th226;
then ex c being Element of COMPLEX st
( z / a = c / a & c in B ) by A2, Th228;
hence z in B by A1, XCMPLX_1:5; ::_thesis: verum
end;
theorem :: MEMBER_1:230
for A, B being complex-membered set
for a being complex number st a <> 0 & A /// a = B /// a holds
A = B
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 & A /// a = B /// a holds
A = B
let a be complex number ; ::_thesis: ( a <> 0 & A /// a = B /// a implies A = B )
assume ( a <> 0 & A /// a = B /// a ) ; ::_thesis: A = B
then ( A c= B & B c= A ) by Th229;
hence A = B by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MEMBER_1:231
for A, B being complex-membered set
for a being complex number st a <> 0 holds
(A /\ B) /// a = (A /// a) /\ (B /// a)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds
(A /\ B) /// a = (A /// a) /\ (B /// a)
let a be complex number ; ::_thesis: ( a <> 0 implies (A /\ B) /// a = (A /// a) /\ (B /// a) )
assume A1: a <> 0 ; ::_thesis: (A /\ B) /// a = (A /// a) /\ (B /// a)
A2: {a} "" = {(a ")} by Th37;
thus (A /\ B) /// a = (a ") ** (A /\ B) by Th37
.= ((a ") ** A) /\ ((a ") ** B) by A1, Th198
.= (A /// a) /\ (B /// a) by A2 ; ::_thesis: verum
end;
theorem :: MEMBER_1:232
for A, B being complex-membered set
for a being complex number st a <> 0 holds
(A \ B) /// a = (A /// a) \ (B /// a)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds
(A \ B) /// a = (A /// a) \ (B /// a)
let a be complex number ; ::_thesis: ( a <> 0 implies (A \ B) /// a = (A /// a) \ (B /// a) )
assume A1: a <> 0 ; ::_thesis: (A \ B) /// a = (A /// a) \ (B /// a)
A2: {a} "" = {(a ")} by Th37;
thus (A \ B) /// a = (a ") ** (A \ B) by Th37
.= ((a ") ** A) \ ((a ") ** B) by A1, Th199
.= (A /// a) \ (B /// a) by A2 ; ::_thesis: verum
end;
theorem :: MEMBER_1:233
for A, B being complex-membered set
for a being complex number st a <> 0 holds
(A \+\ B) /// a = (A /// a) \+\ (B /// a)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number st a <> 0 holds
(A \+\ B) /// a = (A /// a) \+\ (B /// a)
let a be complex number ; ::_thesis: ( a <> 0 implies (A \+\ B) /// a = (A /// a) \+\ (B /// a) )
assume A1: a <> 0 ; ::_thesis: (A \+\ B) /// a = (A /// a) \+\ (B /// a)
A2: {a} "" = {(a ")} by Th37;
thus (A \+\ B) /// a = (a ") ** (A \+\ B) by Th37
.= ((a ") ** A) \+\ ((a ") ** B) by A1, Th200
.= (A /// a) \+\ (B /// a) by A2 ; ::_thesis: verum
end;
theorem Th234: :: MEMBER_1:234
for A, B being complex-membered set
for a being complex number holds (A ++ B) /// a = (A /// a) ++ (B /// a)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds (A ++ B) /// a = (A /// a) ++ (B /// a)
let a be complex number ; ::_thesis: (A ++ B) /// a = (A /// a) ++ (B /// a)
thus (A ++ B) /// a = (a ") ** (A ++ B) by Th37
.= ((a ") ** A) ++ ((a ") ** B) by Th208
.= (A /// a) ++ ((a ") ** B) by Th37
.= (A /// a) ++ (B /// a) by Th37 ; ::_thesis: verum
end;
theorem :: MEMBER_1:235
for A, B being complex-membered set
for a being complex number holds (A -- B) /// a = (A /// a) -- (B /// a)
proof
let A, B be complex-membered set ; ::_thesis: for a being complex number holds (A -- B) /// a = (A /// a) -- (B /// a)
let a be complex number ; ::_thesis: (A -- B) /// a = (A /// a) -- (B /// a)
thus (A -- B) /// a = (A /// a) ++ ((-- B) /// a) by Th234
.= (A /// a) -- (B /// a) by Th94 ; ::_thesis: verum
end;