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