:: RUSUB_1 semantic presentation

definition

let c₁ be RealUnitarySpace;
mode Subspace of c₁ -> RealUnitarySpace means :Def1: :: RUSUB_1:def 1
( the carrier of a₂ c= the carrier of a₁ & the Zero of a₂ = the Zero of a₁ & the add of a₂ = the add of a₁ || the carrier of a₂ & the Mult of a₂ = the Mult of a₁ | [:REAL ,the carrier of a₂:] & the scalar of a₂ = the scalar of a₁ || the carrier of a₂ );
existence

proof end;

end;

:: deftheorem Def1 defines Subspace RUSUB_1:def 1 :

theorem Th1: :: RUSUB_1:1

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁
for b₄ being set st b₄ in b₂ & b₂ is Subspace of b₃ holds
b₄ in b₃

proof end;

theorem Th2: :: RUSUB_1:2

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being set st b₃ in b₂ holds
b₃ in b₁

proof end;

theorem Th3: :: RUSUB_1:3

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₂ holds b₃ is VECTOR of b₁

proof end;

theorem Th4: :: RUSUB_1:4

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds 0. b₂ = 0. b₁ by Def1;

theorem Th5: :: RUSUB_1:5

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds 0. b₂ = 0. b₃

proof end;

theorem Th6: :: RUSUB_1:6

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁
for b₅, b₆ being VECTOR of b₂ st b₅ = b₄ & b₆ = b₃ holds
b₅ + b₆ = b₄ + b₃

proof end;

theorem Th7: :: RUSUB_1:7

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁
for b₄ being VECTOR of b₂
for b₅ being Real st b₄ = b₃ holds
b₅ * b₄ = b₅ * b₃

proof end;

theorem Th8: :: RUSUB_1:8

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁
for b₅, b₆ being VECTOR of b₂ st b₅ = b₃ & b₆ = b₄ holds
b₅ .|. b₆ = b₃ .|. b₄

proof end;

theorem Th9: :: RUSUB_1:9

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁
for b₄ being VECTOR of b₂ st b₄ = b₃ holds
- b₃ = - b₄

proof end;

theorem Th10: :: RUSUB_1:10

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁
for b₅, b₆ being VECTOR of b₂ st b₅ = b₄ & b₆ = b₃ holds
b₅ - b₆ = b₄ - b₃

proof end;

theorem Th11: :: RUSUB_1:11

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds 0. b₁ in b₂

proof end;

theorem Th12: :: RUSUB_1:12

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds 0. b₂ in b₃

proof end;

theorem Th13: :: RUSUB_1:13

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds 0. b₂ in b₁

proof end;

Lemma10: for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being Subset of b₁ st the carrier of b₂ = b₃ holds
b₃ is lineary-closed

proof end;

theorem Th14: :: RUSUB_1:14

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ + b₄ in b₂

proof end;

theorem Th15: :: RUSUB_1:15

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁
for b₄ being Real st b₃ in b₂ holds
b₄ * b₃ in b₂

proof end;

theorem Th16: :: RUSUB_1:16

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ st b₃ in b₂ holds
- b₃ in b₂

proof end;

theorem Th17: :: RUSUB_1:17

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ - b₄ in b₂

proof end;

theorem Th18: :: RUSUB_1:18

for b₁ being RealUnitarySpace
for b₂ being Subset of b₁
for b₃ being non empty set
for b₄ being Element of b₃
for b₅ being BinOp of b₃
for b₆ being Function of [:REAL ,b₃:],b₃
for b₇ being Function of [:b₃,b₃:], REAL st b₂ = b₃ & b₄ = 0. b₁ & b₅ = the add of b₁ || b₂ & b₆ = the Mult of b₁ | [:REAL ,b₂:] & b₇ = the scalar of b₁ || b₂ holds
UNITSTR(# b₃,b₄,b₅,b₆,b₇ #) is Subspace of b₁

proof end;

theorem Th19: :: RUSUB_1:19

for b₁ being RealUnitarySpace holds b₁ is Subspace of b₁

proof end;

theorem Th20: :: RUSUB_1:20

for b₁, b₂ being strict RealUnitarySpace st b₁ is Subspace of b₂ & b₂ is Subspace of b₁ holds
b₁ = b₂

proof end;

theorem Th21: :: RUSUB_1:21

for b₁, b₂, b₃ being RealUnitarySpace st b₁ is Subspace of b₂ & b₂ is Subspace of b₃ holds
b₁ is Subspace of b₃

proof end;

theorem Th22: :: RUSUB_1:22

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is Subspace of b₃

proof end;

theorem Th23: :: RUSUB_1:23

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ st ( for b₄ being VECTOR of b₁ st b₄ in b₂ holds
b₄ in b₃ ) holds
b₂ is Subspace of b₃

proof end;

registration

let c₁ be RealUnitarySpace;
cluster strict Subspace of a₁;
existence

proof end;

end;

theorem Th24: :: RUSUB_1:24

for b₁ being RealUnitarySpace
for b₂, b₃ being strict Subspace of b₁ st the carrier of b₂ = the carrier of b₃ holds
b₂ = b₃

proof end;

theorem Th25: :: RUSUB_1:25

for b₁ being RealUnitarySpace
for b₂, b₃ being strict Subspace of b₁ st ( for b₄ being VECTOR of b₁ holds
( b₄ in b₂ iff b₄ in b₃ ) ) holds
b₂ = b₃

proof end;

theorem Th26: :: RUSUB_1:26

for b₁ being strict RealUnitarySpace
for b₂ being strict Subspace of b₁ st the carrier of b₂ = the carrier of b₁ holds
b₂ = b₁

proof end;

theorem Th27: :: RUSUB_1:27

for b₁ being strict RealUnitarySpace
for b₂ being strict Subspace of b₁ st ( for b₃ being VECTOR of b₁ holds
( b₃ in b₂ iff b₃ in b₁ ) ) holds
b₂ = b₁

proof end;

theorem Th28: :: RUSUB_1:28

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Subset of b₁ st the carrier of b₂ = b₃ holds
b₃ is lineary-closed by Lemma10;

theorem Th29: :: RUSUB_1:29

for b₁ being RealUnitarySpace
for b₂ being Subset of b₁ st b₂ <> {} & b₂ is lineary-closed holds
ex b₃ being strict Subspace of b₁ st b₂ = the carrier of b₃

proof end;

definition

let c₁ be RealUnitarySpace;
func (0). c₁ -> strict Subspace of a₁ means :Def2: :: RUSUB_1:def 2
the carrier of a₂ = {(0. a₁)};
correctness

proof end;

end;

:: deftheorem Def2 defines (0). RUSUB_1:def 2 :

definition

let c₁ be RealUnitarySpace;
func (Omega). c₁ -> strict Subspace of a₁ equals :: RUSUB_1:def 3
UNITSTR(# the carrier of a₁,the Zero of a₁,the add of a₁,the Mult of a₁,the scalar of a₁ #);
coherence

proof end;

end;

:: deftheorem Def3 defines (Omega). RUSUB_1:def 3 :

theorem Th30: :: RUSUB_1:30

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds (0). b₂ = (0). b₁

proof end;

theorem Th31: :: RUSUB_1:31

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds (0). b₂ = (0). b₃

proof end;

theorem Th32: :: RUSUB_1:32

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds (0). b₂ is Subspace of b₁ by Th21;

theorem Th33: :: RUSUB_1:33

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds (0). b₁ is Subspace of b₂

proof end;

theorem Th34: :: RUSUB_1:34

for b₁ being RealUnitarySpace
for b₂, b₃ being Subspace of b₁ holds (0). b₂ is Subspace of b₃

proof end;

theorem Th35: :: RUSUB_1:35

for b₁ being strict RealUnitarySpace holds b₁ is Subspace of (Omega). b₁ ;

definition

let c₁ be RealUnitarySpace;
let c₂ be VECTOR of c₁;
let c₃ be Subspace of c₁;
func c₂ + c₃ -> Subset of a₁ equals :: RUSUB_1:def 4
{ (a₂ + b₁) where B is VECTOR of a₁ : b₁ in a₃ } ;
coherence

proof end;

end;

:: deftheorem Def4 defines + RUSUB_1:def 4 :

Lemma26: for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds (0. b₁) + b₂ = the carrier of b₂

proof end;

definition

let c₁ be RealUnitarySpace;
let c₂ be Subspace of c₁;
mode Coset of c₂ -> Subset of a₁ means :Def5: :: RUSUB_1:def 5
ex b₁ being VECTOR of a₁ st a₃ = b₁ + a₂;
existence

proof end;

end;

:: deftheorem Def5 defines Coset RUSUB_1:def 5 :

theorem Th36: :: RUSUB_1:36

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ holds
( 0. b₁ in b₃ + b₂ iff b₃ in b₂ )

proof end;

theorem Th37: :: RUSUB_1:37

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ holds b₃ in b₃ + b₂

proof end;

theorem Th38: :: RUSUB_1:38

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds (0. b₁) + b₂ = the carrier of b₂ by Lemma26;

theorem Th39: :: RUSUB_1:39

for b₁ being RealUnitarySpace
for b₂ being VECTOR of b₁ holds b₂ + ((0). b₁) = {b₂}

proof end;

Lemma31: for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ holds
( b₃ in b₂ iff b₃ + b₂ = the carrier of b₂ )

proof end;

theorem Th40: :: RUSUB_1:40

for b₁ being RealUnitarySpace
for b₂ being VECTOR of b₁ holds b₂ + ((Omega). b₁) = the carrier of b₁

proof end;

theorem Th41: :: RUSUB_1:41

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ holds
( 0. b₁ in b₃ + b₂ iff b₃ + b₂ = the carrier of b₂ )

proof end;

theorem Th42: :: RUSUB_1:42

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ holds
( b₃ in b₂ iff b₃ + b₂ = the carrier of b₂ ) by Lemma31;

theorem Th43: :: RUSUB_1:43

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁
for b₄ being Real st b₃ in b₂ holds
(b₄ * b₃) + b₂ = the carrier of b₂

proof end;

theorem Th44: :: RUSUB_1:44

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁
for b₄ being Real st b₄ <> 0 & (b₄ * b₃) + b₂ = the carrier of b₂ holds
b₃ in b₂

proof end;

theorem Th45: :: RUSUB_1:45

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ holds
( b₃ in b₂ iff (- b₃) + b₂ = the carrier of b₂ )

proof end;

theorem Th46: :: RUSUB_1:46

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ holds
( b₃ in b₂ iff b₄ + b₂ = (b₄ + b₃) + b₂ )

proof end;

theorem Th47: :: RUSUB_1:47

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ holds
( b₃ in b₂ iff b₄ + b₂ = (b₄ - b₃) + b₂ )

proof end;

theorem Th48: :: RUSUB_1:48

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ holds
( b₄ in b₃ + b₂ iff b₃ + b₂ = b₄ + b₂ )

proof end;

theorem Th49: :: RUSUB_1:49

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ holds
( b₃ + b₂ = (- b₃) + b₂ iff b₃ in b₂ )

proof end;

theorem Th50: :: RUSUB_1:50

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄, b₅ being VECTOR of b₁ st b₃ in b₄ + b₂ & b₃ in b₅ + b₂ holds
b₄ + b₂ = b₅ + b₂

proof end;

theorem Th51: :: RUSUB_1:51

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ st b₃ in b₄ + b₂ & b₃ in (- b₄) + b₂ holds
b₄ in b₂

proof end;

theorem Th52: :: RUSUB_1:52

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁
for b₄ being Real st b₄ <> 1 & b₄ * b₃ in b₃ + b₂ holds
b₃ in b₂

proof end;

theorem Th53: :: RUSUB_1:53

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁
for b₄ being Real st b₃ in b₂ holds
b₄ * b₃ in b₃ + b₂

proof end;

theorem Th54: :: RUSUB_1:54

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ holds
( - b₃ in b₃ + b₂ iff b₃ in b₂ )

proof end;

theorem Th55: :: RUSUB_1:55

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ holds
( b₃ + b₄ in b₄ + b₂ iff b₃ in b₂ )

proof end;

theorem Th56: :: RUSUB_1:56

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ holds
( b₄ - b₃ in b₄ + b₂ iff b₃ in b₂ )

proof end;

theorem Th57: :: RUSUB_1:57

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ holds
( b₃ in b₄ + b₂ iff ex b₅ being VECTOR of b₁ st
( b₅ in b₂ & b₃ = b₄ + b₅ ) )

proof end;

theorem Th58: :: RUSUB_1:58

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ holds
( b₃ in b₄ + b₂ iff ex b₅ being VECTOR of b₁ st
( b₅ in b₂ & b₃ = b₄ - b₅ ) )

proof end;

theorem Th59: :: RUSUB_1:59

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ holds
( ex b₅ being VECTOR of b₁ st
( b₃ in b₅ + b₂ & b₄ in b₅ + b₂ ) iff b₃ - b₄ in b₂ )

proof end;

theorem Th60: :: RUSUB_1:60

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ st b₄ + b₂ = b₃ + b₂ holds
ex b₅ being VECTOR of b₁ st
( b₅ in b₂ & b₄ + b₅ = b₃ )

proof end;

theorem Th61: :: RUSUB_1:61

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ st b₄ + b₂ = b₃ + b₂ holds
ex b₅ being VECTOR of b₁ st
( b₅ in b₂ & b₄ - b₅ = b₃ )

proof end;

theorem Th62: :: RUSUB_1:62

for b₁ being RealUnitarySpace
for b₂, b₃ being strict Subspace of b₁
for b₄ being VECTOR of b₁ holds
( b₄ + b₂ = b₄ + b₃ iff b₂ = b₃ )

proof end;

theorem Th63: :: RUSUB_1:63

for b₁ being RealUnitarySpace
for b₂, b₃ being strict Subspace of b₁
for b₄, b₅ being VECTOR of b₁ st b₅ + b₂ = b₄ + b₃ holds
b₂ = b₃

proof end;

theorem Th64: :: RUSUB_1:64

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Coset of b₂ holds
( b₃ is lineary-closed iff b₃ = the carrier of b₂ )

proof end;

theorem Th65: :: RUSUB_1:65

for b₁ being RealUnitarySpace
for b₂, b₃ being strict Subspace of b₁
for b₄ being Coset of b₂
for b₅ being Coset of b₃ st b₄ = b₅ holds
b₂ = b₃

proof end;

theorem Th66: :: RUSUB_1:66

for b₁ being RealUnitarySpace
for b₂ being VECTOR of b₁ holds {b₂} is Coset of (0). b₁

proof end;

theorem Th67: :: RUSUB_1:67

for b₁ being RealUnitarySpace
for b₂ being Subset of b₁ st b₂ is Coset of (0). b₁ holds
ex b₃ being VECTOR of b₁ st b₂ = {b₃}

proof end;

theorem Th68: :: RUSUB_1:68

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁ holds the carrier of b₂ is Coset of b₂

proof end;

theorem Th69: :: RUSUB_1:69

for b₁ being RealUnitarySpace holds the carrier of b₁ is Coset of (Omega). b₁

proof end;

theorem Th70: :: RUSUB_1:70

for b₁ being RealUnitarySpace
for b₂ being Subset of b₁ st b₂ is Coset of (Omega). b₁ holds
b₂ = the carrier of b₁

proof end;

theorem Th71: :: RUSUB_1:71

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Coset of b₂ holds
( 0. b₁ in b₃ iff b₃ = the carrier of b₂ )

proof end;

theorem Th72: :: RUSUB_1:72

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Coset of b₂
for b₄ being VECTOR of b₁ holds
( b₄ in b₃ iff b₃ = b₄ + b₂ )

proof end;

theorem Th73: :: RUSUB_1:73

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Coset of b₂
for b₄, b₅ being VECTOR of b₁ st b₄ in b₃ & b₅ in b₃ holds
ex b₆ being VECTOR of b₁ st
( b₆ in b₂ & b₄ + b₆ = b₅ )

proof end;

theorem Th74: :: RUSUB_1:74

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being Coset of b₂
for b₄, b₅ being VECTOR of b₁ st b₄ in b₃ & b₅ in b₃ holds
ex b₆ being VECTOR of b₁ st
( b₆ in b₂ & b₄ - b₆ = b₅ )

proof end;

theorem Th75: :: RUSUB_1:75

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃, b₄ being VECTOR of b₁ holds
( ex b₅ being Coset of b₂ st
( b₃ in b₅ & b₄ in b₅ ) iff b₃ - b₄ in b₂ )

proof end;

theorem Th76: :: RUSUB_1:76

for b₁ being RealUnitarySpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁
for b₄, b₅ being Coset of b₂ st b₃ in b₄ & b₃ in b₅ holds
b₄ = b₅

proof end;