:: ANPROJ_2 semantic presentation

theorem Th1: :: ANPROJ_2:1

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

proof end;

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

proof end;

theorem Th2: :: ANPROJ_2:2

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

proof end;

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

proof end;

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

theorem Th3: :: ANPROJ_2:3

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

proof end;

Lemma7: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for 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₅)

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th4: :: ANPROJ_2:4

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

proof end;

theorem Th5: :: ANPROJ_2:5

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

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄ be Element of c₁;
pred c₂,c₃,c₄ are_Prop_Vect means :Def1: :: ANPROJ_2:def 1
( a₂ is_Prop_Vect & a₃ is_Prop_Vect & a₄ is_Prop_Vect );

end;

:: deftheorem Def1 defines are_Prop_Vect ANPROJ_2:def 1 :

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄, c₅, c₆, c₇ be Element of c₁;
pred c₂,c₃,c₄,c₅,c₆,c₇ lie_on_a_triangle means :Def2: :: ANPROJ_2:def 2
( a₂,a₃,a₇ are_LinDep & a₂,a₄,a₆ are_LinDep & a₃,a₄,a₅ are_LinDep );

end;

:: deftheorem Def2 defines lie_on_a_triangle ANPROJ_2:def 2 :

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄, c₅, c₆, c₇, c₈ be Element of c₁;
pred c₂,c₃,c₄,c₅,c₆,c₇,c₈ are_perspective means :Def3: :: ANPROJ_2:def 3
( a₂,a₃,a₆ are_LinDep & a₂,a₄,a₇ are_LinDep & a₂,a₅,a₈ are_LinDep );

end;

:: deftheorem Def3 defines are_perspective ANPROJ_2:def 3 :

Lemma16: for b₁ being RealLinearSpace
for b₂ being Element of b₁
for b₃ being Real holds - (b₃ * b₂) = (- b₃) * b₂

proof end;

theorem Th6: :: ANPROJ_2:6

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

proof end;

theorem Th7: :: ANPROJ_2:7

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

proof end;

Lemma19: for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁
for b₄ being Real st b₄ * b₂ = b₃ & b₄ <> 0 holds
are_Prop b₂,b₃

proof end;

Lemma20: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁
for b₇, b₈ being Real st b₂ = b₃ + (b₇ * b₄) & b₅ = b₃ + (b₈ * b₆) & are_Prop b₂,b₅ & b₇ <> 0 holds
b₃,b₄,b₆ are_LinDep

proof end;

Lemma21: for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁
for b₄ being Real st b₄ * b₂ = b₃ & b₄ <> 0 & b₂ is_Prop_Vect holds
b₃ is_Prop_Vect

proof end;

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

proof end;

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

proof end;

Lemma24: for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁ holds (0 * b₂) + (0 * b₃) = 0. b₁

proof end;

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

proof end;

theorem Th8: :: ANPROJ_2:8

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being Element of b₁ st b₂ is_Prop_Vect & b₃,b₄,b₅ are_Prop_Vect & b₆,b₇,b₈ are_Prop_Vect & b₉,b₁₀,b₁₁ are_Prop_Vect & b₂,b₃,b₄,b₅,b₆,b₇,b₈ are_perspective & not are_Prop b₂,b₆ & not are_Prop b₂,b₇ & not are_Prop b₂,b₈ & not are_Prop b₃,b₆ & not are_Prop b₄,b₇ & not are_Prop b₅,b₈ & not b₂,b₃,b₄ are_LinDep & not b₂,b₃,b₅ are_LinDep & not b₂,b₄,b₅ are_LinDep & b₃,b₄,b₅,b₉,b₁₀,b₁₁ lie_on_a_triangle & b₆,b₇,b₈,b₉,b₁₀,b₁₁ lie_on_a_triangle holds
b₉,b₁₀,b₁₁ are_LinDep

proof end;

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄, c₅, c₆, c₇, c₈ be Element of c₁;
pred c₂,c₃,c₄,c₅,c₆,c₇,c₈ lie_on_an_angle means :Def4: :: ANPROJ_2:def 4
( not a₂,a₃,a₆ are_LinDep & a₂,a₃,a₄ are_LinDep & a₂,a₃,a₅ are_LinDep & a₂,a₆,a₇ are_LinDep & a₂,a₆,a₈ are_LinDep );

end;

:: deftheorem Def4 defines lie_on_an_angle ANPROJ_2:def 4 :

definition

let c₁ be RealLinearSpace;
let c₂, c₃, c₄, c₅, c₆, c₇, c₈ be Element of c₁;
pred c₂,c₃,c₄,c₅,c₆,c₇,c₈ are_half_mutually_not_Prop means :Def5: :: ANPROJ_2:def 5
( not are_Prop a₂,a₄ & not are_Prop a₂,a₅ & not are_Prop a₂,a₇ & not are_Prop a₂,a₈ & not are_Prop a₃,a₄ & not are_Prop a₃,a₅ & not are_Prop a₆,a₇ & not are_Prop a₆,a₈ & not are_Prop a₄,a₅ & not are_Prop a₇,a₈ );

end;

:: deftheorem Def5 defines are_half_mutually_not_Prop ANPROJ_2:def 5 :

Lemma29: for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁
for b₄ being Real st b₄ * b₂ = b₃ & b₄ <> 0 holds
are_Prop b₂,b₃

proof end;

Lemma30: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Element of b₁
for b₅ being Real st not are_Prop b₂,b₃ & b₄ = b₅ * b₃ & b₅ <> 0 holds
not are_Prop b₂,b₄

proof end;

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

proof end;

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

proof end;

Lemma33: for b₁ being RealLinearSpace
for b₂, b₃ being Element of b₁
for b₄ being Real st b₄ * b₂ = b₃ & b₄ <> 0 & b₂ is_Prop_Vect holds
b₃ is_Prop_Vect

proof end;

Lemma34: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆, b₇ being Real st not are_Prop b₂,b₃ & b₄ = b₆ * b₃ & b₆ <> 0 & b₅ = b₇ * b₂ & b₇ <> 0 holds
not are_Prop b₅,b₄

proof end;

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

proof end;

Lemma36: for b₁, b₂, b₃ being Real st b₁ <> b₂ & b₃ <> 0 holds
(b₂ * b₃) - (b₁ * b₃) <> 0

proof end;

Lemma37: for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Real st b₅ + b₇ = b₆ + b₈ & b₅ * b₁ = b₆ * b₂ & b₇ * b₃ = b₈ * b₄ & b₁ <> b₂ & b₄ <> 0 holds
b₅ = (((b₂ * b₃) - (b₂ * b₄)) * (((b₂ * b₄) - (b₁ * b₄)) " )) * b₇

proof end;

Lemma38: for b₁, b₂, b₃, b₄ being Real st b₁ <> 0 & b₂ <> b₃ & b₄ <> 0 holds
b₄ * (((b₃ * b₁) - (b₂ * b₁)) " ) <> 0

proof end;

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

proof end;

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

Lemma41: for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁
for b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being Real st 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₁₃ = (b₁₀ * b₁₁) - (b₈ * b₉) & (b₁₂ * b₈) + (b₁₃ * b₁₀) = (b₁₀ * b₈) * (b₁₁ - b₉) & (b₁₂ * b₉) + (b₁₃ * b₁₁) = (b₁₁ * b₉) * (b₁₀ - b₈) holds
((1 * b₂) + (b₁₂ * b₆)) + (b₁₃ * b₇) = 0. b₁

proof end;

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

proof end;

theorem Th9: :: ANPROJ_2:9

for b₁ being RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁ being Element of b₁ st b₂ is_Prop_Vect & b₃,b₄,b₅ are_Prop_Vect & b₆,b₇,b₈ are_Prop_Vect & b₉,b₁₀,b₁₁ are_Prop_Vect & b₂,b₃,b₄,b₅,b₆,b₇,b₈ lie_on_an_angle & b₂,b₃,b₄,b₅,b₆,b₇,b₈ are_half_mutually_not_Prop & 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 holds
b₉,b₁₀,b₁₁ are_LinDep

proof end;

theorem Th10: :: ANPROJ_2:10

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ ex b₅, b₆, b₇ being Element of Funcs b₁,REAL st
( ( for b₈ being set st b₈ in b₁ holds
( ( b₈ = b₂ implies b₅ . b₈ = 1 ) & ( b₈ <> b₂ implies b₅ . b₈ = 0 ) ) ) & ( for b₈ being set st b₈ in b₁ holds
( ( b₈ = b₃ implies b₆ . b₈ = 1 ) & ( b₈ <> b₃ implies b₆ . b₈ = 0 ) ) ) & ( for b₈ being set st b₈ in b₁ holds
( ( b₈ = b₄ implies b₇ . b₈ = 1 ) & ( b₈ <> b₄ implies b₇ . b₈ = 0 ) ) ) )

proof end;

theorem Th11: :: ANPROJ_2:11

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,REAL
for b₅, b₆, b₇ being Element of b₁ st b₅ in b₁ & b₆ in b₁ & b₇ in b₁ & b₅ <> b₆ & b₅ <> b₇ & b₆ <> b₇ & ( for b₈ being set st b₈ in b₁ holds
( ( b₈ = b₅ implies b₂ . b₈ = 1 ) & ( b₈ <> b₅ implies b₂ . b₈ = 0 ) ) ) & ( for b₈ being set st b₈ in b₁ holds
( ( b₈ = b₆ implies b₃ . b₈ = 1 ) & ( b₈ <> b₆ implies b₃ . b₈ = 0 ) ) ) & ( for b₈ being set st b₈ in b₁ holds
( ( b₈ = b₇ implies b₄ . b₈ = 1 ) & ( b₈ <> b₇ implies b₄ . b₈ = 0 ) ) ) holds
for b₈, b₉, b₁₀ being Real st (RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₈,b₂]),((RealFuncExtMult b₁) . [b₉,b₃])),((RealFuncExtMult b₁) . [b₁₀,b₄]) = RealFuncZero b₁ holds
( b₈ = 0 & b₉ = 0 & b₁₀ = 0 )

proof end;

theorem Th12: :: ANPROJ_2:12

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ st b₂ in b₁ & b₃ in b₁ & b₄ in b₁ & b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ holds
ex b₅, b₆, b₇ being Element of Funcs b₁,REAL st
for b₈, b₉, b₁₀ being Real st (RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₈,b₅]),((RealFuncExtMult b₁) . [b₉,b₆])),((RealFuncExtMult b₁) . [b₁₀,b₇]) = RealFuncZero b₁ holds
( b₈ = 0 & b₉ = 0 & b₁₀ = 0 )

proof end;

theorem Th13: :: ANPROJ_2:13

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,REAL
for b₅, b₆, b₇ being Element of b₁ st b₁ = {b₅,b₆,b₇} & b₅ <> b₆ & b₅ <> b₇ & b₆ <> b₇ & ( for b₈ being set st b₈ in b₁ holds
( ( b₈ = b₅ implies b₂ . b₈ = 1 ) & ( b₈ <> b₅ implies b₂ . b₈ = 0 ) ) ) & ( for b₈ being set st b₈ in b₁ holds
( ( b₈ = b₆ implies b₃ . b₈ = 1 ) & ( b₈ <> b₆ implies b₃ . b₈ = 0 ) ) ) & ( for b₈ being set st b₈ in b₁ holds
( ( b₈ = b₇ implies b₄ . b₈ = 1 ) & ( b₈ <> b₇ implies b₄ . b₈ = 0 ) ) ) holds
for b₈ being Element of Funcs b₁,REAL ex b₉, b₁₀, b₁₁ being Real st b₈ = (RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₉,b₂]),((RealFuncExtMult b₁) . [b₁₀,b₃])),((RealFuncExtMult b₁) . [b₁₁,b₄])

proof end;

theorem Th14: :: ANPROJ_2:14

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ st b₁ = {b₂,b₃,b₄} & b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ holds
ex b₅, b₆, b₇ being Element of Funcs b₁,REAL st
for b₈ being Element of Funcs b₁,REAL ex b₉, b₁₀, b₁₁ being Real st b₈ = (RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₉,b₅]),((RealFuncExtMult b₁) . [b₁₀,b₆])),((RealFuncExtMult b₁) . [b₁₁,b₇])

proof end;

theorem Th15: :: ANPROJ_2:15

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ st b₁ = {b₂,b₃,b₄} & b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ holds
ex b₅, b₆, b₇ being Element of Funcs b₁,REAL st
( ( for b₈, b₉, b₁₀ being Real st (RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₈,b₅]),((RealFuncExtMult b₁) . [b₉,b₆])),((RealFuncExtMult b₁) . [b₁₀,b₇]) = RealFuncZero b₁ holds
( b₈ = 0 & b₉ = 0 & b₁₀ = 0 ) ) & ( for b₈ being Element of Funcs b₁,REAL ex b₉, b₁₀, b₁₁ being Real st b₈ = (RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₉,b₅]),((RealFuncExtMult b₁) . [b₁₀,b₆])),((RealFuncExtMult b₁) . [b₁₁,b₇]) ) )

proof end;

Lemma48: ex b₁ being non empty set ex b₂, b₃, b₄ being Element of b₁ st
( b₁ = {b₂,b₃,b₄} & b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ )

proof end;

theorem Th16: :: ANPROJ_2:16

ex b₁ being non trivial RealLinearSpaceex b₂, b₃, b₄ being Element of b₁ st
( ( for b₅, b₆, b₇ being Real st ((b₅ * b₂) + (b₆ * b₃)) + (b₇ * b₄) = 0. b₁ holds
( b₅ = 0 & b₆ = 0 & b₇ = 0 ) ) & ( for b₅ being Element of b₁ ex b₆, b₇, b₈ being Real st b₅ = ((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄) ) )

proof end;

theorem Th17: :: ANPROJ_2:17

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of b₁ ex b₆, b₇, b₈, b₉ being Element of Funcs b₁,REAL st
( ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₂ implies b₆ . b₁₀ = 1 ) & ( b₁₀ <> b₂ implies b₆ . b₁₀ = 0 ) ) ) & ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₃ implies b₇ . b₁₀ = 1 ) & ( b₁₀ <> b₃ implies b₇ . b₁₀ = 0 ) ) ) & ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₄ implies b₈ . b₁₀ = 1 ) & ( b₁₀ <> b₄ implies b₈ . b₁₀ = 0 ) ) ) & ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₅ implies b₉ . b₁₀ = 1 ) & ( b₁₀ <> b₅ implies b₉ . b₁₀ = 0 ) ) ) )

proof end;

theorem Th18: :: ANPROJ_2:18

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of Funcs b₁,REAL
for b₆, b₇, b₈, b₉ being Element of b₁ st b₆ in b₁ & b₇ in b₁ & b₈ in b₁ & b₉ in b₁ & b₆ <> b₇ & b₆ <> b₈ & b₆ <> b₉ & b₇ <> b₈ & b₇ <> b₉ & b₈ <> b₉ & ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₆ implies b₂ . b₁₀ = 1 ) & ( b₁₀ <> b₆ implies b₂ . b₁₀ = 0 ) ) ) & ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₇ implies b₃ . b₁₀ = 1 ) & ( b₁₀ <> b₇ implies b₃ . b₁₀ = 0 ) ) ) & ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₈ implies b₄ . b₁₀ = 1 ) & ( b₁₀ <> b₈ implies b₄ . b₁₀ = 0 ) ) ) & ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₉ implies b₅ . b₁₀ = 1 ) & ( b₁₀ <> b₉ implies b₅ . b₁₀ = 0 ) ) ) holds
for b₁₀, b₁₁, b₁₂, b₁₃ being Real st (RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₁₀,b₂]),((RealFuncExtMult b₁) . [b₁₁,b₃])),((RealFuncExtMult b₁) . [b₁₂,b₄])),((RealFuncExtMult b₁) . [b₁₃,b₅]) = RealFuncZero b₁ holds
( b₁₀ = 0 & b₁₁ = 0 & b₁₂ = 0 & b₁₃ = 0 )

proof end;

theorem Th19: :: ANPROJ_2:19

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ in b₁ & b₃ in b₁ & b₄ in b₁ & b₅ in b₁ & b₂ <> b₃ & b₂ <> b₄ & b₂ <> b₅ & b₃ <> b₄ & b₃ <> b₅ & b₄ <> b₅ holds
ex b₆, b₇, b₈, b₉ being Element of Funcs b₁,REAL st
for b₁₀, b₁₁, b₁₂, b₁₃ being Real st (RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₁₀,b₆]),((RealFuncExtMult b₁) . [b₁₁,b₇])),((RealFuncExtMult b₁) . [b₁₂,b₈])),((RealFuncExtMult b₁) . [b₁₃,b₉]) = RealFuncZero b₁ holds
( b₁₀ = 0 & b₁₁ = 0 & b₁₂ = 0 & b₁₃ = 0 )

proof end;

theorem Th20: :: ANPROJ_2:20

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of Funcs b₁,REAL
for b₆, b₇, b₈, b₉ being Element of b₁ st b₁ = {b₆,b₇,b₈,b₉} & b₆ <> b₇ & b₆ <> b₈ & b₆ <> b₉ & b₇ <> b₈ & b₇ <> b₉ & b₈ <> b₉ & ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₆ implies b₂ . b₁₀ = 1 ) & ( b₁₀ <> b₆ implies b₂ . b₁₀ = 0 ) ) ) & ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₇ implies b₃ . b₁₀ = 1 ) & ( b₁₀ <> b₇ implies b₃ . b₁₀ = 0 ) ) ) & ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₈ implies b₄ . b₁₀ = 1 ) & ( b₁₀ <> b₈ implies b₄ . b₁₀ = 0 ) ) ) & ( for b₁₀ being set st b₁₀ in b₁ holds
( ( b₁₀ = b₉ implies b₅ . b₁₀ = 1 ) & ( b₁₀ <> b₉ implies b₅ . b₁₀ = 0 ) ) ) holds
for b₁₀ being Element of Funcs b₁,REAL ex b₁₁, b₁₂, b₁₃, b₁₄ being Real st b₁₀ = (RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₁₁,b₂]),((RealFuncExtMult b₁) . [b₁₂,b₃])),((RealFuncExtMult b₁) . [b₁₃,b₄])),((RealFuncExtMult b₁) . [b₁₄,b₅])

proof end;

theorem Th21: :: ANPROJ_2:21

proof end;

theorem Th22: :: ANPROJ_2:22

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Element of b₁ st b₁ = {b₂,b₃,b₄,b₅} & b₂ <> b₃ & b₂ <> b₄ & b₂ <> b₅ & b₃ <> b₄ & b₃ <> b₅ & b₄ <> b₅ holds
ex b₆, b₇, b₈, b₉ being Element of Funcs b₁,REAL st
( ( for b₁₀, b₁₁, b₁₂, b₁₃ being Real st (RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₁₀,b₆]),((RealFuncExtMult b₁) . [b₁₁,b₇])),((RealFuncExtMult b₁) . [b₁₂,b₈])),((RealFuncExtMult b₁) . [b₁₃,b₉]) = RealFuncZero b₁ holds
( b₁₀ = 0 & b₁₁ = 0 & b₁₂ = 0 & b₁₃ = 0 ) ) & ( for b₁₀ being Element of Funcs b₁,REAL ex b₁₁, b₁₂, b₁₃, b₁₄ being Real st b₁₀ = (RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncAdd b₁) . ((RealFuncExtMult b₁) . [b₁₁,b₆]),((RealFuncExtMult b₁) . [b₁₂,b₇])),((RealFuncExtMult b₁) . [b₁₃,b₈])),((RealFuncExtMult b₁) . [b₁₄,b₉]) ) )

proof end;

Lemma54: ex b₁ being non empty set ex b₂, b₃, b₄, b₅ being Element of b₁ st
( b₁ = {b₂,b₃,b₄,b₅} & b₂ <> b₃ & b₂ <> b₄ & b₂ <> b₅ & b₃ <> b₄ & b₃ <> b₅ & b₄ <> b₅ )

proof end;

theorem Th23: :: ANPROJ_2:23

ex b₁ being non trivial RealLinearSpaceex b₂, b₃, b₄, b₅ being Element of b₁ st
( ( for b₆, b₇, b₈, b₉ being Real st (((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄)) + (b₉ * b₅) = 0. b₁ holds
( b₆ = 0 & b₇ = 0 & b₈ = 0 & b₉ = 0 ) ) & ( for b₆ being Element of b₁ ex b₇, b₈, b₉, b₁₀ being Real st b₆ = (((b₇ * b₂) + (b₈ * b₃)) + (b₉ * b₄)) + (b₁₀ * b₅) ) )

proof end;

definition

let c₁ be RealLinearSpace;
attr a₁ is up-3-dimensional means :Def6: :: ANPROJ_2:def 6
ex b₁, b₂, b₃ being Element of a₁ st
for b₄, b₅, b₆ being Real st ((b₄ * b₁) + (b₅ * b₂)) + (b₆ * b₃) = 0. a₁ holds
( b₄ = 0 & b₅ = 0 & b₆ = 0 );

end;

:: deftheorem Def6 defines up-3-dimensional ANPROJ_2:def 6 :

registration

cluster up-3-dimensional RLSStruct ;
existence

proof end;

end;

registration

cluster up-3-dimensional -> non trivial RLSStruct ;
coherence

proof end;

end;

definition

let c₁ be non empty CollStr ;
redefine attr a₁ is reflexive means :Def7: :: ANPROJ_2:def 7
for b₁, b₂, b₃ being Element of a₁ holds
( b₁,b₂,b₁ is_collinear & b₁,b₁,b₂ is_collinear & b₁,b₂,b₂ is_collinear );
compatibility

proof end;

redefine attr a₁ is transitive means :Def8: :: ANPROJ_2:def 8
for b₁, b₂, b₃, b₄, b₅ being Element of a₁ st b₁ <> b₂ & b₁,b₂,b₃ is_collinear & b₁,b₂,b₄ is_collinear & b₁,b₂,b₅ is_collinear holds
b₃,b₄,b₅ is_collinear ;
compatibility

proof end;

end;

:: deftheorem Def7 defines reflexive ANPROJ_2:def 7 :

:: deftheorem Def8 defines transitive ANPROJ_2:def 8 :

definition

let c₁ be non empty CollStr ;
attr a₁ is Vebleian means :Def9: :: ANPROJ_2:def 9
for b₁, b₂, b₃, b₄, b₅ being Element of a₁ st b₁,b₂,b₄ is_collinear & b₂,b₃,b₅ is_collinear holds
ex b₆ being Element of a₁ st
( b₁,b₃,b₆ is_collinear & b₄,b₅,b₆ is_collinear );
attr a₁ is at_least_3rank means :Def10: :: ANPROJ_2:def 10
for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st
( b₁ <> b₃ & b₂ <> b₃ & b₁,b₂,b₃ is_collinear );

end;

:: deftheorem Def9 defines Vebleian ANPROJ_2:def 9 :

:: deftheorem Def10 defines at_least_3rank ANPROJ_2:def 10 :

theorem Th24: :: ANPROJ_2:24

for b₁ being non trivial RealLinearSpace
for b₂, b₃, b₄ being Element of (ProjectiveSpace b₁) holds
( b₂,b₃,b₄ is_collinear iff 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 ) )

proof end;

Lemma62: for b₁ being non trivial RealLinearSpace holds ProjectiveSpace b₁ is reflexive

proof end;

Lemma63: for b₁ being non trivial RealLinearSpace holds ProjectiveSpace b₁ is transitive

proof end;

registration

let c₁ be non trivial RealLinearSpace;
cluster ProjectiveSpace a₁ -> reflexive transitive ;
coherence by Lemma62, Lemma63;

end;

theorem Th25: :: ANPROJ_2:25

for b₁ being non trivial RealLinearSpace
for b₂, b₃, b₄ being Element of (ProjectiveSpace b₁) st b₂,b₃,b₄ is_collinear holds
( b₂,b₄,b₃ is_collinear & b₃,b₂,b₄ is_collinear & b₄,b₃,b₂ is_collinear & b₄,b₂,b₃ is_collinear & b₃,b₄,b₂ is_collinear )

proof end;

Lemma65: for b₁ being non trivial RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being Element of (ProjectiveSpace b₁) st b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₃,b₄,b₆ is_collinear holds
ex b₇ being Element of (ProjectiveSpace b₁) st
( b₂,b₄,b₇ is_collinear & b₅,b₆,b₇ is_collinear )

proof end;

Lemma66: for b₁ being non trivial RealLinearSpace
for b₂, b₃, b₄, b₅, b₆ being Element of (ProjectiveSpace b₁) st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₃,b₄,b₆ is_collinear holds
ex b₇ being Element of (ProjectiveSpace b₁) st
( b₂,b₄,b₇ is_collinear & b₅,b₆,b₇ is_collinear )

proof end;

Lemma67: for b₁ being non trivial RealLinearSpace holds ProjectiveSpace b₁ is Vebleian

proof end;

registration

let c₁ be non trivial RealLinearSpace;
cluster ProjectiveSpace a₁ -> reflexive transitive Vebleian ;
coherence by Lemma67;

end;

Lemma68: for b₁ being non trivial RealLinearSpace st b₁ is up-3-dimensional holds
ProjectiveSpace b₁ is proper

proof end;

registration

let c₁ be up-3-dimensional RealLinearSpace;
cluster ProjectiveSpace a₁ -> reflexive transitive proper Vebleian ;
coherence by Lemma68;

end;

theorem Th26: :: ANPROJ_2:26

for b₁ being non trivial RealLinearSpace st ex b₂, b₃ being Element of b₁ st
for b₄, b₅ being Real st (b₄ * b₂) + (b₅ * b₃) = 0. b₁ holds
( b₄ = 0 & b₅ = 0 ) holds
ProjectiveSpace b₁ is at_least_3rank

proof end;

Lemma70: for b₁ being non trivial RealLinearSpace st b₁ is up-3-dimensional holds
ProjectiveSpace b₁ is at_least_3rank

proof end;

registration

let c₁ be up-3-dimensional RealLinearSpace;
cluster ProjectiveSpace a₁ -> reflexive transitive proper Vebleian at_least_3rank ;
coherence by Lemma70;

end;

registration

cluster non empty reflexive transitive proper Vebleian at_least_3rank CollStr ;
existence

proof end;

end;

definition

mode CollProjectiveSpace is non empty reflexive transitive proper Vebleian at_least_3rank CollStr ;

end;

Lemma71: for b₁ being up-3-dimensional RealLinearSpace holds ProjectiveSpace b₁ is CollProjectiveSpace
;

definition

let c₁ be CollProjectiveSpace;
attr a₁ is Fanoian means :Def11: :: ANPROJ_2:def 11
for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being Element of a₁ st b₁,b₂,b₃ is_collinear & b₄,b₅,b₃ is_collinear & b₁,b₄,b₆ is_collinear & b₂,b₅,b₆ is_collinear & b₁,b₅,b₇ is_collinear & b₂,b₄,b₇ is_collinear & b₆,b₃,b₇ is_collinear & not b₁,b₂,b₅ is_collinear & not b₁,b₂,b₄ is_collinear & not b₁,b₄,b₅ is_collinear holds
b₂,b₄,b₅ is_collinear ;
attr a₁ is Desarguesian means :: ANPROJ_2:def 12
for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of a₁ st b₁ <> b₅ & b₂ <> b₅ & b₁ <> b₆ & b₃ <> b₆ & b₁ <> b₇ & b₄ <> b₇ & not b₁,b₂,b₃ is_collinear & not b₁,b₂,b₄ is_collinear & not b₁,b₃,b₄ is_collinear & b₂,b₃,b₁₀ is_collinear & b₅,b₆,b₁₀ is_collinear & b₃,b₄,b₈ is_collinear & b₆,b₇,b₈ is_collinear & b₂,b₄,b₉ is_collinear & b₅,b₇,b₉ is_collinear & b₁,b₂,b₅ is_collinear & b₁,b₃,b₆ is_collinear & b₁,b₄,b₇ is_collinear holds
b₈,b₉,b₁₀ is_collinear ;
attr a₁ is Pappian means :: ANPROJ_2:def 13
for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of a₁ st b₁ <> b₃ & b₁ <> b₄ & b₃ <> b₄ & b₂ <> b₃ & b₂ <> b₄ & b₁ <> b₆ & b₁ <> b₇ & b₆ <> b₇ & b₅ <> b₆ & b₅ <> b₇ & not b₁,b₂,b₅ is_collinear & b₁,b₂,b₃ is_collinear & b₁,b₂,b₄ is_collinear & b₁,b₅,b₆ is_collinear & b₁,b₅,b₇ is_collinear & b₂,b₆,b₁₀ is_collinear & b₅,b₃,b₁₀ is_collinear & b₂,b₇,b₉ is_collinear & b₄,b₅,b₉ is_collinear & b₃,b₇,b₈ is_collinear & b₄,b₆,b₈ is_collinear holds
b₈,b₉,b₁₀ is_collinear ;

end;

:: deftheorem Def11 defines Fanoian ANPROJ_2:def 11 :

:: deftheorem Def12 defines Desarguesian ANPROJ_2:def 12 :

:: deftheorem Def13 defines Pappian ANPROJ_2:def 13 :

definition

let c₁ be CollProjectiveSpace;
attr a₁ is 2-dimensional means :Def14: :: ANPROJ_2:def 14
for b₁, b₂, b₃, b₄ being Element of a₁ ex b₅ being Element of a₁ st
( b₁,b₂,b₅ is_collinear & b₃,b₄,b₅ is_collinear );

end;

:: deftheorem Def14 defines 2-dimensional ANPROJ_2:def 14 :

notation

let c₁ be CollProjectiveSpace;
antonym up-3-dimensional c₁ for 2-dimensional c₁;

end;

definition

let c₁ be CollProjectiveSpace;
attr a₁ is at_most-3-dimensional means :Def15: :: ANPROJ_2:def 15
for b₁, b₂, b₃, b₄, b₅ being Element of a₁ ex b₆, b₇ being Element of a₁ st
( b₁,b₃,b₆ is_collinear & b₂,b₄,b₇ is_collinear & b₅,b₆,b₇ is_collinear );

end;

:: deftheorem Def15 defines at_most-3-dimensional ANPROJ_2:def 15 :

theorem Th27: :: ANPROJ_2:27

canceled;

theorem Th28: :: ANPROJ_2:28

for b₁ being non trivial RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Element of (ProjectiveSpace b₁) st b₂,b₃,b₄ is_collinear & b₅,b₆,b₄ is_collinear & b₂,b₅,b₇ is_collinear & b₃,b₆,b₇ is_collinear & b₂,b₆,b₈ is_collinear & b₃,b₅,b₈ is_collinear & b₇,b₄,b₈ is_collinear & not b₂,b₃,b₆ is_collinear & not b₂,b₃,b₅ is_collinear & not b₂,b₅,b₆ is_collinear holds
b₃,b₅,b₆ is_collinear

proof end;

Lemma76: for b₁ being up-3-dimensional RealLinearSpace holds ProjectiveSpace b₁ is Fanoian

proof end;

Lemma77: for b₁ being up-3-dimensional RealLinearSpace holds ProjectiveSpace b₁ is Desarguesian

proof end;

Lemma78: for b₁ being up-3-dimensional RealLinearSpace holds ProjectiveSpace b₁ is Pappian

proof end;

registration

let c₁ be up-3-dimensional RealLinearSpace;
cluster ProjectiveSpace a₁ -> reflexive transitive proper Vebleian at_least_3rank Fanoian Desarguesian Pappian ;
coherence by Lemma76, Lemma77, Lemma78;

end;

theorem Th29: :: ANPROJ_2:29

for b₁ being non trivial RealLinearSpace st ex b₂, b₃, b₄ being Element of b₁ st
( ( for b₅, b₆, b₇ being Real st ((b₅ * b₂) + (b₆ * b₃)) + (b₇ * b₄) = 0. b₁ holds
( b₅ = 0 & b₆ = 0 & b₇ = 0 ) ) & ( for b₅ being Element of b₁ ex b₆, b₇, b₈ being Real st b₅ = ((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄) ) ) holds
ex b₂, b₃ being Element of (ProjectiveSpace b₁) st
( b₂ <> b₃ & ( for b₄, b₅ being Element of (ProjectiveSpace b₁) ex b₆ being Element of (ProjectiveSpace b₁) st
( b₂,b₃,b₆ is_collinear & b₄,b₅,b₆ is_collinear ) ) )

proof end;

theorem Th30: :: ANPROJ_2:30

for b₁ being non trivial RealLinearSpace st ex b₂, b₃ being Element of (ProjectiveSpace b₁) st
( b₂ <> b₃ & ( for b₄, b₅ being Element of (ProjectiveSpace b₁) ex b₆ being Element of (ProjectiveSpace b₁) st
( b₂,b₃,b₆ is_collinear & b₄,b₅,b₆ is_collinear ) ) ) holds
for b₂, b₃, b₄, b₅ being Element of (ProjectiveSpace b₁) ex b₆ being Element of (ProjectiveSpace b₁) st
( b₂,b₃,b₆ is_collinear & b₄,b₅,b₆ is_collinear )

proof end;

theorem Th31: :: ANPROJ_2:31

for b₁ being non trivial RealLinearSpace st ex b₂, b₃, b₄ being Element of b₁ st
( ( for b₅, b₆, b₇ being Real st ((b₅ * b₂) + (b₆ * b₃)) + (b₇ * b₄) = 0. b₁ holds
( b₅ = 0 & b₆ = 0 & b₇ = 0 ) ) & ( for b₅ being Element of b₁ ex b₆, b₇, b₈ being Real st b₅ = ((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄) ) ) holds
ex b₂ being CollProjectiveSpace st
( b₂ = ProjectiveSpace b₁ & b₂ is 2-dimensional )

proof end;

Lemma82: for b₁ being non trivial RealLinearSpace st ex b₂, b₃, b₄, b₅ being Element of b₁ st
for b₆, b₇, b₈, b₉ being Real st (((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄)) + (b₉ * b₅) = 0. b₁ holds
( b₆ = 0 & b₇ = 0 & b₈ = 0 & b₉ = 0 ) holds
b₁ is up-3-dimensional

proof end;

Lemma83: for b₁ being non trivial RealLinearSpace st ex b₂, b₃, b₄, b₅ being Element of b₁ st
for b₆, b₇, b₈, b₉ being Real st (((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄)) + (b₉ * b₅) = 0. b₁ holds
( b₆ = 0 & b₇ = 0 & b₈ = 0 & b₉ = 0 ) holds
( ProjectiveSpace b₁ is proper & ProjectiveSpace b₁ is at_least_3rank )

proof end;

theorem Th32: :: ANPROJ_2:32

for b₁ being non trivial RealLinearSpace st ex b₂, b₃, b₄, b₅ being Element of b₁ st
( ( for b₆ being Element of b₁ ex b₇, b₈, b₉, b₁₀ being Real st b₆ = (((b₇ * b₂) + (b₈ * b₃)) + (b₉ * b₄)) + (b₁₀ * b₅) ) & ( for b₆, b₇, b₈, b₉ being Real st (((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄)) + (b₉ * b₅) = 0. b₁ holds
( b₆ = 0 & b₇ = 0 & b₈ = 0 & b₉ = 0 ) ) ) holds
ex b₂, b₃, b₄ being Element of (ProjectiveSpace b₁) st
( not b₂,b₃,b₄ is_collinear & ( for b₅, b₆ being Element of (ProjectiveSpace b₁) ex b₇, b₈ being Element of (ProjectiveSpace b₁) st
( b₅,b₆,b₈ is_collinear & b₃,b₄,b₇ is_collinear & b₂,b₈,b₇ is_collinear ) ) )

proof end;

Lemma85: for b₁ being non trivial RealLinearSpace
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of (ProjectiveSpace b₁) st not b₇,b₄,b₃ is_collinear & b₄,b₃,b₂ is_collinear & b₇,b₅,b₄ is_collinear & b₇,b₆,b₃ is_collinear holds
ex b₈ being Element of (ProjectiveSpace b₁) st
( b₅,b₆,b₈ is_collinear & b₇,b₂,b₈ is_collinear )

proof end;

theorem Th33: :: ANPROJ_2:33

for b₁ being non trivial RealLinearSpace st ProjectiveSpace b₁ is proper & ProjectiveSpace b₁ is at_least_3rank & ex b₂, b₃, b₄ being Element of (ProjectiveSpace b₁) st
( not b₂,b₃,b₄ is_collinear & ( for b₅, b₆ being Element of (ProjectiveSpace b₁) ex b₇, b₈ being Element of (ProjectiveSpace b₁) st
( b₅,b₆,b₈ is_collinear & b₃,b₄,b₇ is_collinear & b₂,b₈,b₇ is_collinear ) ) ) holds
ex b₂ being CollProjectiveSpace st
( b₂ = ProjectiveSpace b₁ & b₂ is at_most-3-dimensional )

proof end;

theorem Th34: :: ANPROJ_2:34

for b₁ being non trivial RealLinearSpace st ex b₂, b₃, b₄, b₅ being Element of b₁ st
( ( for b₆ being Element of b₁ ex b₇, b₈, b₉, b₁₀ being Real st b₆ = (((b₇ * b₂) + (b₈ * b₃)) + (b₉ * b₄)) + (b₁₀ * b₅) ) & ( for b₆, b₇, b₈, b₉ being Real st (((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄)) + (b₉ * b₅) = 0. b₁ holds
( b₆ = 0 & b₇ = 0 & b₈ = 0 & b₉ = 0 ) ) ) holds
ex b₂ being CollProjectiveSpace st
( b₂ = ProjectiveSpace b₁ & b₂ is at_most-3-dimensional )

proof end;

theorem Th35: :: ANPROJ_2:35

for b₁ being non trivial RealLinearSpace st ex b₂, b₃, b₄, b₅ being Element of b₁ st
for b₆, b₇, b₈, b₉ being Real st (((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄)) + (b₉ * b₅) = 0. b₁ holds
( b₆ = 0 & b₇ = 0 & b₈ = 0 & b₉ = 0 ) holds
ex b₂ being CollProjectiveSpace st
( b₂ = ProjectiveSpace b₁ & not b₂ is 2-dimensional )

proof end;

theorem Th36: :: ANPROJ_2:36

for b₁ being non trivial RealLinearSpace st ex b₂, b₃, b₄, b₅ being Element of b₁ st
( ( for b₆ being Element of b₁ ex b₇, b₈, b₉, b₁₀ being Real st b₆ = (((b₇ * b₂) + (b₈ * b₃)) + (b₉ * b₄)) + (b₁₀ * b₅) ) & ( for b₆, b₇, b₈, b₉ being Real st (((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄)) + (b₉ * b₅) = 0. b₁ holds
( b₆ = 0 & b₇ = 0 & b₈ = 0 & b₉ = 0 ) ) ) holds
ex b₂ being CollProjectiveSpace st
( b₂ = ProjectiveSpace b₁ & not b₂ is 2-dimensional & b₂ is at_most-3-dimensional )

proof end;

registration

cluster strict Fanoian Desarguesian Pappian 2-dimensional CollStr ;
existence

proof end;

cluster strict Fanoian Desarguesian Pappian up-3-dimensional at_most-3-dimensional CollStr ;
existence

proof end;

end;

definition

mode CollProjectivePlane is 2-dimensional CollProjectiveSpace;

end;

theorem Th37: :: ANPROJ_2:37

for b₁ being non empty CollStr holds
( b₁ is 2-dimensional CollProjectiveSpace iff ( b₁ is proper at_least_3rank CollSp & ( for b₂, b₃, b₄, b₅ being Element of b₁ ex b₆ being Element of b₁ st
( b₂,b₃,b₆ is_collinear & b₄,b₅,b₆ is_collinear ) ) ) )

proof end;