:: Subspaces and Cosets of Subspaces in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received July 24, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

let V be RealLinearSpace;
let V1 be Subset of V;
attr V1 is linearly-closed means :Def1: :: RLSUB_1:def 1
( ( for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1 ) );

end;

:: deftheorem Def1 defines linearly-closed RLSUB_1:def 1 :
for V being RealLinearSpace
for V1 being Subset of V holds
( V1 is linearly-closed iff ( ( for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1 ) ) );

theorem :: RLSUB_1:1

canceled;

theorem :: RLSUB_1:2

canceled;

theorem :: RLSUB_1:3

canceled;

theorem Th4: :: RLSUB_1:4

for V being RealLinearSpace
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
0. V in V1

proof end;

theorem Th5: :: RLSUB_1:5

for V being RealLinearSpace
for V1 being Subset of V st V1 is linearly-closed holds
for v being VECTOR of V st v in V1 holds
- v in V1

proof end;

theorem :: RLSUB_1:6

for V being RealLinearSpace
for V1 being Subset of V st V1 is linearly-closed holds
for v, u being VECTOR of V st v in V1 & u in V1 holds
v - u in V1

proof end;

theorem Th7: :: RLSUB_1:7

for V being RealLinearSpace holds {(0. V)} is linearly-closed

proof end;

theorem :: RLSUB_1:8

for V being RealLinearSpace
for V1 being Subset of V st the carrier of V = V1 holds
V1 is linearly-closed

proof end;

theorem :: RLSUB_1:9

for V being RealLinearSpace
for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } holds
V3 is linearly-closed

proof end;

theorem :: RLSUB_1:10

for V being RealLinearSpace
for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds
V1 /\ V2 is linearly-closed

proof end;

definition

let V be RealLinearSpace;
mode Subspace of V -> RealLinearSpace means :Def2: :: RLSUB_1:def 2
( the carrier of it c= the carrier of V & 0. it = 0. V & the addF of it = the addF of V || the carrier of it & the Mult of it = the Mult of V | [:REAL, the carrier of it:] );
existence
ex b₁ being RealLinearSpace st
( the carrier of b₁ c= the carrier of V & 0. b₁ = 0. V & the addF of b₁ = the addF of V || the carrier of b₁ & the Mult of b₁ = the Mult of V | [:REAL, the carrier of b₁:] )

proof end;

end;

:: deftheorem Def2 defines Subspace RLSUB_1:def 2 :
for V, b₂ being RealLinearSpace holds
( b₂ is Subspace of V iff ( the carrier of b₂ c= the carrier of V & 0. b₂ = 0. V & the addF of b₂ = the addF of V || the carrier of b₂ & the Mult of b₂ = the Mult of V | [:REAL, the carrier of b₂:] ) );

theorem :: RLSUB_1:11

canceled;

theorem :: RLSUB_1:12

canceled;

theorem :: RLSUB_1:13

canceled;

theorem :: RLSUB_1:14

canceled;

theorem :: RLSUB_1:15

canceled;

theorem :: RLSUB_1:16

for V being RealLinearSpace
for x being set
for W1, W2 being Subspace of V st x in W1 & W1 is Subspace of W2 holds
x in W2

proof end;

theorem Th17: :: RLSUB_1:17

for V being RealLinearSpace
for x being set
for W being Subspace of V st x in W holds
x in V

proof end;

theorem Th18: :: RLSUB_1:18

for V being RealLinearSpace
for W being Subspace of V
for w being VECTOR of W holds w is VECTOR of V

proof end;

theorem :: RLSUB_1:19

for V being RealLinearSpace
for W being Subspace of V holds 0. W = 0. V by Def2;

theorem :: RLSUB_1:20

for V being RealLinearSpace
for W1, W2 being Subspace of V holds 0. W1 = 0. W2

proof end;

theorem Th21: :: RLSUB_1:21

for V being RealLinearSpace
for v, u being VECTOR of V
for W being Subspace of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 + w2 = v + u

proof end;

theorem Th22: :: RLSUB_1:22

for V being RealLinearSpace
for v being VECTOR of V
for a being Real
for W being Subspace of V
for w being VECTOR of W st w = v holds
a * w = a * v

proof end;

theorem Th23: :: RLSUB_1:23

for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V
for w being VECTOR of W st w = v holds
- v = - w

proof end;

theorem Th24: :: RLSUB_1:24

for V being RealLinearSpace
for v, u being VECTOR of V
for W being Subspace of V
for w1, w2 being VECTOR of W st w1 = v & w2 = u holds
w1 - w2 = v - u

proof end;

Lm1: for V being RealLinearSpace
for V1 being Subset of V
for W being Subspace of V st the carrier of W = V1 holds
V1 is linearly-closed

proof end;

theorem Th25: :: RLSUB_1:25

for V being RealLinearSpace
for W being Subspace of V holds 0. V in W

proof end;

theorem :: RLSUB_1:26

for V being RealLinearSpace
for W1, W2 being Subspace of V holds 0. W1 in W2

proof end;

theorem :: RLSUB_1:27

for V being RealLinearSpace
for W being Subspace of V holds 0. W in V by Th17, RLVECT_1:3;

theorem Th28: :: RLSUB_1:28

for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V st u in W & v in W holds
u + v in W

proof end;

theorem Th29: :: RLSUB_1:29

for V being RealLinearSpace
for v being VECTOR of V
for a being Real
for W being Subspace of V st v in W holds
a * v in W

proof end;

theorem Th30: :: RLSUB_1:30

for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V st v in W holds
- v in W

proof end;

theorem Th31: :: RLSUB_1:31

for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V st u in W & v in W holds
u - v in W

proof end;

theorem Th32: :: RLSUB_1:32

for V being RealLinearSpace
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:REAL,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
RLSStruct(# D,d1,A,M #) is Subspace of V

proof end;

theorem Th33: :: RLSUB_1:33

for V being RealLinearSpace holds V is Subspace of V

proof end;

theorem Th34: :: RLSUB_1:34

for V, X being strict RealLinearSpace st V is Subspace of X & X is Subspace of V holds
V = X

proof end;

theorem Th35: :: RLSUB_1:35

for V, X, Y being RealLinearSpace st V is Subspace of X & X is Subspace of Y holds
V is Subspace of Y

proof end;

theorem Th36: :: RLSUB_1:36

for V being RealLinearSpace
for W1, W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 is Subspace of W2

proof end;

theorem :: RLSUB_1:37

for V being RealLinearSpace
for W1, W2 being Subspace of V st ( for v being VECTOR of V st v in W1 holds
v in W2 ) holds
W1 is Subspace of W2

proof end;

registration

let V be RealLinearSpace;
cluster non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V96() Subspace of V;
existence
ex b₁ being Subspace of V st b₁ is strict

proof end;

end;

theorem Th38: :: RLSUB_1:38

for V being RealLinearSpace
for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds
W1 = W2

proof end;

theorem Th39: :: RLSUB_1:39

for V being RealLinearSpace
for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds
( v in W1 iff v in W2 ) ) holds
W1 = W2

proof end;

theorem :: RLSUB_1:40

for V being strict RealLinearSpace
for W being strict Subspace of V st the carrier of W = the carrier of V holds
W = V

proof end;

theorem :: RLSUB_1:41

for V being strict RealLinearSpace
for W being strict Subspace of V st ( for v being VECTOR of V holds
( v in W iff v in V ) ) holds
W = V

proof end;

theorem :: RLSUB_1:42

for V being RealLinearSpace
for V1 being Subset of V
for W being Subspace of V st the carrier of W = V1 holds
V1 is linearly-closed by Lm1;

theorem Th43: :: RLSUB_1:43

for V being RealLinearSpace
for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds
ex W being strict Subspace of V st V1 = the carrier of W

proof end;

definition

let V be RealLinearSpace;
func (0). V -> strict Subspace of V means :Def3: :: RLSUB_1:def 3
the carrier of it = {(0. V)};
correctness
existence
ex b₁ being strict Subspace of V st the carrier of b₁ = {(0. V)};
uniqueness
for b₁, b₂ being strict Subspace of V st the carrier of b₁ = {(0. V)} & the carrier of b₂ = {(0. V)} holds
b₁ = b₂;
by Th7, Th38, Th43;

end;

:: deftheorem Def3 defines (0). RLSUB_1:def 3 :
for V being RealLinearSpace
for b₂ being strict Subspace of V holds
( b₂ = (0). V iff the carrier of b₂ = {(0. V)} );

definition

let V be RealLinearSpace;
func (Omega). V -> strict Subspace of V equals :: RLSUB_1:def 4
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);
coherence
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V

proof end;

end;

:: deftheorem defines (Omega). RLSUB_1:def 4 :
for V being RealLinearSpace holds (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);

theorem :: RLSUB_1:44

canceled;

theorem :: RLSUB_1:45

canceled;

theorem :: RLSUB_1:46

canceled;

theorem :: RLSUB_1:47

canceled;

theorem Th48: :: RLSUB_1:48

for V being RealLinearSpace
for W being Subspace of V holds (0). W = (0). V

proof end;

theorem Th49: :: RLSUB_1:49

for V being RealLinearSpace
for W1, W2 being Subspace of V holds (0). W1 = (0). W2

proof end;

theorem :: RLSUB_1:50

for V being RealLinearSpace
for W being Subspace of V holds (0). W is Subspace of V by Th35;

theorem :: RLSUB_1:51

for V being RealLinearSpace
for W being Subspace of V holds (0). V is Subspace of W

proof end;

theorem :: RLSUB_1:52

for V being RealLinearSpace
for W1, W2 being Subspace of V holds (0). W1 is Subspace of W2

proof end;

theorem :: RLSUB_1:53

canceled;

theorem :: RLSUB_1:54

for V being strict RealLinearSpace holds V is Subspace of (Omega). V ;

definition

let V be RealLinearSpace;
let v be VECTOR of V;
let W be Subspace of V;
func v + W -> Subset of V equals :: RLSUB_1:def 5
{ (v + u) where u is VECTOR of V : u in W } ;
coherence
{ (v + u) where u is VECTOR of V : u in W } is Subset of V

proof end;

end;

:: deftheorem defines + RLSUB_1:def 5 :
for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds v + W = { (v + u) where u is VECTOR of V : u in W } ;

Lm2: for V being RealLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W

proof end;

definition

let V be RealLinearSpace;
let W be Subspace of V;
mode Coset of W -> Subset of V means :Def6: :: RLSUB_1:def 6
ex v being VECTOR of V st it = v + W;
existence
ex b₁ being Subset of V ex v being VECTOR of V st b₁ = v + W

proof end;

end;

:: deftheorem Def6 defines Coset RLSUB_1:def 6 :
for V being RealLinearSpace
for W being Subspace of V
for b₃ being Subset of V holds
( b₃ is Coset of W iff ex v being VECTOR of V st b₃ = v + W );

theorem :: RLSUB_1:55

canceled;

theorem :: RLSUB_1:56

canceled;

theorem :: RLSUB_1:57

canceled;

theorem Th58: :: RLSUB_1:58

for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( 0. V in v + W iff v in W )

proof end;

theorem Th59: :: RLSUB_1:59

for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds v in v + W

proof end;

theorem :: RLSUB_1:60

for V being RealLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W by Lm2;

theorem Th61: :: RLSUB_1:61

for V being RealLinearSpace
for v being VECTOR of V holds v + ((0). V) = {v}

proof end;

Lm3: for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )

proof end;

theorem Th62: :: RLSUB_1:62

for V being RealLinearSpace
for v being VECTOR of V holds v + ((Omega). V) = the carrier of V

proof end;

theorem Th63: :: RLSUB_1:63

for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( 0. V in v + W iff v + W = the carrier of W )

proof end;

theorem :: RLSUB_1:64

for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W ) by Lm3;

theorem Th65: :: RLSUB_1:65

for V being RealLinearSpace
for v being VECTOR of V
for a being Real
for W being Subspace of V st v in W holds
(a * v) + W = the carrier of W

proof end;

theorem Th66: :: RLSUB_1:66

for V being RealLinearSpace
for v being VECTOR of V
for a being Real
for W being Subspace of V st a <> 0 & (a * v) + W = the carrier of W holds
v in W

proof end;

theorem Th67: :: RLSUB_1:67

for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v in W iff (- v) + W = the carrier of W )

proof end;

theorem Th68: :: RLSUB_1:68

for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in W iff v + W = (v + u) + W )

proof end;

theorem :: RLSUB_1:69

for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in W iff v + W = (v - u) + W )

proof end;

theorem Th70: :: RLSUB_1:70

for V being RealLinearSpace
for v, u being VECTOR of V
for W being Subspace of V holds
( v in u + W iff u + W = v + W )

proof end;

theorem Th71: :: RLSUB_1:71

for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v + W = (- v) + W iff v in W )

proof end;

theorem Th72: :: RLSUB_1:72

for V being RealLinearSpace
for u, v1, v2 being VECTOR of V
for W being Subspace of V st u in v1 + W & u in v2 + W holds
v1 + W = v2 + W

proof end;

theorem :: RLSUB_1:73

for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V st u in v + W & u in (- v) + W holds
v in W

proof end;

theorem Th74: :: RLSUB_1:74

for V being RealLinearSpace
for v being VECTOR of V
for a being Real
for W being Subspace of V st a <> 1 & a * v in v + W holds
v in W

proof end;

theorem Th75: :: RLSUB_1:75

for V being RealLinearSpace
for v being VECTOR of V
for a being Real
for W being Subspace of V st v in W holds
a * v in v + W

proof end;

theorem :: RLSUB_1:76

for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( - v in v + W iff v in W )

proof end;

theorem Th77: :: RLSUB_1:77

for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u + v in v + W iff u in W )

proof end;

theorem :: RLSUB_1:78

for V being RealLinearSpace
for v, u being VECTOR of V
for W being Subspace of V holds
( v - u in v + W iff u in W )

proof end;

theorem Th79: :: RLSUB_1:79

for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v + v1 ) )

proof end;

theorem :: RLSUB_1:80

for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V holds
( u in v + W iff ex v1 being VECTOR of V st
( v1 in W & u = v - v1 ) )

proof end;

theorem Th81: :: RLSUB_1:81

for V being RealLinearSpace
for v1, v2 being VECTOR of V
for W being Subspace of V holds
( ex v being VECTOR of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )

proof end;

theorem Th82: :: RLSUB_1:82

for V being RealLinearSpace
for v, u being VECTOR of V
for W being Subspace of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v + v1 = u )

proof end;

theorem Th83: :: RLSUB_1:83

for V being RealLinearSpace
for v, u being VECTOR of V
for W being Subspace of V st v + W = u + W holds
ex v1 being VECTOR of V st
( v1 in W & v - v1 = u )

proof end;

theorem Th84: :: RLSUB_1:84

for V being RealLinearSpace
for v being VECTOR of V
for W1, W2 being strict Subspace of V holds
( v + W1 = v + W2 iff W1 = W2 )

proof end;

theorem Th85: :: RLSUB_1:85

for V being RealLinearSpace
for v, u being VECTOR of V
for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds
W1 = W2

proof end;

theorem :: RLSUB_1:86

for V being RealLinearSpace
for W being Subspace of V
for C being Coset of W holds
( C is linearly-closed iff C = the carrier of W )

proof end;

theorem :: RLSUB_1:87

for V being RealLinearSpace
for W1, W2 being strict Subspace of V
for C1 being Coset of W1
for C2 being Coset of W2 st C1 = C2 holds
W1 = W2

proof end;

theorem :: RLSUB_1:88

for V being RealLinearSpace
for v being VECTOR of V holds {v} is Coset of (0). V

proof end;

theorem :: RLSUB_1:89

for V being RealLinearSpace
for V1 being Subset of V st V1 is Coset of (0). V holds
ex v being VECTOR of V st V1 = {v}

proof end;

theorem :: RLSUB_1:90

for V being RealLinearSpace
for W being Subspace of V holds the carrier of W is Coset of W

proof end;

theorem :: RLSUB_1:91

for V being RealLinearSpace holds the carrier of V is Coset of (Omega). V

proof end;

theorem :: RLSUB_1:92

for V being RealLinearSpace
for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V

proof end;

theorem :: RLSUB_1:93

for V being RealLinearSpace
for W being Subspace of V
for C being Coset of W holds
( 0. V in C iff C = the carrier of W )

proof end;

theorem Th94: :: RLSUB_1:94

for V being RealLinearSpace
for u being VECTOR of V
for W being Subspace of V
for C being Coset of W holds
( u in C iff C = u + W )

proof end;

theorem :: RLSUB_1:95

for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V
for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u + v1 = v )

proof end;

theorem :: RLSUB_1:96

for V being RealLinearSpace
for u, v being VECTOR of V
for W being Subspace of V
for C being Coset of W st u in C & v in C holds
ex v1 being VECTOR of V st
( v1 in W & u - v1 = v )

proof end;

theorem :: RLSUB_1:97

for V being RealLinearSpace
for v1, v2 being VECTOR of V
for W being Subspace of V holds
( ex C being Coset of W st
( v1 in C & v2 in C ) iff v1 - v2 in W )

proof end;

theorem :: RLSUB_1:98

for V being RealLinearSpace
for u being VECTOR of V
for W being Subspace of V
for B, C being Coset of W st u in B & u in C holds
B = C

proof end;