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