:: Collective Operations on Number-Membered Sets
:: by Artur Korni{\l}owicz
::
:: Received December 19, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, MEMBERED, XCMPLX_0, XXREAL_0, ARYTM_1,
RELAT_1, TARSKI, XBOOLE_0, ARYTM_3, RAT_1, INT_1, CARD_1, MEMBER_1,
NAT_1, REAL_1, XREAL_0, ORDINAL1;
notations TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, RAT_1, INT_1, MEMBERED, XXREAL_3, XXREAL_0;
constructors XCMPLX_0, RAT_1, MEMBERED, ENUMSET1, BINOP_2, XXREAL_3;
registrations XREAL_0, INT_1, RAT_1, ORDINAL1, MEMBERED, XCMPLX_0, NAT_1,
XXREAL_3, XBOOLE_0;
requirements BOOLE, SUBSET, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0, MEMBERED;
equalities XBOOLE_0, XCMPLX_0, XXREAL_3;
expansions MEMBERED;
theorems XCMPLX_0, TARSKI, XBOOLE_0, ENUMSET1, XCMPLX_1, XXREAL_0, XXREAL_3;
begin
reserve w, w1, w2 for Element of ExtREAL;
reserve c, c1, c2 for Complex;
reserve A, B, C, D for complex-membered set;
reserve F, G, H, I for ext-real-membered set;
reserve a, b, s, t, z for Complex;
reserve f, g, h, i, j for ExtReal;
reserve r for Real;
reserve e for set;
definition
let w;
redefine func -w -> Element of ExtREAL; :: redefines - (XXREAL_3, definition)
coherence by XXREAL_0:def 1;
redefine func w" -> Element of ExtREAL; :: redefines " (XXREAL_3, definition)
coherence by XXREAL_0:def 1;
let w1;
redefine func w*w1 -> Element of ExtREAL; :: redefines * (XXREAL_3, definition)
coherence by XXREAL_0:def 1;
end;
registration
let a, b, c, d be Complex;
cluster {a,b,c,d} -> complex-membered;
coherence
by ENUMSET1:def 2;
end;
registration
let a, b, c, d be ExtReal;
cluster {a,b,c,d} -> ext-real-membered;
coherence
by ENUMSET1:def 2;
end;
definition
let F be ext-real-membered set;
func --F -> ext-real-membered set equals
{-w: w in F};
coherence
proof
{-w: w in F} is ext-real-membered
proof
let e be object;
assume e in {-w: w in F};
then ex w st e = -w & w in F;
hence thesis;
end;
hence thesis;
end;
involutiveness
proof
let A, B be ext-real-membered set;
assume
A1: A = {-w: w in B};
thus B c= {-w: w in A}
proof
let z be ExtReal;
A2: z in ExtREAL by XXREAL_0:def 1;
A3: -z in ExtREAL & z = - -z by XXREAL_0:def 1;
assume z in B;
then -z in A by A1,A2;
hence thesis by A3;
end;
let e be object;
assume e in {-w: w in A};
then consider w1 such that
A4: -w1 = e and
A5: w1 in A;
ex w st -w = w1 & w in B by A1,A5;
hence thesis by A4;
end;
end;
theorem Th1:
f in F iff -f in --F
proof
f in ExtREAL by XXREAL_0:def 1;
hence f in F implies -f in --F;
assume -f in --F;
then
A1: ex w st -w = -f & w in F;
- -f = f;
hence thesis by A1;
end;
theorem Th2:
-f in F iff f in --F
proof
- -f = f;
hence thesis by Th1;
end;
registration
let F be empty set;
cluster --F -> empty;
coherence
proof
assume --F is non empty;
then the Element of --F in --F;
then ex w st the Element of --F = -w & w in F;
hence thesis;
end;
end;
registration
let F be ext-real-membered non empty set;
cluster --F -> non empty;
coherence
proof
-the Element of F in --F by Th1;
hence thesis;
end;
end;
Lm1: F c= G implies --F c= --G
proof
assume
A1: F c= G;
let j;
assume j in --F;
then -j in F by Th2;
hence thesis by A1,Th2;
end;
theorem Th3:
F c= G iff --F c= --G
proof
----F = F & ----G = G;
hence thesis by Lm1;
end;
theorem
--F = --G implies F = G
proof
assume --F = --G;
then F c= G & G c= F by Th3;
hence thesis;
end;
theorem Th5:
-- (F \/ G) = (--F) \/ (--G)
proof
let i;
hereby
assume 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;
end;
assume 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 thesis by Th2;
end;
theorem Th6:
-- (F /\ G) = (--F) /\ (--G)
proof
let i;
hereby
assume 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;
end;
assume
A3: 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 thesis by Th2;
end;
theorem Th7:
-- (F \ G) = (--F) \ (--G)
proof
let i;
hereby
assume 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;
end;
assume
A3: 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 thesis by Th2;
end;
theorem Th8:
-- (F \+\ G) = (--F) \+\ (--G)
proof
thus -- (F \+\ G) = --(F\G) \/ --(G\F) by Th5
.= --F \ --G \/ --(G\F) by Th7
.= (--F) \+\ --G by Th7;
end;
theorem Th9:
--{f} = {-f}
proof
let i;
hereby
assume i in --{f};
then consider w 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;
end;
assume 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 thesis by A3;
end;
theorem Th10:
--{f,g} = {-f,-g}
proof
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;
end;
definition
let A be complex-membered set;
func --A -> complex-membered set equals
{-c: c in A};
coherence
proof
{-c: c in A} is complex-membered
proof
let e be object;
assume e in {-c: c in A};
then ex c st e = -c & c in A;
hence thesis;
end;
hence thesis;
end;
involutiveness
proof
let A, B;
assume
A1: A = {-c: c in B};
thus B c= {-c: c in A}
proof
let z;
A2: -z in COMPLEX & z = - -z by XCMPLX_0:def 2;
assume z in B;
then -z in A by A1;
hence thesis by A2;
end;
let e be object;
assume e in {-c: c in A};
then consider r0 being Complex such that
A3: -r0 = e and
A4: r0 in A;
ex c st -c = r0 & c in B by A1,A4;
hence thesis by A3;
end;
end;
theorem Th11:
a in A iff -a in --A
proof
thus a in A implies -a in --A;
assume -a in --A;
then ex c st -c = -a & c in A;
hence thesis;
end;
theorem Th12:
-a in A iff a in --A
proof
- -a = a;
hence thesis by Th11;
end;
registration
let A be empty set;
cluster --A -> empty;
coherence
proof
assume --A is non empty;
then the Element of --A in --A;
then ex c st the Element of --A = -c & c in A;
hence thesis;
end;
end;
registration
let A be complex-membered non empty set;
cluster --A -> non empty;
coherence
proof
-the Element of A in --A;
hence thesis;
end;
end;
registration
let A be real-membered set;
cluster --A -> real-membered;
coherence
proof
let e be object;
assume e in --A;
then ex c st e = -c & c in A;
hence thesis;
end;
end;
registration
let A be rational-membered set;
cluster --A -> rational-membered;
coherence
proof
let e be object;
assume e in --A;
then ex c st e = -c & c in A;
hence thesis;
end;
end;
registration
let A be integer-membered set;
cluster --A -> integer-membered;
coherence
proof
let e be object;
assume e in --A;
then ex c st e = -c & c in A;
hence thesis;
end;
end;
registration
let A be real-membered set, F be ext-real-membered set;
identify --A with --F when A = F;
compatibility
proof
assume
A1: A = F;
let a be ExtReal;
hereby
assume
A2: a in --A;
then reconsider b = a as Real;
-b in A by A2,Th12;
hence a in --F by A1,Th2;
end;
assume a in --F;
then consider w such that
A3: a = -w and
A4: w in F;
reconsider b = w as Real by A1,A4;
-b in --A by A1,A4;
hence thesis by A3;
end;
end;
Lm2: A c= B implies --A c= --B
proof
assume
A1: A c= B;
let a;
assume a in --A;
then -a in A by Th12;
hence thesis by A1,Th12;
end;
theorem Th13:
A c= B iff --A c= --B
proof
----A = A & ----B = B;
hence thesis by Lm2;
end;
theorem
--A = --B implies A = B
proof
assume --A = --B;
then A c= B & B c= A by Th13;
hence thesis;
end;
theorem Th15:
-- (A \/ B) = (--A) \/ (--B)
proof
let z;
hereby
assume 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;
end;
assume 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 thesis by Th12;
end;
theorem Th16:
-- (A /\ B) = (--A) /\ (--B)
proof
let z;
hereby
assume 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;
end;
assume
A3: 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 thesis by Th12;
end;
theorem Th17:
-- (A \ B) = (--A) \ (--B)
proof
let z;
hereby
assume 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;
end;
assume
A3: 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 thesis by Th12;
end;
theorem Th18:
-- (A \+\ B) = (--A) \+\ (--B)
proof
thus -- (A \+\ B) = --(A\B) \/ --(B\A) by Th15
.= --A \ --B \/ --(B\A) by Th17
.= (--A) \+\ --B by Th17;
end;
theorem Th19:
--{a} = {-a}
proof
let z;
hereby
assume z in --{a};
then consider c 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;
end;
assume 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 thesis by A3;
end;
theorem Th20:
--{a,b} = {-a,-b}
proof
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;
end;
definition
let F be ext-real-membered set;
func F"" -> ext-real-membered set equals
{w": w in F};
coherence
proof
{w": w in F} is ext-real-membered
proof
let e be object;
assume e in {w": w in F};
then ex w st e = w" & w in F;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th21:
f in F implies f" in F""
proof
f in ExtREAL by XXREAL_0:def 1;
hence thesis;
end;
registration
let F be empty set;
cluster F"" -> empty;
coherence
proof
assume F"" is non empty;
then the Element of F"" in F"";
then ex w st the Element of F"" = w" & w in F;
hence thesis;
end;
end;
registration
let F be ext-real-membered non empty set;
cluster F"" -> non empty;
coherence
proof
(the Element of F)" in F"" by Th21;
hence thesis;
end;
end;
theorem
F c= G implies F"" c= G""
proof
assume
A1: F c= G;
let i;
assume i in F"";
then ex w st i = w" & w in F;
hence thesis by A1;
end;
theorem Th23:
(F \/ G)"" = (F"") \/ (G"")
proof
let i;
hereby
assume i in (F\/G)"";
then consider w 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;
end;
assume
A3: i in F"" \/ G"";
per cases by A3,XBOOLE_0:def 3;
suppose
i in F"";
then consider w such that
A4: i = w" and
A5: w in F;
w in F\/G by A5,XBOOLE_0:def 3;
hence thesis by A4;
end;
suppose
i in G"";
then consider w such that
A6: i = w" and
A7: w in G;
w in F\/G by A7,XBOOLE_0:def 3;
hence thesis by A6;
end;
end;
theorem Th24:
(F /\ G)"" c= (F"") /\ (G"")
proof
let i;
assume i in (F/\G)"";
then consider w 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 thesis by A1,A3,XBOOLE_0:def 4;
end;
theorem
--(F"") = (--F)""
proof
let i;
hereby
assume i in --F"";
then -i in F"" by Th2;
then consider w 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;
end;
assume i in (--F)"";
then consider w 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 thesis by Th2;
end;
theorem Th26:
{f}"" = {f"}
proof
let i;
hereby
assume i in {f}"";
then consider w 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;
end;
assume 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 thesis by A3;
end;
theorem Th27:
{f,g}"" = {f",g"}
proof
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;
end;
definition
let A be complex-membered set;
func A"" -> complex-membered set equals
{c": c in A};
coherence
proof
{c": c in A} is complex-membered
proof
let e be object;
assume e in {c": c in A};
then ex c st e = c" & c in A;
hence thesis;
end;
hence thesis;
end;
involutiveness
proof
let A, B;
assume
A1: A = {c": c in B};
thus B c= {c": c in A}
proof
let z;
A2: z" in COMPLEX & z = z" " by XCMPLX_0:def 2;
assume z in B;
then z" in A by A1;
hence thesis by A2;
end;
let e be object;
assume e in {c": c in A};
then consider r0 being Complex such that
A3: r0" = e and
A4: r0 in A;
ex c st c" = r0 & c in B by A1,A4;
hence thesis by A3;
end;
end;
theorem Th28:
a in A iff a" in A""
proof
thus a in A implies a" in A"";
assume a" in A"";
then ex c st c" = a" & c in A;
hence thesis by XCMPLX_1:201;
end;
theorem Th29:
a" in A iff a in A""
proof
a" " = a;
hence thesis by Th28;
end;
registration
let A be empty set;
cluster A"" -> empty;
coherence
proof
assume A"" is non empty;
then the Element of A"" in A"";
then ex c st the Element of A"" = c" & c in A;
hence thesis;
end;
end;
registration
let A be complex-membered non empty set;
cluster A"" -> non empty;
coherence
proof
(the Element of A)" in A"";
hence thesis;
end;
end;
registration
let A be real-membered set;
cluster A"" -> real-membered;
coherence
proof
let e be object;
assume e in A"";
then ex c st e = c" & c in A;
hence thesis;
end;
end;
registration
let A be rational-membered set;
cluster A"" -> rational-membered;
coherence
proof
let e be object;
assume e in A"";
then ex c st e = c" & c in A;
hence thesis;
end;
end;
registration
let A be real-membered set, F be ext-real-membered set;
identify A"" with F"" when A = F;
compatibility
proof
assume
A1: A = F;
let a be ExtReal;
hereby
assume a in A"";
then consider c 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 st w = m & w" = m" by A3,XXREAL_3:def 6;
hence a in F"" by A1,A2,A3;
end;
assume a in F"";
then consider w 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 thesis by A1,A4,A5;
end;
end;
Lm3: A c= B implies A"" c= B""
proof
assume
A1: A c= B;
let a;
assume a in A"";
then a" in A by Th29;
hence thesis by A1,Th29;
end;
theorem Th30:
A c= B iff A"" c= B""
proof
A"""" = A & B"""" = B;
hence thesis by Lm3;
end;
theorem
A"" = B"" implies A = B
proof
assume A"" = B"";
then A c= B & B c= A by Th30;
hence thesis;
end;
theorem Th32:
(A \/ B)"" = (A"") \/ (B"")
proof
let a;
hereby
assume 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;
end;
assume 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 thesis by Th29;
end;
theorem Th33:
(A /\ B)"" = (A"") /\ (B"")
proof
let a;
hereby
assume 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;
end;
assume
A3: 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 thesis by Th29;
end;
theorem Th34:
(A \ B)"" = (A"") \ (B"")
proof
let a;
hereby
assume 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;
end;
assume
A3: 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 thesis by Th29;
end;
theorem Th35:
(A \+\ B)"" = (A"") \+\ (B"")
proof
thus (A \+\ B)"" = ((A\B)"") \/ ((B\A)"") by Th32
.= ((A"")\(B"")) \/ ((B\A)"") by Th34
.= (A"") \+\ (B"") by Th34;
end;
theorem Th36:
--(A"") = (--A)""
proof
let a;
A1: (-a)" = -a" by XCMPLX_1:222;
hereby
assume 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;
end;
assume a in (--A)"";
then a" in --A by Th29;
then -a" in A by Th12;
then -a in A"" by A1,Th29;
hence thesis by Th12;
end;
theorem Th37:
{a}"" = {a"}
proof
let z;
hereby
assume z in {a}"";
then consider c 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;
end;
assume 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 thesis by A3;
end;
theorem Th38:
{a,b}"" = {a",b"}
proof
let z;
hereby
assume z in {a,b}"";
then consider c 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;
end;
A3: a in {a,b} & b in {a,b} by TARSKI:def 2;
assume z in {a",b"};
then
A4: z = a" or z = b" by TARSKI:def 2;
thus thesis by A4,A3;
end;
definition
let F, G be ext-real-membered set;
func F++G -> set equals
{w1+w2: w1 in F & w2 in G};
coherence;
commutativity
proof
let X be set;
let F, G;
assume
A1: X = {w1+w2: w1 in F & w2 in G};
thus X c= {w1+w2: w1 in G & w2 in F}
proof
let e be object;
assume e in X;
then ex w1,w2 st e = w1+w2 & w1 in F & w2 in G by A1;
hence thesis;
end;
let e be object;
assume e in {w1+w2: w1 in G & w2 in F};
then ex w1,w2 st e = w1+w2 & w1 in G & w2 in F;
hence thesis by A1;
end;
end;
theorem Th39:
f in F & g in G implies f+g in F++G
proof
f in ExtREAL & g in ExtREAL by XXREAL_0:def 1;
hence thesis;
end;
registration
let F be empty set;
let G be ext-real-membered set;
cluster F++G -> empty;
coherence
proof
assume F++G is non empty;
then the Element of (F++G) in F++G;
then ex w1,w2 st the Element of (F++G) = w1+w2 & w1 in F & w2 in G;
hence thesis;
end;
cluster G++F -> empty;
coherence;
end;
registration
let F, G be ext-real-membered non empty set;
cluster F++G -> non empty;
coherence
proof
(the Element of F)+the Element of G in F++G by Th39;
hence thesis;
end;
end;
registration
let F, G be ext-real-membered set;
cluster F++G -> ext-real-membered;
coherence
proof
let e be object;
assume e in F++G;
then ex w1,w2 st e = w1+w2 & w1 in F & w2 in G;
hence thesis;
end;
end;
theorem
F c= G & H c= I implies F++H c= G++I
proof
assume
A1: F c= G & H c= I;
let i;
assume i in F++H;
then ex w,w1 st i = w+w1 & w in F & w1 in H;
hence thesis by A1;
end;
theorem Th41:
F ++ (G \/ H) = (F++G) \/ (F++H)
proof
let j;
hereby
assume j in F++(G\/H);
then consider w,w1 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;
end;
assume
A4: j in (F++G)\/(F++H);
per cases by A4,XBOOLE_0:def 3;
suppose
j in F++G;
then consider w,w1 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 thesis by A5;
end;
suppose
j in F++H;
then consider w,w1 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 thesis by A7;
end;
end;
theorem Th42:
F ++ (G /\ H) c= (F++G) /\ (F++H)
proof
let j;
assume j in F++(G/\H);
then consider w,w1 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 thesis by A1,A4,XBOOLE_0:def 4;
end;
theorem Th43:
{f}++{g} = {f+g}
proof
let j;
hereby
assume j in {f}++{g};
then consider w1,w2 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;
end;
A3: f in {f} & g in {g} by TARSKI:def 1;
assume 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 thesis by A4,A3;
end;
theorem Th44:
{f}++{g,h} = {f+g,f+h}
proof
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;
end;
theorem Th45:
{f,g}++{h,i} = {f+h,f+i,g+h,g+i}
proof
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;
end;
definition
let A, B be complex-membered set;
func A++B -> set equals
{c1+c2: c1 in A & c2 in B};
coherence;
commutativity
proof
let X be set;
let A, B;
assume
A1: X = {c1+c2: c1 in A & c2 in B};
thus X c= {c1+c2: c1 in B & c2 in A}
proof
let e be object;
assume e in X;
then ex c1,c2 st e = c1+c2 & c1 in A & c2 in B by A1;
hence thesis;
end;
let e be object;
assume e in {c1+c2: c1 in B & c2 in A};
then ex c1,c2 st e = c1+c2 & c1 in B & c2 in A;
hence thesis by A1;
end;
end;
theorem
a in A & b in B implies a+b in A++B;
registration
let A be empty set;
let B be complex-membered set;
cluster A++B -> empty;
coherence
proof
assume A++B is non empty;
then the Element of (A++B) in A++B;
then ex c1,c2 st the Element of (A++B) = c1+c2 & c1 in A & c2 in B;
hence thesis;
end;
cluster B++A -> empty;
coherence;
end;
registration
let A, B be complex-membered non empty set;
cluster A++B -> non empty;
coherence
proof
(the Element of A)+the Element of B in A++B;
hence thesis;
end;
end;
registration
let A, B be complex-membered set;
cluster A++B -> complex-membered;
coherence
proof
let e be object;
assume e in A++B;
then ex c1,c2 st e = c1+c2 & c1 in A & c2 in B;
hence thesis;
end;
end;
registration
let A, B be real-membered set;
cluster A++B -> real-membered;
coherence
proof
let e be object;
assume e in A++B;
then ex c1,c2 st e = c1+c2 & c1 in A & c2 in B;
hence thesis;
end;
end;
registration
let A, B be rational-membered set;
cluster A++B -> rational-membered;
coherence
proof
let e be object;
assume e in A++B;
then ex c1,c2 st e = c1+c2 & c1 in A & c2 in B;
hence thesis;
end;
end;
registration
let A, B be integer-membered set;
cluster A++B -> integer-membered;
coherence
proof
let e be object;
assume e in A++B;
then ex c1,c2 st e = c1+c2 & c1 in A & c2 in B;
hence thesis;
end;
end;
registration
let A, B be natural-membered set;
cluster A++B -> natural-membered;
coherence
proof
let e be object;
assume e in A++B;
then ex c1,c2 st e = c1+c2 & c1 in A & c2 in B;
hence thesis;
end;
end;
registration
let A, B be real-membered set, F, G be ext-real-membered set;
identify A++B with F++G when A = F, B = G;
compatibility
proof
assume
A1: A = F & B = G;
let a be ExtReal;
hereby
assume a in A++B;
then consider c,c1 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;
end;
assume a in F++G;
then consider w,w1 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 thesis by A1,A5;
end;
end;
theorem Th47:
A c= B & C c= D implies A++C c= B++D
proof
assume
A1: A c= B & C c= D;
let a;
assume a in A++C;
then ex c,c1 st a = c+c1 & c in A & c1 in C;
hence thesis by A1;
end;
theorem Th48:
A ++ (B \/ C) = (A++B) \/ (A++C)
proof
let a;
hereby
assume a in A++(B\/C);
then consider c,c1 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;
end;
assume
A4: a in (A++B)\/(A++C);
per cases by A4,XBOOLE_0:def 3;
suppose
a in A++B;
then consider c,c1 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 thesis by A5;
end;
suppose
a in A++C;
then consider c,c1 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 thesis by A7;
end;
end;
theorem Th49:
A ++ (B /\ C) c= (A++B) /\ (A++C)
proof
let a;
assume a in A++(B/\C);
then consider c,c1 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 thesis by A1,A4,XBOOLE_0:def 4;
end;
theorem Th50:
(A++B)++C = A++(B++C)
proof
let a;
hereby
assume a in A++B++C;
then consider c,c1 such that
A1: a = c+c1 and
A2: c in A++B and
A3: c1 in C;
consider c2,c3 being 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;
end;
assume a in A++(B++C);
then consider c,c1 such that
A7: a = c+c1 & c in A and
A8: c1 in B++C;
consider c2,c3 being 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 thesis by A10;
end;
theorem Th51:
{a}++{b} = {a+b}
proof
let z;
hereby
assume z in {a}++{b};
then consider c1,c2 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;
end;
A3: a in {a} & b in {b} by TARSKI:def 1;
assume z in {a+b};
then
A4: z = a+b by TARSKI:def 1;
thus thesis by A4,A3;
end;
theorem Th52:
{a}++{s,t} = {a+s,a+t}
proof
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;
end;
theorem Th53:
{a,b}++{s,t} = {a+s,a+t,b+s,b+t}
proof
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;
end;
definition
let F, G be ext-real-membered set;
func F--G -> set equals
F ++ --G;
coherence;
end;
theorem Th54:
F--G = {w1-w2: w1 in F & w2 in G}
proof
thus F--G c= {w1-w2: w1 in F & w2 in G}
proof
let e be object;
assume e in F--G;
then consider w1,w2 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 thesis by A2;
end;
let e be object;
assume e in {w1-w2: w1 in F & w2 in G};
then consider w1,w2 such that
A4: e = w1-w2 & w1 in F and
A5: w2 in G;
-w2 in --G by A5;
hence thesis by A4;
end;
theorem Th55:
f in F & g in G implies f-g in F--G
proof
A1: f in ExtREAL & g in ExtREAL by XXREAL_0:def 1;
F--G = {w1-w2: w1 in F & w2 in G} by Th54;
hence thesis by A1;
end;
registration
let F be empty set;
let G be ext-real-membered set;
cluster F--G -> empty;
coherence;
cluster G--F -> empty;
coherence;
end;
registration
let F, G be ext-real-membered non empty set;
cluster F--G -> non empty;
coherence;
end;
registration
let F, G be ext-real-membered set;
cluster F--G -> ext-real-membered;
coherence;
end;
theorem
F c= G & H c= I implies F--H c= G--I
proof
assume
A1: F c= G & H c= I;
let i;
A2: F--H = {w1-w2: w1 in F & w2 in H} by Th54;
assume i in F--H;
then ex w,w1 st i = w-w1 & w in F & w1 in H by A2;
hence thesis by A1,Th55;
end;
theorem
F -- (G \/ H) = (F--G) \/ (F--H)
proof
thus F -- (G \/ H) = F++(--G\/--H) by Th5
.= (F--G) \/ (F--H) by Th41;
end;
theorem
F -- (G /\ H) c= (F--G) /\ (F--H)
proof
F -- (G /\ H) = F++((--G)/\--H) by Th6;
hence thesis by Th42;
end;
Lm4: --(F++G) = (--F) ++ --G
proof
let j;
hereby
assume j in --(F++G);
then consider w such that
A1: j = -w and
A2: w in F++G;
consider w1,w2 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;
end;
assume j in (--F) ++ --G;
then consider w1,w2 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 thesis by A6,Th2;
end;
theorem
--(F++G) = (--F) -- G by Lm4;
theorem Th60:
--(F--G) = (--F) ++ G
proof
thus --(F--G) = (--F)----G by Lm4
.= (--F) ++ G;
end;
theorem
{f}--{g} = {f-g}
proof
thus {f}--{g} = {f}++{-g} by Th9
.= {f-g} by Th43;
end;
theorem
{f}--{h,i} = {f-h,f-i}
proof
thus {f}--{h,i} = {f}++{-h,-i} by Th10
.= {f-h,f-i} by Th44;
end;
theorem
{f,g}--{h} = {f-h,g-h}
proof
thus {f,g}--{h} = {f,g}++{-h} by Th9
.= {f-h,g-h} by Th44;
end;
theorem
{f,g}--{h,i} = {f-h,f-i,g-h,g-i}
proof
thus {f,g}--{h,i} = {f,g}++{-h,-i} by Th10
.= {f-h,f-i,g-h,g-i} by Th45;
end;
definition
let A, B be complex-membered set;
func A--B -> set equals
A ++ --B;
coherence;
end;
theorem Th65:
A--B = {c1-c2: c1 in A & c2 in B}
proof
thus A--B c= {c1-c2: c1 in A & c2 in B}
proof
let e be object;
assume e in A--B;
then consider c1,c2 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 thesis by A2;
end;
let e be object;
assume e in {c1-c2: c1 in A & c2 in B};
then consider c1,c2 such that
A4: e = c1-c2 & c1 in A and
A5: c2 in B;
-c2 in --B by A5;
hence thesis by A4;
end;
theorem Th66:
a in A & b in B implies a-b in A--B
proof
A--B = {c1-c2: c1 in A & c2 in B} by Th65;
hence thesis;
end;
registration
let A be empty set;
let B be complex-membered set;
cluster A--B -> empty;
coherence;
cluster B--A -> empty;
coherence;
end;
registration
let A, B be complex-membered non empty set;
cluster A--B -> non empty;
coherence;
end;
registration
let A, B be complex-membered set;
cluster A--B -> complex-membered;
coherence;
end;
registration
let A, B be real-membered set;
cluster A--B -> real-membered;
coherence;
end;
registration
let A, B be rational-membered set;
cluster A--B -> rational-membered;
coherence;
end;
registration
let A, B be integer-membered set;
cluster A--B -> integer-membered;
coherence;
end;
registration
let A, B be real-membered set, F, G be ext-real-membered set;
identify A--B with F--G when A = F, B = G;
compatibility;
end;
theorem Th67:
A c= B & C c= D implies A--C c= B--D
proof
assume
A1: A c= B & C c= D;
let z;
A2: A--C = {c1-c2: c1 in A & c2 in C} by Th65;
assume z in A--C;
then ex c,c1 st z = c-c1 & c in A & c1 in C by A2;
hence thesis by A1,Th66;
end;
Lm5: --(A++B) = (--A) ++ --B
proof
let a;
hereby
assume a in --(A++B);
then consider c such that
A1: a = -c and
A2: c in A++B;
consider c1,c2 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;
end;
assume a in (--A) ++ --B;
then consider c1,c2 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 thesis by Th12;
end;
theorem
A -- (B \/ C) = (A--B) \/ (A--C)
proof
thus A -- (B \/ C) = A++(--B\/--C) by Th15
.= (A--B) \/ (A--C) by Th48;
end;
theorem
A -- (B /\ C) c= (A--B) /\ (A--C)
proof
A -- (B /\ C) = A++((--B)/\--C) by Th16;
hence thesis by Th49;
end;
theorem
--(A++B) = (--A) -- B by Lm5;
theorem Th71:
--(A--B) = (--A) ++ B
proof
thus --(A--B) = (--A)----B by Lm5
.= (--A) ++ B;
end;
theorem
A++(B--C) = A++B--C by Th50;
theorem
A--(B++C) = A--B--C
proof
thus A--(B++C) = A++(--B--C) by Lm5
.= A--B--C by Th50;
end;
theorem
A--(B--C) = A--B++C
proof
thus A--(B--C) = A++((--B)++C) by Th71
.= A--B++C by Th50;
end;
theorem Th75:
{a}--{b} = {a-b}
proof
thus {a}--{b} = {a}++{-b} by Th19
.= {a-b} by Th51;
end;
theorem
{a}--{s,t} = {a-s,a-t}
proof
thus {a}--{s,t} = {a}++{-s,-t} by Th20
.= {a-s,a-t} by Th52;
end;
theorem
{a,b}--{s} = {a-s,b-s}
proof
thus {a,b}--{s} = {a,b}++{-s} by Th19
.= {a-s,b-s} by Th52;
end;
theorem
{a,b}--{s,t} = {a-s,a-t,b-s,b-t}
proof
thus {a,b}--{s,t} = {a,b}++{-s,-t} by Th20
.= {a-s,a-t,b-s,b-t} by Th53;
end;
definition
let F, G be ext-real-membered set;
func F**G -> set equals
{w1*w2: w1 in F & w2 in G};
coherence;
commutativity
proof
let X be set;
let F, G;
assume
A1: X = {w1*w2: w1 in F & w2 in G};
thus X c= {w1*w2: w1 in G & w2 in F}
proof
let e be object;
assume e in X;
then ex w1,w2 st e = w1*w2 & w1 in F & w2 in G by A1;
hence thesis;
end;
let e be object;
assume e in {w1*w2: w1 in G & w2 in F};
then ex w1,w2 st e = w1*w2 & w1 in G & w2 in F;
hence thesis by A1;
end;
end;
registration
let F be empty set;
let G be ext-real-membered set;
cluster F**G -> empty;
coherence
proof
assume F**G is non empty;
then the Element of (F**G) in F**G;
then ex w1,w2 st the Element of (F**G) = w1*w2 & w1 in F & w2 in G;
hence thesis;
end;
cluster G**F -> empty;
coherence;
end;
registration
let F, G be ext-real-membered set;
cluster F**G -> ext-real-membered;
coherence
proof
let e be object;
assume e in F**G;
then ex w1,w2 st e = w1*w2 & w1 in F & w2 in G;
hence thesis;
end;
end;
theorem Th79:
f in F & g in G implies f*g in F**G
proof
f in ExtREAL & g in ExtREAL by XXREAL_0:def 1;
hence thesis;
end;
registration
let F, G be ext-real-membered non empty set;
cluster F**G -> non empty;
coherence
proof
(the Element of F)*the Element of G in F**G by Th79;
hence thesis;
end;
end;
theorem Th80:
(F**G)**H = F**(G**H)
proof
let i;
hereby
assume i in F**G**H;
then consider w,w1 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;
end;
assume i in F**(G**H);
then consider w,w1 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 thesis by A10;
end;
theorem Th81:
F c= G & H c= I implies F**H c= G**I
proof
assume
A1: F c= G & H c= I;
let i;
assume i in F**H;
then ex w,w1 st i = w*w1 & w in F & w1 in H;
hence thesis by A1;
end;
theorem Th82:
F ** (G \/ H) = (F**G) \/ (F**H)
proof
let j;
hereby
assume j in F**(G\/H);
then consider w,w1 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;
end;
assume
A4: j in (F**G)\/(F**H);
per cases by A4,XBOOLE_0:def 3;
suppose
j in F**G;
then consider w,w1 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 thesis by A5;
end;
suppose
j in F**H;
then consider w,w1 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 thesis by A7;
end;
end;
theorem Th83:
F ** (G /\ H) c= (F**G) /\ (F**H)
proof
let j;
assume j in F**(G/\H);
then consider w,w1 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 thesis by A1,A4,XBOOLE_0:def 4;
end;
theorem
F**--G = --(F**G)
proof
let i;
hereby
assume i in F**--G;
then consider w,w1 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;
end;
assume i in --(F**G);
then -i in F**G by Th2;
then consider w,w1 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 thesis by A5;
end;
theorem Th85:
(F**G)"" = (F"") ** (G"")
proof
let i;
hereby
assume i in (F**G)"";
then consider w such that
A1: i = w" and
A2: w in F**G;
consider w1,w2 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;
end;
assume i in (F"")**(G"");
then consider w,w1 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 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 thesis by A13;
end;
theorem Th86:
{f}**{g} = {f*g}
proof
let i;
hereby
assume i in {f}**{g};
then consider w1,w2 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;
end;
A3: f in {f} & g in {g} by TARSKI:def 1;
assume 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 thesis by A4,A3;
end;
theorem Th87:
{f}**{h,i} = {f*h,f*i}
proof
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;
end;
theorem Th88:
{f,g}**{h,i} = {f*h,f*i,g*h,g*i}
proof
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;
end;
definition
let A, B be complex-membered set;
func A**B -> set equals
{c1*c2: c1 in A & c2 in B};
coherence;
commutativity
proof
let X be set;
let A, B;
assume
A1: X = {c1*c2: c1 in A & c2 in B};
thus X c= {c1*c2: c1 in B & c2 in A}
proof
let e be object;
assume e in X;
then ex c1,c2 st e = c1*c2 & c1 in A & c2 in B by A1;
hence thesis;
end;
let e be object;
assume e in {c1*c2: c1 in B & c2 in A};
then ex c1,c2 st e = c1*c2 & c1 in B & c2 in A;
hence thesis by A1;
end;
end;
theorem
a in A & b in B implies a*b in A**B;
registration
let A be empty set;
let B be complex-membered set;
cluster A**B -> empty;
coherence
proof
assume A**B is non empty;
then the Element of (A**B) in A**B;
then ex c1,c2 st the Element of (A**B) = c1*c2 & c1 in A & c2 in B;
hence thesis;
end;
cluster B**A -> empty;
coherence;
end;
registration
let A, B be complex-membered non empty set;
cluster A**B -> non empty;
coherence
proof
(the Element of A)*the Element of B in A**B;
hence thesis;
end;
end;
registration
let A, B be complex-membered set;
cluster A**B -> complex-membered;
coherence
proof
let e be object;
assume e in A**B;
then ex c1,c2 st e = c1*c2 & c1 in A & c2 in B;
hence thesis;
end;
end;
registration
let A, B be real-membered set;
cluster A**B -> real-membered;
coherence
proof
let e be object;
assume e in A**B;
then ex c1,c2 st e = c1*c2 & c1 in A & c2 in B;
hence thesis;
end;
end;
registration
let A, B be rational-membered set;
cluster A**B -> rational-membered;
coherence
proof
let e be object;
assume e in A**B;
then ex c1,c2 st e = c1*c2 & c1 in A & c2 in B;
hence thesis;
end;
end;
registration
let A, B be integer-membered set;
cluster A**B -> integer-membered;
coherence
proof
let e be object;
assume e in A**B;
then ex c1,c2 st e = c1*c2 & c1 in A & c2 in B;
hence thesis;
end;
end;
registration
let A, B be natural-membered set;
cluster A**B -> natural-membered;
coherence
proof
let e be object;
assume e in A**B;
then ex c1,c2 st e = c1*c2 & c1 in A & c2 in B;
hence thesis;
end;
end;
registration
let A, B be real-membered set, F, G be ext-real-membered set;
identify A**B with F**G when A = F, B = G;
compatibility
proof
assume
A1: A = F & B = G;
let a be ExtReal;
hereby
assume a in A**B;
then consider c,c1 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;
end;
assume a in F**G;
then consider w,w1 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 thesis by A1,A5;
end;
end;
theorem Th90:
(A**B)**C = A**(B**C)
proof
let a;
hereby
assume a in A**B**C;
then consider c,c1 such that
A1: a = c*c1 and
A2: c in A**B and
A3: c1 in C;
consider c2,c3 being 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;
end;
assume a in A**(B**C);
then consider c,c1 such that
A7: a = c*c1 & c in A and
A8: c1 in B**C;
consider c2,c3 being 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 thesis by A10;
end;
theorem
A c= B & C c= D implies A**C c= B**D
proof
assume
A1: A c= B & C c= D;
let a;
assume a in A**C;
then ex c,c1 st a = c*c1 & c in A & c1 in C;
hence thesis by A1;
end;
theorem Th92:
A ** (B \/ C) = (A**B) \/ (A**C)
proof
let a;
hereby
assume a in A**(B\/C);
then consider c,c1 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;
end;
assume
A4: a in (A**B)\/(A**C);
per cases by A4,XBOOLE_0:def 3;
suppose
a in A**B;
then consider c,c1 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 thesis by A5;
end;
suppose
a in A**C;
then consider c,c1 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 thesis by A7;
end;
end;
theorem Th93:
A ** (B /\ C) c= (A**B) /\ (A**C)
proof
let a;
assume a in A**(B/\C);
then consider c,c1 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 thesis by A1,A4,XBOOLE_0:def 4;
end;
theorem Th94:
A**--B = --(A**B)
proof
let a;
hereby
assume a in A**--B;
then consider c,c1 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;
end;
assume a in --(A**B);
then -a in A**B by Th12;
then consider c,c1 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 thesis by A6;
end;
theorem Th95:
A**(B++C) c= A**B ++ A**C
proof
let a;
assume a in A**(B++C);
then consider c,c1 such that
A1: a = c*c1 and
A2: c in A and
A3: c1 in B++C;
consider c2,c3 being 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 thesis by A6;
end;
theorem Th96:
A**(B--C) c= A**B -- A**C
proof
A**(B++--C) c= A**B++A**--C by Th95;
hence thesis by Th94;
end;
theorem Th97:
(A**B)"" = (A"") ** (B"")
proof
let a;
hereby
assume a in (A**B)"";
then consider c such that
A1: a = c" and
A2: c in A**B;
consider c1,c2 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;
end;
assume a in (A"")**(B"");
then consider c,c1 such that
A6: a = c*c1 and
A7: c in A"" and
A8: c1 in B"";
consider c3 being Complex such that
A9: c1 = c3" and
A10: c3 in B by A8;
consider c2 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 thesis by A13;
end;
theorem Th98:
{a}**{b} = {a*b}
proof
let z;
hereby
assume z in {a}**{b};
then consider c1,c2 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;
end;
A3: a in {a} & b in {b} by TARSKI:def 1;
assume z in {a*b};
then
A4: z = a*b by TARSKI:def 1;
thus thesis by A4,A3;
end;
theorem Th99:
{a}**{s,t} = {a*s,a*t}
proof
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;
end;
theorem Th100:
{a,b}**{s,t} = {a*s,a*t,b*s,b*t}
proof
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;
end;
definition
let F, G be ext-real-membered set;
func F///G -> set equals
F**(G"");
coherence;
end;
theorem Th101:
F///G = {w1/w2: w1 in F & w2 in G}
proof
thus F///G c= {w1/w2: w1 in F & w2 in G}
proof
let e be object;
assume e in F///G;
then consider w1,w2 such that
A1: e = w1*w2 and
A2: w1 in F and
A3: w2 in G"";
consider w such that
A4: w2 = w" and
A5: w in G by A3;
e = w1/w by A1,A4;
hence thesis by A2,A5;
end;
let e be object;
assume e in {w1/w2: w1 in F & w2 in G};
then consider w1,w2 such that
A6: e = w1/w2 & w1 in F and
A7: w2 in G;
w2" in G"" by A7;
hence thesis by A6;
end;
theorem Th102:
f in F & g in G implies f/g in F///G
proof
A1: f in ExtREAL & g in ExtREAL by XXREAL_0:def 1;
F///G = {w1/w2: w1 in F & w2 in G} by Th101;
hence thesis by A1;
end;
registration
let F be empty set;
let G be ext-real-membered set;
cluster F///G -> empty;
coherence;
cluster G///F -> empty;
coherence;
end;
registration
let F, G be ext-real-membered non empty set;
cluster F///G -> non empty;
coherence;
end;
registration
let F, G be ext-real-membered set;
cluster F///G -> ext-real-membered;
coherence;
end;
theorem
F c= G & H c= I implies F///H c= G///I
proof
assume
A1: F c= G & H c= I;
let i;
A2: F///H = {w1/w2: w1 in F & w2 in H} by Th101;
assume i in F///H;
then ex w,w1 st i = w/w1 & w in F & w1 in H by A2;
hence thesis by A1,Th102;
end;
theorem
(F \/ G) /// H = (F///H) \/ (G///H) by Th82;
theorem
(F /\ G) /// H c= (F///H) /\ (G///H) by Th83;
theorem
F /// (G \/ H) = (F///G) \/ (F///H)
proof
thus F /// (G \/ H) = F**((G"")\/(H"")) by Th23
.= (F///G) \/ (F///H) by Th82;
end;
theorem
F /// (G /\ H) c= (F///G) /\ (F///H)
proof
(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 thesis by A1;
end;
theorem
(F**G)///H = F**(G///H) by Th80;
theorem
(F///G)**H = (F**H)///G by Th80;
theorem
(F///G)///H = F///(G**H)
proof
thus (F///G)///H = F**((G"")**(H"")) by Th80
.= F///(G**H) by Th85;
end;
theorem
{f}///{g} = {f/g}
proof
thus {f}///{g} = {f}**{g"} by Th26
.= {f/g} by Th86;
end;
theorem
{f}///{h,i} = {f/h,f/i}
proof
thus {f}///{h,i} = {f}**{h",i"} by Th27
.= {f/h,f/i} by Th87;
end;
theorem
{f,g}///{h} = {f/h,g/h}
proof
thus {f,g}///{h} = {f,g}**{h"} by Th26
.= {f/h,g/h} by Th87;
end;
theorem
{f,g}///{h,i} = {f/h,f/i,g/h,g/i}
proof
thus {f,g}///{h,i} = {f,g}**{h",i"} by Th27
.= {f/h,f/i,g/h,g/i} by Th88;
end;
definition
let A, B be complex-membered set;
func A///B -> set equals
A**(B"");
coherence;
end;
theorem Th115:
A///B = {c1/c2: c1 in A & c2 in B}
proof
thus A///B c= {c1/c2: c1 in A & c2 in B}
proof
let e be object;
assume e in A///B;
then consider c1,c2 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 thesis by A2;
end;
let e be object;
assume e in {c1/c2: c1 in A & c2 in B};
then consider c1,c2 such that
A4: e = c1/c2 & c1 in A and
A5: c2 in B;
c2" in B"" by A5;
hence thesis by A4;
end;
theorem Th116:
a in A & b in B implies a/b in A///B
proof
A///B = {c1/c2: c1 in A & c2 in B} by Th115;
hence thesis;
end;
registration
let A be empty set;
let B be complex-membered set;
cluster A///B -> empty;
coherence;
cluster B///A -> empty;
coherence;
end;
registration
let A, B be complex-membered non empty set;
cluster A///B -> non empty;
coherence;
end;
registration
let A, B be complex-membered set;
cluster A///B -> complex-membered;
coherence;
end;
registration
let A, B be real-membered set;
cluster A///B -> real-membered;
coherence;
end;
registration
let A, B be rational-membered set;
cluster A///B -> rational-membered;
coherence;
end;
registration
let A, B be real-membered set, F, G be ext-real-membered set;
identify A///B with F///G when A = F, B = G;
compatibility;
end;
theorem
A c= B & C c= D implies A///C c= B///D
proof
assume
A1: A c= B & C c= D;
let z;
A2: A///C = {c1/c2: c1 in A & c2 in C} by Th115;
assume z in A///C;
then ex c,c1 st z = c/c1 & c in A & c1 in C by A2;
hence thesis by A1,Th116;
end;
theorem
A /// (B \/ C) = (A///B) \/ (A///C)
proof
thus A /// (B \/ C) = A**((B"")\/(C"")) by Th32
.= (A///B) \/ (A///C) by Th92;
end;
theorem
A /// (B /\ C) c= (A///B) /\ (A///C)
proof
A /// (B /\ C) = A**((B"")/\(C"")) by Th33;
hence thesis by Th93;
end;
theorem
A///--B = --(A///B)
proof
thus A///--B = A**--(B"") by Th36
.= --(A///B) by Th94;
end;
theorem
(--A)///B = --(A///B) by Th94;
theorem
(A++B)///C c= A///C ++ B///C by Th95;
theorem
(A--B)///C c= A///C -- B///C
proof
(A++--B)///C c= A///C++(--B)///C by Th95;
hence thesis by Th94;
end;
theorem
(A**B)///C = A**(B///C) by Th90;
theorem
(A///B)**C = (A**C)///B by Th90;
theorem
(A///B)///C = A///(B**C)
proof
thus (A///B)///C = A**((B"")**(C"")) by Th90
.= A///(B**C) by Th97;
end;
theorem
A///(B///C) = (A**C)///B
proof
thus A///(B///C) = A**((B"")**(C"""")) by Th97
.= (A**C)///B by Th90;
end;
theorem
{a}///{b} = {a/b}
proof
thus {a}///{b} = {a}**{b"} by Th37
.= {a/b} by Th98;
end;
theorem
{a}///{s,t} = {a/s,a/t}
proof
thus {a}///{s,t} = {a}**{s",t"} by Th38
.= {a/s,a/t} by Th99;
end;
theorem
{a,b}///{s} = {a/s,b/s}
proof
thus {a,b}///{s} = {a,b}**{s"} by Th37
.= {a/s,b/s} by Th99;
end;
theorem
{a,b}///{s,t} = {a/s,a/t,b/s,b/t}
proof
thus {a,b}///{s,t} = {a,b}**{s",t"} by Th38
.= {a/s,a/t,b/s,b/t} by Th100;
end;
definition
let F be ext-real-membered set;
let f be ExtReal;
func f++F -> set equals
{f}++F;
coherence;
end;
theorem Th132:
g in G implies f+g in f++G
proof
f in {f} by TARSKI:def 1;
hence thesis by Th39;
end;
theorem Th133:
f++F = {f+w: w in F}
proof
thus f++F c= {f+w: w in F}
proof
let e be object;
assume e in f++F;
then consider w1,w2 such that
A1: e = w1+w2 and
A2: w1 in {f} and
A3: w2 in F;
w1 = f by A2,TARSKI:def 1;
hence thesis by A1,A3;
end;
let e be object;
assume e in {f+w: w in F};
then ex w st e = f+w & w in F;
hence thesis by Th132;
end;
theorem Th134:
e in f++F implies ex w st e = f+w & w in F
proof
f++F = {f+w: w in F} by Th133;
hence thesis;
end;
registration
let F be empty set;
let f be ExtReal;
cluster f++F -> empty;
coherence;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster f++F -> non empty;
coherence;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster f++F -> ext-real-membered;
coherence;
end;
theorem Th135:
r++F c= r++G implies F c= G
proof
assume
A1: r++F c= r++G;
let i;
assume i in F;
then r+i in r++F by Th132;
then ex w st r+i = r+w & w in G by A1,Th134;
hence thesis by XXREAL_3:11;
end;
theorem
r++F = r++G implies F = G
proof
assume r++F = r++G;
then F c= G & G c= F by Th135;
hence thesis;
end;
theorem Th137:
r ++ (F /\ G) = (r++F) /\ (r++G)
proof
A1: (r++F) /\ (r++G) c= r ++ (F /\ G)
proof
let j;
assume
A2: j in (r++F) /\ (r++G);
then j in r++F by XBOOLE_0:def 4;
then consider w 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 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 thesis by A3,Th132;
end;
r ++ (F /\ G) c= (r++F) /\ (r++G) by Th42;
hence thesis by A1;
end;
theorem Th138:
(f++F) \ (f++G) c= f ++ (F \ G)
proof
let i;
assume
A1: i in (f++F) \ (f++G);
then consider w such that
A2: i = f+w and
A3: w in F by Th134;
now
assume not w in F\G;
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;
end;
hence thesis by A2,Th132;
end;
theorem Th139:
r ++ (F \ G) = (r++F) \ (r++G)
proof
A1: r ++ (F \ G) c= (r++F) \ (r++G)
proof
let i;
assume i in r ++ (F \ G);
then consider w such that
A2: i = r+w and
A3: w in F\G by Th134;
A4: now
assume r+w in r++G;
then consider w1 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;
end;
r+w in r++F by A3,Th132;
hence thesis by A2,A4,XBOOLE_0:def 5;
end;
(r++F) \ (r++G) c= r ++ (F \ G) by Th138;
hence thesis by A1;
end;
theorem Th140:
r ++ (F \+\ G) = (r++F) \+\ (r++G)
proof
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;
end;
definition
let A be complex-membered set;
let a be Complex;
func a++A -> set equals
{a}++A;
coherence;
end;
theorem Th141:
b in A implies a+b in a++A
proof
a in {a} by TARSKI:def 1;
hence thesis;
end;
theorem Th142:
a++A = {a+c: c in A}
proof
thus a++A c= {a+c: c in A}
proof
let e be object;
assume e in a++A;
then consider c1,c2 such that
A1: e = c1+c2 and
A2: c1 in {a} and
A3: c2 in A;
c1 = a by A2,TARSKI:def 1;
hence thesis by A1,A3;
end;
let e be object;
assume e in {a+c: c in A};
then ex c st e = a+c & c in A;
hence thesis by Th141;
end;
theorem Th143:
e in a++A implies ex c st e = a+c & c in A
proof
a++A = {a+c: c in A} by Th142;
hence thesis;
end;
registration
let A be empty set;
let a be Complex;
cluster a++A -> empty;
coherence;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster a++A -> non empty;
coherence;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster a++A -> complex-membered;
coherence;
end;
registration
let A be real-membered set;
let a be Real;
cluster a++A -> real-membered;
coherence;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster a++A -> rational-membered;
coherence;
end;
registration
let A be integer-membered set;
let a be Integer;
cluster a++A -> integer-membered;
coherence;
end;
registration
let A be natural-membered set;
let a be Nat;
cluster a++A -> natural-membered;
coherence;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify a++A with f++F when a = f, A = F;
compatibility;
end;
theorem Th144:
A c= B iff a++A c= a++B
proof
thus A c= B implies a++A c= a++B by Th47;
assume
A1: a++A c= a++B;
let z;
assume z in A;
then a+z in a++A by Th141;
then ex c st a+z = a+c & c in B by A1,Th143;
hence thesis;
end;
theorem
a++A = a++B implies A = B
proof
assume a++A = a++B;
then A c= B & B c= A by Th144;
hence thesis;
end;
theorem
0++A = A
proof
let a;
hereby
assume a in 0++A;
then consider c1,c2 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;
end;
assume a in A;
then 0+a in {0+c: c in A};
hence thesis by Th142;
end;
theorem
(a+b)++A = a++(b++A)
proof
thus (a+b)++A = {a}++{b}++A by Th51
.= a++(b++A) by Th50;
end;
theorem
a++(A++B) = (a++A)++B by Th50;
theorem Th149:
a ++ (A /\ B) = (a++A) /\ (a++B)
proof
A1: (a++A) /\ (a++B) c= a ++ (A /\ B)
proof
let z;
assume
A2: z in (a++A) /\ (a++B);
then z in a++A by XBOOLE_0:def 4;
then consider c 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 st z = a+c1 & c1 in B by Th143;
then c in A/\B by A3,A4,XBOOLE_0:def 4;
hence thesis by A3,Th141;
end;
a ++ (A /\ B) c= (a++A) /\ (a++B) by Th49;
hence thesis by A1;
end;
theorem Th150:
a ++ (A \ B) = (a++A) \ (a++B)
proof
let z;
hereby
assume z in a ++ (A \ B);
then consider c such that
A1: z = a+c and
A2: c in A\B by Th143;
A3: now
assume a+c in a++B;
then ex c1 st a+c = a+c1 & c1 in B by Th143;
hence contradiction by A2,XBOOLE_0:def 5;
end;
a+c in a++A by A2,Th141;
hence z in (a++A) \ (a++B) by A1,A3,XBOOLE_0:def 5;
end;
assume
A4: z in (a++A) \ (a++B);
then consider c such that
A5: z = a+c and
A6: c in A by Th143;
now
assume not c in A\B;
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;
end;
hence thesis by A5,Th141;
end;
theorem Th151:
a ++ (A \+\ B) = (a++A) \+\ (a++B)
proof
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;
end;
definition
let F be ext-real-membered set;
let f be ExtReal;
func f--F -> set equals
{f}--F;
coherence;
end;
theorem Th152:
g in G implies f-g in f--G
proof
f in {f} by TARSKI:def 1;
hence thesis by Th55;
end;
theorem Th153:
f--F = {f-w: w in F}
proof
thus f--F c= {f-w: w in F}
proof
let e be object;
assume e in f--F;
then consider w1,w2 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 thesis by A1,A3;
end;
let e be object;
assume e in {f-w: w in F};
then ex w st e = f-w & w in F;
hence thesis by Th152;
end;
theorem Th154:
e in f--F implies ex w st e = f-w & w in F
proof
f--F = {f-w: w in F} by Th153;
hence thesis;
end;
registration
let F be empty set;
let f be ExtReal;
cluster f--F -> empty;
coherence;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster f--F -> non empty;
coherence;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster f--F -> ext-real-membered;
coherence;
end;
theorem Th155:
r--F c= r--G implies F c= G
proof
assume
A1: r--F c= r--G;
let i;
assume i in F;
then r-i in r--F by Th152;
then ex w st r-i = r-w & w in G by A1,Th154;
hence thesis by XXREAL_3:12;
end;
theorem
r--F = r--G implies F = G
proof
assume r--F = r--G;
then F c= G & G c= F by Th155;
hence thesis;
end;
theorem Th157:
r -- (F/\G) = (r--F) /\ (r--G)
proof
thus r -- (F/\G) = r ++ ((--F)/\(--G)) by Th6
.= (r++--F) /\ (r++--G) by Th137
.= (r--F) /\ (r--G);
end;
theorem Th158:
r -- (F\G) = (r--F) \ (r--G)
proof
thus r -- (F\G) = r ++ ((--F)\(--G)) by Th7
.= (r++--F) \ (r++--G) by Th139
.= (r--F) \ (r--G);
end;
theorem Th159:
r -- (F\+\G) = (r--F) \+\ (r--G)
proof
thus r -- (F\+\G) = r ++ ((--F)\+\(--G)) by Th8
.= (r++--F) \+\ (r++--G) by Th140
.= (r--F) \+\ (r--G);
end;
definition
let A be complex-membered set;
let a be Complex;
func a--A -> set equals
{a}--A;
coherence;
end;
theorem Th160:
b in A implies a-b in a--A
proof
a in {a} by TARSKI:def 1;
hence thesis by Th66;
end;
theorem Th161:
a--A = {a-c: c in A}
proof
A1: a--A = {c1-c2: c1 in {a} & c2 in A} by Th65;
thus a--A c= {a-c: c in A}
proof
let e be object;
assume e in a--A;
then consider c1,c2 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 thesis by A2,A4;
end;
let e be object;
assume e in {a-c: c in A};
then ex c st e = a-c & c in A;
hence thesis by Th160;
end;
theorem Th162:
e in a--A implies ex c st e = a-c & c in A
proof
a--A = {a-c: c in A} by Th161;
hence thesis;
end;
registration
let A be empty set;
let a be Complex;
cluster a--A -> empty;
coherence;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster a--A -> non empty;
coherence;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster a--A -> complex-membered;
coherence;
end;
registration
let A be real-membered set;
let a be Real;
cluster a--A -> real-membered;
coherence;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster a--A -> rational-membered;
coherence;
end;
registration
let A be integer-membered set;
let a be Integer;
cluster a--A -> integer-membered;
coherence;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify a--A with f--F when a = f, A = F;
compatibility;
end;
theorem Th163:
A c= B iff a--A c= a--B
proof
thus A c= B implies a--A c= a--B by Th67;
assume
A1: a--A c= a--B;
let z;
assume z in A;
then a-z in a--A by Th160;
then ex c st a-z = a-c & c in B by A1,Th162;
hence thesis;
end;
theorem
a--A = a--B implies A = B
proof
assume a--A = a--B;
then A c= B & B c= A by Th163;
hence thesis;
end;
theorem Th165:
a -- (A/\B) = (a--A) /\ (a--B)
proof
thus a -- (A/\B) = a ++ ((--A)/\(--B)) by Th16
.= (a++--A) /\ (a++--B) by Th149
.= (a--A) /\ (a--B);
end;
theorem Th166:
a -- (A\B) = (a--A) \ (a--B)
proof
thus a -- (A\B) = a ++ ((--A)\(--B)) by Th17
.= (a++--A) \ (a++--B) by Th150
.= (a--A) \ (a--B);
end;
theorem Th167:
a -- (A\+\B) = (a--A) \+\ (a--B)
proof
thus a -- (A\+\B) = a ++ ((--A)\+\(--B)) by Th18
.= (a++--A) \+\ (a++--B) by Th151
.= (a--A) \+\ (a--B);
end;
definition
let F be ext-real-membered set;
let f be ExtReal;
func F--f -> set equals
F--{f};
coherence;
end;
theorem Th168:
g in G implies g-f in G--f
proof
f in {f} by TARSKI:def 1;
hence thesis by Th55;
end;
theorem Th169:
F--f = {w-f: w in F}
proof
thus F--f c= {w-f: w in F}
proof
let e be object;
assume e in F--f;
then consider w1,w2 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 thesis by A1;
end;
let e be object;
assume e in {w-f: w in F};
then ex w st e = w-f & w in F;
hence thesis by Th168;
end;
theorem
e in F--f implies ex w st e = w-f & w in F
proof
F--f = {w-f: w in F} by Th169;
hence thesis;
end;
registration
let F be empty set;
let f be ExtReal;
cluster F--f -> empty;
coherence;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster F--f -> non empty;
coherence;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster F--f -> ext-real-membered;
coherence;
end;
theorem
F -- f = -- (f -- F) by Th60;
theorem
f -- F = -- (F -- f) by Th60;
theorem
(F/\G) -- r = (F--r) /\ (G--r)
proof
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;
end;
theorem
(F\G) -- r = (F--r) \ (G--r)
proof
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;
end;
theorem
(F\+\G) -- r = (F--r) \+\ (G--r)
proof
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;
end;
definition
let A be complex-membered set;
let a be Complex;
func A--a -> set equals
A--{a};
coherence;
end;
theorem Th176:
b in A implies b-a in A--a
proof
a in {a} by TARSKI:def 1;
hence thesis by Th66;
end;
theorem Th177:
A--a = {c-a: c in A}
proof
A1: A--a = {c1-c2: c1 in A & c2 in {a}} by Th65;
thus A--a c= {c-a: c in A}
proof
let e be object;
assume e in A--a;
then consider c1,c2 such that
A2: e = c1-c2 & c1 in A and
A3: c2 in {a} by A1;
c2 = a by A3,TARSKI:def 1;
hence thesis by A2;
end;
let e be object;
assume e in {c-a: c in A};
then ex c st e = c-a & c in A;
hence thesis by Th176;
end;
theorem Th178:
e in A--a implies ex c st e = c-a & c in A
proof
A--a = {c-a: c in A} by Th177;
hence thesis;
end;
registration
let A be empty set;
let a be Complex;
cluster A--a -> empty;
coherence;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster A--a -> non empty;
coherence;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster A--a -> complex-membered;
coherence;
end;
registration
let A be real-membered set;
let a be Real;
cluster A--a -> real-membered;
coherence;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster A--a -> rational-membered;
coherence;
end;
registration
let A be integer-membered set;
let a be Integer;
cluster A--a -> integer-membered;
coherence;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify A--a with F--f when a = f, A = F;
compatibility;
end;
theorem Th179:
A c= B iff A--a c= B--a
proof
thus A c= B implies A--a c= B--a by Th67;
assume
A1: A--a c= B--a;
let z;
assume z in A;
then z-a in A--a by Th176;
then ex c st z-a = c-a & c in B by A1,Th178;
hence thesis;
end;
theorem
A--a = B--a implies A = B
proof
assume A--a = B--a;
then A c= B & B c= A by Th179;
hence thesis;
end;
theorem
A -- a = -- (a -- A) by Th71;
theorem
a -- A = -- (A -- a) by Th71;
theorem
(A/\B) -- a = (A--a) /\ (B--a)
proof
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;
end;
theorem
(A\B) -- a = (A--a) \ (B--a)
proof
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;
end;
theorem
(A\+\B) -- a = (A--a) \+\ (B--a)
proof
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;
end;
definition
let F be ext-real-membered set;
let f be ExtReal;
func f**F -> set equals
{f}**F;
coherence;
end;
theorem Th186:
g in G implies f*g in f**G
proof
f in {f} by TARSKI:def 1;
hence thesis by Th79;
end;
theorem Th187:
f**F = {f*w: w in F}
proof
thus f**F c= {f*w: w in F}
proof
let e be object;
assume e in f**F;
then consider w1,w2 such that
A1: e = w1*w2 and
A2: w1 in {f} and
A3: w2 in F;
w1 = f by A2,TARSKI:def 1;
hence thesis by A1,A3;
end;
let e be object;
assume e in {f*w: w in F};
then ex w st e = f*w & w in F;
hence thesis by Th186;
end;
theorem Th188:
e in f**F implies ex w st e = f*w & w in F
proof
f**F = {f*w: w in F} by Th187;
hence thesis;
end;
registration
let F be empty set;
let f be ExtReal;
cluster f**F -> empty;
coherence;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster f**F -> non empty;
coherence;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster f**F -> ext-real-membered;
coherence;
end;
theorem
r <> 0 implies r ** (F/\G) = (r**F) /\ (r**G)
proof
assume
A1: r <> 0;
A2: (r**F) /\ (r**G) c= r ** (F /\ G)
proof
let j;
assume
A3: j in (r**F) /\ (r**G);
then j in r**F by XBOOLE_0:def 4;
then consider w 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 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 thesis by A4,Th186;
end;
r ** (F /\ G) c= (r**F) /\ (r**G) by Th83;
hence thesis by A2;
end;
theorem Th190:
(f**F) \ (f**G) c= f ** (F \ G)
proof
let i;
assume
A1: i in (f**F) \ (f**G);
then consider w such that
A2: i = f*w and
A3: w in F by Th188;
now
assume not w in F\G;
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;
end;
hence thesis by A2,Th186;
end;
theorem Th191:
r <> 0 implies r ** (F\G) = (r**F) \ (r**G)
proof
assume
A1: r <> 0;
A2: r ** (F \ G) c= (r**F) \ (r**G)
proof
let i;
assume i in r ** (F \ G);
then consider w such that
A3: i = r*w and
A4: w in F\G by Th188;
A5: now
assume r*w in r**G;
then consider w1 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;
end;
r*w in r**F by A4,Th186;
hence thesis by A3,A5,XBOOLE_0:def 5;
end;
(r**F) \ (r**G) c= r ** (F \ G) by Th190;
hence thesis by A2;
end;
theorem
r <> 0 implies r ** (F\+\G) = (r**F) \+\ (r**G)
proof
assume
A1: r <> 0;
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;
end;
definition
let A be complex-membered set;
let a be Complex;
func a**A -> set equals
{a}**A;
coherence;
end;
theorem Th193:
b in A implies a*b in a**A
proof
a in {a} by TARSKI:def 1;
hence thesis;
end;
theorem Th194:
a**A = {a*c: c in A}
proof
thus a**A c= {a*c: c in A}
proof
let e be object;
assume e in a**A;
then consider c1,c2 such that
A1: e = c1*c2 and
A2: c1 in {a} and
A3: c2 in A;
c1 = a by A2,TARSKI:def 1;
hence thesis by A1,A3;
end;
let e be object;
assume e in {a*c: c in A};
then ex c st e = a*c & c in A;
hence thesis by Th193;
end;
theorem Th195:
e in a**A implies ex c st e = a*c & c in A
proof
a**A = {a*c: c in A} by Th194;
hence thesis;
end;
registration
let A be empty set;
let a be Complex;
cluster a**A -> empty;
coherence;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster a**A -> non empty;
coherence;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster a**A -> complex-membered;
coherence;
end;
registration
let A be real-membered set;
let a be Real;
cluster a**A -> real-membered;
coherence;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster a**A -> rational-membered;
coherence;
end;
registration
let A be integer-membered set;
let a be Integer;
cluster a**A -> integer-membered;
coherence;
end;
registration
let A be natural-membered set;
let a be Nat;
cluster a**A -> natural-membered;
coherence;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify a**A with f**F when a = f, A = F;
compatibility;
end;
theorem Th196:
a <> 0 & a**A c= a**B implies A c= B
proof
assume that
A1: a <> 0 and
A2: a**A c= a**B;
let z;
assume z in A;
then a*z in a**A by Th193;
then ex c st a*z = a*c & c in B by A2,Th195;
hence thesis by A1,XCMPLX_1:5;
end;
theorem
a <> 0 & a**A = a**B implies A = B
proof
assume a <> 0 & a**A = a**B;
then A c= B & B c= A by Th196;
hence thesis;
end;
theorem Th198:
a <> 0 implies a ** (A/\B) = (a**A) /\ (a**B)
proof
assume
A1: a <> 0;
A2: (a**A) /\ (a**B) c= a ** (A /\ B)
proof
let z;
assume
A3: z in (a**A) /\ (a**B);
then z in a**A by XBOOLE_0:def 4;
then consider c 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 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 thesis by A4,Th193;
end;
a ** (A /\ B) c= (a**A) /\ (a**B) by Th93;
hence thesis by A2;
end;
theorem Th199:
a <> 0 implies a ** (A\B) = (a**A) \ (a**B)
proof
assume
A1: a <> 0;
let z;
hereby
assume z in a ** (A \ B);
then consider c such that
A2: z = a*c and
A3: c in A\B by Th195;
A4: now
assume a*c in a**B;
then consider c1 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;
end;
a*c in a**A by A3,Th193;
hence z in (a**A) \ (a**B) by A2,A4,XBOOLE_0:def 5;
end;
assume
A7: z in (a**A) \ (a**B);
then consider c such that
A8: z = a*c and
A9: c in A by Th195;
now
assume not c in A\B;
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;
end;
hence thesis by A8,Th193;
end;
theorem Th200:
a <> 0 implies a ** (A\+\B) = (a**A) \+\ (a**B)
proof
assume
A1: a <> 0;
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;
end;
theorem Th201:
0**A c= {0}
proof
let a;
assume a in 0**A;
then consider c1,c2 such that
A1: a = c1*c2 and
A2: c1 in {0} and
c2 in A;
c1 = 0 by A2,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
theorem
A <> {} implies 0**A = {0}
proof
assume
A1: A <> {};
A2: {0} c= 0**A
proof
set x = the Element of A;
let a be Nat;
assume
A3: a in {0};
A4: 0*x in {0*c: c in A} by A1;
0**A = {0*c: c in A} by Th194;
hence thesis by A3,A4,TARSKI:def 1;
end;
0**A c= {0} by Th201;
hence thesis by A2;
end;
theorem
1**A = A
proof
let a;
hereby
assume a in 1**A;
then consider c1,c2 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;
end;
assume a in A;
then 1*a in {1*c: c in A};
hence thesis by Th194;
end;
theorem
(a*b)**A = a**(b**A)
proof
thus (a*b)**A = {a}**{b}**A by Th98
.= a**(b**A) by Th90;
end;
theorem
a**(A**B) = (a**A)**B by Th90;
theorem
(a+b)**A c= a**A ++ b**A
proof
{a}++{b} = {a+b} by Th51;
hence thesis by Th95;
end;
theorem
(a-b)**A c= a**A -- b**A
proof
{a}--{b} = {a-b} by Th75;
hence thesis by Th96;
end;
theorem Th208:
a**(B++C) = a**B++a**C
proof
A1: a**B++a**C c= a**(B++C)
proof
let z;
assume z in a**B++a**C;
then consider c,c1 such that
A2: z = c+c1 and
A3: c in a**B and
A4: c1 in a**C;
consider c3 being Complex such that
A5: c1 = a*c3 and
A6: c3 in C by A4,Th195;
consider c2 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 thesis by A9,Th193;
end;
a**(B++C) c= a**B++a**C by Th95;
hence thesis by A1;
end;
theorem
a**(B--C) = a**B--a**C
proof
thus a**(B--C) = a**B++a**--C by Th208
.= a**B--a**C by Th94;
end;
definition
let F be ext-real-membered set;
let f be ExtReal;
func f///F -> set equals
{f}///F;
coherence;
end;
theorem Th210:
g in G implies f/g in f///G
proof
f in {f} by TARSKI:def 1;
hence thesis by Th102;
end;
theorem Th211:
f///F = {f/w: w in F}
proof
thus f///F c= {f/w: w in F}
proof
let e be object;
assume e in f///F;
then consider w1,w2 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 thesis by A1,A4;
end;
let e be object;
assume e in {f/w: w in F};
then ex w st e = f/w & w in F;
hence thesis by Th210;
end;
theorem
e in f///F implies ex w st e = f/w & w in F
proof
f///F = {f/w: w in F} by Th211;
hence thesis;
end;
registration
let F be empty set;
let f be ExtReal;
cluster f///F -> empty;
coherence;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster f///F -> non empty;
coherence;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster f///F -> ext-real-membered;
coherence;
end;
definition
let A be complex-membered set;
let a be Complex;
func a///A -> set equals
{a}///A;
coherence;
end;
theorem Th213:
b in A implies a/b in a///A
proof
a in {a} by TARSKI:def 1;
hence thesis by Th116;
end;
theorem Th214:
a///A = {a/c: c in A}
proof
thus a///A c= {a/c: c in A}
proof
let e be object;
assume e in a///A;
then consider c1,c2 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 thesis by A1,A3;
end;
let e be object;
assume e in {a/c: c in A};
then ex c st e = a/c & c in A;
hence thesis by Th213;
end;
theorem Th215:
e in a///A implies ex c st e = a/c & c in A
proof
a///A = {a/c: c in A} by Th214;
hence thesis;
end;
registration
let A be empty set;
let a be Complex;
cluster a///A -> empty;
coherence;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster a///A -> non empty;
coherence;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster a///A -> complex-membered;
coherence;
end;
registration
let A be real-membered set;
let a be Real;
cluster a///A -> real-membered;
coherence;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster a///A -> rational-membered;
coherence;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify a///A with f///F when a = f, A = F;
compatibility;
end;
theorem Th216:
a <> 0 & a///A c= a///B implies A c= B
proof
assume that
A1: a <> 0 and
A2: a///A c= a///B;
let z;
assume z in A;
then a/z in a///A by Th213;
then consider c such that
A3: a/z = a/c and
A4: c in B by A2,Th215;
z" = c" by A1,A3,XCMPLX_1:5;
hence thesis by A4,XCMPLX_1:201;
end;
theorem
a <> 0 & a///A = a///B implies A = B
proof
assume a <> 0 & a///A = a///B;
then A c= B & B c= A by Th216;
hence thesis;
end;
theorem
a <> 0 implies a /// (A/\B) = (a///A) /\ (a///B)
proof
assume
A1: a <> 0;
thus a /// (A/\B) = a ** ((A"")/\(B"")) by Th33
.= (a**(A"")) /\ (a**(B"")) by A1,Th198
.= (a///A) /\ (a///B);
end;
theorem
a <> 0 implies a /// (A\B) = (a///A) \ (a///B)
proof
assume
A1: a <> 0;
thus a /// (A\B) = a ** ((A"")\(B"")) by Th34
.= (a**(A"")) \ (a**(B"")) by A1,Th199
.= (a///A) \ (a///B);
end;
theorem
a <> 0 implies a /// (A\+\B) = (a///A) \+\ (a///B)
proof
assume
A1: a <> 0;
thus a /// (A\+\B) = a ** ((A"")\+\(B"")) by Th35
.= (a**(A"")) \+\ (a**(B"")) by A1,Th200
.= (a///A) \+\ (a///B);
end;
theorem
(a+b)///A c= a///A ++ b///A
proof
{a}++{b} = {a+b} by Th51;
hence thesis by Th95;
end;
theorem
(a-b)///A c= a///A -- b///A
proof
{a}--{b} = {a-b} by Th75;
hence thesis by Th96;
end;
definition
let F be ext-real-membered set;
let f be ExtReal;
func F///f -> set equals
F///{f};
coherence;
end;
theorem Th223:
g in G implies g/f in G///f
proof
f in {f} by TARSKI:def 1;
hence thesis by Th102;
end;
theorem Th224:
F///f = {w/f: w in F}
proof
thus F///f c= {w/f: w in F}
proof
let e be object;
assume e in F///f;
then consider w1,w2 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 thesis by A1,A3;
end;
let e be object;
assume e in {w/f: w in F};
then ex w st e = w/f & w in F;
hence thesis by Th223;
end;
theorem
e in F///f implies ex w st e = w/f & w in F
proof
F///f = {w/f: w in F} by Th224;
hence thesis;
end;
registration
let F be empty set;
let f be ExtReal;
cluster F///f -> empty;
coherence;
end;
registration
let F be ext-real-membered non empty set;
let f be ExtReal;
cluster F///f -> non empty;
coherence;
end;
registration
let F be ext-real-membered set;
let f be ExtReal;
cluster F///f -> ext-real-membered;
coherence;
end;
definition
let A be complex-membered set;
let a be Complex;
func A///a -> set equals
A///{a};
coherence;
end;
theorem Th226:
b in A implies b/a in A///a
proof
a in {a} by TARSKI:def 1;
hence thesis by Th116;
end;
theorem Th227:
A///a = {c/a: c in A}
proof
thus A///a c= {c/a: c in A}
proof
let e be object;
assume e in A///a;
then consider c1,c2 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 thesis by A1;
end;
let e be object;
assume e in {c/a: c in A};
then ex c st e = c/a & c in A;
hence thesis by Th226;
end;
theorem Th228:
e in A///a implies ex c st e = c/a & c in A
proof
A///a = {c/a: c in A} by Th227;
hence thesis;
end;
registration
let A be empty set;
let a be Complex;
cluster A///a -> empty;
coherence;
end;
registration
let A be complex-membered non empty set;
let a be Complex;
cluster A///a -> non empty;
coherence;
end;
registration
let A be complex-membered set;
let a be Complex;
cluster A///a -> complex-membered;
coherence;
end;
registration
let A be real-membered set;
let a be Real;
cluster A///a -> real-membered;
coherence;
end;
registration
let A be rational-membered set;
let a be Rational;
cluster A///a -> rational-membered;
coherence;
end;
registration
let A be real-membered set, F be ext-real-membered set;
let a be Real, f be ExtReal;
identify A///a with F///f when a = f, A = F;
compatibility;
end;
theorem Th229:
a <> 0 & A///a c= B///a implies A c= B
proof
assume that
A1: a <> 0 and
A2: A///a c= B///a;
let z;
assume z in A;
then z/a in A///a by Th226;
then ex c st z/a = c/a & c in B by A2,Th228;
hence thesis by A1,XCMPLX_1:5;
end;
theorem
a <> 0 & A///a = B///a implies A = B
proof
assume a <> 0 & A///a = B///a;
then A c= B & B c= A by Th229;
hence thesis;
end;
theorem
a <> 0 implies (A/\B) /// a = (A///a) /\ (B///a)
proof
assume
A1: a <> 0;
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;
end;
theorem
a <> 0 implies (A\B) /// a = (A///a) \ (B///a)
proof
assume
A1: a <> 0;
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;
end;
theorem
a <> 0 implies (A\+\B) /// a = (A///a) \+\ (B///a)
proof
assume
A1: a <> 0;
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;
end;
theorem Th234:
(A++B)///a = A///a ++ B///a
proof
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;
end;
theorem
(A--B)///a = A///a -- B///a
proof
thus (A--B)///a = A///a ++ (--B)///a by Th234
.= A///a -- B///a by Th94;
end;