:: PENCIL_4 semantic presentation

theorem Th1: :: PENCIL_4:1

for b₁, b₂ being Nat st 1 <= b₁ & b₁ < b₂ & 3 <= b₂ & not b₁ + 1 < b₂ holds
2 <= b₁

proof end;

theorem Th2: :: PENCIL_4:2

for b₁ being finite set
for b₂ being Nat st b₂ <= card b₁ holds
ex b₃ being Subset of b₁ st card b₃ = b₂

proof end;

theorem Th3: :: PENCIL_4:3

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂ holds b₃ is Subspace of (Omega). b₂

proof end;

theorem Th4: :: PENCIL_4:4

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of (Omega). b₂ holds b₃ is Subspace of b₂

proof end;

theorem Th5: :: PENCIL_4:5

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂ holds (Omega). b₃ is Subspace of b₂

proof end;

theorem Th6: :: PENCIL_4:6

for b₁ being Field
for b₂, b₃ being VectSp of b₁ st (Omega). b₃ is Subspace of b₂ holds
b₃ is Subspace of b₂

proof end;

definition

let c₁ be Field;
let c₂ be VectSp of c₁;
let c₃, c₄ be Subspace of c₂;
func segment c₃,c₄ -> Subset of (Subspaces a₂) means :Def1: :: PENCIL_4:def 1
for b₁ being strict Subspace of a₂ holds
( b₁ in a₅ iff ( a₃ is Subspace of b₁ & b₁ is Subspace of a₄ ) ) if a₃ is Subspace of a₄
otherwise a₅ = {} ;
consistency ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines segment PENCIL_4:def 1 :

theorem Th7: :: PENCIL_4:7

for b₁ being Field
for b₂ being VectSp of b₁
for b₃, b₄, b₅, b₆ being Subspace of b₂ st b₃ is Subspace of b₄ & b₅ is Subspace of b₆ & (Omega). b₃ = (Omega). b₅ & (Omega). b₄ = (Omega). b₆ holds
segment b₃,b₄ = segment b₅,b₆

proof end;

definition

let c₁ be Field;
let c₂ be VectSp of c₁;
let c₃, c₄ be Subspace of c₂;
func pencil c₃,c₄ -> Subset of (Subspaces a₂) equals :: PENCIL_4:def 2
(segment a₃,a₄) \ {((Omega). a₃),((Omega). a₄)};
coherence

proof end;

end;

:: deftheorem Def2 defines pencil PENCIL_4:def 2 :

theorem Th8: :: PENCIL_4:8

definition

let c₁ be Field;
let c₂ be finite-dimensional VectSp of c₁;
let c₃, c₄ be Subspace of c₂;
let c₅ be Nat;
func pencil c₃,c₄,c₅ -> Subset of (a₅ Subspaces_of a₂) equals :: PENCIL_4:def 3
(pencil a₃,a₄) /\ (a₅ Subspaces_of a₂);
coherence by XBOOLE_1:17;

end;

:: deftheorem Def3 defines pencil PENCIL_4:def 3 :

theorem Th9: :: PENCIL_4:9

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Nat
for b₄, b₅, b₆ being Subspace of b₂ st b₆ in pencil b₄,b₅,b₃ holds
( b₄ is Subspace of b₆ & b₆ is Subspace of b₅ )

proof end;

theorem Th10: :: PENCIL_4:10

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Nat
for b₄, b₅, b₆, b₇ being Subspace of b₂ st b₄ is Subspace of b₅ & b₆ is Subspace of b₇ & (Omega). b₄ = (Omega). b₆ & (Omega). b₅ = (Omega). b₇ holds
pencil b₄,b₅,b₃ = pencil b₆,b₇,b₃ by Th8;

definition

let c₁ be Field;
let c₂ be finite-dimensional VectSp of c₁;
let c₃ be Nat;
func c₃ Pencils_of c₂ -> Subset-Family of (a₃ Subspaces_of a₂) means :Def4: :: PENCIL_4:def 4
for b₁ being set holds
( b₁ in a₄ iff ex b₂, b₃ being Subspace of a₂ st
( b₂ is Subspace of b₃ & (dim b₂) + 1 = a₃ & dim b₃ = a₃ + 1 & b₁ = pencil b₂,b₃,a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Pencils_of PENCIL_4:def 4 :

theorem Th11: :: PENCIL_4:11

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Nat st 1 <= b₃ & b₃ < dim b₂ holds
not b₃ Pencils_of b₂ is empty

proof end;

theorem Th12: :: PENCIL_4:12

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃, b₄, b₅, b₆ being Subspace of b₂
for b₇ being Nat st 1 <= b₇ & b₇ < dim b₂ & (dim b₃) + 1 = b₇ & dim b₄ = b₇ + 1 & b₅ in pencil b₃,b₄,b₇ & b₆ in pencil b₃,b₄,b₇ & b₅ <> b₆ holds
( b₅ /\ b₆ = (Omega). b₃ & b₅ + b₆ = (Omega). b₄ )

proof end;

theorem Th13: :: PENCIL_4:13

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Vector of b₂ st b₃ <> 0. b₂ holds
dim (Lin {b₃}) = 1

proof end;

theorem Th14: :: PENCIL_4:14

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Vector of b₂ st not b₄ in b₃ holds
dim (b₃ + (Lin {b₄})) = (dim b₃) + 1

proof end;

theorem Th15: :: PENCIL_4:15

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Subspace of b₂
for b₄, b₅ being Vector of b₂ st not b₄ in b₃ & not b₅ in b₃ & b₄ <> b₅ & {b₄,b₅} is linearly-independent & b₃ /\ (Lin {b₄,b₅}) = (0). b₂ holds
dim (b₃ + (Lin {b₄,b₅})) = (dim b₃) + 2

proof end;

theorem Th16: :: PENCIL_4:16

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃, b₄ being Subspace of b₂ st b₃ is Subspace of b₄ holds
for b₅ being Nat st 1 <= b₅ & b₅ < dim b₂ & (dim b₃) + 1 = b₅ & dim b₄ = b₅ + 1 holds
for b₆ being Vector of b₂ st b₆ in b₄ & not b₆ in b₃ holds
b₃ + (Lin {b₆}) in pencil b₃,b₄,b₅

proof end;

theorem Th17: :: PENCIL_4:17

proof end;

definition

let c₁ be Field;
let c₂ be finite-dimensional VectSp of c₁;
let c₃ be Nat;
func PencilSpace c₂,c₃ -> strict TopStruct equals :: PENCIL_4:def 5
TopStruct(# (a₃ Subspaces_of a₂),(a₃ Pencils_of a₂) #);
coherence ;

end;

:: deftheorem Def5 defines PencilSpace PENCIL_4:def 5 :

theorem Th18: :: PENCIL_4:18

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Nat st b₃ <= dim b₂ holds
not PencilSpace b₂,b₃ is empty

proof end;

theorem Th19: :: PENCIL_4:19

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Nat st 1 <= b₃ & b₃ < dim b₂ holds
not PencilSpace b₂,b₃ is void

proof end;

theorem Th20: :: PENCIL_4:20

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Nat st 1 <= b₃ & b₃ < dim b₂ & 3 <= dim b₂ holds
not PencilSpace b₂,b₃ is degenerated

proof end;

theorem Th21: :: PENCIL_4:21

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Nat st 1 <= b₃ & b₃ < dim b₂ holds
PencilSpace b₂,b₃ is with_non_trivial_blocks

proof end;

theorem Th22: :: PENCIL_4:22

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Nat st 1 <= b₃ & b₃ < dim b₂ holds
PencilSpace b₂,b₃ is identifying_close_blocks

proof end;

theorem Th23: :: PENCIL_4:23

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Nat st 1 <= b₃ & b₃ < dim b₂ & 3 <= dim b₂ holds
PencilSpace b₂,b₃ is PLS by Th18, Th19, Th20, Th21, Th22;

definition

let c₁ be Field;
let c₂ be finite-dimensional VectSp of c₁;
let c₃, c₄ be Nat;
func SubspaceSet c₂,c₃,c₄ -> Subset-Family of (a₃ Subspaces_of a₂) means :Def6: :: PENCIL_4:def 6
for b₁ being set holds
( b₁ in a₅ iff ex b₂ being Subspace of a₂ st
( dim b₂ = a₄ & b₁ = a₃ Subspaces_of b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines SubspaceSet PENCIL_4:def 6 :

theorem Th24: :: PENCIL_4:24

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃, b₄ being Nat st b₄ <= dim b₂ holds
not SubspaceSet b₂,b₃,b₄ is empty

proof end;

theorem Th25: :: PENCIL_4:25

for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁ st (Omega). b₂ = (Omega). b₃ holds
for b₄ being Nat holds b₄ Subspaces_of b₂ = b₄ Subspaces_of b₃

proof end;

theorem Th26: :: PENCIL_4:26

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Nat st 1 <= b₄ & b₄ <= dim b₂ & b₄ Subspaces_of b₂ c= b₄ Subspaces_of b₃ holds
(Omega). b₂ = (Omega). b₃

proof end;

definition

let c₁ be Field;
let c₂ be finite-dimensional VectSp of c₁;
let c₃, c₄ be Nat;
func GrassmannSpace c₂,c₃,c₄ -> strict TopStruct equals :: PENCIL_4:def 7
TopStruct(# (a₃ Subspaces_of a₂),(SubspaceSet a₂,a₃,a₄) #);
coherence ;

end;

:: deftheorem Def7 defines GrassmannSpace PENCIL_4:def 7 :

theorem Th27: :: PENCIL_4:27

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃, b₄ being Nat st b₃ <= dim b₂ holds
not GrassmannSpace b₂,b₃,b₄ is empty

proof end;

theorem Th28: :: PENCIL_4:28

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃, b₄ being Nat st b₄ <= dim b₂ holds
not GrassmannSpace b₂,b₃,b₄ is void

proof end;

theorem Th29: :: PENCIL_4:29

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃, b₄ being Nat st 1 <= b₃ & b₃ < b₄ & b₄ < dim b₂ holds
not GrassmannSpace b₂,b₃,b₄ is degenerated

proof end;

theorem Th30: :: PENCIL_4:30

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃, b₄ being Nat st 1 <= b₃ & b₃ < b₄ & b₄ <= dim b₂ holds
GrassmannSpace b₂,b₃,b₄ is with_non_trivial_blocks

proof end;

theorem Th31: :: PENCIL_4:31

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Nat st 1 <= b₃ & b₃ + 1 <= dim b₂ holds
GrassmannSpace b₂,b₃,(b₃ + 1) is identifying_close_blocks

proof end;

theorem Th32: :: PENCIL_4:32

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Nat st 1 <= b₃ & b₃ + 1 < dim b₂ holds
GrassmannSpace b₂,b₃,(b₃ + 1) is PLS

proof end;

definition

let c₁ be set ;
func PairSet c₁ -> set means :Def8: :: PENCIL_4:def 8
for b₁ being set holds
( b₁ in a₂ iff ex b₂, b₃ being set st
( b₂ in a₁ & b₃ in a₁ & b₁ = {b₂,b₃} ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines PairSet PENCIL_4:def 8 :

registration

let c₁ be non empty set ;
cluster PairSet a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁, c₂ be set ;
func PairSet c₁,c₂ -> set means :Def9: :: PENCIL_4:def 9
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being set st
( b₂ in a₂ & b₁ = {a₁,b₂} ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines PairSet PENCIL_4:def 9 :

registration

let c₁ be set ;
let c₂ be non empty set ;
cluster PairSet a₁,a₂ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be non trivial set ;
cluster PairSet a₁,a₂ -> non empty non trivial ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
func PairSetFamily c₂ -> Subset-Family of (PairSet a₁) means :Def10: :: PENCIL_4:def 10
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being set ex b₃ being Subset of a₁ st
( b₂ in a₁ & b₃ in a₂ & b₁ = PairSet b₂,b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines PairSetFamily PENCIL_4:def 10 :

registration

let c₁ be non empty set ;
let c₂ be non empty Subset-Family of c₁;
cluster PairSetFamily a₂ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be TopStruct ;
func VeroneseSpace c₁ -> strict TopStruct equals :: PENCIL_4:def 11
TopStruct(# (PairSet the carrier of a₁),(PairSetFamily the topology of a₁) #);
coherence ;

end;

:: deftheorem Def11 defines VeroneseSpace PENCIL_4:def 11 :

registration

let c₁ be non empty TopStruct ;
cluster VeroneseSpace a₁ -> non empty strict ;
coherence

proof end;

end;

registration

let c₁ be non empty non void TopStruct ;
cluster VeroneseSpace a₁ -> non empty strict non void ;
coherence

proof end;

end;

registration

let c₁ be non empty non void non degenerated TopStruct ;
cluster VeroneseSpace a₁ -> non empty strict non void non degenerated ;
coherence

proof end;

end;

registration

let c₁ be non empty non void with_non_trivial_blocks TopStruct ;
cluster VeroneseSpace a₁ -> non empty strict non void with_non_trivial_blocks ;
coherence

proof end;

end;

registration

let c₁ be identifying_close_blocks TopStruct ;
cluster VeroneseSpace a₁ -> strict identifying_close_blocks ;
coherence

proof end;

end;

definition

let c₁ be PLS;
redefine func VeroneseSpace as VeroneseSpace c₁ -> strict PLS;
coherence ;

end;