:: by Wojciech A. Trybulec

::

:: Received July 24, 1989

:: Copyright (c) 1990-2021 Association of Mizar Users

:: deftheorem 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 ) ) );

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 Th1: :: RLSUB_1:1

for V being RealLinearSpace

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

0. V in V1

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

0. V in V1

proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem Th2: :: RLSUB_1:2

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

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:3

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

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 :: RLSUB_1:5

for V being RealLinearSpace

for V1 being Subset of V st the carrier of V = V1 holds

V1 is linearly-closed ;

for V1 being Subset of V st the carrier of V = V1 holds

V1 is linearly-closed ;

theorem :: RLSUB_1:6

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 u, v is VECTOR of V : ( v in V1 & u in V2 ) } holds

V3 is linearly-closed

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

V3 is linearly-closed

proof end;

theorem :: RLSUB_1:7

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

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;

ex b_{1} being RealLinearSpace st

( the carrier of b_{1} c= the carrier of V & 0. b_{1} = 0. V & the addF of b_{1} = the addF of V || the carrier of b_{1} & the Mult of b_{1} = the Mult of V | [:REAL, the carrier of b_{1}:] )

end;
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 ( 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:] );

ex b

( the carrier of b

proof end;

:: deftheorem Def2 defines Subspace RLSUB_1:def 2 :

for V, b_{2} being RealLinearSpace holds

( b_{2} is Subspace of V iff ( the carrier of b_{2} c= the carrier of V & 0. b_{2} = 0. V & the addF of b_{2} = the addF of V || the carrier of b_{2} & the Mult of b_{2} = the Mult of V | [:REAL, the carrier of b_{2}:] ) );

for V, b

( b

::

:: Axioms of the subspaces of real linear spaces.

::

:: Axioms of the subspaces of real linear spaces.

::

theorem :: RLSUB_1:8

for V being RealLinearSpace

for x being object

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

x in W2

for x being object

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

x in W2

proof end;

theorem Th10: :: RLSUB_1:10

for V being RealLinearSpace

for W being Subspace of V

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

for W being Subspace of V

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

proof end;

theorem :: RLSUB_1:11

theorem Th13: :: RLSUB_1:13

for V being RealLinearSpace

for u, v 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

for u, v 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 Th14: :: RLSUB_1:14

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

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 Th15: :: RLSUB_1:15

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

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 Th16: :: RLSUB_1:16

for V being RealLinearSpace

for u, v 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

for u, v 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 :: RLSUB_1:19

theorem Th20: :: RLSUB_1:20

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

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 Th21: :: RLSUB_1:21

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

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 Th22: :: RLSUB_1:22

for V being RealLinearSpace

for v being VECTOR of V

for W being Subspace of V st v in W holds

- v in W

for v being VECTOR of V

for W being Subspace of V st v in W holds

- v in W

proof end;

theorem Th23: :: RLSUB_1:23

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

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 Th24: :: RLSUB_1:24

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

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 Th27: :: RLSUB_1:27

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

V is Subspace of Y

V is Subspace of Y

proof end;

theorem Th28: :: RLSUB_1:28

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

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:29

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

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;

ex b_{1} being Subspace of V st b_{1} is strict

end;
cluster non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V111() for Subspace of V;

existence ex b

proof end;

theorem Th30: :: RLSUB_1:30

for V being RealLinearSpace

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

W1 = W2

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

W1 = W2

proof end;

theorem Th31: :: RLSUB_1:31

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

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:32

for V being strict RealLinearSpace

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

W = V

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

W = V

proof end;

theorem :: RLSUB_1:33

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

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:34

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;

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 Th35: :: RLSUB_1:35

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

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 of zero subspace and improper subspace of real linear space.

::

:: Definition of zero subspace and improper subspace of real linear space.

::

definition

let V be RealLinearSpace;

correctness

existence

ex b_{1} being strict Subspace of V st the carrier of b_{1} = {(0. V)};

uniqueness

for b_{1}, b_{2} being strict Subspace of V st the carrier of b_{1} = {(0. V)} & the carrier of b_{2} = {(0. V)} holds

b_{1} = b_{2};

by Th4, Th30, Th35;

end;
correctness

existence

ex b

uniqueness

for b

b

by Th4, Th30, Th35;

:: deftheorem Def3 defines (0). RLSUB_1:def 3 :

for V being RealLinearSpace

for b_{2} being strict Subspace of V holds

( b_{2} = (0). V iff the carrier of b_{2} = {(0. V)} );

for V being RealLinearSpace

for b

( b

definition

let V be RealLinearSpace;

RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V

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

RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V

proof 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 #);

for V being RealLinearSpace holds (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);

::

:: Definitional theorems of zero subspace and improper subspace.

::

:: Definitional theorems of zero subspace and improper subspace.

::

theorem :: RLSUB_1:38

::

:: Introduction of the cosets of subspace.

::

:: Introduction of the cosets of subspace.

::

definition

let V be RealLinearSpace;

let v be VECTOR of V;

let W be Subspace of V;

coherence

{ (v + u) where u is VECTOR of V : u in W } is Subset of V

end;
let v be VECTOR of V;

let W be Subspace of V;

coherence

{ (v + u) where u is VECTOR of V : u in W } is Subset of V

proof 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 } ;

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;

existence

ex b_{1} being Subset of V ex v being VECTOR of V st b_{1} = v + W

end;
let W be Subspace of V;

existence

ex b

proof end;

:: deftheorem Def6 defines Coset RLSUB_1:def 6 :

for V being RealLinearSpace

for W being Subspace of V

for b_{3} being Subset of V holds

( b_{3} is Coset of W iff ex v being VECTOR of V st b_{3} = v + W );

for V being RealLinearSpace

for W being Subspace of V

for b

( b

::

:: Definitional theorems of the cosets.

::

:: Definitional theorems of the cosets.

::

theorem Th42: :: RLSUB_1:42

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 )

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 :: RLSUB_1:44

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 Th46: :: RLSUB_1:46

for V being RealLinearSpace

for v being VECTOR of V holds v + ((Omega). V) = the carrier of V by STRUCT_0:def 5, Lm3;

for v being VECTOR of V holds v + ((Omega). V) = the carrier of V by STRUCT_0:def 5, Lm3;

theorem :: RLSUB_1:48

theorem Th49: :: RLSUB_1:49

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

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 Th50: :: RLSUB_1:50

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

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 Th51: :: RLSUB_1:51

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 )

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 Th52: :: RLSUB_1:52

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 )

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:53

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 )

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 Th54: :: RLSUB_1:54

for V being RealLinearSpace

for u, v being VECTOR of V

for W being Subspace of V holds

( v in u + W iff u + W = v + W )

for u, v being VECTOR of V

for W being Subspace of V holds

( v in u + W iff u + W = v + W )

proof end;

theorem Th55: :: RLSUB_1:55

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 )

for v being VECTOR of V

for W being Subspace of V holds

( v + W = (- v) + W iff v in W )

proof end;

theorem Th56: :: RLSUB_1:56

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

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:57

theorem Th58: :: RLSUB_1:58

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

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 Th59: :: RLSUB_1:59

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

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:60

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 )

for v being VECTOR of V

for W being Subspace of V holds

( - v in v + W iff v in W )

proof end;

theorem Th61: :: RLSUB_1:61

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 )

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:62

for V being RealLinearSpace

for u, v being VECTOR of V

for W being Subspace of V holds

( v - u in v + W iff u in W )

for u, v being VECTOR of V

for W being Subspace of V holds

( v - u in v + W iff u in W )

proof end;

theorem Th63: :: RLSUB_1:63

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

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:64

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

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 Th65: :: RLSUB_1:65

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 )

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 Th66: :: RLSUB_1:66

for V being RealLinearSpace

for u, v 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 )

for u, v 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 Th67: :: RLSUB_1:67

for V being RealLinearSpace

for u, v 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 )

for u, v 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 Th68: :: RLSUB_1:68

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 )

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 Th69: :: RLSUB_1:69

for V being RealLinearSpace

for u, v being VECTOR of V

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

W1 = W2

for u, v being VECTOR of V

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

W1 = W2

proof end;

::

:: Theorems concerning cosets of subspace

:: regarded as subsets of the carrier.

::

:: Theorems concerning cosets of subspace

:: regarded as subsets of the carrier.

::

theorem :: RLSUB_1:70

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 )

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:71

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

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:73

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}

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:76

for V being RealLinearSpace

for V1 being Subset of V st V1 is Coset of (Omega). V holds

V1 = the carrier of V

for V1 being Subset of V st V1 is Coset of (Omega). V holds

V1 = the carrier of V

proof end;

theorem :: RLSUB_1:77

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 )

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 Th78: :: RLSUB_1:78

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 )

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:79

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 )

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:80

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 )

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:81

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 )

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:82

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

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;

:: Introduction of predicate linearly closed subsets of the carrier.

::