:: ANPROJ_1 semantic presentation

notation

let c₁ be RealLinearSpace;
let c₂ be Element of c₁;
synonym c₂ is_Prop_Vect for non-zero c₂;

end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃ be Element of c₁;
canceled;
pred are_Prop c₂,c₃ means :Def2: :: ANPROJ_1:def 2
ex b₁, b₂ being Real st
( b₁ * a₂ = b₂ * a₃ & b₁ <> 0 & b₂ <> 0 );
reflexivity

proof end;

symmetry ;

end;

:: deftheorem Def1 ANPROJ_1:def 1 :

:: deftheorem Def2 defines are_Prop ANPROJ_1:def 2 :

theorem Th1: :: ANPROJ_1:1

canceled;

theorem Th2: :: ANPROJ_1:2

canceled;

theorem Th3: :: ANPROJ_1:3

canceled;

theorem Th4: :: ANPROJ_1:4

canceled;

theorem Th5: :: ANPROJ_1:5

for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁ holds
( are_Prop b₂,b₃ iff ex b₄ being Real st
( b₄ <> 0 & b₂ = b₄ * b₃ ) )

proof end;

theorem Th6: :: ANPROJ_1:6

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁ st are_Prop b₂,b₃ & are_Prop b₃,b₄ holds
are_Prop b₂,b₄

proof end;

theorem Th7: :: ANPROJ_1:7

for b₁ being RealLinearSpace
for b₂ being Element of b₁ holds
( are_Prop b₂, 0. b₁ iff b₂ = 0. b₁ )

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄ be Element of c₁;
pred c₂,c₃,c₄ are_LinDep means :Def3: :: ANPROJ_1:def 3
ex b₁, b₂, b₃ being Real st
( ((b₁ * a₂) + (b₂ * a₃)) + (b₃ * a₄) = 0. a₁ & ( b₁ <> 0 or b₂ <> 0 or b₃ <> 0 ) );

end;

:: deftheorem Def3 defines are_LinDep ANPROJ_1:def 3 :

theorem Th8: :: ANPROJ_1:8

canceled;

theorem Th9: :: ANPROJ_1:9

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st are_Prop b₂,b₃ & are_Prop b₄,b₅ & are_Prop b₆,b₇ & b₂,b₄,b₆ are_LinDep holds
b₃,b₅,b₇ are_LinDep

proof end;

theorem Th10: :: ANPROJ_1:10

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁ st b₂,b₃,b₄ are_LinDep holds
( b₂,b₄,b₃ are_LinDep & b₃,b₂,b₄ are_LinDep & b₄,b₃,b₂ are_LinDep & b₄,b₂,b₃ are_LinDep & b₃,b₄,b₂ are_LinDep )

proof end;

Lemma8: for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁
for b₄, b₅ being Real st (b₄ * b₂) + (b₅ * b₃) = 0. b₁ holds
b₄ * b₂ = (- b₅) * b₃

proof end;

Lemma9: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁
for b₅, b₆, b₇ being Real st ((b₅ * b₂) + (b₆ * b₃)) + (b₇ * b₄) = 0. b₁ & b₅ <> 0 holds
b₂ = ((- ((b₅ " ) * b₆)) * b₃) + ((- ((b₅ " ) * b₇)) * b₄)

proof end;

theorem Th11: :: ANPROJ_1:11

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁ st b₂ is_Prop_Vect & b₃ is_Prop_Vect & not are_Prop b₂,b₃ holds
( b₂,b₃,b₄ are_LinDep iff ex b₅, b₆ being Real st b₄ = (b₅ * b₂) + (b₆ * b₃) )

proof end;

Lemma11: for b₁ being RealLinearSpace
for b₂ being Element of b₁
for b₃, b₄, b₅ being Real holds ((b₃ + b₄) + b₅) * b₂ = ((b₃ * b₂) + (b₄ * b₂)) + (b₅ * b₂)

proof end;

Lemma12: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ holds ((b₂ + b₃) + b₄) + ((b₅ + b₆) + b₇) = ((b₂ + b₅) + (b₃ + b₆)) + (b₄ + b₇)

proof end;

Lemma13: for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁
for b₄, b₅, b₆ being Real holds ((b₄ * b₅) * b₂) + ((b₄ * b₆) * b₃) = b₄ * ((b₅ * b₂) + (b₆ * b₃))

proof end;

theorem Th12: :: ANPROJ_1:12

for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁
for b₄, b₅, b₆, b₇ being Real st not are_Prop b₂,b₃ & (b₄ * b₂) + (b₅ * b₃) = (b₆ * b₂) + (b₇ * b₃) & b₂ is_Prop_Vect & b₃ is_Prop_Vect holds
( b₄ = b₆ & b₅ = b₇ )

proof end;

Lemma14: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁
for b₅, b₆ being Real st b₂ + (b₅ * b₃) = b₄ + (b₆ * b₃) holds
((b₅ - b₆) * b₃) + b₂ = b₄

proof end;

theorem Th13: :: ANPROJ_1:13

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁
for b₅, b₆, b₇, b₈, b₉, b₁₀ being Real st not b₂,b₃,b₄ are_LinDep & ((b₅ * b₂) + (b₆ * b₃)) + (b₇ * b₄) = ((b₈ * b₂) + (b₉ * b₃)) + (b₁₀ * b₄) holds
( b₅ = b₈ & b₆ = b₉ & b₇ = b₁₀ )

proof end;

theorem Th14: :: ANPROJ_1:14

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆, b₇, b₈, b₉ being Real st not are_Prop b₂,b₃ & b₄ = (b₆ * b₂) + (b₇ * b₃) & b₅ = (b₈ * b₂) + (b₉ * b₃) & (b₆ * b₉) - (b₈ * b₇) = 0 & b₂ is_Prop_Vect & b₃ is_Prop_Vect & not are_Prop b₄,b₅ & not b₄ = 0. b₁ holds
b₅ = 0. b₁

proof end;

theorem Th15: :: ANPROJ_1:15

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁ st ( b₂ = 0. b₁ or b₃ = 0. b₁ or b₄ = 0. b₁ ) holds
b₂,b₃,b₄ are_LinDep

proof end;

theorem Th16: :: ANPROJ_1:16

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁ st ( are_Prop b₂,b₃ or are_Prop b₄,b₂ or are_Prop b₃,b₄ ) holds
b₄,b₂,b₃ are_LinDep

proof end;

theorem Th17: :: ANPROJ_1:17

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁ st not b₂,b₃,b₄ are_LinDep holds
( b₂ is_Prop_Vect & b₃ is_Prop_Vect & b₄ is_Prop_Vect & not are_Prop b₂,b₃ & not are_Prop b₃,b₄ & not are_Prop b₄,b₂ )

proof end;

theorem Th18: :: ANPROJ_1:18

for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁ st b₂ + b₃ = 0. b₁ holds
are_Prop b₂,b₃

proof end;

theorem Th19: :: ANPROJ_1:19

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not are_Prop b₂,b₃ & b₂,b₃,b₄ are_LinDep & b₂,b₃,b₅ are_LinDep & b₂,b₃,b₆ are_LinDep & b₂ is_Prop_Vect & b₃ is_Prop_Vect holds
b₄,b₅,b₆ are_LinDep

proof end;

Lemma21: for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁
for b₄, b₅, b₆ being Real holds b₄ * ((b₅ * b₂) + (b₆ * b₃)) = ((b₄ * b₅) * b₂) + ((b₄ * b₆) * b₃)

proof end;

theorem Th20: :: ANPROJ_1:20

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃,b₄ are_LinDep & b₂,b₃,b₅ are_LinDep & b₃,b₄,b₆ are_LinDep holds
ex b₇ being Element of b₁ st
( b₂,b₄,b₇ are_LinDep & b₅,b₆,b₇ are_LinDep & b₇ is_Prop_Vect )

proof end;

theorem Th21: :: ANPROJ_1:21

for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁ st not are_Prop b₂,b₃ & b₂ is_Prop_Vect & b₃ is_Prop_Vect holds
for b₄, b₅ being Element of b₁ ex b₆ being Element of b₁ st
( b₆ is_Prop_Vect & b₄,b₅,b₆ are_LinDep & not are_Prop b₄,b₆ & not are_Prop b₅,b₆ )

proof end;

Lemma22: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁ st not b₂,b₃,b₄ are_LinDep holds
for b₅, b₆ being Element of b₁ st b₅ is_Prop_Vect & b₆ is_Prop_Vect & not are_Prop b₅,b₆ holds
ex b₇ being Element of b₁ st not b₅,b₆,b₇ are_LinDep

proof end;

theorem Th22: :: ANPROJ_1:22

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁ st not b₂,b₃,b₄ are_LinDep holds
for b₅, b₆ being Element of b₁ st b₅ is_Prop_Vect & b₆ is_Prop_Vect & not are_Prop b₅,b₆ holds
ex b₇ being Element of b₁ st
( b₇ is_Prop_Vect & not b₅,b₆,b₇ are_LinDep )

proof end;

Lemma23: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁
for b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being Real holds ((b₁₁ * ((b₅ * b₂) + (b₆ * b₃))) + (b₁₂ * ((b₇ * b₃) + (b₈ * b₄)))) + (b₁₃ * ((b₉ * b₂) + (b₁₀ * b₄))) = ((((b₁₁ * b₅) + (b₁₃ * b₉)) * b₂) + (((b₁₁ * b₆) + (b₁₂ * b₇)) * b₃)) + (((b₁₂ * b₈) + (b₁₃ * b₁₀)) * b₄)

proof end;

theorem Th23: :: ANPROJ_1:23

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of b₁ st b₂,b₃,b₄ are_LinDep & b₅,b₆,b₄ are_LinDep & b₂,b₅,b₇ are_LinDep & b₃,b₆,b₇ are_LinDep & b₂,b₆,b₈ are_LinDep & b₃,b₅,b₈ are_LinDep & b₇,b₄,b₈ are_LinDep & b₇ is_Prop_Vect & b₄ is_Prop_Vect & b₈ is_Prop_Vect & not b₂,b₃,b₆ are_LinDep & not b₂,b₃,b₅ are_LinDep & not b₂,b₅,b₆ are_LinDep holds
b₃,b₅,b₆ are_LinDep

proof end;

definition

let c₁ be RealLinearSpace;
func Proper_Vectors_of c₁ -> set means :Def4: :: ANPROJ_1:def 4
for b₁ being set holds
( b₁ in a₂ iff ( b₁ <> 0. a₁ & b₁ is Element of a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Proper_Vectors_of ANPROJ_1:def 4 :

theorem Th24: :: ANPROJ_1:24

canceled;

theorem Th25: :: ANPROJ_1:25

canceled;

theorem Th26: :: ANPROJ_1:26

for b₁ being RealLinearSpace
for b₂ being Element of b₁ holds
( b₂ in Proper_Vectors_of b₁ iff b₂ is_Prop_Vect )

proof end;

definition

let c₁ be RealLinearSpace;
func Proportionality_as_EqRel_of c₁ -> Equivalence_Relation of Proper_Vectors_of a₁ means :Def5: :: ANPROJ_1:def 5
for b₁, b₂ being set holds
( [b₁,b₂] in a₂ iff ( b₁ in Proper_Vectors_of a₁ & b₂ in Proper_Vectors_of a₁ & ex b₃, b₄ being Element of a₁ st
( b₁ = b₃ & b₂ = b₄ & are_Prop b₃,b₄ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Proportionality_as_EqRel_of ANPROJ_1:def 5 :

theorem Th27: :: ANPROJ_1:27

canceled;

theorem Th28: :: ANPROJ_1:28

for b₁ being RealLinearSpace
for b₂, b₃ being set st [b₂,b₃] in Proportionality_as_EqRel_of b₁ holds
( b₂ is Element of b₁ & b₃ is Element of b₁ )

proof end;

theorem Th29: :: ANPROJ_1:29

for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁ holds
( [b₂,b₃] in Proportionality_as_EqRel_of b₁ iff ( b₂ is_Prop_Vect & b₃ is_Prop_Vect & are_Prop b₂,b₃ ) )

proof end;

definition

let c₁ be RealLinearSpace;
let c₂ be Element of c₁;
func Dir c₂ -> Subset of (Proper_Vectors_of a₁) equals :: ANPROJ_1:def 6
Class (Proportionality_as_EqRel_of a₁),a₂;
correctness ;

end;

:: deftheorem Def6 defines Dir ANPROJ_1:def 6 :

definition

let c₁ be RealLinearSpace;
func ProjectivePoints c₁ -> set means :Def7: :: ANPROJ_1:def 7
ex b₁ being Subset-Family of (Proper_Vectors_of a₁) st
( b₁ = Class (Proportionality_as_EqRel_of a₁) & a₂ = b₁ );
correctness ;

end;

:: deftheorem Def7 defines ProjectivePoints ANPROJ_1:def 7 :

definition

let c₁ be non empty ZeroStr ;
redefine attr a₁ is trivial means :Def8: :: ANPROJ_1:def 8
for b₁ being Element of a₁ holds b₁ = 0. a₁;
compatibility

proof end;

end;

:: deftheorem Def8 defines trivial ANPROJ_1:def 8 :

registration

cluster strict non trivial RLSStruct ;
existence

proof end;

end;

theorem Th30: :: ANPROJ_1:30

canceled;

theorem Th31: :: ANPROJ_1:31

canceled;

theorem Th32: :: ANPROJ_1:32

canceled;

theorem Th33: :: ANPROJ_1:33

for b₁ being RealLinearSpace holds
( b₁ is non trivial RealLinearSpace iff ex b₂ being Element of b₁ st b₂ in Proper_Vectors_of b₁ )

proof end;

registration

let c₁ be non trivial RealLinearSpace;
cluster Proper_Vectors_of a₁ -> non empty ;
coherence

proof end;

cluster ProjectivePoints a₁ -> non empty ;
coherence

proof end;

end;

theorem Th34: :: ANPROJ_1:34

for b₁ being non trivial RealLinearSpace
for b₂ being Element of b₁ st b₂ is_Prop_Vect holds
Dir b₂ is Element of ProjectivePoints b₁

proof end;

theorem Th35: :: ANPROJ_1:35

for b₁ being non trivial RealLinearSpace
for b₂, b₃ being Element of b₁ st b₂ is_Prop_Vect & b₃ is_Prop_Vect holds
( Dir b₂ = Dir b₃ iff are_Prop b₂,b₃ )

proof end;

definition

let c₁ be non trivial RealLinearSpace;
func ProjectiveCollinearity c₁ -> Relation3 of ProjectivePoints a₁ means :Def9: :: ANPROJ_1:def 9
for b₁, b₂, b₃ being set holds
( [b₁,b₂,b₃] in a₂ iff ex b₄, b₅, b₆ being Element of a₁ st
( b₁ = Dir b₄ & b₂ = Dir b₅ & b₃ = Dir b₆ & b₄ is_Prop_Vect & b₅ is_Prop_Vect & b₆ is_Prop_Vect & b₄,b₅,b₆ are_LinDep ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines ProjectiveCollinearity ANPROJ_1:def 9 :

definition

let c₁ be non trivial RealLinearSpace;
func ProjectiveSpace c₁ -> strict CollStr equals :: ANPROJ_1:def 10
CollStr(# (ProjectivePoints a₁),(ProjectiveCollinearity a₁) #);
correctness ;

end;

:: deftheorem Def10 defines ProjectiveSpace ANPROJ_1:def 10 :

registration

let c₁ be non trivial RealLinearSpace;
cluster ProjectiveSpace a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th36: :: ANPROJ_1:36

canceled;

theorem Th37: :: ANPROJ_1:37

canceled;

theorem Th38: :: ANPROJ_1:38

canceled;

theorem Th39: :: ANPROJ_1:39

for b₁ being non trivial RealLinearSpace holds
( the carrier of (ProjectiveSpace b₁) = ProjectivePoints b₁ & the Collinearity of (ProjectiveSpace b₁) = ProjectiveCollinearity b₁ ) ;

theorem Th40: :: ANPROJ_1:40

for b₁, b₂, b₃ being set
for b₄ being non trivial RealLinearSpace st [b₁,b₂,b₃] in the Collinearity of (ProjectiveSpace b₄) holds
ex b₅, b₆, b₇ being Element of b₄ st
( b₁ = Dir b₅ & b₂ = Dir b₆ & b₃ = Dir b₇ & b₅ is_Prop_Vect & b₆ is_Prop_Vect & b₇ is_Prop_Vect & b₅,b₆,b₇ are_LinDep ) by Def9;

theorem Th41: :: ANPROJ_1:41

for b₁ being non trivial RealLinearSpace
for b₂, b₃, b₄ being Element of b₁ st b₂ is_Prop_Vect & b₃ is_Prop_Vect & b₄ is_Prop_Vect holds
( [(Dir b₂),(Dir b₃),(Dir b₄)] in the Collinearity of (ProjectiveSpace b₁) iff b₂,b₃,b₄ are_LinDep )

proof end;

theorem Th42: :: ANPROJ_1:42

for b₁ being set
for b₂ being non trivial RealLinearSpace holds
( b₁ is Element of (ProjectiveSpace b₂) iff ex b₃ being Element of b₂ st
( b₃ is_Prop_Vect & b₁ = Dir b₃ ) )

proof end;