:: by Noboru Endou

::

:: Received March 18, 2004

:: Copyright (c) 2004-2019 Association of Mizar Users

definition

let A be set ;

ex b_{1} being BinOp of (Funcs (A,COMPLEX)) st

for f, g being Element of Funcs (A,COMPLEX) holds b_{1} . (f,g) = addcomplex .: (f,g)

for b_{1}, b_{2} being BinOp of (Funcs (A,COMPLEX)) st ( for f, g being Element of Funcs (A,COMPLEX) holds b_{1} . (f,g) = addcomplex .: (f,g) ) & ( for f, g being Element of Funcs (A,COMPLEX) holds b_{2} . (f,g) = addcomplex .: (f,g) ) holds

b_{1} = b_{2}

end;
func ComplexFuncAdd A -> BinOp of (Funcs (A,COMPLEX)) means :Def1: :: CFUNCDOM:def 1

for f, g being Element of Funcs (A,COMPLEX) holds it . (f,g) = addcomplex .: (f,g);

existence for f, g being Element of Funcs (A,COMPLEX) holds it . (f,g) = addcomplex .: (f,g);

ex b

for f, g being Element of Funcs (A,COMPLEX) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines ComplexFuncAdd CFUNCDOM:def 1 :

for A being set

for b_{2} being BinOp of (Funcs (A,COMPLEX)) holds

( b_{2} = ComplexFuncAdd A iff for f, g being Element of Funcs (A,COMPLEX) holds b_{2} . (f,g) = addcomplex .: (f,g) );

for A being set

for b

( b

definition

let A be set ;

ex b_{1} being BinOp of (Funcs (A,COMPLEX)) st

for f, g being Element of Funcs (A,COMPLEX) holds b_{1} . (f,g) = multcomplex .: (f,g)

for b_{1}, b_{2} being BinOp of (Funcs (A,COMPLEX)) st ( for f, g being Element of Funcs (A,COMPLEX) holds b_{1} . (f,g) = multcomplex .: (f,g) ) & ( for f, g being Element of Funcs (A,COMPLEX) holds b_{2} . (f,g) = multcomplex .: (f,g) ) holds

b_{1} = b_{2}

end;
func ComplexFuncMult A -> BinOp of (Funcs (A,COMPLEX)) means :Def2: :: CFUNCDOM:def 2

for f, g being Element of Funcs (A,COMPLEX) holds it . (f,g) = multcomplex .: (f,g);

existence for f, g being Element of Funcs (A,COMPLEX) holds it . (f,g) = multcomplex .: (f,g);

ex b

for f, g being Element of Funcs (A,COMPLEX) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines ComplexFuncMult CFUNCDOM:def 2 :

for A being set

for b_{2} being BinOp of (Funcs (A,COMPLEX)) holds

( b_{2} = ComplexFuncMult A iff for f, g being Element of Funcs (A,COMPLEX) holds b_{2} . (f,g) = multcomplex .: (f,g) );

for A being set

for b

( b

definition

let A be non empty set ;

ex b_{1} being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) st

for z being Complex

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (b_{1} . [z,f]) . x = z * (f . x)

for b_{1}, b_{2} being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) st ( for z being Complex

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (b_{1} . [z,f]) . x = z * (f . x) ) & ( for z being Complex

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (b_{2} . [z,f]) . x = z * (f . x) ) holds

b_{1} = b_{2}

end;
func ComplexFuncExtMult A -> Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) means :Def3: :: CFUNCDOM:def 3

for z being Complex

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (it . [z,f]) . x = z * (f . x);

existence for z being Complex

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (it . [z,f]) . x = z * (f . x);

ex b

for z being Complex

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (b

proof end;

uniqueness for b

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (b

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (b

b

proof end;

:: deftheorem Def3 defines ComplexFuncExtMult CFUNCDOM:def 3 :

for A being non empty set

for b_{2} being Function of [:COMPLEX,(Funcs (A,COMPLEX)):],(Funcs (A,COMPLEX)) holds

( b_{2} = ComplexFuncExtMult A iff for z being Complex

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (b_{2} . [z,f]) . x = z * (f . x) );

for A being non empty set

for b

( b

for f being Element of Funcs (A,COMPLEX)

for x being Element of A holds (b

registration
end;

definition
end;

:: deftheorem defines ComplexFuncZero CFUNCDOM:def 4 :

for A being non empty set holds ComplexFuncZero A = A --> 0;

for A being non empty set holds ComplexFuncZero A = A --> 0;

definition
end;

:: deftheorem defines ComplexFuncUnit CFUNCDOM:def 5 :

for A being non empty set holds ComplexFuncUnit A = A --> 1r;

for A being non empty set holds ComplexFuncUnit A = A --> 1r;

Lm1: for A, B being non empty set

for x being Element of A

for f being Function of A,B holds x in dom f

proof end;

theorem Th1: :: CFUNCDOM:1

for A being non empty set

for f, g, h being Element of Funcs (A,COMPLEX) holds

( h = (ComplexFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) )

for f, g, h being Element of Funcs (A,COMPLEX) holds

( h = (ComplexFuncAdd A) . (f,g) iff for x being Element of A holds h . x = (f . x) + (g . x) )

proof end;

theorem Th2: :: CFUNCDOM:2

for A being non empty set

for f, g, h being Element of Funcs (A,COMPLEX) holds

( h = (ComplexFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )

for f, g, h being Element of Funcs (A,COMPLEX) holds

( h = (ComplexFuncMult A) . (f,g) iff for x being Element of A holds h . x = (f . x) * (g . x) )

proof end;

theorem Th4: :: CFUNCDOM:4

for A being non empty set

for f, h being Element of Funcs (A,COMPLEX)

for a being Complex holds

( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )

for f, h being Element of Funcs (A,COMPLEX)

for a being Complex holds

( h = (ComplexFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )

proof end;

theorem Th5: :: CFUNCDOM:5

for A being non empty set

for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,g) = (ComplexFuncAdd A) . (g,f)

for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,g) = (ComplexFuncAdd A) . (g,f)

proof end;

theorem Th6: :: CFUNCDOM:6

for A being non empty set

for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncAdd A) . (f,g)),h)

for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncAdd A) . (f,g)),h)

proof end;

theorem Th7: :: CFUNCDOM:7

for A being non empty set

for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,g) = (ComplexFuncMult A) . (g,f)

for f, g being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,g) = (ComplexFuncMult A) . (g,f)

proof end;

theorem Th8: :: CFUNCDOM:8

for A being non empty set

for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncMult A) . (g,h))) = (ComplexFuncMult A) . (((ComplexFuncMult A) . (f,g)),h)

for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncMult A) . (g,h))) = (ComplexFuncMult A) . (((ComplexFuncMult A) . (f,g)),h)

proof end;

theorem Th9: :: CFUNCDOM:9

for A being non empty set

for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . ((ComplexFuncUnit A),f) = f

for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . ((ComplexFuncUnit A),f) = f

proof end;

theorem Th10: :: CFUNCDOM:10

for A being non empty set

for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . ((ComplexFuncZero A),f) = f

for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . ((ComplexFuncZero A),f) = f

proof end;

theorem Th11: :: CFUNCDOM:11

for A being non empty set

for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f])) = ComplexFuncZero A

for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncAdd A) . (f,((ComplexFuncExtMult A) . [(- 1r),f])) = ComplexFuncZero A

proof end;

theorem Th12: :: CFUNCDOM:12

for A being non empty set

for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncExtMult A) . [1r,f] = f

for f being Element of Funcs (A,COMPLEX) holds (ComplexFuncExtMult A) . [1r,f] = f

proof end;

theorem Th13: :: CFUNCDOM:13

for A being non empty set

for f being Element of Funcs (A,COMPLEX)

for a, b being Complex holds (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]

for f being Element of Funcs (A,COMPLEX)

for a, b being Complex holds (ComplexFuncExtMult A) . [a,((ComplexFuncExtMult A) . [b,f])] = (ComplexFuncExtMult A) . [(a * b),f]

proof end;

theorem Th14: :: CFUNCDOM:14

for A being non empty set

for f being Element of Funcs (A,COMPLEX)

for a, b being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f]

for f being Element of Funcs (A,COMPLEX)

for a, b being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,f])) = (ComplexFuncExtMult A) . [(a + b),f]

proof end;

Lm2: for A being non empty set

for f, g being Element of Funcs (A,COMPLEX)

for a being Complex holds (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [a,g])) = (ComplexFuncExtMult A) . [a,((ComplexFuncAdd A) . (f,g))]

proof end;

theorem Th15: :: CFUNCDOM:15

for A being non empty set

for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncMult A) . (f,g)),((ComplexFuncMult A) . (f,h)))

for f, g, h being Element of Funcs (A,COMPLEX) holds (ComplexFuncMult A) . (f,((ComplexFuncAdd A) . (g,h))) = (ComplexFuncAdd A) . (((ComplexFuncMult A) . (f,g)),((ComplexFuncMult A) . (f,h)))

proof end;

theorem Th16: :: CFUNCDOM:16

for A being non empty set

for f, g being Element of Funcs (A,COMPLEX)

for a being Complex holds (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]

for f, g being Element of Funcs (A,COMPLEX)

for a being Complex holds (ComplexFuncMult A) . (((ComplexFuncExtMult A) . [a,f]),g) = (ComplexFuncExtMult A) . [a,((ComplexFuncMult A) . (f,g))]

proof end;

theorem Th17: :: CFUNCDOM:17

for x1 being set

for A being non empty set ex f, g being Element of Funcs (A,COMPLEX) st

( ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds

( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) )

for A being non empty set ex f, g being Element of Funcs (A,COMPLEX) st

( ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds

( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) )

proof end;

theorem Th18: :: CFUNCDOM:18

for x1, x2 being set

for A being non empty set

for f, g being Element of Funcs (A,COMPLEX) st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds

( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds

for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0c & b = 0c )

for A being non empty set

for f, g being Element of Funcs (A,COMPLEX) st x1 in A & x2 in A & x1 <> x2 & ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds

( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds

for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0c & b = 0c )

proof end;

theorem :: CFUNCDOM:19

for x1, x2 being set

for A being non empty set st x1 in A & x2 in A & x1 <> x2 holds

ex f, g being Element of Funcs (A,COMPLEX) st

for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0 & b = 0 )

for A being non empty set st x1 in A & x2 in A & x1 <> x2 holds

ex f, g being Element of Funcs (A,COMPLEX) st

for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0 & b = 0 )

proof end;

theorem Th20: :: CFUNCDOM:20

for x1, x2 being set

for A being non empty set

for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds

( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds

for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

for A being non empty set

for f, g being Element of Funcs (A,COMPLEX) st A = {x1,x2} & x1 <> x2 & ( for z being set st z in A holds

( ( z = x1 implies f . z = 1r ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds

( ( z = x1 implies g . z = 0 ) & ( z <> x1 implies g . z = 1r ) ) ) holds

for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

proof end;

theorem :: CFUNCDOM:21

for x1, x2 being set

for A being non empty set st A = {x1,x2} & x1 <> x2 holds

ex f, g being Element of Funcs (A,COMPLEX) st

for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

for A being non empty set st A = {x1,x2} & x1 <> x2 holds

ex f, g being Element of Funcs (A,COMPLEX) st

for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))

proof end;

theorem Th22: :: CFUNCDOM:22

for x1, x2 being set

for A being non empty set st A = {x1,x2} & x1 <> x2 holds

ex f, g being Element of Funcs (A,COMPLEX) st

( ( for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) ) )

for A being non empty set st A = {x1,x2} & x1 <> x2 holds

ex f, g being Element of Funcs (A,COMPLEX) st

( ( for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds

( a = 0 & b = 0 ) ) & ( for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) ) )

proof end;

definition

let A be non empty set ;

CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is non empty strict CLSStruct ;

end;
func ComplexVectSpace A -> non empty strict CLSStruct equals :: CFUNCDOM:def 6

CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);

coherence CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);

CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is non empty strict CLSStruct ;

:: deftheorem defines ComplexVectSpace CFUNCDOM:def 6 :

for A being non empty set holds ComplexVectSpace A = CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);

for A being non empty set holds ComplexVectSpace A = CLSStruct(# (Funcs (A,COMPLEX)),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);

registration

let A be non empty set ;

for b_{1} being non empty strict CLSStruct st b_{1} = ComplexVectSpace A holds

( b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital )

end;
cluster ComplexVectSpace A -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for non empty strict CLSStruct ;

coherence for b

( b

proof end;

Lm3: ex A being non empty set ex x1, x2 being set st

( A = {x1,x2} & x1 <> x2 )

proof end;

theorem :: CFUNCDOM:23

ex V being strict ComplexLinearSpace ex u, v being VECTOR of V st

( ( for a, b being Complex st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Complex st w = (a * u) + (b * v) ) )

( ( for a, b being Complex st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Complex st w = (a * u) + (b * v) ) )

proof end;

definition

let A be non empty set ;

coherence

doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #) is doubleLoopStr ;

;

end;
func CRing A -> doubleLoopStr equals :: CFUNCDOM:def 7

doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

correctness doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

coherence

doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #) is doubleLoopStr ;

;

:: deftheorem defines CRing CFUNCDOM:def 7 :

for A being non empty set holds CRing A = doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

for A being non empty set holds CRing A = doubleLoopStr(# (Funcs (A,COMPLEX)),(ComplexFuncAdd A),(ComplexFuncMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

Lm4: now :: thesis: for A being non empty set

for x, e being Element of (CRing A) st e = ComplexFuncUnit A holds

( e * x = x & x * e = x )

for x, e being Element of (CRing A) st e = ComplexFuncUnit A holds

( e * x = x & x * e = x )

let A be non empty set ; :: thesis: for x, e being Element of (CRing A) st e = ComplexFuncUnit A holds

( e * x = x & x * e = x )

let x, e be Element of (CRing A); :: thesis: ( e = ComplexFuncUnit A implies ( e * x = x & x * e = x ) )

assume e = ComplexFuncUnit A ; :: thesis: ( e * x = x & x * e = x )

hence e * x = x by Th9; :: thesis: x * e = x

hence x * e = x by Th7; :: thesis: verum

end;
( e * x = x & x * e = x )

let x, e be Element of (CRing A); :: thesis: ( e = ComplexFuncUnit A implies ( e * x = x & x * e = x ) )

assume e = ComplexFuncUnit A ; :: thesis: ( e * x = x & x * e = x )

hence e * x = x by Th9; :: thesis: x * e = x

hence x * e = x by Th7; :: thesis: verum

registration
end;

theorem Th24: :: CFUNCDOM:24

for A being non empty set

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) )

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 end;

definition

attr c_{1} is strict ;

struct ComplexAlgebraStr -> doubleLoopStr , CLSStruct ;

aggr ComplexAlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF #) -> ComplexAlgebraStr ;

end;
struct ComplexAlgebraStr -> doubleLoopStr , CLSStruct ;

aggr ComplexAlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF #) -> ComplexAlgebraStr ;

definition

let A be non empty set ;

coherence

ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #) is strict ComplexAlgebraStr ;

;

end;
func CAlgebra A -> strict ComplexAlgebraStr equals :: CFUNCDOM:def 8

ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

correctness ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

coherence

ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #) is strict ComplexAlgebraStr ;

;

:: deftheorem defines CAlgebra CFUNCDOM:def 8 :

for A being non empty set holds CAlgebra A = ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

for A being non empty set holds CAlgebra A = ComplexAlgebraStr(# (Funcs (A,COMPLEX)),(ComplexFuncMult A),(ComplexFuncAdd A),(ComplexFuncExtMult A),(ComplexFuncUnit A),(ComplexFuncZero A) #);

Lm5: now :: thesis: for A being non empty set

for x, e being Element of (CAlgebra A) st e = ComplexFuncUnit A holds

( e * x = x & x * e = x )

for x, e being Element of (CAlgebra A) st e = ComplexFuncUnit A holds

( e * x = x & x * e = x )

let A be non empty set ; :: thesis: for x, e being Element of (CAlgebra A) st e = ComplexFuncUnit A holds

( e * x = x & x * e = x )

let x, e be Element of (CAlgebra A); :: thesis: ( e = ComplexFuncUnit A implies ( e * x = x & x * e = x ) )

assume e = ComplexFuncUnit A ; :: thesis: ( e * x = x & x * e = x )

hence e * x = x by Th9; :: thesis: x * e = x

hence x * e = x by Th7; :: thesis: verum

end;
( e * x = x & x * e = x )

let x, e be Element of (CAlgebra A); :: thesis: ( e = ComplexFuncUnit A implies ( e * x = x & x * e = x ) )

assume e = ComplexFuncUnit A ; :: thesis: ( e * x = x & x * e = x )

hence e * x = x by Th9; :: thesis: x * e = x

hence x * e = x by Th7; :: thesis: verum

theorem :: CFUNCDOM:26

for A being non empty set

for x, y, z being Element of (CAlgebra A)

for a, b being Complex 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) )

for x, y, z being Element of (CAlgebra A)

for a, b being Complex 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 end;

definition

let IT be non empty ComplexAlgebraStr ;

end;
attr IT is vector-associative means :: CFUNCDOM:def 9

for x, y being Element of IT

for a being Complex holds a * (x * y) = (a * x) * y;

for x, y being Element of IT

for a being Complex holds a * (x * y) = (a * x) * y;

:: deftheorem defines vector-associative CFUNCDOM:def 9 :

for IT being non empty ComplexAlgebraStr holds

( IT is vector-associative iff for x, y being Element of IT

for a being Complex holds a * (x * y) = (a * x) * y );

for IT being non empty ComplexAlgebraStr holds

( IT is vector-associative iff for x, y being Element of IT

for a being Complex holds a * (x * y) = (a * x) * y );

registration

let A be non empty set ;

( CAlgebra A is strict & CAlgebra A is Abelian & CAlgebra A is add-associative & CAlgebra A is right_zeroed & CAlgebra A is right_complementable & CAlgebra A is commutative & CAlgebra A is associative & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )

end;
cluster CAlgebra A -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative right-distributive right_unital associative commutative strict vector-associative ;

coherence ( CAlgebra A is strict & CAlgebra A is Abelian & CAlgebra A is add-associative & CAlgebra A is right_zeroed & CAlgebra A is right_complementable & CAlgebra A is commutative & CAlgebra A is associative & CAlgebra A is right_unital & CAlgebra A is right-distributive & CAlgebra A is vector-distributive & CAlgebra A is scalar-distributive & CAlgebra A is scalar-associative & CAlgebra A is vector-associative )

proof end;

registration

ex b_{1} being non empty ComplexAlgebraStr st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is commutative & b_{1} is associative & b_{1} is right_unital & b_{1} is right-distributive & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is vector-associative )
end;

cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative right-distributive right_unital associative commutative strict vector-associative for ComplexAlgebraStr ;

existence ex b

( b

proof end;

definition

mode ComplexAlgebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative right-distributive right_unital associative commutative vector-associative ComplexAlgebraStr ;

end;