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

for EN being Enumeration of Affn st 0* n in Affn & EN . (len EN) = 0* n holds

( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for EN being Enumeration of Affn st 0* n in Affn & EN . (len EN) = 0* n holds

( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )

let EN be Enumeration of Affn; :: thesis: ( 0* n in Affn & EN . (len EN) = 0* n implies ( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A ) ) )

set A = Affn;

set E = EN;

assume that

A1: 0* n in Affn and

A2: EN . (len EN) = 0* n ; :: thesis: ( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )

A3: card Affn >= 1 by A1, NAT_1:14;

set cA = (card Affn) -' 1;

A4: rng EN = Affn by Def1;

(card Affn) -' 1 = (card Affn) - 1 by A1, NAT_1:14, XREAL_1:233;

then A5: len EN = ((card Affn) -' 1) + 1 by A4, FINSEQ_4:62;

A6: len EN = card Affn by A4, FINSEQ_4:62;

A7: not 0* n in rng (EN | ((card Affn) -' 1))

then A12: Affn = (rng (EN | ((card Affn) -' 1))) \/ (rng <*(EN . (len EN))*>) by A4, FINSEQ_1:31

.= (rng (EN | ((card Affn) -' 1))) \/ {(0* n)} by A2, FINSEQ_1:38 ;

hence A13: Affn \ {(0* n)} = rng (EN | ((card Affn) -' 1)) by A7, ZFMISC_1:117; :: thesis: for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A

let A1 be Subset of (n -VectSp_over F_Real); :: thesis: ( Affn = A1 implies EN | ((card Affn) -' 1) is OrdBasis of Lin A1 )

assume A14: Affn = A1 ; :: thesis: EN | ((card Affn) -' 1) is OrdBasis of Lin A1

A1 c= [#] (Lin A1)

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

then Affn \ {(0* n)} is linearly-independent by A1, RLAFFIN1:46;

then A1 \ {(0* n)} is linearly-independent by A14, MATRTOP2:7;

then A15: rng (e | ((card Affn) -' 1)) is linearly-independent by A14, A13, VECTSP_9:12;

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

.= [#] (Lin (Affn \ {(0. (TOP-REAL n))})) by Lm2

.= [#] (Lin (Affn \ {(0* n)})) by EUCLID:66

.= [#] (Lin (A1 \ {(0* n)})) by A14, MATRTOP2:6 ;

then Lin A1 = Lin (A1 \ {(0* n)}) by VECTSP_4:29

.= Lin (rng (e | ((card Affn) -' 1))) by A12, A7, A14, VECTSP_9:17, ZFMISC_1:117 ;

then ( e | ((card Affn) -' 1) is one-to-one & rng (e | ((card Affn) -' 1)) is Basis of (Lin A1) ) by A15, FUNCT_1:52, VECTSP_7:def 3;

hence EN | ((card Affn) -' 1) is OrdBasis of Lin A1 by MATRLIN:def 2; :: thesis: verum

for EN being Enumeration of Affn st 0* n in Affn & EN . (len EN) = 0* n holds

( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for EN being Enumeration of Affn st 0* n in Affn & EN . (len EN) = 0* n holds

( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )

let EN be Enumeration of Affn; :: thesis: ( 0* n in Affn & EN . (len EN) = 0* n implies ( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A ) ) )

set A = Affn;

set E = EN;

assume that

A1: 0* n in Affn and

A2: EN . (len EN) = 0* n ; :: thesis: ( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )

A3: card Affn >= 1 by A1, NAT_1:14;

set cA = (card Affn) -' 1;

A4: rng EN = Affn by Def1;

(card Affn) -' 1 = (card Affn) - 1 by A1, NAT_1:14, XREAL_1:233;

then A5: len EN = ((card Affn) -' 1) + 1 by A4, FINSEQ_4:62;

A6: len EN = card Affn by A4, FINSEQ_4:62;

A7: not 0* n in rng (EN | ((card Affn) -' 1))

proof

EN = (EN | ((card Affn) -' 1)) ^ <*(EN . (len EN))*>
by A5, FINSEQ_3:55;
A8:
len EN in dom EN
by A6, A3, FINSEQ_3:25;

assume 0* n in rng (EN | ((card Affn) -' 1)) ; :: thesis: contradiction

then consider x being object such that

A9: x in dom (EN | ((card Affn) -' 1)) and

A10: (EN | ((card Affn) -' 1)) . x = 0* n by FUNCT_1:def 3;

A11: x in Seg ((card Affn) -' 1) by A9, RELAT_1:57;

( x in dom EN & (EN | ((card Affn) -' 1)) . x = EN . x ) by A9, FUNCT_1:47, RELAT_1:57;

then x = ((card Affn) -' 1) + 1 by A2, A5, A10, A8, FUNCT_1:def 4;

then ((card Affn) -' 1) + 1 <= (card Affn) -' 1 by A11, FINSEQ_1:1;

hence contradiction by NAT_1:13; :: thesis: verum

end;assume 0* n in rng (EN | ((card Affn) -' 1)) ; :: thesis: contradiction

then consider x being object such that

A9: x in dom (EN | ((card Affn) -' 1)) and

A10: (EN | ((card Affn) -' 1)) . x = 0* n by FUNCT_1:def 3;

A11: x in Seg ((card Affn) -' 1) by A9, RELAT_1:57;

( x in dom EN & (EN | ((card Affn) -' 1)) . x = EN . x ) by A9, FUNCT_1:47, RELAT_1:57;

then x = ((card Affn) -' 1) + 1 by A2, A5, A10, A8, FUNCT_1:def 4;

then ((card Affn) -' 1) + 1 <= (card Affn) -' 1 by A11, FINSEQ_1:1;

hence contradiction by NAT_1:13; :: thesis: verum

then A12: Affn = (rng (EN | ((card Affn) -' 1))) \/ (rng <*(EN . (len EN))*>) by A4, FINSEQ_1:31

.= (rng (EN | ((card Affn) -' 1))) \/ {(0* n)} by A2, FINSEQ_1:38 ;

hence A13: Affn \ {(0* n)} = rng (EN | ((card Affn) -' 1)) by A7, ZFMISC_1:117; :: thesis: for A being Subset of (n -VectSp_over F_Real) st Affn = A holds

EN | ((card Affn) -' 1) is OrdBasis of Lin A

let A1 be Subset of (n -VectSp_over F_Real); :: thesis: ( Affn = A1 implies EN | ((card Affn) -' 1) is OrdBasis of Lin A1 )

assume A14: Affn = A1 ; :: thesis: EN | ((card Affn) -' 1) is OrdBasis of Lin A1

A1 c= [#] (Lin A1)

proof

then reconsider e = EN as FinSequence of (Lin A1) by A4, A14, FINSEQ_1:def 4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A1 or x in [#] (Lin A1) )

assume x in A1 ; :: thesis: x in [#] (Lin A1)

then x in Lin A1 by VECTSP_7:8;

hence x in [#] (Lin A1) ; :: thesis: verum

end;assume x in A1 ; :: thesis: x in [#] (Lin A1)

then x in Lin A1 by VECTSP_7:8;

hence x in [#] (Lin A1) ; :: thesis: verum

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

then Affn \ {(0* n)} is linearly-independent by A1, RLAFFIN1:46;

then A1 \ {(0* n)} is linearly-independent by A14, MATRTOP2:7;

then A15: rng (e | ((card Affn) -' 1)) is linearly-independent by A14, A13, VECTSP_9:12;

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

.= [#] (Lin (Affn \ {(0. (TOP-REAL n))})) by Lm2

.= [#] (Lin (Affn \ {(0* n)})) by EUCLID:66

.= [#] (Lin (A1 \ {(0* n)})) by A14, MATRTOP2:6 ;

then Lin A1 = Lin (A1 \ {(0* n)}) by VECTSP_4:29

.= Lin (rng (e | ((card Affn) -' 1))) by A12, A7, A14, VECTSP_9:17, ZFMISC_1:117 ;

then ( e | ((card Affn) -' 1) is one-to-one & rng (e | ((card Affn) -' 1)) is Basis of (Lin A1) ) by A15, FUNCT_1:52, VECTSP_7:def 3;

hence EN | ((card Affn) -' 1) is OrdBasis of Lin A1 by MATRLIN:def 2; :: thesis: verum