:: VFUNCT_2 semantic presentation

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
let c₃, c₄ be PartFunc of c₁,the carrier of c₂;
deffunc H₁( Element of c₁) -> Element of the carrier of c₂ = (c₃ /. a₁) + (c₄ /. a₁);
deffunc H₂( Element of c₁) -> Element of the carrier of c₂ = (c₃ /. a₁) - (c₄ /. a₁);
defpred S₁[ set ] means a₁ in (dom c₃) /\ (dom c₄);
set c₅ = (dom c₃) /\ (dom c₄);
func c₃ + c₄ -> PartFunc of a₁,the carrier of a₂ means :Def1: :: VFUNCT_2:def 1
( dom a₅ = (dom a₃) /\ (dom a₄) & ( for b₁ being Element of a₁ st b₁ in dom a₅ holds
a₅ /. b₁ = (a₃ /. b₁) + (a₄ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

func c₃ - c₄ -> PartFunc of a₁,the carrier of a₂ means :Def2: :: VFUNCT_2:def 2
( dom a₅ = (dom a₃) /\ (dom a₄) & ( for b₁ being Element of a₁ st b₁ in dom a₅ holds
a₅ /. b₁ = (a₃ /. b₁) - (a₄ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines + VFUNCT_2:def 1 :

:: deftheorem Def2 defines - VFUNCT_2:def 2 :

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
let c₃ be PartFunc of c₁, COMPLEX ;
let c₄ be PartFunc of c₁,the carrier of c₂;
deffunc H₁( Element of c₁) -> Element of the carrier of c₂ = (c₃ /. a₁) * (c₄ /. a₁);
defpred S₁[ set ] means a₁ in (dom c₃) /\ (dom c₄);
set c₅ = (dom c₃) /\ (dom c₄);
func c₃ (#) c₄ -> PartFunc of a₁,the carrier of a₂ means :Def3: :: VFUNCT_2:def 3
( dom a₅ = (dom a₃) /\ (dom a₄) & ( for b₁ being Element of a₁ st b₁ in dom a₅ holds
a₅ /. b₁ = (a₃ /. b₁) * (a₄ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines (#) VFUNCT_2:def 3 :

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
let c₃ be PartFunc of c₁,the carrier of c₂;
let c₄ be Complex;
deffunc H₁( Element of c₁) -> Element of the carrier of c₂ = c₄ * (c₃ /. a₁);
defpred S₁[ set ] means a₁ in dom c₃;
set c₅ = dom c₃;
func c₄ (#) c₃ -> PartFunc of a₁,the carrier of a₂ means :Def4: :: VFUNCT_2:def 4
( dom a₅ = dom a₃ & ( for b₁ being Element of a₁ st b₁ in dom a₅ holds
a₅ /. b₁ = a₄ * (a₃ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines (#) VFUNCT_2:def 4 :

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
let c₃ be PartFunc of c₁,the carrier of c₂;
deffunc H₁( Element of c₁) -> Element of REAL = ||.(c₃ /. a₁).||;
deffunc H₂( Element of c₁) -> Element of the carrier of c₂ = - (c₃ /. a₁);
defpred S₁[ set ] means a₁ in dom c₃;
set c₄ = dom c₃;
func ||.c₃.|| -> PartFunc of a₁, REAL means :Def5: :: VFUNCT_2:def 5
( dom a₄ = dom a₃ & ( for b₁ being Element of a₁ st b₁ in dom a₄ holds
a₄ . b₁ = ||.(a₃ /. b₁).|| ) );
existence

proof end;

uniqueness

proof end;

func - c₃ -> PartFunc of a₁,the carrier of a₂ means :Def6: :: VFUNCT_2:def 6
( dom a₄ = dom a₃ & ( for b₁ being Element of a₁ st b₁ in dom a₄ holds
a₄ /. b₁ = - (a₃ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines ||. VFUNCT_2:def 5 :

:: deftheorem Def6 defines - VFUNCT_2:def 6 :

theorem Th1: :: VFUNCT_2:1

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁, COMPLEX
for b₄ being PartFunc of b₁,the carrier of b₂ holds (dom (b₃ (#) b₄)) \ ((b₃ (#) b₄) " {(0. b₂)}) = ((dom b₃) \ (b₃ " {0})) /\ ((dom b₄) \ (b₄ " {(0. b₂)}))

proof end;

theorem Th2: :: VFUNCT_2:2

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds
( ||.b₃.|| " {0} = b₃ " {(0. b₂)} & (- b₃) " {(0. b₂)} = b₃ " {(0. b₂)} )

proof end;

theorem Th3: :: VFUNCT_2:3

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Complex st b₄ <> 0c holds
(b₄ (#) b₃) " {(0. b₂)} = b₃ " {(0. b₂)}

proof end;

theorem Th4: :: VFUNCT_2:4

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂ holds b₃ + b₄ = b₄ + b₃

proof end;

theorem Th5: :: VFUNCT_2:5

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄, b₅ being PartFunc of b₁,the carrier of b₂ holds (b₃ + b₄) + b₅ = b₃ + (b₄ + b₅)

proof end;

theorem Th6: :: VFUNCT_2:6

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁, COMPLEX
for b₅ being PartFunc of b₁,the carrier of b₂ holds (b₃ (#) b₄) (#) b₅ = b₃ (#) (b₄ (#) b₅)

proof end;

theorem Th7: :: VFUNCT_2:7

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄, b₅ being PartFunc of b₁, COMPLEX holds (b₄ + b₅) (#) b₃ = (b₄ (#) b₃) + (b₅ (#) b₃)

proof end;

theorem Th8: :: VFUNCT_2:8

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅ being PartFunc of b₁, COMPLEX holds b₅ (#) (b₃ + b₄) = (b₅ (#) b₃) + (b₅ (#) b₄)

proof end;

theorem Th9: :: VFUNCT_2:9

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Complex
for b₅ being PartFunc of b₁, COMPLEX holds b₄ (#) (b₅ (#) b₃) = (b₄ (#) b₅) (#) b₃

proof end;

theorem Th10: :: VFUNCT_2:10

proof end;

theorem Th11: :: VFUNCT_2:11

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄, b₅ being PartFunc of b₁, COMPLEX holds (b₄ - b₅) (#) b₃ = (b₄ (#) b₃) - (b₅ (#) b₃)

proof end;

theorem Th12: :: VFUNCT_2:12

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅ being PartFunc of b₁, COMPLEX holds (b₅ (#) b₃) - (b₅ (#) b₄) = b₅ (#) (b₃ - b₄)

proof end;

theorem Th13: :: VFUNCT_2:13

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅ being Complex holds b₅ (#) (b₃ + b₄) = (b₅ (#) b₃) + (b₅ (#) b₄)

proof end;

theorem Th14: :: VFUNCT_2:14

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄, b₅ being Complex holds (b₄ * b₅) (#) b₃ = b₄ (#) (b₅ (#) b₃)

proof end;

theorem Th15: :: VFUNCT_2:15

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅ being Complex holds b₅ (#) (b₃ - b₄) = (b₅ (#) b₃) - (b₅ (#) b₄)

proof end;

theorem Th16: :: VFUNCT_2:16

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂ holds b₃ - b₄ = (- 1r ) (#) (b₄ - b₃)

proof end;

theorem Th17: :: VFUNCT_2:17

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄, b₅ being PartFunc of b₁,the carrier of b₂ holds b₃ - (b₄ + b₅) = (b₃ - b₄) - b₅

proof end;

theorem Th18: :: VFUNCT_2:18

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds 1r (#) b₃ = b₃

proof end;

theorem Th19: :: VFUNCT_2:19

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄, b₅ being PartFunc of b₁,the carrier of b₂ holds b₃ - (b₄ - b₅) = (b₃ - b₄) + b₅

proof end;

theorem Th20: :: VFUNCT_2:20

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄, b₅ being PartFunc of b₁,the carrier of b₂ holds b₃ + (b₄ - b₅) = (b₃ + b₄) - b₅

proof end;

theorem Th21: :: VFUNCT_2:21

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being PartFunc of b₁, COMPLEX holds ||.(b₄ (#) b₃).|| = |.b₄.| (#) ||.b₃.||

proof end;

theorem Th22: :: VFUNCT_2:22

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Complex holds ||.(b₄ (#) b₃).|| = |.b₄.| (#) ||.b₃.||

proof end;

theorem Th23: :: VFUNCT_2:23

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds - b₃ = (- 1r ) (#) b₃

proof end;

theorem Th24: :: VFUNCT_2:24

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds - (- b₃) = b₃

proof end;

theorem Th25: :: VFUNCT_2:25

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂ holds b₃ - b₄ = b₃ + (- b₄)

proof end;

theorem Th26: :: VFUNCT_2:26

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂ holds b₃ - (- b₄) = b₃ + b₄

proof end;

theorem Th27: :: VFUNCT_2:27

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅ being set holds
( (b₃ + b₄) | b₅ = (b₃ | b₅) + (b₄ | b₅) & (b₃ + b₄) | b₅ = (b₃ | b₅) + b₄ & (b₃ + b₄) | b₅ = b₃ + (b₄ | b₅) )

proof end;

theorem Th28: :: VFUNCT_2:28

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being set
for b₅ being PartFunc of b₁, COMPLEX holds
( (b₅ (#) b₃) | b₄ = (b₅ | b₄) (#) (b₃ | b₄) & (b₅ (#) b₃) | b₄ = (b₅ | b₄) (#) b₃ & (b₅ (#) b₃) | b₄ = b₅ (#) (b₃ | b₄) )

proof end;

theorem Th29: :: VFUNCT_2:29

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being set holds
( (- b₃) | b₄ = - (b₃ | b₄) & ||.b₃.|| | b₄ = ||.(b₃ | b₄).|| )

proof end;

theorem Th30: :: VFUNCT_2:30

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅ being set holds
( (b₃ - b₄) | b₅ = (b₃ | b₅) - (b₄ | b₅) & (b₃ - b₄) | b₅ = (b₃ | b₅) - b₄ & (b₃ - b₄) | b₅ = b₃ - (b₄ | b₅) )

proof end;

theorem Th31: :: VFUNCT_2:31

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Complex
for b₅ being set holds (b₄ (#) b₃) | b₅ = b₄ (#) (b₃ | b₅)

proof end;

theorem Th32: :: VFUNCT_2:32

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂ holds
( ( b₃ is total & b₄ is total implies b₃ + b₄ is total ) & ( b₃ + b₄ is total implies ( b₃ is total & b₄ is total ) ) & ( b₃ is total & b₄ is total implies b₃ - b₄ is total ) & ( b₃ - b₄ is total implies ( b₃ is total & b₄ is total ) ) )

proof end;

theorem Th33: :: VFUNCT_2:33

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being PartFunc of b₁, COMPLEX holds
( ( b₄ is total & b₃ is total ) iff b₄ (#) b₃ is total )

proof end;

theorem Th34: :: VFUNCT_2:34

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Complex holds
( b₃ is total iff b₄ (#) b₃ is total )

proof end;

theorem Th35: :: VFUNCT_2:35

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds
( b₃ is total iff - b₃ is total )

proof end;

theorem Th36: :: VFUNCT_2:36

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂ holds
( b₃ is total iff ||.b₃.|| is total )

proof end;

theorem Th37: :: VFUNCT_2:37

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅ being Element of b₁ st b₃ is total & b₄ is total holds
( (b₃ + b₄) /. b₅ = (b₃ /. b₅) + (b₄ /. b₅) & (b₃ - b₄) /. b₅ = (b₃ /. b₅) - (b₄ /. b₅) )

proof end;

theorem Th38: :: VFUNCT_2:38

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being PartFunc of b₁, COMPLEX
for b₅ being Element of b₁ st b₄ is total & b₃ is total holds
(b₄ (#) b₃) /. b₅ = (b₄ /. b₅) * (b₃ /. b₅)

proof end;

theorem Th39: :: VFUNCT_2:39

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Complex
for b₅ being Element of b₁ st b₃ is total holds
(b₄ (#) b₃) /. b₅ = b₄ * (b₃ /. b₅)

proof end;

theorem Th40: :: VFUNCT_2:40

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Element of b₁ st b₃ is total holds
( (- b₃) /. b₄ = - (b₃ /. b₄) & ||.b₃.|| . b₄ = ||.(b₃ /. b₄).|| )

proof end;

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
let c₃ be PartFunc of c₁,the carrier of c₂;
let c₄ be set ;
pred c₃ is_bounded_on c₄ means :Def7: :: VFUNCT_2:def 7
ex b₁ being Real st
for b₂ being Element of a₁ st b₂ in a₄ /\ (dom a₃) holds
||.(a₃ /. b₂).|| <= b₁;

end;

:: deftheorem Def7 defines is_bounded_on VFUNCT_2:def 7 :

theorem Th41: :: VFUNCT_2:41

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄, b₅ being set st b₄ c= b₅ & b₃ is_bounded_on b₅ holds
b₃ is_bounded_on b₄

proof end;

theorem Th42: :: VFUNCT_2:42

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being set st b₄ misses dom b₃ holds
b₃ is_bounded_on b₄

proof end;

theorem Th43: :: VFUNCT_2:43

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being set holds 0c (#) b₃ is_bounded_on b₄

proof end;

theorem Th44: :: VFUNCT_2:44

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Complex
for b₅ being set st b₃ is_bounded_on b₅ holds
b₄ (#) b₃ is_bounded_on b₅

proof end;

theorem Th45: :: VFUNCT_2:45

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being set st b₃ is_bounded_on b₄ holds
( ||.b₃.|| is_bounded_on b₄ & - b₃ is_bounded_on b₄ )

proof end;

theorem Th46: :: VFUNCT_2:46

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅, b₆ being set st b₃ is_bounded_on b₅ & b₄ is_bounded_on b₆ holds
b₃ + b₄ is_bounded_on b₅ /\ b₆

proof end;

theorem Th47: :: VFUNCT_2:47

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄, b₅ being set
for b₆ being PartFunc of b₁, COMPLEX st b₆ is_bounded_on b₄ & b₃ is_bounded_on b₅ holds
b₆ (#) b₃ is_bounded_on b₄ /\ b₅

proof end;

theorem Th48: :: VFUNCT_2:48

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅, b₆ being set st b₃ is_bounded_on b₅ & b₄ is_bounded_on b₆ holds
b₃ - b₄ is_bounded_on b₅ /\ b₆

proof end;

theorem Th49: :: VFUNCT_2:49

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄, b₅ being set st b₃ is_bounded_on b₄ & b₃ is_bounded_on b₅ holds
b₃ is_bounded_on b₄ \/ b₅

proof end;

theorem Th50: :: VFUNCT_2:50

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅, b₆ being set st b₃ is_constant_on b₅ & b₄ is_constant_on b₆ holds
( b₃ + b₄ is_constant_on b₅ /\ b₆ & b₃ - b₄ is_constant_on b₅ /\ b₆ )

proof end;

theorem Th51: :: VFUNCT_2:51

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄, b₅ being set
for b₆ being PartFunc of b₁, COMPLEX st b₆ is_constant_on b₄ & b₃ is_constant_on b₅ holds
b₆ (#) b₃ is_constant_on b₄ /\ b₅

proof end;

theorem Th52: :: VFUNCT_2:52

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being Complex
for b₅ being set st b₃ is_constant_on b₅ holds
b₄ (#) b₃ is_constant_on b₅

proof end;

theorem Th53: :: VFUNCT_2:53

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being set st b₃ is_constant_on b₄ holds
( ||.b₃.|| is_constant_on b₄ & - b₃ is_constant_on b₄ )

proof end;

theorem Th54: :: VFUNCT_2:54

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being set st b₃ is_constant_on b₄ holds
b₃ is_bounded_on b₄

proof end;

theorem Th55: :: VFUNCT_2:55

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being PartFunc of b₁,the carrier of b₂
for b₄ being set st b₃ is_constant_on b₄ holds
( ( for b₅ being Complex holds b₅ (#) b₃ is_bounded_on b₄ ) & - b₃ is_bounded_on b₄ & ||.b₃.|| is_bounded_on b₄ )

proof end;

theorem Th56: :: VFUNCT_2:56

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅, b₆ being set st b₃ is_bounded_on b₅ & b₄ is_constant_on b₆ holds
b₃ + b₄ is_bounded_on b₅ /\ b₆

proof end;

theorem Th57: :: VFUNCT_2:57

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being PartFunc of b₁,the carrier of b₂
for b₅, b₆ being set st b₃ is_bounded_on b₅ & b₄ is_constant_on b₆ holds
( b₃ - b₄ is_bounded_on b₅ /\ b₆ & b₄ - b₃ is_bounded_on b₅ /\ b₆ )

proof end;