let x be set ; :: thesis: for V being RealLinearSpace

for I being affinely-independent Subset of V

for B being Subset of V st x in Affin I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )

let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V

for B being Subset of V st x in Affin I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )

let I be affinely-independent Subset of V; :: thesis: for B being Subset of V st x in Affin I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )

let B be Subset of V; :: thesis: ( x in Affin I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) implies ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) ) )

assume that

A1: x in Affin I and

A2: for y being set st y in B holds

(x |-- I) . y = 0 ; :: thesis: ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )

A3: Affin I = { (Sum L) where L is Linear_Combination of I : sum L = 1 } by Th59;

A4: I \ B is affinely-independent by Th43, XBOOLE_1:36;

consider L being Linear_Combination of I such that

A5: ( x = Sum L & sum L = 1 ) by A1, A3;

A6: x |-- I = L by A1, A5, Def7;

Carrier L c= I \ B

then x in { (Sum K) where K is Linear_Combination of I \ B : sum K = 1 } by A5;

then x in Affin (I \ B) by Th59;

hence ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) ) by A4, A5, A6, A9, Def7; :: thesis: verum

for I being affinely-independent Subset of V

for B being Subset of V st x in Affin I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )

let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V

for B being Subset of V st x in Affin I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )

let I be affinely-independent Subset of V; :: thesis: for B being Subset of V st x in Affin I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) holds

( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )

let B be Subset of V; :: thesis: ( x in Affin I & ( for y being set st y in B holds

(x |-- I) . y = 0 ) implies ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) ) )

assume that

A1: x in Affin I and

A2: for y being set st y in B holds

(x |-- I) . y = 0 ; :: thesis: ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )

A3: Affin I = { (Sum L) where L is Linear_Combination of I : sum L = 1 } by Th59;

A4: I \ B is affinely-independent by Th43, XBOOLE_1:36;

consider L being Linear_Combination of I such that

A5: ( x = Sum L & sum L = 1 ) by A1, A3;

A6: x |-- I = L by A1, A5, Def7;

Carrier L c= I \ B

proof

then A9:
L is Linear_Combination of I \ B
by RLVECT_2:def 6;
A7:
Carrier L c= I
by RLVECT_2:def 6;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Carrier L or y in I \ B )

assume A8: y in Carrier L ; :: thesis: y in I \ B

assume not y in I \ B ; :: thesis: contradiction

then y in B by A7, A8, XBOOLE_0:def 5;

then L . y = 0 by A2, A6;

hence contradiction by A8, RLVECT_2:19; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Carrier L or y in I \ B )

assume A8: y in Carrier L ; :: thesis: y in I \ B

assume not y in I \ B ; :: thesis: contradiction

then y in B by A7, A8, XBOOLE_0:def 5;

then L . y = 0 by A2, A6;

hence contradiction by A8, RLVECT_2:19; :: thesis: verum

then x in { (Sum K) where K is Linear_Combination of I \ B : sum K = 1 } by A5;

then x in Affin (I \ B) by Th59;

hence ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) ) by A4, A5, A6, A9, Def7; :: thesis: verum