:: FUNCSDOM semantic presentation

definition

let c₁, c₂ be non empty set ;
let c₃ be BinOp of Funcs c₁,c₂;
let c₄, c₅ be Element of Funcs c₁,c₂;
redefine func . as c₃ . c₄,c₅ -> Element of Funcs a₁,a₂;
coherence

proof end;

end;

definition

let c₁, c₂, c₃, c₄ be non empty set ;
let c₅ be Function of [:c₃,c₄:], Funcs c₁,c₂;
let c₆ be Element of [:c₃,c₄:];
redefine func . as c₅ . c₆ -> Element of Funcs a₁,a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Function of c₁,c₂;
func @ c₃ -> Element of Funcs a₁,a₂ equals :: FUNCSDOM:def 1
a₃;
coherence by FUNCT_2:11;

end;

:: deftheorem Def1 defines @ FUNCSDOM:def 1 :

definition

let c₁, c₂ be non empty set ;
let c₃ be BinOp of c₁;
let c₄, c₅ be Function of c₂,c₁;
redefine func .: as c₃ .: c₄,c₅ -> Element of Funcs a₂,a₁;
coherence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be BinOp of c₁;
let c₄ be Element of c₁;
let c₅ be Function of c₂,c₁;
redefine func [;] as c₃ [;] c₄,c₅ -> Element of Funcs a₂,a₁;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
func RealFuncAdd c₁ -> BinOp of Funcs a₁,REAL means :Def2: :: FUNCSDOM:def 2
for b₁, b₂ being Element of Funcs a₁,REAL holds a₂ . b₁,b₂ = addreal .: b₁,b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines RealFuncAdd FUNCSDOM:def 2 :

definition

let c₁ be non empty set ;
func RealFuncMult c₁ -> BinOp of Funcs a₁,REAL means :Def3: :: FUNCSDOM:def 3
for b₁, b₂ being Element of Funcs a₁,REAL holds a₂ . b₁,b₂ = multreal .: b₁,b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines RealFuncMult FUNCSDOM:def 3 :

definition

let c₁ be non empty set ;
func RealFuncExtMult c₁ -> Function of [:REAL ,(Funcs a₁,REAL ):], Funcs a₁,REAL means :Def4: :: FUNCSDOM:def 4
for b₁ being Real
for b₂ being Element of Funcs a₁,REAL
for b₃ being Element of a₁ holds (a₂ . [b₁,b₂]) . b₃ = b₁ * (b₂ . b₃);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines RealFuncExtMult FUNCSDOM:def 4 :

definition

let c₁ be non empty set ;
func RealFuncZero c₁ -> Element of Funcs a₁,REAL equals :: FUNCSDOM:def 5
a₁ --> 0;
coherence

proof end;

end;

:: deftheorem Def5 defines RealFuncZero FUNCSDOM:def 5 :

definition

let c₁ be non empty set ;
func RealFuncUnit c₁ -> Element of Funcs a₁,REAL equals :: FUNCSDOM:def 6
a₁ --> 1;
coherence

proof end;

end;

:: deftheorem Def6 defines RealFuncUnit FUNCSDOM:def 6 :

Lemma4: for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Function of b₁,b₂ holds b₃ in dom b₄

proof end;

theorem Th1: :: FUNCSDOM:1

canceled;

theorem Th2: :: FUNCSDOM:2

canceled;

theorem Th3: :: FUNCSDOM:3

canceled;

theorem Th4: :: FUNCSDOM:4

canceled;

theorem Th5: :: FUNCSDOM:5

canceled;

theorem Th6: :: FUNCSDOM:6

canceled;

theorem Th7: :: FUNCSDOM:7

canceled;

theorem Th8: :: FUNCSDOM:8

canceled;

theorem Th9: :: FUNCSDOM:9

canceled;

theorem Th10: :: FUNCSDOM:10

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,REAL holds
( b₂ = (RealFuncAdd b₁) . b₃,b₄ iff for b₅ being Element of b₁ holds b₂ . b₅ = (b₃ . b₅) + (b₄ . b₅) )

proof end;

theorem Th11: :: FUNCSDOM:11

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,REAL holds
( b₂ = (RealFuncMult b₁) . b₃,b₄ iff for b₅ being Element of b₁ holds b₂ . b₅ = (b₃ . b₅) * (b₄ . b₅) )

proof end;

theorem Th12: :: FUNCSDOM:12

for b₁ being non empty set
for b₂ being Element of b₁ holds (RealFuncUnit b₁) . b₂ = 1 by FUNCOP_1:13;

theorem Th13: :: FUNCSDOM:13

for b₁ being non empty set
for b₂ being Element of b₁ holds (RealFuncZero b₁) . b₂ = 0 by FUNCOP_1:13;

theorem Th14: :: FUNCSDOM:14

for b₁ being non empty set holds RealFuncZero b₁ <> RealFuncUnit b₁

proof end;

theorem Th15: :: FUNCSDOM:15

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL
for b₄ being Real holds
( b₂ = (RealFuncExtMult b₁) . [b₄,b₃] iff for b₅ being Element of b₁ holds b₂ . b₅ = b₄ * (b₃ . b₅) )

proof end;

theorem Th16: :: FUNCSDOM:16

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (RealFuncAdd b₁) . b₂,b₃ = (RealFuncAdd b₁) . b₃,b₂

proof end;

theorem Th17: :: FUNCSDOM:17

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,REAL holds (RealFuncAdd b₁) . b₂,((RealFuncAdd b₁) . b₃,b₄) = (RealFuncAdd b₁) . ((RealFuncAdd b₁) . b₂,b₃),b₄

proof end;

theorem Th18: :: FUNCSDOM:18

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (RealFuncMult b₁) . b₂,b₃ = (RealFuncMult b₁) . b₃,b₂

proof end;

theorem Th19: :: FUNCSDOM:19

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,REAL holds (RealFuncMult b₁) . b₂,((RealFuncMult b₁) . b₃,b₄) = (RealFuncMult b₁) . ((RealFuncMult b₁) . b₂,b₃),b₄

proof end;

theorem Th20: :: FUNCSDOM:20

for b₁ being non empty set
for b₂ being Element of Funcs b₁,REAL holds (RealFuncMult b₁) . (RealFuncUnit b₁),b₂ = b₂

proof end;

theorem Th21: :: FUNCSDOM:21

for b₁ being non empty set
for b₂ being Element of Funcs b₁,REAL holds (RealFuncAdd b₁) . (RealFuncZero b₁),b₂ = b₂

proof end;

theorem Th22: :: FUNCSDOM:22

for b₁ being non empty set
for b₂ being Element of Funcs b₁,REAL holds (RealFuncAdd b₁) . b₂,((RealFuncExtMult b₁) . [(- 1),b₂]) = RealFuncZero b₁

proof end;

theorem Th23: :: FUNCSDOM:23

for b₁ being non empty set
for b₂ being Element of Funcs b₁,REAL holds (RealFuncExtMult b₁) . [1,b₂] = b₂

proof end;

theorem Th24: :: FUNCSDOM:24

for b₁ being non empty set
for b₂ being Element of Funcs b₁,REAL
for b₃, b₄ being Real holds (RealFuncExtMult b₁) . [b₃,((RealFuncExtMult b₁) . [b₄,b₂])] = (RealFuncExtMult b₁) . [(b₃ * b₄),b₂]

proof end;

theorem Th25: :: FUNCSDOM:25

for b₁ being non empty set
for b₂ being Element of Funcs b₁,REAL
for b₃, b₄ being Real holds (RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₃,b₂]),((RealFuncExtMult b₁) . [b₄,b₂]) = (RealFuncExtMult b₁) . [(b₃ + b₄),b₂]

proof end;

Lemma20: for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL
for b₄ being Real holds (RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₄,b₂]),((RealFuncExtMult b₁) . [b₄,b₃]) = (RealFuncExtMult b₁) . [b₄,((RealFuncAdd b₁) . b₂,b₃)]

proof end;

theorem Th26: :: FUNCSDOM:26

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,REAL holds (RealFuncMult b₁) . b₂,((RealFuncAdd b₁) . b₃,b₄) = (RealFuncAdd b₁) . ((RealFuncMult b₁) . b₂,b₃),((RealFuncMult b₁) . b₂,b₄)

proof end;

theorem Th27: :: FUNCSDOM:27

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL
for b₄ being Real holds (RealFuncMult b₁) . ((RealFuncExtMult b₁) . [b₄,b₂]),b₃ = (RealFuncExtMult b₁) . [b₄,((RealFuncMult b₁) . b₂,b₃)]

proof end;

theorem Th28: :: FUNCSDOM:28

for b₁ being set
for b₂ being non empty set ex b₃, b₄ being Element of Funcs b₂,REAL st
( ( for b₅ being set st b₅ in b₂ holds
( ( b₅ = b₁ implies b₃ . b₅ = 1 ) & ( b₅ <> b₁ implies b₃ . b₅ = 0 ) ) ) & ( for b₅ being set st b₅ in b₂ holds
( ( b₅ = b₁ implies b₄ . b₅ = 0 ) & ( b₅ <> b₁ implies b₄ . b₅ = 1 ) ) ) )

proof end;

theorem Th29: :: FUNCSDOM:29

for b₁, b₂ being set
for b₃ being non empty set
for b₄, b₅ being Element of Funcs b₃,REAL st b₁ in b₃ & b₂ in b₃ & b₁ <> b₂ & ( for b₆ being set st b₆ in b₃ holds
( ( b₆ = b₁ implies b₄ . b₆ = 1 ) & ( b₆ <> b₁ implies b₄ . b₆ = 0 ) ) ) & ( for b₆ being set st b₆ in b₃ holds
( ( b₆ = b₁ implies b₅ . b₆ = 0 ) & ( b₆ <> b₁ implies b₅ . b₆ = 1 ) ) ) holds
for b₆, b₇ being Real st (RealFuncAdd b₃) . ((RealFuncExtMult b₃) . [b₆,b₄]),((RealFuncExtMult b₃) . [b₇,b₅]) = RealFuncZero b₃ holds
( b₆ = 0 & b₇ = 0 )

proof end;

theorem Th30: :: FUNCSDOM:30

for b₁, b₂ being set
for b₃ being non empty set st b₁ in b₃ & b₂ in b₃ & b₁ <> b₂ holds
ex b₄, b₅ being Element of Funcs b₃,REAL st
for b₆, b₇ being Real st (RealFuncAdd b₃) . ((RealFuncExtMult b₃) . [b₆,b₄]),((RealFuncExtMult b₃) . [b₇,b₅]) = RealFuncZero b₃ holds
( b₆ = 0 & b₇ = 0 )

proof end;

theorem Th31: :: FUNCSDOM:31

for b₁, b₂ being set
for b₃ being non empty set
for b₄, b₅ being Element of Funcs b₃,REAL st b₃ = {b₁,b₂} & b₁ <> b₂ & ( for b₆ being set st b₆ in b₃ holds
( ( b₆ = b₁ implies b₄ . b₆ = 1 ) & ( b₆ <> b₁ implies b₄ . b₆ = 0 ) ) ) & ( for b₆ being set st b₆ in b₃ holds
( ( b₆ = b₁ implies b₅ . b₆ = 0 ) & ( b₆ <> b₁ implies b₅ . b₆ = 1 ) ) ) holds
for b₆ being Element of Funcs b₃,REAL ex b₇, b₈ being Real st b₆ = (RealFuncAdd b₃) . ((RealFuncExtMult b₃) . [b₇,b₄]),((RealFuncExtMult b₃) . [b₈,b₅])

proof end;

theorem Th32: :: FUNCSDOM:32

for b₁, b₂ being set
for b₃ being non empty set st b₃ = {b₁,b₂} & b₁ <> b₂ holds
ex b₄, b₅ being Element of Funcs b₃,REAL st
for b₆ being Element of Funcs b₃,REAL ex b₇, b₈ being Real st b₆ = (RealFuncAdd b₃) . ((RealFuncExtMult b₃) . [b₇,b₄]),((RealFuncExtMult b₃) . [b₈,b₅])

proof end;

theorem Th33: :: FUNCSDOM:33

for b₁, b₂ being set
for b₃ being non empty set st b₃ = {b₁,b₂} & b₁ <> b₂ holds
ex b₄, b₅ being Element of Funcs b₃,REAL st
( ( for b₆, b₇ being Real st (RealFuncAdd b₃) . ((RealFuncExtMult b₃) . [b₆,b₄]),((RealFuncExtMult b₃) . [b₇,b₅]) = RealFuncZero b₃ holds
( b₆ = 0 & b₇ = 0 ) ) & ( for b₆ being Element of Funcs b₃,REAL ex b₇, b₈ being Real st b₆ = (RealFuncAdd b₃) . ((RealFuncExtMult b₃) . [b₇,b₄]),((RealFuncExtMult b₃) . [b₈,b₅]) ) )

proof end;

theorem Th34: :: FUNCSDOM:34

for b₁ being non empty set holds RLSStruct(# (Funcs b₁,REAL ),(RealFuncZero b₁),(RealFuncAdd b₁),(RealFuncExtMult b₁) #) is RealLinearSpace

proof end;

definition

let c₁ be non empty set ;
func RealVectSpace c₁ -> strict RealLinearSpace equals :: FUNCSDOM:def 7
RLSStruct(# (Funcs a₁,REAL ),(RealFuncZero a₁),(RealFuncAdd a₁),(RealFuncExtMult a₁) #);
coherence by Th34;

end;

:: deftheorem Def7 defines RealVectSpace FUNCSDOM:def 7 :

Lemma28: ex b₁ being non empty set ex b₂, b₃ being set st
( b₁ = {b₂,b₃} & b₂ <> b₃ )

proof end;

theorem Th35: :: FUNCSDOM:35

canceled;

theorem Th36: :: FUNCSDOM:36

canceled;

theorem Th37: :: FUNCSDOM:37

ex b₁ being strict RealLinearSpaceex b₂, b₃ being VECTOR of b₁ st
( ( for b₄, b₅ being Real st (b₄ * b₂) + (b₅ * b₃) = 0. b₁ holds
( b₄ = 0 & b₅ = 0 ) ) & ( for b₄ being VECTOR of b₁ ex b₅, b₆ being Real st b₄ = (b₅ * b₂) + (b₆ * b₃) ) )

proof end;

definition

let c₁ be non empty set ;
canceled;
canceled;
canceled;
canceled;
func RRing c₁ -> strict doubleLoopStr equals :: FUNCSDOM:def 12
doubleLoopStr(# (Funcs a₁,REAL ),(RealFuncAdd a₁),(RealFuncMult a₁),(RealFuncUnit a₁),(RealFuncZero a₁) #);
correctness ;

end;

:: deftheorem Def8 FUNCSDOM:def 8 :

:: deftheorem Def9 FUNCSDOM:def 9 :

:: deftheorem Def10 FUNCSDOM:def 10 :

:: deftheorem Def11 FUNCSDOM:def 11 :

:: deftheorem Def12 defines RRing FUNCSDOM:def 12 :

registration

let c₁ be non empty set ;
cluster RRing a₁ -> non empty strict ;
coherence

proof end;

end;

E29: now

let c₁ be non empty set ;
set c₂ = RRing c₁;
let c₃, c₄ be Element of (RRing c₁);
assume E30: c₄ = RealFuncUnit c₁ ;
reconsider c₅ = c₃ as Element of Funcs c₁,REAL ;
thus c₃ * c₄ = (RealFuncMult c₁) . c₃,c₄
.= (RealFuncMult c₁) . c₃,(RealFuncUnit c₁) by E30
.= (RealFuncMult c₁) . (RealFuncUnit c₁),c₅ by Th18
.= c₅ by Th20
.= c₃ ;
thus c₄ * c₃ = (RealFuncMult c₁) . c₄,c₃
.= (RealFuncMult c₁) . (RealFuncUnit c₁),c₃ by E30
.= c₅ by Th20
.= c₃ ;

end;

registration

let c₁ be non empty set ;
cluster RRing a₁ -> non empty unital strict ;
coherence

proof end;

end;

theorem Th38: :: FUNCSDOM:38

canceled;

theorem Th39: :: FUNCSDOM:39

canceled;

theorem Th40: :: FUNCSDOM:40

canceled;

theorem Th41: :: FUNCSDOM:41

for b₁ being non empty set holds 1. (RRing b₁) = RealFuncUnit b₁

proof end;

theorem Th42: :: FUNCSDOM:42

for b₁ being non empty set
for b₂, b₃, b₄ being Element of (RRing b₁) holds
( b₂ + b₃ = b₃ + b₂ & (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) & b₂ + (0. (RRing b₁)) = b₂ & ex b₅ being Element of (RRing b₁) st b₂ + b₅ = 0. (RRing b₁) & b₂ * b₃ = b₃ * b₂ & (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) & b₂ * (1. (RRing b₁)) = b₂ & (1. (RRing b₁)) * b₂ = b₂ & b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) & (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂) )

proof end;

registration

cluster non empty Abelian add-associative right_zeroed right_complementable associative commutative strict right-distributive right_unital doubleLoopStr ;
existence

proof end;

end;

definition

mode Ring is non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr ;

end;

theorem Th43: :: FUNCSDOM:43

for b₁ being non empty set holds RRing b₁ is commutative Ring

proof end;

definition

attr a₁ is strict;
struct AlgebraStr -> doubleLoopStr , RLSStruct ;
aggr AlgebraStr(# carrier, mult, add, Mult, unity, Zero #) -> AlgebraStr ;

end;

registration

cluster non empty AlgebraStr ;
existence

proof end;

end;

definition

let c₁ be non empty set ;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
func RAlgebra c₁ -> strict AlgebraStr equals :: FUNCSDOM:def 19
AlgebraStr(# (Funcs a₁,REAL ),(RealFuncMult a₁),(RealFuncAdd a₁),(RealFuncExtMult a₁),(RealFuncUnit a₁),(RealFuncZero a₁) #);
correctness ;

end;

:: deftheorem Def13 FUNCSDOM:def 13 :

:: deftheorem Def14 FUNCSDOM:def 14 :

:: deftheorem Def15 FUNCSDOM:def 15 :

:: deftheorem Def16 FUNCSDOM:def 16 :

:: deftheorem Def17 FUNCSDOM:def 17 :

:: deftheorem Def18 FUNCSDOM:def 18 :

:: deftheorem Def19 defines RAlgebra FUNCSDOM:def 19 :

registration

let c₁ be non empty set ;
cluster RAlgebra a₁ -> non empty strict ;
coherence

proof end;

end;

E32: now

let c₁ be non empty set ;
set c₂ = RAlgebra c₁;
let c₃, c₄ be Element of (RAlgebra c₁);
assume E33: c₄ = RealFuncUnit c₁ ;
reconsider c₅ = c₃ as Element of Funcs c₁,REAL ;
thus c₃ * c₄ = the mult of (RAlgebra c₁) . c₃,c₄
.= (RealFuncMult c₁) . c₅,(RealFuncUnit c₁) by E33
.= (RealFuncMult c₁) . (RealFuncUnit c₁),c₅ by Th18
.= c₃ by Th20 ;
thus c₄ * c₃ = the mult of (RAlgebra c₁) . c₄,c₃
.= (RealFuncMult c₁) . (RealFuncUnit c₁),c₅ by E33
.= c₃ by Th20 ;

end;

registration

let c₁ be non empty set ;
cluster RAlgebra a₁ -> non empty unital strict ;
coherence

proof end;

end;

theorem Th44: :: FUNCSDOM:44

for b₁ being non empty set holds 1. (RAlgebra b₁) = RealFuncUnit b₁

proof end;

theorem Th45: :: FUNCSDOM:45

canceled;

theorem Th46: :: FUNCSDOM:46

canceled;

theorem Th47: :: FUNCSDOM:47

canceled;

theorem Th48: :: FUNCSDOM:48

canceled;

theorem Th49: :: FUNCSDOM:49

for b₁ being non empty set
for b₂, b₃, b₄ being Element of (RAlgebra b₁)
for b₅, b₆ being Real holds
( b₂ + b₃ = b₃ + b₂ & (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) & b₂ + (0. (RAlgebra b₁)) = b₂ & ex b₇ being Element of (RAlgebra b₁) st b₂ + b₇ = 0. (RAlgebra b₁) & b₂ * b₃ = b₃ * b₂ & (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) & b₂ * (1. (RAlgebra b₁)) = b₂ & b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) & b₅ * (b₂ * b₃) = (b₅ * b₂) * b₃ & b₅ * (b₂ + b₃) = (b₅ * b₂) + (b₅ * b₃) & (b₅ + b₆) * b₂ = (b₅ * b₂) + (b₆ * b₂) & (b₅ * b₆) * b₂ = b₅ * (b₆ * b₂) )

proof end;

definition

let c₁ be non empty AlgebraStr ;
attr a₁ is Algebra-like means :Def20: :: FUNCSDOM:def 20
for b₁, b₂, b₃ being Element of a₁
for b₄, b₅ being Real holds
( b₁ * (1. a₁) = b₁ & b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃) & b₄ * (b₁ * b₂) = (b₄ * b₁) * b₂ & b₄ * (b₁ + b₂) = (b₄ * b₁) + (b₄ * b₂) & (b₄ + b₅) * b₁ = (b₄ * b₁) + (b₅ * b₁) & (b₄ * b₅) * b₁ = b₄ * (b₅ * b₁) );

end;

:: deftheorem Def20 defines Algebra-like FUNCSDOM:def 20 :

registration

cluster non empty Abelian add-associative right_zeroed right_complementable associative commutative strict Algebra-like AlgebraStr ;
existence

proof end;

end;

definition

mode Algebra is non empty Abelian add-associative right_zeroed right_complementable associative commutative Algebra-like AlgebraStr ;

end;

theorem Th50: :: FUNCSDOM:50

for b₁ being non empty set holds RAlgebra b₁ is Algebra

proof end;