:: PENCIL_4 semantic presentation
begin
theorem Th1: :: PENCIL_4:1
for k, n being Nat st k < n & 3 <= n & not k + 1 < n holds
2 <= k
proof
let k, n be Nat; ::_thesis: ( k < n & 3 <= n & not k + 1 < n implies 2 <= k )
assume that
A1: k < n and
A2: 3 <= n ; ::_thesis: ( k + 1 < n or 2 <= k )
assume A3: k + 1 >= n ; ::_thesis: 2 <= k
k + 1 <= n by A1, NAT_1:13;
then 3 <= k + 1 by A2, A3, XXREAL_0:1;
then 3 - 1 <= (k + 1) - 1 by XREAL_1:9;
hence 2 <= k ; ::_thesis: verum
end;
Lm1: for X being finite set
for n being Nat st n <= card X holds
ex Y being Subset of X st card Y = n
by FINSEQ_4:72;
theorem Th2: :: PENCIL_4:2
for F being Field
for V being VectSp of F
for W being Subspace of V holds W is Subspace of (Omega). V
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V holds W is Subspace of (Omega). V
let V be VectSp of F; ::_thesis: for W being Subspace of V holds W is Subspace of (Omega). V
let W be Subspace of V; ::_thesis: W is Subspace of (Omega). V
thus the carrier of W c= the carrier of ((Omega). V) by VECTSP_4:def_2; :: according to VECTSP_4:def_2 ::_thesis: ( 0. W = 0. ((Omega). V) & the U5 of W = K109( the U5 of ((Omega). V), the carrier of W) & the lmult of W = K5( the lmult of ((Omega). V),[: the carrier of F, the carrier of W:]) )
thus 0. W = 0. V by VECTSP_4:def_2
.= 0. ((Omega). V) ; ::_thesis: ( the U5 of W = K109( the U5 of ((Omega). V), the carrier of W) & the lmult of W = K5( the lmult of ((Omega). V),[: the carrier of F, the carrier of W:]) )
thus ( the U5 of W = K109( the U5 of ((Omega). V), the carrier of W) & the lmult of W = K5( the lmult of ((Omega). V),[: the carrier of F, the carrier of W:]) ) by VECTSP_4:def_2; ::_thesis: verum
end;
theorem Th3: :: PENCIL_4:3
for F being Field
for V being VectSp of F
for W being Subspace of (Omega). V holds W is Subspace of V
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of (Omega). V holds W is Subspace of V
let V be VectSp of F; ::_thesis: for W being Subspace of (Omega). V holds W is Subspace of V
let W be Subspace of (Omega). V; ::_thesis: W is Subspace of V
thus the carrier of W c= the carrier of V by VECTSP_4:def_2; :: according to VECTSP_4:def_2 ::_thesis: ( 0. W = 0. V & the U5 of W = K109( the U5 of V, the carrier of W) & the lmult of W = K5( the lmult of V,[: the carrier of F, the carrier of W:]) )
thus 0. W = 0. ((Omega). V) by VECTSP_4:def_2
.= 0. V ; ::_thesis: ( the U5 of W = K109( the U5 of V, the carrier of W) & the lmult of W = K5( the lmult of V,[: the carrier of F, the carrier of W:]) )
thus ( the U5 of W = K109( the U5 of V, the carrier of W) & the lmult of W = K5( the lmult of V,[: the carrier of F, the carrier of W:]) ) by VECTSP_4:def_2; ::_thesis: verum
end;
theorem Th4: :: PENCIL_4:4
for F being Field
for V being VectSp of F
for W being Subspace of V holds (Omega). W is Subspace of V
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V holds (Omega). W is Subspace of V
let V be VectSp of F; ::_thesis: for W being Subspace of V holds (Omega). W is Subspace of V
let W be Subspace of V; ::_thesis: (Omega). W is Subspace of V
thus the carrier of ((Omega). W) c= the carrier of V by VECTSP_4:def_2; :: according to VECTSP_4:def_2 ::_thesis: ( 0. ((Omega). W) = 0. V & the U5 of ((Omega). W) = K109( the U5 of V, the carrier of ((Omega). W)) & the lmult of ((Omega). W) = K5( the lmult of V,[: the carrier of F, the carrier of ((Omega). W):]) )
thus 0. ((Omega). W) = 0. W
.= 0. V by VECTSP_4:def_2 ; ::_thesis: ( the U5 of ((Omega). W) = K109( the U5 of V, the carrier of ((Omega). W)) & the lmult of ((Omega). W) = K5( the lmult of V,[: the carrier of F, the carrier of ((Omega). W):]) )
thus ( the U5 of ((Omega). W) = K109( the U5 of V, the carrier of ((Omega). W)) & the lmult of ((Omega). W) = K5( the lmult of V,[: the carrier of F, the carrier of ((Omega). W):]) ) by VECTSP_4:def_2; ::_thesis: verum
end;
theorem Th5: :: PENCIL_4:5
for F being Field
for V, W being VectSp of F st (Omega). W is Subspace of V holds
W is Subspace of V
proof
let F be Field; ::_thesis: for V, W being VectSp of F st (Omega). W is Subspace of V holds
W is Subspace of V
let V, W be VectSp of F; ::_thesis: ( (Omega). W is Subspace of V implies W is Subspace of V )
assume A1: (Omega). W is Subspace of V ; ::_thesis: W is Subspace of V
hence the carrier of W c= the carrier of V by VECTSP_4:def_2; :: according to VECTSP_4:def_2 ::_thesis: ( 0. W = 0. V & the U5 of W = K109( the U5 of V, the carrier of W) & the lmult of W = K5( the lmult of V,[: the carrier of F, the carrier of W:]) )
thus 0. W = 0. ((Omega). W)
.= 0. V by A1, VECTSP_4:def_2 ; ::_thesis: ( the U5 of W = K109( the U5 of V, the carrier of W) & the lmult of W = K5( the lmult of V,[: the carrier of F, the carrier of W:]) )
thus ( the U5 of W = K109( the U5 of V, the carrier of W) & the lmult of W = K5( the lmult of V,[: the carrier of F, the carrier of W:]) ) by A1, VECTSP_4:def_2; ::_thesis: verum
end;
definition
let F be Field;
let V be VectSp of F;
let W1, W2 be Subspace of V;
func segment (W1,W2) -> Subset of (Subspaces V) means :Def1: :: PENCIL_4:def 1
for W being strict Subspace of V holds
( W in it iff ( W1 is Subspace of W & W is Subspace of W2 ) ) if W1 is Subspace of W2
otherwise it = {} ;
consistency
for b1 being Subset of (Subspaces V) holds verum ;
existence
( ( W1 is Subspace of W2 implies ex b1 being Subset of (Subspaces V) st
for W being strict Subspace of V holds
( W in b1 iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( W1 is not Subspace of W2 implies ex b1 being Subset of (Subspaces V) st b1 = {} ) )
proof
hereby ::_thesis: ( W1 is not Subspace of W2 implies ex b1 being Subset of (Subspaces V) st b1 = {} )
defpred S1[ set ] means for W being Subspace of V st W = $1 holds
( W1 is Subspace of W & W is Subspace of W2 );
set A = Subspaces V;
assume W1 is Subspace of W2 ; ::_thesis: ex X being Subset of (Subspaces V) st
for W being strict Subspace of V holds
( ( W in X implies ( W1 is Subspace of W & W is Subspace of W2 ) ) & ( W1 is Subspace of W & W is Subspace of W2 implies W in X ) )
consider X being Subset of (Subspaces V) such that
A1: for x being set holds
( x in X iff ( x in Subspaces V & S1[x] ) ) from SUBSET_1:sch_1();
take X = X; ::_thesis: for W being strict Subspace of V holds
( ( W in X implies ( W1 is Subspace of W & W is Subspace of W2 ) ) & ( W1 is Subspace of W & W is Subspace of W2 implies W in X ) )
let W be strict Subspace of V; ::_thesis: ( ( W in X implies ( W1 is Subspace of W & W is Subspace of W2 ) ) & ( W1 is Subspace of W & W is Subspace of W2 implies W in X ) )
thus ( W in X implies ( W1 is Subspace of W & W is Subspace of W2 ) ) by A1; ::_thesis: ( W1 is Subspace of W & W is Subspace of W2 implies W in X )
assume ( W1 is Subspace of W & W is Subspace of W2 ) ; ::_thesis: W in X
then A2: S1[W] ;
W in Subspaces V by VECTSP_5:def_3;
hence W in X by A1, A2; ::_thesis: verum
end;
hereby ::_thesis: verum
reconsider W = {} as Subset of (Subspaces V) by XBOOLE_1:2;
assume W1 is not Subspace of W2 ; ::_thesis: ex W being Subset of (Subspaces V) st W = {}
take W = W; ::_thesis: W = {}
thus W = {} ; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being Subset of (Subspaces V) holds
( ( W1 is Subspace of W2 & ( for W being strict Subspace of V holds
( W in b1 iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( for W being strict Subspace of V holds
( W in b2 iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) implies b1 = b2 ) & ( W1 is not Subspace of W2 & b1 = {} & b2 = {} implies b1 = b2 ) )
proof
let S, T be Subset of (Subspaces V); ::_thesis: ( ( W1 is Subspace of W2 & ( for W being strict Subspace of V holds
( W in S iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( for W being strict Subspace of V holds
( W in T iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) implies S = T ) & ( W1 is not Subspace of W2 & S = {} & T = {} implies S = T ) )
now__::_thesis:_(_W1_is_Subspace_of_W2_&_(_for_W_being_strict_Subspace_of_V_holds_
(_W_in_S_iff_(_W1_is_Subspace_of_W_&_W_is_Subspace_of_W2_)_)_)_&_(_for_W_being_strict_Subspace_of_V_holds_
(_W_in_T_iff_(_W1_is_Subspace_of_W_&_W_is_Subspace_of_W2_)_)_)_implies_S_=_T_)
assume W1 is Subspace of W2 ; ::_thesis: ( ( for W being strict Subspace of V holds
( W in S iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( for W being strict Subspace of V holds
( W in T iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) implies S = T )
assume that
A3: for W being strict Subspace of V holds
( W in S iff ( W1 is Subspace of W & W is Subspace of W2 ) ) and
A4: for W being strict Subspace of V holds
( W in T iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ; ::_thesis: S = T
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_S_implies_x_in_T_)_&_(_x_in_T_implies_x_in_S_)_)
let x be set ; ::_thesis: ( ( x in S implies x in T ) & ( x in T implies x in S ) )
thus ( x in S implies x in T ) ::_thesis: ( x in T implies x in S )
proof
assume A5: x in S ; ::_thesis: x in T
then consider x1 being strict Subspace of V such that
A6: x1 = x by VECTSP_5:def_3;
( x1 in S iff ( W1 is Subspace of x1 & x1 is Subspace of W2 ) ) by A3;
hence x in T by A4, A5, A6; ::_thesis: verum
end;
assume A7: x in T ; ::_thesis: x in S
then consider x1 being strict Subspace of V such that
A8: x1 = x by VECTSP_5:def_3;
( x1 in T iff ( W1 is Subspace of x1 & x1 is Subspace of W2 ) ) by A4;
hence x in S by A3, A7, A8; ::_thesis: verum
end;
hence S = T by TARSKI:1; ::_thesis: verum
end;
hence ( ( W1 is Subspace of W2 & ( for W being strict Subspace of V holds
( W in S iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( for W being strict Subspace of V holds
( W in T iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) implies S = T ) & ( W1 is not Subspace of W2 & S = {} & T = {} implies S = T ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines segment PENCIL_4:def_1_:_
for F being Field
for V being VectSp of F
for W1, W2 being Subspace of V
for b5 being Subset of (Subspaces V) holds
( ( W1 is Subspace of W2 implies ( b5 = segment (W1,W2) iff for W being strict Subspace of V holds
( W in b5 iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) ) & ( W1 is not Subspace of W2 implies ( b5 = segment (W1,W2) iff b5 = {} ) ) );
theorem Th6: :: PENCIL_4:6
for F being Field
for V being VectSp of F
for W1, W2, W3, W4 being Subspace of V st W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 holds
segment (W1,W2) = segment (W3,W4)
proof
let F be Field; ::_thesis: for V being VectSp of F
for W1, W2, W3, W4 being Subspace of V st W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 holds
segment (W1,W2) = segment (W3,W4)
let V be VectSp of F; ::_thesis: for W1, W2, W3, W4 being Subspace of V st W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 holds
segment (W1,W2) = segment (W3,W4)
let W1, W2, W3, W4 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 implies segment (W1,W2) = segment (W3,W4) )
assume that
A1: W1 is Subspace of W2 and
A2: W3 is Subspace of W4 and
A3: (Omega). W1 = (Omega). W3 and
A4: (Omega). W2 = (Omega). W4 ; ::_thesis: segment (W1,W2) = segment (W3,W4)
thus segment (W1,W2) c= segment (W3,W4) :: according to XBOOLE_0:def_10 ::_thesis: segment (W3,W4) c= segment (W1,W2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in segment (W1,W2) or a in segment (W3,W4) )
assume A5: a in segment (W1,W2) ; ::_thesis: a in segment (W3,W4)
then ex A1 being strict Subspace of V st A1 = a by VECTSP_5:def_3;
then reconsider A = a as strict Subspace of V ;
A is Subspace of W2 by A1, A5, Def1;
then A is Subspace of (Omega). W2 by Th2;
then A6: A is Subspace of W4 by A4, Th3;
W1 is Subspace of A by A1, A5, Def1;
then (Omega). W1 is Subspace of A by Th4;
then W3 is Subspace of A by A3, Th5;
hence a in segment (W3,W4) by A2, A6, Def1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in segment (W3,W4) or a in segment (W1,W2) )
assume A7: a in segment (W3,W4) ; ::_thesis: a in segment (W1,W2)
then ex A1 being strict Subspace of V st A1 = a by VECTSP_5:def_3;
then reconsider A = a as strict Subspace of V ;
A is Subspace of W4 by A2, A7, Def1;
then A is Subspace of (Omega). W4 by Th2;
then A8: A is Subspace of W2 by A4, Th3;
W3 is Subspace of A by A2, A7, Def1;
then (Omega). W3 is Subspace of A by Th4;
then W1 is Subspace of A by A3, Th5;
hence a in segment (W1,W2) by A1, A8, Def1; ::_thesis: verum
end;
definition
let F be Field;
let V be VectSp of F;
let W1, W2 be Subspace of V;
func pencil (W1,W2) -> Subset of (Subspaces V) equals :: PENCIL_4:def 2
(segment (W1,W2)) \ {((Omega). W1),((Omega). W2)};
coherence
(segment (W1,W2)) \ {((Omega). W1),((Omega). W2)} is Subset of (Subspaces V) ;
end;
:: deftheorem defines pencil PENCIL_4:def_2_:_
for F being Field
for V being VectSp of F
for W1, W2 being Subspace of V holds pencil (W1,W2) = (segment (W1,W2)) \ {((Omega). W1),((Omega). W2)};
theorem :: PENCIL_4:7
for F being Field
for V being VectSp of F
for W1, W2, W3, W4 being Subspace of V st W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 holds
pencil (W1,W2) = pencil (W3,W4) by Th6;
definition
let F be Field;
let V be finite-dimensional VectSp of F;
let W1, W2 be Subspace of V;
let k be Nat;
func pencil (W1,W2,k) -> Subset of (k Subspaces_of V) equals :: PENCIL_4:def 3
(pencil (W1,W2)) /\ (k Subspaces_of V);
coherence
(pencil (W1,W2)) /\ (k Subspaces_of V) is Subset of (k Subspaces_of V) by XBOOLE_1:17;
end;
:: deftheorem defines pencil PENCIL_4:def_3_:_
for F being Field
for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V
for k being Nat holds pencil (W1,W2,k) = (pencil (W1,W2)) /\ (k Subspaces_of V);
theorem Th8: :: PENCIL_4:8
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat
for W1, W2, W being Subspace of V st W in pencil (W1,W2,k) holds
( W1 is Subspace of W & W is Subspace of W2 )
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for k being Nat
for W1, W2, W being Subspace of V st W in pencil (W1,W2,k) holds
( W1 is Subspace of W & W is Subspace of W2 )
let V be finite-dimensional VectSp of F; ::_thesis: for k being Nat
for W1, W2, W being Subspace of V st W in pencil (W1,W2,k) holds
( W1 is Subspace of W & W is Subspace of W2 )
let k be Nat; ::_thesis: for W1, W2, W being Subspace of V st W in pencil (W1,W2,k) holds
( W1 is Subspace of W & W is Subspace of W2 )
let W1, W2, W be Subspace of V; ::_thesis: ( W in pencil (W1,W2,k) implies ( W1 is Subspace of W & W is Subspace of W2 ) )
assume A1: W in pencil (W1,W2,k) ; ::_thesis: ( W1 is Subspace of W & W is Subspace of W2 )
then A2: ex X being strict Subspace of V st
( W = X & dim X = k ) by VECTSP_9:def_2;
W in pencil (W1,W2) by A1, XBOOLE_0:def_4;
then A3: W in segment (W1,W2) by XBOOLE_0:def_5;
then W1 is Subspace of W2 by Def1;
hence ( W1 is Subspace of W & W is Subspace of W2 ) by A2, A3, Def1; ::_thesis: verum
end;
theorem :: PENCIL_4:9
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat
for W1, W2, W3, W4 being Subspace of V st W1 is Subspace of W2 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 holds
pencil (W1,W2,k) = pencil (W3,W4,k) by Th6;
definition
let F be Field;
let V be finite-dimensional VectSp of F;
let k be Nat;
funck Pencils_of V -> Subset-Family of (k Subspaces_of V) means :Def4: :: PENCIL_4:def 4
for X being set holds
( X in it iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) );
existence
ex b1 being Subset-Family of (k Subspaces_of V) st
for X being set holds
( X in b1 iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) )
proof
defpred S1[ set ] means ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & $1 = pencil (W1,W2,k) );
set A = bool (k Subspaces_of V);
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool (k Subspaces_of V) & S1[x] ) ) from XBOOLE_0:sch_1();
X c= bool (k Subspaces_of V)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in bool (k Subspaces_of V) )
assume a in X ; ::_thesis: a in bool (k Subspaces_of V)
hence a in bool (k Subspaces_of V) by A1; ::_thesis: verum
end;
then reconsider X = X as Subset-Family of (k Subspaces_of V) ;
take X ; ::_thesis: for X being set holds
( X in X iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) )
let x be set ; ::_thesis: ( x in X iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & x = pencil (W1,W2,k) ) )
thus ( x in X implies ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & x = pencil (W1,W2,k) ) ) by A1; ::_thesis: ( ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & x = pencil (W1,W2,k) ) implies x in X )
given W1, W2 being Subspace of V such that A2: ( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & x = pencil (W1,W2,k) ) ; ::_thesis: x in X
thus x in X by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of (k Subspaces_of V) st ( for X being set holds
( X in b1 iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) ) ) & ( for X being set holds
( X in b2 iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) ) ) holds
b1 = b2
proof
let S, T be Subset-Family of (k Subspaces_of V); ::_thesis: ( ( for X being set holds
( X in S iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) ) ) & ( for X being set holds
( X in T iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) ) ) implies S = T )
assume that
A3: for X being set holds
( X in S iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) ) and
A4: for X being set holds
( X in T iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) ) ; ::_thesis: S = T
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_S_implies_x_in_T_)_&_(_x_in_T_implies_x_in_S_)_)
let x be set ; ::_thesis: ( ( x in S implies x in T ) & ( x in T implies x in S ) )
thus ( x in S implies x in T ) ::_thesis: ( x in T implies x in S )
proof
assume x in S ; ::_thesis: x in T
then ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & x = pencil (W1,W2,k) ) by A3;
hence x in T by A4; ::_thesis: verum
end;
assume x in T ; ::_thesis: x in S
then ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & x = pencil (W1,W2,k) ) by A4;
hence x in S by A3; ::_thesis: verum
end;
hence S = T by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Pencils_of PENCIL_4:def_4_:_
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat
for b4 being Subset-Family of (k Subspaces_of V) holds
( b4 = k Pencils_of V iff for X being set holds
( X in b4 iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) ) );
theorem Th10: :: PENCIL_4:10
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
not k Pencils_of V is empty
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
not k Pencils_of V is empty
let V be finite-dimensional VectSp of F; ::_thesis: for k being Nat st 1 <= k & k < dim V holds
not k Pencils_of V is empty
let k be Nat; ::_thesis: ( 1 <= k & k < dim V implies not k Pencils_of V is empty )
assume that
A1: 1 <= k and
A2: k < dim V ; ::_thesis: not k Pencils_of V is empty
k + 1 <= dim V by A2, NAT_1:13;
then consider W2 being strict Subspace of V such that
A3: dim W2 = k + 1 by VECTSP_9:35;
k -' 1 <= k by NAT_D:35;
then k -' 1 <= dim W2 by A3, NAT_1:13;
then consider W1 being strict Subspace of W2 such that
A4: dim W1 = k -' 1 by VECTSP_9:35;
reconsider W19 = W1 as Subspace of V by VECTSP_4:26;
(dim W1) + 1 = k by A1, A4, XREAL_1:235;
then pencil (W19,W2,k) in k Pencils_of V by A3, Def4;
hence not k Pencils_of V is empty ; ::_thesis: verum
end;
theorem Th11: :: PENCIL_4:11
for F being Field
for V being finite-dimensional VectSp of F
for W1, W2, P, Q being Subspace of V
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 & P in pencil (W1,W2,k) & Q in pencil (W1,W2,k) & P <> Q holds
( P /\ Q = (Omega). W1 & P + Q = (Omega). W2 )
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for W1, W2, P, Q being Subspace of V
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 & P in pencil (W1,W2,k) & Q in pencil (W1,W2,k) & P <> Q holds
( P /\ Q = (Omega). W1 & P + Q = (Omega). W2 )
let V be finite-dimensional VectSp of F; ::_thesis: for W1, W2, P, Q being Subspace of V
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 & P in pencil (W1,W2,k) & Q in pencil (W1,W2,k) & P <> Q holds
( P /\ Q = (Omega). W1 & P + Q = (Omega). W2 )
let W1, W2, P0, Q0 be Subspace of V; ::_thesis: for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 & P0 in pencil (W1,W2,k) & Q0 in pencil (W1,W2,k) & P0 <> Q0 holds
( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 )
let k be Nat; ::_thesis: ( (dim W1) + 1 = k & dim W2 = k + 1 & P0 in pencil (W1,W2,k) & Q0 in pencil (W1,W2,k) & P0 <> Q0 implies ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 ) )
assume that
A1: (dim W1) + 1 = k and
A2: dim W2 = k + 1 and
A3: P0 in pencil (W1,W2,k) and
A4: Q0 in pencil (W1,W2,k) and
A5: P0 <> Q0 ; ::_thesis: ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 )
consider Q being strict Subspace of V such that
A6: Q = Q0 and
A7: dim Q = k by A4, VECTSP_9:def_2;
A8: W1 is Subspace of Q by A4, A6, Th8;
consider P being strict Subspace of V such that
A9: P = P0 and
A10: dim P = k by A3, VECTSP_9:def_2;
W1 is Subspace of P by A3, A9, Th8;
then A11: W1 is Subspace of P /\ Q by A8, VECTSP_5:19;
P /\ Q is Subspace of P by VECTSP_5:15;
then A12: dim (P /\ Q) <= k by A10, VECTSP_9:25;
percases ( dim W1 = dim (P /\ Q) or dim (P /\ Q) = k ) by A1, A12, A11, NAT_1:9, VECTSP_9:25;
supposeA13: dim W1 = dim (P /\ Q) ; ::_thesis: ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 )
then (Omega). W1 = (Omega). (P /\ Q) by A11, VECTSP_9:28;
hence P0 /\ Q0 = (Omega). W1 by A9, A6; ::_thesis: P0 + Q0 = (Omega). W2
( P is Subspace of W2 & Q is Subspace of W2 ) by A3, A4, A9, A6, Th8;
then A14: P + Q is Subspace of W2 by VECTSP_5:34;
((dim (P + Q)) + (dim W1)) - (dim W1) = ((dim P) + (dim Q)) - (dim W1) by A13, VECTSP_9:32;
then (Omega). W2 = (Omega). (P + Q) by A1, A2, A10, A7, A14, VECTSP_9:28;
hence P0 + Q0 = (Omega). W2 by A9, A6; ::_thesis: verum
end;
supposeA15: dim (P /\ Q) = k ; ::_thesis: ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 )
P /\ Q is Subspace of Q by VECTSP_5:15;
then A16: (Omega). (P /\ Q) = (Omega). Q by A7, A15, VECTSP_9:28;
P /\ Q is Subspace of P by VECTSP_5:15;
then (Omega). (P /\ Q) = (Omega). P by A10, A15, VECTSP_9:28;
hence ( P0 /\ Q0 = (Omega). W1 & P0 + Q0 = (Omega). W2 ) by A5, A9, A6, A16; ::_thesis: verum
end;
end;
end;
theorem Th12: :: PENCIL_4:12
for F being Field
for V being finite-dimensional VectSp of F
for v being Vector of V st v <> 0. V holds
dim (Lin {v}) = 1
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for v being Vector of V st v <> 0. V holds
dim (Lin {v}) = 1
let V be finite-dimensional VectSp of F; ::_thesis: for v being Vector of V st v <> 0. V holds
dim (Lin {v}) = 1
let v be Vector of V; ::_thesis: ( v <> 0. V implies dim (Lin {v}) = 1 )
assume v <> 0. V ; ::_thesis: dim (Lin {v}) = 1
then A1: v <> 0. (Lin {v}) by VECTSP_4:11;
v in {v} by TARSKI:def_1;
then v in Lin {v} by VECTSP_7:8;
then reconsider v0 = v as Vector of (Lin {v}) by STRUCT_0:def_5;
( Lin {v0} = Lin {v} & (Omega). (Lin {v0}) = Lin {v0} ) by VECTSP_9:17;
hence dim (Lin {v}) = 1 by A1, VECTSP_9:30; ::_thesis: verum
end;
theorem Th13: :: PENCIL_4:13
for F being Field
for V being finite-dimensional VectSp of F
for W being Subspace of V
for v being Vector of V st not v in W holds
dim (W + (Lin {v})) = (dim W) + 1
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for W being Subspace of V
for v being Vector of V st not v in W holds
dim (W + (Lin {v})) = (dim W) + 1
let V be finite-dimensional VectSp of F; ::_thesis: for W being Subspace of V
for v being Vector of V st not v in W holds
dim (W + (Lin {v})) = (dim W) + 1
let W be Subspace of V; ::_thesis: for v being Vector of V st not v in W holds
dim (W + (Lin {v})) = (dim W) + 1
let v be Vector of V; ::_thesis: ( not v in W implies dim (W + (Lin {v})) = (dim W) + 1 )
assume A1: not v in W ; ::_thesis: dim (W + (Lin {v})) = (dim W) + 1
the carrier of ((Omega). (W /\ (Lin {v}))) = {(0. (W /\ (Lin {v})))}
proof
thus the carrier of ((Omega). (W /\ (Lin {v}))) c= {(0. (W /\ (Lin {v})))} :: according to XBOOLE_0:def_10 ::_thesis: {(0. (W /\ (Lin {v})))} c= the carrier of ((Omega). (W /\ (Lin {v})))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of ((Omega). (W /\ (Lin {v}))) or a in {(0. (W /\ (Lin {v})))} )
assume a in the carrier of ((Omega). (W /\ (Lin {v}))) ; ::_thesis: a in {(0. (W /\ (Lin {v})))}
then A2: a in the carrier of W /\ the carrier of (Lin {v}) by VECTSP_5:def_2;
then a in the carrier of (Lin {v}) by XBOOLE_0:def_4;
then a in Lin {v} by STRUCT_0:def_5;
then consider e being Element of F such that
A3: a = e * v by VECTSP10:3;
a in the carrier of W by A2, XBOOLE_0:def_4;
then A4: a in W by STRUCT_0:def_5;
now__::_thesis:_not_e_<>_0._F
assume e <> 0. F ; ::_thesis: contradiction
then v = (e ") * (e * v) by VECTSP_1:20;
hence contradiction by A1, A4, A3, VECTSP_4:21; ::_thesis: verum
end;
then a = 0. V by A3, VECTSP_1:14;
then a = 0. (W /\ (Lin {v})) by VECTSP_4:11;
hence a in {(0. (W /\ (Lin {v})))} by TARSKI:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {(0. (W /\ (Lin {v})))} or a in the carrier of ((Omega). (W /\ (Lin {v}))) )
assume a in {(0. (W /\ (Lin {v})))} ; ::_thesis: a in the carrier of ((Omega). (W /\ (Lin {v})))
then a = 0. (W /\ (Lin {v})) by TARSKI:def_1;
then a = 0. V by VECTSP_4:11;
then a in W /\ (Lin {v}) by VECTSP_4:17;
hence a in the carrier of ((Omega). (W /\ (Lin {v}))) by STRUCT_0:def_5; ::_thesis: verum
end;
then (Omega). (W /\ (Lin {v})) = (0). (W /\ (Lin {v})) by VECTSP_4:def_3;
then A5: dim (W /\ (Lin {v})) = 0 by VECTSP_9:29;
A6: (dim (W + (Lin {v}))) + (dim (W /\ (Lin {v}))) = (dim W) + (dim (Lin {v})) by VECTSP_9:32;
v <> 0. V by A1, VECTSP_4:17;
hence dim (W + (Lin {v})) = (dim W) + 1 by A5, A6, Th12; ::_thesis: verum
end;
theorem Th14: :: PENCIL_4:14
for F being Field
for V being finite-dimensional VectSp of F
for W being Subspace of V
for v, u being Vector of V st v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V holds
dim (W + (Lin {v,u})) = (dim W) + 2
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for W being Subspace of V
for v, u being Vector of V st v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V holds
dim (W + (Lin {v,u})) = (dim W) + 2
let V be finite-dimensional VectSp of F; ::_thesis: for W being Subspace of V
for v, u being Vector of V st v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V holds
dim (W + (Lin {v,u})) = (dim W) + 2
let W be Subspace of V; ::_thesis: for v, u being Vector of V st v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V holds
dim (W + (Lin {v,u})) = (dim W) + 2
let v, u be Vector of V; ::_thesis: ( v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V implies dim (W + (Lin {v,u})) = (dim W) + 2 )
assume that
A1: v <> u and
A2: {v,u} is linearly-independent and
A3: W /\ (Lin {v,u}) = (0). V ; ::_thesis: dim (W + (Lin {v,u})) = (dim W) + 2
u in {v,u} by TARSKI:def_2;
then A4: u in Lin {v,u} by VECTSP_7:8;
v in {v,u} by TARSKI:def_2;
then v in Lin {v,u} by VECTSP_7:8;
then reconsider v1 = v, u1 = u as Vector of (Lin {v,u}) by A4, STRUCT_0:def_5;
reconsider L = {v1,u1} as linearly-independent Subset of (Lin {v,u}) by A2, VECTSP_9:12;
(Omega). (Lin {v,u}) = Lin L by VECTSP_9:17;
then A5: dim (Lin {v,u}) = 2 by A1, VECTSP_9:31;
(Omega). (W /\ (Lin {v,u})) = (0). (W /\ (Lin {v,u})) by A3, VECTSP_4:36;
then dim (W /\ (Lin {v,u})) = 0 by VECTSP_9:29;
hence dim (W + (Lin {v,u})) = (dim (W + (Lin {v,u}))) + (dim (W /\ (Lin {v,u})))
.= (dim W) + 2 by A5, VECTSP_9:32 ;
::_thesis: verum
end;
theorem Th15: :: PENCIL_4:15
for F being Field
for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)
let V be finite-dimensional VectSp of F; ::_thesis: for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)
let W1, W2 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 implies for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k) )
assume A1: W1 is Subspace of W2 ; ::_thesis: for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)
let k be Nat; ::_thesis: ( (dim W1) + 1 = k & dim W2 = k + 1 implies for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k) )
assume that
A2: (dim W1) + 1 = k and
A3: dim W2 = k + 1 ; ::_thesis: for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)
let v be Vector of V; ::_thesis: ( v in W2 & not v in W1 implies W1 + (Lin {v}) in pencil (W1,W2,k) )
assume that
A4: v in W2 and
A5: not v in W1 ; ::_thesis: W1 + (Lin {v}) in pencil (W1,W2,k)
set W = W1 + (Lin {v});
A6: dim (W1 + (Lin {v})) = k by A2, A5, Th13;
then A7: W1 + (Lin {v}) in k Subspaces_of V by VECTSP_9:def_2;
v in the carrier of W2 by A4, STRUCT_0:def_5;
then {v} c= the carrier of W2 by ZFMISC_1:31;
then Lin {v} is Subspace of W2 by VECTSP_9:16;
then ( W1 is Subspace of W1 + (Lin {v}) & W1 + (Lin {v}) is Subspace of W2 ) by A1, VECTSP_5:7, VECTSP_5:34;
then A8: W1 + (Lin {v}) in segment (W1,W2) by A1, Def1;
dim ((Omega). W2) = k + 1 by A3, VECTSP_9:27;
then A9: W1 + (Lin {v}) <> (Omega). W2 by A6;
(dim ((Omega). W1)) + 1 = k by A2, VECTSP_9:27;
then W1 + (Lin {v}) <> (Omega). W1 by A6;
then not W1 + (Lin {v}) in {((Omega). W1),((Omega). W2)} by A9, TARSKI:def_2;
then W1 + (Lin {v}) in pencil (W1,W2) by A8, XBOOLE_0:def_5;
hence W1 + (Lin {v}) in pencil (W1,W2,k) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th16: :: PENCIL_4:16
for F being Field
for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
let V be finite-dimensional VectSp of F; ::_thesis: for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
let W1, W2 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 implies for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial )
assume W1 is Subspace of W2 ; ::_thesis: for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
then reconsider U = W1 as Subspace of W2 ;
let k be Nat; ::_thesis: ( (dim W1) + 1 = k & dim W2 = k + 1 implies not pencil (W1,W2,k) is trivial )
assume A1: ( (dim W1) + 1 = k & dim W2 = k + 1 ) ; ::_thesis: not pencil (W1,W2,k) is trivial
set W = the Linear_Compl of U;
A2: W2 is_the_direct_sum_of the Linear_Compl of U,U by VECTSP_5:def_5;
then A3: the Linear_Compl of U /\ U = (0). W2 by VECTSP_5:def_4;
dim W2 = (dim U) + (dim the Linear_Compl of U) by A2, VECTSP_9:34;
then consider u, v being Vector of the Linear_Compl of U such that
A4: u <> v and
A5: {u,v} is linearly-independent and
(Omega). the Linear_Compl of U = Lin {u,v} by A1, VECTSP_9:31;
A6: now__::_thesis:_not_v_in_Lin_{u}
assume v in Lin {u} ; ::_thesis: contradiction
then ex a being Element of F st v = a * u by VECTSP10:3;
hence contradiction by A4, A5, VECTSP_7:5; ::_thesis: verum
end;
reconsider u = u, v = v as Vector of W2 by VECTSP_4:10;
reconsider u1 = u, v1 = v as Vector of V by VECTSP_4:10;
A7: v in the Linear_Compl of U by STRUCT_0:def_5;
A8: now__::_thesis:_not_v_in_W1
assume v in W1 ; ::_thesis: contradiction
then v in (0). W2 by A3, A7, VECTSP_5:3;
then v = 0. W2 by VECTSP_4:35;
then v = 0. the Linear_Compl of U by VECTSP_4:11;
hence contradiction by A5, VECTSP_7:4; ::_thesis: verum
end;
A9: u in the Linear_Compl of U by STRUCT_0:def_5;
A10: now__::_thesis:_not_u_in_W1
assume u in W1 ; ::_thesis: contradiction
then u in (0). W2 by A3, A9, VECTSP_5:3;
then u = 0. W2 by VECTSP_4:35;
then u = 0. the Linear_Compl of U by VECTSP_4:11;
hence contradiction by A5, VECTSP_7:4; ::_thesis: verum
end;
v in {v1} by TARSKI:def_1;
then v in Lin {v1} by VECTSP_7:8;
then A11: v in W1 + (Lin {v1}) by VECTSP_5:2;
A12: not v in Lin {u} by A6, VECTSP10:13;
A13: now__::_thesis:_not_W1_+_(Lin_{v1})_=_W1_+_(Lin_{u1})
reconsider Wx = the Linear_Compl of U as Subspace of V by VECTSP_4:26;
assume W1 + (Lin {v1}) = W1 + (Lin {u1}) ; ::_thesis: contradiction
then consider h, j being Vector of V such that
A14: h in W1 and
A15: j in Lin {u1} and
A16: v1 = h + j by A11, VECTSP_5:1;
consider a being Element of F such that
A17: j = a * u1 by A15, VECTSP10:3;
v1 - (a * u1) = h + ((a * u1) - (a * u1)) by A16, A17, RLVECT_1:def_3;
then v1 - (a * u1) = h + (0. V) by RLVECT_1:15;
then A18: v1 - (a * u1) = h by RLVECT_1:4;
a * u = a * u1 by VECTSP_4:14;
then A19: v1 - (a * u1) = v - (a * u) by VECTSP_4:16;
a * u in Wx by A9, VECTSP_4:21;
then v - (a * u) in Wx by A7, VECTSP_4:23;
then v - (a * u) in the Linear_Compl of U /\ U by A14, A18, A19, VECTSP_5:3;
then v - (a * u) = 0. W2 by A3, VECTSP_4:35;
then h = 0. V by A18, A19, VECTSP_4:11;
then v1 = j by A16, RLVECT_1:4;
hence contradiction by A12, A15, VECTSP10:13; ::_thesis: verum
end;
v in W2 by STRUCT_0:def_5;
then A20: W1 + (Lin {v1}) in pencil (W1,W2,k) by A1, A8, Th15;
u in W2 by STRUCT_0:def_5;
then W1 + (Lin {u1}) in pencil (W1,W2,k) by A1, A10, Th15;
then 2 c= card (pencil (W1,W2,k)) by A13, A20, PENCIL_1:2;
hence not pencil (W1,W2,k) is trivial by PENCIL_1:4; ::_thesis: verum
end;
definition
let F be Field;
let V be finite-dimensional VectSp of F;
let k be Nat;
func PencilSpace (V,k) -> strict TopStruct equals :: PENCIL_4:def 5
TopStruct(# (k Subspaces_of V),(k Pencils_of V) #);
coherence
TopStruct(# (k Subspaces_of V),(k Pencils_of V) #) is strict TopStruct ;
end;
:: deftheorem defines PencilSpace PENCIL_4:def_5_:_
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat holds PencilSpace (V,k) = TopStruct(# (k Subspaces_of V),(k Pencils_of V) #);
theorem Th17: :: PENCIL_4:17
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
not PencilSpace (V,k) is void
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
not PencilSpace (V,k) is void
let V be finite-dimensional VectSp of F; ::_thesis: for k being Nat st 1 <= k & k < dim V holds
not PencilSpace (V,k) is void
let k be Nat; ::_thesis: ( 1 <= k & k < dim V implies not PencilSpace (V,k) is void )
assume A1: ( 1 <= k & k < dim V ) ; ::_thesis: not PencilSpace (V,k) is void
set S = PencilSpace (V,k);
not the topology of (PencilSpace (V,k)) is empty by A1, Th10;
hence not PencilSpace (V,k) is void by PENCIL_1:def_4; ::_thesis: verum
end;
theorem Th18: :: PENCIL_4:18
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V & 3 <= dim V holds
not PencilSpace (V,k) is degenerated
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V & 3 <= dim V holds
not PencilSpace (V,k) is degenerated
let V be finite-dimensional VectSp of F; ::_thesis: for k being Nat st 1 <= k & k < dim V & 3 <= dim V holds
not PencilSpace (V,k) is degenerated
let k be Nat; ::_thesis: ( 1 <= k & k < dim V & 3 <= dim V implies not PencilSpace (V,k) is degenerated )
assume that
A1: 1 <= k and
A2: k < dim V and
A3: 3 <= dim V ; ::_thesis: not PencilSpace (V,k) is degenerated
set S = PencilSpace (V,k);
now__::_thesis:_for_B_being_Block_of_(PencilSpace_(V,k))_holds_the_carrier_of_(PencilSpace_(V,k))_<>_B
let B be Block of (PencilSpace (V,k)); ::_thesis: the carrier of (PencilSpace (V,k)) <> b1
not the topology of (PencilSpace (V,k)) is empty by A1, A2, Th10;
then consider W1, W2 being Subspace of V such that
A4: W1 is Subspace of W2 and
A5: (dim W1) + 1 = k and
A6: dim W2 = k + 1 and
A7: B = pencil (W1,W2,k) by Def4;
A8: the carrier of W1 c= the carrier of V by VECTSP_4:def_2;
percases ( k + 1 < dim V or ( 2 <= k & k + 1 >= dim V ) ) by A2, A3, Th1;
suppose k + 1 < dim V ; ::_thesis: the carrier of (PencilSpace (V,k)) <> b1
then A9: (Omega). W2 <> (Omega). V by A6, VECTSP_9:28;
A10: now__::_thesis:_not_the_carrier_of_V_=_the_carrier_of_W2
assume A11: the carrier of V = the carrier of W2 ; ::_thesis: contradiction
(Omega). W2 is Subspace of V by Th4;
hence contradiction by A9, A11, VECTSP_4:29; ::_thesis: verum
end;
the carrier of W2 c= the carrier of V by VECTSP_4:def_2;
then not the carrier of V c= the carrier of W2 by A10, XBOOLE_0:def_10;
then consider v being set such that
A12: v in the carrier of V and
A13: not v in the carrier of W2 by TARSKI:def_3;
reconsider v = v as Vector of V by A12;
set X = W1 + (Lin {v});
A14: now__::_thesis:_not_W1_+_(Lin_{v})_in_B
v in {v} by TARSKI:def_1;
then v in Lin {v} by VECTSP_7:8;
then v in W1 + (Lin {v}) by VECTSP_5:2;
then A15: v in the carrier of (W1 + (Lin {v})) by STRUCT_0:def_5;
assume W1 + (Lin {v}) in B ; ::_thesis: contradiction
then W1 + (Lin {v}) is Subspace of W2 by A7, Th8;
then the carrier of (W1 + (Lin {v})) c= the carrier of W2 by VECTSP_4:def_2;
hence contradiction by A13, A15; ::_thesis: verum
end;
not v in W2 by A13, STRUCT_0:def_5;
then dim (W1 + (Lin {v})) = k by A4, A5, Th13, VECTSP_4:8;
hence the carrier of (PencilSpace (V,k)) <> B by A14, VECTSP_9:def_2; ::_thesis: verum
end;
supposeA16: ( 2 <= k & k + 1 >= dim V ) ; ::_thesis: the carrier of (PencilSpace (V,k)) <> b1
set I = the Basis of W1;
reconsider I1 = the Basis of W1 as finite Subset of W1 by VECTSP_9:20;
2 - 1 <= ((dim W1) + 1) - 1 by A5, A16, XREAL_1:9;
then 1 <= card I1 by VECTSP_9:def_1;
then not I1 is empty ;
then consider i being set such that
A17: i in the Basis of W1 by XBOOLE_0:def_1;
reconsider i = i as Vector of W1 by A17;
reconsider J = I1 \ {i} as finite Subset of V by A8, XBOOLE_1:1;
the Basis of W1 is linearly-independent by VECTSP_7:def_3;
then the Basis of W1 \ {i} is linearly-independent by VECTSP_7:1, XBOOLE_1:36;
then reconsider JJ = the Basis of W1 \ {i} as linearly-independent Subset of V by VECTSP_9:11;
J c= the carrier of (Lin J)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in J or a in the carrier of (Lin J) )
assume a in J ; ::_thesis: a in the carrier of (Lin J)
then a in Lin J by VECTSP_7:8;
hence a in the carrier of (Lin J) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider JJJ = JJ as linearly-independent Subset of (Lin J) by VECTSP_9:12;
Lin JJJ = Lin J by VECTSP_9:17;
then A18: J is Basis of Lin J by VECTSP_7:def_3;
A19: card the Basis of W1 = dim W1 by VECTSP_9:def_1;
set T = the Linear_Compl of W1;
A20: V is_the_direct_sum_of W1, the Linear_Compl of W1 by VECTSP_5:38;
then A21: W1 /\ the Linear_Compl of W1 = (0). V by VECTSP_5:def_4;
k + 1 <= dim V by A2, NAT_1:13;
then dim V = k + 1 by A16, XXREAL_0:1;
then (k + 1) - ((dim W1) + 1) = ((dim W1) + (dim the Linear_Compl of W1)) - ((dim W1) + 1) by A20, VECTSP_9:34;
then consider u, v being Vector of the Linear_Compl of W1 such that
A22: u <> v and
A23: {u,v} is linearly-independent and
A24: (Omega). the Linear_Compl of W1 = Lin {u,v} by A5, VECTSP_9:31;
A25: v in the carrier of the Linear_Compl of W1 ;
( the carrier of the Linear_Compl of W1 c= the carrier of V & u in the carrier of the Linear_Compl of W1 ) by VECTSP_4:def_2;
then reconsider u1 = u, v1 = v as Vector of V by A25;
reconsider Y = {u,v} as linearly-independent Subset of V by A23, VECTSP_9:11;
A26: Y = {u,v} ;
Lin ( the Basis of W1 \ {i}) is Subspace of Lin the Basis of W1 by VECTSP_7:13, XBOOLE_1:36;
then A27: Lin J is Subspace of W1 by VECTSP_9:17;
the carrier of ((Lin J) /\ (Lin {u1,v1})) c= the carrier of ((0). V)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of ((Lin J) /\ (Lin {u1,v1})) or a in the carrier of ((0). V) )
assume a in the carrier of ((Lin J) /\ (Lin {u1,v1})) ; ::_thesis: a in the carrier of ((0). V)
then A28: a in (Lin J) /\ (Lin {u1,v1}) by STRUCT_0:def_5;
then a in Lin {u1,v1} by VECTSP_5:3;
then a in Lin {u,v} by VECTSP_9:17;
then a in the carrier of VectSpStr(# the carrier of the Linear_Compl of W1, the U5 of the Linear_Compl of W1, the ZeroF of the Linear_Compl of W1, the lmult of the Linear_Compl of W1 #) by A24, STRUCT_0:def_5;
then A29: a in the Linear_Compl of W1 by STRUCT_0:def_5;
a in Lin J by A28, VECTSP_5:3;
then a in W1 by A27, VECTSP_4:8;
then a in W1 /\ the Linear_Compl of W1 by A29, VECTSP_5:3;
hence a in the carrier of ((0). V) by A21, STRUCT_0:def_5; ::_thesis: verum
end;
then A30: ( (0). V is Subspace of (Lin J) /\ (Lin {u1,v1}) & (Lin J) /\ (Lin {u1,v1}) is Subspace of (0). V ) by VECTSP_4:27, VECTSP_4:39;
card J = (card I1) - (card {i}) by A17, EULER_1:4
.= (dim W1) - 1 by A19, CARD_1:30 ;
then dim (Lin J) = (dim W1) - 1 by A18, VECTSP_9:def_1;
then A31: dim ((Lin J) + (Lin {u1,v1})) = ((dim W1) - 1) + 2 by A22, A26, A30, Th14, VECTSP_4:25;
A32: Lin the Basis of W1 = (Omega). W1 by VECTSP_7:def_3;
A33: i in W1 by STRUCT_0:def_5;
now__::_thesis:_not_(Lin_J)_+_(Lin_{u1,v1})_in_B
A34: now__::_thesis:_not_i_in_(Lin_J)_+_(Lin_{u1,v1})
reconsider IV = the Basis of W1 as Subset of V by A8, XBOOLE_1:1;
assume A35: i in (Lin J) + (Lin {u1,v1}) ; ::_thesis: contradiction
IV c= the carrier of ((Lin J) + (Lin {u1,v1}))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in IV or a in the carrier of ((Lin J) + (Lin {u1,v1})) )
{i} c= the Basis of W1 by A17, ZFMISC_1:31;
then A36: ( the Basis of W1 \ {i}) \/ {i} = the Basis of W1 by XBOOLE_1:45;
assume A37: a in IV ; ::_thesis: a in the carrier of ((Lin J) + (Lin {u1,v1}))
percases ( a in J or a in {i} ) by A37, A36, XBOOLE_0:def_3;
suppose a in J ; ::_thesis: a in the carrier of ((Lin J) + (Lin {u1,v1}))
then A38: a in Lin J by VECTSP_7:8;
then a in V by VECTSP_4:9;
then reconsider o = a as Vector of V by STRUCT_0:def_5;
o in (Lin J) + (Lin {u1,v1}) by A38, VECTSP_5:2;
hence a in the carrier of ((Lin J) + (Lin {u1,v1})) by STRUCT_0:def_5; ::_thesis: verum
end;
suppose a in {i} ; ::_thesis: a in the carrier of ((Lin J) + (Lin {u1,v1}))
then a = i by TARSKI:def_1;
hence a in the carrier of ((Lin J) + (Lin {u1,v1})) by A35, STRUCT_0:def_5; ::_thesis: verum
end;
end;
end;
then Lin IV is Subspace of (Lin J) + (Lin {u1,v1}) by VECTSP_9:16;
then Lin the Basis of W1 is Subspace of (Lin J) + (Lin {u1,v1}) by VECTSP_9:17;
then A39: W1 is Subspace of (Lin J) + (Lin {u1,v1}) by A32, Th5;
the carrier of (W1 /\ (Lin {u1,v1})) c= the carrier of ((0). V)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of (W1 /\ (Lin {u1,v1})) or a in the carrier of ((0). V) )
assume a in the carrier of (W1 /\ (Lin {u1,v1})) ; ::_thesis: a in the carrier of ((0). V)
then A40: a in W1 /\ (Lin {u1,v1}) by STRUCT_0:def_5;
then a in Lin {u1,v1} by VECTSP_5:3;
then a in Lin {u,v} by VECTSP_9:17;
then a in the carrier of VectSpStr(# the carrier of the Linear_Compl of W1, the U5 of the Linear_Compl of W1, the ZeroF of the Linear_Compl of W1, the lmult of the Linear_Compl of W1 #) by A24, STRUCT_0:def_5;
then A41: a in the Linear_Compl of W1 by STRUCT_0:def_5;
a in W1 by A40, VECTSP_5:3;
then a in W1 /\ the Linear_Compl of W1 by A41, VECTSP_5:3;
hence a in the carrier of ((0). V) by A21, STRUCT_0:def_5; ::_thesis: verum
end;
then ( (0). V is Subspace of W1 /\ (Lin {u1,v1}) & W1 /\ (Lin {u1,v1}) is Subspace of (0). V ) by VECTSP_4:27, VECTSP_4:39;
then A42: dim (W1 + (Lin {u1,v1})) = (dim W1) + 2 by A22, A26, Th14, VECTSP_4:25;
Lin {u1,v1} is Subspace of (Lin J) + (Lin {u1,v1}) by VECTSP_5:7;
then W1 + (Lin {u1,v1}) is Subspace of (Lin J) + (Lin {u1,v1}) by A39, VECTSP_5:34;
then ((dim W1) + 1) + 1 <= (dim W1) + 1 by A31, A42, VECTSP_9:25;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
assume (Lin J) + (Lin {u1,v1}) in B ; ::_thesis: contradiction
then W1 is Subspace of (Lin J) + (Lin {u1,v1}) by A7, Th8;
hence contradiction by A33, A34, VECTSP_4:8; ::_thesis: verum
end;
hence the carrier of (PencilSpace (V,k)) <> B by A5, A31, VECTSP_9:def_2; ::_thesis: verum
end;
end;
end;
then the carrier of (PencilSpace (V,k)) is not Block of (PencilSpace (V,k)) ;
hence not PencilSpace (V,k) is degenerated by PENCIL_1:def_5; ::_thesis: verum
end;
theorem Th19: :: PENCIL_4:19
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
PencilSpace (V,k) is with_non_trivial_blocks
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
PencilSpace (V,k) is with_non_trivial_blocks
let V be finite-dimensional VectSp of F; ::_thesis: for k being Nat st 1 <= k & k < dim V holds
PencilSpace (V,k) is with_non_trivial_blocks
let k be Nat; ::_thesis: ( 1 <= k & k < dim V implies PencilSpace (V,k) is with_non_trivial_blocks )
assume A1: ( 1 <= k & k < dim V ) ; ::_thesis: PencilSpace (V,k) is with_non_trivial_blocks
set S = PencilSpace (V,k);
thus PencilSpace (V,k) is with_non_trivial_blocks ::_thesis: verum
proof
let X be Block of (PencilSpace (V,k)); :: according to PENCIL_1:def_6 ::_thesis: 2 c= card X
not PencilSpace (V,k) is void by A1, Th17;
then ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) by Def4;
then not X is trivial by Th16;
hence 2 c= card X by PENCIL_1:4; ::_thesis: verum
end;
end;
theorem Th20: :: PENCIL_4:20
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
PencilSpace (V,k) is identifying_close_blocks
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
PencilSpace (V,k) is identifying_close_blocks
let V be finite-dimensional VectSp of F; ::_thesis: for k being Nat st 1 <= k & k < dim V holds
PencilSpace (V,k) is identifying_close_blocks
let k be Nat; ::_thesis: ( 1 <= k & k < dim V implies PencilSpace (V,k) is identifying_close_blocks )
assume that
A1: 1 <= k and
A2: k < dim V ; ::_thesis: PencilSpace (V,k) is identifying_close_blocks
set S = PencilSpace (V,k);
thus PencilSpace (V,k) is identifying_close_blocks ::_thesis: verum
proof
let X, Y be Block of (PencilSpace (V,k)); :: according to PENCIL_1:def_7 ::_thesis: ( not 2 c= card (X /\ Y) or X = Y )
assume 2 c= card (X /\ Y) ; ::_thesis: X = Y
then consider P, Q being set such that
A3: ( P in X /\ Y & Q in X /\ Y ) and
A4: P <> Q by PENCIL_1:2;
A5: ( P in X & Q in X ) by A3, XBOOLE_0:def_4;
A6: ( P in Y & Q in Y ) by A3, XBOOLE_0:def_4;
A7: not PencilSpace (V,k) is void by A1, A2, Th17;
then consider W1, W2 being Subspace of V such that
A8: W1 is Subspace of W2 and
A9: ( (dim W1) + 1 = k & dim W2 = k + 1 ) and
A10: X = pencil (W1,W2,k) by Def4;
not the topology of (PencilSpace (V,k)) is empty by A7;
then X in the topology of (PencilSpace (V,k)) ;
then reconsider P = P, Q = Q as Point of (PencilSpace (V,k)) by A5;
A11: not PencilSpace (V,k) is empty by A2, VECTSP_9:36;
then ex P1 being strict Subspace of V st
( P1 = P & dim P1 = k ) by VECTSP_9:def_2;
then reconsider P = P as strict Subspace of V ;
ex Q1 being strict Subspace of V st
( Q1 = Q & dim Q1 = k ) by A11, VECTSP_9:def_2;
then reconsider Q = Q as strict Subspace of V ;
consider U1, U2 being Subspace of V such that
A12: U1 is Subspace of U2 and
A13: ( (dim U1) + 1 = k & dim U2 = k + 1 ) and
A14: Y = pencil (U1,U2,k) by A7, Def4;
A15: (Omega). W2 = P + Q by A4, A5, A9, A10, Th11
.= (Omega). U2 by A4, A6, A13, A14, Th11 ;
(Omega). W1 = P /\ Q by A4, A5, A9, A10, Th11
.= (Omega). U1 by A4, A6, A13, A14, Th11 ;
hence X = Y by A8, A10, A12, A14, A15, Th6; ::_thesis: verum
end;
end;
theorem :: PENCIL_4:21
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V & 3 <= dim V holds
PencilSpace (V,k) is PLS by Th17, Th18, Th19, Th20, VECTSP_9:36;
begin
definition
let F be Field;
let V be finite-dimensional VectSp of F;
let m, n be Nat;
func SubspaceSet (V,m,n) -> Subset-Family of (m Subspaces_of V) means :Def6: :: PENCIL_4:def 6
for X being set holds
( X in it iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) );
existence
ex b1 being Subset-Family of (m Subspaces_of V) st
for X being set holds
( X in b1 iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) )
proof
defpred S1[ set ] means ex W being Subspace of V st
( dim W = n & $1 = m Subspaces_of W );
set A = bool (m Subspaces_of V);
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool (m Subspaces_of V) & S1[x] ) ) from XBOOLE_0:sch_1();
X c= bool (m Subspaces_of V)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in bool (m Subspaces_of V) )
assume a in X ; ::_thesis: a in bool (m Subspaces_of V)
hence a in bool (m Subspaces_of V) by A1; ::_thesis: verum
end;
then reconsider X = X as Subset-Family of (m Subspaces_of V) ;
take X ; ::_thesis: for X being set holds
( X in X iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) )
let x be set ; ::_thesis: ( x in X iff ex W being Subspace of V st
( dim W = n & x = m Subspaces_of W ) )
thus ( x in X implies ex W being Subspace of V st
( dim W = n & x = m Subspaces_of W ) ) by A1; ::_thesis: ( ex W being Subspace of V st
( dim W = n & x = m Subspaces_of W ) implies x in X )
given W being Subspace of V such that A2: dim W = n and
A3: x = m Subspaces_of W ; ::_thesis: x in X
x c= m Subspaces_of V by A3, VECTSP_9:38;
hence x in X by A1, A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of (m Subspaces_of V) st ( for X being set holds
( X in b1 iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ) & ( for X being set holds
( X in b2 iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ) holds
b1 = b2
proof
let S, T be Subset-Family of (m Subspaces_of V); ::_thesis: ( ( for X being set holds
( X in S iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ) & ( for X being set holds
( X in T iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ) implies S = T )
assume that
A4: for X being set holds
( X in S iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) and
A5: for X being set holds
( X in T iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ; ::_thesis: S = T
now__::_thesis:_for_X_being_set_holds_
(_(_X_in_S_implies_X_in_T_)_&_(_X_in_T_implies_X_in_S_)_)
let X be set ; ::_thesis: ( ( X in S implies X in T ) & ( X in T implies X in S ) )
thus ( X in S implies X in T ) ::_thesis: ( X in T implies X in S )
proof
assume X in S ; ::_thesis: X in T
then ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) by A4;
hence X in T by A5; ::_thesis: verum
end;
assume X in T ; ::_thesis: X in S
then ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) by A5;
hence X in S by A4; ::_thesis: verum
end;
hence S = T by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines SubspaceSet PENCIL_4:def_6_:_
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat
for b5 being Subset-Family of (m Subspaces_of V) holds
( b5 = SubspaceSet (V,m,n) iff for X being set holds
( X in b5 iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) );
theorem Th22: :: PENCIL_4:22
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st n <= dim V holds
not SubspaceSet (V,m,n) is empty
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for m, n being Nat st n <= dim V holds
not SubspaceSet (V,m,n) is empty
let V be finite-dimensional VectSp of F; ::_thesis: for m, n being Nat st n <= dim V holds
not SubspaceSet (V,m,n) is empty
let m, n be Nat; ::_thesis: ( n <= dim V implies not SubspaceSet (V,m,n) is empty )
assume n <= dim V ; ::_thesis: not SubspaceSet (V,m,n) is empty
then consider W being strict Subspace of V such that
A1: dim W = n by VECTSP_9:35;
m Subspaces_of W in SubspaceSet (V,m,n) by A1, Def6;
hence not SubspaceSet (V,m,n) is empty ; ::_thesis: verum
end;
theorem Th23: :: PENCIL_4:23
for F being Field
for W1, W2 being finite-dimensional VectSp of F st (Omega). W1 = (Omega). W2 holds
for m being Nat holds m Subspaces_of W1 = m Subspaces_of W2
proof
let F be Field; ::_thesis: for W1, W2 being finite-dimensional VectSp of F st (Omega). W1 = (Omega). W2 holds
for m being Nat holds m Subspaces_of W1 = m Subspaces_of W2
let W1, W2 be finite-dimensional VectSp of F; ::_thesis: ( (Omega). W1 = (Omega). W2 implies for m being Nat holds m Subspaces_of W1 = m Subspaces_of W2 )
assume A1: (Omega). W1 = (Omega). W2 ; ::_thesis: for m being Nat holds m Subspaces_of W1 = m Subspaces_of W2
let m be Nat; ::_thesis: m Subspaces_of W1 = m Subspaces_of W2
(Omega). W1 is Subspace of (Omega). W2 by A1, VECTSP_4:24;
then W1 is Subspace of (Omega). W2 by Th5;
then W1 is Subspace of W2 by Th3;
hence m Subspaces_of W1 c= m Subspaces_of W2 by VECTSP_9:38; :: according to XBOOLE_0:def_10 ::_thesis: m Subspaces_of W2 c= m Subspaces_of W1
(Omega). W2 is Subspace of (Omega). W1 by A1, VECTSP_4:24;
then W2 is Subspace of (Omega). W1 by Th5;
then W2 is Subspace of W1 by Th3;
hence m Subspaces_of W2 c= m Subspaces_of W1 by VECTSP_9:38; ::_thesis: verum
end;
theorem Th24: :: PENCIL_4:24
for F being Field
for V being finite-dimensional VectSp of F
for W being Subspace of V
for m being Nat st 1 <= m & m <= dim V & m Subspaces_of V c= m Subspaces_of W holds
(Omega). V = (Omega). W
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for W being Subspace of V
for m being Nat st 1 <= m & m <= dim V & m Subspaces_of V c= m Subspaces_of W holds
(Omega). V = (Omega). W
let V be finite-dimensional VectSp of F; ::_thesis: for W being Subspace of V
for m being Nat st 1 <= m & m <= dim V & m Subspaces_of V c= m Subspaces_of W holds
(Omega). V = (Omega). W
let W be Subspace of V; ::_thesis: for m being Nat st 1 <= m & m <= dim V & m Subspaces_of V c= m Subspaces_of W holds
(Omega). V = (Omega). W
let m be Nat; ::_thesis: ( 1 <= m & m <= dim V & m Subspaces_of V c= m Subspaces_of W implies (Omega). V = (Omega). W )
assume that
A1: 1 <= m and
A2: m <= dim V and
A3: m Subspaces_of V c= m Subspaces_of W ; ::_thesis: (Omega). V = (Omega). W
hereby ::_thesis: verum
A4: dim W <= dim V by VECTSP_9:25;
assume A5: (Omega). V <> (Omega). W ; ::_thesis: contradiction
then dim W <> dim V by VECTSP_9:28;
then A6: dim W < dim V by A4, XXREAL_0:1;
percases ( m = dim V or m < dim V ) by A2, XXREAL_0:1;
suppose m = dim V ; ::_thesis: contradiction
then m Subspaces_of W = {} by A6, VECTSP_9:37;
hence contradiction by A2, A3, VECTSP_9:36; ::_thesis: verum
end;
supposeA7: m < dim V ; ::_thesis: contradiction
A8: now__::_thesis:_not_the_carrier_of_V_=_the_carrier_of_W
assume A9: the carrier of V = the carrier of W ; ::_thesis: contradiction
(Omega). W is strict Subspace of V by Th4;
hence contradiction by A5, A9, VECTSP_4:29; ::_thesis: verum
end;
the carrier of W c= the carrier of V by VECTSP_4:def_2;
then not the carrier of V c= the carrier of W by A8, XBOOLE_0:def_10;
then consider x being set such that
A10: x in the carrier of V and
A11: not x in the carrier of W by TARSKI:def_3;
reconsider x = x as Vector of V by A10;
0. V in W by VECTSP_4:17;
then x <> 0. V by A11, STRUCT_0:def_5;
then {x} is linearly-independent by VECTSP_7:3;
then consider I being Basis of V such that
A12: {x} c= I by VECTSP_7:19;
reconsider J = I as finite Subset of V by VECTSP_9:20;
card J = dim V by VECTSP_9:def_1;
then consider K being Subset of J such that
A13: card K = m by A7, Lm1;
A14: I is linearly-independent by VECTSP_7:def_3;
percases ( x in K or not x in K ) ;
supposeA15: x in K ; ::_thesis: contradiction
reconsider L = K as finite Subset of V by XBOOLE_1:1;
L c= the carrier of (Lin L)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in L or a in the carrier of (Lin L) )
assume a in L ; ::_thesis: a in the carrier of (Lin L)
then a in Lin L by VECTSP_7:8;
hence a in the carrier of (Lin L) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider L9 = L as Subset of (Lin L) ;
L is linearly-independent by A14, VECTSP_7:1;
then reconsider LL1 = L9 as linearly-independent Subset of (Lin L) by VECTSP_9:12;
Lin LL1 = VectSpStr(# the carrier of (Lin L), the U5 of (Lin L), the ZeroF of (Lin L), the lmult of (Lin L) #) by VECTSP_9:17;
then L is Basis of Lin L by VECTSP_7:def_3;
then dim (Lin L) = m by A13, VECTSP_9:def_1;
then Lin L in m Subspaces_of V by VECTSP_9:def_2;
then ex M being strict Subspace of W st
( M = Lin L & dim M = m ) by A3, VECTSP_9:def_2;
then x in W by A15, VECTSP_4:9, VECTSP_7:8;
hence contradiction by A11, STRUCT_0:def_5; ::_thesis: verum
end;
supposeA16: not x in K ; ::_thesis: contradiction
consider y being set such that
A17: y in K by A1, A13, CARD_1:27, XBOOLE_0:def_1;
(K \ {y}) \/ {x} c= the carrier of V
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (K \ {y}) \/ {x} or a in the carrier of V )
assume a in (K \ {y}) \/ {x} ; ::_thesis: a in the carrier of V
then ( a in K \ {y} or a in {x} ) by XBOOLE_0:def_3;
hence a in the carrier of V by TARSKI:def_3; ::_thesis: verum
end;
then reconsider L = (K \ {y}) \/ {x} as finite Subset of V ;
L c= the carrier of (Lin L)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in L or a in the carrier of (Lin L) )
assume a in L ; ::_thesis: a in the carrier of (Lin L)
then a in Lin L by VECTSP_7:8;
hence a in the carrier of (Lin L) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider L9 = L as Subset of (Lin L) ;
L c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in L or a in I )
assume a in L ; ::_thesis: a in I
then ( a in K \ {y} or a in {x} ) by XBOOLE_0:def_3;
hence a in I by A12; ::_thesis: verum
end;
then L is linearly-independent by A14, VECTSP_7:1;
then reconsider LL1 = L9 as linearly-independent Subset of (Lin L) by VECTSP_9:12;
Lin LL1 = VectSpStr(# the carrier of (Lin L), the U5 of (Lin L), the ZeroF of (Lin L), the lmult of (Lin L) #) by VECTSP_9:17;
then A18: L is Basis of Lin L by VECTSP_7:def_3;
not x in K \ {y} by A16, XBOOLE_0:def_5;
then card L = (card (K \ {y})) + 1 by CARD_2:41
.= ((card K) - (card {y})) + 1 by A17, EULER_1:4
.= ((card K) - 1) + 1 by CARD_1:30
.= m by A13 ;
then dim (Lin L) = m by A18, VECTSP_9:def_1;
then Lin L in m Subspaces_of V by VECTSP_9:def_2;
then A19: ex M being strict Subspace of W st
( M = Lin L & dim M = m ) by A3, VECTSP_9:def_2;
x in {x} by TARSKI:def_1;
then x in L by XBOOLE_0:def_3;
then x in W by A19, VECTSP_4:9, VECTSP_7:8;
hence contradiction by A11, STRUCT_0:def_5; ::_thesis: verum
end;
end;
end;
end;
end;
end;
definition
let F be Field;
let V be finite-dimensional VectSp of F;
let m, n be Nat;
func GrassmannSpace (V,m,n) -> strict TopStruct equals :: PENCIL_4:def 7
TopStruct(# (m Subspaces_of V),(SubspaceSet (V,m,n)) #);
coherence
TopStruct(# (m Subspaces_of V),(SubspaceSet (V,m,n)) #) is strict TopStruct ;
end;
:: deftheorem defines GrassmannSpace PENCIL_4:def_7_:_
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat holds GrassmannSpace (V,m,n) = TopStruct(# (m Subspaces_of V),(SubspaceSet (V,m,n)) #);
theorem Th25: :: PENCIL_4:25
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st n <= dim V holds
not GrassmannSpace (V,m,n) is void
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for m, n being Nat st n <= dim V holds
not GrassmannSpace (V,m,n) is void
let V be finite-dimensional VectSp of F; ::_thesis: for m, n being Nat st n <= dim V holds
not GrassmannSpace (V,m,n) is void
let m, n be Nat; ::_thesis: ( n <= dim V implies not GrassmannSpace (V,m,n) is void )
assume n <= dim V ; ::_thesis: not GrassmannSpace (V,m,n) is void
then not the topology of (GrassmannSpace (V,m,n)) is empty by Th22;
hence not GrassmannSpace (V,m,n) is void by PENCIL_1:def_4; ::_thesis: verum
end;
theorem Th26: :: PENCIL_4:26
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st 1 <= m & m < n & n < dim V holds
not GrassmannSpace (V,m,n) is degenerated
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for m, n being Nat st 1 <= m & m < n & n < dim V holds
not GrassmannSpace (V,m,n) is degenerated
let V be finite-dimensional VectSp of F; ::_thesis: for m, n being Nat st 1 <= m & m < n & n < dim V holds
not GrassmannSpace (V,m,n) is degenerated
let m, n be Nat; ::_thesis: ( 1 <= m & m < n & n < dim V implies not GrassmannSpace (V,m,n) is degenerated )
assume that
A1: 1 <= m and
A2: m < n and
A3: n < dim V ; ::_thesis: not GrassmannSpace (V,m,n) is degenerated
set S = GrassmannSpace (V,m,n);
A4: m < dim V by A2, A3, XXREAL_0:2;
hereby :: according to PENCIL_1:def_5 ::_thesis: verum
assume A5: the carrier of (GrassmannSpace (V,m,n)) is Block of (GrassmannSpace (V,m,n)) ; ::_thesis: contradiction
not the topology of (GrassmannSpace (V,m,n)) is empty by A3, Th22;
then consider W being Subspace of V such that
A6: dim W = n and
A7: m Subspaces_of V = m Subspaces_of W by A5, Def6;
(Omega). V = (Omega). W by A1, A4, A7, Th24;
then dim W = dim ((Omega). V) by VECTSP_9:27;
hence contradiction by A3, A6, VECTSP_9:27; ::_thesis: verum
end;
end;
theorem Th27: :: PENCIL_4:27
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st 1 <= m & m < n & n <= dim V holds
GrassmannSpace (V,m,n) is with_non_trivial_blocks
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for m, n being Nat st 1 <= m & m < n & n <= dim V holds
GrassmannSpace (V,m,n) is with_non_trivial_blocks
let V be finite-dimensional VectSp of F; ::_thesis: for m, n being Nat st 1 <= m & m < n & n <= dim V holds
GrassmannSpace (V,m,n) is with_non_trivial_blocks
let m, n be Nat; ::_thesis: ( 1 <= m & m < n & n <= dim V implies GrassmannSpace (V,m,n) is with_non_trivial_blocks )
assume that
A1: 1 <= m and
A2: m < n and
A3: n <= dim V ; ::_thesis: GrassmannSpace (V,m,n) is with_non_trivial_blocks
set S = GrassmannSpace (V,m,n);
let B be Block of (GrassmannSpace (V,m,n)); :: according to PENCIL_1:def_6 ::_thesis: 2 c= card B
not the topology of (GrassmannSpace (V,m,n)) is empty by A3, Th22;
then consider W being Subspace of V such that
A4: dim W = n and
A5: B = m Subspaces_of W by Def6;
m + 1 <= n by A2, NAT_1:13;
then consider U being strict Subspace of W such that
A6: dim U = m + 1 by A4, VECTSP_9:35;
set I = the Basis of U;
A7: card the Basis of U = m + 1 by A6, VECTSP_9:def_1;
reconsider I9 = the Basis of U as finite Subset of U by VECTSP_9:20;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
1 + 1 <= m + 1 by A1, XREAL_1:7;
then 2 c= card the Basis of U by A7, NAT_1:39;
then consider i, j being set such that
A8: i in the Basis of U and
A9: j in the Basis of U and
A10: i <> j by PENCIL_1:2;
reconsider I1 = I9 \ {i} as finite Subset of U ;
I1 c= the carrier of (Lin I1)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in I1 or a in the carrier of (Lin I1) )
assume a in I1 ; ::_thesis: a in the carrier of (Lin I1)
then a in Lin I1 by VECTSP_7:8;
hence a in the carrier of (Lin I1) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider I19 = I1 as Subset of (Lin I1) ;
A11: the Basis of U is linearly-independent by VECTSP_7:def_3;
then I1 is linearly-independent by VECTSP_7:1, XBOOLE_1:36;
then reconsider II1 = I19 as linearly-independent Subset of (Lin I1) by VECTSP_9:12;
Lin II1 = VectSpStr(# the carrier of (Lin I1), the U5 of (Lin I1), the ZeroF of (Lin I1), the lmult of (Lin I1) #) by VECTSP_9:17;
then A12: I1 is Basis of Lin I1 by VECTSP_7:def_3;
reconsider I2 = I9 \ {j} as finite Subset of U ;
I2 c= the carrier of (Lin I2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in I2 or a in the carrier of (Lin I2) )
assume a in I2 ; ::_thesis: a in the carrier of (Lin I2)
then a in Lin I2 by VECTSP_7:8;
hence a in the carrier of (Lin I2) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider I29 = I2 as Subset of (Lin I2) ;
I2 is linearly-independent by A11, VECTSP_7:1, XBOOLE_1:36;
then reconsider II2 = I29 as linearly-independent Subset of (Lin I2) by VECTSP_9:12;
Lin II2 = VectSpStr(# the carrier of (Lin I2), the U5 of (Lin I2), the ZeroF of (Lin I2), the lmult of (Lin I2) #) by VECTSP_9:17;
then A13: I2 is Basis of Lin I2 by VECTSP_7:def_3;
card I2 = (card I9) - (card {j}) by A9, EULER_1:4
.= (m + 1) - 1 by A7, CARD_1:30 ;
then A14: dim (Lin I2) = m by A13, VECTSP_9:def_1;
Lin I2 is strict Subspace of W by VECTSP_4:26;
then A15: Lin I2 in B by A5, A14, VECTSP_9:def_2;
card I1 = (card I9) - (card {i}) by A8, EULER_1:4
.= (m + 1) - 1 by A7, CARD_1:30 ;
then A16: dim (Lin I1) = m by A12, VECTSP_9:def_1;
Lin I1 is strict Subspace of W by VECTSP_4:26;
then A17: Lin I1 in B by A5, A16, VECTSP_9:def_2;
not j in {i} by A10, TARSKI:def_1;
then j in I1 by A9, XBOOLE_0:def_5;
then A18: j in Lin I1 by VECTSP_7:8;
not j in Lin I2 by A11, A9, VECTSP_9:14;
hence 2 c= card B by A17, A15, A18, PENCIL_1:2; ::_thesis: verum
end;
theorem Th28: :: PENCIL_4:28
for F being Field
for V being finite-dimensional VectSp of F
for m being Nat st m + 1 <= dim V holds
GrassmannSpace (V,m,(m + 1)) is identifying_close_blocks
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for m being Nat st m + 1 <= dim V holds
GrassmannSpace (V,m,(m + 1)) is identifying_close_blocks
let V be finite-dimensional VectSp of F; ::_thesis: for m being Nat st m + 1 <= dim V holds
GrassmannSpace (V,m,(m + 1)) is identifying_close_blocks
let m be Nat; ::_thesis: ( m + 1 <= dim V implies GrassmannSpace (V,m,(m + 1)) is identifying_close_blocks )
assume A1: m + 1 <= dim V ; ::_thesis: GrassmannSpace (V,m,(m + 1)) is identifying_close_blocks
set S = GrassmannSpace (V,m,(m + 1));
let K, L be Block of (GrassmannSpace (V,m,(m + 1))); :: according to PENCIL_1:def_7 ::_thesis: ( not 2 c= card (K /\ L) or K = L )
A2: not the topology of (GrassmannSpace (V,m,(m + 1))) is empty by A1, Th22;
then consider W1 being Subspace of V such that
A3: dim W1 = m + 1 and
A4: K = m Subspaces_of W1 by Def6;
assume 2 c= card (K /\ L) ; ::_thesis: K = L
then consider x, y being set such that
A5: x in K /\ L and
A6: y in K /\ L and
A7: x <> y by PENCIL_1:2;
y in K by A6, XBOOLE_0:def_4;
then consider Y being strict Subspace of W1 such that
A8: y = Y and
A9: dim Y = m by A4, VECTSP_9:def_2;
consider W2 being Subspace of V such that
A10: dim W2 = m + 1 and
A11: L = m Subspaces_of W2 by A2, Def6;
y in L by A6, XBOOLE_0:def_4;
then consider Y9 being strict Subspace of W2 such that
A12: y = Y9 and
dim Y9 = m by A11, VECTSP_9:def_2;
x in L by A5, XBOOLE_0:def_4;
then consider X9 being strict Subspace of W2 such that
A13: x = X9 and
dim X9 = m by A11, VECTSP_9:def_2;
x in K by A5, XBOOLE_0:def_4;
then consider X being strict Subspace of W1 such that
A14: x = X and
A15: dim X = m by A4, VECTSP_9:def_2;
reconsider x = x, y = y as strict Subspace of V by A14, A8, VECTSP_4:26;
A16: now__::_thesis:_not_dim_(x_+_y)_=_m
reconsider y9 = y as strict Subspace of x + y by VECTSP_5:7;
reconsider x9 = x as strict Subspace of x + y by VECTSP_5:7;
assume A17: dim (x + y) = m ; ::_thesis: contradiction
then (Omega). x9 = (Omega). (x + y) by A14, A15, VECTSP_9:28;
then x = y + x by VECTSP_5:5;
then A18: y is Subspace of x by VECTSP_5:8;
(Omega). y9 = (Omega). (x + y) by A8, A9, A17, VECTSP_9:28;
then x is Subspace of y by VECTSP_5:8;
hence contradiction by A7, A18, VECTSP_4:25; ::_thesis: verum
end;
x + y is Subspace of W1 by A14, A8, VECTSP_5:34;
then ( x is Subspace of x + y & dim (x + y) <= m + 1 ) by A3, VECTSP_5:7, VECTSP_9:25;
then A19: dim (x + y) = m + 1 by A14, A15, A16, NAT_1:9, VECTSP_9:25;
X9 + Y9 = x + y by A13, A12, VECTSP10:12;
then A20: (Omega). (X9 + Y9) = (Omega). W2 by A10, A19, VECTSP_9:28;
A21: X + Y = x + y by A14, A8, VECTSP10:12;
then (Omega). (X + Y) = (Omega). W1 by A3, A19, VECTSP_9:28;
hence K = L by A4, A11, A13, A12, A21, A20, Th23, VECTSP10:12; ::_thesis: verum
end;
theorem :: PENCIL_4:29
for F being Field
for V being finite-dimensional VectSp of F
for m being Nat st 1 <= m & m + 1 < dim V holds
GrassmannSpace (V,m,(m + 1)) is PLS
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F
for m being Nat st 1 <= m & m + 1 < dim V holds
GrassmannSpace (V,m,(m + 1)) is PLS
let V be finite-dimensional VectSp of F; ::_thesis: for m being Nat st 1 <= m & m + 1 < dim V holds
GrassmannSpace (V,m,(m + 1)) is PLS
let m be Nat; ::_thesis: ( 1 <= m & m + 1 < dim V implies GrassmannSpace (V,m,(m + 1)) is PLS )
assume that
A1: 1 <= m and
A2: m + 1 < dim V ; ::_thesis: GrassmannSpace (V,m,(m + 1)) is PLS
A3: m < m + 1 by NAT_1:13;
m <= dim V by A2, NAT_1:13;
hence GrassmannSpace (V,m,(m + 1)) is PLS by A1, A2, A3, Th25, Th26, Th27, Th28, VECTSP_9:36; ::_thesis: verum
end;
begin
definition
let X be set ;
func PairSet X -> set means :Def8: :: PENCIL_4:def 8
for z being set holds
( z in it iff ex x, y being set st
( x in X & y in X & z = {x,y} ) );
existence
ex b1 being set st
for z being set holds
( z in b1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) )
proof
defpred S1[ set ] means ex x, y being set st
( x in X & y in X & $1 = {x,y} );
consider S being set such that
A1: for z being set holds
( z in S iff ( z in bool X & S1[z] ) ) from XBOOLE_0:sch_1();
take S ; ::_thesis: for z being set holds
( z in S iff ex x, y being set st
( x in X & y in X & z = {x,y} ) )
let z be set ; ::_thesis: ( z in S iff ex x, y being set st
( x in X & y in X & z = {x,y} ) )
thus ( z in S implies S1[z] ) by A1; ::_thesis: ( ex x, y being set st
( x in X & y in X & z = {x,y} ) implies z in S )
assume A2: S1[z] ; ::_thesis: z in S
then z c= X by ZFMISC_1:32;
hence z in S by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for z being set holds
( z in b1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) & ( for z being set holds
( z in b2 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) holds
b1 = b2
proof
let p1, p2 be set ; ::_thesis: ( ( for z being set holds
( z in p1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) & ( for z being set holds
( z in p2 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) implies p1 = p2 )
assume that
A3: for z being set holds
( z in p1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) and
A4: for z being set holds
( z in p2 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ; ::_thesis: p1 = p2
now__::_thesis:_for_z_being_set_holds_
(_z_in_p1_iff_z_in_p2_)
let z be set ; ::_thesis: ( z in p1 iff z in p2 )
( z in p1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) by A3;
hence ( z in p1 iff z in p2 ) by A4; ::_thesis: verum
end;
hence p1 = p2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines PairSet PENCIL_4:def_8_:_
for X being set
for b2 being set holds
( b2 = PairSet X iff for z being set holds
( z in b2 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) );
registration
let X be non empty set ;
cluster PairSet X -> non empty ;
coherence
not PairSet X is empty
proof
consider x being set such that
A1: x in X by XBOOLE_0:def_1;
{x,x} in PairSet X by A1, Def8;
hence not PairSet X is empty ; ::_thesis: verum
end;
end;
definition
let t, X be set ;
func PairSet (t,X) -> set means :Def9: :: PENCIL_4:def 9
for z being set holds
( z in it iff ex y being set st
( y in X & z = {t,y} ) );
existence
ex b1 being set st
for z being set holds
( z in b1 iff ex y being set st
( y in X & z = {t,y} ) )
proof
t in {t} by TARSKI:def_1;
then A1: t in X \/ {t} by XBOOLE_0:def_3;
defpred S1[ set ] means ex y being set st
( y in X & $1 = {t,y} );
consider S being set such that
A2: for z being set holds
( z in S iff ( z in bool (X \/ {t}) & S1[z] ) ) from XBOOLE_0:sch_1();
take S ; ::_thesis: for z being set holds
( z in S iff ex y being set st
( y in X & z = {t,y} ) )
let z be set ; ::_thesis: ( z in S iff ex y being set st
( y in X & z = {t,y} ) )
thus ( z in S implies S1[z] ) by A2; ::_thesis: ( ex y being set st
( y in X & z = {t,y} ) implies z in S )
assume A3: S1[z] ; ::_thesis: z in S
then consider y being set such that
A4: y in X and
A5: z = {t,y} ;
y in X \/ {t} by A4, XBOOLE_0:def_3;
then z c= X \/ {t} by A5, A1, ZFMISC_1:32;
hence z in S by A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for z being set holds
( z in b1 iff ex y being set st
( y in X & z = {t,y} ) ) ) & ( for z being set holds
( z in b2 iff ex y being set st
( y in X & z = {t,y} ) ) ) holds
b1 = b2
proof
let p1, p2 be set ; ::_thesis: ( ( for z being set holds
( z in p1 iff ex y being set st
( y in X & z = {t,y} ) ) ) & ( for z being set holds
( z in p2 iff ex y being set st
( y in X & z = {t,y} ) ) ) implies p1 = p2 )
assume that
A6: for z being set holds
( z in p1 iff ex y being set st
( y in X & z = {t,y} ) ) and
A7: for z being set holds
( z in p2 iff ex y being set st
( y in X & z = {t,y} ) ) ; ::_thesis: p1 = p2
now__::_thesis:_for_z_being_set_holds_
(_z_in_p1_iff_z_in_p2_)
let z be set ; ::_thesis: ( z in p1 iff z in p2 )
( z in p1 iff ex y being set st
( y in X & z = {t,y} ) ) by A6;
hence ( z in p1 iff z in p2 ) by A7; ::_thesis: verum
end;
hence p1 = p2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines PairSet PENCIL_4:def_9_:_
for t, X being set
for b3 being set holds
( b3 = PairSet (t,X) iff for z being set holds
( z in b3 iff ex y being set st
( y in X & z = {t,y} ) ) );
registration
let t be set ;
let X be non empty set ;
cluster PairSet (t,X) -> non empty ;
coherence
not PairSet (t,X) is empty
proof
consider x being set such that
A1: x in X by XBOOLE_0:def_1;
{t,x} in PairSet (t,X) by A1, Def9;
hence not PairSet (t,X) is empty ; ::_thesis: verum
end;
end;
registration
let t be set ;
let X be non trivial set ;
cluster PairSet (t,X) -> non trivial ;
coherence
not PairSet (t,X) is trivial
proof
2 c= card X by PENCIL_1:4;
then consider x, y being set such that
A1: ( x in X & y in X ) and
A2: x <> y by PENCIL_1:2;
A3: now__::_thesis:_not_{t,x}_=_{t,y}
assume A4: {t,x} = {t,y} ; ::_thesis: contradiction
then y = t by A2, ZFMISC_1:6;
hence contradiction by A2, A4, ZFMISC_1:6; ::_thesis: verum
end;
( {t,x} in PairSet (t,X) & {t,y} in PairSet (t,X) ) by A1, Def9;
then 2 c= card (PairSet (t,X)) by A3, PENCIL_1:2;
hence not PairSet (t,X) is trivial by PENCIL_1:4; ::_thesis: verum
end;
end;
definition
let X be set ;
let L be Subset-Family of X;
func PairSetFamily L -> Subset-Family of (PairSet X) means :Def10: :: PENCIL_4:def 10
for S being set holds
( S in it iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) );
existence
ex b1 being Subset-Family of (PairSet X) st
for S being set holds
( S in b1 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) )
proof
set A = PairSet X;
defpred S1[ Subset of (PairSet X)] means ex t being set ex l being Subset of X st
( t in X & l in L & $1 = PairSet (t,l) );
consider F being Subset-Family of (PairSet X) such that
A1: for B being Subset of (PairSet X) holds
( B in F iff S1[B] ) from SUBSET_1:sch_3();
take F ; ::_thesis: for S being set holds
( S in F iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) )
let S be set ; ::_thesis: ( S in F iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) )
thus ( S in F implies ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) by A1; ::_thesis: ( ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) implies S in F )
given t being set , l being Subset of X such that A2: t in X and
A3: l in L and
A4: S = PairSet (t,l) ; ::_thesis: S in F
S c= PairSet X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in S or a in PairSet X )
assume a in S ; ::_thesis: a in PairSet X
then ex y being set st
( y in l & a = {t,y} ) by A4, Def9;
hence a in PairSet X by A2, Def8; ::_thesis: verum
end;
hence S in F by A1, A2, A3, A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of (PairSet X) st ( for S being set holds
( S in b1 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) ) & ( for S being set holds
( S in b2 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) ) holds
b1 = b2
proof
let p1, p2 be Subset-Family of (PairSet X); ::_thesis: ( ( for S being set holds
( S in p1 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) ) & ( for S being set holds
( S in p2 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) ) implies p1 = p2 )
assume that
A5: for z being set holds
( z in p1 iff ex t being set ex l being Subset of X st
( t in X & l in L & z = PairSet (t,l) ) ) and
A6: for z being set holds
( z in p2 iff ex t being set ex l being Subset of X st
( t in X & l in L & z = PairSet (t,l) ) ) ; ::_thesis: p1 = p2
now__::_thesis:_for_z_being_set_holds_
(_z_in_p1_iff_z_in_p2_)
let z be set ; ::_thesis: ( z in p1 iff z in p2 )
( z in p1 iff ex t being set ex l being Subset of X st
( t in X & l in L & z = PairSet (t,l) ) ) by A5;
hence ( z in p1 iff z in p2 ) by A6; ::_thesis: verum
end;
hence p1 = p2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines PairSetFamily PENCIL_4:def_10_:_
for X being set
for L being Subset-Family of X
for b3 being Subset-Family of (PairSet X) holds
( b3 = PairSetFamily L iff for S being set holds
( S in b3 iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet (t,l) ) ) );
registration
let X be non empty set ;
let L be non empty Subset-Family of X;
cluster PairSetFamily L -> non empty ;
coherence
not PairSetFamily L is empty
proof
consider l being set such that
A1: l in L by XBOOLE_0:def_1;
consider t being set such that
A2: t in X by XBOOLE_0:def_1;
PairSet (t,l) in PairSetFamily L by A2, A1, Def10;
hence not PairSetFamily L is empty ; ::_thesis: verum
end;
end;
definition
let S be TopStruct ;
func VeroneseSpace S -> strict TopStruct equals :: PENCIL_4:def 11
TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #);
coherence
TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #) is strict TopStruct ;
end;
:: deftheorem defines VeroneseSpace PENCIL_4:def_11_:_
for S being TopStruct holds VeroneseSpace S = TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #);
registration
let S be non empty TopStruct ;
cluster VeroneseSpace S -> non empty strict ;
coherence
not VeroneseSpace S is empty ;
end;
registration
let S be non empty non void TopStruct ;
cluster VeroneseSpace S -> strict non void ;
coherence
not VeroneseSpace S is void
proof
thus not the topology of (VeroneseSpace S) is empty ; :: according to PENCIL_1:def_4 ::_thesis: verum
end;
end;
registration
let S be non empty non void non degenerated TopStruct ;
cluster VeroneseSpace S -> strict non degenerated ;
coherence
not VeroneseSpace S is degenerated
proof
assume the carrier of (VeroneseSpace S) is Block of (VeroneseSpace S) ; :: according to PENCIL_1:def_5 ::_thesis: contradiction
then consider t being set , l being Subset of S such that
A1: t in the carrier of S and
A2: l in the topology of S and
A3: PairSet the carrier of S = PairSet (t,l) by Def10;
not the carrier of S in the topology of S by PENCIL_1:def_5;
then not the carrier of S c= l by A2, XBOOLE_0:def_10;
then consider s being set such that
A4: s in the carrier of S and
A5: not s in l by TARSKI:def_3;
now__::_thesis:_not_{t,s}_in_PairSet_(t,l)
assume {t,s} in PairSet (t,l) ; ::_thesis: contradiction
then A6: ex z being set st
( z in l & {t,s} = {t,z} ) by Def9;
then s = t by A5, ZFMISC_1:6;
hence contradiction by A5, A6, ZFMISC_1:6; ::_thesis: verum
end;
hence contradiction by A1, A3, A4, Def8; ::_thesis: verum
end;
end;
registration
let S be non empty non void with_non_trivial_blocks TopStruct ;
cluster VeroneseSpace S -> strict with_non_trivial_blocks ;
coherence
VeroneseSpace S is with_non_trivial_blocks
proof
let L be Block of (VeroneseSpace S); :: according to PENCIL_1:def_6 ::_thesis: 2 c= card L
consider t being set , l being Subset of S such that
t in the carrier of S and
A1: l in the topology of S and
A2: L = PairSet (t,l) by Def10;
2 c= card l by A1, PENCIL_1:def_6;
then reconsider l = l as non trivial set by PENCIL_1:4;
not PairSet (t,l) is trivial ;
hence 2 c= card L by A2, PENCIL_1:4; ::_thesis: verum
end;
end;
registration
let S be identifying_close_blocks TopStruct ;
cluster VeroneseSpace S -> strict identifying_close_blocks ;
coherence
VeroneseSpace S is identifying_close_blocks
proof
let K, L be Block of (VeroneseSpace S); :: according to PENCIL_1:def_7 ::_thesis: ( not 2 c= card (K /\ L) or K = L )
assume 2 c= card (K /\ L) ; ::_thesis: K = L
then consider a, b being set such that
A1: a in K /\ L and
A2: b in K /\ L and
A3: a <> b by PENCIL_1:2;
A4: a in K by A1, XBOOLE_0:def_4;
then A5: not the topology of (VeroneseSpace S) is empty by SUBSET_1:def_1;
then consider t being set , k being Subset of S such that
t in the carrier of S and
A6: k in the topology of S and
A7: K = PairSet (t,k) by Def10;
b in K by A2, XBOOLE_0:def_4;
then consider y being set such that
A8: y in k and
A9: b = {t,y} by A7, Def9;
consider x being set such that
A10: x in k and
A11: a = {t,x} by A4, A7, Def9;
consider s being set , l being Subset of S such that
s in the carrier of S and
A12: l in the topology of S and
A13: L = PairSet (s,l) by A5, Def10;
a in L by A1, XBOOLE_0:def_4;
then consider z being set such that
A14: z in l and
A15: a = {s,z} by A13, Def9;
b in L by A2, XBOOLE_0:def_4;
then consider w being set such that
A16: w in l and
A17: b = {s,w} by A13, Def9;
A18: ( t = s or t = z ) by A11, A15, ZFMISC_1:6;
now__::_thesis:_not_y_<>_w
assume A19: y <> w ; ::_thesis: contradiction
then y = t by A3, A9, A15, A17, A18, ZFMISC_1:6;
hence contradiction by A9, A17, A19, ZFMISC_1:6; ::_thesis: verum
end;
then A20: y in k /\ l by A8, A16, XBOOLE_0:def_4;
A21: ( t = s or t = w ) by A9, A17, ZFMISC_1:6;
now__::_thesis:_not_x_<>_z
assume A22: x <> z ; ::_thesis: contradiction
then x = t by A3, A11, A15, A17, A21, ZFMISC_1:6;
hence contradiction by A11, A15, A22, ZFMISC_1:6; ::_thesis: verum
end;
then x in k /\ l by A10, A14, XBOOLE_0:def_4;
then 2 c= card (k /\ l) by A3, A11, A9, A20, PENCIL_1:2;
hence K = L by A3, A6, A7, A12, A13, A15, A17, A18, A21, PENCIL_1:def_7; ::_thesis: verum
end;
end;