let n be Nat; :: thesis: for Affn being affinely-independent Subset of (TOP-REAL n)

for EN being Enumeration of Affn

for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds

for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for EN being Enumeration of Affn

for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds

for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

let EN be Enumeration of Affn; :: thesis: for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds

for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

reconsider Z = 0 as Element of REAL by Lm5;

set TR = TOP-REAL n;

set A = Affn;

set V = n -VectSp_over F_Real;

set E = EN;

let A1 be Subset of (n -VectSp_over F_Real); :: thesis: ( Affn = A1 & 0* n in Affn & EN . (len EN) = 0* n implies for B being OrdBasis of Lin A1 st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1) )

assume that

A1: Affn = A1 and

A2: 0* n in Affn and

A3: EN . (len EN) = 0* n ; :: thesis: for B being OrdBasis of Lin A1 st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

deffunc H_{1}( set ) -> Element of REAL = Z;

A4: Affin Affn = [#] (Lin Affn) by A2, Th11;

set cA = (card Affn) -' 1;

let B be OrdBasis of Lin A1; :: thesis: ( B = EN | ((card Affn) -' 1) implies for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1) )

assume A5: B = EN | ((card Affn) -' 1) ; :: thesis: for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

A6: rng B = Affn \ {(0* n)} by A2, A3, A5, Th23;

then reconsider rB = rng B as Subset of (TOP-REAL n) ;

let v be Element of (Lin A1); :: thesis: v |-- B = (v |-- EN) | ((card Affn) -' 1)

set vB = v |-- B;

consider KV being Linear_Combination of Lin A1 such that

A7: v = Sum KV and

A8: Carrier KV c= rng B and

A9: for k being Nat st 1 <= k & k <= len (v |-- B) holds

(v |-- B) /. k = KV . (B /. k) by MATRLIN:def 7;

A10: (v |-- EN) | ((card Affn) -' 1) = (v |-- Affn) * (EN | ((card Affn) -' 1)) by RELAT_1:83;

dom (v |-- Affn) = [#] (TOP-REAL n) by FUNCT_2:def 1;

then rB c= dom (v |-- Affn) ;

then A11: len ((v |-- EN) | ((card Affn) -' 1)) = len B by A5, A10, FINSEQ_2:29;

A12: [#] (Lin A1) = [#] (Lin Affn) by A1, MATRTOP2:6;

then reconsider RB = rB as Subset of (Lin Affn) ;

reconsider KR = KV as Linear_Combination of Lin Affn by A12, MATRTOP2:11;

A13: Carrier KR = Carrier KV by MATRTOP2:12;

consider KR1 being Linear_Combination of TOP-REAL n such that

A14: Carrier KR1 = Carrier KR and

A15: Sum KR1 = Sum KR by RLVECT_5:11;

rng B c= Affn by A6, XBOOLE_1:36;

then A16: Carrier KR1 c= Affn by A8, A13, A14;

reconsider KR2 = KR1 | ([#] (Lin Affn)) as Linear_Combination of Lin Affn by MATRTOP2:10;

A17: ( Carrier KR2 = Carrier KR1 & Sum KR2 = Sum KR1 ) by A14, RLVECT_5:10;

reconsider KR1 = KR1 as Linear_Combination of Affn by A16, RLVECT_2:def 6;

reconsider ms = 1 - (sum KR1) as Element of REAL by XREAL_0:def 1;

consider KR0 being Function of the carrier of (TOP-REAL n),REAL such that

A18: KR0 . (0. (TOP-REAL n)) = ms and

A19: for u being Element of (TOP-REAL n) st u <> 0. (TOP-REAL n) holds

KR0 . u = H_{1}(u)
from FUNCT_2:sch 6();

reconsider KR0 = KR0 as Element of Funcs ( the carrier of (TOP-REAL n),REAL) by FUNCT_2:8;

Carrier KR0 c= {(0. (TOP-REAL n))}

A22: Carrier KR0 c= {(0. (TOP-REAL n))} by RLVECT_2:def 6;

rng B is Basis of (Lin A1) by MATRLIN:def 2;

then rng B is linearly-independent by VECTSP_7:def 3;

then rng B is linearly-independent Subset of (n -VectSp_over F_Real) by VECTSP_9:11;

then rB is linearly-independent by MATRTOP2:7;

then A23: RB is linearly-independent by RLVECT_5:15;

A24: len (v |-- B) = len B by MATRLIN:def 7;

A25: Sum KR0 = (KR0 . (0. (TOP-REAL n))) * (0. (TOP-REAL n)) by RLVECT_2:32

.= 0. (TOP-REAL n) by RLVECT_1:10 ;

A26: 0. (TOP-REAL n) = 0* n by EUCLID:66;

then {(0. (TOP-REAL n))} c= Affn by A2, ZFMISC_1:31;

then reconsider KR0 = KR0 as Linear_Combination of Affn by RLVECT_2:21;

reconsider K = KR1 + KR0 as Linear_Combination of Affn by RLVECT_2:38;

A27: sum K = (sum KR1) + (sum KR0) by RLAFFIN1:34

.= (sum KR1) + (1 - (sum KR1)) by A18, A22, RLAFFIN1:32

.= 1 ;

Sum K = (Sum KR1) + (Sum KR0) by RLVECT_3:1

.= Sum KR1 by A25, RLVECT_1:def 4

.= v by A7, A15, MATRTOP2:12 ;

then A28: v |-- Affn = K by A12, A4, A27, RLAFFIN1:def 7;

for EN being Enumeration of Affn

for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds

for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for EN being Enumeration of Affn

for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds

for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

let EN be Enumeration of Affn; :: thesis: for A being Subset of (n -VectSp_over F_Real) st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds

for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

reconsider Z = 0 as Element of REAL by Lm5;

set TR = TOP-REAL n;

set A = Affn;

set V = n -VectSp_over F_Real;

set E = EN;

let A1 be Subset of (n -VectSp_over F_Real); :: thesis: ( Affn = A1 & 0* n in Affn & EN . (len EN) = 0* n implies for B being OrdBasis of Lin A1 st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1) )

assume that

A1: Affn = A1 and

A2: 0* n in Affn and

A3: EN . (len EN) = 0* n ; :: thesis: for B being OrdBasis of Lin A1 st B = EN | ((card Affn) -' 1) holds

for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

deffunc H

A4: Affin Affn = [#] (Lin Affn) by A2, Th11;

set cA = (card Affn) -' 1;

let B be OrdBasis of Lin A1; :: thesis: ( B = EN | ((card Affn) -' 1) implies for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1) )

assume A5: B = EN | ((card Affn) -' 1) ; :: thesis: for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

A6: rng B = Affn \ {(0* n)} by A2, A3, A5, Th23;

then reconsider rB = rng B as Subset of (TOP-REAL n) ;

let v be Element of (Lin A1); :: thesis: v |-- B = (v |-- EN) | ((card Affn) -' 1)

set vB = v |-- B;

consider KV being Linear_Combination of Lin A1 such that

A7: v = Sum KV and

A8: Carrier KV c= rng B and

A9: for k being Nat st 1 <= k & k <= len (v |-- B) holds

(v |-- B) /. k = KV . (B /. k) by MATRLIN:def 7;

A10: (v |-- EN) | ((card Affn) -' 1) = (v |-- Affn) * (EN | ((card Affn) -' 1)) by RELAT_1:83;

dom (v |-- Affn) = [#] (TOP-REAL n) by FUNCT_2:def 1;

then rB c= dom (v |-- Affn) ;

then A11: len ((v |-- EN) | ((card Affn) -' 1)) = len B by A5, A10, FINSEQ_2:29;

A12: [#] (Lin A1) = [#] (Lin Affn) by A1, MATRTOP2:6;

then reconsider RB = rB as Subset of (Lin Affn) ;

reconsider KR = KV as Linear_Combination of Lin Affn by A12, MATRTOP2:11;

A13: Carrier KR = Carrier KV by MATRTOP2:12;

consider KR1 being Linear_Combination of TOP-REAL n such that

A14: Carrier KR1 = Carrier KR and

A15: Sum KR1 = Sum KR by RLVECT_5:11;

rng B c= Affn by A6, XBOOLE_1:36;

then A16: Carrier KR1 c= Affn by A8, A13, A14;

reconsider KR2 = KR1 | ([#] (Lin Affn)) as Linear_Combination of Lin Affn by MATRTOP2:10;

A17: ( Carrier KR2 = Carrier KR1 & Sum KR2 = Sum KR1 ) by A14, RLVECT_5:10;

reconsider KR1 = KR1 as Linear_Combination of Affn by A16, RLVECT_2:def 6;

reconsider ms = 1 - (sum KR1) as Element of REAL by XREAL_0:def 1;

consider KR0 being Function of the carrier of (TOP-REAL n),REAL such that

A18: KR0 . (0. (TOP-REAL n)) = ms and

A19: for u being Element of (TOP-REAL n) st u <> 0. (TOP-REAL n) holds

KR0 . u = H

reconsider KR0 = KR0 as Element of Funcs ( the carrier of (TOP-REAL n),REAL) by FUNCT_2:8;

now :: thesis: for u being VECTOR of (TOP-REAL n) st not u in {(0. (TOP-REAL n))} holds

KR0 . u = 0

then reconsider KR0 = KR0 as Linear_Combination of TOP-REAL n by RLVECT_2:def 3;KR0 . u = 0

let u be VECTOR of (TOP-REAL n); :: thesis: ( not u in {(0. (TOP-REAL n))} implies KR0 . u = 0 )

assume not u in {(0. (TOP-REAL n))} ; :: thesis: KR0 . u = 0

then u <> 0. (TOP-REAL n) by TARSKI:def 1;

hence KR0 . u = 0 by A19; :: thesis: verum

end;assume not u in {(0. (TOP-REAL n))} ; :: thesis: KR0 . u = 0

then u <> 0. (TOP-REAL n) by TARSKI:def 1;

hence KR0 . u = 0 by A19; :: thesis: verum

Carrier KR0 c= {(0. (TOP-REAL n))}

proof

then reconsider KR0 = KR0 as Linear_Combination of {(0. (TOP-REAL n))} by RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier KR0 or x in {(0. (TOP-REAL n))} )

assume that

A20: x in Carrier KR0 and

A21: not x in {(0. (TOP-REAL n))} ; :: thesis: contradiction

( KR0 . x <> 0 & x <> 0. (TOP-REAL n) ) by A20, A21, RLVECT_2:19, TARSKI:def 1;

hence contradiction by A19, A20; :: thesis: verum

end;assume that

A20: x in Carrier KR0 and

A21: not x in {(0. (TOP-REAL n))} ; :: thesis: contradiction

( KR0 . x <> 0 & x <> 0. (TOP-REAL n) ) by A20, A21, RLVECT_2:19, TARSKI:def 1;

hence contradiction by A19, A20; :: thesis: verum

A22: Carrier KR0 c= {(0. (TOP-REAL n))} by RLVECT_2:def 6;

rng B is Basis of (Lin A1) by MATRLIN:def 2;

then rng B is linearly-independent by VECTSP_7:def 3;

then rng B is linearly-independent Subset of (n -VectSp_over F_Real) by VECTSP_9:11;

then rB is linearly-independent by MATRTOP2:7;

then A23: RB is linearly-independent by RLVECT_5:15;

A24: len (v |-- B) = len B by MATRLIN:def 7;

A25: Sum KR0 = (KR0 . (0. (TOP-REAL n))) * (0. (TOP-REAL n)) by RLVECT_2:32

.= 0. (TOP-REAL n) by RLVECT_1:10 ;

A26: 0. (TOP-REAL n) = 0* n by EUCLID:66;

then {(0. (TOP-REAL n))} c= Affn by A2, ZFMISC_1:31;

then reconsider KR0 = KR0 as Linear_Combination of Affn by RLVECT_2:21;

reconsider K = KR1 + KR0 as Linear_Combination of Affn by RLVECT_2:38;

A27: sum K = (sum KR1) + (sum KR0) by RLAFFIN1:34

.= (sum KR1) + (1 - (sum KR1)) by A18, A22, RLAFFIN1:32

.= 1 ;

Sum K = (Sum KR1) + (Sum KR0) by RLVECT_3:1

.= Sum KR1 by A25, RLVECT_1:def 4

.= v by A7, A15, MATRTOP2:12 ;

then A28: v |-- Affn = K by A12, A4, A27, RLAFFIN1:def 7;

now :: thesis: for k being Nat st 1 <= k & k <= len B holds

((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k

hence
v |-- B = (v |-- EN) | ((card Affn) -' 1)
by A24, A11; :: thesis: verum((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len B implies ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k )

reconsider Bk = B /. k as Element of (TOP-REAL n) by A12, RLSUB_1:10;

assume A29: ( 1 <= k & k <= len B ) ; :: thesis: ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k

then A30: ( (v |-- B) /. k = KV . Bk & k in dom ((v |-- EN) | ((card Affn) -' 1)) ) by A24, A9, A11, FINSEQ_3:25;

A31: k in dom B by A29, FINSEQ_3:25;

then A32: Bk = B . k by PARTFUN1:def 6;

then Bk in rng B by A31, FUNCT_1:def 3;

then Bk <> 0. (TOP-REAL n) by A6, A26, ZFMISC_1:56;

then not Bk in Carrier KR0 by A22, TARSKI:def 1;

then A33: KR0 . Bk = 0 by RLVECT_2:19;

k in dom (v |-- B) by A24, A29, FINSEQ_3:25;

then A34: (v |-- B) . k = (v |-- B) /. k by PARTFUN1:def 6;

K . Bk = (KR1 . Bk) + (KR0 . Bk) by RLVECT_2:def 10;

then K . Bk = KR2 . Bk by A12, A33, FUNCT_1:49

.= KV . Bk by A23, A8, A13, A14, A15, A17, RLVECT_5:1 ;

hence ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k by A5, A28, A10, A30, A34, A32, FUNCT_1:12; :: thesis: verum

end;reconsider Bk = B /. k as Element of (TOP-REAL n) by A12, RLSUB_1:10;

assume A29: ( 1 <= k & k <= len B ) ; :: thesis: ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k

then A30: ( (v |-- B) /. k = KV . Bk & k in dom ((v |-- EN) | ((card Affn) -' 1)) ) by A24, A9, A11, FINSEQ_3:25;

A31: k in dom B by A29, FINSEQ_3:25;

then A32: Bk = B . k by PARTFUN1:def 6;

then Bk in rng B by A31, FUNCT_1:def 3;

then Bk <> 0. (TOP-REAL n) by A6, A26, ZFMISC_1:56;

then not Bk in Carrier KR0 by A22, TARSKI:def 1;

then A33: KR0 . Bk = 0 by RLVECT_2:19;

k in dom (v |-- B) by A24, A29, FINSEQ_3:25;

then A34: (v |-- B) . k = (v |-- B) /. k by PARTFUN1:def 6;

K . Bk = (KR1 . Bk) + (KR0 . Bk) by RLVECT_2:def 10;

then K . Bk = KR2 . Bk by A12, A33, FUNCT_1:49

.= KV . Bk by A23, A8, A13, A14, A15, A17, RLVECT_5:1 ;

hence ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k by A5, A28, A10, A30, A34, A32, FUNCT_1:12; :: thesis: verum