:: MATRTOP2 semantic presentation
begin
Lm1: for n being Nat holds the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)
proof
let n be Nat; ::_thesis: the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)
thus the carrier of (n -VectSp_over F_Real) = REAL n by MATRIX13:102
.= the carrier of (TOP-REAL n) by EUCLID:22 ; ::_thesis: verum
end;
Lm2: for n being Nat holds 0. (n -VectSp_over F_Real) = 0. (TOP-REAL n)
proof
let n be Nat; ::_thesis: 0. (n -VectSp_over F_Real) = 0. (TOP-REAL n)
thus 0. (n -VectSp_over F_Real) = n |-> (0. F_Real) by MATRIX13:102
.= 0* n
.= 0. (TOP-REAL n) by EUCLID:70 ; ::_thesis: verum
end;
Lm3: for n being Nat
for f being b1 -element real-valued FinSequence holds f is Point of (TOP-REAL n)
proof
let n be Nat; ::_thesis: for f being n -element real-valued FinSequence holds f is Point of (TOP-REAL n)
let f be n -element real-valued FinSequence; ::_thesis: f is Point of (TOP-REAL n)
( len f = n & @ (@ f) = f ) by CARD_1:def_7;
hence f is Point of (TOP-REAL n) by TOPREAL3:46; ::_thesis: verum
end;
theorem Th1: :: MATRTOP2:1
for X being set
for n being Nat holds
( X is Linear_Combination of n -VectSp_over F_Real iff X is Linear_Combination of TOP-REAL n )
proof
let X be set ; ::_thesis: for n being Nat holds
( X is Linear_Combination of n -VectSp_over F_Real iff X is Linear_Combination of TOP-REAL n )
let n be Nat; ::_thesis: ( X is Linear_Combination of n -VectSp_over F_Real iff X is Linear_Combination of TOP-REAL n )
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;
hereby ::_thesis: ( X is Linear_Combination of TOP-REAL n implies X is Linear_Combination of n -VectSp_over F_Real )
assume X is Linear_Combination of n -VectSp_over F_Real ; ::_thesis: X is Linear_Combination of TOP-REAL n
then reconsider L = X as Linear_Combination of n -VectSp_over F_Real ;
consider S being finite Subset of (n -VectSp_over F_Real) such that
A1: for v being Element of (n -VectSp_over F_Real) st not v in S holds
L . v = 0. F_Real by VECTSP_6:def_1;
A2: now__::_thesis:_for_v_being_Element_of_(TOP-REAL_n)_st_not_v_in_S_holds_
0_=_L_._v
let v be Element of (TOP-REAL n); ::_thesis: ( not v in S implies 0 = L . v )
assume A3: not v in S ; ::_thesis: 0 = L . v
v is Element of (n -VectSp_over F_Real) by Lm1;
hence 0 = L . v by A1, A3; ::_thesis: verum
end;
( L is Element of Funcs ( the carrier of (TOP-REAL n),REAL) & S is finite Subset of (TOP-REAL n) ) by Lm1;
hence X is Linear_Combination of TOP-REAL n by A2, RLVECT_2:def_3; ::_thesis: verum
end;
assume X is Linear_Combination of TOP-REAL n ; ::_thesis: X is Linear_Combination of n -VectSp_over F_Real
then reconsider L = X as Linear_Combination of TOP-REAL n ;
consider S being finite Subset of (TOP-REAL n) such that
A4: for v being Element of (TOP-REAL n) st not v in S holds
L . v = 0 by RLVECT_2:def_3;
A5: now__::_thesis:_for_v_being_Element_of_(n_-VectSp_over_F_Real)_st_not_v_in_S_holds_
0._F_Real_=_L_._v
let v be Element of (n -VectSp_over F_Real); ::_thesis: ( not v in S implies 0. F_Real = L . v )
assume A6: not v in S ; ::_thesis: 0. F_Real = L . v
v is Element of (TOP-REAL n) by Lm1;
hence 0. F_Real = L . v by A4, A6; ::_thesis: verum
end;
( L is Element of Funcs ( the carrier of (n -VectSp_over F_Real), the carrier of F_Real) & S is finite Subset of (n -VectSp_over F_Real) ) by Lm1;
hence X is Linear_Combination of n -VectSp_over F_Real by A5, VECTSP_6:def_1; ::_thesis: verum
end;
theorem Th2: :: MATRTOP2:2
for n being Nat
for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Carrier Lr = Carrier Lv
proof
let n be Nat; ::_thesis: for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Carrier Lr = Carrier Lv
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;
let Lv be Linear_Combination of n -VectSp_over F_Real; ::_thesis: for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Carrier Lr = Carrier Lv
let Lr be Linear_Combination of TOP-REAL n; ::_thesis: ( Lr = Lv implies Carrier Lr = Carrier Lv )
assume A1: Lr = Lv ; ::_thesis: Carrier Lr = Carrier Lv
thus Carrier Lr c= Carrier Lv :: according to XBOOLE_0:def_10 ::_thesis: Carrier Lv c= Carrier Lr
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier Lr or x in Carrier Lv )
assume A2: x in Carrier Lr ; ::_thesis: x in Carrier Lv
then reconsider v = x as Element of (TOP-REAL n) ;
reconsider u = v as Element of (n -VectSp_over F_Real) by Lm1;
Lv . u <> 0. F_Real by A1, A2, RLVECT_2:19;
hence x in Carrier Lv by VECTSP_6:1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier Lv or x in Carrier Lr )
assume x in Carrier Lv ; ::_thesis: x in Carrier Lr
then consider u being Element of (n -VectSp_over F_Real) such that
A3: x = u and
A4: Lv . u <> 0. F_Real by VECTSP_6:1;
reconsider v = u as Element of (TOP-REAL n) by Lm1;
v in Carrier Lr by A1, A4, RLVECT_2:19;
hence x in Carrier Lr by A3; ::_thesis: verum
end;
theorem Th3: :: MATRTOP2:3
for n being Nat
for F being FinSequence of (TOP-REAL n)
for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
proof
let n be Nat; ::_thesis: for F being FinSequence of (TOP-REAL n)
for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let F be FinSequence of (TOP-REAL n); ::_thesis: for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let fr be Function of (TOP-REAL n),REAL; ::_thesis: for Fv being FinSequence of (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let Fv be FinSequence of (n -VectSp_over F_Real); ::_thesis: for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let fv be Function of (n -VectSp_over F_Real),F_Real; ::_thesis: ( fr = fv & F = Fv implies fr (#) F = fv (#) Fv )
assume that
A1: fr = fv and
A2: F = Fv ; ::_thesis: fr (#) F = fv (#) Fv
A3: len (fv (#) Fv) = len Fv by VECTSP_6:def_5;
A4: len (fr (#) F) = len F by RLVECT_2:def_7;
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_F_holds_
(fr_(#)_F)_._i_=_(fv_(#)_Fv)_._i
reconsider T = TOP-REAL n as RealLinearSpace ;
let i be Nat; ::_thesis: ( 1 <= i & i <= len F implies (fr (#) F) . i = (fv (#) Fv) . i )
reconsider Fi = F /. i as FinSequence of REAL by EUCLID:24;
reconsider Fvi = Fv /. i as Element of n -tuples_on the carrier of F_Real by MATRIX13:102;
reconsider Fii = F /. i as Element of T ;
assume A5: ( 1 <= i & i <= len F ) ; ::_thesis: (fr (#) F) . i = (fv (#) Fv) . i
then A6: i in dom (fv (#) Fv) by A2, A3, FINSEQ_3:25;
i in dom F by A5, FINSEQ_3:25;
then A7: F /. i = F . i by PARTFUN1:def_6;
i in dom Fv by A2, A5, FINSEQ_3:25;
then A8: Fv /. i = Fv . i by PARTFUN1:def_6;
i in dom (fr (#) F) by A4, A5, FINSEQ_3:25;
hence (fr (#) F) . i = (fr . Fii) * Fii by RLVECT_2:def_7
.= (fr . Fi) * Fi by EUCLID:65
.= (fv . (Fv /. i)) * Fvi by A1, A2, A7, A8, MATRIXR1:17
.= (fv . (Fv /. i)) * (Fv /. i) by MATRIX13:102
.= (fv (#) Fv) . i by A6, VECTSP_6:def_5 ;
::_thesis: verum
end;
hence fr (#) F = fv (#) Fv by A2, A4, A3, FINSEQ_1:14; ::_thesis: verum
end;
theorem Th4: :: MATRTOP2:4
for n being Nat
for F being FinSequence of (TOP-REAL n)
for Fv being FinSequence of (n -VectSp_over F_Real) st Fv = F holds
Sum F = Sum Fv
proof
let n be Nat; ::_thesis: for F being FinSequence of (TOP-REAL n)
for Fv being FinSequence of (n -VectSp_over F_Real) st Fv = F holds
Sum F = Sum Fv
set T = TOP-REAL n;
set V = n -VectSp_over F_Real;
let F be FinSequence of (TOP-REAL n); ::_thesis: for Fv being FinSequence of (n -VectSp_over F_Real) st Fv = F holds
Sum F = Sum Fv
let Fv be FinSequence of (n -VectSp_over F_Real); ::_thesis: ( Fv = F implies Sum F = Sum Fv )
assume A1: Fv = F ; ::_thesis: Sum F = Sum Fv
reconsider T = TOP-REAL n as RealLinearSpace ;
consider f being Function of NAT, the carrier of T such that
A2: Sum F = f . (len F) and
A3: f . 0 = 0. T and
A4: for j being Element of NAT
for v being Element of T st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def_12;
consider fv being Function of NAT, the carrier of (n -VectSp_over F_Real) such that
A5: Sum Fv = fv . (len Fv) and
A6: fv . 0 = 0. (n -VectSp_over F_Real) and
A7: for j being Element of NAT
for v being Element of (n -VectSp_over F_Real) st j < len Fv & v = Fv . (j + 1) holds
fv . (j + 1) = (fv . j) + v by RLVECT_1:def_12;
defpred S1[ Nat] means ( $1 <= len F implies f . $1 = fv . $1 );
A8: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A9: S1[i] ; ::_thesis: S1[i + 1]
set i1 = i + 1;
reconsider Fvi1 = Fv /. (i + 1), fvi = fv . i as Element of n -tuples_on the carrier of F_Real by MATRIX13:102;
A10: ( @ (@ Fvi1) = Fvi1 & @ (@ fvi) = fvi ) ;
reconsider Fi1 = F /. (i + 1) as Element of T ;
assume A11: i + 1 <= len F ; ::_thesis: f . (i + 1) = fv . (i + 1)
then A12: i < len F by NAT_1:13;
1 <= i + 1 by NAT_1:11;
then A13: i + 1 in dom F by A11, FINSEQ_3:25;
then F . (i + 1) = F /. (i + 1) by PARTFUN1:def_6;
then A14: f . (i + 1) = (f . i) + Fi1 by A4, A12;
A15: Fv /. (i + 1) = Fv . (i + 1) by A1, A13, PARTFUN1:def_6;
then Fvi1 = F /. (i + 1) by A1, A13, PARTFUN1:def_6;
hence f . (i + 1) = (@ fvi) + (@ Fvi1) by A9, A11, A14, EUCLID:64, NAT_1:13
.= fvi + Fvi1 by A10, MATRTOP1:1
.= (fv . i) + (Fv /. (i + 1)) by MATRIX13:102
.= fv . (i + 1) by A1, A7, A12, A15 ;
::_thesis: verum
end;
A16: S1[ 0 ] by A3, A6, Lm2;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A16, A8);
hence Sum F = Sum Fv by A1, A2, A5; ::_thesis: verum
end;
theorem Th5: :: MATRTOP2:5
for n being Nat
for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv
proof
let n be Nat; ::_thesis: for Lv being Linear_Combination of n -VectSp_over F_Real
for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;
let Lv be Linear_Combination of n -VectSp_over F_Real; ::_thesis: for Lr being Linear_Combination of TOP-REAL n st Lr = Lv holds
Sum Lr = Sum Lv
let Lr be Linear_Combination of TOP-REAL n; ::_thesis: ( Lr = Lv implies Sum Lr = Sum Lv )
assume A1: Lr = Lv ; ::_thesis: Sum Lr = Sum Lv
consider F being FinSequence of the carrier of (TOP-REAL n) such that
A2: ( F is one-to-one & rng F = Carrier Lr ) and
A3: Sum Lr = Sum (Lr (#) F) by RLVECT_2:def_8;
reconsider F1 = F as FinSequence of the carrier of (n -VectSp_over F_Real) by Lm1;
A4: Lr (#) F = Lv (#) F1 by A1, Th3;
Carrier Lr = Carrier Lv by A1, Th2;
hence Sum Lv = Sum (Lv (#) F1) by A2, VECTSP_6:def_6
.= Sum Lr by A3, A4, Th4 ;
::_thesis: verum
end;
theorem Th6: :: MATRTOP2:6
for n being Nat
for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
proof
let n be Nat; ::_thesis: for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;
let Af be Subset of (n -VectSp_over F_Real); ::_thesis: for Ar being Subset of (TOP-REAL n) st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
let Ar be Subset of (TOP-REAL n); ::_thesis: ( Af = Ar implies [#] (Lin Ar) = [#] (Lin Af) )
assume A1: Af = Ar ; ::_thesis: [#] (Lin Ar) = [#] (Lin Af)
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: [#] (Lin Af) c= [#] (Lin Ar)
let x be set ; ::_thesis: ( x in [#] (Lin Ar) implies x in [#] (Lin Af) )
assume x in [#] (Lin Ar) ; ::_thesis: x in [#] (Lin Af)
then x in Lin Ar by STRUCT_0:def_5;
then consider L being Linear_Combination of Ar such that
A2: x = Sum L by RLVECT_3:14;
reconsider L1 = L as Linear_Combination of n -VectSp_over F_Real by Th1;
( Carrier L1 = Carrier L & Carrier L c= Ar ) by Th2, RLVECT_2:def_6;
then A3: L1 is Linear_Combination of Af by A1, VECTSP_6:def_4;
Sum L1 = Sum L by Th5;
then x in Lin Af by A2, A3, VECTSP_7:7;
hence x in [#] (Lin Af) by STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] (Lin Af) or x in [#] (Lin Ar) )
assume x in [#] (Lin Af) ; ::_thesis: x in [#] (Lin Ar)
then x in Lin Af by STRUCT_0:def_5;
then consider L being Linear_Combination of Af such that
A4: x = Sum L by VECTSP_7:7;
reconsider L1 = L as Linear_Combination of TOP-REAL n by Th1;
( Carrier L1 = Carrier L & Carrier L c= Af ) by Th2, VECTSP_6:def_4;
then A5: L1 is Linear_Combination of Ar by A1, RLVECT_2:def_6;
Sum L1 = Sum L by Th5;
then x in Lin Ar by A4, A5, RLVECT_3:14;
hence x in [#] (Lin Ar) by STRUCT_0:def_5; ::_thesis: verum
end;
theorem Th7: :: MATRTOP2:7
for n being Nat
for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )
proof
let n be Nat; ::_thesis: for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )
set V = n -VectSp_over F_Real;
let AV be Subset of (n -VectSp_over F_Real); ::_thesis: for Ar being Subset of (TOP-REAL n) st AV = Ar holds
( AV is linearly-independent iff Ar is linearly-independent )
set T = TOP-REAL n;
let AR be Subset of (TOP-REAL n); ::_thesis: ( AV = AR implies ( AV is linearly-independent iff AR is linearly-independent ) )
assume A1: AV = AR ; ::_thesis: ( AV is linearly-independent iff AR is linearly-independent )
hereby ::_thesis: ( AR is linearly-independent implies AV is linearly-independent )
assume A2: AV is linearly-independent ; ::_thesis: AR is linearly-independent
now__::_thesis:_for_L_being_Linear_Combination_of_AR_st_Sum_L_=_0._(TOP-REAL_n)_holds_
Carrier_L_=_{}
let L be Linear_Combination of AR; ::_thesis: ( Sum L = 0. (TOP-REAL n) implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of n -VectSp_over F_Real by Th1;
A3: Carrier L1 = Carrier L by Th2;
assume Sum L = 0. (TOP-REAL n) ; ::_thesis: Carrier L = {}
then A4: 0. (n -VectSp_over F_Real) = Sum L by Lm2
.= Sum L1 by Th5 ;
Carrier L c= AR by RLVECT_2:def_6;
then L1 is Linear_Combination of AV by A1, A3, VECTSP_6:def_4;
hence Carrier L = {} by A2, A3, A4, VECTSP_7:def_1; ::_thesis: verum
end;
hence AR is linearly-independent by RLVECT_3:def_1; ::_thesis: verum
end;
assume A5: AR is linearly-independent ; ::_thesis: AV is linearly-independent
now__::_thesis:_for_L_being_Linear_Combination_of_AV_st_Sum_L_=_0._(n_-VectSp_over_F_Real)_holds_
Carrier_L_=_{}
let L be Linear_Combination of AV; ::_thesis: ( Sum L = 0. (n -VectSp_over F_Real) implies Carrier L = {} )
reconsider L1 = L as Linear_Combination of TOP-REAL n by Th1;
A6: Carrier L1 = Carrier L by Th2;
Carrier L c= AV by VECTSP_6:def_4;
then reconsider L1 = L1 as Linear_Combination of AR by A1, A6, RLVECT_2:def_6;
assume Sum L = 0. (n -VectSp_over F_Real) ; ::_thesis: Carrier L = {}
then 0. (TOP-REAL n) = Sum L by Lm2
.= Sum L1 by Th5 ;
hence Carrier L = {} by A5, A6, RLVECT_3:def_1; ::_thesis: verum
end;
hence AV is linearly-independent by VECTSP_7:def_1; ::_thesis: verum
end;
theorem Th8: :: MATRTOP2:8
for K being Field
for V being VectSp of K
for W being Subspace of V
for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W
proof
let K be Field; ::_thesis: for V being VectSp of K
for W being Subspace of V
for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W
let V be VectSp of K; ::_thesis: for W being Subspace of V
for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W
let W be Subspace of V; ::_thesis: for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W
let L be Linear_Combination of V; ::_thesis: L | the carrier of W is Linear_Combination of W
set cW = the carrier of W;
the carrier of W c= [#] V by VECTSP_4:def_2;
then L | the carrier of W is Function of the carrier of W, the carrier of K by FUNCT_2:32;
then reconsider L1 = L | the carrier of W as Element of Funcs ( the carrier of W, the carrier of K) by FUNCT_2:8;
A1: for v being Element of W st not v in (Carrier L) /\ the carrier of W holds
L1 . v = 0. K
proof
let v be Element of W; ::_thesis: ( not v in (Carrier L) /\ the carrier of W implies L1 . v = 0. K )
reconsider w = v as Element of V by VECTSP_4:10;
assume not v in (Carrier L) /\ the carrier of W ; ::_thesis: L1 . v = 0. K
then A2: not v in Carrier L by XBOOLE_0:def_4;
L . w = L1 . v by FUNCT_1:49;
hence L1 . v = 0. K by A2, VECTSP_6:2; ::_thesis: verum
end;
(Carrier L) /\ the carrier of W c= the carrier of W by XBOOLE_1:17;
hence L | the carrier of W is Linear_Combination of W by A1, VECTSP_6:def_1; ::_thesis: verum
end;
theorem :: MATRTOP2:9
for K being Field
for V being VectSp of K
for A being linearly-independent Subset of V
for L1, L2 being Linear_Combination of V st Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2 holds
L1 = L2
proof
let K be Field; ::_thesis: for V being VectSp of K
for A being linearly-independent Subset of V
for L1, L2 being Linear_Combination of V st Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2 holds
L1 = L2
let V be VectSp of K; ::_thesis: for A being linearly-independent Subset of V
for L1, L2 being Linear_Combination of V st Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2 holds
L1 = L2
let A be linearly-independent Subset of V; ::_thesis: for L1, L2 being Linear_Combination of V st Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2 holds
L1 = L2
let L1, L2 be Linear_Combination of V; ::_thesis: ( Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2 implies L1 = L2 )
assume that
A1: ( Carrier L1 c= A & Carrier L2 c= A ) and
A2: Sum L1 = Sum L2 ; ::_thesis: L1 = L2
( L1 is Linear_Combination of A & L2 is Linear_Combination of A ) by A1, VECTSP_6:def_4;
then A3: L1 - L2 is Linear_Combination of A by VECTSP_6:42;
Sum (L1 - L2) = (Sum L1) - (Sum L2) by VECTSP_6:47
.= 0. V by A2, RLVECT_1:15 ;
then Carrier (L1 - L2) = {} by A3, VECTSP_7:def_1;
then ZeroLC V = L1 - L2 by VECTSP_6:def_3
.= L1 + (- L2) by VECTSP_6:def_11
.= (- L2) + L1 by VECTSP_6:25 ;
then L1 = - (- L2) by VECTSP_6:37;
hence L1 = L2 ; ::_thesis: verum
end;
theorem :: MATRTOP2:10
for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W
proof
let V be RealLinearSpace; ::_thesis: for W being Subspace of V
for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W
let W be Subspace of V; ::_thesis: for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W
let L be Linear_Combination of V; ::_thesis: L | the carrier of W is Linear_Combination of W
set cW = the carrier of W;
the carrier of W c= [#] V by RLSUB_1:def_2;
then L | the carrier of W is Function of the carrier of W,REAL by FUNCT_2:32;
then reconsider L1 = L | the carrier of W as Element of Funcs ( the carrier of W,REAL) by FUNCT_2:8;
A1: for v being Element of W st not v in (Carrier L) /\ the carrier of W holds
L1 . v = 0
proof
let v be Element of W; ::_thesis: ( not v in (Carrier L) /\ the carrier of W implies L1 . v = 0 )
reconsider w = v as Element of V by RLSUB_1:10;
assume not v in (Carrier L) /\ the carrier of W ; ::_thesis: L1 . v = 0
then A2: not v in Carrier L by XBOOLE_0:def_4;
L . w = L1 . v by FUNCT_1:49;
hence L1 . v = 0 by A2, RLVECT_2:19; ::_thesis: verum
end;
(Carrier L) /\ the carrier of W c= the carrier of W by XBOOLE_1:17;
hence L | the carrier of W is Linear_Combination of W by A1, RLVECT_2:def_3; ::_thesis: verum
end;
theorem :: MATRTOP2:11
for X being set
for n being Nat
for U being Subspace of n -VectSp_over F_Real
for W being Subspace of TOP-REAL n st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
proof
let X be set ; ::_thesis: for n being Nat
for U being Subspace of n -VectSp_over F_Real
for W being Subspace of TOP-REAL n st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
let n be Nat; ::_thesis: for U being Subspace of n -VectSp_over F_Real
for W being Subspace of TOP-REAL n st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;
let U be Subspace of n -VectSp_over F_Real; ::_thesis: for W being Subspace of TOP-REAL n st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
let W be Subspace of TOP-REAL n; ::_thesis: ( [#] U = [#] W implies ( X is Linear_Combination of U iff X is Linear_Combination of W ) )
assume A1: [#] U = [#] W ; ::_thesis: ( X is Linear_Combination of U iff X is Linear_Combination of W )
hereby ::_thesis: ( X is Linear_Combination of W implies X is Linear_Combination of U )
assume X is Linear_Combination of U ; ::_thesis: X is Linear_Combination of W
then reconsider L = X as Linear_Combination of U ;
ex S being finite Subset of U st
for v being Element of U st not v in S holds
L . v = 0. F_Real by VECTSP_6:def_1;
hence X is Linear_Combination of W by A1, RLVECT_2:def_3; ::_thesis: verum
end;
assume X is Linear_Combination of W ; ::_thesis: X is Linear_Combination of U
then reconsider L = X as Linear_Combination of W ;
consider S being finite Subset of W such that
A2: for v being Element of W st not v in S holds
L . v = 0 by RLVECT_2:def_3;
for v being Element of U st not v in S holds
0. F_Real = L . v by A1, A2;
hence X is Linear_Combination of U by A1, VECTSP_6:def_1; ::_thesis: verum
end;
theorem :: MATRTOP2:12
for n being Nat
for U being Subspace of n -VectSp_over F_Real
for W being Subspace of TOP-REAL n
for LU being Linear_Combination of U
for LW being Linear_Combination of W st LU = LW holds
( Carrier LU = Carrier LW & Sum LU = Sum LW )
proof
let n be Nat; ::_thesis: for U being Subspace of n -VectSp_over F_Real
for W being Subspace of TOP-REAL n
for LU being Linear_Combination of U
for LW being Linear_Combination of W st LU = LW holds
( Carrier LU = Carrier LW & Sum LU = Sum LW )
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;
let U be Subspace of n -VectSp_over F_Real; ::_thesis: for W being Subspace of TOP-REAL n
for LU being Linear_Combination of U
for LW being Linear_Combination of W st LU = LW holds
( Carrier LU = Carrier LW & Sum LU = Sum LW )
let W be Subspace of TOP-REAL n; ::_thesis: for LU being Linear_Combination of U
for LW being Linear_Combination of W st LU = LW holds
( Carrier LU = Carrier LW & Sum LU = Sum LW )
let LU be Linear_Combination of U; ::_thesis: for LW being Linear_Combination of W st LU = LW holds
( Carrier LU = Carrier LW & Sum LU = Sum LW )
let LW be Linear_Combination of W; ::_thesis: ( LU = LW implies ( Carrier LU = Carrier LW & Sum LU = Sum LW ) )
assume A1: LU = LW ; ::_thesis: ( Carrier LU = Carrier LW & Sum LU = Sum LW )
reconsider LW9 = LW as Function of the carrier of W,REAL ;
defpred S1[ set , set ] means ( ( $1 in W & $2 = LW . $1 ) or ( not $1 in W & $2 = 0 ) );
A2: ( dom LU = [#] U & dom LW = [#] W ) by FUNCT_2:def_1;
A3: for x being set st x in the carrier of (TOP-REAL n) holds
ex y being set st
( y in REAL & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of (TOP-REAL n) implies ex y being set st
( y in REAL & S1[x,y] ) )
assume x in the carrier of (TOP-REAL n) ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
then reconsider x = x as VECTOR of (TOP-REAL n) ;
percases ( x in W or not x in W ) ;
supposeA4: x in W ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
then reconsider x = x as VECTOR of W by STRUCT_0:def_5;
S1[x,LW . x] by A4;
hence ex y being set st
( y in REAL & S1[x,y] ) ; ::_thesis: verum
end;
suppose not x in W ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
hence ex y being set st
( y in REAL & S1[x,y] ) ; ::_thesis: verum
end;
end;
end;
consider L being Function of the carrier of (TOP-REAL n),REAL such that
A5: for x being set st x in the carrier of (TOP-REAL n) holds
S1[x,L . x] from FUNCT_2:sch_1(A3);
A6: the carrier of W c= the carrier of (TOP-REAL n) by RLSUB_1:def_2;
then reconsider C = Carrier LW as finite Subset of (TOP-REAL n) by XBOOLE_1:1;
A7: L is Element of Funcs ( the carrier of (TOP-REAL n),REAL) by FUNCT_2:8;
now__::_thesis:_for_v_being_VECTOR_of_(TOP-REAL_n)_st_not_v_in_C_holds_
L_._v_=_0
let v be VECTOR of (TOP-REAL n); ::_thesis: ( not v in C implies L . v = 0 )
assume not v in C ; ::_thesis: L . v = 0
then ( ( S1[v,LW . v] & not v in C & v in the carrier of W ) or S1[v, 0 ] ) by STRUCT_0:def_5;
then ( ( S1[v,LW . v] & LW . v = 0 ) or S1[v, 0 ] ) by RLVECT_2:19;
hence L . v = 0 by A5; ::_thesis: verum
end;
then reconsider L = L as Linear_Combination of TOP-REAL n by A7, RLVECT_2:def_3;
reconsider L9 = L | the carrier of W as Function of the carrier of W,REAL by A6, FUNCT_2:32;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_W_holds_
LW9_._x_=_L9_._x
let x be set ; ::_thesis: ( x in the carrier of W implies LW9 . x = L9 . x )
assume A8: x in the carrier of W ; ::_thesis: LW9 . x = L9 . x
then S1[x,L . x] by A6, A5;
hence LW9 . x = L9 . x by A8, FUNCT_1:49, STRUCT_0:def_5; ::_thesis: verum
end;
then A9: LW = L9 by FUNCT_2:12;
reconsider K = L as Linear_Combination of n -VectSp_over F_Real by Th1;
now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_
x_in_the_carrier_of_W
let x be set ; ::_thesis: ( x in Carrier L implies x in the carrier of W )
assume that
A10: x in Carrier L and
A11: not x in the carrier of W ; ::_thesis: contradiction
consider v being VECTOR of (TOP-REAL n) such that
A12: x = v and
A13: L . v <> 0 by A10, RLVECT_5:3;
S1[v, 0 ] by A11, A12, STRUCT_0:def_5;
hence contradiction by A5, A13; ::_thesis: verum
end;
then A14: Carrier L c= the carrier of W by TARSKI:def_3;
then A15: ( Carrier L = Carrier LW & Sum L = Sum LW ) by A9, RLVECT_5:10;
A16: Carrier L = Carrier K by Th2;
then Sum K = Sum LU by A1, A2, A14, A9, VECTSP_9:7;
hence ( Carrier LU = Carrier LW & Sum LU = Sum LW ) by A1, A2, A9, A15, A16, Th5, VECTSP_9:7; ::_thesis: verum
end;
registration
let m be Nat;
let K be Field;
let A be Subset of (m -VectSp_over K);
cluster Lin A -> finite-dimensional ;
coherence
Lin A is finite-dimensional ;
end;
Lm4: for n, m being Nat
for M being Matrix of n,m,F_Real holds lines M c= [#] (Lin (lines M))
proof
let n, m be Nat; ::_thesis: for M being Matrix of n,m,F_Real holds lines M c= [#] (Lin (lines M))
let M be Matrix of n,m,F_Real; ::_thesis: lines M c= [#] (Lin (lines M))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lines M or x in [#] (Lin (lines M)) )
assume x in lines M ; ::_thesis: x in [#] (Lin (lines M))
then x in Lin (lines M) by VECTSP_7:8;
hence x in [#] (Lin (lines M)) by STRUCT_0:def_5; ::_thesis: verum
end;
begin
theorem :: MATRTOP2:13
for m, n being Nat
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
M is OrdBasis of Lin (lines M)
proof
let m, n be Nat; ::_thesis: for M being Matrix of n,m,F_Real st the_rank_of M = n holds
M is OrdBasis of Lin (lines M)
let M be Matrix of n,m,F_Real; ::_thesis: ( the_rank_of M = n implies M is OrdBasis of Lin (lines M) )
A1: lines M c= [#] (Lin (lines M)) by Lm4;
then reconsider L = lines M as Subset of (Lin (lines M)) ;
reconsider B = M as FinSequence of (Lin (lines M)) by A1, FINSEQ_1:def_4;
assume A2: the_rank_of M = n ; ::_thesis: M is OrdBasis of Lin (lines M)
A3: M is one-to-one by A2, MATRIX13:121;
lines M is linearly-independent by A2, MATRIX13:121;
then A4: L is linearly-independent by VECTSP_9:12;
Lin L = Lin (lines M) by VECTSP_9:17;
then L is Basis of Lin (lines M) by A4, VECTSP_7:def_3;
then B is OrdBasis of Lin (lines M) by A3, MATRLIN:def_2;
hence M is OrdBasis of Lin (lines M) ; ::_thesis: verum
end;
theorem Th14: :: MATRTOP2:14
for K being Field
for V, W being VectSp of K
for T being linear-transformation of V,W
for A being Subset of V
for L being Linear_Combination of A st T | A is one-to-one holds
T . (Sum L) = Sum (T @ L)
proof
let K be Field; ::_thesis: for V, W being VectSp of K
for T being linear-transformation of V,W
for A being Subset of V
for L being Linear_Combination of A st T | A is one-to-one holds
T . (Sum L) = Sum (T @ L)
let V, W be VectSp of K; ::_thesis: for T being linear-transformation of V,W
for A being Subset of V
for L being Linear_Combination of A st T | A is one-to-one holds
T . (Sum L) = Sum (T @ L)
let T be linear-transformation of V,W; ::_thesis: for A being Subset of V
for L being Linear_Combination of A st T | A is one-to-one holds
T . (Sum L) = Sum (T @ L)
let A be Subset of V; ::_thesis: for L being Linear_Combination of A st T | A is one-to-one holds
T . (Sum L) = Sum (T @ L)
let L be Linear_Combination of A; ::_thesis: ( T | A is one-to-one implies T . (Sum L) = Sum (T @ L) )
consider G being FinSequence of V such that
A1: G is one-to-one and
A2: rng G = Carrier L and
A3: Sum L = Sum (L (#) G) by VECTSP_6:def_6;
set H = T * G;
reconsider H = T * G as FinSequence of W ;
Carrier L c= A by VECTSP_6:def_4;
then A4: (T | A) | (Carrier L) = T | (Carrier L) by RELAT_1:74;
assume A5: T | A is one-to-one ; ::_thesis: T . (Sum L) = Sum (T @ L)
then A6: T | (Carrier L) is one-to-one by A4, FUNCT_1:52;
A7: rng H = T .: (Carrier L) by A2, RELAT_1:127
.= Carrier (T @ L) by A6, RANKNULL:39 ;
dom T = [#] V by FUNCT_2:def_1;
then H is one-to-one by A5, A4, A1, A2, FUNCT_1:52, RANKNULL:1;
then A8: Sum (T @ L) = Sum ((T @ L) (#) H) by A7, VECTSP_6:def_6;
T * (L (#) G) = (T @ L) (#) H by A6, A2, RANKNULL:38;
hence T . (Sum L) = Sum (T @ L) by A3, A8, MATRLIN:16; ::_thesis: verum
end;
Lm5: for m, n being Nat
for f being b2 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st card (lines M) = 1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) ) )
proof
let m, n be Nat; ::_thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st card (lines M) = 1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) ) )
let f be n -element real-valued FinSequence; ::_thesis: for M being Matrix of n,m,F_Real st card (lines M) = 1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) ) )
let M be Matrix of n,m,F_Real; ::_thesis: ( card (lines M) = 1 implies ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) ) ) )
assume A1: card (lines M) = 1 ; ::_thesis: ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) ) )
percases ( n <> 0 or n = 0 ) ;
supposeA2: n <> 0 ; ::_thesis: ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) ) )
deffunc H1( set ) -> Element of the carrier of F_Real = 0. F_Real;
A3: len M = n by A2, MATRIX13:1;
reconsider Sf = Sum f as Element of F_Real by XREAL_0:def_1;
set Mf = (Mx2Tran M) . f;
A4: len ((Mx2Tran M) . f) = m by CARD_1:def_7;
A5: len f = n by CARD_1:def_7;
set V = m -VectSp_over F_Real;
consider x being set such that
A6: lines M = {x} by A1, CARD_2:42;
x in lines M by A6, TARSKI:def_1;
then consider j being set such that
A7: j in dom M and
A8: M . j = x by FUNCT_1:def_3;
reconsider j = j as Nat by A7;
A9: width M = m by A2, MATRIX13:1;
then reconsider LMj = Line (M,j) as Element of (m -VectSp_over F_Real) by MATRIX13:102;
consider L being Function of the carrier of (m -VectSp_over F_Real), the carrier of F_Real such that
A10: L . LMj = 1. F_Real and
A11: for z being Element of (m -VectSp_over F_Real) st z <> LMj holds
L . z = H1(z) from FUNCT_2:sch_6();
reconsider L = L as Element of Funcs ( the carrier of (m -VectSp_over F_Real), the carrier of F_Real) by FUNCT_2:8;
A12: x = Line (M,j) by A7, A8, MATRIX_2:16;
A13: now__::_thesis:_for_z_being_Vector_of_(m_-VectSp_over_F_Real)_st_not_z_in_lines_M_holds_
L_._z_=_0._F_Real
let z be Vector of (m -VectSp_over F_Real); ::_thesis: ( not z in lines M implies L . z = 0. F_Real )
assume A14: not z in lines M ; ::_thesis: L . z = 0. F_Real
z <> LMj by A6, A12, A14, TARSKI:def_1;
hence L . z = 0. F_Real by A11; ::_thesis: verum
end;
A15: len (Sf * (Line (M,j))) = m by A9, CARD_1:def_7;
A16: now__::_thesis:_for_w_being_Nat_st_1_<=_w_&_w_<=_m_holds_
((Mx2Tran_M)_._f)_._w_=_(Sf_*_(Line_(M,j)))_._w
len (@ f) = n by CARD_1:def_7;
then reconsider F = @ f as Element of n -tuples_on the carrier of F_Real by FINSEQ_2:92;
let w be Nat; ::_thesis: ( 1 <= w & w <= m implies ((Mx2Tran M) . f) . w = (Sf * (Line (M,j))) . w )
set Mjw = M * (j,w);
A17: n in NAT by ORDINAL1:def_12;
assume A18: ( 1 <= w & w <= m ) ; ::_thesis: ((Mx2Tran M) . f) . w = (Sf * (Line (M,j))) . w
then A19: w in dom (Sf * (Line (M,j))) by A15, FINSEQ_3:25;
A20: w in Seg m by A18, FINSEQ_1:1;
then A21: (Line (M,j)) . w = M * (j,w) by A9, MATRIX_1:def_7;
A22: now__::_thesis:_for_z_being_Nat_st_1_<=_z_&_z_<=_n_holds_
(Col_(M,w))_._z_=_(n_|->_(M_*_(j,w)))_._z
let z be Nat; ::_thesis: ( 1 <= z & z <= n implies (Col (M,w)) . z = (n |-> (M * (j,w))) . z )
assume A23: ( 1 <= z & z <= n ) ; ::_thesis: (Col (M,w)) . z = (n |-> (M * (j,w))) . z
then A24: z in Seg n by FINSEQ_1:1;
then A25: Line (M,z) in lines M by MATRIX13:103;
z in dom M by A3, A23, FINSEQ_3:25;
hence (Col (M,w)) . z = M * (z,w) by MATRIX_1:def_8
.= (Line (M,z)) . w by A9, A20, MATRIX_1:def_7
.= M * (j,w) by A6, A12, A21, A25, TARSKI:def_1
.= (n |-> (M * (j,w))) . z by A24, FINSEQ_2:57 ;
::_thesis: verum
end;
( len (Col (M,w)) = n & len (n |-> (M * (j,w))) = n ) by A3, CARD_1:def_7;
then A26: Col (M,w) = n |-> (M * (j,w)) by A22, FINSEQ_1:14;
thus ((Mx2Tran M) . f) . w = (@ f) "*" (Col (M,w)) by A2, A18, MATRTOP1:18
.= Sum (mlt ((@ f),(Col (M,w)))) by FVSUM_1:def_9
.= Sum ((M * (j,w)) * F) by A26, A17, FVSUM_1:66
.= (M * (j,w)) * (Sum (@ f)) by FVSUM_1:73
.= (M * (j,w)) * Sf by MATRPROB:36
.= (Sf * (Line (M,j))) . w by A19, A21, FVSUM_1:50 ; ::_thesis: verum
end;
reconsider L = L as Linear_Combination of m -VectSp_over F_Real by A13, VECTSP_6:def_1;
Carrier L c= {LMj}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier L or x in {LMj} )
assume A27: x in Carrier L ; ::_thesis: x in {LMj}
L . x <> 0. F_Real by A27, VECTSP_6:2;
then x = LMj by A11, A27;
hence x in {LMj} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider L = L as Linear_Combination of lines M by A6, A12, VECTSP_6:def_4;
A28: Sum L = (1. F_Real) * LMj by A6, A12, A10, VECTSP_6:17
.= LMj by VECTSP_1:def_17 ;
reconsider SfL = Sf * L as Linear_Combination of lines M by VECTSP_6:31;
take SfL ; ::_thesis: ( Sum SfL = (Mx2Tran M) . f & ( for k being Nat st k in Seg n holds
( SfL . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) ) )
Sum SfL = Sf * (Sum L) by VECTSP_6:45
.= Sf * (Line (M,j)) by A9, A28, MATRIX13:102 ;
hence Sum SfL = (Mx2Tran M) . f by A15, A4, A16, FINSEQ_1:14; ::_thesis: for k being Nat st k in Seg n holds
( SfL . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f )
let w be Nat; ::_thesis: ( w in Seg n implies ( SfL . (Line (M,w)) = Sum f & M " {(Line (M,w))} = dom f ) )
assume A29: w in Seg n ; ::_thesis: ( SfL . (Line (M,w)) = Sum f & M " {(Line (M,w))} = dom f )
Line (M,w) in lines M by A29, MATRIX13:103;
then A30: Line (M,w) = LMj by A6, A12, TARSKI:def_1;
thus Sum f = Sf * (1. F_Real)
.= SfL . (Line (M,w)) by A10, A30, VECTSP_6:def_9 ; ::_thesis: M " {(Line (M,w))} = dom f
thus M " {(Line (M,w))} = dom M by A6, A12, A30, RELAT_1:134
.= dom f by A3, A5, FINSEQ_3:29 ; ::_thesis: verum
end;
supposeA31: n = 0 ; ::_thesis: ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) ) )
reconsider L = ZeroLC (m -VectSp_over F_Real) as Linear_Combination of lines M by VECTSP_6:5;
take L ; ::_thesis: ( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) ) )
thus Sum L = 0. (m -VectSp_over F_Real) by VECTSP_6:15
.= 0. (TOP-REAL m) by Lm2
.= (Mx2Tran M) . f by A31, MATRTOP1:def_3 ; ::_thesis: for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f )
thus for k being Nat st k in Seg n holds
( L . (Line (M,k)) = Sum f & M " {(Line (M,k))} = dom f ) by A31; ::_thesis: verum
end;
end;
end;
theorem Th15: :: MATRTOP2:15
for m, n being Nat
for f being b2 -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
proof
let m, n be Nat; ::_thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
let f be n -element real-valued FinSequence; ::_thesis: for M being Matrix of n,m,F_Real
for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
let M be Matrix of n,m,F_Real; ::_thesis: for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
defpred S1[ Nat] means for n, m being Nat
for M being Matrix of n,m,F_Real
for f being b1 -element real-valued FinSequence
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = $1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) );
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: S1[i] ; ::_thesis: S1[i + 1]
let n, m be Nat; ::_thesis: for M being Matrix of n,m,F_Real
for f being n -element real-valued FinSequence
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = i + 1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
let M be Matrix of n,m,F_Real; ::_thesis: for f being n -element real-valued FinSequence
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = i + 1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
let f be n -element real-valued FinSequence; ::_thesis: for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = i + 1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
let S be Subset of (Seg n); ::_thesis: ( ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = i + 1 implies ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) ) )
assume that
A3: ( n = 0 implies m = 0 ) and
A4: M | S is one-to-one and
A5: rng (M | S) = lines M and
A6: card (lines M) = i + 1 ; ::_thesis: ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
A7: len M = n by A3, MATRIX13:1;
A8: width M = m by A3, MATRIX13:1;
percases ( i = 0 or i > 0 ) ;
suppose i = 0 ; ::_thesis: ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
then consider L being Linear_Combination of lines M such that
A9: Sum L = (Mx2Tran M) . f and
A10: for i being Nat st i in Seg n holds
( L . (Line (M,i)) = Sum f & M " {(Line (M,i))} = dom f ) by A6, Lm5;
take L ; ::_thesis: ( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
thus Sum L = (Mx2Tran M) . f by A9; ::_thesis: for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))})))
let w be Nat; ::_thesis: ( w in S implies L . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))}))) )
assume A11: w in S ; ::_thesis: L . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))})))
M " {(Line (M,w))} = dom f by A10, A11;
then A12: f | (M " {(Line (M,w))}) = f by RELAT_1:69;
L . (Line (M,w)) = Sum f by A10, A11;
hence Sum (Seq (f | (M " {(Line (M,w))}))) = L . (Line (M,w)) by A12, FINSEQ_3:116; ::_thesis: verum
end;
supposeA13: i > 0 ; ::_thesis: ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
lines M <> {} by A6;
then consider x being set such that
A14: x in lines M by XBOOLE_0:def_1;
reconsider LM = {x} as Subset of (lines M) by A14, ZFMISC_1:31;
set n1 = n -' (card (M " LM));
reconsider ML1 = M - LM as Matrix of n -' (card (M " LM)),m,F_Real by MATRTOP1:14;
A15: LM ` = (lines M) \ LM by SUBSET_1:def_4;
then A16: LM misses LM ` by XBOOLE_1:79;
LM \/ (LM `) = [#] (lines M) by SUBSET_1:10
.= lines M by SUBSET_1:def_3 ;
then A17: (M " LM) \/ (M " (LM `)) = M " (rng M) by RELAT_1:140
.= dom M by RELAT_1:134 ;
A18: len ML1 = (len M) - (card (M " LM)) by FINSEQ_3:59;
then A19: n - (card (M " LM)) = n -' (card (M " LM)) by A7, XREAL_1:49, XREAL_1:233;
LM misses LM ` by A15, XBOOLE_1:79;
then A20: (card (M " LM)) + (card (M " (LM `))) = card (dom M) by A17, CARD_2:40, FUNCT_1:71
.= n by A7, CARD_1:62 ;
A21: n -' (card (M " LM)) <> 0
proof
assume n -' (card (M " LM)) = 0 ; ::_thesis: contradiction
then M " (LM `) = {} by A7, A18, A20, XREAL_1:49, XREAL_1:233;
then LM ` misses rng M by RELAT_1:138;
then {} = (lines M) \ LM by A15, XBOOLE_1:67;
then lines M c= LM by XBOOLE_1:37;
then lines M = LM by XBOOLE_0:def_10;
then i + 1 = 1 by A6, CARD_2:42;
hence contradiction by A13; ::_thesis: verum
end;
set n2 = n -' (card (M " (LM `)));
reconsider ML2 = M - (LM `) as Matrix of n -' (card (M " (LM `))),m,F_Real by MATRTOP1:14;
rng ML2 = (rng M) \ (LM `) by FINSEQ_3:65;
then A22: rng ML2 = (LM `) ` by SUBSET_1:def_4;
reconsider FR = F_Real as Field ;
set Mf = (Mx2Tran M) . f;
set V = m -VectSp_over F_Real;
len f = n by CARD_1:def_7;
then A23: dom f = Seg n by FINSEQ_1:def_3;
consider j being set such that
A24: j in dom (M | S) and
A25: (M | S) . j = x by A5, A14, FUNCT_1:def_3;
A26: x = M . j by A24, A25, FUNCT_1:47;
A27: j in dom M by A24, RELAT_1:57;
A28: j in S by A24;
reconsider j = j as Nat by A24;
A29: x = Line (M,j) by A27, A26, MATRIX_2:16;
A30: len ML2 = (len M) - (card (M " (LM `))) by FINSEQ_3:59;
then A31: n - (card (M " (LM `))) = n -' (card (M " (LM `))) by A7, XREAL_1:49, XREAL_1:233;
A32: rng ML1 = (rng M) \ LM by FINSEQ_3:65;
then A33: rng ML1 = LM ` by SUBSET_1:def_4;
reconsider LMj = Line (M,j) as Element of (m -VectSp_over F_Real) by A8, MATRIX13:102;
A34: card (rng ML1) = (card (rng M)) - (card LM) by A32, CARD_2:44
.= (i + 1) - 1 by A6, CARD_2:42 ;
(LM `) ` = LM ;
then consider P being Permutation of (dom M) such that
A35: (M - LM) ^ (M - (LM `)) = M * P by FINSEQ_3:115;
dom M = Seg n by A7, FINSEQ_1:def_3;
then reconsider p = P as Permutation of (Seg n) ;
A36: (M | S) * P = (M | S) * (p | (dom p))
.= (M * p) | ((dom p) /\ (p " S)) by FUNCT_1:100
.= (M * p) | (p " S) by RELAT_1:132, XBOOLE_1:28 ;
reconsider pp = P as one-to-one Function ;
len (M * p) = n by MATRIX_1:def_2;
then A37: dom (M * p) = Seg n by FINSEQ_1:def_3;
set ppj = (pp ") . j;
A38: rng p = Seg n by FUNCT_2:def_3;
then A39: ( p " S = (pp ") .: S & dom (pp ") = Seg n ) by FUNCT_1:33, FUNCT_1:85;
then A40: (pp ") . j in p " S by A28, FUNCT_1:def_6;
A41: p . ((pp ") . j) = j by A28, A38, FUNCT_1:35;
A42: not (pp ") . j in dom ML1
proof
assume A43: (pp ") . j in dom ML1 ; ::_thesis: contradiction
(M * P) . ((pp ") . j) = M . j by A40, A41, A37, FUNCT_1:12;
then (M * P) . ((pp ") . j) = LMj by A27, MATRIX_2:16;
then ML1 . ((pp ") . j) = LMj by A35, A43, FINSEQ_1:def_7;
then A44: ML1 . ((pp ") . j) in LM by A29, TARSKI:def_1;
ML1 . ((pp ") . j) in LM ` by A33, A43, FUNCT_1:def_3;
hence contradiction by A16, A44, XBOOLE_0:3; ::_thesis: verum
end;
set pSj = (p " S) \ {((pp ") . j)};
dom M = Seg n by A7, FINSEQ_1:def_3;
then A45: dom (M | S) = S by RELAT_1:62;
A46: (p " S) \ {((pp ") . j)} c= dom ML1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (p " S) \ {((pp ") . j)} or y in dom ML1 )
assume A47: y in (p " S) \ {((pp ") . j)} ; ::_thesis: y in dom ML1
then reconsider Y = y as Nat ;
A48: (M * p) . y = M . (p . y) by A37, A47, FUNCT_1:12;
not y in {((pp ") . j)} by A47, XBOOLE_0:def_5;
then A49: y <> (pp ") . j by TARSKI:def_1;
A50: (pp ") . j in dom P by A40, FUNCT_1:def_7;
A51: y in p " S by A47, XBOOLE_0:def_5;
then A52: p . y in dom (M | S) by A45, FUNCT_1:def_7;
y in dom P by A51, FUNCT_1:def_7;
then p . y <> j by A41, A49, A50, FUNCT_1:def_4;
then (M | S) . (p . y) <> (M | S) . j by A4, A24, A52, FUNCT_1:def_4;
then (M * p) . y <> LMj by A25, A29, A48, A52, FUNCT_1:47;
then A53: not (M * p) . y in LM by A29, TARSKI:def_1;
assume not y in dom ML1 ; ::_thesis: contradiction
then consider w being Nat such that
A54: w in dom ML2 and
A55: Y = (len ML1) + w by A35, A37, A47, FINSEQ_1:25;
(M * p) . Y = ML2 . w by A35, A54, A55, FINSEQ_1:def_7;
hence contradiction by A22, A53, A54, FUNCT_1:def_3; ::_thesis: verum
end;
then ( (M * p) | ((p " S) \ {((pp ") . j)}) = ((M * p) | (p " S)) | ((p " S) \ {((pp ") . j)}) & (M * p) | ((p " S) \ {((pp ") . j)}) = ML1 | ((p " S) \ {((pp ") . j)}) ) by A35, FINSEQ_6:11, RELAT_1:74, XBOOLE_1:36;
then A56: ML1 | ((p " S) \ {((pp ") . j)}) is one-to-one by A4, A36, FUNCT_1:52;
( dom p = Seg n & p . ((pp ") . j) = j ) by A28, A38, FUNCT_1:35, FUNCT_2:52;
then A57: (pp ") . j in dom ((M | S) * p) by A24, A40, FUNCT_1:11;
then ((M | S) * p) . ((pp ") . j) = LMj by A25, A29, A41, FUNCT_1:12;
then A58: LM = Im (((M | S) * p),((pp ") . j)) by A29, A57, FUNCT_1:59
.= ((M * p) | (p " S)) .: {((pp ") . j)} by A36, RELAT_1:def_16 ;
rng M = rng ((M * p) | (p " S)) by A5, A36, A38, A45, RELAT_1:28
.= (M * p) .: (p " S) by RELAT_1:115
.= ((M * p) | (p " S)) .: (p " S) by RELAT_1:129 ;
then A59: rng ML1 = ((M * p) | (p " S)) .: ((p " S) \ {((pp ") . j)}) by A4, A36, A32, A58, FUNCT_1:64
.= rng (((M * p) | (p " S)) | ((p " S) \ {((pp ") . j)})) by RELAT_1:115
.= rng ((M * p) | ((p " S) \ {((pp ") . j)})) by RELAT_1:74, XBOOLE_1:36
.= rng (ML1 | ((p " S) \ {((pp ") . j)})) by A35, A46, FINSEQ_6:11 ;
reconsider fp = f * p as n -element FinSequence of REAL by MATRTOP1:21;
A60: (n -' (card (M " LM))) + (n -' (card (M " (LM `)))) = len (ML1 ^ ML2) by MATRIX_1:def_2
.= len (M * p) by A35
.= n by MATRIX_1:def_2 ;
len fp = n by CARD_1:def_7;
then consider fp1, fp2 being FinSequence of REAL such that
A61: len fp1 = n -' (card (M " LM)) and
A62: len fp2 = n -' (card (M " (LM `))) and
A63: fp = fp1 ^ fp2 by A60, FINSEQ_2:23;
A64: fp2 is n -' (card (M " (LM `))) -element by A62, CARD_1:def_7;
then A65: len ((Mx2Tran ML2) . fp2) = m by CARD_1:def_7;
card LM = 1 by CARD_2:42;
then consider L2 being Linear_Combination of lines ML2 such that
A66: Sum L2 = (Mx2Tran ML2) . fp2 and
A67: for i being Nat st i in Seg (n -' (card (M " (LM `)))) holds
( L2 . (Line (ML2,i)) = Sum fp2 & ML2 " {(Line (ML2,i))} = dom fp2 ) by A64, A22, Lm5;
A68: fp1 is n -' (card (M " LM)) -element by A61, CARD_1:def_7;
then len ((Mx2Tran ML1) . fp1) = m by CARD_1:def_7;
then reconsider Mf1 = @ ((Mx2Tran ML1) . fp1), Mf2 = @ ((Mx2Tran ML2) . fp2) as Element of m -tuples_on the carrier of F_Real by A65, FINSEQ_2:92;
A69: Carrier L2 c= lines ML2 by VECTSP_6:def_4;
len ML1 = n -' (card (M " LM)) by A7, A18, XREAL_1:49, XREAL_1:233;
then (p " S) \ {((pp ") . j)} is Subset of (Seg (n -' (card (M " LM)))) by A46, FINSEQ_1:def_3;
then consider L1 being Linear_Combination of lines ML1 such that
A70: Sum L1 = (Mx2Tran ML1) . fp1 and
A71: for i being Nat st i in (p " S) \ {((pp ") . j)} holds
L1 . (Line (ML1,i)) = Sum (Seq (fp1 | (ML1 " {(Line (ML1,i))}))) by A2, A68, A21, A56, A59, A34;
A72: Carrier L1 c= lines ML1 by VECTSP_6:def_4;
(rng ML1) \/ (rng ML2) = [#] (lines M) by A22, A33, SUBSET_1:10
.= lines M by SUBSET_1:def_3 ;
then ( L1 is Linear_Combination of lines M & L2 is Linear_Combination of lines M ) by VECTSP_6:4, XBOOLE_1:7;
then reconsider L12 = L1 + L2 as Linear_Combination of lines M by VECTSP_6:24;
take L12 ; ::_thesis: ( Sum L12 = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L12 . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
thus (Mx2Tran M) . f = (Mx2Tran (ML1 ^ ML2)) . (fp1 ^ fp2) by A35, A60, A63, MATRTOP1:21
.= ((Mx2Tran ML1) . fp1) + ((Mx2Tran ML2) . fp2) by A68, A64, MATRTOP1:36
.= Mf1 + Mf2 by MATRTOP1:1
.= (Sum L1) + (Sum L2) by A70, A66, MATRIX13:102
.= Sum L12 by VECTSP_6:44 ; ::_thesis: for i being Nat st i in S holds
L12 . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))})))
let w be Nat; ::_thesis: ( w in S implies L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))}))) )
assume A73: w in S ; ::_thesis: L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))})))
Line (M,w) in lines M by A73, MATRIX13:103;
then reconsider LMw = Line (M,w) as Element of (m -VectSp_over F_Real) ;
p " (M " {LMw}) = (M * p) " {LMw} by RELAT_1:146;
then A74: Sum (Seq (f | (M " {LMw}))) = Sum (Seq (fp | ((M * p) " {LMw}))) by A23, MATRTOP1:10
.= Sum ((Seq (fp1 | (ML1 " {LMw}))) ^ (Seq (fp2 | (ML2 " {LMw})))) by A7, A35, A61, A62, A63, A18, A30, A19, A31, MATRTOP1:13
.= (Sum (Seq (fp1 | (ML1 " {LMw})))) + (Sum (Seq (fp2 | (ML2 " {LMw})))) by RVSUM_1:75 ;
set ppw = (pp ") . w;
A75: (pp ") . w in p " S by A39, A73, FUNCT_1:def_6;
p . ((pp ") . w) = w by A38, A73, FUNCT_1:35;
then A76: (M * P) . ((pp ") . w) = M . w by A37, A75, FUNCT_1:12;
reconsider ppw = (pp ") . w as Nat by A75;
A77: M . w = LMw by A73, MATRIX_2:8;
reconsider L1w = L1 . LMw, L2w = L2 . LMw as Element of FR ;
A78: L12 . LMw = L1w + L2w by VECTSP_6:22;
percases ( ppw in dom ML1 or ex z being Nat st
( z in dom ML2 & ppw = (len ML1) + z ) ) by A35, A37, A75, FINSEQ_1:25;
supposeA79: ppw in dom ML1 ; ::_thesis: L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))})))
then A80: ML1 . ppw = LMw by A35, A76, A77, FINSEQ_1:def_7;
then A81: LMw in rng ML1 by A79, FUNCT_1:def_3;
then not LMw in Carrier L2 by A22, A33, A69, A16, XBOOLE_0:3;
then A82: L2 . LMw = 0. F_Real by VECTSP_6:2;
not LMw in rng ML2 by A22, A33, A16, A81, XBOOLE_0:3;
then {LMw} misses rng ML2 by ZFMISC_1:50;
then ML2 " {LMw} = {} by RELAT_1:138;
then A83: Sum (Seq (fp2 | (ML2 " {LMw}))) = 0 by RVSUM_1:72;
( Line (ML1,ppw) = ML1 . ppw & ppw in (p " S) \ {((pp ") . j)} ) by A75, A42, A79, MATRIX_2:16, ZFMISC_1:56;
then L1 . LMw = Sum (Seq (fp1 | (ML1 " {LMw}))) by A71, A80;
hence L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))}))) by A74, A78, A82, A83, RLVECT_1:def_4; ::_thesis: verum
end;
suppose ex z being Nat st
( z in dom ML2 & ppw = (len ML1) + z ) ; ::_thesis: L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))})))
then consider z being Nat such that
A84: z in dom ML2 and
A85: ppw = (len ML1) + z ;
A86: ML2 . z = LMw by A35, A76, A77, A84, A85, FINSEQ_1:def_7;
then A87: LMw in rng ML2 by A84, FUNCT_1:def_3;
then not LMw in Carrier L1 by A22, A33, A72, A16, XBOOLE_0:3;
then A88: L1 . LMw = 0. F_Real by VECTSP_6:2;
not LMw in LM ` by A22, A16, A87, XBOOLE_0:3;
then {LMw} misses rng ML1 by A33, ZFMISC_1:50;
then ML1 " {LMw} = {} by RELAT_1:138;
then A89: Seq (fp1 | (ML1 " {LMw})) = <*> REAL ;
L1w + L2w = L2w + L1w by RLVECT_1:def_2;
then A90: L12 . LMw = L2 . LMw by A78, A88, RLVECT_1:def_4;
A91: dom ML2 = Seg (n -' (card (M " (LM `)))) by A7, A30, A31, FINSEQ_1:def_3;
A92: ML2 . z = Line (ML2,z) by A84, MATRIX_2:16;
then ML2 " {LMw} = dom fp2 by A67, A84, A86, A91;
then A93: fp2 | (ML2 " {LMw}) = fp2 by RELAT_1:69;
L2 . LMw = Sum fp2 by A67, A84, A86, A92, A91;
hence L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))}))) by A74, A90, A89, A93, FINSEQ_3:116, RVSUM_1:72; ::_thesis: verum
end;
end;
end;
end;
end;
A94: S1[ 0 ]
proof
let n, m be Nat; ::_thesis: for M being Matrix of n,m,F_Real
for f being n -element real-valued FinSequence
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = 0 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
let M be Matrix of n,m,F_Real; ::_thesis: for f being n -element real-valued FinSequence
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = 0 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
let f be n -element real-valued FinSequence; ::_thesis: for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = 0 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
let S be Subset of (Seg n); ::_thesis: ( ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = 0 implies ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) ) )
assume that
A95: ( n = 0 implies m = 0 ) and
M | S is one-to-one and
rng (M | S) = lines M and
A96: card (lines M) = 0 ; ::_thesis: ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
reconsider L = ZeroLC (m -VectSp_over F_Real) as Linear_Combination of lines M by VECTSP_6:5;
take L ; ::_thesis: ( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
A97: Sum L = 0. (m -VectSp_over F_Real) by VECTSP_6:15
.= 0. (TOP-REAL m) by Lm2 ;
A98: ( len M = n & M = {} ) by A95, A96, MATRIX13:1;
then 0. (TOP-REAL m) = {} by A95;
hence Sum L = (Mx2Tran M) . f by A95, A98, A97; ::_thesis: for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))})))
let i be Nat; ::_thesis: ( i in S implies L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) )
thus ( i in S implies L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) by A98; ::_thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch_2(A94, A1);
then A99: S1[ card (lines M)] ;
percases ( n <> 0 or n = 0 ) ;
suppose n <> 0 ; ::_thesis: for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
hence for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) ) by A99; ::_thesis: verum
end;
supposeA100: n = 0 ; ::_thesis: for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
let S be Subset of (Seg n); ::_thesis: ( M | S is one-to-one & rng (M | S) = lines M implies ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) ) )
assume ( M | S is one-to-one & rng (M | S) = lines M ) ; ::_thesis: ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
reconsider L = ZeroLC (m -VectSp_over F_Real) as Linear_Combination of lines M by VECTSP_6:5;
take L ; ::_thesis: ( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
thus Sum L = 0. (m -VectSp_over F_Real) by VECTSP_6:15
.= 0. (TOP-REAL m) by Lm2
.= (Mx2Tran M) . f by A100, MATRTOP1:def_3 ; ::_thesis: for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))})))
thus for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) by A100; ::_thesis: verum
end;
end;
end;
theorem Th16: :: MATRTOP2:16
for n, m being Nat
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real st M is without_repeated_line holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) )
proof
let n, m be Nat; ::_thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real st M is without_repeated_line holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) )
let f be n -element real-valued FinSequence; ::_thesis: for M being Matrix of n,m,F_Real st M is without_repeated_line holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) )
let M be Matrix of n,m,F_Real; ::_thesis: ( M is without_repeated_line implies ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) ) )
assume A1: M is without_repeated_line ; ::_thesis: ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) )
A2: len M = n by MATRIX_1:def_2;
then dom M c= Seg n by FINSEQ_1:def_3;
then reconsider D = dom M as Subset of (Seg n) ;
len f = n by CARD_1:def_7;
then A3: dom f = dom M by A2, FINSEQ_3:29;
M | (dom M) = M ;
then consider L being Linear_Combination of lines M such that
A4: Sum L = (Mx2Tran M) . f and
A5: for i being Nat st i in D holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) by A1, Th15;
take L ; ::_thesis: ( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k ) )
thus Sum L = (Mx2Tran M) . f by A4; ::_thesis: for k being Nat st k in dom f holds
L . (Line (M,k)) = f . k
let i be Nat; ::_thesis: ( i in dom f implies L . (Line (M,i)) = f . i )
assume A6: i in dom f ; ::_thesis: L . (Line (M,i)) = f . i
i >= 1 by A6, FINSEQ_3:25;
then A7: Sgm {i} = <*i*> by FINSEQ_3:44;
set LM = Line (M,i);
A8: Line (M,i) in {(Line (M,i))} by TARSKI:def_1;
dom M = Seg n by A2, FINSEQ_1:def_3;
then Line (M,i) in lines M by A3, A6, MATRIX13:103;
then consider x being set such that
A9: M " {(Line (M,i))} = {x} by A1, FUNCT_1:74;
A10: dom (f | {i}) = (dom f) /\ {i} by RELAT_1:61;
{i} c= dom f by A6, ZFMISC_1:31;
then A11: dom (f | {i}) = {i} by A10, XBOOLE_1:28;
then i in dom (f | {i}) by TARSKI:def_1;
then A12: (f | {i}) . i = f . i by FUNCT_1:47;
rng <*i*> = {i} by FINSEQ_1:38;
then A13: <*i*> is FinSequence of {i} by FINSEQ_1:def_4;
( rng (f | {i}) <> {} & f | {i} is Function of {i},(rng (f | {i})) ) by A11, FUNCT_2:1, RELAT_1:42;
then Seq (f | {i}) = <*(f . i)*> by A11, A7, A13, A12, FINSEQ_2:35;
then A14: Sum (Seq (f | {i})) = f . i by RVSUM_1:73;
M . i = Line (M,i) by A3, A6, MATRIX_2:16;
then i in M " {(Line (M,i))} by A3, A6, A8, FUNCT_1:def_7;
then f | (M " {(Line (M,i))}) = f | {i} by A9, TARSKI:def_1;
hence L . (Line (M,i)) = f . i by A5, A3, A6, A14; ::_thesis: verum
end;
theorem :: MATRTOP2:17
for n, m being Nat
for f being b1 -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for B being OrdBasis of Lin (lines M) st B = M holds
for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f
proof
let n, m be Nat; ::_thesis: for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for B being OrdBasis of Lin (lines M) st B = M holds
for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f
let f be n -element real-valued FinSequence; ::_thesis: for M being Matrix of n,m,F_Real
for B being OrdBasis of Lin (lines M) st B = M holds
for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f
let M be Matrix of n,m,F_Real; ::_thesis: for B being OrdBasis of Lin (lines M) st B = M holds
for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f
set LM = lines M;
let B be OrdBasis of Lin (lines M); ::_thesis: ( B = M implies for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f )
assume A1: B = M ; ::_thesis: for Mf being Element of (Lin (lines M)) st Mf = (Mx2Tran M) . f holds
Mf |-- B = f
A2: B is one-to-one by MATRLIN:def_2;
let Mf be Element of (Lin (lines M)); ::_thesis: ( Mf = (Mx2Tran M) . f implies Mf |-- B = f )
assume A3: Mf = (Mx2Tran M) . f ; ::_thesis: Mf |-- B = f
consider L being Linear_Combination of lines M such that
A4: Sum L = Mf and
A5: for i being Nat st i in dom f holds
L . (Line (M,i)) = f . i by A1, A3, A2, Th16;
reconsider L1 = L | the carrier of (Lin (lines M)) as Linear_Combination of Lin (lines M) by Th8;
A6: len M = n by MATRIX_1:def_2;
A7: len f = n by CARD_1:def_7;
A8: lines M c= [#] (Lin (lines M)) by Lm4;
A9: now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_n_holds_
(@_f)_/._k_=_L1_._(B_/._k)
let k be Nat; ::_thesis: ( 1 <= k & k <= n implies (@ f) /. k = L1 . (B /. k) )
assume A10: ( 1 <= k & k <= n ) ; ::_thesis: (@ f) /. k = L1 . (B /. k)
then k in Seg n by FINSEQ_1:1;
then A11: M . k = Line (M,k) by MATRIX_2:8;
A12: k in dom M by A6, A10, FINSEQ_3:25;
then A13: B /. k = M . k by A1, PARTFUN1:def_6;
M . k in lines M by A12, FUNCT_1:def_3;
then A14: L . (M . k) = L1 . (M . k) by A8, FUNCT_1:49;
A15: k in dom f by A7, A10, FINSEQ_3:25;
then f . k = (@ f) /. k by PARTFUN1:def_6;
hence (@ f) /. k = L1 . (B /. k) by A5, A15, A13, A11, A14; ::_thesis: verum
end;
A16: Carrier L c= lines M by VECTSP_6:def_4;
then Carrier L c= [#] (Lin (lines M)) by A8, XBOOLE_1:1;
then ( Carrier L = Carrier L1 & Sum L1 = Sum L ) by VECTSP_9:7;
hence Mf |-- B = f by A1, A4, A6, A7, A16, A9, MATRLIN:def_7; ::_thesis: verum
end;
theorem Th18: :: MATRTOP2:18
for n, m being Nat
for M being Matrix of n,m,F_Real holds rng (Mx2Tran M) = [#] (Lin (lines M))
proof
let n, m be Nat; ::_thesis: for M being Matrix of n,m,F_Real holds rng (Mx2Tran M) = [#] (Lin (lines M))
let M be Matrix of n,m,F_Real; ::_thesis: rng (Mx2Tran M) = [#] (Lin (lines M))
consider X being set such that
A1: X c= dom M and
A2: lines M = rng (M | X) and
A3: M | X is one-to-one by MATRTOP1:6;
set V = m -VectSp_over F_Real;
set TM = Mx2Tran M;
A4: len M = n by MATRIX_1:def_2;
then reconsider X = X as Subset of (Seg n) by A1, FINSEQ_1:def_3;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: [#] (Lin (lines M)) c= rng (Mx2Tran M)
let y be set ; ::_thesis: ( y in rng (Mx2Tran M) implies y in [#] (Lin (lines M)) )
assume y in rng (Mx2Tran M) ; ::_thesis: y in [#] (Lin (lines M))
then consider x being set such that
A5: x in dom (Mx2Tran M) and
A6: (Mx2Tran M) . x = y by FUNCT_1:def_3;
reconsider x = x as Element of (TOP-REAL n) by A5;
consider L being Linear_Combination of lines M such that
A7: Sum L = y and
for i being Nat st i in X holds
L . (Line (M,i)) = Sum (Seq (x | (M " {(Line (M,i))}))) by A2, A3, A6, Th15;
Sum L in Lin (lines M) by VECTSP_7:7;
hence y in [#] (Lin (lines M)) by A7, STRUCT_0:def_5; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [#] (Lin (lines M)) or y in rng (Mx2Tran M) )
assume y in [#] (Lin (lines M)) ; ::_thesis: y in rng (Mx2Tran M)
then y in Lin (lines M) by STRUCT_0:def_5;
then consider L being Linear_Combination of lines M such that
A8: y = Sum L by VECTSP_7:7;
defpred S1[ set , set ] means ( ( $1 in X implies $2 = L . (M . $1) ) & ( not $1 in X implies $2 = 0 ) );
A9: for i being Nat st i in Seg n holds
ex x being set st S1[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg n implies ex x being set st S1[i,x] )
assume i in Seg n ; ::_thesis: ex x being set st S1[i,x]
( i in X or not i in X ) ;
hence ex x being set st S1[i,x] ; ::_thesis: verum
end;
consider f being FinSequence such that
A10: ( dom f = Seg n & ( for j being Nat st j in Seg n holds
S1[j,f . j] ) ) from FINSEQ_1:sch_1(A9);
A11: dom M = Seg n by A4, FINSEQ_1:def_3;
rng f c= REAL
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in REAL )
assume z in rng f ; ::_thesis: z in REAL
then consider x being set such that
A12: x in dom f and
A13: f . x = z by FUNCT_1:def_3;
reconsider x = x as Nat by A12;
A14: S1[x,f . x] by A10, A12;
M . x = Line (M,x) by A11, A10, A12, MATRIX_2:16;
then M . x in lines M by A10, A12, MATRIX13:103;
then reconsider Mx = M . x as Element of (m -VectSp_over F_Real) ;
percases ( not x in X or x in X ) ;
suppose not x in X ; ::_thesis: z in REAL
then f . x = 0 by A10, A12;
hence z in REAL by A13; ::_thesis: verum
end;
suppose x in X ; ::_thesis: z in REAL
thus z in REAL by A13, A14, XREAL_0:def_1; ::_thesis: verum
end;
end;
end;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
len f = n by A4, A10, FINSEQ_1:def_3;
then A15: f is n -element by CARD_1:def_7;
then consider K being Linear_Combination of lines M such that
A16: Sum K = (Mx2Tran M) . f and
A17: for i being Nat st i in X holds
K . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) by A2, A3, Th15;
now__::_thesis:_for_v_being_Element_of_(m_-VectSp_over_F_Real)_holds_L_._v_=_K_._v
let v be Element of (m -VectSp_over F_Real); ::_thesis: L . b1 = K . b1
percases ( v in lines M or not v in lines M ) ;
suppose v in lines M ; ::_thesis: L . b1 = K . b1
then consider i being set such that
A18: i in dom (M | X) and
A19: (M | X) . i = v by A2, FUNCT_1:def_3;
A20: M . i = v by A18, A19, FUNCT_1:47;
set D = dom (f | (M " {v}));
Seq (f | (M " {v})) = @ (@ (Seq (f | (M " {v})))) ;
then reconsider F = Seq (f | (M " {v})) as FinSequence of REAL ;
A21: rng (Sgm (dom (f | (M " {v})))) = dom (f | (M " {v})) by FINSEQ_1:50;
then A22: dom F = dom (Sgm (dom (f | (M " {v})))) by RELAT_1:27;
A23: i in dom M by A18, RELAT_1:57;
A24: i in X by A18;
reconsider i = i as Nat by A18;
M . i = Line (M,i) by A23, MATRIX_2:16;
then A25: K . v = Sum (Seq (f | (M " {v}))) by A17, A24, A20;
v in {v} by TARSKI:def_1;
then i in M " {v} by A23, A20, FUNCT_1:def_7;
then i in dom (f | (M " {v})) by A10, A24, RELAT_1:57;
then consider j being set such that
A26: j in dom (Sgm (dom (f | (M " {v})))) and
A27: (Sgm (dom (f | (M " {v})))) . j = i by A21, FUNCT_1:def_3;
reconsider j = j as Element of NAT by A26;
( F . j = (f | (M " {v})) . i & i in dom (f | (M " {v})) ) by A22, A26, A27, FUNCT_1:11, FUNCT_1:12;
then A28: F . j = f . i by FUNCT_1:47;
dom (f | (M " {v})) c= dom f by RELAT_1:60;
then A29: Sgm (dom (f | (M " {v}))) is one-to-one by A10, FINSEQ_3:92;
now__::_thesis:_for_w_being_Element_of_NAT_st_w_in_dom_F_&_w_<>_j_holds_
F_._w_=_0
let w be Element of NAT ; ::_thesis: ( w in dom F & w <> j implies F . w = 0 )
assume that
A30: w in dom F and
A31: w <> j ; ::_thesis: F . w = 0
A32: (Sgm (dom (f | (M " {v})))) . w in dom (f | (M " {v})) by A21, A22, A30, FUNCT_1:def_3;
then (Sgm (dom (f | (M " {v})))) . w in M " {v} by RELAT_1:57;
then M . ((Sgm (dom (f | (M " {v})))) . w) in {v} by FUNCT_1:def_7;
then A33: M . ((Sgm (dom (f | (M " {v})))) . w) = v by TARSKI:def_1;
A34: not (Sgm (dom (f | (M " {v})))) . w in X
proof
assume (Sgm (dom (f | (M " {v})))) . w in X ; ::_thesis: contradiction
then A35: (Sgm (dom (f | (M " {v})))) . w in dom (M | X) by A11, RELAT_1:57;
then v = (M | X) . ((Sgm (dom (f | (M " {v})))) . w) by A33, FUNCT_1:47;
then i = (Sgm (dom (f | (M " {v})))) . w by A3, A18, A19, A35, FUNCT_1:def_4;
hence contradiction by A22, A29, A26, A27, A30, A31, FUNCT_1:def_4; ::_thesis: verum
end;
F . w = (f | (M " {v})) . ((Sgm (dom (f | (M " {v})))) . w) by A30, FUNCT_1:12;
then A36: F . w = f . ((Sgm (dom (f | (M " {v})))) . w) by A32, FUNCT_1:47;
(Sgm (dom (f | (M " {v})))) . w in dom f by A32, RELAT_1:57;
hence F . w = 0 by A10, A36, A34; ::_thesis: verum
end;
then A37: F has_onlyone_value_in j by A22, A26, ENTROPY1:def_2;
f . i = L . v by A10, A24, A20;
hence L . v = K . v by A25, A28, A37, ENTROPY1:13; ::_thesis: verum
end;
supposeA38: not v in lines M ; ::_thesis: L . b1 = K . b1
Carrier L c= lines M by VECTSP_6:def_4;
then not v in Carrier L by A38;
then A39: L . v = 0. F_Real by VECTSP_6:2;
Carrier K c= lines M by VECTSP_6:def_4;
then not v in Carrier K by A38;
hence L . v = K . v by A39, VECTSP_6:2; ::_thesis: verum
end;
end;
end;
then A40: Sum K = Sum L by VECTSP_6:def_7;
( dom (Mx2Tran M) = [#] (TOP-REAL n) & f is Point of (TOP-REAL n) ) by A15, Lm3, FUNCT_2:def_1;
hence y in rng (Mx2Tran M) by A8, A16, A40, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th19: :: MATRTOP2:19
for n being Nat
for F being one-to-one FinSequence of (TOP-REAL n) st rng F is linearly-independent holds
ex M being Matrix of n,F_Real st
( M is invertible & M | (len F) = F )
proof
let n be Nat; ::_thesis: for F being one-to-one FinSequence of (TOP-REAL n) st rng F is linearly-independent holds
ex M being Matrix of n,F_Real st
( M is invertible & M | (len F) = F )
let F be one-to-one FinSequence of (TOP-REAL n); ::_thesis: ( rng F is linearly-independent implies ex M being Matrix of n,F_Real st
( M is invertible & M | (len F) = F ) )
assume A1: rng F is linearly-independent ; ::_thesis: ex M being Matrix of n,F_Real st
( M is invertible & M | (len F) = F )
reconsider f = F as FinSequence of (n -VectSp_over F_Real) by Lm1;
set M = FinS2MX f;
lines (FinS2MX f) is linearly-independent by A1, Th7;
then A2: the_rank_of (FinS2MX f) = len F by MATRIX13:121;
then consider A being Matrix of n -' (len F),n,F_Real such that
A3: the_rank_of ((FinS2MX f) ^ A) = n by MATRTOP1:16;
len F <= width (FinS2MX f) by A2, MATRIX13:74;
then len F <= n by MATRIX_1:23;
then n - (len F) = n -' (len F) by XREAL_1:233;
then reconsider MA = (FinS2MX f) ^ A as Matrix of n,F_Real ;
take MA ; ::_thesis: ( MA is invertible & MA | (len F) = F )
Det MA <> 0. F_Real by A3, MATRIX13:83;
hence MA is invertible by LAPLACE:34; ::_thesis: MA | (len F) = F
thus F = MA | (dom F) by FINSEQ_1:21
.= MA | (len F) by FINSEQ_1:def_3 ; ::_thesis: verum
end;
theorem Th20: :: MATRTOP2:20
for n, k being Nat
for f being b1 -element real-valued FinSequence
for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
( f in Lin (rng (B | k)) iff f = (f | k) ^ ((n -' k) |-> 0) )
proof
let n, k be Nat; ::_thesis: for f being n -element real-valued FinSequence
for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
( f in Lin (rng (B | k)) iff f = (f | k) ^ ((n -' k) |-> 0) )
let f be n -element real-valued FinSequence; ::_thesis: for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
( f in Lin (rng (B | k)) iff f = (f | k) ^ ((n -' k) |-> 0) )
set V = n -VectSp_over F_Real;
set nk0 = (n -' k) |-> 0;
let B be OrdBasis of n -VectSp_over F_Real; ::_thesis: ( B = MX2FinS (1. (F_Real,n)) implies ( f in Lin (rng (B | k)) iff f = (f | k) ^ ((n -' k) |-> 0) ) )
assume A1: B = MX2FinS (1. (F_Real,n)) ; ::_thesis: ( f in Lin (rng (B | k)) iff f = (f | k) ^ ((n -' k) |-> 0) )
A2: len B = n by A1, MATRIX_1:def_2;
A3: f is Point of (TOP-REAL n) by Lm3;
then A4: f is Point of (n -VectSp_over F_Real) by Lm1;
A5: rng B is Basis of n -VectSp_over F_Real by MATRLIN:def_2;
then A6: rng B is linearly-independent by VECTSP_7:def_3;
Lin (rng B) = VectSpStr(# the carrier of (n -VectSp_over F_Real), the addF of (n -VectSp_over F_Real), the ZeroF of (n -VectSp_over F_Real), the lmult of (n -VectSp_over F_Real) #) by A5, VECTSP_7:def_3;
then A7: f in Lin (rng B) by A4, STRUCT_0:def_5;
A8: B is one-to-one by MATRLIN:def_2;
reconsider F = f as Point of (n -VectSp_over F_Real) by A3, Lm1;
A9: len f = n by CARD_1:def_7;
percases ( k >= n or k < n ) ;
supposeA10: k >= n ; ::_thesis: ( f in Lin (rng (B | k)) iff f = (f | k) ^ ((n -' k) |-> 0) )
then n - k <= 0 by XREAL_1:47;
then n -' k = 0 by XREAL_0:def_2;
then A11: (n -' k) |-> 0 = {} ;
f | k = f by A9, A10, FINSEQ_1:58;
hence ( f in Lin (rng (B | k)) iff f = (f | k) ^ ((n -' k) |-> 0) ) by A2, A7, A10, A11, FINSEQ_1:34, FINSEQ_1:58; ::_thesis: verum
end;
supposeA12: k < n ; ::_thesis: ( f in Lin (rng (B | k)) iff f = (f | k) ^ ((n -' k) |-> 0) )
then A13: len (f | k) = k by A9, FINSEQ_1:59;
A14: len ((n -' k) |-> 0) = n -' k by CARD_1:def_7;
consider KL being Linear_Combination of n -VectSp_over F_Real such that
A15: F = Sum KL and
A16: Carrier KL c= rng B and
A17: for k being Nat st 1 <= k & k <= len (F |-- B) holds
(F |-- B) /. k = KL . (B /. k) by MATRLIN:def_7;
reconsider KL = KL as Linear_Combination of rng B by A16, VECTSP_6:def_4;
A18: F |-- B = F by A1, A2, MATRLIN2:46;
n -' k = n - k by A12, XREAL_1:233;
then len ((f | k) ^ ((n -' k) |-> 0)) = k + (n - k) by A13, A14, FINSEQ_1:22;
then A19: dom ((f | k) ^ ((n -' k) |-> 0)) = dom f by A9, FINSEQ_3:29;
hereby ::_thesis: ( f = (f | k) ^ ((n -' k) |-> 0) implies f in Lin (rng (B | k)) )
assume f in Lin (rng (B | k)) ; ::_thesis: (f | k) ^ ((n -' k) |-> 0) = f
then consider L being Linear_Combination of rng (B | k) such that
A20: Sum L = f by VECTSP_7:7;
reconsider L1 = L as Linear_Combination of rng B by RELAT_1:70, VECTSP_6:4;
A21: KL - L1 is Linear_Combination of rng B by VECTSP_6:42;
Sum (KL - L1) = (Sum KL) - (Sum L1) by VECTSP_6:47
.= 0. (n -VectSp_over F_Real) by A15, A20, VECTSP_1:19 ;
then Carrier (KL - L1) = {} by A6, A21, VECTSP_7:def_1;
then A22: ZeroLC (n -VectSp_over F_Real) = KL - L1 by VECTSP_6:def_3
.= KL + (- L1) by VECTSP_6:def_11
.= (- L1) + KL by VECTSP_6:25 ;
reconsider M1 = - (1. F_Real) as Element of F_Real ;
A23: Carrier L c= rng (B | k) by VECTSP_6:def_4;
L1 = - (- L1) ;
then A24: KL = L1 by A22, VECTSP_6:37;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_f_holds_
((f_|_k)_^_((n_-'_k)_|->_0))_._i_=_f_._i
let i be Nat; ::_thesis: ( i in dom f implies ((f | k) ^ ((n -' k) |-> 0)) . b1 = f . b1 )
assume A25: i in dom f ; ::_thesis: ((f | k) ^ ((n -' k) |-> 0)) . b1 = f . b1
percases ( i in dom (f | k) or ex j being Nat st
( j in dom ((n -' k) |-> 0) & i = k + j ) ) by A13, A19, A25, FINSEQ_1:25;
supposeA26: i in dom (f | k) ; ::_thesis: ((f | k) ^ ((n -' k) |-> 0)) . b1 = f . b1
then (f | k) . i = f . i by FUNCT_1:47;
hence ((f | k) ^ ((n -' k) |-> 0)) . i = f . i by A26, FINSEQ_1:def_7; ::_thesis: verum
end;
supposeA27: ex j being Nat st
( j in dom ((n -' k) |-> 0) & i = k + j ) ; ::_thesis: f . b1 = ((f | k) ^ ((n -' k) |-> 0)) . b1
A28: i in dom B by A9, A2, A25, FINSEQ_3:29;
then A29: B /. i = B . i by PARTFUN1:def_6;
consider j being Nat such that
A30: j in dom ((n -' k) |-> 0) and
A31: i = k + j by A27;
A32: 1 <= j by A30, FINSEQ_3:25;
not B . i in rng (B | k)
proof
assume B . i in rng (B | k) ; ::_thesis: contradiction
then consider x being set such that
A33: x in dom (B | k) and
A34: (B | k) . x = B . i by FUNCT_1:def_3;
( B . x = B . i & x in dom B ) by A33, A34, FUNCT_1:47, RELAT_1:57;
then A35: i = x by A8, A28, FUNCT_1:def_4;
x in Seg k by A33, RELAT_1:57;
then A36: i <= k by A35, FINSEQ_1:1;
i >= k + 1 by A31, A32, XREAL_1:6;
hence contradiction by A36, NAT_1:13; ::_thesis: verum
end;
then A37: not B . i in Carrier L by A23;
( 1 <= i & i <= n ) by A9, A25, FINSEQ_3:25;
then A38: (F |-- B) /. i = KL . (B /. i) by A9, A18, A17;
f . i = (F |-- B) /. i by A18, A25, PARTFUN1:def_6;
hence f . i = 0. F_Real by A24, A38, A29, A37, VECTSP_6:2
.= ((n -' k) |-> 0) . j
.= ((f | k) ^ ((n -' k) |-> 0)) . i by A13, A30, A31, FINSEQ_1:def_7 ;
::_thesis: verum
end;
end;
end;
hence (f | k) ^ ((n -' k) |-> 0) = f by A19, FINSEQ_1:13; ::_thesis: verum
end;
assume A39: (f | k) ^ ((n -' k) |-> 0) = f ; ::_thesis: f in Lin (rng (B | k))
Carrier KL c= rng (B | k)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier KL or x in rng (B | k) )
assume A40: x in Carrier KL ; ::_thesis: x in rng (B | k)
Carrier KL c= rng B by VECTSP_6:def_4;
then consider i being set such that
A41: i in dom B and
A42: B . i = x by A40, FUNCT_1:def_3;
reconsider i = i as Element of NAT by A41;
A43: B /. i = B . i by A41, PARTFUN1:def_6;
A44: dom B = dom f by A9, A2, FINSEQ_3:29;
assume A45: not x in rng (B | k) ; ::_thesis: contradiction
not i in Seg k
proof
assume i in Seg k ; ::_thesis: contradiction
then A46: i in dom (B | k) by A41, RELAT_1:57;
then (B | k) . i = B . i by FUNCT_1:47;
hence contradiction by A42, A45, A46, FUNCT_1:def_3; ::_thesis: verum
end;
then not i in dom (f | k) by A13, FINSEQ_1:def_3;
then consider j being Nat such that
A47: j in dom ((n -' k) |-> 0) and
A48: i = k + j by A13, A19, A41, A44, FINSEQ_1:25;
A49: ((n -' k) |-> 0) . j = 0 ;
A50: ( 1 <= i & i <= n ) by A2, A41, FINSEQ_3:25;
(F |-- B) /. i = (F |-- B) . i by A18, A41, A44, PARTFUN1:def_6;
then KL . (B /. i) = f . i by A9, A18, A17, A50
.= 0. F_Real by A13, A39, A47, A48, A49, FINSEQ_1:def_7 ;
hence contradiction by A40, A42, A43, VECTSP_6:2; ::_thesis: verum
end;
then KL is Linear_Combination of rng (B | k) by VECTSP_6:def_4;
hence f in Lin (rng (B | k)) by A15, VECTSP_7:7; ::_thesis: verum
end;
end;
end;
theorem Th21: :: MATRTOP2:21
for n being Nat
for F being one-to-one FinSequence of (TOP-REAL n) st rng F is linearly-independent holds
for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
proof
let n be Nat; ::_thesis: for F being one-to-one FinSequence of (TOP-REAL n) st rng F is linearly-independent holds
for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
let F be one-to-one FinSequence of (TOP-REAL n); ::_thesis: ( rng F is linearly-independent implies for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F)) )
assume A1: rng F is linearly-independent ; ::_thesis: for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
reconsider f = F as FinSequence of (n -VectSp_over F_Real) by Lm1;
set MF = FinS2MX f;
set n1 = n -' (len F);
set L = len F;
lines (FinS2MX f) is linearly-independent by A1, Th7;
then the_rank_of (FinS2MX f) = len F by MATRIX13:121;
then len F <= width (FinS2MX f) by MATRIX13:74;
then A2: len F <= n by MATRIX_1:23;
then A3: n - (len F) = n -' (len F) by XREAL_1:233;
set V = n -VectSp_over F_Real;
let B be OrdBasis of n -VectSp_over F_Real; ::_thesis: ( B = MX2FinS (1. (F_Real,n)) implies for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F)) )
assume A4: B = MX2FinS (1. (F_Real,n)) ; ::_thesis: for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
let M be Matrix of n,F_Real; ::_thesis: ( M is invertible & M | (len F) = F implies (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F)) )
assume that
M is invertible and
A5: M | (len F) = F ; ::_thesis: (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
consider q being FinSequence such that
A6: M = F ^ q by A5, FINSEQ_1:80;
M = MX2FinS M ;
then reconsider q = q as FinSequence of (n -VectSp_over F_Real) by A6, FINSEQ_1:36;
A7: len M = (len F) + (len q) by A6, FINSEQ_1:22;
set Mq = FinS2MX q;
set MT = Mx2Tran M;
A8: len M = n by MATRIX_1:def_2;
A9: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:52;
A10: dom (Mx2Tran (FinS2MX f)) = [#] (TOP-REAL (len F)) by FUNCT_2:def_1;
A11: the carrier of (TOP-REAL n) = REAL n by EUCLID:22
.= n -tuples_on REAL ;
A12: rng (Mx2Tran (FinS2MX f)) = [#] (Lin (lines (FinS2MX f))) by Th18
.= [#] (Lin (rng F)) by Th6 ;
A13: n |-> 0 = 0* n
.= 0. (TOP-REAL n) by EUCLID:70 ;
A14: (n -' (len F)) |-> 0 = 0* (n -' (len F))
.= 0. (TOP-REAL (n -' (len F))) by EUCLID:70 ;
then A15: (Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0) = 0. (TOP-REAL n) by A3, A8, A7, MATRTOP1:29;
thus (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) c= [#] (Lin (rng F)) :: according to XBOOLE_0:def_10 ::_thesis: [#] (Lin (rng F)) c= (Mx2Tran M) .: ([#] (Lin (rng (B | (len F)))))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) or y in [#] (Lin (rng F)) )
assume y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) ; ::_thesis: y in [#] (Lin (rng F))
then consider x being set such that
A16: x in dom (Mx2Tran M) and
A17: x in [#] (Lin (rng (B | (len F)))) and
A18: (Mx2Tran M) . x = y by FUNCT_1:def_6;
reconsider x = x as Element of (TOP-REAL n) by A16;
len x = n by CARD_1:def_7;
then len (x | (len F)) = len F by A2, FINSEQ_1:59;
then A19: x | (len F) is len F -element by CARD_1:def_7;
then A20: x | (len F) is Element of (TOP-REAL (len F)) by Lm3;
A21: (Mx2Tran (FinS2MX f)) . (x | (len F)) is Element of n -tuples_on REAL by A11, A19, Lm3;
x in Lin (rng (B | (len F))) by A17, STRUCT_0:def_5;
then x = (x | (len F)) ^ ((n -' (len F)) |-> 0) by A4, Th20;
then y = ((Mx2Tran (FinS2MX f)) . (x | (len F))) + ((Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0)) by A3, A8, A6, A7, A18, A19, MATRTOP1:36
.= (Mx2Tran (FinS2MX f)) . (x | (len F)) by A13, A15, A21, RVSUM_1:16 ;
hence y in [#] (Lin (rng F)) by A12, A10, A20, FUNCT_1:def_3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [#] (Lin (rng F)) or y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) )
assume y in [#] (Lin (rng F)) ; ::_thesis: y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F)))))
then consider x being set such that
A22: x in dom (Mx2Tran (FinS2MX f)) and
A23: (Mx2Tran (FinS2MX f)) . x = y by A12, FUNCT_1:def_3;
reconsider x = x as Element of (TOP-REAL (len F)) by A22;
(Mx2Tran (FinS2MX f)) . x is Element of (TOP-REAL n) by Lm3;
then A24: y = ((Mx2Tran (FinS2MX f)) . x) + (0. (TOP-REAL n)) by A11, A13, A23, RVSUM_1:16
.= ((Mx2Tran (FinS2MX f)) . x) + ((Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0)) by A3, A8, A7, A14, MATRTOP1:29
.= (Mx2Tran M) . (x ^ ((n -' (len F)) |-> 0)) by A6, A3, A8, A7, MATRTOP1:36 ;
set xx = x ^ ((n -' (len F)) |-> 0);
len x = len F by CARD_1:def_7;
then dom x = Seg (len F) by FINSEQ_1:def_3;
then x ^ ((n -' (len F)) |-> 0) = ((x ^ ((n -' (len F)) |-> 0)) | (len F)) ^ ((n -' (len F)) |-> 0) by FINSEQ_1:21;
then x ^ ((n -' (len F)) |-> 0) in Lin (rng (B | (len F))) by A4, A3, Th20;
then A25: x ^ ((n -' (len F)) |-> 0) in [#] (Lin (rng (B | (len F)))) by STRUCT_0:def_5;
x ^ ((n -' (len F)) |-> 0) is Element of (TOP-REAL n) by A3, Lm3;
hence y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) by A9, A24, A25, FUNCT_1:def_6; ::_thesis: verum
end;
theorem :: MATRTOP2:22
for n being Nat
for A, B being linearly-independent Subset of (TOP-REAL n) st card A = card B holds
ex M being Matrix of n,F_Real st
( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) )
proof
let n be Nat; ::_thesis: for A, B being linearly-independent Subset of (TOP-REAL n) st card A = card B holds
ex M being Matrix of n,F_Real st
( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) )
set TRn = TOP-REAL n;
let A, B be linearly-independent Subset of (TOP-REAL n); ::_thesis: ( card A = card B implies ex M being Matrix of n,F_Real st
( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) ) )
assume A1: card A = card B ; ::_thesis: ex M being Matrix of n,F_Real st
( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) )
reconsider BB = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
set V = n -VectSp_over F_Real;
A is linearly-independent Subset of (n -VectSp_over F_Real) by Lm1, Th7;
then A is finite by VECTSP_9:21;
then consider fA being FinSequence such that
A2: rng fA = A and
A3: fA is one-to-one by FINSEQ_4:58;
A4: len fA = card A by A2, A3, PRE_POLY:19;
B is linearly-independent Subset of (n -VectSp_over F_Real) by Lm1, Th7;
then B is finite by VECTSP_9:21;
then consider fB being FinSequence such that
A5: rng fB = B and
A6: fB is one-to-one by FINSEQ_4:58;
A7: len fB = card B by A5, A6, PRE_POLY:19;
reconsider fA = fA, fB = fB as FinSequence of (TOP-REAL n) by A2, A5, FINSEQ_1:def_4;
consider MA being Matrix of n,F_Real such that
A8: MA is invertible and
A9: MA | (len fA) = fA by A2, A3, Th19;
A10: [#] (Lin (rng (BB | (len fA)))) c= [#] (n -VectSp_over F_Real) by VECTSP_4:def_2;
set Ma = Mx2Tran MA;
A11: Det MA <> 0. F_Real by A8, LAPLACE:34;
then A12: Mx2Tran MA is one-to-one by MATRTOP1:40;
then A13: rng ((Mx2Tran MA) ") = dom (Mx2Tran MA) by FUNCT_1:33;
A14: ( [#] (TOP-REAL n) = [#] (n -VectSp_over F_Real) & dom (Mx2Tran MA) = [#] (TOP-REAL n) ) by Lm1, FUNCT_2:52;
((Mx2Tran MA) ") " ([#] (Lin (rng (BB | (len fA))))) = (Mx2Tran MA) .: ([#] (Lin (rng (BB | (len fA))))) by A12, FUNCT_1:84
.= [#] (Lin A) by A2, A3, A8, A9, Th21 ;
then A15: ((Mx2Tran MA) ") .: ([#] (Lin A)) = [#] (Lin (rng (BB | (len fB)))) by A1, A4, A7, A14, A13, A10, FUNCT_1:77;
consider MB being Matrix of n,F_Real such that
A16: MB is invertible and
A17: MB | (len fB) = fB by A5, A6, Th19;
set Mb = Mx2Tran MB;
A18: ( n = 0 implies n = 0 ) ;
then reconsider mb = MB as Matrix of width (MA ~),n,F_Real by MATRIX13:1;
A19: width MB = n by A18, MATRIX13:1;
then reconsider MM = (MA ~) * mb as Matrix of n,F_Real by A18, MATRIX13:1;
take MM ; ::_thesis: ( MM is invertible & (Mx2Tran MM) .: ([#] (Lin A)) = [#] (Lin B) )
MA ~ is invertible by A8, MATRIX_6:16;
hence MM is invertible by A16, MATRIX_6:45; ::_thesis: (Mx2Tran MM) .: ([#] (Lin A)) = [#] (Lin B)
(Mx2Tran MB) * ((Mx2Tran MA) ") = (Mx2Tran mb) * ((Mx2Tran MA) ") by A18, MATRIX13:1
.= (Mx2Tran mb) * (Mx2Tran (MA ~)) by A11, MATRTOP1:43
.= Mx2Tran ((MA ~) * mb) by A18, MATRTOP1:32
.= Mx2Tran MM by A18, A19, MATRIX13:1 ;
hence (Mx2Tran MM) .: ([#] (Lin A)) = (Mx2Tran MB) .: ([#] (Lin (rng (BB | (len fB))))) by A15, RELAT_1:126
.= [#] (Lin B) by A5, A6, A16, A17, Th21 ;
::_thesis: verum
end;
begin
theorem Th23: :: MATRTOP2:23
for m, n being Nat
for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is linearly-independent
proof
let m, n be Nat; ::_thesis: for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is linearly-independent
let M be Matrix of n,m,F_Real; ::_thesis: for A being linearly-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is linearly-independent
let A be linearly-independent Subset of (TOP-REAL n); ::_thesis: ( the_rank_of M = n implies (Mx2Tran M) .: A is linearly-independent )
assume A1: the_rank_of M = n ; ::_thesis: (Mx2Tran M) .: A is linearly-independent
set nV = n -VectSp_over F_Real;
set mV = m -VectSp_over F_Real;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
reconsider Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
len Bn = n by MATRTOP1:19;
then reconsider M1 = M as Matrix of len Bn, len Bm,F_Real by MATRTOP1:19;
set MT = Mx2Tran (M1,Bn,Bm);
A2: Mx2Tran M = Mx2Tran (M1,Bn,Bm) by MATRTOP1:20;
reconsider A1 = A as Subset of (n -VectSp_over F_Real) by Lm1;
A3: A1 is linearly-independent by Th7;
(Mx2Tran (M1,Bn,Bm)) .: A1 is linearly-independent
proof
assume not (Mx2Tran (M1,Bn,Bm)) .: A1 is linearly-independent ; ::_thesis: contradiction
then consider L being Linear_Combination of (Mx2Tran (M1,Bn,Bm)) .: A1 such that
A4: Carrier L <> {} and
A5: Sum L = 0. (m -VectSp_over F_Real) by RANKNULL:41;
A6: Mx2Tran (M1,Bn,Bm) is one-to-one by A1, A2, MATRTOP1:39;
then A7: ker (Mx2Tran (M1,Bn,Bm)) = (0). (n -VectSp_over F_Real) by RANKNULL:15;
A8: (Mx2Tran (M1,Bn,Bm)) | A1 is one-to-one by A6, FUNCT_1:52;
then A9: (Mx2Tran (M1,Bn,Bm)) @ ((Mx2Tran (M1,Bn,Bm)) # L) = L by RANKNULL:43;
(Mx2Tran (M1,Bn,Bm)) | (Carrier ((Mx2Tran (M1,Bn,Bm)) # L)) is one-to-one by A6, FUNCT_1:52;
then (Mx2Tran (M1,Bn,Bm)) .: (Carrier ((Mx2Tran (M1,Bn,Bm)) # L)) = Carrier L by A9, RANKNULL:39;
then A10: Carrier ((Mx2Tran (M1,Bn,Bm)) # L) <> {} by A4;
(Mx2Tran (M1,Bn,Bm)) . (Sum ((Mx2Tran (M1,Bn,Bm)) # L)) = 0. (m -VectSp_over F_Real) by A5, A8, A9, Th14;
then Sum ((Mx2Tran (M1,Bn,Bm)) # L) in ker (Mx2Tran (M1,Bn,Bm)) by RANKNULL:10;
then Sum ((Mx2Tran (M1,Bn,Bm)) # L) = 0. (n -VectSp_over F_Real) by A7, VECTSP_4:35;
hence contradiction by A3, A10, VECTSP_7:def_1; ::_thesis: verum
end;
hence (Mx2Tran M) .: A is linearly-independent by A2, Th7; ::_thesis: verum
end;
theorem Th24: :: MATRTOP2:24
for m, n being Nat
for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is affinely-independent
proof
let m, n be Nat; ::_thesis: for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is affinely-independent
let M be Matrix of n,m,F_Real; ::_thesis: for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is affinely-independent
set MT = Mx2Tran M;
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
let A be affinely-independent Subset of (TOP-REAL n); ::_thesis: ( the_rank_of M = n implies (Mx2Tran M) .: A is affinely-independent )
assume A1: the_rank_of M = n ; ::_thesis: (Mx2Tran M) .: A is affinely-independent
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: (Mx2Tran M) .: A is affinely-independent
then (Mx2Tran M) .: A is empty ;
hence (Mx2Tran M) .: A is affinely-independent ; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: (Mx2Tran M) .: A is affinely-independent
then consider v being Element of (TOP-REAL n) such that
A2: v in A and
A3: ((- v) + A) \ {(0. (TOP-REAL n))} is linearly-independent by RLAFFIN1:def_4;
A4: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def_1;
then A5: (Mx2Tran M) . v in (Mx2Tran M) .: A by A2, FUNCT_1:def_6;
(Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m) by MATRTOP1:29;
then A6: {(0. (TOP-REAL m))} = Im ((Mx2Tran M),(0. (TOP-REAL n))) by A4, FUNCT_1:59
.= (Mx2Tran M) .: {(0. (TOP-REAL n))} by RELAT_1:def_16 ;
- v = (0. (TOP-REAL n)) - v by RLVECT_1:14;
then A7: (Mx2Tran M) . (- v) = ((Mx2Tran M) . (0. (TOP-REAL n))) - ((Mx2Tran M) . v) by MATRTOP1:28
.= (0. (TOP-REAL m)) - ((Mx2Tran M) . v) by MATRTOP1:29
.= - ((Mx2Tran M) . v) by RLVECT_1:14 ;
Mx2Tran M is one-to-one by A1, MATRTOP1:39;
then A8: (Mx2Tran M) .: (((- v) + A) \ {(0. (TOP-REAL n))}) = ((Mx2Tran M) .: ((- v) + A)) \ ((Mx2Tran M) .: {(0. (TOP-REAL n))}) by FUNCT_1:64
.= ((- ((Mx2Tran M) . v)) + ((Mx2Tran M) .: A)) \ {(0. (TOP-REAL m))} by A6, A7, MATRTOP1:30 ;
(Mx2Tran M) .: (((- v) + A) \ {(0. (TOP-REAL n))}) is linearly-independent by A1, A3, Th23;
hence (Mx2Tran M) .: A is affinely-independent by A5, A8, RLAFFIN1:def_4; ::_thesis: verum
end;
end;
end;
theorem :: MATRTOP2:25
for m, n being Nat
for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
for v being Element of (TOP-REAL n) st v in Affin A holds
( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being b2 -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )
proof
let m, n be Nat; ::_thesis: for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
for v being Element of (TOP-REAL n) st v in Affin A holds
( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being n -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )
let M be Matrix of n,m,F_Real; ::_thesis: for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
for v being Element of (TOP-REAL n) st v in Affin A holds
( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being n -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )
reconsider Z = 0 as Element of NAT ;
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
let A be affinely-independent Subset of (TOP-REAL n); ::_thesis: ( the_rank_of M = n implies for v being Element of (TOP-REAL n) st v in Affin A holds
( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being n -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) ) )
assume A1: the_rank_of M = n ; ::_thesis: for v being Element of (TOP-REAL n) st v in Affin A holds
( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being n -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )
set MT = Mx2Tran M;
let v be Element of (TOP-REAL n); ::_thesis: ( v in Affin A implies ( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being n -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) ) )
assume A2: v in Affin A ; ::_thesis: ( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being n -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )
set vA = v |-- A;
set C = Carrier (v |-- A);
defpred S1[ set , set ] means ( ( not $1 in rng (Mx2Tran M) implies $2 = 0 ) & ( $1 in rng (Mx2Tran M) implies for f being n -element real-valued FinSequence st (Mx2Tran M) . f = $1 holds
$2 = (v |-- A) . f ) );
consider H being FinSequence of the carrier of (TOP-REAL n) such that
A3: H is one-to-one and
A4: rng H = Carrier (v |-- A) and
A5: Sum ((v |-- A) (#) H) = Sum (v |-- A) by RLVECT_2:def_8;
A6: Sum (v |-- A) = v by A2, RLAFFIN1:def_7;
reconsider MTR = (Mx2Tran M) * H as FinSequence of (TOP-REAL m) ;
A7: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def_1;
then rng H c= dom (Mx2Tran M) ;
then A8: len MTR = len H by FINSEQ_2:29;
A9: Mx2Tran M is one-to-one by A1, MATRTOP1:39;
A10: for x being set st x in the carrier of (TOP-REAL m) holds
ex y being set st
( y in REAL & S1[x,y] )
proof
let y be set ; ::_thesis: ( y in the carrier of (TOP-REAL m) implies ex y being set st
( y in REAL & S1[y,y] ) )
assume y in the carrier of (TOP-REAL m) ; ::_thesis: ex y being set st
( y in REAL & S1[y,y] )
percases ( y in rng (Mx2Tran M) or not y in rng (Mx2Tran M) ) ;
supposeA11: y in rng (Mx2Tran M) ; ::_thesis: ex y being set st
( y in REAL & S1[y,y] )
then consider x being set such that
A12: x in dom (Mx2Tran M) and
A13: (Mx2Tran M) . x = y by FUNCT_1:def_3;
reconsider x = x as Element of (TOP-REAL n) by A12;
take (v |-- A) . x ; ::_thesis: ( (v |-- A) . x in REAL & S1[y,(v |-- A) . x] )
thus ( (v |-- A) . x in REAL & ( not y in rng (Mx2Tran M) implies (v |-- A) . x = 0 ) ) by A11; ::_thesis: ( y in rng (Mx2Tran M) implies for f being n -element real-valued FinSequence st (Mx2Tran M) . f = y holds
(v |-- A) . x = (v |-- A) . f )
assume y in rng (Mx2Tran M) ; ::_thesis: for f being n -element real-valued FinSequence st (Mx2Tran M) . f = y holds
(v |-- A) . x = (v |-- A) . f
let f be n -element real-valued FinSequence; ::_thesis: ( (Mx2Tran M) . f = y implies (v |-- A) . x = (v |-- A) . f )
assume A14: (Mx2Tran M) . f = y ; ::_thesis: (v |-- A) . x = (v |-- A) . f
f is Element of (TOP-REAL n) by Lm3;
hence (v |-- A) . x = (v |-- A) . f by A7, A9, A13, A14, FUNCT_1:def_4; ::_thesis: verum
end;
supposeA15: not y in rng (Mx2Tran M) ; ::_thesis: ex y being set st
( y in REAL & S1[y,y] )
take x = 0 ; ::_thesis: ( x in REAL & S1[y,x] )
thus ( x in REAL & S1[y,x] ) by A15; ::_thesis: verum
end;
end;
end;
consider F being Function of the carrier of (TOP-REAL m),REAL such that
A16: for x being set st x in the carrier of (TOP-REAL m) holds
S1[x,F . x] from FUNCT_2:sch_1(A10);
reconsider F = F as Element of Funcs ( the carrier of (TOP-REAL m),REAL) by FUNCT_2:8;
A17: now__::_thesis:_for_w_being_Element_of_(TOP-REAL_m)_st_not_w_in_(Mx2Tran_M)_.:_(Carrier_(v_|--_A))_holds_
not_F_._w_<>_0
let w be Element of (TOP-REAL m); ::_thesis: ( not w in (Mx2Tran M) .: (Carrier (v |-- A)) implies not F . w <> 0 )
assume A18: not w in (Mx2Tran M) .: (Carrier (v |-- A)) ; ::_thesis: not F . w <> 0
assume A19: F . w <> 0 ; ::_thesis: contradiction
then w in rng (Mx2Tran M) by A16;
then consider f being set such that
A20: f in dom (Mx2Tran M) and
A21: (Mx2Tran M) . f = w by FUNCT_1:def_3;
reconsider f = f as Element of (TOP-REAL n) by A20;
(v |-- A) . f = F . w by A16, A19, A21;
then f in Carrier (v |-- A) by A19, RLVECT_2:19;
hence contradiction by A18, A20, A21, FUNCT_1:def_6; ::_thesis: verum
end;
then reconsider F = F as Linear_Combination of TOP-REAL m by RLVECT_2:def_3;
A22: (Mx2Tran M) .: (Carrier (v |-- A)) c= Carrier F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Mx2Tran M) .: (Carrier (v |-- A)) or y in Carrier F )
assume A23: y in (Mx2Tran M) .: (Carrier (v |-- A)) ; ::_thesis: y in Carrier F
then consider x being set such that
A24: x in dom (Mx2Tran M) and
A25: x in Carrier (v |-- A) and
A26: (Mx2Tran M) . x = y by FUNCT_1:def_6;
reconsider x = x as Element of (TOP-REAL n) by A24;
A27: (v |-- A) . x <> 0 by A25, RLVECT_2:19;
reconsider f = y as Element of (TOP-REAL m) by A23;
S1[f,F . f] by A16;
then F . f = (v |-- A) . x by A24, A26, FUNCT_1:def_3;
hence y in Carrier F by A27, RLVECT_2:19; ::_thesis: verum
end;
Carrier F c= (Mx2Tran M) .: (Carrier (v |-- A))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier F or x in (Mx2Tran M) .: (Carrier (v |-- A)) )
assume A28: x in Carrier F ; ::_thesis: x in (Mx2Tran M) .: (Carrier (v |-- A))
then reconsider w = x as Element of (TOP-REAL m) ;
F . w <> 0 by A28, RLVECT_2:19;
hence x in (Mx2Tran M) .: (Carrier (v |-- A)) by A17; ::_thesis: verum
end;
then A29: Carrier F = (Mx2Tran M) .: (Carrier (v |-- A)) by A22, XBOOLE_0:def_10;
Carrier (v |-- A) c= A by RLVECT_2:def_6;
then (Mx2Tran M) .: (Carrier (v |-- A)) c= (Mx2Tran M) .: A by RELAT_1:123;
then reconsider F = F as Linear_Combination of (Mx2Tran M) .: A by A29, RLVECT_2:def_6;
set Fm = F (#) MTR;
consider fm being Function of NAT,(TOP-REAL m) such that
A30: Sum (F (#) MTR) = fm . (len (F (#) MTR)) and
A31: fm . 0 = 0. (TOP-REAL m) and
A32: for j being Element of NAT
for v being Element of (TOP-REAL m) st j < len (F (#) MTR) & v = (F (#) MTR) . (j + 1) holds
fm . (j + 1) = (fm . j) + v by RLVECT_1:def_12;
A33: rng MTR = (Mx2Tran M) .: (Carrier (v |-- A)) by A4, RELAT_1:127;
dom (v |-- A) = [#] (TOP-REAL n) by FUNCT_2:def_1;
then A34: len ((v |-- A) * H) = len H by A4, FINSEQ_2:29;
set vAH = (v |-- A) (#) H;
consider h being Function of NAT,(TOP-REAL n) such that
A35: Sum ((v |-- A) (#) H) = h . (len ((v |-- A) (#) H)) and
A36: h . 0 = 0. (TOP-REAL n) and
A37: for j being Element of NAT
for v being Element of (TOP-REAL n) st j < len ((v |-- A) (#) H) & v = ((v |-- A) (#) H) . (j + 1) holds
h . (j + 1) = (h . j) + v by RLVECT_1:def_12;
A38: len ((v |-- A) (#) H) = len H by RLVECT_2:def_7;
defpred S2[ Nat] means ( $1 <= len (F (#) MTR) implies fm . $1 = (Mx2Tran M) . (h . $1) );
A39: len (F (#) MTR) = len MTR by RLVECT_2:def_7;
A40: (Mx2Tran M) .: (Carrier (v |-- A)) c= rng (Mx2Tran M) by RELAT_1:111;
A41: for j being Nat st S2[j] holds
S2[j + 1]
proof
reconsider TRM = TOP-REAL m as RealLinearSpace ;
reconsider TRN = TOP-REAL n as RealLinearSpace ;
let j be Nat; ::_thesis: ( S2[j] implies S2[j + 1] )
reconsider J = j as Element of NAT by ORDINAL1:def_12;
set j1 = J + 1;
assume A42: S2[j] ; ::_thesis: S2[j + 1]
reconsider MTRj1 = MTR /. (J + 1) as Element of TRM ;
reconsider hj1 = H /. (J + 1) as n -element real-valued FinSequence ;
reconsider Hj1 = H /. (J + 1) as Element of TRN ;
assume A43: j + 1 <= len (F (#) MTR) ; ::_thesis: fm . (j + 1) = (Mx2Tran M) . (h . (j + 1))
A44: 1 <= J + 1 by NAT_1:11;
then A45: J + 1 in dom MTR by A39, A43, FINSEQ_3:25;
then A46: MTRj1 = MTR . (J + 1) by PARTFUN1:def_6;
A47: MTR . (J + 1) in (Mx2Tran M) .: (Carrier (v |-- A)) by A33, A45, FUNCT_1:def_3;
J + 1 in dom H by A39, A8, A43, A44, FINSEQ_3:25;
then A48: Hj1 = H . (J + 1) by PARTFUN1:def_6;
then MTR . (J + 1) = (Mx2Tran M) . Hj1 by A45, FUNCT_1:12;
then A49: F . MTRj1 = (v |-- A) . Hj1 by A16, A40, A46, A47;
A50: J + 1 in dom ((v |-- A) (#) H) by A39, A38, A8, A43, A44, FINSEQ_3:25;
then ((v |-- A) (#) H) . (J + 1) in rng ((v |-- A) (#) H) by FUNCT_1:def_3;
then reconsider vAHj1 = ((v |-- A) (#) H) . (J + 1) as Element of (TOP-REAL n) ;
A51: J + 1 in dom (F (#) MTR) by A43, A44, FINSEQ_3:25;
then (F (#) MTR) . (J + 1) in rng (F (#) MTR) by FUNCT_1:def_3;
then reconsider Fmj1 = (F (#) MTR) . (J + 1) as Element of (TOP-REAL m) ;
A52: (Mx2Tran M) . vAHj1 = (Mx2Tran M) . (((v |-- A) . Hj1) * Hj1) by A50, RLVECT_2:def_7
.= (Mx2Tran M) . (((v |-- A) . Hj1) * hj1) by EUCLID:65
.= ((v |-- A) . Hj1) * ((Mx2Tran M) . hj1) by MATRTOP1:23
.= (F . MTRj1) * MTRj1 by A45, A48, A46, A49, EUCLID:65, FUNCT_1:12
.= Fmj1 by A51, RLVECT_2:def_7 ;
A53: j < len (F (#) MTR) by A43, NAT_1:13;
then h . (J + 1) = (h . J) + vAHj1 by A37, A39, A38, A8;
hence (Mx2Tran M) . (h . (j + 1)) = ((Mx2Tran M) . (h . J)) + ((Mx2Tran M) . vAHj1) by MATRTOP1:27
.= fm . (j + 1) by A32, A52, A53, A42 ;
::_thesis: verum
end;
A54: S2[ 0 ] by A36, A31, MATRTOP1:29;
for j being Nat holds S2[j] from NAT_1:sch_2(A54, A41);
then Sum (F (#) MTR) = (Mx2Tran M) . (Sum ((v |-- A) (#) H)) by A35, A30, A39, A38, A8;
then A55: Sum F = (Mx2Tran M) . v by A9, A29, A3, A5, A6, A33, RLVECT_2:def_8;
A56: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_H_holds_
(F_*_MTR)_._i_=_((v_|--_A)_*_H)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len H implies (F * MTR) . i = ((v |-- A) * H) . i )
assume A57: ( 1 <= i & i <= len H ) ; ::_thesis: (F * MTR) . i = ((v |-- A) * H) . i
then A58: i in dom H by FINSEQ_3:25;
then A59: ((v |-- A) * H) . i = (v |-- A) . (H . i) by FUNCT_1:13;
H . i in rng H by A58, FUNCT_1:def_3;
then reconsider Hi = H . i as Element of (TOP-REAL n) ;
A60: MTR . i = (Mx2Tran M) . (H . i) by A58, FUNCT_1:13;
A61: i in dom MTR by A8, A57, FINSEQ_3:25;
then A62: MTR . i in rng MTR by FUNCT_1:def_3;
(F * MTR) . i = F . (MTR . i) by A61, FUNCT_1:13;
then S1[(Mx2Tran M) . Hi,(F * MTR) . i] by A16, A60;
hence (F * MTR) . i = ((v |-- A) * H) . i by A33, A40, A59, A60, A62; ::_thesis: verum
end;
dom F = [#] (TOP-REAL m) by FUNCT_2:def_1;
then len (F * MTR) = len MTR by A33, FINSEQ_2:29;
then (v |-- A) * H = F * MTR by A8, A34, A56, FINSEQ_1:14;
then Sum (F * MTR) = sum (v |-- A) by A3, A4, RLAFFIN1:def_3
.= 1 by A2, RLAFFIN1:def_7 ;
then A63: sum F = 1 by A9, A29, A3, A33, RLAFFIN1:def_3;
then Sum F in { (Sum L) where L is Linear_Combination of (Mx2Tran M) .: A : sum L = 1 } ;
hence A64: (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) by A55, RLAFFIN1:59; ::_thesis: for f being n -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f)
let f be n -element real-valued FinSequence; ::_thesis: (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f)
f is Element of (TOP-REAL n) by Lm3;
then A65: (Mx2Tran M) . f in rng (Mx2Tran M) by A7, FUNCT_1:def_3;
(Mx2Tran M) .: A is affinely-independent by A1, Th24;
then F = ((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A) by A55, A63, A64, RLAFFIN1:def_7;
hence (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) by A16, A65; ::_thesis: verum
end;
theorem Th26: :: MATRTOP2:26
for m, n being Nat
for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (TOP-REAL m) st the_rank_of M = n holds
(Mx2Tran M) " A is linearly-independent
proof
let m, n be Nat; ::_thesis: for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (TOP-REAL m) st the_rank_of M = n holds
(Mx2Tran M) " A is linearly-independent
let M be Matrix of n,m,F_Real; ::_thesis: for A being linearly-independent Subset of (TOP-REAL m) st the_rank_of M = n holds
(Mx2Tran M) " A is linearly-independent
let A be linearly-independent Subset of (TOP-REAL m); ::_thesis: ( the_rank_of M = n implies (Mx2Tran M) " A is linearly-independent )
assume A1: the_rank_of M = n ; ::_thesis: (Mx2Tran M) " A is linearly-independent
set nV = n -VectSp_over F_Real;
set mV = m -VectSp_over F_Real;
reconsider Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
reconsider A1 = A as Subset of (m -VectSp_over F_Real) by Lm1;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
len Bn = n by MATRTOP1:19;
then reconsider M1 = M as Matrix of len Bn, len Bm,F_Real by MATRTOP1:19;
set MT = Mx2Tran (M1,Bn,Bm);
A2: Mx2Tran M = Mx2Tran (M1,Bn,Bm) by MATRTOP1:20;
A3: Mx2Tran (M1,Bn,Bm) is one-to-one by A1, A2, MATRTOP1:39;
reconsider R = A /\ (rng (Mx2Tran (M1,Bn,Bm))) as Subset of (m -VectSp_over F_Real) ;
A4: R c= A by XBOOLE_1:17;
A1 is linearly-independent by Th7;
then A5: ( dom (Mx2Tran (M1,Bn,Bm)) = [#] (n -VectSp_over F_Real) & R is linearly-independent ) by A4, FUNCT_2:def_1, VECTSP_7:1;
(Mx2Tran (M1,Bn,Bm)) " R is linearly-independent
proof
assume not (Mx2Tran (M1,Bn,Bm)) " R is linearly-independent ; ::_thesis: contradiction
then consider L being Linear_Combination of (Mx2Tran (M1,Bn,Bm)) " R such that
A6: Carrier L <> {} and
A7: Sum L = 0. (n -VectSp_over F_Real) by RANKNULL:41;
set C = Carrier L;
A8: Carrier L c= (Mx2Tran (M1,Bn,Bm)) " R by VECTSP_6:def_4;
( (Mx2Tran (M1,Bn,Bm)) .: ((Mx2Tran (M1,Bn,Bm)) " R) = R & (Mx2Tran (M1,Bn,Bm)) @ L is Linear_Combination of (Mx2Tran (M1,Bn,Bm)) .: (Carrier L) ) by FUNCT_1:77, RANKNULL:29, XBOOLE_1:17;
then A9: (Mx2Tran (M1,Bn,Bm)) @ L is Linear_Combination of R by A8, RELAT_1:123, VECTSP_6:4;
(Mx2Tran (M1,Bn,Bm)) | (Carrier L) is one-to-one by A3, FUNCT_1:52;
then A10: Carrier ((Mx2Tran (M1,Bn,Bm)) @ L) = (Mx2Tran (M1,Bn,Bm)) .: (Carrier L) by RANKNULL:39;
(Mx2Tran (M1,Bn,Bm)) | ((Mx2Tran (M1,Bn,Bm)) " R) is one-to-one by A3, FUNCT_1:52;
then Sum ((Mx2Tran (M1,Bn,Bm)) @ L) = (Mx2Tran (M1,Bn,Bm)) . (Sum L) by Th14
.= 0. (m -VectSp_over F_Real) by A7, RANKNULL:9 ;
hence contradiction by A5, A6, A10, A9, VECTSP_7:def_1; ::_thesis: verum
end;
then (Mx2Tran (M1,Bn,Bm)) " A is linearly-independent by RELAT_1:133;
hence (Mx2Tran M) " A is linearly-independent by A2, Th7; ::_thesis: verum
end;
theorem :: MATRTOP2:27
for m, n being Nat
for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL m) st the_rank_of M = n holds
(Mx2Tran M) " A is affinely-independent
proof
let m, n be Nat; ::_thesis: for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL m) st the_rank_of M = n holds
(Mx2Tran M) " A is affinely-independent
let M be Matrix of n,m,F_Real; ::_thesis: for A being affinely-independent Subset of (TOP-REAL m) st the_rank_of M = n holds
(Mx2Tran M) " A is affinely-independent
set MT = Mx2Tran M;
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
let A be affinely-independent Subset of (TOP-REAL m); ::_thesis: ( the_rank_of M = n implies (Mx2Tran M) " A is affinely-independent )
assume A1: the_rank_of M = n ; ::_thesis: (Mx2Tran M) " A is affinely-independent
reconsider R = A /\ (rng (Mx2Tran M)) as affinely-independent Subset of (TOP-REAL m) by RLAFFIN1:43, XBOOLE_1:17;
A2: (Mx2Tran M) " A = (Mx2Tran M) " (A /\ (rng (Mx2Tran M))) by RELAT_1:133;
percases ( R is empty or not R is empty ) ;
suppose R is empty ; ::_thesis: (Mx2Tran M) " A is affinely-independent
then (Mx2Tran M) " A is empty by A2;
hence (Mx2Tran M) " A is affinely-independent ; ::_thesis: verum
end;
suppose not R is empty ; ::_thesis: (Mx2Tran M) " A is affinely-independent
then consider v being Element of (TOP-REAL m) such that
A3: v in R and
A4: ((- v) + R) \ {(0. (TOP-REAL m))} is linearly-independent by RLAFFIN1:def_4;
v in rng (Mx2Tran M) by A3, XBOOLE_0:def_4;
then consider x being set such that
A5: x in dom (Mx2Tran M) and
A6: (Mx2Tran M) . x = v by FUNCT_1:def_3;
reconsider x = x as Element of (TOP-REAL n) by A5;
- x = (0. (TOP-REAL n)) - x by RLVECT_1:14;
then A7: (Mx2Tran M) . (- x) = ((Mx2Tran M) . (0. (TOP-REAL n))) - ((Mx2Tran M) . x) by MATRTOP1:28
.= (0. (TOP-REAL m)) - ((Mx2Tran M) . x) by MATRTOP1:29
.= - v by A6, RLVECT_1:14 ;
A8: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def_1;
(Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m) by MATRTOP1:29;
then A9: {(0. (TOP-REAL m))} = Im ((Mx2Tran M),(0. (TOP-REAL n))) by A8, FUNCT_1:59
.= (Mx2Tran M) .: {(0. (TOP-REAL n))} by RELAT_1:def_16 ;
Mx2Tran M is one-to-one by A1, MATRTOP1:39;
then A10: (Mx2Tran M) " {(0. (TOP-REAL m))} c= {(0. (TOP-REAL n))} by A9, FUNCT_1:82;
{(0. (TOP-REAL n))} c= [#] (TOP-REAL n) by ZFMISC_1:31;
then {(0. (TOP-REAL n))} c= (Mx2Tran M) " {(0. (TOP-REAL m))} by A8, A9, FUNCT_1:76;
then (Mx2Tran M) " {(0. (TOP-REAL m))} = {(0. (TOP-REAL n))} by A10, XBOOLE_0:def_10;
then (Mx2Tran M) " (((- v) + R) \ {(0. (TOP-REAL m))}) = ((Mx2Tran M) " ((- v) + R)) \ {(0. (TOP-REAL n))} by FUNCT_1:69
.= ((- x) + ((Mx2Tran M) " R)) \ {(0. (TOP-REAL n))} by A7, MATRTOP1:31 ;
then A11: ((- x) + ((Mx2Tran M) " R)) \ {(0. (TOP-REAL n))} is linearly-independent by A1, A4, Th26;
x in (Mx2Tran M) " R by A3, A5, A6, FUNCT_1:def_7;
hence (Mx2Tran M) " A is affinely-independent by A2, A11, RLAFFIN1:def_4; ::_thesis: verum
end;
end;
end;