RLVECT

:: RLVECT_2 semantic presentation

begin

definition

let S be ( ( ) ( ) 1-sorted ) ;
let x be ( ( ) ( ) set ) ;
assume x : ( ( ) ( ) set ) in S : ( ( ) ( ) 1-sorted ) ;

func vector (S,x) -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: RLVECT_2:def 1
x : ( ( ) ( ) VectSpStr over S : ( ( ) ( ) 1-sorted ) ) ;

end;

theorem :: RLVECT_2:1

for S being ( ( non empty ) ( non empty ) 1-sorted )
for v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds vector (S : ( ( non empty ) ( non empty ) 1-sorted ) ,v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_2:2

theorem :: RLVECT_2:3

theorem :: RLVECT_2:4

theorem :: RLVECT_2:5

theorem :: RLVECT_2:6

theorem :: RLVECT_2:7

definition

let V be ( ( non empty ) ( non empty ) addLoopStr ) ;
let T be ( ( finite ) ( finite ) Subset of ) ;
assume ( V : ( ( non empty ) ( non empty ) addLoopStr ) is Abelian & V : ( ( non empty ) ( non empty ) addLoopStr ) is add-associative & V : ( ( non empty ) ( non empty ) addLoopStr ) is right_zeroed ) ;

func Sum T -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: RLVECT_2:def 2
ex F being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V122() V123() V124() V125() V126() V127() V128() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) st
( rng F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V122() V123() V124() V125() V126() V127() V128() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( finite ) Element of bool the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = T : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) 1-sorted ) ) & F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V122() V123() V124() V125() V126() V127() V128() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) is one-to-one & it : ( ( Function-like quasi_total ) ( Relation-like [:T : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) 1-sorted ) ) ,T : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) -defined T : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) 1-sorted ) ) -valued Function-like quasi_total ) Element of bool [:[:T : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) 1-sorted ) ) ,T : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,T : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = Sum F : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V122() V123() V124() V125() V126() V127() V128() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) );

end;

theorem :: RLVECT_2:8

theorem :: RLVECT_2:9

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr )
for v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Sum {v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty ext-real positive ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V122() V123() V124() V125() V126() V127() V128() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_2:10

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr )
for v1, v2 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st v1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> v2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
Sum {v1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = v1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + v2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_2:11

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr )
for v1, v2, v3 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st v1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> v2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & v2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> v3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & v1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> v3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
Sum {v1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,v2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,v3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (v1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + v2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) + v3 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_2:12

for V being ( ( non empty Abelian add-associative right_zeroed ) ( non empty Abelian add-associative right_zeroed V108() ) addLoopStr )
for S, T being ( ( finite ) ( finite ) Subset of ) st T : ( ( finite ) ( finite ) Subset of ) misses S : ( ( finite ) ( finite ) Subset of ) holds
Sum (T : ( ( finite ) ( finite ) Subset of ) \/ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty Abelian add-associative right_zeroed ) ( non empty Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (Sum T : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (Sum S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty Abelian add-associative right_zeroed ) ( non empty Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_2:13

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr )
for S, T being ( ( finite ) ( finite ) Subset of ) holds Sum (T : ( ( finite ) ( finite ) Subset of ) \/ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = ((Sum T : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (Sum S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) - (Sum (T : ( ( finite ) ( finite ) Subset of ) /\ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_2:14

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr )
for S, T being ( ( finite ) ( finite ) Subset of ) holds Sum (T : ( ( finite ) ( finite ) Subset of ) /\ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = ((Sum T : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (Sum S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) - (Sum (T : ( ( finite ) ( finite ) Subset of ) \/ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_2:15

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr )
for S, T being ( ( finite ) ( finite ) Subset of ) holds Sum (T : ( ( finite ) ( finite ) Subset of ) \ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (Sum (T : ( ( finite ) ( finite ) Subset of ) \/ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) - (Sum S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_2:16

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr )
for S, T being ( ( finite ) ( finite ) Subset of ) holds Sum (T : ( ( finite ) ( finite ) Subset of ) \ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (Sum T : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) - (Sum (T : ( ( finite ) ( finite ) Subset of ) /\ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_2:17

for V being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr )
for S, T being ( ( finite ) ( finite ) Subset of ) holds Sum (T : ( ( finite ) ( finite ) Subset of ) \+\ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (Sum (T : ( ( finite ) ( finite ) Subset of ) \/ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) - (Sum (T : ( ( finite ) ( finite ) Subset of ) /\ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: RLVECT_2:18

for V being ( ( non empty Abelian add-associative right_zeroed ) ( non empty Abelian add-associative right_zeroed V108() ) addLoopStr )
for S, T being ( ( finite ) ( finite ) Subset of ) holds Sum (T : ( ( finite ) ( finite ) Subset of ) \+\ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty Abelian add-associative right_zeroed ) ( non empty Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (Sum (T : ( ( finite ) ( finite ) Subset of ) \ S : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty Abelian add-associative right_zeroed ) ( non empty Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (Sum (S : ( ( finite ) ( finite ) Subset of ) \ T : ( ( finite ) ( finite ) Subset of ) ) : ( ( ) ( finite ) Element of bool the carrier of b₁ : ( ( non empty Abelian add-associative right_zeroed ) ( non empty Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty Abelian add-associative right_zeroed ) ( non empty Abelian add-associative right_zeroed V108() ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ;

definition

let V be ( ( non empty ) ( non empty ) ZeroStr ) ;

mode Linear_Combination of V -> ( ( ) ( Relation-like the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) -valued Function-like total quasi_total V112() V113() V114() ) Element of Funcs ( the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) ) ) means :: RLVECT_2:def 3
ex T being ( ( finite ) ( finite ) Subset of ) st
for v being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in T : ( ( finite ) ( finite ) Subset of ) holds
it : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) 1-sorted ) ) . v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) ) = 0 : ( ( ) ( ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V122() V123() V124() V125() V126() V127() V128() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ;

end;

notation

let V be ( ( non empty ) ( non empty ) addLoopStr ) ;
let L be ( ( ) ( Relation-like the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) -valued Function-like total quasi_total V112() V113() V114() ) Element of Funcs ( the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) ) ) ;
synonym Carrier L for support V;

end;

definition

:: original: Carrier
redefine func Carrier L -> ( ( ) ( ) Subset of ) equals :: RLVECT_2:def 4
{ v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where v is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : L : ( ( ) ( ) VectSpStr over V : ( ( ) ( ) 1-sorted ) ) . v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) ) <> 0 : ( ( ) ( ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V122() V123() V124() V125() V126() V127() V128() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) } ;

end;

registration

cluster Carrier : ( ( ) ( ) set ) -> finite ;

end;

theorem :: RLVECT_2:19

for V being ( ( non empty ) ( non empty ) addLoopStr )
for L being ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) -valued Function-like total quasi_total V112() V113() V114() ) Linear_Combination of V : ( ( non empty ) ( non empty ) addLoopStr ) )
for v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( L : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) -valued Function-like total quasi_total V112() V113() V114() ) Linear_Combination of b₁ : ( ( non empty ) ( non empty ) addLoopStr ) ) . v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) ) = 0 : ( ( ) ( ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V122() V123() V124() V125() V126() V127() V128() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) iff not v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in Carrier L : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) -valued Function-like total quasi_total V112() V113() V114() ) Linear_Combination of b₁ : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( finite ) Subset of ) ) ;

definition

let V be ( ( non empty ) ( non empty ) addLoopStr ) ;

func ZeroLC V -> ( ( ) ( Relation-like the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() V133() associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) -valued Function-like total quasi_total V112() V113() V114() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() V133() associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) means :: RLVECT_2:def 5
Carrier it : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Subset of ) = {} : ( ( ) ( ) set ) ;

end;

theorem :: RLVECT_2:20

for V being ( ( non empty ) ( non empty ) addLoopStr )
for v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (ZeroLC V : ( ( non empty ) ( non empty ) addLoopStr ) ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) -valued Function-like total quasi_total V112() V113() V114() ) Linear_Combination of b₁ : ( ( non empty ) ( non empty ) addLoopStr ) ) . v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) ) = 0 : ( ( ) ( ext-real ordinal natural V36() real finite cardinal V110() V111() V122() V123() V124() V125() V126() V127() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V122() V123() V124() V125() V126() V127() V128() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ;

definition

let V be ( ( non empty ) ( non empty ) addLoopStr ) ;
let A be ( ( ) ( ) Subset of ) ;

mode Linear_Combination of A -> ( ( ) ( Relation-like the carrier of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() V133() associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) -valued Function-like total quasi_total V112() V113() V114() ) Linear_Combination of V : ( ( non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed V108() V133() associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoopStr ) ) means :: RLVECT_2:def 6
Carrier it : ( ( Function-like quasi_total ) ( Relation-like [:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined A : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:[:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) c= A : ( ( non empty ) ( non empty ) set ) ;

end;

theorem :: RLVECT_2:21

theorem :: RLVECT_2:22

theorem :: RLVECT_2:23

definition

end;

theorem :: RLVECT_2:24

theorem :: RLVECT_2:25

theorem :: RLVECT_2:26

theorem :: RLVECT_2:27

theorem :: RLVECT_2:28

definition

end;

theorem :: RLVECT_2:29

theorem :: RLVECT_2:30

theorem :: RLVECT_2:31

theorem :: RLVECT_2:32

theorem :: RLVECT_2:33

theorem :: RLVECT_2:34

theorem :: RLVECT_2:35

theorem :: RLVECT_2:36

definition

let V be ( ( non empty ) ( non empty ) addLoopStr ) ;
let L1, L2 be ( ( ) ( Relation-like the carrier of V : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) -valued Function-like total quasi_total V112() V113() V114() ) Linear_Combination of V : ( ( non empty ) ( non empty ) addLoopStr ) ) ;

:: original: =
redefine pred L1 = L2 means :: RLVECT_2:def 9
for v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds L1 : ( ( non empty ) ( non empty ) set ) . v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) ) = L2 : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty ) ( non empty ) set ) ,L1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined L1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of bool [:[:L1 : ( ( non empty ) ( non empty ) set ) ,L1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,L1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty non trivial non finite V122() V123() V124() V128() ) set ) ) ;

end;

definition