:: Complex Valued Function's Space
:: by Noboru Endou
::
:: Received March 18, 2004
:: Copyright (c) 2004-2016 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 XBOOLE_0, SUBSET_1, FUNCT_2, NUMBERS, BINOP_1, FUNCT_1, BINOP_2,
RELAT_1, ZFMISC_1, XCMPLX_0, FUNCOP_1, CARD_1, COMPLEX1, ARYTM_3,
RLVECT_1, CLVECT_1, ARYTM_1, ALGSTR_0, SUPINF_2, CLOPBAN1, STRUCT_0,
GROUP_1, MESFUNC1, FUNCSDOM, VECTSP_1, CFUNCDOM, VALUED_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, XCMPLX_0, VALUED_0,
VALUED_2, BINOP_2, STRUCT_0, ALGSTR_0, RLVECT_1, COMPLEX1, GROUP_1,
VECTSP_1, FUNCSDOM, CLVECT_1;
constructors DOMAIN_1, BINOP_2, COMPLEX1, FUNCSDOM, CLVECT_1, VECTSP_1,
RELSET_1, VALUED_2, VALUED_0, MEMBERED, NUMBERS, GROUP_1;
registrations XBOOLE_0, RELSET_1, NUMBERS, VECTSP_1, CLVECT_1, ALGSTR_0,
XCMPLX_0, VALUED_2, MEMBERED;
requirements SUBSET, BOOLE, ARITHM, NUMERALS;
definitions RLVECT_1, STRUCT_0, GROUP_1, CLVECT_1, ALGSTR_0, VECTSP_1;
equalities STRUCT_0, CLVECT_1, BINOP_1, ALGSTR_0;
expansions RLVECT_1, STRUCT_0, GROUP_1, CLVECT_1, BINOP_1, VECTSP_1;
theorems FUNCT_2, FUNCOP_1, RLVECT_1, VECTSP_1, TARSKI, COMPLEX1, BINOP_2,
GROUP_1, ALGSTR_0, XCMPLX_0;
schemes BINOP_1, FUNCT_2;
begin :: Operation of complex functions
reserve x1,x2,z for set;
reserve A,B for non empty set;
reserve f,g,h for Element of Funcs(A,COMPLEX);
definition
let A be set;
func ComplexFuncAdd(A) -> BinOp of Funcs(A,COMPLEX) means
:Def1:
for f,g being Element of Funcs(A,COMPLEX) holds it.(f,g) = addcomplex.:(f,g);
existence
proof
deffunc F(Element of Funcs(A,COMPLEX),Element of Funcs(A,COMPLEX)) =
addcomplex.:($1,$2);
consider F being BinOp of Funcs(A,COMPLEX) such that
A1: for x,y being Element of Funcs(A,COMPLEX) holds F.(x,y) = F(x,y)
from BINOP_1:sch 4;
take F;
let f,g be Element of Funcs(A,COMPLEX);
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be BinOp of Funcs(A,COMPLEX) such that
A2: for f,g being Element of Funcs(A,COMPLEX) holds it1.(f,g) =
addcomplex.:(f,g) and
A3: for f,g being Element of Funcs(A,COMPLEX) holds it2.(f,g) =
addcomplex.:(f,g);
now
let f,g be Element of Funcs(A,COMPLEX);
thus it1.(f,g) = addcomplex.:(f,g) by A2
.= it2.(f,g) by A3;
end;
hence thesis;
end;
end;
registration let A be set;
cluster ComplexFuncAdd A -> complex-functions-valued;
coherence;
end;
definition
let A be set;
func ComplexFuncMult(A) -> BinOp of Funcs(A,COMPLEX) means
:Def2:
for f,g
being Element of Funcs(A,COMPLEX) holds it.(f,g) = multcomplex.:(f,g);
existence
proof
deffunc F(Element of Funcs(A,COMPLEX),Element of Funcs(A,COMPLEX)) =
multcomplex.:($1,$2);
consider F being BinOp of Funcs(A,COMPLEX) such that
A1: for x,y being Element of Funcs(A,COMPLEX) holds F.(x,y) = F(x,y)
from BINOP_1:sch 4;
take F;
let f,g be Element of Funcs(A,COMPLEX);
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be BinOp of Funcs(A,COMPLEX) such that
A2: for f,g being Element of Funcs(A,COMPLEX) holds it1.(f,g) =
multcomplex.:(f,g) and
A3: for f,g being Element of Funcs(A,COMPLEX) holds it2.(f,g) =
multcomplex.:(f,g);
now
let f,g be Element of Funcs(A,COMPLEX);
thus it1.(f,g) = multcomplex.:(f,g) by A2
.=it2.(f,g) by A3;
end;
hence thesis;
end;
end;
registration let A be set;
cluster ComplexFuncMult A -> complex-functions-valued;
coherence;
end;
definition
let A be non empty set;
func ComplexFuncExtMult(A) ->
Function of [:COMPLEX,Funcs(A,COMPLEX):], Funcs(A,COMPLEX) means
:Def3:
for z being Complex, f being Element of Funcs(A, COMPLEX),
x being Element of A
holds (it.[z,f]).x = z*(f.x);
existence
proof
deffunc F(Element of COMPLEX,Element of Funcs(A,COMPLEX)) = (multcomplex
[;]($1,$2));
consider F being Function of [:COMPLEX,Funcs(A,COMPLEX):],Funcs(A,COMPLEX)
such that
A1: for z being Element of COMPLEX, f being Element of Funcs(A,COMPLEX
) holds F.(z,f) = F(z,f) from BINOP_1:sch 4;
take F;
let z be Complex,
f be Element of Funcs(A,COMPLEX), x be Element of A;
A2: z in COMPLEX by XCMPLX_0:def 2;
then F.(z,f) = (multcomplex[;](z,f)) by A1;
hence (F.[z,f]).x = multcomplex.(z,f.x) by FUNCOP_1:53,A2
.= z*(f.x) by BINOP_2:def 5;
end;
uniqueness
proof
let it1,it2 be Function of [:COMPLEX,Funcs(A,COMPLEX):],Funcs(A,COMPLEX)
such that
A3: for z being Complex, f being Element of Funcs(A,COMPLEX
), x being Element of A holds (it1.[z,f]).x = z*(f.x) and
A4: for z being Complex, f being Element of Funcs(A,COMPLEX
), x being Element of A holds (it2.[z,f]).x = z*(f.x);
now
let z be Element of COMPLEX, f be Element of Funcs(A,COMPLEX);
now
let x be Element of A;
thus (it1.[z,f]).x = z*(f.x) by A3
.= (it2.[z,f]).x by A4;
end;
hence it1.(z,f) = it2.(z,f) by FUNCT_2:63;
end;
hence thesis;
end;
end;
registration let A be non empty set;
cluster ComplexFuncExtMult A -> complex-functions-valued;
coherence;
end;
definition
let A;
func ComplexFuncZero(A) -> Element of Funcs(A,COMPLEX) equals
A --> 0;
coherence
proof
A -->0c is Function of A,COMPLEX;
hence thesis by FUNCT_2:8;
end;
end;
definition
let A;
func ComplexFuncUnit(A) -> Element of Funcs(A,COMPLEX) equals
A --> 1r;
coherence by FUNCT_2:8;
end;
Lm1: for x being (Element of A), f being Function of A,B holds x in dom f
proof
let x be (Element of A);
let f be Function of A,B;
x in A;
hence thesis by FUNCT_2:def 1;
end;
theorem Th1:
h = (ComplexFuncAdd(A)).(f,g) iff for x being Element of A holds
h.x = f.x + g.x
proof
A1: now
assume
A2: for x being Element of A holds h.x=f.x + g.x;
now
let x be Element of A;
A3: x in dom (addcomplex.:(f,g)) by Lm1;
thus ((ComplexFuncAdd(A)).(f,g)).x = (addcomplex.:(f,g)).x by Def1
.= addcomplex.(f.x,g.x) by A3,FUNCOP_1:22
.= f.x + g.x by BINOP_2:def 3
.= h.x by A2;
end;
hence h = (ComplexFuncAdd(A)).(f,g) by FUNCT_2:63;
end;
now
assume
A4: h = (ComplexFuncAdd(A)).(f,g);
let x be Element of A;
A5: x in dom (addcomplex.:(f,g)) by Lm1;
thus h.x = (addcomplex.:(f,g)).x by A4,Def1
.= addcomplex.(f.x,g.x) by A5,FUNCOP_1:22
.= f.x + g.x by BINOP_2:def 3;
end;
hence thesis by A1;
end;
theorem Th2:
h = (ComplexFuncMult(A)).(f,g) iff for x being Element of A holds
h.x = f.x * g.x
proof
A1: now
assume
A2: for x being Element of A holds h.x=f.x * g.x;
now
let x be Element of A;
A3: x in dom (multcomplex.:(f,g)) by Lm1;
thus ((ComplexFuncMult(A)).(f,g)).x = (multcomplex.:(f,g)).x by Def2
.= multcomplex.(f.x,g.x) by A3,FUNCOP_1:22
.= f.x * g.x by BINOP_2:def 5
.= h.x by A2;
end;
hence h = (ComplexFuncMult(A)).(f,g) by FUNCT_2:63;
end;
now
assume
A4: h = (ComplexFuncMult(A)).(f,g);
let x be Element of A;
A5: x in dom (multcomplex.:(f,g)) by Lm1;
thus h.x = (multcomplex.:(f,g)).x by A4,Def2
.= multcomplex.(f.x,g.x) by A5,FUNCOP_1:22
.= f.x * g.x by BINOP_2:def 5;
end;
hence thesis by A1;
end;
theorem
ComplexFuncZero(A) <> ComplexFuncUnit(A)
proof
set a = the Element of A;
(ComplexFuncZero(A)).a=0c by FUNCOP_1:7;
hence thesis by COMPLEX1:def 4,FUNCOP_1:7;
end;
reserve a,b for Complex;
theorem Th4:
h = (ComplexFuncExtMult(A)).[a,f] iff for x being Element of A
holds h.x = a*(f.x)
proof
thus h = (ComplexFuncExtMult(A)).[a,f] implies for x being Element of A
holds h.x = a*(f.x) by Def3;
reconsider a as Element of COMPLEX by XCMPLX_0:def 2;
now
assume
A1: for x being Element of A holds h.x = a*(f.x);
for x being Element of A holds h.x = ((ComplexFuncExtMult(A)).[a,f]).x
proof
let x be Element of A;
thus h.x = a*(f.x) by A1
.= ((ComplexFuncExtMult(A)).[a,f]).x by Def3;
end;
hence h = (ComplexFuncExtMult(A)).[a,f] by FUNCT_2:63;
end;
hence thesis;
end;
theorem Th5:
(ComplexFuncAdd(A)).(f,g) = (ComplexFuncAdd(A)).(g,f)
proof
now
let x be Element of A;
thus ((ComplexFuncAdd(A)).(f,g)).x = g.x + f.x by Th1
.= ((ComplexFuncAdd(A)).(g,f)).x by Th1;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th6:
(ComplexFuncAdd(A)).(f,(ComplexFuncAdd(A)).(g,h)) = (
ComplexFuncAdd(A)).((ComplexFuncAdd(A)).(f,g),h)
proof
now
let x be Element of A;
thus ((ComplexFuncAdd(A)).(f,(ComplexFuncAdd(A)).(g,h))).x = f.x + ((
ComplexFuncAdd(A)).(g,h)).x by Th1
.= f.x + (g.x + h.x) by Th1
.= (f.x + g.x) + h.x
.= ((ComplexFuncAdd(A)).(f,g)).x + h.x by Th1
.= ((ComplexFuncAdd(A)).((ComplexFuncAdd(A)).(f,g),h)).x by Th1;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th7:
(ComplexFuncMult(A)).(f,g) = (ComplexFuncMult(A)).(g,f)
proof
now
let x be Element of A;
thus ((ComplexFuncMult(A)).(f,g)).x = g.x * f.x by Th2
.= ((ComplexFuncMult(A)).(g,f)).x by Th2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th8:
(ComplexFuncMult(A)).(f,(ComplexFuncMult(A)).(g,h)) = (
ComplexFuncMult(A)).((ComplexFuncMult(A)).(f,g),h)
proof
now
let x be Element of A;
thus ((ComplexFuncMult(A)).(f,(ComplexFuncMult(A)).(g,h))).x = f.x * ((
ComplexFuncMult(A)).(g,h)).x by Th2
.= f.x * (g.x * h.x) by Th2
.= (f.x * g.x) * h.x
.= ((ComplexFuncMult(A)).(f,g)).x * h.x by Th2
.= ((ComplexFuncMult(A)).((ComplexFuncMult(A)).(f,g),h)).x by Th2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th9:
(ComplexFuncMult(A)).(ComplexFuncUnit(A),f) = f
proof
now
let x be Element of A;
thus ((ComplexFuncMult(A)).(ComplexFuncUnit(A),f)).x= (ComplexFuncUnit(A))
.x * f.x by Th2
.=1r * f.x by FUNCOP_1:7
.= f.x by COMPLEX1:def 4;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th10:
(ComplexFuncAdd(A)).(ComplexFuncZero(A),f) = f
proof
now
let x be Element of A;
thus ((ComplexFuncAdd(A)).(ComplexFuncZero(A),f)).x = (ComplexFuncZero(A))
.x + f.x by Th1
.= 0c + f.x by FUNCOP_1:7
.= f.x;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th11:
(ComplexFuncAdd(A)).(f,(ComplexFuncExtMult(A)).[-1r,f]) = ComplexFuncZero(A)
proof
reconsider mj = -1r as Element of COMPLEX by XCMPLX_0:def 2;
now
let x be Element of A;
set y=f.x;
thus ((ComplexFuncAdd(A)).(f,(ComplexFuncExtMult(A)).[mj,f])).x
= f.x + ((ComplexFuncExtMult(A)).[mj,f]).x by Th1
.= f.x + (mj*y) by Th4
.= (ComplexFuncZero(A)).x by COMPLEX1:def 4,FUNCOP_1:7;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th12:
(ComplexFuncExtMult(A)).[1r,f] = f
proof
now
let x be Element of A;
thus ((ComplexFuncExtMult(A)).[1r,f]).x = 1r*(f.x) by Th4
.= f.x by COMPLEX1:def 4;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th13:
for a, b be Complex holds
(ComplexFuncExtMult(A)).[a,(ComplexFuncExtMult(A)).[b,f]] = (
ComplexFuncExtMult(A)).[a*b,f]
proof
let a, b be Complex;
reconsider a,b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider ab = a*b as Element of COMPLEX by XCMPLX_0:def 2;
now
let x be Element of A;
thus ((ComplexFuncExtMult(A)).[a,(ComplexFuncExtMult(A)).[b,f]]).x = a*(((
ComplexFuncExtMult(A)).[b,f]).x) by Th4
.= a*(b*(f.x)) by Th4
.= (a*b)*(f.x)
.= ((ComplexFuncExtMult(A)).[ab,f]).x by Th4;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th14:
for a, b be Complex holds
(ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[b,f]) = (ComplexFuncExtMult(A)).[a+b,f]
proof
let a, b be Complex;
reconsider a, b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider ab = a+b as Element of COMPLEX by XCMPLX_0:def 2;
now
let x be Element of A;
thus ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[b,f])).x = ((ComplexFuncExtMult(A)).[a,f]).x + ((
ComplexFuncExtMult(A)).[b,f]).x by Th1
.= a*(f.x) + ((ComplexFuncExtMult(A)).[b,f]).x by Th4
.= a*(f.x) + b*(f.x) by Th4
.= (a+b)*(f.x)
.= ((ComplexFuncExtMult(A)).[ab,f]).x by Th4;
end;
hence thesis by FUNCT_2:63;
end;
Lm2:
for a be Complex holds
(ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A
)).[a,g]) = (ComplexFuncExtMult(A)).[a,(ComplexFuncAdd(A)).(f,g)]
proof
let a be Complex;
reconsider a as Element of COMPLEX by XCMPLX_0:def 2;
now
let x be Element of A;
thus ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[a,g])).x = ((ComplexFuncExtMult(A)).[a,f]).x + ((
ComplexFuncExtMult(A)).[a,g]).x by Th1
.= a*(f.x) + ((ComplexFuncExtMult(A)).[a,g]).x by Th4
.= a*(f.x) + a*(g.x) by Th4
.= a*(f.x + g.x)
.= a*(((ComplexFuncAdd(A)).(f,g)).x) by Th1
.= ((ComplexFuncExtMult(A)).[a,(ComplexFuncAdd(A)).(f,g)]).x by Th4;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th15:
(ComplexFuncMult(A)).(f,(ComplexFuncAdd(A)).(g,h)) = (
ComplexFuncAdd(A)).((ComplexFuncMult(A)).(f,g),(ComplexFuncMult(A)).(f,h))
proof
now
let x be Element of A;
thus ((ComplexFuncMult(A)).(f,(ComplexFuncAdd(A)).(g,h))).x = f.x * (((
ComplexFuncAdd(A)).(g,h)).x) by Th2
.= f.x * (g.x + h.x) by Th1
.= (f.x * g.x) + (f.x * h.x)
.= ((ComplexFuncMult(A)).(f,g)).x + (f.x * h.x) by Th2
.= ((ComplexFuncMult(A)).(f,g)).x + ((ComplexFuncMult(A)).(f,h)).x by Th2
.= ((ComplexFuncAdd(A)). ((ComplexFuncMult(A)).(f,g),(ComplexFuncMult(
A)).(f,h))).x by Th1;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th16:
(ComplexFuncMult(A)).((ComplexFuncExtMult(A)).[a,f],g) = (
ComplexFuncExtMult(A)).[a,(ComplexFuncMult(A)).(f,g)]
proof
reconsider a as Element of COMPLEX by XCMPLX_0:def 2;
now
let x be Element of A;
thus ((ComplexFuncMult(A)).((ComplexFuncExtMult(A)).[a,f],g)).x
= ((ComplexFuncExtMult(A)).[a,f]).x * g.x by Th2
.= (a*(f.x)) * g.x by Th4
.= a*(f.x * g.x)
.= a*(((ComplexFuncMult(A)).(f,g)).x) by Th2
.= ((ComplexFuncExtMult(A)).[a,(ComplexFuncMult(A)).(f,g)]).x
by Th4;
end;
hence thesis by FUNCT_2:63;
end;
begin :: Complex linear space of complex valued functions
theorem Th17:
ex f,g st (for z st z in A holds (z = x1 implies f.z = 1r) & (z
<>x1 implies f.z = 0)) & for z st z in A holds (z = x1 implies g.z = 0) & (z<>
x1 implies g.z = 1r)
proof
deffunc G(object) = 1r;
deffunc F(object) = 0c;
defpred P[object] means $1 = x1;
A1: for z being object st z in A
holds (P[z] implies G(z) in COMPLEX) & (not P[z] implies
F(z) in COMPLEX);
consider f being Function of A,COMPLEX such that
A2: for z being object st z in A
holds (P[z] implies f.z = G(z)) & (not P[z] implies
f.z = F(z)) from FUNCT_2:sch 5(A1);
A3: for z being object st z in A
holds (P[z] implies F(z) in COMPLEX) & (not P[z] implies
G(z) in COMPLEX);
consider g being Function of A,COMPLEX such that
A4: for z being object st z in A
holds (P[z] implies g.z = F(z)) & (not P[z] implies
g.z = G(z)) from FUNCT_2:sch 5(A3);
reconsider f,g as Element of Funcs(A,COMPLEX) by FUNCT_2:8;
take f,g;
thus thesis by A2,A4;
end;
theorem Th18:
x1 in A & x2 in A & x1<>x2 & (for z st z in A holds (z=x1
implies f.z = 1r) & (z<>x1 implies f.z = 0)) & (for z st z in A holds (z=x1
implies g.z = 0) & (z<>x1 implies g.z = 1r)) implies for a,b st (ComplexFuncAdd
(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g]) =
ComplexFuncZero(A) holds a=0c & b=0c
proof
assume that
A1: x1 in A and
A2: x2 in A and
A3: x1<>x2 and
A4: ( for z st z in A holds (z=x1 implies f.z = 1r) & (z<>x1 implies f.z
= 0))& for z st z in A holds (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1r);
A5: f.x2=0c & g.x2=1r by A2,A3,A4;
A6: f.x1=1r & g.x1=0c by A1,A4;
let a,b;
reconsider x1,x2 as Element of A by A1,A2;
assume
A7: (ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[b,g]) = ComplexFuncZero(A);
reconsider a,b as Element of COMPLEX by XCMPLX_0:def 2;
A8: 0c = ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[b,g])).x2 by FUNCOP_1:7,A7
.= (((ComplexFuncExtMult(A)).[a,f]).x2) + (((ComplexFuncExtMult(A)).[b,g
]).x2) by Th1
.= a*(f.x2) + (((ComplexFuncExtMult(A)).[b,g]).x2) by Th4
.= 0c + b*1r by A5,Th4
.= b by COMPLEX1:def 4;
0c = ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[b,g])).x1 by A7,FUNCOP_1:7
.= (((ComplexFuncExtMult(A)).[a,f]).x1) + (((ComplexFuncExtMult(A)).[b,g
]).x1) by Th1
.= a*(f.x1) + (((ComplexFuncExtMult(A)).[b,g]).x1) by Th4
.= a + b*0c by A6,Th4,COMPLEX1:def 4
.= a;
hence thesis by A8;
end;
theorem
x1 in A & x2 in A & x1<>x2 implies ex f,g st for a,b st (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
]) = ComplexFuncZero(A) holds a=0 & b=0
proof
assume
A1: x1 in A & x2 in A & x1<>x2;
consider f,g such that
A2: ( for z st z in A holds (z=x1 implies f.z = 1r) & (z<>x1 implies f.z
= 0c))& for z st z in A holds (z=x1 implies g.z = 0c) & (z<>x1 implies g.z = 1r
) by Th17;
take f,g;
let a,b;
assume (ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[b,g]) = ComplexFuncZero(A);
hence thesis by A1,A2,Th18;
end;
theorem Th20:
A = {x1,x2} & x1<>x2 & ( for z st z in A holds (z=x1 implies f.z
= 1r) & (z<>x1 implies f.z = 0) ) & ( for z st z in A holds (z=x1 implies g.z =
0) & (z<>x1 implies g.z = 1r) ) implies for h holds ex a,b st h = (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
])
proof
assume that
A1: A = {x1,x2} and
A2: x1<>x2 and
A3: ( for z st z in A holds (z=x1 implies f.z = 1r) & (z<>x1 implies f.z
= 0))& for z st z in A holds (z=x1 implies g.z = 0) & (z<>x1 implies g.z = 1r);
x2 in A by A1,TARSKI:def 2;
then
A4: f.x2=0c & g.x2=1r by A2,A3;
x1 in A by A1,TARSKI:def 2;
then
A5: f.x1=1r & g.x1=0c by A3;
let h;
reconsider x1,x2 as Element of A by A1,TARSKI:def 2;
take a = h.x1, b = h.x2;
now
let x be Element of A;
A6: x = x1 or x = x2 by A1,TARSKI:def 2;
A7: ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[b,g])).x2 = (((ComplexFuncExtMult(A)).[a,f]).x2) + (((
ComplexFuncExtMult(A)).[b,g]).x2) by Th1
.= a*(f.x2) + (((ComplexFuncExtMult(A)).[b,g]).x2) by Th4
.= 0c + b*1r by A4,Th4
.= h.x2 by COMPLEX1:def 4;
((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[b,g])).x1 = (((ComplexFuncExtMult(A)).[a,f]).x1) + (((
ComplexFuncExtMult(A)).[b,g]).x1) by Th1
.= a*(f.x1) + (((ComplexFuncExtMult(A)).[b,g]).x1) by Th4
.= a + b*0c by A5,Th4,COMPLEX1:def 4
.= h.x1;
hence h.x = ((ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(
ComplexFuncExtMult(A)).[b,g])).x by A6,A7;
end;
hence thesis by FUNCT_2:63;
end;
theorem
A = {x1,x2} & x1<>x2 implies ex f,g st for h holds ex a,b st h = (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
])
proof
assume
A1: A = {x1,x2} & x1<>x2;
consider f,g such that
A2: ( for z st z in A holds (z=x1 implies f.z = 1r) & (z<>x1 implies f.z
=0c))& for z st z in A holds (z=x1 implies g.z = 0c) & (z<>x1 implies g.z = 1r)
by Th17;
take f,g;
let h;
thus thesis by A1,A2,Th20;
end;
theorem Th22:
A = {x1,x2} & x1<>x2 implies ex f,g st (for a,b st (
ComplexFuncAdd(A)).((ComplexFuncExtMult(A)).[a,f], (ComplexFuncExtMult(A)).[b,g
]) = ComplexFuncZero(A) holds a=0 & b=0) & for h holds ex a,b st h = (
ComplexFuncAdd(A)). ((ComplexFuncExtMult(A)).[a,f],(ComplexFuncExtMult(A)).[b,g
])
proof
assume that
A1: A = {x1,x2} and
A2: x1<>x2;
consider f,g such that
A3: ( for z st z in A holds (z=x1 implies f.z = 1r) & (z<>x1 implies f.z
=0c))& for z st z in A holds (z=x1 implies g.z = 0c) & (z<>x1 implies g.z = 1r)
by Th17;
take f,g;
x1 in A & x2 in A by A1,TARSKI:def 2;
hence thesis by A1,A2,A3,Th18,Th20;
end;
definition
let A;
func ComplexVectSpace(A) -> strict non empty CLSStruct equals
CLSStruct(# Funcs(A,COMPLEX), ComplexFuncZero A,
ComplexFuncAdd A, ComplexFuncExtMult A #);
coherence;
end;
reserve C for strict non empty CLSStruct,
u,v,w for Element of C;
registration
let A;
cluster ComplexVectSpace A -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital for strict non empty CLSStruct;
coherence
proof let C such that
A1: C = ComplexVectSpace A;
thus u+v = v+u by Th5,A1;
thus (u + v) + w = u + (v + w) by Th6,A1;
thus u+0.C = u
proof
reconsider v=u as Element of Funcs(A,COMPLEX) by A1;
thus u+0.C = (ComplexFuncAdd(A)).(ComplexFuncZero(A),v) by Th5,A1
.= u by Th10;
end;
thus u is right_complementable
proof
reconsider v = u as Element of Funcs(A,COMPLEX) by A1;
reconsider mj = -1r as Element of COMPLEX by XCMPLX_0:def 2;
reconsider w = (ComplexFuncExtMult(A)).[mj,v] as VECTOR of C by A1;
take w;
thus thesis by Th11,A1;
end;
thus for a be Complex, u,v be VECTOR of C holds a * (u + v) = a*u + a*v
by Lm2,A1;
thus for a,b be Complex, v be VECTOR of C holds (a+b)*v = a*v + b*v
by Th14,A1;
thus for a,b be Complex, v be VECTOR of C holds (a*b)*v = a*(b*v) by Th13,A1
;
thus 1r * v = v by Th12,A1;
end;
end;
Lm3: ex A,x1,x2 st A={x1,x2} & x1<>x2
proof
reconsider A={1,2} as non empty set;
take A;
thus thesis;
end;
theorem
ex V being strict ComplexLinearSpace st ex u,v being VECTOR of V st (
for a,b st a*u + b*v = 0.V holds a=0 & b=0) & for w being VECTOR of V
ex a,b st w = a*u + b*v
proof
consider A,x1,x2 such that
A1: A={x1,x2} & x1<>x2 by Lm3;
take V = ComplexVectSpace(A);
consider f,g such that
A2: for a,b st (ComplexFuncAdd(A)).((ComplexFuncExtMult(A)).[a,f], (
ComplexFuncExtMult(A)).[b,g]) = ComplexFuncZero(A) holds a=0c & b=0c and
A3: for h holds ex a,b st h = (ComplexFuncAdd(A)). ((ComplexFuncExtMult(
A)).[a,f],(ComplexFuncExtMult(A)).[b,g]) by A1,Th22;
reconsider u=f, v=g as VECTOR of V;
take u,v;
thus for a,b st a*u + b*v = 0.V holds a=0 & b=0 by A2;
thus for w being VECTOR of V ex a,b st w = a*u + b*v
proof
let w be VECTOR of V;
reconsider h=w as Element of Funcs(A,COMPLEX);
consider a,b such that
A4: h = (ComplexFuncAdd(A)).((ComplexFuncExtMult(A)).[a,f], (
ComplexFuncExtMult(A)).[b,g]) by A3;
h = a*u + b*v by A4;
hence thesis;
end;
end;
definition
let A;
func CRing(A) -> doubleLoopStr equals
doubleLoopStr(# Funcs(A,COMPLEX), ComplexFuncAdd A, ComplexFuncMult A,
ComplexFuncUnit A, ComplexFuncZero A #);
correctness;
end;
registration
let A;
cluster CRing A -> non empty strict;
coherence;
end;
Lm4: now
let A;
let x, e be Element of CRing(A);
assume e = ComplexFuncUnit(A);
hence e * x = x by Th9;
hence x * e = x by Th7;
end;
registration
let A;
cluster CRing(A) -> unital;
coherence
proof
reconsider e = ComplexFuncUnit(A) as Element of CRing(A);
take e;
thus thesis by Lm4;
end;
end;
theorem Th24:
for x,y,z being Element of CRing(A) holds x+y = y+x & (x+y)+z =
x+(y+z) & x+(0.CRing(A)) = x & x is right_complementable & x*y = y*x & (x*y)*z
= x*(y*z) & x*(1.CRing(A)) = x & (1.CRing(A))*x = x & x*(y+z) = x*y + x*z & (y+
z)*x = y*x + z*x
proof
let x,y,z be Element of CRing(A);
set IT = CRing(A);
reconsider f=x as Element of Funcs(A,COMPLEX);
thus x+y = y+x by Th5;
thus (x+y)+z = x+(y+z) by Th6;
thus x+(0.CRing(A)) = (ComplexFuncAdd(A)).(ComplexFuncZero(A),f) by Th5
.= x by Th10;
thus ex t being Element of CRing(A) st x+t=(0.CRing(A))
proof
reconsider mj=-1r as Element of COMPLEX by XCMPLX_0:def 2;
set h = (ComplexFuncExtMult(A)).[mj,f];
reconsider t=h as Element of IT;
take t;
thus thesis by Th11;
end;
thus x*y = y*x by Th7;
thus (x*y)*z = x*(y*z) by Th8;
thus x*(1.CRing(A)) = (ComplexFuncMult(A)).(ComplexFuncUnit(A),f) by Th7
.= x by Th9;
hence (1.CRing(A))*x = x by Th7;
thus x*(y+z) = x*y + x*z by Th15;
hence (y+z)*x = x*y + x*z by Th7
.= y*x + x*z by Th7
.= y*x + z*x by Th7;
end;
theorem
CRing(A) is commutative Ring
proof
for x,y,z being Element of CRing(A) holds x+y = y+x & (x+y)+z = x+(y+z)
& x+(0.CRing(A)) = x & x is right_complementable & x*y = y*x & (x*y)*z = x*(y*z
) & x*(1.CRing(A)) = x & (1.CRing(A))*x = x & x*(y+z) = x*y + x*z & (y+z)*x = y
*x + z*x by Th24;
hence thesis by ALGSTR_0:def 16,GROUP_1:def 3,def 12,RLVECT_1:def 2,def 3
,def 4,VECTSP_1:def 6,def 7;
end;
definition
struct(doubleLoopStr,CLSStruct) ComplexAlgebraStr (# carrier -> set, multF,
addF -> (BinOp of the carrier), Mult -> (Function of [:COMPLEX,the carrier:],
the carrier), OneF,ZeroF -> Element of the carrier #);
end;
registration
cluster non empty for ComplexAlgebraStr;
existence
proof
set X = the non empty set,m = the BinOp of X,M = the Function of [:COMPLEX,X:],
X,u = the Element of X;
take ComplexAlgebraStr(#X,m,m,M,u,u#);
thus the carrier of ComplexAlgebraStr(#X,m,m,M,u,u#) is non empty;
end;
end;
definition
let A;
func CAlgebra(A) -> strict ComplexAlgebraStr equals
ComplexAlgebraStr(#Funcs
(A,COMPLEX),ComplexFuncMult(A),ComplexFuncAdd(A), ComplexFuncExtMult(A),(
ComplexFuncUnit(A)),(ComplexFuncZero(A))#);
correctness;
end;
registration
let A;
cluster CAlgebra(A) -> non empty;
coherence;
end;
Lm5: now
let A;
let x, e be Element of CAlgebra(A);
assume e = ComplexFuncUnit(A);
hence e * x = x by Th9;
hence x * e = x by Th7;
end;
registration
let A;
cluster CAlgebra(A) -> unital;
coherence
proof
reconsider e = ComplexFuncUnit(A) as Element of CAlgebra(A);
take e;
thus thesis by Lm5;
end;
end;
theorem
for x,y,z being Element of CAlgebra(A), a,b holds x + y = y + x
& (x + y) + z = x + (y + z) & x + (0.CAlgebra(A)) = x & x is
right_complementable & x * y = y * x & (x * y) * z = x * (y * z) & x * (1.
CAlgebra(A)) = x & x * (y + z) = x * y + x * z & a * (x * y) = (a * x) * y & a
* (x + y) = a * x + a * y & (a + b) * x = a * x + b * x & (a * b) * x = a * (b
* x)
proof
let x,y,z be Element of CAlgebra(A);
let a,b;
set IT = CAlgebra(A);
reconsider f=x as Element of Funcs(A,COMPLEX);
thus x+y = y+x by Th5;
thus (x+y)+z = x+(y+z) by Th6;
thus x+(0.CAlgebra(A)) = (ComplexFuncAdd(A)).(ComplexFuncZero(A),f) by Th5
.= x by Th10;
thus ex t being Element of CAlgebra(A) st x+t=(0.CAlgebra(A))
proof
reconsider mj = -1r as Element of COMPLEX by XCMPLX_0:def 2;
set h = (ComplexFuncExtMult(A)).[mj,f];
reconsider t=h as Element of IT;
take t;
thus thesis by Th11;
end;
thus x*y = y*x by Th7;
thus (x*y)*z = x*(y*z) by Th8;
thus x*(1.CAlgebra(A)) = (ComplexFuncMult(A)).(ComplexFuncUnit(A),f) by Th7
.= x by Th9;
thus x*(y+z) = x*y + x*z by Th15;
thus a*(x*y) = (a*x)*y by Th16;
thus a*(x+y) = (a*x) + (a*y) by Lm2;
thus (a+b)*x = (a*x) + (b*x) by Th14;
thus thesis by Th13;
end;
definition
let IT be non empty ComplexAlgebraStr;
attr IT is vector-associative means
for x,y being Element of IT, a holds a * (x * y) = (a * x) * y;
end;
registration let A;
cluster CAlgebra A -> strict Abelian add-associative right_zeroed
right_complementable commutative associative right_unital
right-distributive vector-distributive scalar-distributive
scalar-associative vector-associative;
coherence
proof set C = CAlgebra A;
thus C is strict;
thus C is Abelian by Th5;
thus C is add-associative by Th6;
thus C is right_zeroed proof let x be Element of C;
reconsider f=x as Element of Funcs(A,COMPLEX);
thus x+0.C = (ComplexFuncAdd A).(ComplexFuncZero A,f) by Th5
.= x by Th10;
end;
thus C is right_complementable proof let x be Element of C;
reconsider mj = -1r as Element of COMPLEX by XCMPLX_0:def 2;
reconsider f=x as Element of Funcs(A,COMPLEX);
reconsider t=(ComplexFuncExtMult A).[mj,f] as Element of C;
take t;
thus thesis by Th11;
end;
thus C is commutative by Th7;
thus C is associative by Th8;
thus C is right_unital proof let x be Element of C;
reconsider f=x as Element of Funcs(A,COMPLEX);
thus x* 1.C = (ComplexFuncMult A).(ComplexFuncUnit A,f) by Th7
.= x by Th9;
end;
thus C is right-distributive by Th15;
thus C is vector-distributive by Lm2;
thus C is scalar-distributive by Th14;
thus C is scalar-associative by Th13;
let x,y be Element of C; let a;
thus thesis by Th16;
end;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
commutative associative right_unital right-distributive vector-distributive
scalar-distributive scalar-associative vector-associative
for non empty ComplexAlgebraStr;
existence
proof
take CAlgebra {0};
thus thesis;
end;
end;
definition
mode ComplexAlgebra is Abelian add-associative right_zeroed
right_complementable commutative associative right_unital
right-distributive vector-distributive scalar-distributive
scalar-associative vector-associative non empty ComplexAlgebraStr;
end;
theorem
CAlgebra(A) is ComplexAlgebra;
theorem
1.CRing(A) = ComplexFuncUnit(A);
theorem
1.CAlgebra(A) = ComplexFuncUnit(A);