:: VECTSP_6 semantic presentation
begin
definition
let GF be non empty ZeroStr ;
let V be non empty VectSpStr over GF;
mode Linear_Combination of V -> Element of Funcs ( the carrier of V, the carrier of GF) means :Def1: :: VECTSP_6:def 1
ex T being finite Subset of V st
for v being Element of V st not v in T holds
it . v = 0. GF;
existence
ex b1 being Element of Funcs ( the carrier of V, the carrier of GF) ex T being finite Subset of V st
for v being Element of V st not v in T holds
b1 . v = 0. GF
proof
reconsider f = the carrier of V --> (0. GF) as Function of the carrier of V, the carrier of GF ;
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
take f ; ::_thesis: ex T being finite Subset of V st
for v being Element of V st not v in T holds
f . v = 0. GF
take {} V ; ::_thesis: for v being Element of V st not v in {} V holds
f . v = 0. GF
thus for v being Element of V st not v in {} V holds
f . v = 0. GF by FUNCOP_1:7; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Linear_Combination VECTSP_6:def_1_:_
for GF being non empty ZeroStr
for V being non empty VectSpStr over GF
for b3 being Element of Funcs ( the carrier of V, the carrier of GF) holds
( b3 is Linear_Combination of V iff ex T being finite Subset of V st
for v being Element of V st not v in T holds
b3 . v = 0. GF );
definition
let GF be non empty ZeroStr ;
let V be non empty VectSpStr over GF;
let L be Linear_Combination of V;
func Carrier L -> finite Subset of V equals :: VECTSP_6:def 2
{ v where v is Element of V : L . v <> 0. GF } ;
coherence
{ v where v is Element of V : L . v <> 0. GF } is finite Subset of V
proof
set A = { v where v is Element of V : L . v <> 0. GF } ;
consider T being finite Subset of V such that
A1: for v being Element of V st not v in T holds
L . v = 0. GF by Def1;
{ v where v is Element of V : L . v <> 0. GF } c= T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Element of V : L . v <> 0. GF } or x in T )
assume x in { v where v is Element of V : L . v <> 0. GF } ; ::_thesis: x in T
then ex v being Element of V st
( x = v & L . v <> 0. GF ) ;
hence x in T by A1; ::_thesis: verum
end;
hence { v where v is Element of V : L . v <> 0. GF } is finite Subset of V by XBOOLE_1:1; ::_thesis: verum
end;
end;
:: deftheorem defines Carrier VECTSP_6:def_2_:_
for GF being non empty ZeroStr
for V being non empty VectSpStr over GF
for L being Linear_Combination of V holds Carrier L = { v where v is Element of V : L . v <> 0. GF } ;
theorem :: VECTSP_6:1
for x being set
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds
( x in Carrier L iff ex v being Element of V st
( x = v & L . v <> 0. GF ) ) ;
theorem :: VECTSP_6:2
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L being Linear_Combination of V holds
( L . v = 0. GF iff not v in Carrier L )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L being Linear_Combination of V holds
( L . v = 0. GF iff not v in Carrier L )
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V
for L being Linear_Combination of V holds
( L . v = 0. GF iff not v in Carrier L )
let v be Element of V; ::_thesis: for L being Linear_Combination of V holds
( L . v = 0. GF iff not v in Carrier L )
let L be Linear_Combination of V; ::_thesis: ( L . v = 0. GF iff not v in Carrier L )
thus ( L . v = 0. GF implies not v in Carrier L ) ::_thesis: ( not v in Carrier L implies L . v = 0. GF )
proof
assume A1: L . v = 0. GF ; ::_thesis: not v in Carrier L
assume v in Carrier L ; ::_thesis: contradiction
then ex u being Element of V st
( u = v & L . u <> 0. GF ) ;
hence contradiction by A1; ::_thesis: verum
end;
assume not v in Carrier L ; ::_thesis: L . v = 0. GF
hence L . v = 0. GF ; ::_thesis: verum
end;
definition
let GF be non empty ZeroStr ;
let V be non empty VectSpStr over GF;
func ZeroLC V -> Linear_Combination of V means :Def3: :: VECTSP_6:def 3
Carrier it = {} ;
existence
ex b1 being Linear_Combination of V st Carrier b1 = {}
proof
reconsider f = the carrier of V --> (0. GF) as Function of the carrier of V, the carrier of GF ;
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
f is Linear_Combination of V
proof
reconsider T = {} V as empty finite Subset of V ;
take T ; :: according to VECTSP_6:def_1 ::_thesis: for v being Element of V st not v in T holds
f . v = 0. GF
thus for v being Element of V st not v in T holds
f . v = 0. GF by FUNCOP_1:7; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V ;
take f ; ::_thesis: Carrier f = {}
set C = { v where v is Element of V : f . v <> 0. GF } ;
now__::_thesis:_not__{__v_where_v_is_Element_of_V_:_f_._v_<>_0._GF__}__<>_{}
set x = the Element of { v where v is Element of V : f . v <> 0. GF } ;
assume { v where v is Element of V : f . v <> 0. GF } <> {} ; ::_thesis: contradiction
then the Element of { v where v is Element of V : f . v <> 0. GF } in { v where v is Element of V : f . v <> 0. GF } ;
then ex v being Element of V st
( the Element of { v where v is Element of V : f . v <> 0. GF } = v & f . v <> 0. GF ) ;
hence contradiction by FUNCOP_1:7; ::_thesis: verum
end;
hence Carrier f = {} ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Linear_Combination of V st Carrier b1 = {} & Carrier b2 = {} holds
b1 = b2
proof
let L, L9 be Linear_Combination of V; ::_thesis: ( Carrier L = {} & Carrier L9 = {} implies L = L9 )
reconsider K = L, K9 = L9 as Function of the carrier of V, the carrier of GF ;
assume that
A1: Carrier L = {} and
A2: Carrier L9 = {} ; ::_thesis: L = L9
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_
K_._x_=_K9_._x
let x be set ; ::_thesis: ( x in the carrier of V implies K . x = K9 . x )
assume x in the carrier of V ; ::_thesis: K . x = K9 . x
then reconsider v = x as Element of V ;
A3: now__::_thesis:_not_L9_._v_<>_0._GF
assume L9 . v <> 0. GF ; ::_thesis: contradiction
then v in { u where u is Element of V : L9 . u <> 0. GF } ;
hence contradiction by A2; ::_thesis: verum
end;
now__::_thesis:_not_L_._v_<>_0._GF
assume L . v <> 0. GF ; ::_thesis: contradiction
then v in { u where u is Element of V : L . u <> 0. GF } ;
hence contradiction by A1; ::_thesis: verum
end;
hence K . x = K9 . x by A3; ::_thesis: verum
end;
hence L = L9 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines ZeroLC VECTSP_6:def_3_:_
for GF being non empty ZeroStr
for V being non empty VectSpStr over GF
for b3 being Linear_Combination of V holds
( b3 = ZeroLC V iff Carrier b3 = {} );
theorem Th3: :: VECTSP_6:3
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V holds (ZeroLC V) . v = 0. GF
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V holds (ZeroLC V) . v = 0. GF
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V holds (ZeroLC V) . v = 0. GF
let v be Element of V; ::_thesis: (ZeroLC V) . v = 0. GF
( Carrier (ZeroLC V) = {} & not v in {} ) by Def3;
hence (ZeroLC V) . v = 0. GF ; ::_thesis: verum
end;
definition
let GF be non empty ZeroStr ;
let V be non empty VectSpStr over GF;
let A be Subset of V;
mode Linear_Combination of A -> Linear_Combination of V means :Def4: :: VECTSP_6:def 4
Carrier it c= A;
existence
ex b1 being Linear_Combination of V st Carrier b1 c= A
proof
take L = ZeroLC V; ::_thesis: Carrier L c= A
Carrier L = {} by Def3;
hence Carrier L c= A by XBOOLE_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Linear_Combination VECTSP_6:def_4_:_
for GF being non empty ZeroStr
for V being non empty VectSpStr over GF
for A being Subset of V
for b4 being Linear_Combination of V holds
( b4 is Linear_Combination of A iff Carrier b4 c= A );
theorem :: VECTSP_6:4
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B
let A, B be Subset of V; ::_thesis: for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B
let l be Linear_Combination of A; ::_thesis: ( A c= B implies l is Linear_Combination of B )
assume A1: A c= B ; ::_thesis: l is Linear_Combination of B
Carrier l c= A by Def4;
then Carrier l c= B by A1, XBOOLE_1:1;
hence l is Linear_Combination of B by Def4; ::_thesis: verum
end;
theorem Th5: :: VECTSP_6:5
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V holds ZeroLC V is Linear_Combination of A
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V holds ZeroLC V is Linear_Combination of A
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for A being Subset of V holds ZeroLC V is Linear_Combination of A
let A be Subset of V; ::_thesis: ZeroLC V is Linear_Combination of A
( Carrier (ZeroLC V) = {} & {} c= A ) by Def3, XBOOLE_1:2;
hence ZeroLC V is Linear_Combination of A by Def4; ::_thesis: verum
end;
theorem Th6: :: VECTSP_6:6
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for l being Linear_Combination of {} the carrier of V holds l = ZeroLC V
let l be Linear_Combination of {} the carrier of V; ::_thesis: l = ZeroLC V
Carrier l c= {} by Def4;
then Carrier l = {} ;
hence l = ZeroLC V by Def3; ::_thesis: verum
end;
theorem :: VECTSP_6:7
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds L is Linear_Combination of Carrier L by Def4;
definition
let GF be non empty addLoopStr ;
let V be non empty VectSpStr over GF;
let F be FinSequence of the carrier of V;
let f be Function of V,GF;
funcf (#) F -> FinSequence of V means :Def5: :: VECTSP_6:def 5
( len it = len F & ( for i being Nat st i in dom it holds
it . i = (f . (F /. i)) * (F /. i) ) );
existence
ex b1 being FinSequence of V st
( len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = (f . (F /. i)) * (F /. i) ) )
proof
deffunc H1( Nat) -> Element of the carrier of V = (f . (F /. $1)) * (F /. $1);
consider G being FinSequence such that
A1: len G = len F and
A2: for n being Nat st n in dom G holds
G . n = H1(n) from FINSEQ_1:sch_2();
rng G c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in the carrier of V )
assume x in rng G ; ::_thesis: x in the carrier of V
then consider y being set such that
A3: y in dom G and
A4: G . y = x by FUNCT_1:def_3;
y in Seg (len F) by A1, A3, FINSEQ_1:def_3;
then reconsider y = y as Element of NAT ;
G . y = (f . (F /. y)) * (F /. y) by A2, A3;
hence x in the carrier of V by A4; ::_thesis: verum
end;
then reconsider G = G as FinSequence of the carrier of V by FINSEQ_1:def_4;
take G ; ::_thesis: ( len G = len F & ( for i being Nat st i in dom G holds
G . i = (f . (F /. i)) * (F /. i) ) )
thus ( len G = len F & ( for i being Nat st i in dom G holds
G . i = (f . (F /. i)) * (F /. i) ) ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of V st len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = (f . (F /. i)) * (F /. i) ) & len b2 = len F & ( for i being Nat st i in dom b2 holds
b2 . i = (f . (F /. i)) * (F /. i) ) holds
b1 = b2
proof
let H1, H2 be FinSequence of the carrier of V; ::_thesis: ( len H1 = len F & ( for i being Nat st i in dom H1 holds
H1 . i = (f . (F /. i)) * (F /. i) ) & len H2 = len F & ( for i being Nat st i in dom H2 holds
H2 . i = (f . (F /. i)) * (F /. i) ) implies H1 = H2 )
assume that
A5: len H1 = len F and
A6: for i being Nat st i in dom H1 holds
H1 . i = (f . (F /. i)) * (F /. i) and
A7: len H2 = len F and
A8: for i being Nat st i in dom H2 holds
H2 . i = (f . (F /. i)) * (F /. i) ; ::_thesis: H1 = H2
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_H1_holds_
H1_._k_=_H2_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len H1 implies H1 . k = H2 . k )
assume ( 1 <= k & k <= len H1 ) ; ::_thesis: H1 . k = H2 . k
then A9: k in Seg (len H1) by FINSEQ_1:1;
then k in dom H1 by FINSEQ_1:def_3;
then A10: H1 . k = (f . (F /. k)) * (F /. k) by A6;
k in dom H2 by A5, A7, A9, FINSEQ_1:def_3;
hence H1 . k = H2 . k by A8, A10; ::_thesis: verum
end;
hence H1 = H2 by A5, A7, FINSEQ_1:14; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines (#) VECTSP_6:def_5_:_
for GF being non empty addLoopStr
for V being non empty VectSpStr over GF
for F being FinSequence of the carrier of V
for f being Function of V,GF
for b5 being FinSequence of V holds
( b5 = f (#) F iff ( len b5 = len F & ( for i being Nat st i in dom b5 holds
b5 . i = (f . (F /. i)) * (F /. i) ) ) );
theorem Th8: :: VECTSP_6:8
for i being Element of NAT
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for F being FinSequence of V
for f being Function of V,GF st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
proof
let i be Element of NAT ; ::_thesis: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for F being FinSequence of V
for f being Function of V,GF st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for F being FinSequence of V
for f being Function of V,GF st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V
for F being FinSequence of V
for f being Function of V,GF st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let v be Element of V; ::_thesis: for F being FinSequence of V
for f being Function of V,GF st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let F be FinSequence of V; ::_thesis: for f being Function of V,GF st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v
let f be Function of V,GF; ::_thesis: ( i in dom F & v = F . i implies (f (#) F) . i = (f . v) * v )
assume that
A1: i in dom F and
A2: v = F . i ; ::_thesis: (f (#) F) . i = (f . v) * v
A3: F /. i = F . i by A1, PARTFUN1:def_6;
len (f (#) F) = len F by Def5;
then i in dom (f (#) F) by A1, FINSEQ_3:29;
hence (f (#) F) . i = (f . v) * v by A2, A3, Def5; ::_thesis: verum
end;
theorem :: VECTSP_6:9
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for f being Function of V,GF holds f (#) (<*> the carrier of V) = <*> the carrier of V
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for f being Function of V,GF holds f (#) (<*> the carrier of V) = <*> the carrier of V
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for f being Function of V,GF holds f (#) (<*> the carrier of V) = <*> the carrier of V
let f be Function of V,GF; ::_thesis: f (#) (<*> the carrier of V) = <*> the carrier of V
len (f (#) (<*> the carrier of V)) = len (<*> the carrier of V) by Def5
.= 0 ;
hence f (#) (<*> the carrier of V) = <*> the carrier of V ; ::_thesis: verum
end;
theorem Th10: :: VECTSP_6:10
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*>
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*>
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V
for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*>
let v be Element of V; ::_thesis: for f being Function of V,GF holds f (#) <*v*> = <*((f . v) * v)*>
let f be Function of V,GF; ::_thesis: f (#) <*v*> = <*((f . v) * v)*>
A1: 1 in {1} by TARSKI:def_1;
A2: len (f (#) <*v*>) = len <*v*> by Def5
.= 1 by FINSEQ_1:40 ;
then dom (f (#) <*v*>) = {1} by FINSEQ_1:2, FINSEQ_1:def_3;
then (f (#) <*v*>) . 1 = (f . (<*v*> /. 1)) * (<*v*> /. 1) by A1, Def5
.= (f . (<*v*> /. 1)) * v by FINSEQ_4:16
.= (f . v) * v by FINSEQ_4:16 ;
hence f (#) <*v*> = <*((f . v) * v)*> by A2, FINSEQ_1:40; ::_thesis: verum
end;
theorem Th11: :: VECTSP_6:11
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2 being Element of V
for f being Function of V,GF holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2 being Element of V
for f being Function of V,GF holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v1, v2 being Element of V
for f being Function of V,GF holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
let v1, v2 be Element of V; ::_thesis: for f being Function of V,GF holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
let f be Function of V,GF; ::_thesis: f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>
A1: len (f (#) <*v1,v2*>) = len <*v1,v2*> by Def5
.= 2 by FINSEQ_1:44 ;
then A2: dom (f (#) <*v1,v2*>) = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3;
2 in {1,2} by TARSKI:def_2;
then A3: (f (#) <*v1,v2*>) . 2 = (f . (<*v1,v2*> /. 2)) * (<*v1,v2*> /. 2) by A2, Def5
.= (f . (<*v1,v2*> /. 2)) * v2 by FINSEQ_4:17
.= (f . v2) * v2 by FINSEQ_4:17 ;
1 in {1,2} by TARSKI:def_2;
then (f (#) <*v1,v2*>) . 1 = (f . (<*v1,v2*> /. 1)) * (<*v1,v2*> /. 1) by A2, Def5
.= (f . (<*v1,v2*> /. 1)) * v1 by FINSEQ_4:17
.= (f . v1) * v1 by FINSEQ_4:17 ;
hence f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*> by A1, A3, FINSEQ_1:44; ::_thesis: verum
end;
theorem :: VECTSP_6:12
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2, v3 being Element of V
for f being Function of V,GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2, v3 being Element of V
for f being Function of V,GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v1, v2, v3 being Element of V
for f being Function of V,GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
let v1, v2, v3 be Element of V; ::_thesis: for f being Function of V,GF holds f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
let f be Function of V,GF; ::_thesis: f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*>
A1: len (f (#) <*v1,v2,v3*>) = len <*v1,v2,v3*> by Def5
.= 3 by FINSEQ_1:45 ;
then A2: dom (f (#) <*v1,v2,v3*>) = {1,2,3} by FINSEQ_1:def_3, FINSEQ_3:1;
3 in {1,2,3} by ENUMSET1:def_1;
then A3: (f (#) <*v1,v2,v3*>) . 3 = (f . (<*v1,v2,v3*> /. 3)) * (<*v1,v2,v3*> /. 3) by A2, Def5
.= (f . (<*v1,v2,v3*> /. 3)) * v3 by FINSEQ_4:18
.= (f . v3) * v3 by FINSEQ_4:18 ;
2 in {1,2,3} by ENUMSET1:def_1;
then A4: (f (#) <*v1,v2,v3*>) . 2 = (f . (<*v1,v2,v3*> /. 2)) * (<*v1,v2,v3*> /. 2) by A2, Def5
.= (f . (<*v1,v2,v3*> /. 2)) * v2 by FINSEQ_4:18
.= (f . v2) * v2 by FINSEQ_4:18 ;
1 in {1,2,3} by ENUMSET1:def_1;
then (f (#) <*v1,v2,v3*>) . 1 = (f . (<*v1,v2,v3*> /. 1)) * (<*v1,v2,v3*> /. 1) by A2, Def5
.= (f . (<*v1,v2,v3*> /. 1)) * v1 by FINSEQ_4:18
.= (f . v1) * v1 by FINSEQ_4:18 ;
hence f (#) <*v1,v2,v3*> = <*((f . v1) * v1),((f . v2) * v2),((f . v3) * v3)*> by A1, A4, A3, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th13: :: VECTSP_6:13
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for F, G being FinSequence of V
for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for F, G being FinSequence of V
for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for F, G being FinSequence of V
for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let F, G be FinSequence of V; ::_thesis: for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let f be Function of V,GF; ::_thesis: f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
set H = (f (#) F) ^ (f (#) G);
set I = F ^ G;
A1: len F = len (f (#) F) by Def5;
A2: len ((f (#) F) ^ (f (#) G)) = (len (f (#) F)) + (len (f (#) G)) by FINSEQ_1:22
.= (len F) + (len (f (#) G)) by Def5
.= (len F) + (len G) by Def5
.= len (F ^ G) by FINSEQ_1:22 ;
A3: len G = len (f (#) G) by Def5;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_((f_(#)_F)_^_(f_(#)_G))_holds_
((f_(#)_F)_^_(f_(#)_G))_._k_=_(f_._((F_^_G)_/._k))_*_((F_^_G)_/._k)
let k be Nat; ::_thesis: ( k in dom ((f (#) F) ^ (f (#) G)) implies ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) )
assume A4: k in dom ((f (#) F) ^ (f (#) G)) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)
now__::_thesis:_((f_(#)_F)_^_(f_(#)_G))_._k_=_(f_._((F_^_G)_/._k))_*_((F_^_G)_/._k)
percases ( k in dom (f (#) F) or ex n being Nat st
( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ) by A4, FINSEQ_1:25;
supposeA5: k in dom (f (#) F) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)
then A6: k in dom F by A1, FINSEQ_3:29;
then A7: k in dom (F ^ G) by FINSEQ_3:22;
A8: F /. k = F . k by A6, PARTFUN1:def_6
.= (F ^ G) . k by A6, FINSEQ_1:def_7
.= (F ^ G) /. k by A7, PARTFUN1:def_6 ;
thus ((f (#) F) ^ (f (#) G)) . k = (f (#) F) . k by A5, FINSEQ_1:def_7
.= (f . ((F ^ G) /. k)) * ((F ^ G) /. k) by A5, A8, Def5 ; ::_thesis: verum
end;
supposeA9: ex n being Nat st
( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)
A10: k in dom (F ^ G) by A2, A4, FINSEQ_3:29;
consider n being Nat such that
A11: n in dom (f (#) G) and
A12: k = (len (f (#) F)) + n by A9;
A13: n in dom G by A3, A11, FINSEQ_3:29;
then A14: G /. n = G . n by PARTFUN1:def_6
.= (F ^ G) . k by A1, A12, A13, FINSEQ_1:def_7
.= (F ^ G) /. k by A10, PARTFUN1:def_6 ;
thus ((f (#) F) ^ (f (#) G)) . k = (f (#) G) . n by A11, A12, FINSEQ_1:def_7
.= (f . ((F ^ G) /. k)) * ((F ^ G) /. k) by A11, A14, Def5 ; ::_thesis: verum
end;
end;
end;
hence ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) ; ::_thesis: verum
end;
hence f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by A2, Def5; ::_thesis: verum
end;
definition
let GF be non empty addLoopStr ;
let V be non empty VectSpStr over GF;
let L be Linear_Combination of V;
assume A1: ( V is Abelian & V is add-associative & V is right_zeroed & V is right_complementable ) ;
func Sum L -> Element of V means :Def6: :: VECTSP_6:def 6
ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & it = Sum (L (#) F) );
existence
ex b1 being Element of V ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) )
proof
consider F being FinSequence such that
A2: rng F = Carrier L and
A3: F is one-to-one by FINSEQ_4:58;
reconsider F = F as FinSequence of the carrier of V by A2, FINSEQ_1:def_4;
take Sum (L (#) F) ; ::_thesis: ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) )
take F ; ::_thesis: ( F is one-to-one & rng F = Carrier L & Sum (L (#) F) = Sum (L (#) F) )
thus ( F is one-to-one & rng F = Carrier L ) by A2, A3; ::_thesis: Sum (L (#) F) = Sum (L (#) F)
thus Sum (L (#) F) = Sum (L (#) F) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of V st ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & b1 = Sum (L (#) F) ) & ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & b2 = Sum (L (#) F) ) holds
b1 = b2
proof
let v1, v2 be Element of V; ::_thesis: ( ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & v1 = Sum (L (#) F) ) & ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & v2 = Sum (L (#) F) ) implies v1 = v2 )
given F1 being FinSequence of the carrier of V such that A4: F1 is one-to-one and
A5: rng F1 = Carrier L and
A6: v1 = Sum (L (#) F1) ; ::_thesis: ( for F being FinSequence of the carrier of V holds
( not F is one-to-one or not rng F = Carrier L or not v2 = Sum (L (#) F) ) or v1 = v2 )
given F2 being FinSequence of the carrier of V such that A7: F2 is one-to-one and
A8: rng F2 = Carrier L and
A9: v2 = Sum (L (#) F2) ; ::_thesis: v1 = v2
defpred S1[ set , set ] means {$2} = F1 " {(F2 . $1)};
A10: len F1 = len F2 by A4, A5, A7, A8, FINSEQ_1:48;
A11: dom F1 = Seg (len F1) by FINSEQ_1:def_3;
A12: dom F2 = Seg (len F2) by FINSEQ_1:def_3;
A13: for x being set st x in dom F1 holds
ex y being set st
( y in dom F1 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in dom F1 implies ex y being set st
( y in dom F1 & S1[x,y] ) )
assume x in dom F1 ; ::_thesis: ex y being set st
( y in dom F1 & S1[x,y] )
then F2 . x in rng F1 by A5, A8, A10, A11, A12, FUNCT_1:def_3;
then consider y being set such that
A14: F1 " {(F2 . x)} = {y} by A4, FUNCT_1:74;
take y ; ::_thesis: ( y in dom F1 & S1[x,y] )
y in F1 " {(F2 . x)} by A14, TARSKI:def_1;
hence y in dom F1 by FUNCT_1:def_7; ::_thesis: S1[x,y]
thus S1[x,y] by A14; ::_thesis: verum
end;
consider f being Function of (dom F1),(dom F1) such that
A15: for x being set st x in dom F1 holds
S1[x,f . x] from FUNCT_2:sch_1(A13);
A16: rng f = dom F1
proof
thus rng f c= dom F1 by RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: dom F1 c= rng f
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom F1 or y in rng f )
assume A17: y in dom F1 ; ::_thesis: y in rng f
then F1 . y in rng F2 by A5, A8, FUNCT_1:def_3;
then consider x being set such that
A18: x in dom F2 and
A19: F2 . x = F1 . y by FUNCT_1:def_3;
F1 " {(F2 . x)} = F1 " (Im (F1,y)) by A17, A19, FUNCT_1:59;
then F1 " {(F2 . x)} c= {y} by A4, FUNCT_1:82;
then {(f . x)} c= {y} by A10, A11, A12, A15, A18;
then A20: f . x = y by ZFMISC_1:18;
x in dom f by A10, A11, A12, A18, FUNCT_2:def_1;
hence y in rng f by A20, FUNCT_1:def_3; ::_thesis: verum
end;
set G1 = L (#) F1;
A21: len (L (#) F1) = len F1 by Def5;
A22: ( dom F1 = {} implies dom F1 = {} ) ;
A23: f is one-to-one
proof
let y1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not y1 in dom f or not b1 in dom f or not f . y1 = f . b1 or y1 = b1 )
let y2 be set ; ::_thesis: ( not y1 in dom f or not y2 in dom f or not f . y1 = f . y2 or y1 = y2 )
assume that
A24: y1 in dom f and
A25: y2 in dom f and
A26: f . y1 = f . y2 ; ::_thesis: y1 = y2
A27: y2 in dom F1 by A22, A25, FUNCT_2:def_1;
then A28: F1 " {(F2 . y2)} = {(f . y2)} by A15;
A29: y1 in dom F1 by A22, A24, FUNCT_2:def_1;
then F2 . y1 in rng F1 by A5, A8, A10, A11, A12, FUNCT_1:def_3;
then A30: {(F2 . y1)} c= rng F1 by ZFMISC_1:31;
F2 . y2 in rng F1 by A5, A8, A10, A11, A12, A27, FUNCT_1:def_3;
then A31: {(F2 . y2)} c= rng F1 by ZFMISC_1:31;
F1 " {(F2 . y1)} = {(f . y1)} by A15, A29;
then {(F2 . y1)} = {(F2 . y2)} by A26, A28, A30, A31, FUNCT_1:91;
then A32: F2 . y1 = F2 . y2 by ZFMISC_1:3;
( y1 in dom F2 & y2 in dom F2 ) by A10, A11, A12, A22, A24, A25, FUNCT_2:def_1;
hence y1 = y2 by A7, A32, FUNCT_1:def_4; ::_thesis: verum
end;
set G2 = L (#) F2;
A33: dom (L (#) F2) = Seg (len (L (#) F2)) by FINSEQ_1:def_3;
reconsider f = f as Permutation of (dom F1) by A16, A23, FUNCT_2:57;
( dom F1 = Seg (len F1) & dom (L (#) F1) = Seg (len (L (#) F1)) ) by FINSEQ_1:def_3;
then reconsider f = f as Permutation of (dom (L (#) F1)) by A21;
A34: len (L (#) F2) = len F2 by Def5;
A35: dom (L (#) F1) = Seg (len (L (#) F1)) by FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(L_(#)_F2)_holds_
(L_(#)_F2)_._i_=_(L_(#)_F1)_._(f_._i)
let i be Element of NAT ; ::_thesis: ( i in dom (L (#) F2) implies (L (#) F2) . i = (L (#) F1) . (f . i) )
assume A36: i in dom (L (#) F2) ; ::_thesis: (L (#) F2) . i = (L (#) F1) . (f . i)
then A37: ( (L (#) F2) . i = (L . (F2 /. i)) * (F2 /. i) & F2 . i = F2 /. i ) by A34, A12, A33, Def5, PARTFUN1:def_6;
i in dom F2 by A34, A36, FINSEQ_3:29;
then reconsider u = F2 . i as Element of V by FINSEQ_2:11;
i in dom f by A10, A21, A34, A35, A33, A36, FUNCT_2:def_1;
then A38: f . i in dom F1 by A16, FUNCT_1:def_3;
then reconsider m = f . i as Element of NAT by A11;
reconsider v = F1 . m as Element of V by A38, FINSEQ_2:11;
{(F1 . (f . i))} = Im (F1,(f . i)) by A38, FUNCT_1:59
.= F1 .: (F1 " {(F2 . i)}) by A10, A34, A11, A33, A15, A36 ;
then A39: u = v by FUNCT_1:75, ZFMISC_1:18;
F1 . m = F1 /. m by A38, PARTFUN1:def_6;
hence (L (#) F2) . i = (L (#) F1) . (f . i) by A21, A11, A35, A38, A39, A37, Def5; ::_thesis: verum
end;
hence v1 = v2 by A1, A4, A5, A6, A7, A8, A9, A21, A34, FINSEQ_1:48, RLVECT_2:6; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines Sum VECTSP_6:def_6_:_
for GF being non empty addLoopStr
for V being non empty VectSpStr over GF
for L being Linear_Combination of V st V is Abelian & V is add-associative & V is right_zeroed & V is right_complementable holds
for b4 being Element of V holds
( b4 = Sum L iff ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & b4 = Sum (L (#) F) ) );
Lm1: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds Sum (ZeroLC V) = 0. V
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds Sum (ZeroLC V) = 0. V
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: Sum (ZeroLC V) = 0. V
consider F being FinSequence of V such that
F is one-to-one and
A1: rng F = Carrier (ZeroLC V) and
A2: Sum (ZeroLC V) = Sum ((ZeroLC V) (#) F) by Def6;
Carrier (ZeroLC V) = {} by Def3;
then F = {} by A1, RELAT_1:41;
then len F = 0 ;
then len ((ZeroLC V) (#) F) = 0 by Def5;
hence Sum (ZeroLC V) = 0. V by A2, RLVECT_1:75; ::_thesis: verum
end;
theorem :: VECTSP_6:14
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V st 0. GF <> 1. GF holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V st 0. GF <> 1. GF holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for A being Subset of V st 0. GF <> 1. GF holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
let A be Subset of V; ::_thesis: ( 0. GF <> 1. GF implies ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) )
assume A1: 0. GF <> 1. GF ; ::_thesis: ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
thus ( A <> {} & A is linearly-closed implies for l being Linear_Combination of A holds Sum l in A ) ::_thesis: ( ( for l being Linear_Combination of A holds Sum l in A ) implies ( A <> {} & A is linearly-closed ) )
proof
defpred S1[ Element of NAT ] means for l being Linear_Combination of A st card (Carrier l) = $1 holds
Sum l in A;
assume that
A2: A <> {} and
A3: A is linearly-closed ; ::_thesis: for l being Linear_Combination of A holds Sum l in A
A4: S1[ 0 ]
proof
let l be Linear_Combination of A; ::_thesis: ( card (Carrier l) = 0 implies Sum l in A )
assume card (Carrier l) = 0 ; ::_thesis: Sum l in A
then Carrier l = {} ;
then l = ZeroLC V by Def3;
then Sum l = 0. V by Lm1;
hence Sum l in A by A2, A3, VECTSP_4:1; ::_thesis: verum
end;
A5: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; ::_thesis: S1[k + 1]
let l be Linear_Combination of A; ::_thesis: ( card (Carrier l) = k + 1 implies Sum l in A )
deffunc H1( Element of V) -> Element of the carrier of GF = l . $1;
consider F being FinSequence of V such that
A7: F is one-to-one and
A8: rng F = Carrier l and
A9: Sum l = Sum (l (#) F) by Def6;
reconsider G = F | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;
assume A10: card (Carrier l) = k + 1 ; ::_thesis: Sum l in A
then A11: len F = k + 1 by A7, A8, FINSEQ_4:62;
then A12: len (l (#) F) = k + 1 by Def5;
A13: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A14: k + 1 in dom F by A11, FINSEQ_1:def_3;
k + 1 in dom F by A11, A13, FINSEQ_1:def_3;
then reconsider v = F . (k + 1) as Element of V by FINSEQ_2:11;
consider f being Function of the carrier of V, the carrier of GF such that
A15: f . v = 0. GF and
A16: for u being Element of V st u <> v holds
f . u = H1(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
A17: v in Carrier l by A8, A14, FUNCT_1:def_3;
now__::_thesis:_for_u_being_Element_of_V_st_not_u_in_Carrier_l_holds_
f_._u_=_0._GF
let u be Element of V; ::_thesis: ( not u in Carrier l implies f . u = 0. GF )
assume A18: not u in Carrier l ; ::_thesis: f . u = 0. GF
hence f . u = l . u by A17, A16
.= 0. GF by A18 ;
::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def1;
A19: A \ {v} c= A by XBOOLE_1:36;
A20: Carrier l c= A by Def4;
then A21: (l . v) * v in A by A3, A17, VECTSP_4:def_1;
A22: Carrier f = (Carrier l) \ {v}
proof
thus Carrier f c= (Carrier l) \ {v} :: according to XBOOLE_0:def_10 ::_thesis: (Carrier l) \ {v} c= Carrier f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in (Carrier l) \ {v} )
assume x in Carrier f ; ::_thesis: x in (Carrier l) \ {v}
then consider u being Element of V such that
A23: u = x and
A24: f . u <> 0. GF ;
f . u = l . u by A15, A16, A24;
then A25: x in Carrier l by A23, A24;
not x in {v} by A15, A23, A24, TARSKI:def_1;
hence x in (Carrier l) \ {v} by A25, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Carrier l) \ {v} or x in Carrier f )
assume A26: x in (Carrier l) \ {v} ; ::_thesis: x in Carrier f
then x in Carrier l by XBOOLE_0:def_5;
then consider u being Element of V such that
A27: x = u and
A28: l . u <> 0. GF ;
not x in {v} by A26, XBOOLE_0:def_5;
then x <> v by TARSKI:def_1;
then l . u = f . u by A16, A27;
hence x in Carrier f by A27, A28; ::_thesis: verum
end;
then Carrier f c= A \ {v} by A20, XBOOLE_1:33;
then Carrier f c= A by A19, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by Def4;
A29: len G = k by A11, FINSEQ_3:53;
then A30: len (f (#) G) = k by Def5;
A31: rng G = Carrier f
proof
thus rng G c= Carrier f :: according to XBOOLE_0:def_10 ::_thesis: Carrier f c= rng G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in Carrier f )
assume x in rng G ; ::_thesis: x in Carrier f
then consider y being set such that
A32: y in dom G and
A33: G . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A32, FINSEQ_3:23;
A34: ( dom G c= dom F & G . y = F . y ) by A32, FUNCT_1:47, RELAT_1:60;
now__::_thesis:_not_x_=_v
assume x = v ; ::_thesis: contradiction
then A35: k + 1 = y by A7, A14, A32, A33, A34, FUNCT_1:def_4;
y <= k by A29, A32, FINSEQ_3:25;
hence contradiction by A35, XREAL_1:29; ::_thesis: verum
end;
then A36: not x in {v} by TARSKI:def_1;
x in rng F by A32, A33, A34, FUNCT_1:def_3;
hence x in Carrier f by A8, A22, A36, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in rng G )
assume A37: x in Carrier f ; ::_thesis: x in rng G
then x in rng F by A8, A22, XBOOLE_0:def_5;
then consider y being set such that
A38: y in dom F and
A39: F . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A38, FINSEQ_3:23;
now__::_thesis:_y_in_Seg_k
assume not y in Seg k ; ::_thesis: contradiction
then y in (dom F) \ (Seg k) by A38, XBOOLE_0:def_5;
then y in (Seg (k + 1)) \ (Seg k) by A11, FINSEQ_1:def_3;
then y in {(k + 1)} by FINSEQ_3:15;
then y = k + 1 by TARSKI:def_1;
then not v in {v} by A22, A37, A39, XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
then y in (dom F) /\ (Seg k) by A38, XBOOLE_0:def_4;
then A40: y in dom G by RELAT_1:61;
then G . y = F . y by FUNCT_1:47;
hence x in rng G by A39, A40, FUNCT_1:def_3; ::_thesis: verum
end;
(Seg (k + 1)) /\ (Seg k) = Seg k by FINSEQ_1:7, NAT_1:12
.= dom (f (#) G) by A30, FINSEQ_1:def_3 ;
then A41: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by A12, FINSEQ_1:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_(#)_G)_holds_
(f_(#)_G)_._x_=_(l_(#)_F)_._x
let x be set ; ::_thesis: ( x in dom (f (#) G) implies (f (#) G) . x = (l (#) F) . x )
A42: rng F c= the carrier of V by FINSEQ_1:def_4;
assume A43: x in dom (f (#) G) ; ::_thesis: (f (#) G) . x = (l (#) F) . x
then reconsider n = x as Element of NAT by FINSEQ_3:23;
n in dom (l (#) F) by A41, A43, XBOOLE_0:def_4;
then A44: n in dom F by A11, A12, FINSEQ_3:29;
then F . n in rng F by FUNCT_1:def_3;
then reconsider w = F . n as Element of V by A42;
A45: n in dom G by A29, A30, A43, FINSEQ_3:29;
then A46: G . n in rng G by FUNCT_1:def_3;
rng G c= the carrier of V by FINSEQ_1:def_4;
then reconsider u = G . n as Element of V by A46;
not u in {v} by A22, A31, A46, XBOOLE_0:def_5;
then A47: u <> v by TARSKI:def_1;
A48: (f (#) G) . n = (f . u) * u by A45, Th8
.= (l . u) * u by A16, A47 ;
w = u by A45, FUNCT_1:47;
hence (f (#) G) . x = (l (#) F) . x by A48, A44, Th8; ::_thesis: verum
end;
then f (#) G = (l (#) F) | (Seg k) by A41, FUNCT_1:46;
then A49: f (#) G = (l (#) F) | (dom (f (#) G)) by A30, FINSEQ_1:def_3;
v in rng F by A14, FUNCT_1:def_3;
then {v} c= Carrier l by A8, ZFMISC_1:31;
then card (Carrier f) = (k + 1) - (card {v}) by A10, A22, CARD_2:44
.= (k + 1) - 1 by CARD_1:30
.= k by XCMPLX_1:26 ;
then A50: Sum f in A by A6;
G is one-to-one by A7, FUNCT_1:52;
then A51: Sum (f (#) G) = Sum f by A31, Def6;
(l (#) F) . (len F) = (l . v) * v by A11, A14, Th8;
then Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v) by A11, A12, A30, A49, RLVECT_1:38;
hence Sum l in A by A3, A9, A21, A51, A50, VECTSP_4:def_1; ::_thesis: verum
end;
let l be Linear_Combination of A; ::_thesis: Sum l in A
A52: card (Carrier l) = card (Carrier l) ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A5);
hence Sum l in A by A52; ::_thesis: verum
end;
assume A53: for l being Linear_Combination of A holds Sum l in A ; ::_thesis: ( A <> {} & A is linearly-closed )
hence A <> {} ; ::_thesis: A is linearly-closed
( ZeroLC V is Linear_Combination of A & Sum (ZeroLC V) = 0. V ) by Lm1, Th5;
then A54: 0. V in A by A53;
A55: for a being Element of GF
for v being Element of V st v in A holds
a * v in A
proof
let a be Element of GF; ::_thesis: for v being Element of V st v in A holds
a * v in A
let v be Element of V; ::_thesis: ( v in A implies a * v in A )
assume A56: v in A ; ::_thesis: a * v in A
now__::_thesis:_a_*_v_in_A
percases ( a = 0. GF or a <> 0. GF ) ;
suppose a = 0. GF ; ::_thesis: a * v in A
hence a * v in A by A54, VECTSP_1:14; ::_thesis: verum
end;
supposeA57: a <> 0. GF ; ::_thesis: a * v in A
deffunc H1( set ) -> Element of the carrier of GF = 0. GF;
consider f being Function of V,GF such that
A58: f . v = a and
A59: for u being Element of V st u <> v holds
f . u = H1(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
now__::_thesis:_for_u_being_Element_of_V_st_not_u_in_{v}_holds_
f_._u_=_0._GF
let u be Element of V; ::_thesis: ( not u in {v} implies f . u = 0. GF )
assume not u in {v} ; ::_thesis: f . u = 0. GF
then u <> v by TARSKI:def_1;
hence f . u = 0. GF by A59; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def1;
A60: Carrier f = {v}
proof
thus Carrier f c= {v} :: according to XBOOLE_0:def_10 ::_thesis: {v} c= Carrier f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume x in Carrier f ; ::_thesis: x in {v}
then consider u being Element of V such that
A61: x = u and
A62: f . u <> 0. GF ;
u = v by A59, A62;
hence x in {v} by A61, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in Carrier f )
assume x in {v} ; ::_thesis: x in Carrier f
then x = v by TARSKI:def_1;
hence x in Carrier f by A57, A58; ::_thesis: verum
end;
{v} c= A by A56, ZFMISC_1:31;
then reconsider f = f as Linear_Combination of A by A60, Def4;
consider F being FinSequence of V such that
A63: ( F is one-to-one & rng F = Carrier f ) and
A64: Sum (f (#) F) = Sum f by Def6;
F = <*v*> by A60, A63, FINSEQ_3:97;
then f (#) F = <*((f . v) * v)*> by Th10;
then Sum f = a * v by A58, A64, RLVECT_1:44;
hence a * v in A by A53; ::_thesis: verum
end;
end;
end;
hence a * v in A ; ::_thesis: verum
end;
thus for v, u being Element of V st v in A & u in A holds
v + u in A :: according to VECTSP_4:def_1 ::_thesis: for b1 being Element of the carrier of GF
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A )
proof
let v, u be Element of V; ::_thesis: ( v in A & u in A implies v + u in A )
assume that
A65: v in A and
A66: u in A ; ::_thesis: v + u in A
now__::_thesis:_v_+_u_in_A
percases ( u = v or v <> u ) ;
suppose u = v ; ::_thesis: v + u in A
then v + u = ((1. GF) * v) + v by VECTSP_1:def_17
.= ((1. GF) * v) + ((1. GF) * v) by VECTSP_1:def_17
.= ((1. GF) + (1. GF)) * v by VECTSP_1:def_15 ;
hence v + u in A by A55, A65; ::_thesis: verum
end;
supposeA67: v <> u ; ::_thesis: v + u in A
deffunc H1( set ) -> Element of the carrier of GF = 0. GF;
consider f being Function of V,GF such that
A68: ( f . v = 1. GF & f . u = 1. GF ) and
A69: for w being Element of V st w <> v & w <> u holds
f . w = H1(w) from FUNCT_2:sch_7(A67);
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
now__::_thesis:_for_w_being_Element_of_V_st_not_w_in_{v,u}_holds_
f_._w_=_0._GF
let w be Element of V; ::_thesis: ( not w in {v,u} implies f . w = 0. GF )
assume not w in {v,u} ; ::_thesis: f . w = 0. GF
then ( w <> v & w <> u ) by TARSKI:def_2;
hence f . w = 0. GF by A69; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def1;
A70: Carrier f = {v,u}
proof
thus Carrier f c= {v,u} :: according to XBOOLE_0:def_10 ::_thesis: {v,u} c= Carrier f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v,u} )
assume x in Carrier f ; ::_thesis: x in {v,u}
then ex w being Element of V st
( x = w & f . w <> 0. GF ) ;
then ( x = v or x = u ) by A69;
hence x in {v,u} by TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v,u} or x in Carrier f )
assume x in {v,u} ; ::_thesis: x in Carrier f
then ( x = v or x = u ) by TARSKI:def_2;
hence x in Carrier f by A1, A68; ::_thesis: verum
end;
then A71: Carrier f c= A by A65, A66, ZFMISC_1:32;
A72: ( (1. GF) * u = u & (1. GF) * v = v ) by VECTSP_1:def_17;
reconsider f = f as Linear_Combination of A by A71, Def4;
consider F being FinSequence of V such that
A73: ( F is one-to-one & rng F = Carrier f ) and
A74: Sum (f (#) F) = Sum f by Def6;
( F = <*v,u*> or F = <*u,v*> ) by A67, A70, A73, FINSEQ_3:99;
then ( f (#) F = <*((1. GF) * v),((1. GF) * u)*> or f (#) F = <*((1. GF) * u),((1. GF) * v)*> ) by A68, Th11;
then Sum f = v + u by A74, A72, RLVECT_1:45;
hence v + u in A by A53; ::_thesis: verum
end;
end;
end;
hence v + u in A ; ::_thesis: verum
end;
thus for b1 being Element of the carrier of GF
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A ) by A55; ::_thesis: verum
end;
theorem :: VECTSP_6:15
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds Sum (ZeroLC V) = 0. V by Lm1;
theorem :: VECTSP_6:16
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V
let l be Linear_Combination of {} the carrier of V; ::_thesis: Sum l = 0. V
l = ZeroLC V by Th6;
hence Sum l = 0. V by Lm1; ::_thesis: verum
end;
theorem Th17: :: VECTSP_6:17
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for l being Linear_Combination of {v} holds Sum l = (l . v) * v
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for l being Linear_Combination of {v} holds Sum l = (l . v) * v
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V
for l being Linear_Combination of {v} holds Sum l = (l . v) * v
let v be Element of V; ::_thesis: for l being Linear_Combination of {v} holds Sum l = (l . v) * v
let l be Linear_Combination of {v}; ::_thesis: Sum l = (l . v) * v
A1: Carrier l c= {v} by Def4;
now__::_thesis:_Sum_l_=_(l_._v)_*_v
percases ( Carrier l = {} or Carrier l = {v} ) by A1, ZFMISC_1:33;
suppose Carrier l = {} ; ::_thesis: Sum l = (l . v) * v
then A2: l = ZeroLC V by Def3;
hence Sum l = 0. V by Lm1
.= (0. GF) * v by VECTSP_1:14
.= (l . v) * v by A2, Th3 ;
::_thesis: verum
end;
suppose Carrier l = {v} ; ::_thesis: Sum l = (l . v) * v
then consider F being FinSequence of V such that
A3: ( F is one-to-one & rng F = {v} ) and
A4: Sum l = Sum (l (#) F) by Def6;
F = <*v*> by A3, FINSEQ_3:97;
then l (#) F = <*((l . v) * v)*> by Th10;
hence Sum l = (l . v) * v by A4, RLVECT_1:44; ::_thesis: verum
end;
end;
end;
hence Sum l = (l . v) * v ; ::_thesis: verum
end;
theorem Th18: :: VECTSP_6:18
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2 being Element of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2 being Element of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v1, v2 being Element of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
let v1, v2 be Element of V; ::_thesis: ( v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) )
assume A1: v1 <> v2 ; ::_thesis: for l being Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
let l be Linear_Combination of {v1,v2}; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
A2: Carrier l c= {v1,v2} by Def4;
now__::_thesis:_Sum_l_=_((l_._v1)_*_v1)_+_((l_._v2)_*_v2)
percases ( Carrier l = {} or Carrier l = {v1} or Carrier l = {v2} or Carrier l = {v1,v2} ) by A2, ZFMISC_1:36;
suppose Carrier l = {} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
then A3: l = ZeroLC V by Def3;
hence Sum l = 0. V by Lm1
.= (0. V) + (0. V) by RLVECT_1:4
.= ((0. GF) * v1) + (0. V) by VECTSP_1:14
.= ((0. GF) * v1) + ((0. GF) * v2) by VECTSP_1:14
.= ((l . v1) * v1) + ((0. GF) * v2) by A3, Th3
.= ((l . v1) * v1) + ((l . v2) * v2) by A3, Th3 ;
::_thesis: verum
end;
supposeA4: Carrier l = {v1} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
then reconsider L = l as Linear_Combination of {v1} by Def4;
A5: not v2 in Carrier l by A1, A4, TARSKI:def_1;
thus Sum l = Sum L
.= (l . v1) * v1 by Th17
.= ((l . v1) * v1) + (0. V) by RLVECT_1:4
.= ((l . v1) * v1) + ((0. GF) * v2) by VECTSP_1:14
.= ((l . v1) * v1) + ((l . v2) * v2) by A5 ; ::_thesis: verum
end;
supposeA6: Carrier l = {v2} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
then reconsider L = l as Linear_Combination of {v2} by Def4;
A7: not v1 in Carrier l by A1, A6, TARSKI:def_1;
thus Sum l = Sum L
.= (l . v2) * v2 by Th17
.= (0. V) + ((l . v2) * v2) by RLVECT_1:4
.= ((0. GF) * v1) + ((l . v2) * v2) by VECTSP_1:14
.= ((l . v1) * v1) + ((l . v2) * v2) by A7 ; ::_thesis: verum
end;
suppose Carrier l = {v1,v2} ; ::_thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
then consider F being FinSequence of V such that
A8: ( F is one-to-one & rng F = {v1,v2} ) and
A9: Sum l = Sum (l (#) F) by Def6;
( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A8, FINSEQ_3:99;
then ( l (#) F = <*((l . v1) * v1),((l . v2) * v2)*> or l (#) F = <*((l . v2) * v2),((l . v1) * v1)*> ) by Th11;
hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) by A9, RLVECT_1:45; ::_thesis: verum
end;
end;
end;
hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) ; ::_thesis: verum
end;
theorem :: VECTSP_6:19
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L being Linear_Combination of V st Carrier L = {} holds
Sum L = 0. V
let L be Linear_Combination of V; ::_thesis: ( Carrier L = {} implies Sum L = 0. V )
assume Carrier L = {} ; ::_thesis: Sum L = 0. V
then L = ZeroLC V by Def3;
hence Sum L = 0. V by Lm1; ::_thesis: verum
end;
theorem :: VECTSP_6:20
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V
for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v
let v be Element of V; ::_thesis: for L being Linear_Combination of V st Carrier L = {v} holds
Sum L = (L . v) * v
let L be Linear_Combination of V; ::_thesis: ( Carrier L = {v} implies Sum L = (L . v) * v )
assume Carrier L = {v} ; ::_thesis: Sum L = (L . v) * v
then L is Linear_Combination of {v} by Def4;
hence Sum L = (L . v) * v by Th17; ::_thesis: verum
end;
theorem :: VECTSP_6:21
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2 being Element of V
for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = ((L . v1) * v1) + ((L . v2) * v2)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v1, v2 being Element of V
for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = ((L . v1) * v1) + ((L . v2) * v2)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v1, v2 being Element of V
for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = ((L . v1) * v1) + ((L . v2) * v2)
let v1, v2 be Element of V; ::_thesis: for L being Linear_Combination of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = ((L . v1) * v1) + ((L . v2) * v2)
let L be Linear_Combination of V; ::_thesis: ( Carrier L = {v1,v2} & v1 <> v2 implies Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
assume that
A1: Carrier L = {v1,v2} and
A2: v1 <> v2 ; ::_thesis: Sum L = ((L . v1) * v1) + ((L . v2) * v2)
L is Linear_Combination of {v1,v2} by A1, Def4;
hence Sum L = ((L . v1) * v1) + ((L . v2) * v2) by A2, Th18; ::_thesis: verum
end;
definition
let GF be non empty ZeroStr ;
let V be non empty VectSpStr over GF;
let L1, L2 be Linear_Combination of V;
:: original: =
redefine predL1 = L2 means :: VECTSP_6:def 7
for v being Element of V holds L1 . v = L2 . v;
compatibility
( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v ) by FUNCT_2:63;
end;
:: deftheorem defines = VECTSP_6:def_7_:_
for GF being non empty ZeroStr
for V being non empty VectSpStr over GF
for L1, L2 being Linear_Combination of V holds
( L1 = L2 iff for v being Element of V holds L1 . v = L2 . v );
definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let L1, L2 be Linear_Combination of V;
funcL1 + L2 -> Linear_Combination of V equals :: VECTSP_6:def 8
L1 + L2;
coherence
L1 + L2 is Linear_Combination of V
proof
set f = L1 + L2;
A1: ( dom L1 = the carrier of V & dom L2 = the carrier of V ) by FUNCT_2:def_1;
A2: dom (L1 + L2) = (dom L1) /\ (dom L2) by VFUNCT_1:def_1;
then L1 + L2 is Function of V,GF by A1, FUNCT_2:67;
then A3: L1 + L2 is Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
now__::_thesis:_for_v_being_Element_of_V_st_not_v_in_(Carrier_L1)_\/_(Carrier_L2)_holds_
(L1_+_L2)_._v_=_0._GF
let v be Element of V; ::_thesis: ( not v in (Carrier L1) \/ (Carrier L2) implies (L1 + L2) . v = 0. GF )
assume A4: not v in (Carrier L1) \/ (Carrier L2) ; ::_thesis: (L1 + L2) . v = 0. GF
then not v in Carrier L2 by XBOOLE_0:def_3;
then A5: L2 . v = 0. GF ;
A6: ( L1 /. v = L1 . v & L2 /. v = L2 . v ) by A1, PARTFUN1:def_6;
not v in Carrier L1 by A4, XBOOLE_0:def_3;
then A7: L1 . v = 0. GF ;
thus (L1 + L2) . v = (L1 + L2) /. v by A1, A2, PARTFUN1:def_6
.= (0. GF) + (0. GF) by A1, A2, A5, A6, A7, VFUNCT_1:def_1
.= 0. GF by RLVECT_1:4 ; ::_thesis: verum
end;
hence L1 + L2 is Linear_Combination of V by A3, Def1; ::_thesis: verum
end;
end;
:: deftheorem defines + VECTSP_6:def_8_:_
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds L1 + L2 = L1 + L2;
theorem Th22: :: VECTSP_6:22
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L1, L2 being Linear_Combination of V holds (L1 + L2) . v = (L1 . v) + (L2 . v)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L1, L2 being Linear_Combination of V holds (L1 + L2) . v = (L1 . v) + (L2 . v)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V
for L1, L2 being Linear_Combination of V holds (L1 + L2) . v = (L1 . v) + (L2 . v)
let v be Element of V; ::_thesis: for L1, L2 being Linear_Combination of V holds (L1 + L2) . v = (L1 . v) + (L2 . v)
let L1, L2 be Linear_Combination of V; ::_thesis: (L1 + L2) . v = (L1 . v) + (L2 . v)
( dom L1 = the carrier of V & dom L2 = the carrier of V ) by FUNCT_2:def_1;
then A1: ( L1 /. v = L1 . v & L2 /. v = L2 . v ) by PARTFUN1:def_6;
A2: dom (L1 + L2) = the carrier of V by FUNCT_2:def_1;
hence (L1 + L2) . v = (L1 + L2) /. v by PARTFUN1:def_6
.= (L1 . v) + (L2 . v) by A1, A2, VFUNCT_1:def_1 ;
::_thesis: verum
end;
theorem Th23: :: VECTSP_6:23
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L1, L2 being Linear_Combination of V holds Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
let L1, L2 be Linear_Combination of V; ::_thesis: Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier (L1 + L2) or x in (Carrier L1) \/ (Carrier L2) )
assume x in Carrier (L1 + L2) ; ::_thesis: x in (Carrier L1) \/ (Carrier L2)
then consider u being Element of V such that
A1: x = u and
A2: (L1 + L2) . u <> 0. GF ;
(L1 + L2) . u = (L1 . u) + (L2 . u) by Th22;
then ( L1 . u <> 0. GF or L2 . u <> 0. GF ) by A2, RLVECT_1:4;
then ( x in { v1 where v1 is Element of V : L1 . v1 <> 0. GF } or x in { v2 where v2 is Element of V : L2 . v2 <> 0. GF } ) by A1;
hence x in (Carrier L1) \/ (Carrier L2) by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th24: :: VECTSP_6:24
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A
let A be Subset of V; ::_thesis: for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 + L2 is Linear_Combination of A
let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 is Linear_Combination of A & L2 is Linear_Combination of A implies L1 + L2 is Linear_Combination of A )
assume ( L1 is Linear_Combination of A & L2 is Linear_Combination of A ) ; ::_thesis: L1 + L2 is Linear_Combination of A
then ( Carrier L1 c= A & Carrier L2 c= A ) by Def4;
then A1: (Carrier L1) \/ (Carrier L2) c= A by XBOOLE_1:8;
Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) by Th23;
hence Carrier (L1 + L2) c= A by A1, XBOOLE_1:1; :: according to VECTSP_6:def_4 ::_thesis: verum
end;
theorem Th25: :: VECTSP_6:25
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L1, L2 being Linear_Combination of V holds L1 + L2 = L2 + L1
let L1, L2 be Linear_Combination of V; ::_thesis: L1 + L2 = L2 + L1
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: (L1 + L2) . v = (L2 + L1) . v
thus (L1 + L2) . v = (L2 . v) + (L1 . v) by Th22
.= (L2 + L1) . v by Th22 ; ::_thesis: verum
end;
theorem :: VECTSP_6:26
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L1, L2, L3 being Linear_Combination of V holds L1 + (L2 + L3) = (L1 + L2) + L3
let L1, L2, L3 be Linear_Combination of V; ::_thesis: L1 + (L2 + L3) = (L1 + L2) + L3
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: (L1 + (L2 + L3)) . v = ((L1 + L2) + L3) . v
thus (L1 + (L2 + L3)) . v = (L1 . v) + ((L2 + L3) . v) by Th22
.= (L1 . v) + ((L2 . v) + (L3 . v)) by Th22
.= ((L1 . v) + (L2 . v)) + (L3 . v) by RLVECT_1:def_3
.= ((L1 + L2) . v) + (L3 . v) by Th22
.= ((L1 + L2) + L3) . v by Th22 ; ::_thesis: verum
end;
theorem :: VECTSP_6:27
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds
( L + (ZeroLC V) = L & (ZeroLC V) + L = L )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds
( L + (ZeroLC V) = L & (ZeroLC V) + L = L )
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L being Linear_Combination of V holds
( L + (ZeroLC V) = L & (ZeroLC V) + L = L )
let L be Linear_Combination of V; ::_thesis: ( L + (ZeroLC V) = L & (ZeroLC V) + L = L )
thus L + (ZeroLC V) = L ::_thesis: (ZeroLC V) + L = L
proof
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: (L + (ZeroLC V)) . v = L . v
thus (L + (ZeroLC V)) . v = (L . v) + ((ZeroLC V) . v) by Th22
.= (L . v) + (0. GF) by Th3
.= L . v by RLVECT_1:4 ; ::_thesis: verum
end;
hence (ZeroLC V) + L = L by Th25; ::_thesis: verum
end;
definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let a be Element of GF;
let L be Linear_Combination of V;
funca * L -> Linear_Combination of V means :Def9: :: VECTSP_6:def 9
for v being Element of V holds it . v = a * (L . v);
existence
ex b1 being Linear_Combination of V st
for v being Element of V holds b1 . v = a * (L . v)
proof
deffunc H1( Element of V) -> Element of the carrier of GF = a * (L . $1);
consider f being Function of the carrier of V, the carrier of GF such that
A1: for v being Element of V holds f . v = H1(v) from FUNCT_2:sch_4();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
now__::_thesis:_for_v_being_Element_of_V_st_not_v_in_Carrier_L_holds_
f_._v_=_0._GF
let v be Element of V; ::_thesis: ( not v in Carrier L implies f . v = 0. GF )
assume not v in Carrier L ; ::_thesis: f . v = 0. GF
then L . v = 0. GF ;
hence f . v = a * (0. GF) by A1
.= 0. GF by VECTSP_1:6 ;
::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def1;
take f ; ::_thesis: for v being Element of V holds f . v = a * (L . v)
let v be Element of V; ::_thesis: f . v = a * (L . v)
thus f . v = a * (L . v) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Linear_Combination of V st ( for v being Element of V holds b1 . v = a * (L . v) ) & ( for v being Element of V holds b2 . v = a * (L . v) ) holds
b1 = b2
proof
let L1, L2 be Linear_Combination of V; ::_thesis: ( ( for v being Element of V holds L1 . v = a * (L . v) ) & ( for v being Element of V holds L2 . v = a * (L . v) ) implies L1 = L2 )
assume A2: for v being Element of V holds L1 . v = a * (L . v) ; ::_thesis: ( ex v being Element of V st not L2 . v = a * (L . v) or L1 = L2 )
assume A3: for v being Element of V holds L2 . v = a * (L . v) ; ::_thesis: L1 = L2
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: L1 . v = L2 . v
thus L1 . v = a * (L . v) by A2
.= L2 . v by A3 ; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines * VECTSP_6:def_9_:_
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for L, b5 being Linear_Combination of V holds
( b5 = a * L iff for v being Element of V holds b5 . v = a * (L . v) );
theorem Th28: :: VECTSP_6:28
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for a being Element of GF
for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L
let a be Element of GF; ::_thesis: for L being Linear_Combination of V holds Carrier (a * L) c= Carrier L
let L be Linear_Combination of V; ::_thesis: Carrier (a * L) c= Carrier L
set T = { u where u is Element of V : (a * L) . u <> 0. GF } ;
set S = { v where v is Element of V : L . v <> 0. GF } ;
{ u where u is Element of V : (a * L) . u <> 0. GF } c= { v where v is Element of V : L . v <> 0. GF }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Element of V : (a * L) . u <> 0. GF } or x in { v where v is Element of V : L . v <> 0. GF } )
assume x in { u where u is Element of V : (a * L) . u <> 0. GF } ; ::_thesis: x in { v where v is Element of V : L . v <> 0. GF }
then consider u being Element of V such that
A1: x = u and
A2: (a * L) . u <> 0. GF ;
(a * L) . u = a * (L . u) by Def9;
then L . u <> 0. GF by A2, VECTSP_1:6;
hence x in { v where v is Element of V : L . v <> 0. GF } by A1; ::_thesis: verum
end;
hence Carrier (a * L) c= Carrier L ; ::_thesis: verum
end;
theorem Th29: :: VECTSP_6:29
for GF being Field
for V being VectSp of GF
for a being Element of GF
for L being Linear_Combination of V st a <> 0. GF holds
Carrier (a * L) = Carrier L
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for a being Element of GF
for L being Linear_Combination of V st a <> 0. GF holds
Carrier (a * L) = Carrier L
let V be VectSp of GF; ::_thesis: for a being Element of GF
for L being Linear_Combination of V st a <> 0. GF holds
Carrier (a * L) = Carrier L
let a be Element of GF; ::_thesis: for L being Linear_Combination of V st a <> 0. GF holds
Carrier (a * L) = Carrier L
let L be Linear_Combination of V; ::_thesis: ( a <> 0. GF implies Carrier (a * L) = Carrier L )
set T = { u where u is Vector of V : (a * L) . u <> 0. GF } ;
set S = { v where v is Vector of V : L . v <> 0. GF } ;
assume A1: a <> 0. GF ; ::_thesis: Carrier (a * L) = Carrier L
{ u where u is Vector of V : (a * L) . u <> 0. GF } = { v where v is Vector of V : L . v <> 0. GF }
proof
thus { u where u is Vector of V : (a * L) . u <> 0. GF } c= { v where v is Vector of V : L . v <> 0. GF } :: according to XBOOLE_0:def_10 ::_thesis: { v where v is Vector of V : L . v <> 0. GF } c= { u where u is Vector of V : (a * L) . u <> 0. GF }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Vector of V : (a * L) . u <> 0. GF } or x in { v where v is Vector of V : L . v <> 0. GF } )
assume x in { u where u is Vector of V : (a * L) . u <> 0. GF } ; ::_thesis: x in { v where v is Vector of V : L . v <> 0. GF }
then consider u being Vector of V such that
A2: x = u and
A3: (a * L) . u <> 0. GF ;
(a * L) . u = a * (L . u) by Def9;
then L . u <> 0. GF by A3, VECTSP_1:7;
hence x in { v where v is Vector of V : L . v <> 0. GF } by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Vector of V : L . v <> 0. GF } or x in { u where u is Vector of V : (a * L) . u <> 0. GF } )
assume x in { v where v is Vector of V : L . v <> 0. GF } ; ::_thesis: x in { u where u is Vector of V : (a * L) . u <> 0. GF }
then consider v being Vector of V such that
A4: x = v and
A5: L . v <> 0. GF ;
(a * L) . v = a * (L . v) by Def9;
then (a * L) . v <> 0. GF by A1, A5, VECTSP_1:12;
hence x in { u where u is Vector of V : (a * L) . u <> 0. GF } by A4; ::_thesis: verum
end;
hence Carrier (a * L) = Carrier L ; ::_thesis: verum
end;
theorem Th30: :: VECTSP_6:30
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds (0. GF) * L = ZeroLC V
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds (0. GF) * L = ZeroLC V
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L being Linear_Combination of V holds (0. GF) * L = ZeroLC V
let L be Linear_Combination of V; ::_thesis: (0. GF) * L = ZeroLC V
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: ((0. GF) * L) . v = (ZeroLC V) . v
thus ((0. GF) * L) . v = (0. GF) * (L . v) by Def9
.= 0. GF by VECTSP_1:7
.= (ZeroLC V) . v by Th3 ; ::_thesis: verum
end;
theorem Th31: :: VECTSP_6:31
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for a being Element of GF
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
let a be Element of GF; ::_thesis: for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
let A be Subset of V; ::_thesis: for L being Linear_Combination of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A
let L be Linear_Combination of V; ::_thesis: ( L is Linear_Combination of A implies a * L is Linear_Combination of A )
assume L is Linear_Combination of A ; ::_thesis: a * L is Linear_Combination of A
then A1: Carrier L c= A by Def4;
Carrier (a * L) c= Carrier L by Th28;
then Carrier (a * L) c= A by A1, XBOOLE_1:1;
hence a * L is Linear_Combination of A by Def4; ::_thesis: verum
end;
theorem :: VECTSP_6:32
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a, b being Element of GF
for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a, b being Element of GF
for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for a, b being Element of GF
for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)
let a, b be Element of GF; ::_thesis: for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)
let L be Linear_Combination of V; ::_thesis: (a + b) * L = (a * L) + (b * L)
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: ((a + b) * L) . v = ((a * L) + (b * L)) . v
thus ((a + b) * L) . v = (a + b) * (L . v) by Def9
.= (a * (L . v)) + (b * (L . v)) by VECTSP_1:def_7
.= ((a * L) . v) + (b * (L . v)) by Def9
.= ((a * L) . v) + ((b * L) . v) by Def9
.= ((a * L) + (b * L)) . v by Th22 ; ::_thesis: verum
end;
theorem :: VECTSP_6:33
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a being Element of GF
for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for a being Element of GF
for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)
let a be Element of GF; ::_thesis: for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)
let L1, L2 be Linear_Combination of V; ::_thesis: a * (L1 + L2) = (a * L1) + (a * L2)
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: (a * (L1 + L2)) . v = ((a * L1) + (a * L2)) . v
thus (a * (L1 + L2)) . v = a * ((L1 + L2) . v) by Def9
.= a * ((L1 . v) + (L2 . v)) by Th22
.= (a * (L1 . v)) + (a * (L2 . v)) by VECTSP_1:def_7
.= ((a * L1) . v) + (a * (L2 . v)) by Def9
.= ((a * L1) . v) + ((a * L2) . v) by Def9
.= ((a * L1) + (a * L2)) . v by Th22 ; ::_thesis: verum
end;
theorem Th34: :: VECTSP_6:34
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a, b being Element of GF
for L being Linear_Combination of V holds a * (b * L) = (a * b) * L
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for a, b being Element of GF
for L being Linear_Combination of V holds a * (b * L) = (a * b) * L
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for a, b being Element of GF
for L being Linear_Combination of V holds a * (b * L) = (a * b) * L
let a, b be Element of GF; ::_thesis: for L being Linear_Combination of V holds a * (b * L) = (a * b) * L
let L be Linear_Combination of V; ::_thesis: a * (b * L) = (a * b) * L
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: (a * (b * L)) . v = ((a * b) * L) . v
thus (a * (b * L)) . v = a * ((b * L) . v) by Def9
.= a * (b * (L . v)) by Def9
.= (a * b) * (L . v) by GROUP_1:def_3
.= ((a * b) * L) . v by Def9 ; ::_thesis: verum
end;
theorem :: VECTSP_6:35
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds (1. GF) * L = L
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds (1. GF) * L = L
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L being Linear_Combination of V holds (1. GF) * L = L
let L be Linear_Combination of V; ::_thesis: (1. GF) * L = L
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: ((1. GF) * L) . v = L . v
thus ((1. GF) * L) . v = (1. GF) * (L . v) by Def9
.= L . v by VECTSP_1:def_8 ; ::_thesis: verum
end;
definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let L be Linear_Combination of V;
func - L -> Linear_Combination of V equals :: VECTSP_6:def 10
(- (1. GF)) * L;
correctness
coherence
(- (1. GF)) * L is Linear_Combination of V;
;
involutiveness
for b1, b2 being Linear_Combination of V st b1 = (- (1. GF)) * b2 holds
b2 = (- (1. GF)) * b1
proof
let L, L9 be Linear_Combination of V; ::_thesis: ( L = (- (1. GF)) * L9 implies L9 = (- (1. GF)) * L )
assume A1: L = (- (1. GF)) * L9 ; ::_thesis: L9 = (- (1. GF)) * L
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: L9 . v = ((- (1. GF)) * L) . v
thus L9 . v = (1. GF) * (L9 . v) by VECTSP_1:def_8
.= ((1. GF) * (1. GF)) * (L9 . v) by VECTSP_1:def_8
.= ((- (1. GF)) * (- (1. GF))) * (L9 . v) by VECTSP_1:10
.= (((- (1. GF)) * (- (1. GF))) * L9) . v by Def9
.= ((- (1. GF)) * L) . v by A1, Th34 ; ::_thesis: verum
end;
end;
:: deftheorem defines - VECTSP_6:def_10_:_
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds - L = (- (1. GF)) * L;
Lm2: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of GF holds (- (1. GF)) * a = - a
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of GF holds (- (1. GF)) * a = - a
let a be Element of GF; ::_thesis: (- (1. GF)) * a = - a
thus (- (1. GF)) * a = ((0. GF) - (1. GF)) * a by RLVECT_1:14
.= ((0. GF) * a) - ((1. GF) * a) by VECTSP_1:13
.= (0. GF) - ((1. GF) * a) by VECTSP_1:7
.= - ((1. GF) * a) by RLVECT_1:14
.= - a by VECTSP_1:def_8 ; ::_thesis: verum
end;
theorem Th36: :: VECTSP_6:36
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V
for L being Linear_Combination of V holds (- L) . v = - (L . v)
let v be Element of V; ::_thesis: for L being Linear_Combination of V holds (- L) . v = - (L . v)
let L be Linear_Combination of V; ::_thesis: (- L) . v = - (L . v)
thus (- L) . v = (- (1. GF)) * (L . v) by Def9
.= - (L . v) by Lm2 ; ::_thesis: verum
end;
theorem :: VECTSP_6:37
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L1, L2 being Linear_Combination of V st L1 + L2 = ZeroLC V holds
L2 = - L1
let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 + L2 = ZeroLC V implies L2 = - L1 )
assume A1: L1 + L2 = ZeroLC V ; ::_thesis: L2 = - L1
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: L2 . v = (- L1) . v
(L1 . v) + (L2 . v) = (ZeroLC V) . v by A1, Th22
.= 0. GF by Th3 ;
hence L2 . v = - (L1 . v) by RLVECT_1:6
.= (- L1) . v by Th36 ;
::_thesis: verum
end;
Lm3: for GF being Field holds - (1. GF) <> 0. GF
proof
let GF be Field; ::_thesis: - (1. GF) <> 0. GF
assume not - (1. GF) <> 0. GF ; ::_thesis: contradiction
then 1. GF = - (0. GF) by RLVECT_1:17;
hence contradiction by RLVECT_1:12; ::_thesis: verum
end;
theorem Th38: :: VECTSP_6:38
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds Carrier (- L) = Carrier L
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds Carrier (- L) = Carrier L
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L being Linear_Combination of V holds Carrier (- L) = Carrier L
let L be Linear_Combination of V; ::_thesis: Carrier (- L) = Carrier L
( Carrier (- L) c= Carrier L & Carrier (- (- L)) c= Carrier (- L) ) by Th28;
hence Carrier (- L) = Carrier L by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: VECTSP_6:39
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V
for L being Linear_Combination of V st L is Linear_Combination of A holds
- L is Linear_Combination of A by Th31;
definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let L1, L2 be Linear_Combination of V;
funcL1 - L2 -> Linear_Combination of V equals :: VECTSP_6:def 11
L1 + (- L2);
coherence
L1 + (- L2) is Linear_Combination of V ;
end;
:: deftheorem defines - VECTSP_6:def_11_:_
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds L1 - L2 = L1 + (- L2);
theorem Th40: :: VECTSP_6:40
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for v being Element of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
let v be Element of V; ::_thesis: for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v)
let L1, L2 be Linear_Combination of V; ::_thesis: (L1 - L2) . v = (L1 . v) - (L2 . v)
thus (L1 - L2) . v = (L1 . v) + ((- L2) . v) by Th22
.= (L1 . v) + (- (L2 . v)) by Th36
.= (L1 . v) - (L2 . v) by RLVECT_1:def_11 ; ::_thesis: verum
end;
theorem :: VECTSP_6:41
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L1, L2 being Linear_Combination of V holds Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
let L1, L2 be Linear_Combination of V; ::_thesis: Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2)
Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier (- L2)) by Th23;
hence Carrier (L1 - L2) c= (Carrier L1) \/ (Carrier L2) by Th38; ::_thesis: verum
end;
theorem :: VECTSP_6:42
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for A being Subset of V
for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A
let A be Subset of V; ::_thesis: for L1, L2 being Linear_Combination of V st L1 is Linear_Combination of A & L2 is Linear_Combination of A holds
L1 - L2 is Linear_Combination of A
let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 is Linear_Combination of A & L2 is Linear_Combination of A implies L1 - L2 is Linear_Combination of A )
assume that
A1: L1 is Linear_Combination of A and
A2: L2 is Linear_Combination of A ; ::_thesis: L1 - L2 is Linear_Combination of A
- L2 is Linear_Combination of A by A2, Th31;
hence L1 - L2 is Linear_Combination of A by A1, Th24; ::_thesis: verum
end;
theorem Th43: :: VECTSP_6:43
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds L - L = ZeroLC V
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds L - L = ZeroLC V
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L being Linear_Combination of V holds L - L = ZeroLC V
let L be Linear_Combination of V; ::_thesis: L - L = ZeroLC V
let v be Element of V; :: according to VECTSP_6:def_7 ::_thesis: (L - L) . v = (ZeroLC V) . v
thus (L - L) . v = (L . v) - (L . v) by Th40
.= 0. GF by RLVECT_1:15
.= (ZeroLC V) . v by Th3 ; ::_thesis: verum
end;
theorem Th44: :: VECTSP_6:44
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
let L1, L2 be Linear_Combination of V; ::_thesis: Sum (L1 + L2) = (Sum L1) + (Sum L2)
set A = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2);
set C1 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1);
consider p being FinSequence such that
A1: rng p = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of the carrier of V by A1, FINSEQ_1:def_4;
A3: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier L1) \/ ((Carrier (L1 + L2)) \/ (Carrier L2)) by XBOOLE_1:4;
set C3 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2));
consider r being FinSequence such that
A4: rng r = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) and
A5: r is one-to-one by FINSEQ_4:58;
reconsider r = r as FinSequence of the carrier of V by A4, FINSEQ_1:def_4;
A6: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier (L1 + L2)) \/ ((Carrier L1) \/ (Carrier L2)) by XBOOLE_1:4;
set C2 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2);
consider q being FinSequence such that
A7: rng q = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) and
A8: q is one-to-one by FINSEQ_4:58;
reconsider q = q as FinSequence of the carrier of V by A7, FINSEQ_1:def_4;
consider F being FinSequence of V such that
A9: F is one-to-one and
A10: rng F = Carrier (L1 + L2) and
A11: Sum ((L1 + L2) (#) F) = Sum (L1 + L2) by Def6;
set FF = F ^ r;
consider G being FinSequence of V such that
A12: G is one-to-one and
A13: rng G = Carrier L1 and
A14: Sum (L1 (#) G) = Sum L1 by Def6;
rng (F ^ r) = (rng F) \/ (rng r) by FINSEQ_1:31;
then rng (F ^ r) = (Carrier (L1 + L2)) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A10, A4, XBOOLE_1:39;
then A15: rng (F ^ r) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A6, XBOOLE_1:7, XBOOLE_1:12;
set GG = G ^ p;
rng (G ^ p) = (rng G) \/ (rng p) by FINSEQ_1:31;
then rng (G ^ p) = (Carrier L1) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A13, A1, XBOOLE_1:39;
then A16: rng (G ^ p) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A3, XBOOLE_1:7, XBOOLE_1:12;
rng F misses rng r
proof
set x = the Element of (rng F) /\ (rng r);
assume not rng F misses rng r ; ::_thesis: contradiction
then (rng F) /\ (rng r) <> {} by XBOOLE_0:def_7;
then ( the Element of (rng F) /\ (rng r) in Carrier (L1 + L2) & the Element of (rng F) /\ (rng r) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) ) by A10, A4, XBOOLE_0:def_4;
hence contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
then A17: F ^ r is one-to-one by A9, A5, FINSEQ_3:91;
rng G misses rng p
proof
set x = the Element of (rng G) /\ (rng p);
assume not rng G misses rng p ; ::_thesis: contradiction
then (rng G) /\ (rng p) <> {} by XBOOLE_0:def_7;
then ( the Element of (rng G) /\ (rng p) in Carrier L1 & the Element of (rng G) /\ (rng p) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) ) by A13, A1, XBOOLE_0:def_4;
hence contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
then A18: G ^ p is one-to-one by A12, A2, FINSEQ_3:91;
then A19: len (G ^ p) = len (F ^ r) by A17, A16, A15, FINSEQ_1:48;
deffunc H1( Nat) -> set = (F ^ r) <- ((G ^ p) . $1);
consider P being FinSequence such that
A20: len P = len (F ^ r) and
A21: for k being Nat st k in dom P holds
P . k = H1(k) from FINSEQ_1:sch_2();
A22: dom P = Seg (len (F ^ r)) by A20, FINSEQ_1:def_3;
A23: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_^_p)_holds_
(G_^_p)_._x_=_(F_^_r)_._(P_._x)
let x be set ; ::_thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (F ^ r) . (P . x) )
assume A24: x in dom (G ^ p) ; ::_thesis: (G ^ p) . x = (F ^ r) . (P . x)
then reconsider n = x as Element of NAT by FINSEQ_3:23;
(G ^ p) . n in rng (F ^ r) by A16, A15, A24, FUNCT_1:def_3;
then A25: F ^ r just_once_values (G ^ p) . n by A17, FINSEQ_4:8;
n in Seg (len (F ^ r)) by A19, A24, FINSEQ_1:def_3;
then (F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by A21, A22
.= (G ^ p) . n by A25, FINSEQ_4:def_3 ;
hence (G ^ p) . x = (F ^ r) . (P . x) ; ::_thesis: verum
end;
A26: rng P c= dom (F ^ r)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P or x in dom (F ^ r) )
assume x in rng P ; ::_thesis: x in dom (F ^ r)
then consider y being set such that
A27: y in dom P and
A28: P . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A27, FINSEQ_3:23;
y in dom (G ^ p) by A19, A20, A27, FINSEQ_3:29;
then (G ^ p) . y in rng (F ^ r) by A16, A15, FUNCT_1:def_3;
then A29: F ^ r just_once_values (G ^ p) . y by A17, FINSEQ_4:8;
P . y = (F ^ r) <- ((G ^ p) . y) by A21, A27;
hence x in dom (F ^ r) by A28, A29, FINSEQ_4:def_3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_(G_^_p)_implies_(_x_in_dom_P_&_P_._x_in_dom_(F_^_r)_)_)_&_(_x_in_dom_P_&_P_._x_in_dom_(F_^_r)_implies_x_in_dom_(G_^_p)_)_)
let x be set ; ::_thesis: ( ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) & ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) ) )
thus ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) ::_thesis: ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) )
proof
assume x in dom (G ^ p) ; ::_thesis: ( x in dom P & P . x in dom (F ^ r) )
then x in Seg (len P) by A19, A20, FINSEQ_1:def_3;
hence x in dom P by FINSEQ_1:def_3; ::_thesis: P . x in dom (F ^ r)
then P . x in rng P by FUNCT_1:def_3;
hence P . x in dom (F ^ r) by A26; ::_thesis: verum
end;
assume that
A30: x in dom P and
P . x in dom (F ^ r) ; ::_thesis: x in dom (G ^ p)
x in Seg (len P) by A30, FINSEQ_1:def_3;
hence x in dom (G ^ p) by A19, A20, FINSEQ_1:def_3; ::_thesis: verum
end;
then A31: G ^ p = (F ^ r) * P by A23, FUNCT_1:10;
dom (F ^ r) c= rng P
proof
set f = ((F ^ r) ") * (G ^ p);
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (F ^ r) or x in rng P )
assume A32: x in dom (F ^ r) ; ::_thesis: x in rng P
dom ((F ^ r) ") = rng (G ^ p) by A17, A16, A15, FUNCT_1:33;
then A33: rng (((F ^ r) ") * (G ^ p)) = rng ((F ^ r) ") by RELAT_1:28
.= dom (F ^ r) by A17, FUNCT_1:33 ;
((F ^ r) ") * (G ^ p) = (((F ^ r) ") * (F ^ r)) * P by A31, RELAT_1:36
.= (id (dom (F ^ r))) * P by A17, FUNCT_1:39
.= P by A26, RELAT_1:53 ;
hence x in rng P by A32, A33; ::_thesis: verum
end;
then A34: dom (F ^ r) = rng P by A26, XBOOLE_0:def_10;
A35: len r = len ((L1 + L2) (#) r) by Def5;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_
((L1_+_L2)_(#)_r)_._k_=_(0._GF)_*_(r_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom r implies ((L1 + L2) (#) r) . k = (0. GF) * (r /. k) )
assume A36: k in dom r ; ::_thesis: ((L1 + L2) (#) r) . k = (0. GF) * (r /. k)
then r /. k = r . k by PARTFUN1:def_6;
then r /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) by A4, A36, FUNCT_1:def_3;
then A37: not r /. k in Carrier (L1 + L2) by XBOOLE_0:def_5;
k in dom ((L1 + L2) (#) r) by A35, A36, FINSEQ_3:29;
then ((L1 + L2) (#) r) . k = ((L1 + L2) . (r /. k)) * (r /. k) by Def5;
hence ((L1 + L2) (#) r) . k = (0. GF) * (r /. k) by A37; ::_thesis: verum
end;
then A38: Sum ((L1 + L2) (#) r) = (0. GF) * (Sum r) by A35, RLVECT_2:67
.= 0. V by VECTSP_1:14 ;
A39: len p = len (L1 (#) p) by Def5;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_
(L1_(#)_p)_._k_=_(0._GF)_*_(p_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom p implies (L1 (#) p) . k = (0. GF) * (p /. k) )
assume A40: k in dom p ; ::_thesis: (L1 (#) p) . k = (0. GF) * (p /. k)
then p /. k = p . k by PARTFUN1:def_6;
then p /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) by A1, A40, FUNCT_1:def_3;
then A41: not p /. k in Carrier L1 by XBOOLE_0:def_5;
k in dom (L1 (#) p) by A39, A40, FINSEQ_3:29;
then (L1 (#) p) . k = (L1 . (p /. k)) * (p /. k) by Def5;
hence (L1 (#) p) . k = (0. GF) * (p /. k) by A41; ::_thesis: verum
end;
then A42: Sum (L1 (#) p) = (0. GF) * (Sum p) by A39, RLVECT_2:67
.= 0. V by VECTSP_1:14 ;
A43: len q = len (L2 (#) q) by Def5;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_q_holds_
(L2_(#)_q)_._k_=_(0._GF)_*_(q_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom q implies (L2 (#) q) . k = (0. GF) * (q /. k) )
assume A44: k in dom q ; ::_thesis: (L2 (#) q) . k = (0. GF) * (q /. k)
then q /. k = q . k by PARTFUN1:def_6;
then q /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) by A7, A44, FUNCT_1:def_3;
then A45: not q /. k in Carrier L2 by XBOOLE_0:def_5;
k in dom (L2 (#) q) by A43, A44, FINSEQ_3:29;
then (L2 (#) q) . k = (L2 . (q /. k)) * (q /. k) by Def5;
hence (L2 (#) q) . k = (0. GF) * (q /. k) by A45; ::_thesis: verum
end;
then A46: Sum (L2 (#) q) = (0. GF) * (Sum q) by A43, RLVECT_2:67
.= 0. V by VECTSP_1:14 ;
set g = L1 (#) (G ^ p);
A47: len (L1 (#) (G ^ p)) = len (G ^ p) by Def5;
then A48: Seg (len (G ^ p)) = dom (L1 (#) (G ^ p)) by FINSEQ_1:def_3;
set f = (L1 + L2) (#) (F ^ r);
consider H being FinSequence of V such that
A49: H is one-to-one and
A50: rng H = Carrier L2 and
A51: Sum (L2 (#) H) = Sum L2 by Def6;
set HH = H ^ q;
rng H misses rng q
proof
set x = the Element of (rng H) /\ (rng q);
assume not rng H misses rng q ; ::_thesis: contradiction
then (rng H) /\ (rng q) <> {} by XBOOLE_0:def_7;
then ( the Element of (rng H) /\ (rng q) in Carrier L2 & the Element of (rng H) /\ (rng q) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) ) by A50, A7, XBOOLE_0:def_4;
hence contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
then A52: H ^ q is one-to-one by A49, A8, FINSEQ_3:91;
rng (H ^ q) = (rng H) \/ (rng q) by FINSEQ_1:31;
then rng (H ^ q) = (Carrier L2) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A50, A7, XBOOLE_1:39;
then A53: rng (H ^ q) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by XBOOLE_1:7, XBOOLE_1:12;
then A54: len (G ^ p) = len (H ^ q) by A52, A18, A16, FINSEQ_1:48;
deffunc H2( Nat) -> set = (H ^ q) <- ((G ^ p) . $1);
consider R being FinSequence such that
A55: len R = len (H ^ q) and
A56: for k being Nat st k in dom R holds
R . k = H2(k) from FINSEQ_1:sch_2();
A57: dom R = Seg (len (H ^ q)) by A55, FINSEQ_1:def_3;
A58: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_^_p)_holds_
(G_^_p)_._x_=_(H_^_q)_._(R_._x)
let x be set ; ::_thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (H ^ q) . (R . x) )
assume A59: x in dom (G ^ p) ; ::_thesis: (G ^ p) . x = (H ^ q) . (R . x)
then reconsider n = x as Element of NAT by FINSEQ_3:23;
(G ^ p) . n in rng (H ^ q) by A16, A53, A59, FUNCT_1:def_3;
then A60: H ^ q just_once_values (G ^ p) . n by A52, FINSEQ_4:8;
n in Seg (len (H ^ q)) by A54, A59, FINSEQ_1:def_3;
then (H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by A56, A57
.= (G ^ p) . n by A60, FINSEQ_4:def_3 ;
hence (G ^ p) . x = (H ^ q) . (R . x) ; ::_thesis: verum
end;
A61: rng R c= dom (H ^ q)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng R or x in dom (H ^ q) )
assume x in rng R ; ::_thesis: x in dom (H ^ q)
then consider y being set such that
A62: y in dom R and
A63: R . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A62, FINSEQ_3:23;
y in dom (G ^ p) by A54, A55, A62, FINSEQ_3:29;
then (G ^ p) . y in rng (H ^ q) by A16, A53, FUNCT_1:def_3;
then A64: H ^ q just_once_values (G ^ p) . y by A52, FINSEQ_4:8;
R . y = (H ^ q) <- ((G ^ p) . y) by A56, A62;
hence x in dom (H ^ q) by A63, A64, FINSEQ_4:def_3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_(G_^_p)_implies_(_x_in_dom_R_&_R_._x_in_dom_(H_^_q)_)_)_&_(_x_in_dom_R_&_R_._x_in_dom_(H_^_q)_implies_x_in_dom_(G_^_p)_)_)
let x be set ; ::_thesis: ( ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) & ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) ) )
thus ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) ::_thesis: ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) )
proof
assume x in dom (G ^ p) ; ::_thesis: ( x in dom R & R . x in dom (H ^ q) )
then x in Seg (len R) by A54, A55, FINSEQ_1:def_3;
hence x in dom R by FINSEQ_1:def_3; ::_thesis: R . x in dom (H ^ q)
then R . x in rng R by FUNCT_1:def_3;
hence R . x in dom (H ^ q) by A61; ::_thesis: verum
end;
assume that
A65: x in dom R and
R . x in dom (H ^ q) ; ::_thesis: x in dom (G ^ p)
x in Seg (len R) by A65, FINSEQ_1:def_3;
hence x in dom (G ^ p) by A54, A55, FINSEQ_1:def_3; ::_thesis: verum
end;
then A66: G ^ p = (H ^ q) * R by A58, FUNCT_1:10;
dom (H ^ q) c= rng R
proof
set f = ((H ^ q) ") * (G ^ p);
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (H ^ q) or x in rng R )
assume A67: x in dom (H ^ q) ; ::_thesis: x in rng R
dom ((H ^ q) ") = rng (G ^ p) by A52, A16, A53, FUNCT_1:33;
then A68: rng (((H ^ q) ") * (G ^ p)) = rng ((H ^ q) ") by RELAT_1:28
.= dom (H ^ q) by A52, FUNCT_1:33 ;
((H ^ q) ") * (G ^ p) = (((H ^ q) ") * (H ^ q)) * R by A66, RELAT_1:36
.= (id (dom (H ^ q))) * R by A52, FUNCT_1:39
.= R by A61, RELAT_1:53 ;
hence x in rng R by A67, A68; ::_thesis: verum
end;
then A69: dom (H ^ q) = rng R by A61, XBOOLE_0:def_10;
set h = L2 (#) (H ^ q);
A70: Sum (L2 (#) (H ^ q)) = Sum ((L2 (#) H) ^ (L2 (#) q)) by Th13
.= (Sum (L2 (#) H)) + (0. V) by A46, RLVECT_1:41
.= Sum (L2 (#) H) by RLVECT_1:4 ;
A71: Sum (L1 (#) (G ^ p)) = Sum ((L1 (#) G) ^ (L1 (#) p)) by Th13
.= (Sum (L1 (#) G)) + (0. V) by A42, RLVECT_1:41
.= Sum (L1 (#) G) by RLVECT_1:4 ;
A72: dom P = dom (F ^ r) by A20, FINSEQ_3:29;
then A73: P is one-to-one by A34, FINSEQ_4:60;
A74: dom R = dom (H ^ q) by A55, FINSEQ_3:29;
then A75: R is one-to-one by A69, FINSEQ_4:60;
reconsider R = R as Function of (dom (H ^ q)),(dom (H ^ q)) by A61, A74, FUNCT_2:2;
reconsider R = R as Permutation of (dom (H ^ q)) by A69, A75, FUNCT_2:57;
A76: len (L2 (#) (H ^ q)) = len (H ^ q) by Def5;
then dom (L2 (#) (H ^ q)) = dom (H ^ q) by FINSEQ_3:29;
then reconsider R = R as Permutation of (dom (L2 (#) (H ^ q))) ;
reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of the carrier of V by FINSEQ_2:47;
A77: len Hp = len (G ^ p) by A54, A76, FINSEQ_2:44;
reconsider P = P as Function of (dom (F ^ r)),(dom (F ^ r)) by A26, A72, FUNCT_2:2;
reconsider P = P as Permutation of (dom (F ^ r)) by A34, A73, FUNCT_2:57;
A78: len ((L1 + L2) (#) (F ^ r)) = len (F ^ r) by Def5;
then dom ((L1 + L2) (#) (F ^ r)) = dom (F ^ r) by FINSEQ_3:29;
then reconsider P = P as Permutation of (dom ((L1 + L2) (#) (F ^ r))) ;
reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of the carrier of V by FINSEQ_2:47;
A79: Sum ((L1 + L2) (#) (F ^ r)) = Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Th13
.= (Sum ((L1 + L2) (#) F)) + (0. V) by A38, RLVECT_1:41
.= Sum ((L1 + L2) (#) F) by RLVECT_1:4 ;
deffunc H3( Nat) -> Element of the carrier of V = ((L1 (#) (G ^ p)) /. $1) + (Hp /. $1);
consider I being FinSequence such that
A80: len I = len (G ^ p) and
A81: for k being Nat st k in dom I holds
I . k = H3(k) from FINSEQ_1:sch_2();
A82: dom I = Seg (len (G ^ p)) by A80, FINSEQ_1:def_3;
then A83: for k being Element of NAT st k in Seg (len (G ^ p)) holds
I . k = H3(k) by A81;
rng I c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng I or x in the carrier of V )
assume x in rng I ; ::_thesis: x in the carrier of V
then consider y being set such that
A84: y in dom I and
A85: I . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A84, FINSEQ_3:23;
I . y = ((L1 (#) (G ^ p)) /. y) + (Hp /. y) by A81, A84;
hence x in the carrier of V by A85; ::_thesis: verum
end;
then reconsider I = I as FinSequence of the carrier of V by FINSEQ_1:def_4;
A86: len Fp = len I by A19, A78, A80, FINSEQ_2:44;
A87: now__::_thesis:_for_x_being_set_st_x_in_Seg_(len_I)_holds_
I_._x_=_Fp_._x
let x be set ; ::_thesis: ( x in Seg (len I) implies I . x = Fp . x )
assume A88: x in Seg (len I) ; ::_thesis: I . x = Fp . x
then reconsider k = x as Element of NAT ;
A89: x in dom Hp by A80, A77, A88, FINSEQ_1:def_3;
then A90: Hp /. k = ((L2 (#) (H ^ q)) * R) . k by PARTFUN1:def_6
.= (L2 (#) (H ^ q)) . (R . k) by A89, FUNCT_1:12 ;
set v = (G ^ p) /. k;
x in dom Fp by A86, A88, FINSEQ_1:def_3;
then A91: Fp . k = ((L1 + L2) (#) (F ^ r)) . (P . k) by FUNCT_1:12;
A92: x in dom (H ^ q) by A54, A80, A88, FINSEQ_1:def_3;
then R . k in dom R by A69, A74, FUNCT_1:def_3;
then reconsider j = R . k as Element of NAT by FINSEQ_3:23;
A93: x in dom (G ^ p) by A80, A88, FINSEQ_1:def_3;
then A94: (H ^ q) . j = (G ^ p) . k by A58
.= (G ^ p) /. k by A93, PARTFUN1:def_6 ;
A95: dom (F ^ r) = dom (G ^ p) by A19, FINSEQ_3:29;
then P . k in dom P by A34, A72, A93, FUNCT_1:def_3;
then reconsider l = P . k as Element of NAT by FINSEQ_3:23;
A96: (F ^ r) . l = (G ^ p) . k by A23, A93
.= (G ^ p) /. k by A93, PARTFUN1:def_6 ;
R . k in dom (H ^ q) by A69, A74, A92, FUNCT_1:def_3;
then A97: (L2 (#) (H ^ q)) . j = (L2 . ((G ^ p) /. k)) * ((G ^ p) /. k) by A94, Th8;
P . k in dom (F ^ r) by A34, A72, A93, A95, FUNCT_1:def_3;
then A98: ((L1 + L2) (#) (F ^ r)) . l = ((L1 + L2) . ((G ^ p) /. k)) * ((G ^ p) /. k) by A96, Th8
.= ((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) * ((G ^ p) /. k) by Th22
.= ((L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)) + ((L2 . ((G ^ p) /. k)) * ((G ^ p) /. k)) by VECTSP_1:def_15 ;
A99: x in dom (L1 (#) (G ^ p)) by A80, A47, A88, FINSEQ_1:def_3;
then (L1 (#) (G ^ p)) /. k = (L1 (#) (G ^ p)) . k by PARTFUN1:def_6
.= (L1 . ((G ^ p) /. k)) * ((G ^ p) /. k) by A99, Def5 ;
hence I . x = Fp . x by A80, A81, A82, A88, A90, A97, A91, A98; ::_thesis: verum
end;
( dom I = Seg (len I) & dom Fp = Seg (len I) ) by A86, FINSEQ_1:def_3;
then A100: I = Fp by A87, FUNCT_1:2;
( Sum Fp = Sum ((L1 + L2) (#) (F ^ r)) & Sum Hp = Sum (L2 (#) (H ^ q)) ) by RLVECT_2:7;
hence Sum (L1 + L2) = (Sum L1) + (Sum L2) by A11, A14, A51, A71, A70, A79, A80, A83, A77, A47, A100, A48, RLVECT_2:2; ::_thesis: verum
end;
theorem :: VECTSP_6:45
for GF being Field
for V being VectSp of GF
for L being Linear_Combination of V
for a being Element of GF holds Sum (a * L) = a * (Sum L)
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for L being Linear_Combination of V
for a being Element of GF holds Sum (a * L) = a * (Sum L)
let V be VectSp of GF; ::_thesis: for L being Linear_Combination of V
for a being Element of GF holds Sum (a * L) = a * (Sum L)
let L be Linear_Combination of V; ::_thesis: for a being Element of GF holds Sum (a * L) = a * (Sum L)
let a be Element of GF; ::_thesis: Sum (a * L) = a * (Sum L)
percases ( a <> 0. GF or a = 0. GF ) ;
supposeA1: a <> 0. GF ; ::_thesis: Sum (a * L) = a * (Sum L)
set l = a * L;
consider F being FinSequence of the carrier of V such that
A2: F is one-to-one and
A3: rng F = Carrier (a * L) and
A4: Sum (a * L) = Sum ((a * L) (#) F) by Def6;
consider G being FinSequence of the carrier of V such that
A5: G is one-to-one and
A6: rng G = Carrier L and
A7: Sum L = Sum (L (#) G) by Def6;
A8: len G = len F by A1, A2, A3, A5, A6, Th29, FINSEQ_1:48;
set f = (a * L) (#) F;
set g = L (#) G;
deffunc H1( Nat) -> set = F <- (G . $1);
consider P being FinSequence such that
A9: len P = len F and
A10: for k being Nat st k in dom P holds
P . k = H1(k) from FINSEQ_1:sch_2();
A11: Carrier (a * L) = Carrier L by A1, Th29;
A12: rng P c= Seg (len F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P or x in Seg (len F) )
assume x in rng P ; ::_thesis: x in Seg (len F)
then consider y being set such that
A13: y in dom P and
A14: P . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A13, FINSEQ_3:23;
y in Seg (len F) by A9, A13, FINSEQ_1:def_3;
then y in dom G by A8, FINSEQ_1:def_3;
then G . y in rng F by A3, A6, A11, FUNCT_1:def_3;
then A15: F just_once_values G . y by A2, FINSEQ_4:8;
P . y = F <- (G . y) by A10, A13;
then P . y in dom F by A15, FINSEQ_4:def_3;
hence x in Seg (len F) by A14, FINSEQ_1:def_3; ::_thesis: verum
end;
A16: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_G_implies_(_x_in_dom_P_&_P_._x_in_dom_F_)_)_&_(_x_in_dom_P_&_P_._x_in_dom_F_implies_x_in_dom_G_)_)
let x be set ; ::_thesis: ( ( x in dom G implies ( x in dom P & P . x in dom F ) ) & ( x in dom P & P . x in dom F implies x in dom G ) )
thus ( x in dom G implies ( x in dom P & P . x in dom F ) ) ::_thesis: ( x in dom P & P . x in dom F implies x in dom G )
proof
assume x in dom G ; ::_thesis: ( x in dom P & P . x in dom F )
then x in Seg (len P) by A9, A8, FINSEQ_1:def_3;
hence x in dom P by FINSEQ_1:def_3; ::_thesis: P . x in dom F
then P . x in rng P by FUNCT_1:def_3;
then P . x in Seg (len F) by A12;
hence P . x in dom F by FINSEQ_1:def_3; ::_thesis: verum
end;
assume that
A17: x in dom P and
P . x in dom F ; ::_thesis: x in dom G
x in Seg (len P) by A17, FINSEQ_1:def_3;
hence x in dom G by A9, A8, FINSEQ_1:def_3; ::_thesis: verum
end;
A18: dom P = Seg (len F) by A9, FINSEQ_1:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_G_holds_
G_._x_=_F_._(P_._x)
let x be set ; ::_thesis: ( x in dom G implies G . x = F . (P . x) )
assume A19: x in dom G ; ::_thesis: G . x = F . (P . x)
then reconsider n = x as Element of NAT by FINSEQ_3:23;
G . n in rng F by A3, A6, A11, A19, FUNCT_1:def_3;
then A20: F just_once_values G . n by A2, FINSEQ_4:8;
n in Seg (len F) by A8, A19, FINSEQ_1:def_3;
then F . (P . n) = F . (F <- (G . n)) by A10, A18
.= G . n by A20, FINSEQ_4:def_3 ;
hence G . x = F . (P . x) ; ::_thesis: verum
end;
then A21: G = F * P by A16, FUNCT_1:10;
Seg (len F) c= rng P
proof
set f = (F ") * G;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg (len F) or x in rng P )
assume A22: x in Seg (len F) ; ::_thesis: x in rng P
dom (F ") = rng G by A2, A3, A6, A11, FUNCT_1:33;
then A23: rng ((F ") * G) = rng (F ") by RELAT_1:28
.= dom F by A2, FUNCT_1:33 ;
A24: rng P c= dom F by A12, FINSEQ_1:def_3;
(F ") * G = ((F ") * F) * P by A21, RELAT_1:36
.= (id (dom F)) * P by A2, FUNCT_1:39
.= P by A24, RELAT_1:53 ;
hence x in rng P by A22, A23, FINSEQ_1:def_3; ::_thesis: verum
end;
then A25: Seg (len F) = rng P by A12, XBOOLE_0:def_10;
A26: dom P = Seg (len F) by A9, FINSEQ_1:def_3;
then A27: P is one-to-one by A25, FINSEQ_4:60;
reconsider P = P as Function of (Seg (len F)),(Seg (len F)) by A12, A26, FUNCT_2:2;
reconsider P = P as Permutation of (Seg (len F)) by A25, A27, FUNCT_2:57;
A28: len ((a * L) (#) F) = len F by Def5;
then dom ((a * L) (#) F) = Seg (len F) by FINSEQ_1:def_3;
then reconsider P = P as Permutation of (dom ((a * L) (#) F)) ;
reconsider Fp = ((a * L) (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:47;
A29: len Fp = len ((a * L) (#) F) by FINSEQ_2:44;
then A30: len Fp = len (L (#) G) by A8, A28, Def5;
A31: now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_Vector_of_V_st_k_in_dom_(L_(#)_G)_&_v_=_(L_(#)_G)_._k_holds_
Fp_._k_=_a_*_v
let k be Element of NAT ; ::_thesis: for v being Vector of V st k in dom (L (#) G) & v = (L (#) G) . k holds
Fp . k = a * v
let v be Vector of V; ::_thesis: ( k in dom (L (#) G) & v = (L (#) G) . k implies Fp . k = a * v )
assume that
A32: k in dom (L (#) G) and
A33: v = (L (#) G) . k ; ::_thesis: Fp . k = a * v
A34: k in Seg (len (L (#) G)) by A32, FINSEQ_1:def_3;
then A35: k in dom P by A9, A28, A29, A30, FINSEQ_1:def_3;
A36: k in dom G by A8, A28, A29, A30, A34, FINSEQ_1:def_3;
then G . k in rng G by FUNCT_1:def_3;
then F just_once_values G . k by A2, A3, A6, A11, FINSEQ_4:8;
then A37: F <- (G . k) in dom F by FINSEQ_4:def_3;
then reconsider i = F <- (G . k) as Element of NAT by FINSEQ_3:23;
A38: G /. k = G . k by A36, PARTFUN1:def_6
.= F . (P . k) by A21, A35, FUNCT_1:13
.= F . i by A10, A18, A28, A29, A30, A34
.= F /. i by A37, PARTFUN1:def_6 ;
i in Seg (len ((a * L) (#) F)) by A28, A37, FINSEQ_1:def_3;
then A39: i in dom ((a * L) (#) F) by FINSEQ_1:def_3;
thus Fp . k = ((a * L) (#) F) . (P . k) by A35, FUNCT_1:13
.= ((a * L) (#) F) . (F <- (G . k)) by A10, A18, A28, A29, A30, A34
.= ((a * L) . (F /. i)) * (F /. i) by A39, Def5
.= (a * (L . (F /. i))) * (F /. i) by Def9
.= a * ((L . (F /. i)) * (F /. i)) by VECTSP_1:def_16
.= a * v by A32, A33, A38, Def5 ; ::_thesis: verum
end;
( Sum Fp = Sum ((a * L) (#) F) & dom Fp = dom (L (#) G) ) by A30, FINSEQ_3:29, RLVECT_2:7;
hence Sum (a * L) = a * (Sum L) by A4, A7, A30, A31, RLVECT_2:66; ::_thesis: verum
end;
supposeA40: a = 0. GF ; ::_thesis: Sum (a * L) = a * (Sum L)
hence Sum (a * L) = Sum (ZeroLC V) by Th30
.= 0. V by Lm1
.= a * (Sum L) by A40, VECTSP_1:14 ;
::_thesis: verum
end;
end;
end;
theorem Th46: :: VECTSP_6:46
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
let L be Linear_Combination of V; ::_thesis: Sum (- L) = - (Sum L)
(Sum L) + (Sum (- L)) = Sum (L - L) by Th44
.= Sum (ZeroLC V) by Th43
.= 0. V by Lm1 ;
hence Sum (- L) = - (Sum L) by VECTSP_1:16; ::_thesis: verum
end;
theorem :: VECTSP_6:47
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
let L1, L2 be Linear_Combination of V; ::_thesis: Sum (L1 - L2) = (Sum L1) - (Sum L2)
thus Sum (L1 - L2) = (Sum L1) + (Sum (- L2)) by Th44
.= (Sum L1) + (- (Sum L2)) by Th46
.= (Sum L1) - (Sum L2) by RLVECT_1:def_11 ; ::_thesis: verum
end;
theorem :: VECTSP_6:48
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of GF holds (- (1. GF)) * a = - a by Lm2;
theorem :: VECTSP_6:49
for GF being Field holds - (1. GF) <> 0. GF by Lm3;