:: ANALMETR semantic presentation
begin
Lm1: for V being RealLinearSpace
for v1, w, y, v2 being VECTOR of V
for b1, b2, c1, c2 being Real st v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) )
proof
let V be RealLinearSpace; ::_thesis: for v1, w, y, v2 being VECTOR of V
for b1, b2, c1, c2 being Real st v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) )
let v1, w, y, v2 be VECTOR of V; ::_thesis: for b1, b2, c1, c2 being Real st v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) )
let b1, b2, c1, c2 be Real; ::_thesis: ( v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) implies ( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) ) )
assume A1: ( v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) ) ; ::_thesis: ( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) )
hence v1 + v2 = (((b1 * w) + (b2 * y)) + (c1 * w)) + (c2 * y) by RLVECT_1:def_3
.= (((b1 * w) + (c1 * w)) + (b2 * y)) + (c2 * y) by RLVECT_1:def_3
.= (((b1 + c1) * w) + (b2 * y)) + (c2 * y) by RLVECT_1:def_6
.= ((b1 + c1) * w) + ((b2 * y) + (c2 * y)) by RLVECT_1:def_3
.= ((b1 + c1) * w) + ((b2 + c2) * y) by RLVECT_1:def_6 ;
::_thesis: v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y)
thus v1 - v2 = ((b1 * w) + (b2 * y)) + ((- (c1 * w)) + (- (c2 * y))) by A1, RLVECT_1:31
.= ((b1 * w) + (b2 * y)) + ((c1 * (- w)) + (- (c2 * y))) by RLVECT_1:25
.= ((b1 * w) + (b2 * y)) + ((c1 * (- w)) + (c2 * (- y))) by RLVECT_1:25
.= ((b1 * w) + (b2 * y)) + (((- c1) * w) + (c2 * (- y))) by RLVECT_1:24
.= ((b1 * w) + (b2 * y)) + (((- c1) * w) + ((- c2) * y)) by RLVECT_1:24
.= (((b1 * w) + (b2 * y)) + ((- c1) * w)) + ((- c2) * y) by RLVECT_1:def_3
.= (((b1 * w) + ((- c1) * w)) + (b2 * y)) + ((- c2) * y) by RLVECT_1:def_3
.= (((b1 + (- c1)) * w) + (b2 * y)) + ((- c2) * y) by RLVECT_1:def_6
.= ((b1 + (- c1)) * w) + ((b2 * y) + ((- c2) * y)) by RLVECT_1:def_3
.= ((b1 - c1) * w) + ((b2 + (- c2)) * y) by RLVECT_1:def_6
.= ((b1 - c1) * w) + ((b2 - c2) * y) ; ::_thesis: verum
end;
Lm2: for V being RealLinearSpace
for w, y being VECTOR of V holds (0 * w) + (0 * y) = 0. V
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V holds (0 * w) + (0 * y) = 0. V
let w, y be VECTOR of V; ::_thesis: (0 * w) + (0 * y) = 0. V
thus (0 * w) + (0 * y) = (0. V) + (0 * y) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ; ::_thesis: verum
end;
Lm3: for V being RealLinearSpace
for v, w, y being VECTOR of V
for b1, b2, a being Real st v = (b1 * w) + (b2 * y) holds
a * v = ((a * b1) * w) + ((a * b2) * y)
proof
let V be RealLinearSpace; ::_thesis: for v, w, y being VECTOR of V
for b1, b2, a being Real st v = (b1 * w) + (b2 * y) holds
a * v = ((a * b1) * w) + ((a * b2) * y)
let v, w, y be VECTOR of V; ::_thesis: for b1, b2, a being Real st v = (b1 * w) + (b2 * y) holds
a * v = ((a * b1) * w) + ((a * b2) * y)
let b1, b2, a be Real; ::_thesis: ( v = (b1 * w) + (b2 * y) implies a * v = ((a * b1) * w) + ((a * b2) * y) )
assume v = (b1 * w) + (b2 * y) ; ::_thesis: a * v = ((a * b1) * w) + ((a * b2) * y)
hence a * v = (a * (b1 * w)) + (a * (b2 * y)) by RLVECT_1:def_5
.= ((a * b1) * w) + (a * (b2 * y)) by RLVECT_1:def_7
.= ((a * b1) * w) + ((a * b2) * y) by RLVECT_1:def_7 ;
::_thesis: verum
end;
definition
let V be RealLinearSpace;
let w, y be VECTOR of V;
pred Gen w,y means :Def1: :: ANALMETR:def 1
( ( for u being VECTOR of V ex a1, a2 being Real st u = (a1 * w) + (a2 * y) ) & ( for a1, a2 being Real st (a1 * w) + (a2 * y) = 0. V holds
( a1 = 0 & a2 = 0 ) ) );
end;
:: deftheorem Def1 defines Gen ANALMETR:def_1_:_
for V being RealLinearSpace
for w, y being VECTOR of V holds
( Gen w,y iff ( ( for u being VECTOR of V ex a1, a2 being Real st u = (a1 * w) + (a2 * y) ) & ( for a1, a2 being Real st (a1 * w) + (a2 * y) = 0. V holds
( a1 = 0 & a2 = 0 ) ) ) );
definition
let V be RealLinearSpace;
let u, v, w, y be VECTOR of V;
predu,v are_Ort_wrt w,y means :Def2: :: ANALMETR:def 2
ex a1, a2, b1, b2 being Real st
( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) & (a1 * b1) + (a2 * b2) = 0 );
end;
:: deftheorem Def2 defines are_Ort_wrt ANALMETR:def_2_:_
for V being RealLinearSpace
for u, v, w, y being VECTOR of V holds
( u,v are_Ort_wrt w,y iff ex a1, a2, b1, b2 being Real st
( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) & (a1 * b1) + (a2 * b2) = 0 ) );
Lm4: for V being RealLinearSpace
for w, y being VECTOR of V
for a1, a2, b1, b2 being Real st Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V
for a1, a2, b1, b2 being Real st Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
let w, y be VECTOR of V; ::_thesis: for a1, a2, b1, b2 being Real st Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
let a1, a2, b1, b2 be Real; ::_thesis: ( Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) implies ( a1 = b1 & a2 = b2 ) )
assume that
A1: Gen w,y and
A2: (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) ; ::_thesis: ( a1 = b1 & a2 = b2 )
0. V = ((a1 * w) + (a2 * y)) - ((b1 * w) + (b2 * y)) by A2, RLVECT_1:15
.= ((a1 - b1) * w) + ((a2 - b2) * y) by Lm1 ;
then ( (- b1) + a1 = 0 & (- b2) + a2 = 0 ) by A1, Def1;
hence ( a1 = b1 & a2 = b2 ) ; ::_thesis: verum
end;
theorem Th1: :: ANALMETR:1
for V being RealLinearSpace
for u, v, w, y being VECTOR of V st Gen w,y holds
( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, y being VECTOR of V st Gen w,y holds
( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 )
let u, v, w, y be VECTOR of V; ::_thesis: ( Gen w,y implies ( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 ) )
assume A1: Gen w,y ; ::_thesis: ( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 )
hereby ::_thesis: ( ( for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 ) implies u,v are_Ort_wrt w,y )
assume u,v are_Ort_wrt w,y ; ::_thesis: for a19, a29, b19, b29 being Real st u = (a19 * w) + (a29 * y) & v = (b19 * w) + (b29 * y) holds
0 = (a19 * b19) + (a29 * b29)
then consider a1, a2, b1, b2 being Real such that
A2: u = (a1 * w) + (a2 * y) and
A3: v = (b1 * w) + (b2 * y) and
A4: (a1 * b1) + (a2 * b2) = 0 by Def2;
let a19, a29, b19, b29 be Real; ::_thesis: ( u = (a19 * w) + (a29 * y) & v = (b19 * w) + (b29 * y) implies 0 = (a19 * b19) + (a29 * b29) )
assume that
A5: u = (a19 * w) + (a29 * y) and
A6: v = (b19 * w) + (b29 * y) ; ::_thesis: 0 = (a19 * b19) + (a29 * b29)
A7: b1 = b19 by A1, A3, A6, Lm4;
( a1 = a19 & a2 = a29 ) by A1, A2, A5, Lm4;
hence 0 = (a19 * b19) + (a29 * b29) by A1, A3, A4, A6, A7, Lm4; ::_thesis: verum
end;
consider a1, a2 being Real such that
A8: u = (a1 * w) + (a2 * y) by A1, Def1;
consider b1, b2 being Real such that
A9: v = (b1 * w) + (b2 * y) by A1, Def1;
assume for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 ; ::_thesis: u,v are_Ort_wrt w,y
then (a1 * b1) + (a2 * b2) = 0 by A8, A9;
hence u,v are_Ort_wrt w,y by A8, A9, Def2; ::_thesis: verum
end;
Lm5: for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
( w <> 0. V & y <> 0. V )
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds
( w <> 0. V & y <> 0. V )
let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies ( w <> 0. V & y <> 0. V ) )
assume A1: Gen w,y ; ::_thesis: ( w <> 0. V & y <> 0. V )
thus w <> 0. V ::_thesis: y <> 0. V
proof
assume w = 0. V ; ::_thesis: contradiction
then 0. V = 1 * w by RLVECT_1:def_8
.= (1 * w) + (0. V) by RLVECT_1:4
.= (1 * w) + (0 * y) by RLVECT_1:10 ;
hence contradiction by A1, Def1; ::_thesis: verum
end;
thus y <> 0. V ::_thesis: verum
proof
assume y = 0. V ; ::_thesis: contradiction
then 0. V = 1 * y by RLVECT_1:def_8
.= (0. V) + (1 * y) by RLVECT_1:4
.= (0 * w) + (1 * y) by RLVECT_1:10 ;
hence contradiction by A1, Def1; ::_thesis: verum
end;
end;
theorem :: ANALMETR:2
for V being RealLinearSpace
for w, y being VECTOR of V holds w,y are_Ort_wrt w,y
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V holds w,y are_Ort_wrt w,y
let w, y be VECTOR of V; ::_thesis: w,y are_Ort_wrt w,y
A1: y = (0. V) + y by RLVECT_1:4
.= (0. V) + (1 * y) by RLVECT_1:def_8
.= (0 * w) + (1 * y) by RLVECT_1:10 ;
A2: (1 * 0) + (0 * 1) = 0 ;
w = w + (0. V) by RLVECT_1:4
.= (1 * w) + (0. V) by RLVECT_1:def_8
.= (1 * w) + (0 * y) by RLVECT_1:10 ;
hence w,y are_Ort_wrt w,y by A1, A2, Def2; ::_thesis: verum
end;
theorem Th3: :: ANALMETR:3
ex V being RealLinearSpace ex w, y being VECTOR of V st Gen w,y
proof
consider V being RealLinearSpace such that
A1: ex u, v being VECTOR of V st
( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) by FUNCSDOM:23;
take V ; ::_thesis: ex w, y being VECTOR of V st Gen w,y
consider u, v being VECTOR of V such that
A2: ( ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Real st w = (a * u) + (b * v) ) ) by A1;
take u ; ::_thesis: ex y being VECTOR of V st Gen u,y
take v ; ::_thesis: Gen u,v
thus Gen u,v by A2, Def1; ::_thesis: verum
end;
theorem Th4: :: ANALMETR:4
for V being RealLinearSpace
for u, v, w, y being VECTOR of V st u,v are_Ort_wrt w,y holds
v,u are_Ort_wrt w,y
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, y being VECTOR of V st u,v are_Ort_wrt w,y holds
v,u are_Ort_wrt w,y
let u, v, w, y be VECTOR of V; ::_thesis: ( u,v are_Ort_wrt w,y implies v,u are_Ort_wrt w,y )
assume u,v are_Ort_wrt w,y ; ::_thesis: v,u are_Ort_wrt w,y
then ex a1, a2, b1, b2 being Real st
( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) & (a1 * b1) + (a2 * b2) = 0 ) by Def2;
hence v,u are_Ort_wrt w,y by Def2; ::_thesis: verum
end;
theorem Th5: :: ANALMETR:5
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V holds
( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y )
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V holds
( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y )
let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies for u, v being VECTOR of V holds
( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y ) )
assume A1: Gen w,y ; ::_thesis: for u, v being VECTOR of V holds
( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y )
let u, v be VECTOR of V; ::_thesis: ( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y )
consider a1, a2 being Real such that
A2: u = (a1 * w) + (a2 * y) by A1, Def1;
consider b1, b2 being Real such that
A3: v = (b1 * w) + (b2 * y) by A1, Def1;
A4: 0. V = (0. V) + (0. V) by RLVECT_1:4
.= (0 * w) + (0. V) by RLVECT_1:10
.= (0 * w) + (0 * y) by RLVECT_1:10 ;
(a1 * 0) + (a2 * 0) = 0 ;
hence u, 0. V are_Ort_wrt w,y by A2, A4, Def2; ::_thesis: 0. V,v are_Ort_wrt w,y
(0 * b1) + (0 * b2) = 0 ;
hence 0. V,v are_Ort_wrt w,y by A3, A4, Def2; ::_thesis: verum
end;
theorem Th6: :: ANALMETR:6
for V being RealLinearSpace
for u, v, w, y being VECTOR of V
for a, b being Real st u,v are_Ort_wrt w,y holds
a * u,b * v are_Ort_wrt w,y
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, y being VECTOR of V
for a, b being Real st u,v are_Ort_wrt w,y holds
a * u,b * v are_Ort_wrt w,y
let u, v, w, y be VECTOR of V; ::_thesis: for a, b being Real st u,v are_Ort_wrt w,y holds
a * u,b * v are_Ort_wrt w,y
let a, b be Real; ::_thesis: ( u,v are_Ort_wrt w,y implies a * u,b * v are_Ort_wrt w,y )
assume u,v are_Ort_wrt w,y ; ::_thesis: a * u,b * v are_Ort_wrt w,y
then consider a1, a2, b1, b2 being Real such that
A1: u = (a1 * w) + (a2 * y) and
A2: v = (b1 * w) + (b2 * y) and
A3: (a1 * b1) + (a2 * b2) = 0 by Def2;
A4: b * v = (b * (b1 * w)) + (b * (b2 * y)) by A2, RLVECT_1:def_5
.= ((b * b1) * w) + (b * (b2 * y)) by RLVECT_1:def_7
.= ((b * b1) * w) + ((b * b2) * y) by RLVECT_1:def_7 ;
A5: ((a * a1) * (b * b1)) + ((a * a2) * (b * b2)) = (b * a) * ((a1 * b1) + (a2 * b2))
.= 0 by A3 ;
a * u = (a * (a1 * w)) + (a * (a2 * y)) by A1, RLVECT_1:def_5
.= ((a * a1) * w) + (a * (a2 * y)) by RLVECT_1:def_7
.= ((a * a1) * w) + ((a * a2) * y) by RLVECT_1:def_7 ;
hence a * u,b * v are_Ort_wrt w,y by A4, A5, Def2; ::_thesis: verum
end;
theorem Th7: :: ANALMETR:7
for V being RealLinearSpace
for u, v, w, y being VECTOR of V
for a, b being Real st u,v are_Ort_wrt w,y holds
( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y )
proof
let V be RealLinearSpace; ::_thesis: for u, v, w, y being VECTOR of V
for a, b being Real st u,v are_Ort_wrt w,y holds
( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y )
let u, v, w, y be VECTOR of V; ::_thesis: for a, b being Real st u,v are_Ort_wrt w,y holds
( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y )
let a, b be Real; ::_thesis: ( u,v are_Ort_wrt w,y implies ( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y ) )
A1: ( v = 1 * v & u = 1 * u ) by RLVECT_1:def_8;
assume u,v are_Ort_wrt w,y ; ::_thesis: ( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y )
hence ( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y ) by A1, Th6; ::_thesis: verum
end;
theorem Th8: :: ANALMETR:8
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u being VECTOR of V ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds
for u being VECTOR of V ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies for u being VECTOR of V ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V ) )
assume A1: Gen w,y ; ::_thesis: for u being VECTOR of V ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
let u be VECTOR of V; ::_thesis: ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
consider a1, a2 being Real such that
A2: u = (a1 * w) + (a2 * y) by A1, Def1;
A3: now__::_thesis:_(_u_<>_0._V_implies_ex_v_being_Element_of_the_carrier_of_V_st_
(_u,v_are_Ort_wrt_w,y_&_v_<>_0._V_)_)
set v = (a2 * w) + ((- a1) * y);
assume A4: u <> 0. V ; ::_thesis: ex v being Element of the carrier of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
take v = (a2 * w) + ((- a1) * y); ::_thesis: ( u,v are_Ort_wrt w,y & v <> 0. V )
(a1 * a2) + (a2 * (- a1)) = 0 ;
hence u,v are_Ort_wrt w,y by A2, Def2; ::_thesis: v <> 0. V
v <> 0. V
proof
assume v = 0. V ; ::_thesis: contradiction
then ( a2 = 0 & - a1 = 0 ) by A1, Def1;
then u = (0 * w) + (0. V) by A2, RLVECT_1:10
.= 0 * w by RLVECT_1:4
.= 0. V by RLVECT_1:10 ;
hence contradiction by A4; ::_thesis: verum
end;
hence v <> 0. V ; ::_thesis: verum
end;
now__::_thesis:_(_u_=_0._V_implies_ex_v_being_VECTOR_of_V_st_
(_u,v_are_Ort_wrt_w,y_&_v_<>_0._V_)_)
assume A5: u = 0. V ; ::_thesis: ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
take v = w; ::_thesis: ( u,v are_Ort_wrt w,y & v <> 0. V )
thus u,v are_Ort_wrt w,y by A1, A5, Th5; ::_thesis: v <> 0. V
thus v <> 0. V by A1, Lm5; ::_thesis: verum
end;
hence ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V ) by A3; ::_thesis: verum
end;
theorem Th9: :: ANALMETR:9
for V being RealLinearSpace
for w, y, v, u1, u2 being VECTOR of V st Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v <> 0. V holds
ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
proof
let V be RealLinearSpace; ::_thesis: for w, y, v, u1, u2 being VECTOR of V st Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v <> 0. V holds
ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
let w, y, v, u1, u2 be VECTOR of V; ::_thesis: ( Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v <> 0. V implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )
assume that
A1: Gen w,y and
A2: v,u1 are_Ort_wrt w,y and
A3: v,u2 are_Ort_wrt w,y and
A4: v <> 0. V ; ::_thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
consider a1, a2, b1, b2 being Real such that
A5: v = (a1 * w) + (a2 * y) and
A6: u1 = (b1 * w) + (b2 * y) and
A7: (a1 * b1) + (a2 * b2) = 0 by A2, Def2;
consider a19, a29, c1, c2 being Real such that
A8: v = (a19 * w) + (a29 * y) and
A9: u2 = (c1 * w) + (c2 * y) and
A10: (a19 * c1) + (a29 * c2) = 0 by A3, Def2;
A11: a2 = a29 by A1, A5, A8, Lm4;
A12: a1 = a19 by A1, A5, A8, Lm4;
A13: now__::_thesis:_(_a1_=_0_implies_ex_a,_b_being_Real_st_
(_a_*_u1_=_b_*_u2_&_(_a_<>_0_or_b_<>_0_)_)_)
assume A14: a1 = 0 ; ::_thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
then A15: a2 <> 0 by A4, A5, Lm2;
then c2 = 0 by A10, A12, A11, A14, XCMPLX_1:6;
then u2 = (c1 * w) + (0. V) by A9, RLVECT_1:10;
then A16: u2 = c1 * w by RLVECT_1:4;
b2 = 0 by A7, A14, A15, XCMPLX_1:6;
then A17: u1 = (b1 * w) + (0. V) by A6, RLVECT_1:10;
then A18: u1 = b1 * w by RLVECT_1:4;
A19: now__::_thesis:_(_b1_=_0_implies_ex_a,_b_being_Real_st_
(_a_*_u1_=_b_*_u2_&_(_a_<>_0_or_b_<>_0_)_)_)
assume b1 = 0 ; ::_thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
then 1 * u1 = 0 * w by A18, RLVECT_1:def_8
.= 0. V by RLVECT_1:10
.= 0 * u2 by RLVECT_1:10 ;
hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) ; ::_thesis: verum
end;
c1 * u1 = c1 * (b1 * w) by A17, RLVECT_1:4
.= (b1 * c1) * w by RLVECT_1:def_7
.= b1 * u2 by A16, RLVECT_1:def_7 ;
hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A19; ::_thesis: verum
end;
now__::_thesis:_(_a1_<>_0_implies_ex_a,_b_being_Real_st_
(_a_*_u1_=_b_*_u2_&_(_a_<>_0_or_b_<>_0_)_)_)
A20: c2 * (((- a2) * b2) * (a1 ")) = b2 * (((- a2) * c2) * (a1 ")) ;
assume A21: a1 <> 0 ; ::_thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
A22: b1 = 1 * b1
.= (a1 * (a1 ")) * b1 by A21, XCMPLX_0:def_7
.= (a1 * b1) * (a1 ")
.= ((- a2) * b2) * (a1 ") by A7 ;
A23: c1 = 1 * c1
.= (a1 * (a1 ")) * c1 by A21, XCMPLX_0:def_7
.= (a1 * c1) * (a1 ")
.= ((- a2) * c2) * (a1 ") by A1, A5, A8, A10, A11, Lm4 ;
then A24: b2 * u2 = ((b2 * (((- a2) * c2) * (a1 "))) * w) + ((b2 * c2) * y) by A9, Lm3;
A25: now__::_thesis:_(_(_c2_<>_0_or_b2_<>_0_)_implies_ex_a,_b_being_Real_st_
(_a_*_u1_=_b_*_u2_&_(_a_<>_0_or_b_<>_0_)_)_)
assume A26: ( c2 <> 0 or b2 <> 0 ) ; ::_thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
take a = c2; ::_thesis: ex b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
take b = b2; ::_thesis: ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
thus ( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A6, A22, A24, A20, A26, Lm3; ::_thesis: verum
end;
now__::_thesis:_(_b2_=_0_&_c2_=_0_implies_ex_a,_b_being_Real_st_
(_a_*_u1_=_b_*_u2_&_(_a_<>_0_or_b_<>_0_)_)_)
assume ( b2 = 0 & c2 = 0 ) ; ::_thesis: ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
then 1 * u1 = 1 * u2 by A6, A9, A22, A23;
hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) ; ::_thesis: verum
end;
hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A25; ::_thesis: verum
end;
hence ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) by A13; ::_thesis: verum
end;
theorem Th10: :: ANALMETR:10
for V being RealLinearSpace
for w, y, u, v1, v2 being VECTOR of V st Gen w,y & u,v1 are_Ort_wrt w,y & u,v2 are_Ort_wrt w,y holds
( u,v1 + v2 are_Ort_wrt w,y & u,v1 - v2 are_Ort_wrt w,y )
proof
let V be RealLinearSpace; ::_thesis: for w, y, u, v1, v2 being VECTOR of V st Gen w,y & u,v1 are_Ort_wrt w,y & u,v2 are_Ort_wrt w,y holds
( u,v1 + v2 are_Ort_wrt w,y & u,v1 - v2 are_Ort_wrt w,y )
let w, y, u, v1, v2 be VECTOR of V; ::_thesis: ( Gen w,y & u,v1 are_Ort_wrt w,y & u,v2 are_Ort_wrt w,y implies ( u,v1 + v2 are_Ort_wrt w,y & u,v1 - v2 are_Ort_wrt w,y ) )
assume that
A1: Gen w,y and
A2: u,v1 are_Ort_wrt w,y and
A3: u,v2 are_Ort_wrt w,y ; ::_thesis: ( u,v1 + v2 are_Ort_wrt w,y & u,v1 - v2 are_Ort_wrt w,y )
consider a1, a2, b1, b2 being Real such that
A4: u = (a1 * w) + (a2 * y) and
A5: v1 = (b1 * w) + (b2 * y) and
A6: (a1 * b1) + (a2 * b2) = 0 by A2, Def2;
consider a19, a29, c1, c2 being Real such that
A7: u = (a19 * w) + (a29 * y) and
A8: v2 = (c1 * w) + (c2 * y) and
A9: (a19 * c1) + (a29 * c2) = 0 by A3, Def2;
A10: ( a1 = a19 & a2 = a29 ) by A1, A4, A7, Lm4;
then A11: (a1 * (b1 + c1)) + (a2 * (b2 + c2)) = 0 by A6, A9;
A12: (a1 * (b1 - c1)) + (a2 * (b2 - c2)) = 0 by A6, A9, A10;
v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) by A5, A8, Lm1;
hence u,v1 + v2 are_Ort_wrt w,y by A4, A11, Def2; ::_thesis: u,v1 - v2 are_Ort_wrt w,y
v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) by A5, A8, Lm1;
hence u,v1 - v2 are_Ort_wrt w,y by A4, A12, Def2; ::_thesis: verum
end;
theorem Th11: :: ANALMETR:11
for V being RealLinearSpace
for w, y, u being VECTOR of V st Gen w,y & u,u are_Ort_wrt w,y holds
u = 0. V
proof
let V be RealLinearSpace; ::_thesis: for w, y, u being VECTOR of V st Gen w,y & u,u are_Ort_wrt w,y holds
u = 0. V
let w, y, u be VECTOR of V; ::_thesis: ( Gen w,y & u,u are_Ort_wrt w,y implies u = 0. V )
A1: now__::_thesis:_for_a_being_Real_st_a_<>_0_holds_
0_<_a_*_a
let a be Real; ::_thesis: ( a <> 0 implies 0 < a * a )
assume A2: a <> 0 ; ::_thesis: 0 < a * a
( 0 < a implies 0 < a * a ) by XREAL_1:129;
hence 0 < a * a by A2, XREAL_1:130; ::_thesis: verum
end;
assume that
A3: Gen w,y and
A4: u,u are_Ort_wrt w,y ; ::_thesis: u = 0. V
consider a1, a2, b1, b2 being Real such that
A5: u = (a1 * w) + (a2 * y) and
A6: u = (b1 * w) + (b2 * y) and
A7: (a1 * b1) + (a2 * b2) = 0 by A4, Def2;
A8: ( a1 = b1 & a2 = b2 ) by A3, A5, A6, Lm4;
A9: a2 = 0
proof
assume a2 <> 0 ; ::_thesis: contradiction
then 0 < a2 * a2 by A1;
hence contradiction by A7, A8, XREAL_1:29, XREAL_1:63; ::_thesis: verum
end;
a1 = 0
proof
assume a1 <> 0 ; ::_thesis: contradiction
then 0 < a1 * a1 by A1;
hence contradiction by A7, A8, XREAL_1:29, XREAL_1:63; ::_thesis: verum
end;
hence u = (0 * w) + (0. V) by A5, A9, RLVECT_1:10
.= 0 * w by RLVECT_1:4
.= 0. V by RLVECT_1:10 ;
::_thesis: verum
end;
theorem Th12: :: ANALMETR:12
for V being RealLinearSpace
for w, y, u, u1, u2 being VECTOR of V st Gen w,y & u,u1 - u2 are_Ort_wrt w,y & u1,u2 - u are_Ort_wrt w,y holds
u2,u - u1 are_Ort_wrt w,y
proof
let V be RealLinearSpace; ::_thesis: for w, y, u, u1, u2 being VECTOR of V st Gen w,y & u,u1 - u2 are_Ort_wrt w,y & u1,u2 - u are_Ort_wrt w,y holds
u2,u - u1 are_Ort_wrt w,y
let w, y, u, u1, u2 be VECTOR of V; ::_thesis: ( Gen w,y & u,u1 - u2 are_Ort_wrt w,y & u1,u2 - u are_Ort_wrt w,y implies u2,u - u1 are_Ort_wrt w,y )
assume that
A1: Gen w,y and
A2: u,u1 - u2 are_Ort_wrt w,y and
A3: u1,u2 - u are_Ort_wrt w,y ; ::_thesis: u2,u - u1 are_Ort_wrt w,y
consider a1, a2 being Real such that
A4: u = (a1 * w) + (a2 * y) by A1, Def1;
consider c1, c2 being Real such that
A5: u2 = (c1 * w) + (c2 * y) by A1, Def1;
consider b1, b2 being Real such that
A6: u1 = (b1 * w) + (b2 * y) by A1, Def1;
A7: u - u1 = ((a1 - b1) * w) + ((a2 - b2) * y) by A4, A6, Lm1;
u2 - u = ((c1 - a1) * w) + ((c2 - a2) * y) by A4, A5, Lm1;
then A8: (b1 * (c1 - a1)) + (b2 * (c2 - a2)) = 0 by A1, A3, A6, Th1;
u1 - u2 = ((b1 - c1) * w) + ((b2 - c2) * y) by A6, A5, Lm1;
then (a1 * (b1 - c1)) + (a2 * (b2 - c2)) = 0 by A1, A2, A4, Th1;
then 0 = (c1 * (a1 - b1)) + (c2 * (a2 - b2)) by A8;
hence u2,u - u1 are_Ort_wrt w,y by A5, A7, Def2; ::_thesis: verum
end;
theorem Th13: :: ANALMETR:13
for V being RealLinearSpace
for w, y, u, v being VECTOR of V st Gen w,y & u <> 0. V holds
ex a being Real st v - (a * u),u are_Ort_wrt w,y
proof
let V be RealLinearSpace; ::_thesis: for w, y, u, v being VECTOR of V st Gen w,y & u <> 0. V holds
ex a being Real st v - (a * u),u are_Ort_wrt w,y
let w, y, u, v be VECTOR of V; ::_thesis: ( Gen w,y & u <> 0. V implies ex a being Real st v - (a * u),u are_Ort_wrt w,y )
assume that
A1: Gen w,y and
A2: u <> 0. V ; ::_thesis: ex a being Real st v - (a * u),u are_Ort_wrt w,y
consider a1, a2 being Real such that
A3: u = (a1 * w) + (a2 * y) by A1, Def1;
consider b1, b2 being Real such that
A4: v = (b1 * w) + (b2 * y) by A1, Def1;
set a = ((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ");
(((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * u = (((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1) * w) + (((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2) * y) by A3, Lm3;
then A5: v - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * u) = ((b1 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) * w) + ((b2 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2)) * y) by A4, Lm1;
A6: ((b1 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) * a1) + ((b2 - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2)) * a2) = ((a1 * b1) + (a2 * b2)) + ((- 1) * ((a1 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) + (a2 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2)))) ;
A7: (a1 * a1) + (a2 * a2) <> 0
proof
assume (a1 * a1) + (a2 * a2) = 0 ; ::_thesis: contradiction
then u,u are_Ort_wrt w,y by A3, Def2;
hence contradiction by A1, A2, Th11; ::_thesis: verum
end;
(- 1) * ((a1 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a1)) + (a2 * ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * a2))) = (- 1) * (((b1 * a1) + (b2 * a2)) * ((((a1 * a1) + (a2 * a2)) ") * ((a1 * a1) + (a2 * a2))))
.= (- 1) * (((b1 * a1) + (b2 * a2)) * 1) by A7, XCMPLX_0:def_7
.= - ((a1 * b1) + (a2 * b2)) ;
then v - ((((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) ")) * u),u are_Ort_wrt w,y by A3, A5, A6, Def2;
hence ex a being Real st v - (a * u),u are_Ort_wrt w,y ; ::_thesis: verum
end;
theorem Th14: :: ANALMETR:14
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of V holds
( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
proof
let V be RealLinearSpace; ::_thesis: for u, v, u1, v1 being VECTOR of V holds
( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
let u, v, u1, v1 be VECTOR of V; ::_thesis: ( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
A1: now__::_thesis:_for_w,_y,_w1,_y1_being_VECTOR_of_V_st_ex_a,_b_being_Real_st_
(_a_*_(y_-_w)_=_b_*_(y1_-_w1)_&_a_=_0_&_b_<>_0_)_holds_
w,y_//_w1,y1
let w, y, w1, y1 be VECTOR of V; ::_thesis: ( ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & a = 0 & b <> 0 ) implies w,y // w1,y1 )
given a, b being Real such that A2: ( a * (y - w) = b * (y1 - w1) & a = 0 ) and
A3: b <> 0 ; ::_thesis: w,y // w1,y1
0. V = b * (y1 - w1) by A2, RLVECT_1:10;
then y1 - w1 = 0. V by A3, RLVECT_1:11;
then y1 = w1 by RLVECT_1:21;
hence w,y // w1,y1 by ANALOAF:9; ::_thesis: verum
end;
A4: now__::_thesis:_for_w,_y,_w1,_y1_being_VECTOR_of_V_st_ex_a,_b_being_Real_st_
(_a_*_(y_-_w)_=_b_*_(y1_-_w1)_&_0_<_a_&_b_<_0_)_holds_
w,y_//_y1,w1
let w, y, w1, y1 be VECTOR of V; ::_thesis: ( ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & 0 < a & b < 0 ) implies w,y // y1,w1 )
given a, b being Real such that A5: a * (y - w) = b * (y1 - w1) and
A6: 0 < a and
A7: b < 0 ; ::_thesis: w,y // y1,w1
A8: a * (y - w) = b * (- (w1 - y1)) by A5, RLVECT_1:33
.= (- b) * (w1 - y1) by RLVECT_1:24 ;
0 < - b by A7, XREAL_1:58;
hence w,y // y1,w1 by A6, A8, ANALOAF:def_1; ::_thesis: verum
end;
A9: now__::_thesis:_(_for_a,_b_being_Real_holds_
(_not_a_*_(v_-_u)_=_b_*_(v1_-_u1)_or_(_not_a_<>_0_&_not_b_<>_0_)_)_or_u,v_//_u1,v1_or_u,v_//_v1,u1_)
given a, b being Real such that A10: a * (v - u) = b * (v1 - u1) and
A11: ( a <> 0 or b <> 0 ) ; ::_thesis: ( u,v // u1,v1 or u,v // v1,u1 )
A12: now__::_thesis:_(_a_<>_0_&_b_<>_0_&_not_u,v_//_u1,v1_implies_u,v_//_v1,u1_)
A13: now__::_thesis:_(_a_<_0_&_b_<_0_&_not_u,v_//_u1,v1_implies_u,v_//_v1,u1_)
assume ( a < 0 & b < 0 ) ; ::_thesis: ( u,v // u1,v1 or u,v // v1,u1 )
then A14: ( 0 < - a & 0 < - b ) by XREAL_1:58;
(- a) * (u - v) = a * (- (u - v)) by RLVECT_1:24
.= b * (v1 - u1) by A10, RLVECT_1:33
.= b * (- (u1 - v1)) by RLVECT_1:33
.= (- b) * (u1 - v1) by RLVECT_1:24 ;
then v,u // v1,u1 by A14, ANALOAF:def_1;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:12; ::_thesis: verum
end;
A15: now__::_thesis:_(_a_<_0_&_0_<_b_&_not_u,v_//_u1,v1_implies_u,v_//_v1,u1_)
assume ( a < 0 & 0 < b ) ; ::_thesis: ( u,v // u1,v1 or u,v // v1,u1 )
then u1,v1 // v,u by A4, A10;
then v,u // u1,v1 by ANALOAF:12;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:12; ::_thesis: verum
end;
assume A16: ( a <> 0 & b <> 0 ) ; ::_thesis: ( u,v // u1,v1 or u,v // v1,u1 )
( 0 < a & b < 0 & not u,v // u1,v1 implies u,v // v1,u1 ) by A4, A10;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by A10, A16, A15, A13, ANALOAF:def_1; ::_thesis: verum
end;
now__::_thesis:_(_not_b_=_0_or_u,v_//_u1,v1_or_u,v_//_v1,u1_)
assume b = 0 ; ::_thesis: ( u,v // u1,v1 or u,v // v1,u1 )
then u1,v1 // u,v by A1, A10, A11;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:12; ::_thesis: verum
end;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by A1, A10, A12; ::_thesis: verum
end;
A17: now__::_thesis:_for_w,_y,_w1,_y1_being_VECTOR_of_V_st_w,y_//_w1,y1_holds_
ex_a,_b_being_Real_st_
(_a_*_(y_-_w)_=_b_*_(y1_-_w1)_&_(_a_<>_0_or_b_<>_0_)_)
let w, y, w1, y1 be VECTOR of V; ::_thesis: ( w,y // w1,y1 implies ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) )
assume A18: w,y // w1,y1 ; ::_thesis: ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) )
A19: now__::_thesis:_(_w_=_y_implies_ex_a,_b_being_Real_st_
(_a_*_(y_-_w)_=_b_*_(y1_-_w1)_&_(_a_<>_0_or_b_<>_0_)_)_)
assume w = y ; ::_thesis: ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) )
then 1 * (y - w) = 0. V by RLVECT_1:10, RLVECT_1:15
.= 0 * (y1 - w1) by RLVECT_1:10 ;
hence ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ; ::_thesis: verum
end;
A20: now__::_thesis:_(_w1_=_y1_implies_ex_a,_b_being_Real_st_
(_a_*_(y_-_w)_=_b_*_(y1_-_w1)_&_(_a_<>_0_or_b_<>_0_)_)_)
assume w1 = y1 ; ::_thesis: ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) )
then 1 * (y1 - w1) = 0. V by RLVECT_1:10, RLVECT_1:15
.= 0 * (y - w) by RLVECT_1:10 ;
hence ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ; ::_thesis: verum
end;
( ex a, b being Real st
( 0 < a & 0 < b & a * (y - w) = b * (y1 - w1) ) implies ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ) ;
hence ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) by A18, A19, A20, ANALOAF:def_1; ::_thesis: verum
end;
now__::_thesis:_(_u,v_//_v1,u1_implies_ex_a,_b_being_Real_st_
(_a_*_(v_-_u)_=_b_*_(v1_-_u1)_&_(_a_<>_0_or_b_<>_0_)_)_)
assume u,v // v1,u1 ; ::_thesis: ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) )
then consider a, b being Real such that
A21: a * (v - u) = b * (u1 - v1) and
A22: ( a <> 0 or b <> 0 ) by A17;
A23: ( a <> 0 or - b <> 0 ) by A22;
(- b) * (v1 - u1) = b * (- (v1 - u1)) by RLVECT_1:24
.= a * (v - u) by A21, RLVECT_1:33 ;
hence ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by A23; ::_thesis: verum
end;
hence ( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) by A17, A9; ::_thesis: verum
end;
theorem Th15: :: ANALMETR:15
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of V holds
( [[u,v],[u1,v1]] in lambda (DirPar V) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
proof
let V be RealLinearSpace; ::_thesis: for u, v, u1, v1 being VECTOR of V holds
( [[u,v],[u1,v1]] in lambda (DirPar V) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
let u, v, u1, v1 be VECTOR of V; ::_thesis: ( [[u,v],[u1,v1]] in lambda (DirPar V) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
( [[u,v],[u1,v1]] in lambda (DirPar V) iff ( [[u,v],[u1,v1]] in DirPar V or [[u,v],[v1,u1]] in DirPar V ) ) by DIRAF:def_1;
then ( [[u,v],[u1,v1]] in lambda (DirPar V) iff ( u,v // u1,v1 or u,v // v1,u1 ) ) by ANALOAF:22;
hence ( [[u,v],[u1,v1]] in lambda (DirPar V) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) by Th14; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
let u, u1, v, v1, w, y be VECTOR of V;
predu,u1,v,v1 are_Ort_wrt w,y means :Def3: :: ANALMETR:def 3
u1 - u,v1 - v are_Ort_wrt w,y;
end;
:: deftheorem Def3 defines are_Ort_wrt ANALMETR:def_3_:_
for V being RealLinearSpace
for u, u1, v, v1, w, y being VECTOR of V holds
( u,u1,v,v1 are_Ort_wrt w,y iff u1 - u,v1 - v are_Ort_wrt w,y );
definition
let V be RealLinearSpace;
let w, y be VECTOR of V;
func Orthogonality (V,w,y) -> Relation of [: the carrier of V, the carrier of V:] means :Def4: :: ANALMETR:def 4
for x, z being set holds
( [x,z] in it iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) );
existence
ex b1 being Relation of [: the carrier of V, the carrier of V:] st
for x, z being set holds
( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) )
proof
defpred S1[ set , set ] means ex u, u1, v, v1 being VECTOR of V st
( $1 = [u,u1] & $2 = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y );
set VV = [: the carrier of V, the carrier of V:];
consider P being Relation of [: the carrier of V, the carrier of V:],[: the carrier of V, the carrier of V:] such that
A1: for x, z being set holds
( [x,z] in P iff ( x in [: the carrier of V, the carrier of V:] & z in [: the carrier of V, the carrier of V:] & S1[x,z] ) ) from RELSET_1:sch_1();
take P ; ::_thesis: for x, z being set holds
( [x,z] in P iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) )
let x, z be set ; ::_thesis: ( [x,z] in P iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) )
thus ( [x,z] in P implies ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) by A1; ::_thesis: ( ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) implies [x,z] in P )
assume ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ; ::_thesis: [x,z] in P
hence [x,z] in P by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Relation of [: the carrier of V, the carrier of V:] st ( for x, z being set holds
( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) & ( for x, z being set holds
( [x,z] in b2 iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) holds
b1 = b2
proof
let P, Q be Relation of [: the carrier of V, the carrier of V:]; ::_thesis: ( ( for x, z being set holds
( [x,z] in P iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) & ( for x, z being set holds
( [x,z] in Q iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) implies P = Q )
assume that
A2: for x, z being set holds
( [x,z] in P iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) and
A3: for x, z being set holds
( [x,z] in Q iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ; ::_thesis: P = Q
for x, z being set holds
( [x,z] in P iff [x,z] in Q )
proof
let x, z be set ; ::_thesis: ( [x,z] in P iff [x,z] in Q )
( [x,z] in P iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) by A2;
hence ( [x,z] in P iff [x,z] in Q ) by A3; ::_thesis: verum
end;
hence P = Q by RELAT_1:def_2; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Orthogonality ANALMETR:def_4_:_
for V being RealLinearSpace
for w, y being VECTOR of V
for b4 being Relation of [: the carrier of V, the carrier of V:] holds
( b4 = Orthogonality (V,w,y) iff for x, z being set holds
( [x,z] in b4 iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) );
theorem Th16: :: ANALMETR:16
for V being RealLinearSpace holds the carrier of (Lambda (OASpace V)) = the carrier of V
proof
let V be RealLinearSpace; ::_thesis: the carrier of (Lambda (OASpace V)) = the carrier of V
( Lambda (OASpace V) = AffinStruct(# the carrier of (OASpace V),(lambda the CONGR of (OASpace V)) #) & OASpace V = AffinStruct(# the carrier of V,(DirPar V) #) ) by ANALOAF:def_4, DIRAF:def_2;
hence the carrier of (Lambda (OASpace V)) = the carrier of V ; ::_thesis: verum
end;
theorem Th17: :: ANALMETR:17
for V being RealLinearSpace holds the CONGR of (Lambda (OASpace V)) = lambda (DirPar V)
proof
let V be RealLinearSpace; ::_thesis: the CONGR of (Lambda (OASpace V)) = lambda (DirPar V)
( Lambda (OASpace V) = AffinStruct(# the carrier of (OASpace V),(lambda the CONGR of (OASpace V)) #) & OASpace V = AffinStruct(# the carrier of V,(DirPar V) #) ) by ANALOAF:def_4, DIRAF:def_2;
hence the CONGR of (Lambda (OASpace V)) = lambda (DirPar V) ; ::_thesis: verum
end;
theorem :: ANALMETR:18
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of V
for p, q, p1, q1 being Element of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
proof
let V be RealLinearSpace; ::_thesis: for u, v, u1, v1 being VECTOR of V
for p, q, p1, q1 being Element of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
let u, v, u1, v1 be VECTOR of V; ::_thesis: for p, q, p1, q1 being Element of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
let p, q, p1, q1 be Element of (Lambda (OASpace V)); ::_thesis: ( p = u & q = v & p1 = u1 & q1 = v1 implies ( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) )
assume A1: ( p = u & q = v & p1 = u1 & q1 = v1 ) ; ::_thesis: ( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
hereby ::_thesis: ( ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) implies p,q // p1,q1 )
assume p,q // p1,q1 ; ::_thesis: ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) )
then [[p,q],[p1,q1]] in the CONGR of (Lambda (OASpace V)) by ANALOAF:def_2;
then [[u,v],[u1,v1]] in lambda (DirPar V) by A1, Th17;
hence ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by Th15; ::_thesis: verum
end;
given a, b being Real such that A2: ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ; ::_thesis: p,q // p1,q1
[[u,v],[u1,v1]] in lambda (DirPar V) by A2, Th15;
then [[p,q],[p1,q1]] in the CONGR of (Lambda (OASpace V)) by A1, Th17;
hence p,q // p1,q1 by ANALOAF:def_2; ::_thesis: verum
end;
definition
attrc1 is strict ;
struct ParOrtStr -> AffinStruct ;
aggrParOrtStr(# carrier, CONGR, orthogonality #) -> ParOrtStr ;
sel orthogonality c1 -> Relation of [: the carrier of c1, the carrier of c1:];
end;
registration
cluster non empty for ParOrtStr ;
existence
not for b1 being ParOrtStr holds b1 is empty
proof
set A = the non empty set ;
set C = the Relation of [: the non empty set , the non empty set :];
take ParOrtStr(# the non empty set , the Relation of [: the non empty set , the non empty set :], the Relation of [: the non empty set , the non empty set :] #) ; ::_thesis: not ParOrtStr(# the non empty set , the Relation of [: the non empty set , the non empty set :], the Relation of [: the non empty set , the non empty set :] #) is empty
thus not the carrier of ParOrtStr(# the non empty set , the Relation of [: the non empty set , the non empty set :], the Relation of [: the non empty set , the non empty set :] #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
definition
let POS be non empty ParOrtStr ;
let a, b, c, d be Element of POS;
preda,b _|_ c,d means :Def5: :: ANALMETR:def 5
[[a,b],[c,d]] in the orthogonality of POS;
end;
:: deftheorem Def5 defines _|_ ANALMETR:def_5_:_
for POS being non empty ParOrtStr
for a, b, c, d being Element of POS holds
( a,b _|_ c,d iff [[a,b],[c,d]] in the orthogonality of POS );
definition
let V be RealLinearSpace;
let w, y be VECTOR of V;
func AMSpace (V,w,y) -> strict ParOrtStr equals :: ANALMETR:def 6
ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality (V,w,y)) #);
correctness
coherence
ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality (V,w,y)) #) is strict ParOrtStr ;
;
end;
:: deftheorem defines AMSpace ANALMETR:def_6_:_
for V being RealLinearSpace
for w, y being VECTOR of V holds AMSpace (V,w,y) = ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality (V,w,y)) #);
registration
let V be RealLinearSpace;
let w, y be VECTOR of V;
cluster AMSpace (V,w,y) -> non empty strict ;
coherence
not AMSpace (V,w,y) is empty ;
end;
theorem :: ANALMETR:19
for V being RealLinearSpace
for w, y being VECTOR of V holds
( the carrier of (AMSpace (V,w,y)) = the carrier of V & the CONGR of (AMSpace (V,w,y)) = lambda (DirPar V) & the orthogonality of (AMSpace (V,w,y)) = Orthogonality (V,w,y) ) ;
definition
let POS be non empty ParOrtStr ;
func Af POS -> strict AffinStruct equals :: ANALMETR:def 7
AffinStruct(# the carrier of POS, the CONGR of POS #);
correctness
coherence
AffinStruct(# the carrier of POS, the CONGR of POS #) is strict AffinStruct ;
;
end;
:: deftheorem defines Af ANALMETR:def_7_:_
for POS being non empty ParOrtStr holds Af POS = AffinStruct(# the carrier of POS, the CONGR of POS #);
registration
let POS be non empty ParOrtStr ;
cluster Af POS -> non empty strict ;
coherence
not Af POS is empty ;
end;
theorem Th20: :: ANALMETR:20
for V being RealLinearSpace
for w, y being VECTOR of V holds Af (AMSpace (V,w,y)) = Lambda (OASpace V)
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V holds Af (AMSpace (V,w,y)) = Lambda (OASpace V)
let w, y be VECTOR of V; ::_thesis: Af (AMSpace (V,w,y)) = Lambda (OASpace V)
set Y = OASpace V;
the carrier of (Lambda (OASpace V)) = the carrier of V by Th16;
hence Af (AMSpace (V,w,y)) = Lambda (OASpace V) by Th17; ::_thesis: verum
end;
theorem Th21: :: ANALMETR:21
for V being RealLinearSpace
for u, u1, v, v1, w, y being VECTOR of V
for p, p1, q, q1 being Element of (AMSpace (V,w,y)) st p = u & p1 = u1 & q = v & q1 = v1 holds
( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y )
proof
let V be RealLinearSpace; ::_thesis: for u, u1, v, v1, w, y being VECTOR of V
for p, p1, q, q1 being Element of (AMSpace (V,w,y)) st p = u & p1 = u1 & q = v & q1 = v1 holds
( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y )
let u, u1, v, v1, w, y be VECTOR of V; ::_thesis: for p, p1, q, q1 being Element of (AMSpace (V,w,y)) st p = u & p1 = u1 & q = v & q1 = v1 holds
( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y )
let p, p1, q, q1 be Element of (AMSpace (V,w,y)); ::_thesis: ( p = u & p1 = u1 & q = v & q1 = v1 implies ( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y ) )
assume A1: ( p = u & p1 = u1 & q = v & q1 = v1 ) ; ::_thesis: ( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y )
A2: ( p,q _|_ p1,q1 iff [[p,q],[p1,q1]] in the orthogonality of (AMSpace (V,w,y)) ) by Def5;
hereby ::_thesis: ( u,v,u1,v1 are_Ort_wrt w,y implies p,q _|_ p1,q1 )
assume p,q _|_ p1,q1 ; ::_thesis: u,v,u1,v1 are_Ort_wrt w,y
then consider u9, v9, u19, v19 being VECTOR of V such that
A3: [u,v] = [u9,v9] and
A4: [u1,v1] = [u19,v19] and
A5: u9,v9,u19,v19 are_Ort_wrt w,y by A1, A2, Def4;
A6: u1 = u19 by A4, XTUPLE_0:1;
( u = u9 & v = v9 ) by A3, XTUPLE_0:1;
hence u,v,u1,v1 are_Ort_wrt w,y by A4, A5, A6, XTUPLE_0:1; ::_thesis: verum
end;
assume u,v,u1,v1 are_Ort_wrt w,y ; ::_thesis: p,q _|_ p1,q1
hence p,q _|_ p1,q1 by A1, A2, Def4; ::_thesis: verum
end;
theorem Th22: :: ANALMETR:22
for V being RealLinearSpace
for w, y, u, v, u1, v1 being VECTOR of V
for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
proof
let V be RealLinearSpace; ::_thesis: for w, y, u, v, u1, v1 being VECTOR of V
for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
let w, y, u, v, u1, v1 be VECTOR of V; ::_thesis: for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
let p, q, p1, q1 be Element of (AMSpace (V,w,y)); ::_thesis: ( p = u & q = v & p1 = u1 & q1 = v1 implies ( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) )
assume A1: ( p = u & q = v & p1 = u1 & q1 = v1 ) ; ::_thesis: ( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
hereby ::_thesis: ( ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) implies p,q // p1,q1 )
assume p,q // p1,q1 ; ::_thesis: ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) )
then [[p,q],[p1,q1]] in the CONGR of (AMSpace (V,w,y)) by ANALOAF:def_2;
hence ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by A1, Th15; ::_thesis: verum
end;
given a, b being Real such that A2: ( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ; ::_thesis: p,q // p1,q1
[[u,v],[u1,v1]] in lambda (DirPar V) by A2, Th15;
hence p,q // p1,q1 by A1, ANALOAF:def_2; ::_thesis: verum
end;
theorem Th23: :: ANALMETR:23
for V being RealLinearSpace
for w, y being VECTOR of V
for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds
p1,q1 _|_ p,q
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V
for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds
p1,q1 _|_ p,q
let w, y be VECTOR of V; ::_thesis: for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds
p1,q1 _|_ p,q
let p, q, p1, q1 be Element of (AMSpace (V,w,y)); ::_thesis: ( p,q _|_ p1,q1 implies p1,q1 _|_ p,q )
reconsider u = p, v = q, u1 = p1, v1 = q1 as Element of V ;
assume p,q _|_ p1,q1 ; ::_thesis: p1,q1 _|_ p,q
then u,v,u1,v1 are_Ort_wrt w,y by Th21;
then v - u,v1 - u1 are_Ort_wrt w,y by Def3;
then v1 - u1,v - u are_Ort_wrt w,y by Th4;
then u1,v1,u,v are_Ort_wrt w,y by Def3;
hence p1,q1 _|_ p,q by Th21; ::_thesis: verum
end;
theorem Th24: :: ANALMETR:24
for V being RealLinearSpace
for w, y being VECTOR of V
for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds
p,q _|_ q1,p1
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V
for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds
p,q _|_ q1,p1
let w, y be VECTOR of V; ::_thesis: for p, q, p1, q1 being Element of (AMSpace (V,w,y)) st p,q _|_ p1,q1 holds
p,q _|_ q1,p1
let p, q, p1, q1 be Element of (AMSpace (V,w,y)); ::_thesis: ( p,q _|_ p1,q1 implies p,q _|_ q1,p1 )
reconsider u = p, v = q, u1 = p1, v1 = q1 as Element of V ;
assume p,q _|_ p1,q1 ; ::_thesis: p,q _|_ q1,p1
then u,v,u1,v1 are_Ort_wrt w,y by Th21;
then v - u,v1 - u1 are_Ort_wrt w,y by Def3;
then A1: v - u,(- 1) * (v1 - u1) are_Ort_wrt w,y by Th7;
(- 1) * (v1 - u1) = - (v1 - u1) by RLVECT_1:16
.= u1 - v1 by RLVECT_1:33 ;
then u,v,v1,u1 are_Ort_wrt w,y by A1, Def3;
hence p,q _|_ q1,p1 by Th21; ::_thesis: verum
end;
theorem Th25: :: ANALMETR:25
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for p, q, r being Element of (AMSpace (V,w,y)) holds p,q _|_ r,r
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds
for p, q, r being Element of (AMSpace (V,w,y)) holds p,q _|_ r,r
let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies for p, q, r being Element of (AMSpace (V,w,y)) holds p,q _|_ r,r )
assume A1: Gen w,y ; ::_thesis: for p, q, r being Element of (AMSpace (V,w,y)) holds p,q _|_ r,r
let p, q, r be Element of (AMSpace (V,w,y)); ::_thesis: p,q _|_ r,r
reconsider u = p, v = q, u1 = r as Element of V ;
u1 - u1 = 0. V by RLVECT_1:15;
then v - u,u1 - u1 are_Ort_wrt w,y by A1, Th5;
then u,v,u1,u1 are_Ort_wrt w,y by Def3;
hence p,q _|_ r,r by Th21; ::_thesis: verum
end;
theorem Th26: :: ANALMETR:26
for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1, q, q1, r, r1 being Element of (AMSpace (V,w,y)) st p,p1 _|_ q,q1 & p,p1 // r,r1 & not p = p1 holds
q,q1 _|_ r,r1
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V
for p, p1, q, q1, r, r1 being Element of (AMSpace (V,w,y)) st p,p1 _|_ q,q1 & p,p1 // r,r1 & not p = p1 holds
q,q1 _|_ r,r1
let w, y be VECTOR of V; ::_thesis: for p, p1, q, q1, r, r1 being Element of (AMSpace (V,w,y)) st p,p1 _|_ q,q1 & p,p1 // r,r1 & not p = p1 holds
q,q1 _|_ r,r1
let p, p1, q, q1, r, r1 be Element of (AMSpace (V,w,y)); ::_thesis: ( p,p1 _|_ q,q1 & p,p1 // r,r1 & not p = p1 implies q,q1 _|_ r,r1 )
assume that
A1: p,p1 _|_ q,q1 and
A2: p,p1 // r,r1 ; ::_thesis: ( p = p1 or q,q1 _|_ r,r1 )
reconsider u = p, v = p1, u1 = q, v1 = q1, u2 = r, v2 = r1 as Element of V ;
consider a, b being Real such that
A3: a * (v - u) = b * (v2 - u2) and
A4: ( a <> 0 or b <> 0 ) by A2, Th22;
assume A5: p <> p1 ; ::_thesis: q,q1 _|_ r,r1
b <> 0
proof
assume A6: b = 0 ; ::_thesis: contradiction
then a * (v - u) = 0. V by A3, RLVECT_1:10;
then v - u = 0. V by A4, A6, RLVECT_1:11;
hence contradiction by A5, RLVECT_1:21; ::_thesis: verum
end;
then A7: v2 - u2 = (b ") * (a * (v - u)) by A3, ANALOAF:5
.= ((b ") * a) * (v - u) by RLVECT_1:def_7 ;
u,v,u1,v1 are_Ort_wrt w,y by A1, Th21;
then v - u,v1 - u1 are_Ort_wrt w,y by Def3;
then v2 - u2,v1 - u1 are_Ort_wrt w,y by A7, Th7;
then v1 - u1,v2 - u2 are_Ort_wrt w,y by Th4;
then u1,v1,u2,v2 are_Ort_wrt w,y by Def3;
hence q,q1 _|_ r,r1 by Th21; ::_thesis: verum
end;
theorem Th27: :: ANALMETR:27
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for p, q, r being Element of (AMSpace (V,w,y)) ex r1 being Element of (AMSpace (V,w,y)) st
( p,q _|_ r,r1 & r <> r1 )
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds
for p, q, r being Element of (AMSpace (V,w,y)) ex r1 being Element of (AMSpace (V,w,y)) st
( p,q _|_ r,r1 & r <> r1 )
let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies for p, q, r being Element of (AMSpace (V,w,y)) ex r1 being Element of (AMSpace (V,w,y)) st
( p,q _|_ r,r1 & r <> r1 ) )
assume A1: Gen w,y ; ::_thesis: for p, q, r being Element of (AMSpace (V,w,y)) ex r1 being Element of (AMSpace (V,w,y)) st
( p,q _|_ r,r1 & r <> r1 )
let p, q, r be Element of (AMSpace (V,w,y)); ::_thesis: ex r1 being Element of (AMSpace (V,w,y)) st
( p,q _|_ r,r1 & r <> r1 )
reconsider u = p, v = q, u1 = r as Element of V ;
consider v2 being VECTOR of V such that
A2: v - u,v2 are_Ort_wrt w,y and
A3: v2 <> 0. V by A1, Th8;
set v1 = u1 + v2;
reconsider r1 = u1 + v2 as Element of (AMSpace (V,w,y)) ;
A4: (u1 + v2) - u1 = v2 + (u1 - u1) by RLVECT_1:def_3
.= v2 + (0. V) by RLVECT_1:15
.= v2 by RLVECT_1:4 ;
then u,v,u1,u1 + v2 are_Ort_wrt w,y by A2, Def3;
then A5: p,q _|_ r,r1 by Th21;
r <> r1 by A3, A4, RLVECT_1:15;
hence ex r1 being Element of (AMSpace (V,w,y)) st
( p,q _|_ r,r1 & r <> r1 ) by A5; ::_thesis: verum
end;
theorem Th28: :: ANALMETR:28
for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1, q, q1, r, r1 being Element of (AMSpace (V,w,y)) st Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 & not p = p1 holds
q,q1 // r,r1
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V
for p, p1, q, q1, r, r1 being Element of (AMSpace (V,w,y)) st Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 & not p = p1 holds
q,q1 // r,r1
let w, y be VECTOR of V; ::_thesis: for p, p1, q, q1, r, r1 being Element of (AMSpace (V,w,y)) st Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 & not p = p1 holds
q,q1 // r,r1
let p, p1, q, q1, r, r1 be Element of (AMSpace (V,w,y)); ::_thesis: ( Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 & not p = p1 implies q,q1 // r,r1 )
assume that
A1: Gen w,y and
A2: p,p1 _|_ q,q1 and
A3: p,p1 _|_ r,r1 ; ::_thesis: ( p = p1 or q,q1 // r,r1 )
reconsider u = p, v = p1, u1 = q, v1 = q1, u2 = r, v2 = r1 as Element of V ;
u,v,u2,v2 are_Ort_wrt w,y by A3, Th21;
then A4: v - u,v2 - u2 are_Ort_wrt w,y by Def3;
assume p <> p1 ; ::_thesis: q,q1 // r,r1
then A5: v - u <> 0. V by RLVECT_1:21;
u,v,u1,v1 are_Ort_wrt w,y by A2, Th21;
then v - u,v1 - u1 are_Ort_wrt w,y by Def3;
then ex a, b being Real st
( a * (v1 - u1) = b * (v2 - u2) & ( a <> 0 or b <> 0 ) ) by A1, A4, A5, Th9;
hence q,q1 // r,r1 by Th22; ::_thesis: verum
end;
theorem Th29: :: ANALMETR:29
for V being RealLinearSpace
for w, y being VECTOR of V
for p, q, r, r1, r2 being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 holds
p,q _|_ r1,r2
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V
for p, q, r, r1, r2 being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 holds
p,q _|_ r1,r2
let w, y be VECTOR of V; ::_thesis: for p, q, r, r1, r2 being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 holds
p,q _|_ r1,r2
let p, q, r, r1, r2 be Element of (AMSpace (V,w,y)); ::_thesis: ( Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 implies p,q _|_ r1,r2 )
assume that
A1: Gen w,y and
A2: p,q _|_ r,r1 and
A3: p,q _|_ r,r2 ; ::_thesis: p,q _|_ r1,r2
reconsider u = p, v = q, w1 = r, v1 = r1, v2 = r2 as Element of V ;
u,v,w1,v2 are_Ort_wrt w,y by A3, Th21;
then A4: v - u,v2 - w1 are_Ort_wrt w,y by Def3;
A5: (v2 - w1) - (v1 - w1) = v2 - ((v1 - w1) + w1) by RLVECT_1:27
.= v2 - (v1 - (w1 - w1)) by RLVECT_1:29
.= v2 - (v1 - (0. V)) by RLVECT_1:15
.= v2 - v1 by RLVECT_1:13 ;
u,v,w1,v1 are_Ort_wrt w,y by A2, Th21;
then v - u,v1 - w1 are_Ort_wrt w,y by Def3;
then v - u,(v2 - w1) - (v1 - w1) are_Ort_wrt w,y by A1, A4, Th10;
then u,v,v1,v2 are_Ort_wrt w,y by A5, Def3;
hence p,q _|_ r1,r2 by Th21; ::_thesis: verum
end;
theorem Th30: :: ANALMETR:30
for V being RealLinearSpace
for w, y being VECTOR of V
for p, q being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p,q holds
p = q
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V
for p, q being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p,q holds
p = q
let w, y be VECTOR of V; ::_thesis: for p, q being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p,q holds
p = q
let p, q be Element of (AMSpace (V,w,y)); ::_thesis: ( Gen w,y & p,q _|_ p,q implies p = q )
assume that
A1: Gen w,y and
A2: p,q _|_ p,q ; ::_thesis: p = q
reconsider u = p, v = q as Element of V ;
u,v,u,v are_Ort_wrt w,y by A2, Th21;
then v - u,v - u are_Ort_wrt w,y by Def3;
then v - u = 0. V by A1, Th11;
hence p = q by RLVECT_1:21; ::_thesis: verum
end;
theorem :: ANALMETR:31
for V being RealLinearSpace
for w, y being VECTOR of V
for p, q, p1, p2 being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p holds
p2,q _|_ p,p1
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V
for p, q, p1, p2 being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p holds
p2,q _|_ p,p1
let w, y be VECTOR of V; ::_thesis: for p, q, p1, p2 being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p holds
p2,q _|_ p,p1
let p, q, p1, p2 be Element of (AMSpace (V,w,y)); ::_thesis: ( Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p implies p2,q _|_ p,p1 )
assume that
A1: Gen w,y and
A2: p,q _|_ p1,p2 and
A3: p1,q _|_ p2,p ; ::_thesis: p2,q _|_ p,p1
reconsider u = p, v = q, u1 = p1, u2 = p2 as Element of V ;
u,v,u1,u2 are_Ort_wrt w,y by A2, Th21;
then A4: v - u,u2 - u1 are_Ort_wrt w,y by Def3;
u1,v,u2,u are_Ort_wrt w,y by A3, Th21;
then A5: v - u1,u - u2 are_Ort_wrt w,y by Def3;
A6: now__::_thesis:_for_u,_v,_w_being_VECTOR_of_V_holds_(u_-_v)_-_(u_-_w)_=_w_-_v
let u, v, w be VECTOR of V; ::_thesis: (u - v) - (u - w) = w - v
thus (u - v) - (u - w) = (w - u) + (u - v) by RLVECT_1:33
.= w - v by ANALOAF:1 ; ::_thesis: verum
end;
then A7: (v - u) - (v - u1) = u1 - u ;
( (v - u1) - (v - u2) = u2 - u1 & (v - u2) - (v - u) = u - u2 ) by A6;
then v - u2,(v - u) - (v - u1) are_Ort_wrt w,y by A1, A4, A5, Th12;
then u2,v,u,u1 are_Ort_wrt w,y by A7, Def3;
hence p2,q _|_ p,p1 by Th21; ::_thesis: verum
end;
theorem Th32: :: ANALMETR:32
for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1 being Element of (AMSpace (V,w,y)) st Gen w,y & p <> p1 holds
for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V
for p, p1 being Element of (AMSpace (V,w,y)) st Gen w,y & p <> p1 holds
for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
let w, y be VECTOR of V; ::_thesis: for p, p1 being Element of (AMSpace (V,w,y)) st Gen w,y & p <> p1 holds
for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
let p, p1 be Element of (AMSpace (V,w,y)); ::_thesis: ( Gen w,y & p <> p1 implies for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q ) )
assume that
A1: Gen w,y and
A2: p <> p1 ; ::_thesis: for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
let q be Element of (AMSpace (V,w,y)); ::_thesis: ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
reconsider u = p, v = q, u1 = p1 as Element of V ;
u1 - u <> 0. V by A2, RLVECT_1:21;
then consider a being Real such that
A3: (v - u) - (a * (u1 - u)),u1 - u are_Ort_wrt w,y by A1, Th13;
set v1 = u + (a * (u1 - u));
reconsider q1 = u + (a * (u1 - u)) as Element of (AMSpace (V,w,y)) ;
v - (u + (a * (u1 - u))) = (v - u) - (a * (u1 - u)) by RLVECT_1:27;
then u1 - u,v - (u + (a * (u1 - u))) are_Ort_wrt w,y by A3, Th4;
then u,u1,u + (a * (u1 - u)),v are_Ort_wrt w,y by Def3;
then A4: p,p1 _|_ q1,q by Th21;
a * (u1 - u) = (a * (u1 - u)) + (0. V) by RLVECT_1:4
.= (a * (u1 - u)) + (u - u) by RLVECT_1:15
.= (u + (a * (u1 - u))) - u by RLVECT_1:def_3
.= 1 * ((u + (a * (u1 - u))) - u) by RLVECT_1:def_8 ;
then p,p1 // p,q1 by Th22;
hence ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q ) by A4; ::_thesis: verum
end;
consider V0 being RealLinearSpace such that
Lm6: ex w, y being VECTOR of V0 st Gen w,y by Th3;
consider w0, y0 being VECTOR of V0 such that
Lm7: Gen w0,y0 by Lm6;
Lm8: now__::_thesis:_(_AffinStruct(#_the_carrier_of_(AMSpace_(V0,w0,y0)),_the_CONGR_of_(AMSpace_(V0,w0,y0))_#)_is_AffinSpace_&_(_for_a,_b,_c,_d,_p,_q,_r,_s_being_Element_of_(AMSpace_(V0,w0,y0))_holds_
(_(_a,b__|__a,b_implies_a_=_b_)_&_a,b__|__c,c_&_(_a,b__|__c,d_implies_(_a,b__|__d,c_&_c,d__|__a,b_)_)_&_(_a,b__|__p,q_&_a,b_//_r,s_&_not_p,q__|__r,s_implies_a_=_b_)_&_(_a,b__|__p,q_&_a,b__|__p,s_implies_a,b__|__q,s_)_)_)_&_(_for_a,_b,_c_being_Element_of_(AMSpace_(V0,w0,y0))_st_a_<>_b_holds_
ex_x_being_Element_of_(AMSpace_(V0,w0,y0))_st_
(_a,b_//_a,x_&_a,b__|__x,c_)_)_&_(_for_a,_b,_c_being_Element_of_(AMSpace_(V0,w0,y0))_ex_x_being_Element_of_(AMSpace_(V0,w0,y0))_st_
(_a,b__|__c,x_&_c_<>_x_)_)_)
set X = AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #);
AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) = Af (AMSpace (V0,w0,y0)) ;
then A1: AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) = Lambda (OASpace V0) by Th20;
for a, b being Real st (a * w0) + (b * y0) = 0. V0 holds
( a = 0 & b = 0 ) by Def1, Lm7;
then OASpace V0 is OAffinSpace by ANALOAF:26;
hence ( AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) is AffinSpace & ( for a, b, c, d, p, q, r, s being Element of (AMSpace (V0,w0,y0)) holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) ) & ( for a, b, c being Element of (AMSpace (V0,w0,y0)) st a <> b holds
ex x being Element of (AMSpace (V0,w0,y0)) st
( a,b // a,x & a,b _|_ x,c ) ) & ( for a, b, c being Element of (AMSpace (V0,w0,y0)) ex x being Element of (AMSpace (V0,w0,y0)) st
( a,b _|_ c,x & c <> x ) ) ) by A1, Lm7, Th23, Th24, Th25, Th26, Th27, Th29, Th30, Th32, DIRAF:41; ::_thesis: verum
end;
definition
let IT be non empty ParOrtStr ;
attrIT is OrtAfSp-like means :Def8: :: ANALMETR:def 8
( AffinStruct(# the carrier of IT, the CONGR of IT #) is AffinSpace & ( for a, b, c, d, p, q, r, s being Element of IT holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) ) & ( for a, b, c being Element of IT st a <> b holds
ex x being Element of IT st
( a,b // a,x & a,b _|_ x,c ) ) & ( for a, b, c being Element of IT ex x being Element of IT st
( a,b _|_ c,x & c <> x ) ) );
end;
:: deftheorem Def8 defines OrtAfSp-like ANALMETR:def_8_:_
for IT being non empty ParOrtStr holds
( IT is OrtAfSp-like iff ( AffinStruct(# the carrier of IT, the CONGR of IT #) is AffinSpace & ( for a, b, c, d, p, q, r, s being Element of IT holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) ) & ( for a, b, c being Element of IT st a <> b holds
ex x being Element of IT st
( a,b // a,x & a,b _|_ x,c ) ) & ( for a, b, c being Element of IT ex x being Element of IT st
( a,b _|_ c,x & c <> x ) ) ) );
registration
cluster non empty strict OrtAfSp-like for ParOrtStr ;
existence
ex b1 being non empty ParOrtStr st
( b1 is strict & b1 is OrtAfSp-like )
proof
AMSpace (V0,w0,y0) is OrtAfSp-like by Def8, Lm8;
hence ex b1 being non empty ParOrtStr st
( b1 is strict & b1 is OrtAfSp-like ) ; ::_thesis: verum
end;
end;
definition
mode OrtAfSp is non empty OrtAfSp-like ParOrtStr ;
end;
theorem :: ANALMETR:33
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
AMSpace (V,w,y) is OrtAfSp
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds
AMSpace (V,w,y) is OrtAfSp
let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies AMSpace (V,w,y) is OrtAfSp )
set POS = AMSpace (V,w,y);
set X = AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #);
assume A1: Gen w,y ; ::_thesis: AMSpace (V,w,y) is OrtAfSp
then A2: for a, b, c being Element of (AMSpace (V,w,y)) ex x being Element of (AMSpace (V,w,y)) st
( a,b _|_ c,x & c <> x ) by Th27;
AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Af (AMSpace (V,w,y)) ;
then A3: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Lambda (OASpace V) by Th20;
for a, b being Real st (a * w) + (b * y) = 0. V holds
( a = 0 & b = 0 ) by A1, Def1;
then OASpace V is OAffinSpace by ANALOAF:26;
then A4: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) is AffinSpace by A3, DIRAF:41;
( ( for a, b, c, d, p, q, r, s being Element of (AMSpace (V,w,y)) holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) ) & ( for a, b, c being Element of (AMSpace (V,w,y)) st a <> b holds
ex x being Element of (AMSpace (V,w,y)) st
( a,b // a,x & a,b _|_ x,c ) ) ) by A1, Th23, Th24, Th25, Th26, Th29, Th30, Th32;
hence AMSpace (V,w,y) is OrtAfSp by A2, A4, Def8; ::_thesis: verum
end;
consider V0 being RealLinearSpace such that
Lm9: ex w, y being VECTOR of V0 st Gen w,y by Th3;
consider w0, y0 being VECTOR of V0 such that
Lm10: Gen w0,y0 by Lm9;
Lm11: now__::_thesis:_(_AffinStruct(#_the_carrier_of_(AMSpace_(V0,w0,y0)),_the_CONGR_of_(AMSpace_(V0,w0,y0))_#)_is_AffinPlane_&_(_for_a,_b,_c,_d,_p,_q,_r,_s_being_Element_of_(AMSpace_(V0,w0,y0))_holds_
(_(_a,b__|__a,b_implies_a_=_b_)_&_a,b__|__c,c_&_(_a,b__|__c,d_implies_(_a,b__|__d,c_&_c,d__|__a,b_)_)_&_(_a,b__|__p,q_&_a,b_//_r,s_&_not_p,q__|__r,s_implies_a_=_b_)_&_(_a,b__|__p,q_&_a,b__|__r,s_&_not_p,q_//_r,s_implies_a_=_b_)_)_)_&_(_for_a,_b,_c_being_Element_of_(AMSpace_(V0,w0,y0))_ex_x_being_Element_of_(AMSpace_(V0,w0,y0))_st_
(_a,b__|__c,x_&_c_<>_x_)_)_)
set X = AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #);
AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) = Af (AMSpace (V0,w0,y0)) ;
then A1: AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) = Lambda (OASpace V0) by Th20;
( ( for a, b being Real st (a * w0) + (b * y0) = 0. V0 holds
( a = 0 & b = 0 ) ) & ( for w1 being VECTOR of V0 ex a, b being Real st w1 = (a * w0) + (b * y0) ) ) by Def1, Lm10;
then OASpace V0 is OAffinPlane by ANALOAF:28;
hence ( AffinStruct(# the carrier of (AMSpace (V0,w0,y0)), the CONGR of (AMSpace (V0,w0,y0)) #) is AffinPlane & ( for a, b, c, d, p, q, r, s being Element of (AMSpace (V0,w0,y0)) holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of (AMSpace (V0,w0,y0)) ex x being Element of (AMSpace (V0,w0,y0)) st
( a,b _|_ c,x & c <> x ) ) ) by A1, Lm10, Th23, Th24, Th25, Th26, Th27, Th28, Th30, DIRAF:45; ::_thesis: verum
end;
definition
let IT be non empty ParOrtStr ;
attrIT is OrtAfPl-like means :Def9: :: ANALMETR:def 9
( AffinStruct(# the carrier of IT, the CONGR of IT #) is AffinPlane & ( for a, b, c, d, p, q, r, s being Element of IT holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of IT ex x being Element of IT st
( a,b _|_ c,x & c <> x ) ) );
end;
:: deftheorem Def9 defines OrtAfPl-like ANALMETR:def_9_:_
for IT being non empty ParOrtStr holds
( IT is OrtAfPl-like iff ( AffinStruct(# the carrier of IT, the CONGR of IT #) is AffinPlane & ( for a, b, c, d, p, q, r, s being Element of IT holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of IT ex x being Element of IT st
( a,b _|_ c,x & c <> x ) ) ) );
registration
cluster non empty strict OrtAfPl-like for ParOrtStr ;
existence
ex b1 being non empty ParOrtStr st
( b1 is strict & b1 is OrtAfPl-like )
proof
AMSpace (V0,w0,y0) is OrtAfPl-like by Def9, Lm11;
hence ex b1 being non empty ParOrtStr st
( b1 is strict & b1 is OrtAfPl-like ) ; ::_thesis: verum
end;
end;
definition
mode OrtAfPl is non empty OrtAfPl-like ParOrtStr ;
end;
theorem :: ANALMETR:34
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
AMSpace (V,w,y) is OrtAfPl
proof
let V be RealLinearSpace; ::_thesis: for w, y being VECTOR of V st Gen w,y holds
AMSpace (V,w,y) is OrtAfPl
let w, y be VECTOR of V; ::_thesis: ( Gen w,y implies AMSpace (V,w,y) is OrtAfPl )
set POS = AMSpace (V,w,y);
set X = AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #);
AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Af (AMSpace (V,w,y)) ;
then A1: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Lambda (OASpace V) by Th20;
assume A2: Gen w,y ; ::_thesis: AMSpace (V,w,y) is OrtAfPl
then ( ( for a, b being Real st (a * w) + (b * y) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w1 being VECTOR of V ex a, b being Real st w1 = (a * w) + (b * y) ) ) by Def1;
then OASpace V is OAffinPlane by ANALOAF:28;
then A3: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) is AffinPlane by A1, DIRAF:45;
( ( for a, b, c, d, p, q, r, s being Element of (AMSpace (V,w,y)) holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of (AMSpace (V,w,y)) ex x being Element of (AMSpace (V,w,y)) st
( a,b _|_ c,x & c <> x ) ) ) by A2, Th23, Th24, Th25, Th26, Th27, Th28, Th30;
hence AMSpace (V,w,y) is OrtAfPl by A3, Def9; ::_thesis: verum
end;
theorem :: ANALMETR:35
for POS being non empty ParOrtStr
for x being set holds
( x is Element of POS iff x is Element of (Af POS) ) ;
theorem Th36: :: ANALMETR:36
for POS being non empty ParOrtStr
for a, b, c, d being Element of POS
for a9, b9, c9, d9 being Element of (Af POS) st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b // c,d iff a9,b9 // c9,d9 )
proof
let POS be non empty ParOrtStr ; ::_thesis: for a, b, c, d being Element of POS
for a9, b9, c9, d9 being Element of (Af POS) st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b // c,d iff a9,b9 // c9,d9 )
set AF = Af POS;
let a, b, c, d be Element of POS; ::_thesis: for a9, b9, c9, d9 being Element of (Af POS) st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b // c,d iff a9,b9 // c9,d9 )
let a9, b9, c9, d9 be Element of (Af POS); ::_thesis: ( a = a9 & b = b9 & c = c9 & d = d9 implies ( a,b // c,d iff a9,b9 // c9,d9 ) )
assume A1: ( a = a9 & b = b9 & c = c9 & d = d9 ) ; ::_thesis: ( a,b // c,d iff a9,b9 // c9,d9 )
hereby ::_thesis: ( a9,b9 // c9,d9 implies a,b // c,d )
assume a,b // c,d ; ::_thesis: a9,b9 // c9,d9
then [[a9,b9],[c9,d9]] in the CONGR of (Af POS) by A1, ANALOAF:def_2;
hence a9,b9 // c9,d9 by ANALOAF:def_2; ::_thesis: verum
end;
assume a9,b9 // c9,d9 ; ::_thesis: a,b // c,d
then [[a,b],[c,d]] in the CONGR of POS by A1, ANALOAF:def_2;
hence a,b // c,d by ANALOAF:def_2; ::_thesis: verum
end;
registration
let POS be OrtAfSp;
cluster Af POS -> non trivial strict AffinSpace-like ;
correctness
coherence
( Af POS is AffinSpace-like & not Af POS is trivial );
by Def8;
end;
registration
let POS be OrtAfPl;
cluster Af POS -> non trivial strict AffinSpace-like 2-dimensional ;
correctness
coherence
( Af POS is 2-dimensional & Af POS is AffinSpace-like & not Af POS is trivial );
by Def9;
end;
theorem Th37: :: ANALMETR:37
for POS being OrtAfPl holds POS is OrtAfSp
proof
let POS be OrtAfPl; ::_thesis: POS is OrtAfSp
for a, b, c, d, p, q, r, s being Element of POS st a,b _|_ p,q & a,b _|_ p,s holds
a,b _|_ q,s
proof
let a, b, c, d, p, q, r, s be Element of POS; ::_thesis: ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s )
assume that
A1: a,b _|_ p,q and
A2: a,b _|_ p,s ; ::_thesis: a,b _|_ q,s
A3: now__::_thesis:_(_a_<>_b_&_p_<>_q_implies_a,b__|__q,s_)
reconsider p9 = p, q9 = q, s9 = s as Element of (Af POS) ;
assume that
A4: a <> b and
A5: p <> q ; ::_thesis: a,b _|_ q,s
p,q // p,s by A1, A2, A4, Def9;
then p9,q9 // p9,s9 by Th36;
then q9,p9 // q9,s9 by DIRAF:40;
then p9,q9 // q9,s9 by AFF_1:4;
then A6: p,q // q,s by Th36;
p,q _|_ a,b by A1, Def9;
hence a,b _|_ q,s by A5, A6, Def9; ::_thesis: verum
end;
now__::_thesis:_(_a_=_b_implies_a,b__|__q,s_)
assume a = b ; ::_thesis: a,b _|_ q,s
then q,s _|_ a,b by Def9;
hence a,b _|_ q,s by Def9; ::_thesis: verum
end;
hence a,b _|_ q,s by A2, A3; ::_thesis: verum
end;
then A7: for a, b, c, d, p, q, r, s being Element of POS holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) by Def9;
A8: for a, b, c being Element of POS st a <> b holds
ex x being Element of POS st
( a,b // a,x & a,b _|_ x,c )
proof
let a, b, c be Element of POS; ::_thesis: ( a <> b implies ex x being Element of POS st
( a,b // a,x & a,b _|_ x,c ) )
assume A9: a <> b ; ::_thesis: ex x being Element of POS st
( a,b // a,x & a,b _|_ x,c )
consider y being Element of POS such that
A10: a,b _|_ c,y and
A11: c <> y by Def9;
reconsider a9 = a, b9 = b, c9 = c, y9 = y as Element of (Af POS) ;
not a9,b9 // c9,y9
proof
assume a9,b9 // c9,y9 ; ::_thesis: contradiction
then a,b // c,y by Th36;
then c,y _|_ c,y by A9, A10, Def9;
hence contradiction by A11, Def9; ::_thesis: verum
end;
then consider x9 being Element of (Af POS) such that
A12: LIN a9,b9,x9 and
A13: LIN c9,y9,x9 by AFF_1:60;
reconsider x = x9 as Element of POS ;
c9,y9 // c9,x9 by A13, AFF_1:def_1;
then A14: c,y // c,x by Th36;
c,y _|_ a,b by A10, Def9;
then a,b _|_ c,x by A11, A14, Def9;
then A15: a,b _|_ x,c by Def9;
a9,b9 // a9,x9 by A12, AFF_1:def_1;
then a,b // a,x by Th36;
hence ex x being Element of POS st
( a,b // a,x & a,b _|_ x,c ) by A15; ::_thesis: verum
end;
( Af POS = AffinStruct(# the carrier of POS, the CONGR of POS #) & ( for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x ) ) ) by Def9;
hence POS is OrtAfSp by A8, A7, Def8; ::_thesis: verum
end;
registration
cluster non empty OrtAfPl-like -> non empty OrtAfSp-like for ParOrtStr ;
coherence
for b1 being non empty ParOrtStr st b1 is OrtAfPl-like holds
b1 is OrtAfSp-like by Th37;
end;
theorem :: ANALMETR:38
for POS being OrtAfSp st Af POS is AffinPlane holds
POS is OrtAfPl
proof
let POS be OrtAfSp; ::_thesis: ( Af POS is AffinPlane implies POS is OrtAfPl )
assume A1: Af POS is AffinPlane ; ::_thesis: POS is OrtAfPl
A2: now__::_thesis:_for_a,_b,_c,_d,_p,_q,_r,_s_being_Element_of_POS_holds_
(_(_a,b__|__a,b_implies_a_=_b_)_&_a,b__|__c,c_&_(_a,b__|__c,d_implies_(_a,b__|__d,c_&_c,d__|__a,b_)_)_&_(_a,b__|__p,q_&_a,b_//_r,s_&_not_p,q__|__r,s_implies_a_=_b_)_&_(_a,b__|__p,q_&_a,b__|__r,s_&_not_p,q_//_r,s_implies_a_=_b_)_)
let a, b, c, d, p, q, r, s be Element of POS; ::_thesis: ( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) )
thus ( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) ) by Def8; ::_thesis: ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b )
thus ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ::_thesis: verum
proof
reconsider a9 = a, b9 = b, p9 = p, q9 = q, r9 = r, s9 = s as Element of (Af POS) ;
assume that
A3: a,b _|_ p,q and
A4: a,b _|_ r,s ; ::_thesis: ( p,q // r,s or a = b )
A5: p,q _|_ a,b by A3, Def8;
A6: r,s _|_ a,b by A4, Def8;
assume A7: ( not p,q // r,s & not a = b ) ; ::_thesis: contradiction
then A8: not p9,q9 // r9,s9 by Th36;
then A9: p9 <> q9 by AFF_1:3;
consider x9 being Element of (Af POS) such that
A10: LIN p9,q9,x9 and
A11: LIN r9,s9,x9 by A1, A8, AFF_1:60;
reconsider x = x9 as Element of POS ;
A12: r9 <> s9 by A8, AFF_1:3;
LIN s9,r9,x9 by A11, AFF_1:6;
then s9,r9 // s9,x9 by AFF_1:def_1;
then A13: r9,s9 // x9,s9 by AFF_1:4;
then r,s // x,s by Th36;
then a,b _|_ x,s by A12, A6, Def8;
then A14: x,s _|_ a,b by Def8;
LIN q9,p9,x9 by A10, AFF_1:6;
then q9,p9 // q9,x9 by AFF_1:def_1;
then p9,q9 // x9,q9 by AFF_1:4;
then p,q // x,q by Th36;
then A15: a,b _|_ x,q by A9, A5, Def8;
A16: now__::_thesis:_(_x_<>_q_implies_not_x_<>_s_)
consider y9 being Element of (Af POS) such that
A17: ( a9,b9 // q9,y9 & q9 <> y9 ) by DIRAF:40;
assume that
A18: x <> q and
A19: x <> s ; ::_thesis: contradiction
not q9,y9 // x9,s9
proof
assume q9,y9 // x9,s9 ; ::_thesis: contradiction
then q9,y9 // r9,s9 by A13, A19, AFF_1:5;
then r9,s9 // a9,b9 by A17, AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12, A6, Def8;
hence contradiction by A7, Def8; ::_thesis: verum
end;
then consider z9 being Element of (Af POS) such that
A20: LIN q9,y9,z9 and
A21: LIN x9,s9,z9 by A1, AFF_1:60;
reconsider z = z9 as Element of POS ;
q9,y9 // q9,z9 by A20, AFF_1:def_1;
then a9,b9 // q9,z9 by A17, AFF_1:5;
then A22: a,b // q,z by Th36;
A23: x9,s9 // x9,z9 by A21, AFF_1:def_1;
then x,s // x,z by Th36;
then a,b _|_ x,z by A14, A19, Def8;
then a,b _|_ q,z by A15, Def8;
then q,z _|_ q,z by A7, A22, Def8;
then x9,s9 // x9,q9 by A23, Def8;
then A24: LIN x9,s9,q9 by AFF_1:def_1;
( LIN x9,s9,x9 & LIN x9,q9,p9 ) by A10, AFF_1:6, AFF_1:7;
then LIN x9,s9,p9 by A18, A24, AFF_1:11;
then x9,s9 // p9,q9 by A24, AFF_1:10;
then p9,q9 // r9,s9 by A13, A19, AFF_1:5;
hence contradiction by A7, Th36; ::_thesis: verum
end;
r9,s9 // r9,x9 by A11, AFF_1:def_1;
then A25: r9,s9 // x9,r9 by AFF_1:4;
then r,s // x,r by Th36;
then a,b _|_ x,r by A12, A6, Def8;
then A26: x,r _|_ a,b by Def8;
A27: now__::_thesis:_(_x_<>_q_implies_not_x_<>_r_)
consider y9 being Element of (Af POS) such that
A28: ( a9,b9 // q9,y9 & q9 <> y9 ) by DIRAF:40;
assume that
A29: x <> q and
A30: x <> r ; ::_thesis: contradiction
not q9,y9 // x9,r9
proof
assume q9,y9 // x9,r9 ; ::_thesis: contradiction
then q9,y9 // r9,s9 by A25, A30, AFF_1:5;
then r9,s9 // a9,b9 by A28, AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12, A6, Def8;
hence contradiction by A7, Def8; ::_thesis: verum
end;
then consider z9 being Element of (Af POS) such that
A31: LIN q9,y9,z9 and
A32: LIN x9,r9,z9 by A1, AFF_1:60;
reconsider z = z9 as Element of POS ;
q9,y9 // q9,z9 by A31, AFF_1:def_1;
then a9,b9 // q9,z9 by A28, AFF_1:5;
then A33: a,b // q,z by Th36;
A34: x9,r9 // x9,z9 by A32, AFF_1:def_1;
then x,r // x,z by Th36;
then a,b _|_ x,z by A26, A30, Def8;
then a,b _|_ q,z by A15, Def8;
then q,z _|_ q,z by A7, A33, Def8;
then x9,r9 // x9,q9 by A34, Def8;
then A35: LIN x9,r9,q9 by AFF_1:def_1;
( LIN x9,r9,x9 & LIN x9,q9,p9 ) by A10, AFF_1:6, AFF_1:7;
then LIN x9,r9,p9 by A29, A35, AFF_1:11;
then x9,r9 // p9,q9 by A35, AFF_1:10;
then p9,q9 // r9,s9 by A25, A30, AFF_1:5;
hence contradiction by A7, Th36; ::_thesis: verum
end;
p9,q9 // p9,x9 by A10, AFF_1:def_1;
then p9,q9 // x9,p9 by AFF_1:4;
then p,q // x,p by Th36;
then A36: a,b _|_ x,p by A9, A5, Def8;
A37: now__::_thesis:_(_x_<>_p_implies_not_x_<>_s_)
consider y9 being Element of (Af POS) such that
A38: ( a9,b9 // p9,y9 & p9 <> y9 ) by DIRAF:40;
assume that
A39: x <> p and
A40: x <> s ; ::_thesis: contradiction
not p9,y9 // x9,s9
proof
assume p9,y9 // x9,s9 ; ::_thesis: contradiction
then p9,y9 // r9,s9 by A13, A40, AFF_1:5;
then r9,s9 // a9,b9 by A38, AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12, A6, Def8;
hence contradiction by A7, Def8; ::_thesis: verum
end;
then consider z9 being Element of (Af POS) such that
A41: LIN p9,y9,z9 and
A42: LIN x9,s9,z9 by A1, AFF_1:60;
reconsider z = z9 as Element of POS ;
p9,y9 // p9,z9 by A41, AFF_1:def_1;
then a9,b9 // p9,z9 by A38, AFF_1:5;
then A43: a,b // p,z by Th36;
A44: x9,s9 // x9,z9 by A42, AFF_1:def_1;
then x,s // x,z by Th36;
then a,b _|_ x,z by A14, A40, Def8;
then a,b _|_ p,z by A36, Def8;
then p,z _|_ p,z by A7, A43, Def8;
then x9,s9 // x9,p9 by A44, Def8;
then A45: LIN x9,s9,p9 by AFF_1:def_1;
( LIN x9,s9,x9 & LIN x9,p9,q9 ) by A10, AFF_1:6, AFF_1:7;
then LIN x9,s9,q9 by A39, A45, AFF_1:11;
then x9,s9 // p9,q9 by A45, AFF_1:10;
then p9,q9 // r9,s9 by A13, A40, AFF_1:5;
hence contradiction by A7, Th36; ::_thesis: verum
end;
now__::_thesis:_(_x_<>_p_implies_not_x_<>_r_)
consider y9 being Element of (Af POS) such that
A46: ( a9,b9 // p9,y9 & p9 <> y9 ) by DIRAF:40;
assume that
A47: x <> p and
A48: x <> r ; ::_thesis: contradiction
not p9,y9 // x9,r9
proof
assume p9,y9 // x9,r9 ; ::_thesis: contradiction
then p9,y9 // r9,s9 by A25, A48, AFF_1:5;
then r9,s9 // a9,b9 by A46, AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12, A6, Def8;
hence contradiction by A7, Def8; ::_thesis: verum
end;
then consider z9 being Element of (Af POS) such that
A49: LIN p9,y9,z9 and
A50: LIN x9,r9,z9 by A1, AFF_1:60;
reconsider z = z9 as Element of POS ;
p9,y9 // p9,z9 by A49, AFF_1:def_1;
then a9,b9 // p9,z9 by A46, AFF_1:5;
then A51: a,b // p,z by Th36;
A52: x9,r9 // x9,z9 by A50, AFF_1:def_1;
then x,r // x,z by Th36;
then a,b _|_ x,z by A26, A48, Def8;
then a,b _|_ p,z by A36, Def8;
then p,z _|_ p,z by A7, A51, Def8;
then x9,r9 // x9,p9 by A52, Def8;
then A53: LIN x9,r9,p9 by AFF_1:def_1;
( LIN x9,r9,x9 & LIN x9,p9,q9 ) by A10, AFF_1:6, AFF_1:7;
then LIN x9,r9,q9 by A47, A53, AFF_1:11;
then x9,r9 // p9,q9 by A53, AFF_1:10;
then p9,q9 // r9,s9 by A25, A48, AFF_1:5;
hence contradiction by A7, Th36; ::_thesis: verum
end;
hence contradiction by A8, A37, A27, A16, AFF_1:3; ::_thesis: verum
end;
end;
for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x ) by Def8;
hence POS is OrtAfPl by A1, A2, Def9; ::_thesis: verum
end;
theorem :: ANALMETR:39
for POS being non empty ParOrtStr holds
( POS is OrtAfPl-like iff ( ex a, b being Element of POS st a <> b & ( for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) ) ) ) )
proof
let POS be non empty ParOrtStr ; ::_thesis: ( POS is OrtAfPl-like iff ( ex a, b being Element of POS st a <> b & ( for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) ) ) ) )
set P = Af POS;
hereby ::_thesis: ( ex a, b being Element of POS st a <> b & ( for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) ) ) implies POS is OrtAfPl-like )
assume A1: POS is OrtAfPl-like ; ::_thesis: ( ex x, y being Element of POS st x <> y & ( for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) ) ) )
then Af POS is AffinPlane ;
hence ex x, y being Element of POS st x <> y by DIRAF:46; ::_thesis: for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
let a, b, c, d, p, q, r, s be Element of POS; ::_thesis: ( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p, q9 = q, r9 = r, s9 = s as Element of (Af POS) ;
consider x9 being Element of (Af POS) such that
A2: ( a9,b9 // c9,x9 & a9,c9 // b9,x9 ) by A1, DIRAF:46;
( a9,b9 // b9,a9 & a9,b9 // c9,c9 ) by A1, DIRAF:46;
hence ( a,b // b,a & a,b // c,c ) by Th36; ::_thesis: ( ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
hereby ::_thesis: ( ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
assume ( a,b // p,q & a,b // r,s ) ; ::_thesis: ( p,q // r,s or a = b )
then ( a9,b9 // p9,q9 & a9,b9 // r9,s9 ) by Th36;
then ( p9,q9 // r9,s9 or a9 = b9 ) by A1, DIRAF:46;
hence ( p,q // r,s or a = b ) by Th36; ::_thesis: verum
end;
hereby ::_thesis: ( ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
assume a,b // a,c ; ::_thesis: b,a // b,c
then a9,b9 // a9,c9 by Th36;
then b9,a9 // b9,c9 by A1, DIRAF:46;
hence b,a // b,c by Th36; ::_thesis: verum
end;
reconsider x = x9 as Element of POS ;
consider x9, y9, z9 being Element of (Af POS) such that
A3: not x9,y9 // x9,z9 by A1, DIRAF:46;
( a,b // c,x & a,c // b,x ) by A2, Th36;
hence ex x being Element of POS st
( a,b // c,x & a,c // b,x ) ; ::_thesis: ( not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
reconsider x = x9, y = y9, z = z9 as Element of POS ;
consider x9 being Element of (Af POS) such that
A4: a9,b9 // c9,x9 and
A5: c9 <> x9 by A1, DIRAF:46;
not x,y // x,z by A3, Th36;
hence not for x, y, z being Element of POS holds x,y // x,z ; ::_thesis: ( ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
reconsider x = x9 as Element of POS ;
a,b // c,x by A4, Th36;
hence ex x being Element of POS st
( a,b // c,x & c <> x ) by A5; ::_thesis: ( ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
hereby ::_thesis: ( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
assume that
A6: a,b // b,d and
A7: b <> a ; ::_thesis: ex x being Element of POS st
( c,b // b,x & c,a // d,x )
a9,b9 // b9,d9 by A6, Th36;
then consider x9 being Element of (Af POS) such that
A8: ( c9,b9 // b9,x9 & c9,a9 // d9,x9 ) by A1, A7, DIRAF:46;
reconsider x = x9 as Element of POS ;
( c,b // b,x & c,a // d,x ) by A8, Th36;
hence ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ; ::_thesis: verum
end;
thus ( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) ) by A1, Def9; ::_thesis: ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) )
assume not a,b // c,d ; ::_thesis: ex x being Element of POS st
( a,b // a,x & c,d // c,x )
then not a9,b9 // c9,d9 by Th36;
then consider x9 being Element of (Af POS) such that
A9: ( a9,b9 // a9,x9 & c9,d9 // c9,x9 ) by A1, DIRAF:46;
reconsider x = x9 as Element of POS ;
( a,b // a,x & c,d // c,x ) by A9, Th36;
hence ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ; ::_thesis: verum
end;
given a, b being Element of POS such that A10: a <> b ; ::_thesis: ( ex a, b, c, d, p, q, r, s being Element of POS st
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) implies ( not a,b // c,d & ( for x being Element of POS holds
( not a,b // a,x or not c,d // c,x ) ) ) ) or POS is OrtAfPl-like )
assume A11: for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) ) ; ::_thesis: POS is OrtAfPl-like
A12: now__::_thesis:_for_x,_y,_z_being_Element_of_(Af_POS)_ex_t_being_Element_of_(Af_POS)_st_
(_x,z_//_y,t_&_y_<>_t_)
let x, y, z be Element of (Af POS); ::_thesis: ex t being Element of (Af POS) st
( x,z // y,t & y <> t )
reconsider x9 = x, y9 = y, z9 = z as Element of POS ;
consider t9 being Element of POS such that
A13: x9,z9 // y9,t9 and
A14: y9 <> t9 by A11;
reconsider t = t9 as Element of (Af POS) ;
x,z // y,t by A13, Th36;
hence ex t being Element of (Af POS) st
( x,z // y,t & y <> t ) by A14; ::_thesis: verum
end;
A15: now__::_thesis:_for_x,_y,_z,_t,_u,_w_being_Element_of_(Af_POS)_holds_
(_x,y_//_y,x_&_x,y_//_z,z_&_(_x_<>_y_&_x,y_//_z,t_&_x,y_//_u,w_implies_z,t_//_u,w_)_&_(_x,y_//_x,z_implies_y,x_//_y,z_)_)
let x, y, z, t, u, w be Element of (Af POS); ::_thesis: ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) )
reconsider a = x, b = y, c = z, d = t, e = u, f = w as Element of POS ;
( a,b // b,a & a,b // c,c ) by A11;
hence ( x,y // y,x & x,y // z,z ) by Th36; ::_thesis: ( ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) )
thus ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) ::_thesis: ( x,y // x,z implies y,x // y,z )
proof
assume that
A16: x <> y and
A17: ( x,y // z,t & x,y // u,w ) ; ::_thesis: z,t // u,w
( a,b // c,d & a,b // e,f ) by A17, Th36;
then c,d // e,f by A11, A16;
hence z,t // u,w by Th36; ::_thesis: verum
end;
thus ( x,y // x,z implies y,x // y,z ) ::_thesis: verum
proof
assume x,y // x,z ; ::_thesis: y,x // y,z
then a,b // a,c by Th36;
then b,a // b,c by A11;
hence y,x // y,z by Th36; ::_thesis: verum
end;
end;
A18: now__::_thesis:_for_x,_y,_z,_t_being_Element_of_(Af_POS)_st_not_x,y_//_z,t_holds_
ex_u_being_Element_of_(Af_POS)_st_
(_x,y_//_x,u_&_z,t_//_z,u_)
let x, y, z, t be Element of (Af POS); ::_thesis: ( not x,y // z,t implies ex u being Element of (Af POS) st
( x,y // x,u & z,t // z,u ) )
assume A19: not x,y // z,t ; ::_thesis: ex u being Element of (Af POS) st
( x,y // x,u & z,t // z,u )
reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of POS ;
not x9,y9 // z9,t9 by A19, Th36;
then consider u9 being Element of POS such that
A20: ( x9,y9 // x9,u9 & z9,t9 // z9,u9 ) by A11;
reconsider u = u9 as Element of (Af POS) ;
( x,y // x,u & z,t // z,u ) by A20, Th36;
hence ex u being Element of (Af POS) st
( x,y // x,u & z,t // z,u ) ; ::_thesis: verum
end;
A21: now__::_thesis:_for_x,_y,_z,_t_being_Element_of_(Af_POS)_st_z,x_//_x,t_&_x_<>_z_holds_
ex_u_being_Element_of_(Af_POS)_st_
(_y,x_//_x,u_&_y,z_//_t,u_)
let x, y, z, t be Element of (Af POS); ::_thesis: ( z,x // x,t & x <> z implies ex u being Element of (Af POS) st
( y,x // x,u & y,z // t,u ) )
assume that
A22: z,x // x,t and
A23: x <> z ; ::_thesis: ex u being Element of (Af POS) st
( y,x // x,u & y,z // t,u )
reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of POS ;
z9,x9 // x9,t9 by A22, Th36;
then consider u9 being Element of POS such that
A24: ( y9,x9 // x9,u9 & y9,z9 // t9,u9 ) by A11, A23;
reconsider u = u9 as Element of (Af POS) ;
( y,x // x,u & y,z // t,u ) by A24, Th36;
hence ex u being Element of (Af POS) st
( y,x // x,u & y,z // t,u ) ; ::_thesis: verum
end;
A25: now__::_thesis:_for_x,_y,_z_being_Element_of_(Af_POS)_ex_t_being_Element_of_(Af_POS)_st_
(_x,y_//_z,t_&_x,z_//_y,t_)
let x, y, z be Element of (Af POS); ::_thesis: ex t being Element of (Af POS) st
( x,y // z,t & x,z // y,t )
reconsider x9 = x, y9 = y, z9 = z as Element of POS ;
consider t9 being Element of POS such that
A26: ( x9,y9 // z9,t9 & x9,z9 // y9,t9 ) by A11;
reconsider t = t9 as Element of (Af POS) ;
( x,y // z,t & x,z // y,t ) by A26, Th36;
hence ex t being Element of (Af POS) st
( x,y // z,t & x,z // y,t ) ; ::_thesis: verum
end;
not for x, y, z being Element of (Af POS) holds x,y // x,z
proof
consider x, y, z being Element of POS such that
A27: not x,y // x,z by A11;
reconsider x9 = x, y9 = y, z9 = z as Element of (Af POS) ;
not x9,y9 // x9,z9 by A27, Th36;
hence not for x, y, z being Element of (Af POS) holds x,y // x,z ; ::_thesis: verum
end;
hence AffinStruct(# the carrier of POS, the CONGR of POS #) is AffinPlane by A10, A15, A12, A25, A21, A18, DIRAF:46; :: according to ANALMETR:def_9 ::_thesis: ( ( for a, b, c, d, p, q, r, s being Element of POS holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x ) ) )
thus for a, b, c, d, p, q, r, s being Element of POS holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) by A11; ::_thesis: for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x )
thus for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x ) by A11; ::_thesis: verum
end;
definition
let POS be non empty ParOrtStr ;
let a, b, c be Element of POS;
pred LIN a,b,c means :Def10: :: ANALMETR:def 10
a,b // a,c;
end;
:: deftheorem Def10 defines LIN ANALMETR:def_10_:_
for POS being non empty ParOrtStr
for a, b, c being Element of POS holds
( LIN a,b,c iff a,b // a,c );
definition
let POS be non empty ParOrtStr ;
let a, b be Element of POS;
func Line (a,b) -> Subset of POS means :Def11: :: ANALMETR:def 11
for x being Element of POS holds
( x in it iff LIN a,b,x );
existence
ex b1 being Subset of POS st
for x being Element of POS holds
( x in b1 iff LIN a,b,x )
proof
defpred S1[ set ] means for y being Element of POS st y = $1 holds
LIN a,b,y;
consider X being Subset of POS such that
A1: for x being set holds
( x in X iff ( x in the carrier of POS & S1[x] ) ) from SUBSET_1:sch_1();
take X ; ::_thesis: for x being Element of POS holds
( x in X iff LIN a,b,x )
let x be Element of POS; ::_thesis: ( x in X iff LIN a,b,x )
thus ( x in X implies LIN a,b,x ) by A1; ::_thesis: ( LIN a,b,x implies x in X )
assume LIN a,b,x ; ::_thesis: x in X
then for y being Element of POS st y = x holds
LIN a,b,y ;
hence x in X by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of POS st ( for x being Element of POS holds
( x in b1 iff LIN a,b,x ) ) & ( for x being Element of POS holds
( x in b2 iff LIN a,b,x ) ) holds
b1 = b2
proof
let X1, X2 be Subset of POS; ::_thesis: ( ( for x being Element of POS holds
( x in X1 iff LIN a,b,x ) ) & ( for x being Element of POS holds
( x in X2 iff LIN a,b,x ) ) implies X1 = X2 )
assume that
A2: for x being Element of POS holds
( x in X1 iff LIN a,b,x ) and
A3: for x being Element of POS holds
( x in X2 iff LIN a,b,x ) ; ::_thesis: X1 = X2
for x being set holds
( x in X1 iff x in X2 )
proof
let x be set ; ::_thesis: ( x in X1 iff x in X2 )
thus ( x in X1 implies x in X2 ) ::_thesis: ( x in X2 implies x in X1 )
proof
assume A4: x in X1 ; ::_thesis: x in X2
then reconsider x9 = x as Element of POS ;
LIN a,b,x9 by A2, A4;
hence x in X2 by A3; ::_thesis: verum
end;
assume A5: x in X2 ; ::_thesis: x in X1
then reconsider x9 = x as Element of POS ;
LIN a,b,x9 by A3, A5;
hence x in X1 by A2; ::_thesis: verum
end;
hence X1 = X2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines Line ANALMETR:def_11_:_
for POS being non empty ParOrtStr
for a, b being Element of POS
for b4 being Subset of POS holds
( b4 = Line (a,b) iff for x being Element of POS holds
( x in b4 iff LIN a,b,x ) );
definition
let POS be non empty ParOrtStr ;
let A be Subset of POS;
attrA is being_line means :Def12: :: ANALMETR:def 12
ex a, b being Element of POS st
( a <> b & A = Line (a,b) );
end;
:: deftheorem Def12 defines being_line ANALMETR:def_12_:_
for POS being non empty ParOrtStr
for A being Subset of POS holds
( A is being_line iff ex a, b being Element of POS st
( a <> b & A = Line (a,b) ) );
theorem Th40: :: ANALMETR:40
for POS being OrtAfSp
for a, b, c being Element of POS
for a9, b9, c9 being Element of (Af POS) st a = a9 & b = b9 & c = c9 holds
( LIN a,b,c iff LIN a9,b9,c9 )
proof
let POS be OrtAfSp; ::_thesis: for a, b, c being Element of POS
for a9, b9, c9 being Element of (Af POS) st a = a9 & b = b9 & c = c9 holds
( LIN a,b,c iff LIN a9,b9,c9 )
let a, b, c be Element of POS; ::_thesis: for a9, b9, c9 being Element of (Af POS) st a = a9 & b = b9 & c = c9 holds
( LIN a,b,c iff LIN a9,b9,c9 )
let a9, b9, c9 be Element of (Af POS); ::_thesis: ( a = a9 & b = b9 & c = c9 implies ( LIN a,b,c iff LIN a9,b9,c9 ) )
assume A1: ( a = a9 & b = b9 & c = c9 ) ; ::_thesis: ( LIN a,b,c iff LIN a9,b9,c9 )
hereby ::_thesis: ( LIN a9,b9,c9 implies LIN a,b,c )
assume LIN a,b,c ; ::_thesis: LIN a9,b9,c9
then a,b // a,c by Def10;
then a9,b9 // a9,c9 by A1, Th36;
hence LIN a9,b9,c9 by AFF_1:def_1; ::_thesis: verum
end;
assume LIN a9,b9,c9 ; ::_thesis: LIN a,b,c
then a9,b9 // a9,c9 by AFF_1:def_1;
then a,b // a,c by A1, Th36;
hence LIN a,b,c by Def10; ::_thesis: verum
end;
theorem Th41: :: ANALMETR:41
for POS being OrtAfSp
for a, b being Element of POS
for a9, b9 being Element of (Af POS) st a = a9 & b = b9 holds
Line (a,b) = Line (a9,b9)
proof
let POS be OrtAfSp; ::_thesis: for a, b being Element of POS
for a9, b9 being Element of (Af POS) st a = a9 & b = b9 holds
Line (a,b) = Line (a9,b9)
let a, b be Element of POS; ::_thesis: for a9, b9 being Element of (Af POS) st a = a9 & b = b9 holds
Line (a,b) = Line (a9,b9)
let a9, b9 be Element of (Af POS); ::_thesis: ( a = a9 & b = b9 implies Line (a,b) = Line (a9,b9) )
assume A1: ( a = a9 & b = b9 ) ; ::_thesis: Line (a,b) = Line (a9,b9)
set X = Line (a,b);
set Y = Line (a9,b9);
now__::_thesis:_for_x1_being_set_holds_
(_x1_in_Line_(a,b)_iff_x1_in_Line_(a9,b9)_)
let x1 be set ; ::_thesis: ( x1 in Line (a,b) iff x1 in Line (a9,b9) )
A2: now__::_thesis:_(_x1_in_Line_(a9,b9)_implies_x1_in_Line_(a,b)_)
assume A3: x1 in Line (a9,b9) ; ::_thesis: x1 in Line (a,b)
then reconsider x9 = x1 as Element of (Af POS) ;
reconsider x = x9 as Element of POS ;
LIN a9,b9,x9 by A3, AFF_1:def_2;
then LIN a,b,x by A1, Th40;
hence x1 in Line (a,b) by Def11; ::_thesis: verum
end;
now__::_thesis:_(_x1_in_Line_(a,b)_implies_x1_in_Line_(a9,b9)_)
assume A4: x1 in Line (a,b) ; ::_thesis: x1 in Line (a9,b9)
then reconsider x = x1 as Element of POS ;
reconsider x9 = x as Element of (Af POS) ;
LIN a,b,x by A4, Def11;
then LIN a9,b9,x9 by A1, Th40;
hence x1 in Line (a9,b9) by AFF_1:def_2; ::_thesis: verum
end;
hence ( x1 in Line (a,b) iff x1 in Line (a9,b9) ) by A2; ::_thesis: verum
end;
hence Line (a,b) = Line (a9,b9) by TARSKI:1; ::_thesis: verum
end;
theorem :: ANALMETR:42
for POS being non empty ParOrtStr
for X being set holds
( X is Subset of POS iff X is Subset of (Af POS) ) ;
theorem Th43: :: ANALMETR:43
for POS being OrtAfSp
for X being Subset of POS
for Y being Subset of (Af POS) st X = Y holds
( X is being_line iff Y is being_line )
proof
let POS be OrtAfSp; ::_thesis: for X being Subset of POS
for Y being Subset of (Af POS) st X = Y holds
( X is being_line iff Y is being_line )
let X be Subset of the carrier of POS; ::_thesis: for Y being Subset of (Af POS) st X = Y holds
( X is being_line iff Y is being_line )
let Y be Subset of (Af POS); ::_thesis: ( X = Y implies ( X is being_line iff Y is being_line ) )
assume A1: X = Y ; ::_thesis: ( X is being_line iff Y is being_line )
hereby ::_thesis: ( Y is being_line implies X is being_line )
assume X is being_line ; ::_thesis: Y is being_line
then consider a, b being Element of POS such that
A2: a <> b and
A3: X = Line (a,b) by Def12;
reconsider a9 = a, b9 = b as Element of (Af POS) ;
Y = Line (a9,b9) by A1, A3, Th41;
hence Y is being_line by A2, AFF_1:def_3; ::_thesis: verum
end;
assume Y is being_line ; ::_thesis: X is being_line
then consider a9, b9 being Element of (Af POS) such that
A4: a9 <> b9 and
A5: Y = Line (a9,b9) by AFF_1:def_3;
reconsider a = a9, b = b9 as Element of POS ;
X = Line (a,b) by A1, A5, Th41;
hence X is being_line by A4, Def12; ::_thesis: verum
end;
definition
let POS be non empty ParOrtStr ;
let a, b be Element of POS;
let K be Subset of POS;
preda,b _|_ K means :Def13: :: ANALMETR:def 13
ex p, q being Element of POS st
( p <> q & K = Line (p,q) & a,b _|_ p,q );
end;
:: deftheorem Def13 defines _|_ ANALMETR:def_13_:_
for POS being non empty ParOrtStr
for a, b being Element of POS
for K being Subset of POS holds
( a,b _|_ K iff ex p, q being Element of POS st
( p <> q & K = Line (p,q) & a,b _|_ p,q ) );
definition
let POS be non empty ParOrtStr ;
let K, M be Subset of POS;
predK _|_ M means :Def14: :: ANALMETR:def 14
ex p, q being Element of POS st
( p <> q & K = Line (p,q) & p,q _|_ M );
end;
:: deftheorem Def14 defines _|_ ANALMETR:def_14_:_
for POS being non empty ParOrtStr
for K, M being Subset of POS holds
( K _|_ M iff ex p, q being Element of POS st
( p <> q & K = Line (p,q) & p,q _|_ M ) );
definition
let POS be non empty ParOrtStr ;
let K, M be Subset of POS;
predK // M means :Def15: :: ANALMETR:def 15
ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b // c,d );
end;
:: deftheorem Def15 defines // ANALMETR:def_15_:_
for POS being non empty ParOrtStr
for K, M being Subset of POS holds
( K // M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b // c,d ) );
theorem Th44: :: ANALMETR:44
for POS being non empty ParOrtStr
for a, b being Element of POS
for K, M being Subset of POS holds
( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) )
proof
let POS be non empty ParOrtStr ; ::_thesis: for a, b being Element of POS
for K, M being Subset of POS holds
( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) )
let a, b be Element of POS; ::_thesis: for K, M being Subset of POS holds
( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) )
let K, M be Subset of POS; ::_thesis: ( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) )
A1: now__::_thesis:_for_a,_b_being_Element_of_POS
for_K_being_Subset_of_POS_st_a,b__|__K_holds_
K_is_being_line
let a, b be Element of POS; ::_thesis: for K being Subset of POS st a,b _|_ K holds
K is being_line
let K be Subset of POS; ::_thesis: ( a,b _|_ K implies K is being_line )
assume a,b _|_ K ; ::_thesis: K is being_line
then ex p, q being Element of POS st
( p <> q & K = Line (p,q) & a,b _|_ p,q ) by Def13;
hence K is being_line by Def12; ::_thesis: verum
end;
now__::_thesis:_(_K__|__M_implies_(_K_is_being_line_&_M_is_being_line_)_)
assume K _|_ M ; ::_thesis: ( K is being_line & M is being_line )
then A2: ex p, q being Element of POS st
( p <> q & K = Line (p,q) & p,q _|_ M ) by Def14;
hence K is being_line by Def12; ::_thesis: M is being_line
thus M is being_line by A1, A2; ::_thesis: verum
end;
hence ( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) ) by A1; ::_thesis: verum
end;
theorem Th45: :: ANALMETR:45
for POS being non empty ParOrtStr
for K, M being Subset of POS holds
( K _|_ M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d ) )
proof
let POS be non empty ParOrtStr ; ::_thesis: for K, M being Subset of POS holds
( K _|_ M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d ) )
let K, M be Subset of POS; ::_thesis: ( K _|_ M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d ) )
hereby ::_thesis: ( ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d ) implies K _|_ M )
assume K _|_ M ; ::_thesis: ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d )
then consider a, b being Element of POS such that
A1: ( a <> b & K = Line (a,b) ) and
A2: a,b _|_ M by Def14;
ex c, d being Element of POS st
( c <> d & M = Line (c,d) & a,b _|_ c,d ) by A2, Def13;
hence ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b _|_ c,d ) by A1; ::_thesis: verum
end;
given a, b, c, d being Element of POS such that A3: a <> b and
A4: c <> d and
A5: K = Line (a,b) and
A6: ( M = Line (c,d) & a,b _|_ c,d ) ; ::_thesis: K _|_ M
a,b _|_ M by A4, A6, Def13;
hence K _|_ M by A3, A5, Def14; ::_thesis: verum
end;
theorem Th46: :: ANALMETR:46
for POS being OrtAfSp
for M, N being Subset of POS
for M9, N9 being Subset of (Af POS) st M = M9 & N = N9 holds
( M // N iff M9 // N9 )
proof
let POS be OrtAfSp; ::_thesis: for M, N being Subset of POS
for M9, N9 being Subset of (Af POS) st M = M9 & N = N9 holds
( M // N iff M9 // N9 )
let M, N be Subset of POS; ::_thesis: for M9, N9 being Subset of (Af POS) st M = M9 & N = N9 holds
( M // N iff M9 // N9 )
let M9, N9 be Subset of (Af POS); ::_thesis: ( M = M9 & N = N9 implies ( M // N iff M9 // N9 ) )
assume A1: ( M = M9 & N = N9 ) ; ::_thesis: ( M // N iff M9 // N9 )
hereby ::_thesis: ( M9 // N9 implies M // N )
assume M // N ; ::_thesis: M9 // N9
then consider a, b, c, d being Element of POS such that
A2: ( a <> b & c <> d ) and
A3: ( M = Line (a,b) & N = Line (c,d) ) and
A4: a,b // c,d by Def15;
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ;
A5: a9,b9 // c9,d9 by A4, Th36;
( M9 = Line (a9,b9) & N9 = Line (c9,d9) ) by A1, A3, Th41;
hence M9 // N9 by A2, A5, AFF_1:37; ::_thesis: verum
end;
assume M9 // N9 ; ::_thesis: M // N
then consider a9, b9, c9, d9 being Element of (Af POS) such that
A6: ( a9 <> b9 & c9 <> d9 ) and
A7: a9,b9 // c9,d9 and
A8: ( M9 = Line (a9,b9) & N9 = Line (c9,d9) ) by AFF_1:37;
reconsider a = a9, b = b9, c = c9, d = d9 as Element of POS ;
A9: a,b // c,d by A7, Th36;
( M = Line (a,b) & N = Line (c,d) ) by A1, A8, Th41;
hence M // N by A6, A9, Def15; ::_thesis: verum
end;
theorem :: ANALMETR:47
for POS being OrtAfSp
for K being Subset of POS
for a being Element of POS st K is being_line holds
a,a _|_ K
proof
let POS be OrtAfSp; ::_thesis: for K being Subset of POS
for a being Element of POS st K is being_line holds
a,a _|_ K
let K be Subset of POS; ::_thesis: for a being Element of POS st K is being_line holds
a,a _|_ K
let a be Element of POS; ::_thesis: ( K is being_line implies a,a _|_ K )
assume K is being_line ; ::_thesis: a,a _|_ K
then consider p, q being Element of POS such that
A1: ( p <> q & K = Line (p,q) ) by Def12;
p,q _|_ a,a by Def8;
then a,a _|_ p,q by Def8;
hence a,a _|_ K by A1, Def13; ::_thesis: verum
end;
theorem :: ANALMETR:48
for POS being OrtAfSp
for K being Subset of POS
for a, b, c, d being Element of POS st a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b holds
c,d _|_ K
proof
let POS be OrtAfSp; ::_thesis: for K being Subset of POS
for a, b, c, d being Element of POS st a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b holds
c,d _|_ K
let K be Subset of POS; ::_thesis: for a, b, c, d being Element of POS st a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b holds
c,d _|_ K
let a, b, c, d be Element of POS; ::_thesis: ( a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b implies c,d _|_ K )
assume that
A1: a,b _|_ K and
A2: ( a,b // c,d or c,d // a,b ) and
A3: a <> b ; ::_thesis: c,d _|_ K
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ;
consider p, q being Element of POS such that
A4: ( p <> q & K = Line (p,q) ) and
A5: a,b _|_ p,q by A1, Def13;
( a9,b9 // c9,d9 or c9,d9 // a9,b9 ) by A2, Th36;
then a9,b9 // c9,d9 by AFF_1:4;
then a,b // c,d by Th36;
then p,q _|_ c,d by A3, A5, Def8;
then c,d _|_ p,q by Def8;
hence c,d _|_ K by A4, Def13; ::_thesis: verum
end;
theorem :: ANALMETR:49
for POS being OrtAfSp
for K being Subset of POS
for a, b being Element of POS st a,b _|_ K holds
b,a _|_ K
proof
let POS be OrtAfSp; ::_thesis: for K being Subset of POS
for a, b being Element of POS st a,b _|_ K holds
b,a _|_ K
let K be Subset of POS; ::_thesis: for a, b being Element of POS st a,b _|_ K holds
b,a _|_ K
let a, b be Element of POS; ::_thesis: ( a,b _|_ K implies b,a _|_ K )
assume a,b _|_ K ; ::_thesis: b,a _|_ K
then consider p, q being Element of POS such that
A1: ( p <> q & K = Line (p,q) ) and
A2: a,b _|_ p,q by Def13;
p,q _|_ a,b by A2, Def8;
then p,q _|_ b,a by Def8;
then b,a _|_ p,q by Def8;
hence b,a _|_ K by A1, Def13; ::_thesis: verum
end;
definition
let POS be OrtAfSp;
let K, M be Subset of POS;
:: original: //
redefine predK // M;
symmetry
for K, M being Subset of POS st (POS,b1,b2) holds
(POS,b2,b1)
proof
let K, M be Subset of POS; ::_thesis: ( (POS,K,M) implies (POS,M,K) )
assume K // M ; ::_thesis: (POS,M,K)
then consider a, b, c, d being Element of POS such that
A1: ( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) ) and
A2: a,b // c,d by Def15;
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ;
a9,b9 // c9,d9 by A2, Th36;
then c9,d9 // a9,b9 by AFF_1:4;
then c,d // a,b by Th36;
hence (POS,M,K) by A1, Def15; ::_thesis: verum
end;
end;
theorem Th50: :: ANALMETR:50
for POS being OrtAfSp
for K, M being Subset of POS
for r, s being Element of POS st r,s _|_ K & K // M holds
r,s _|_ M
proof
let POS be OrtAfSp; ::_thesis: for K, M being Subset of POS
for r, s being Element of POS st r,s _|_ K & K // M holds
r,s _|_ M
let K, M be Subset of POS; ::_thesis: for r, s being Element of POS st r,s _|_ K & K // M holds
r,s _|_ M
let r, s be Element of POS; ::_thesis: ( r,s _|_ K & K // M implies r,s _|_ M )
assume that
A1: r,s _|_ K and
A2: K // M ; ::_thesis: r,s _|_ M
consider p, q being Element of POS such that
A3: p <> q and
A4: K = Line (p,q) and
A5: r,s _|_ p,q by A1, Def13;
consider a, b, c, d being Element of POS such that
A6: a <> b and
A7: c <> d and
A8: K = Line (a,b) and
A9: M = Line (c,d) and
A10: a,b // c,d by A2, Def15;
reconsider p9 = p, q9 = q, a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ;
A11: K = Line (a9,b9) by A8, Th41;
A12: K = Line (p9,q9) by A4, Th41;
then q9 in K by AFF_1:15;
then A13: LIN a9,b9,q9 by A11, AFF_1:def_2;
p9 in K by A12, AFF_1:15;
then LIN a9,b9,p9 by A11, AFF_1:def_2;
then A14: a9,b9 // p9,q9 by A13, AFF_1:10;
A15: p,q _|_ r,s by A5, Def8;
a9,b9 // c9,d9 by A10, Th36;
then p9,q9 // c9,d9 by A6, A14, AFF_1:5;
then p,q // c,d by Th36;
then r,s _|_ c,d by A3, A15, Def8;
hence r,s _|_ M by A7, A9, Def13; ::_thesis: verum
end;
theorem Th51: :: ANALMETR:51
for POS being OrtAfSp
for K being Subset of POS
for a, b being Element of POS st a in K & b in K & a,b _|_ K holds
a = b
proof
let POS be OrtAfSp; ::_thesis: for K being Subset of POS
for a, b being Element of POS st a in K & b in K & a,b _|_ K holds
a = b
let K be Subset of POS; ::_thesis: for a, b being Element of POS st a in K & b in K & a,b _|_ K holds
a = b
let a, b be Element of POS; ::_thesis: ( a in K & b in K & a,b _|_ K implies a = b )
assume that
A1: a in K and
A2: b in K and
A3: a,b _|_ K ; ::_thesis: a = b
consider p, q being Element of POS such that
A4: p <> q and
A5: K = Line (p,q) and
A6: a,b _|_ p,q by A3, Def13;
reconsider a9 = a, b9 = b, p9 = p, q9 = q as Element of (Af POS) ;
set K9 = Line (p9,q9);
b9 in Line (p9,q9) by A2, A5, Th41;
then A7: LIN p9,q9,b9 by AFF_1:def_2;
a9 in Line (p9,q9) by A1, A5, Th41;
then LIN p9,q9,a9 by AFF_1:def_2;
then p9,q9 // a9,b9 by A7, AFF_1:10;
then A8: p,q // a,b by Th36;
p,q _|_ a,b by A6, Def8;
then a,b _|_ a,b by A4, A8, Def8;
hence a = b by Def8; ::_thesis: verum
end;
definition
let POS be OrtAfSp;
let K, M be Subset of POS;
:: original: _|_
redefine predK _|_ M;
irreflexivity
for K being Subset of POS holds (POS,b1,b1)
proof
let K be Subset of POS; ::_thesis: (POS,K,K)
assume (POS,K,K) ; ::_thesis: contradiction
then consider a, b being Element of POS such that
A1: a <> b and
A2: K = Line (a,b) and
A3: a,b _|_ K by Def14;
reconsider a9 = a, b9 = b as Element of (Af POS) ;
K = Line (a9,b9) by A2, Th41;
then ( a in K & b in K ) by AFF_1:15;
hence contradiction by A1, A3, Th51; ::_thesis: verum
end;
symmetry
for K, M being Subset of POS st (POS,b1,b2) holds
(POS,b2,b1)
proof
let K, M be Subset of POS; ::_thesis: ( (POS,K,M) implies (POS,M,K) )
assume K _|_ M ; ::_thesis: (POS,M,K)
then consider a, b, c, d being Element of POS such that
A4: ( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) ) and
A5: a,b _|_ c,d by Th45;
c,d _|_ a,b by A5, Def8;
hence (POS,M,K) by A4, Th45; ::_thesis: verum
end;
end;
theorem Th52: :: ANALMETR:52
for POS being OrtAfSp
for K, M, N being Subset of POS st K _|_ M & K // N holds
N _|_ M
proof
let POS be OrtAfSp; ::_thesis: for K, M, N being Subset of POS st K _|_ M & K // N holds
N _|_ M
let K, M, N be Subset of POS; ::_thesis: ( K _|_ M & K // N implies N _|_ M )
assume that
A1: K _|_ M and
A2: K // N ; ::_thesis: N _|_ M
consider r, s being Element of POS such that
A3: ( r <> s & M = Line (r,s) ) and
A4: r,s _|_ K by A1, Def14;
r,s _|_ N by A2, A4, Th50;
hence N _|_ M by A3, Def14; ::_thesis: verum
end;
theorem :: ANALMETR:53
for POS being OrtAfSp
for K being Subset of POS
for a, b, c, d being Element of POS st a in K & b in K & c,d _|_ K holds
( c,d _|_ a,b & a,b _|_ c,d )
proof
let POS be OrtAfSp; ::_thesis: for K being Subset of POS
for a, b, c, d being Element of POS st a in K & b in K & c,d _|_ K holds
( c,d _|_ a,b & a,b _|_ c,d )
let K be Subset of POS; ::_thesis: for a, b, c, d being Element of POS st a in K & b in K & c,d _|_ K holds
( c,d _|_ a,b & a,b _|_ c,d )
let a, b, c, d be Element of POS; ::_thesis: ( a in K & b in K & c,d _|_ K implies ( c,d _|_ a,b & a,b _|_ c,d ) )
assume that
A1: a in K and
A2: b in K and
A3: c,d _|_ K ; ::_thesis: ( c,d _|_ a,b & a,b _|_ c,d )
consider p, q being Element of POS such that
A4: p <> q and
A5: K = Line (p,q) and
A6: c,d _|_ p,q by A3, Def13;
reconsider a9 = a, b9 = b, p9 = p, q9 = q as Element of (Af POS) ;
LIN p,q,b by A2, A5, Def11;
then A7: LIN p9,q9,b9 by Th40;
LIN p,q,a by A1, A5, Def11;
then LIN p9,q9,a9 by Th40;
then p9,q9 // a9,b9 by A7, AFF_1:10;
then A8: p,q // a,b by Th36;
p,q _|_ c,d by A6, Def8;
hence c,d _|_ a,b by A4, A8, Def8; ::_thesis: a,b _|_ c,d
hence a,b _|_ c,d by Def8; ::_thesis: verum
end;
theorem Th54: :: ANALMETR:54
for POS being OrtAfSp
for K being Subset of POS
for a, b being Element of POS st a in K & b in K & a <> b & K is being_line holds
K = Line (a,b)
proof
let POS be OrtAfSp; ::_thesis: for K being Subset of POS
for a, b being Element of POS st a in K & b in K & a <> b & K is being_line holds
K = Line (a,b)
let K be Subset of POS; ::_thesis: for a, b being Element of POS st a in K & b in K & a <> b & K is being_line holds
K = Line (a,b)
let a, b be Element of POS; ::_thesis: ( a in K & b in K & a <> b & K is being_line implies K = Line (a,b) )
assume that
A1: ( a in K & b in K & a <> b ) and
A2: K is being_line ; ::_thesis: K = Line (a,b)
reconsider a9 = a, b9 = b as Element of (Af POS) ;
reconsider K9 = K as Subset of (Af POS) ;
K9 is being_line by A2, Th43;
then K9 = Line (a9,b9) by A1, AFF_1:57;
hence K = Line (a,b) by Th41; ::_thesis: verum
end;
theorem :: ANALMETR:55
for POS being OrtAfSp
for K being Subset of POS
for a, b, c, d being Element of POS st a in K & b in K & a <> b & K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) holds
c,d _|_ K
proof
let POS be OrtAfSp; ::_thesis: for K being Subset of POS
for a, b, c, d being Element of POS st a in K & b in K & a <> b & K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) holds
c,d _|_ K
let K be Subset of POS; ::_thesis: for a, b, c, d being Element of POS st a in K & b in K & a <> b & K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) holds
c,d _|_ K
let a, b, c, d be Element of POS; ::_thesis: ( a in K & b in K & a <> b & K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) implies c,d _|_ K )
assume that
A1: ( a in K & b in K ) and
A2: a <> b and
A3: ( K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) ) ; ::_thesis: c,d _|_ K
( c,d _|_ a,b & K = Line (a,b) ) by A1, A2, A3, Def8, Th54;
hence c,d _|_ K by A2, Def13; ::_thesis: verum
end;
theorem Th56: :: ANALMETR:56
for POS being OrtAfSp
for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & c in N & d in N & M _|_ N holds
a,b _|_ c,d
proof
let POS be OrtAfSp; ::_thesis: for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & c in N & d in N & M _|_ N holds
a,b _|_ c,d
let M, N be Subset of POS; ::_thesis: for a, b, c, d being Element of POS st a in M & b in M & c in N & d in N & M _|_ N holds
a,b _|_ c,d
let a, b, c, d be Element of POS; ::_thesis: ( a in M & b in M & c in N & d in N & M _|_ N implies a,b _|_ c,d )
assume that
A1: a in M and
A2: b in M and
A3: c in N and
A4: d in N and
A5: M _|_ N ; ::_thesis: a,b _|_ c,d
consider p1, q1, p2, q2 being Element of POS such that
A6: p1 <> q1 and
A7: p2 <> q2 and
A8: M = Line (p1,q1) and
A9: N = Line (p2,q2) and
A10: p1,q1 _|_ p2,q2 by A5, Th45;
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p19 = p1, q19 = q1, p29 = p2, q29 = q2 as Element of (Af POS) ;
LIN p1,q1,b by A2, A8, Def11;
then A11: LIN p19,q19,b9 by Th40;
LIN p1,q1,a by A1, A8, Def11;
then LIN p19,q19,a9 by Th40;
then p19,q19 // a9,b9 by A11, AFF_1:10;
then p1,q1 // a,b by Th36;
then A12: p2,q2 _|_ a,b by A6, A10, Def8;
LIN p2,q2,d by A4, A9, Def11;
then A13: LIN p29,q29,d9 by Th40;
LIN p2,q2,c by A3, A9, Def11;
then LIN p29,q29,c9 by Th40;
then p29,q29 // c9,d9 by A13, AFF_1:10;
then p2,q2 // c,d by Th36;
hence a,b _|_ c,d by A7, A12, Def8; ::_thesis: verum
end;
theorem :: ANALMETR:57
for POS being OrtAfSp
for M, N, K, A being Subset of POS
for p, a, b being Element of POS st p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is being_line holds
A _|_ K
proof
let POS be OrtAfSp; ::_thesis: for M, N, K, A being Subset of POS
for p, a, b being Element of POS st p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is being_line holds
A _|_ K
let M, N, K, A be Subset of POS; ::_thesis: for p, a, b being Element of POS st p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is being_line holds
A _|_ K
let p, a, b be Element of POS; ::_thesis: ( p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is being_line implies A _|_ K )
assume that
A1: ( p in M & p in N & a in M & b in N ) and
A2: a <> b and
A3: ( a in K & b in K ) and
A4: A _|_ M and
A5: A _|_ N and
A6: K is being_line ; ::_thesis: A _|_ K
A is being_line by A4, Th44;
then consider q, r being Element of POS such that
A7: q <> r and
A8: A = Line (q,r) by Def12;
reconsider q9 = q, r9 = r as Element of (Af POS) ;
Line (q,r) = Line (q9,r9) by Th41;
then ( q in A & r in A ) by A8, AFF_1:15;
then ( q,r _|_ p,a & q,r _|_ p,b ) by A1, A4, A5, Th56;
then A9: q,r _|_ a,b by Def8;
K = Line (a,b) by A2, A3, A6, Th54;
hence A _|_ K by A2, A7, A8, A9, Th45; ::_thesis: verum
end;
theorem Th58: :: ANALMETR:58
for POS being OrtAfSp
for b, c, a being Element of POS holds
( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c )
proof
let POS be OrtAfSp; ::_thesis: for b, c, a being Element of POS holds
( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c )
let b, c, a be Element of POS; ::_thesis: ( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c )
reconsider a9 = a, b9 = b, c9 = c as Element of (Af POS) ;
thus b,c _|_ a,a by Def8; ::_thesis: ( a,a _|_ b,c & b,c // a,a & a,a // b,c )
hence a,a _|_ b,c by Def8; ::_thesis: ( b,c // a,a & a,a // b,c )
( b9,c9 // a9,a9 & a9,a9 // b9,c9 ) by AFF_1:3;
hence ( b,c // a,a & a,a // b,c ) by Th36; ::_thesis: verum
end;
theorem Th59: :: ANALMETR:59
for POS being OrtAfSp
for a, b, c, d being Element of POS st a,b // c,d holds
( a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a )
proof
let POS be OrtAfSp; ::_thesis: for a, b, c, d being Element of POS st a,b // c,d holds
( a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a )
let a, b, c, d be Element of POS; ::_thesis: ( a,b // c,d implies ( a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a ) )
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ;
assume a,b // c,d ; ::_thesis: ( a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a )
then A1: a9,b9 // c9,d9 by Th36;
then A2: ( b9,a9 // d9,c9 & c9,d9 // a9,b9 ) by AFF_1:4;
A3: d9,c9 // b9,a9 by A1, AFF_1:4;
A4: ( c9,d9 // b9,a9 & d9,c9 // a9,b9 ) by A1, AFF_1:4;
( a9,b9 // d9,c9 & b9,a9 // c9,d9 ) by A1, AFF_1:4;
hence ( a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a ) by A2, A4, A3, Th36; ::_thesis: verum
end;
theorem :: ANALMETR:60
for POS being OrtAfSp
for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q // a,b & p,q // c,d ) or ( p,q // a,b & c,d // p,q ) or ( a,b // p,q & c,d // p,q ) or ( a,b // p,q & p,q // c,d ) ) holds
a,b // c,d
proof
let POS be OrtAfSp; ::_thesis: for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q // a,b & p,q // c,d ) or ( p,q // a,b & c,d // p,q ) or ( a,b // p,q & c,d // p,q ) or ( a,b // p,q & p,q // c,d ) ) holds
a,b // c,d
let p, q, a, b, c, d be Element of POS; ::_thesis: ( p <> q & ( ( p,q // a,b & p,q // c,d ) or ( p,q // a,b & c,d // p,q ) or ( a,b // p,q & c,d // p,q ) or ( a,b // p,q & p,q // c,d ) ) implies a,b // c,d )
assume that
A1: p <> q and
A2: ( ( p,q // a,b & p,q // c,d ) or ( p,q // a,b & c,d // p,q ) or ( a,b // p,q & c,d // p,q ) or ( a,b // p,q & p,q // c,d ) ) ; ::_thesis: a,b // c,d
reconsider p9 = p, q9 = q, a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ;
( ( p9,q9 // a9,b9 & p9,q9 // c9,d9 ) or ( p9,q9 // a9,b9 & c9,d9 // p9,q9 ) or ( a9,b9 // p9,q9 & c9,d9 // p9,q9 ) or ( a9,b9 // p9,q9 & p9,q9 // c9,d9 ) ) by A2, Th36;
then a9,b9 // c9,d9 by A1, AFF_1:5;
hence a,b // c,d by Th36; ::_thesis: verum
end;
theorem Th61: :: ANALMETR:61
for POS being OrtAfSp
for a, b, c, d being Element of POS st a,b _|_ c,d holds
( a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a )
proof
let POS be OrtAfSp; ::_thesis: for a, b, c, d being Element of POS st a,b _|_ c,d holds
( a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a )
let a, b, c, d be Element of POS; ::_thesis: ( a,b _|_ c,d implies ( a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a ) )
assume A1: a,b _|_ c,d ; ::_thesis: ( a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a )
then a,b _|_ d,c by Def8;
then A2: d,c _|_ a,b by Def8;
then d,c _|_ b,a by Def8;
then b,a _|_ d,c by Def8;
then b,a _|_ c,d by Def8;
hence ( a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a ) by A1, A2, Def8; ::_thesis: verum
end;
theorem Th62: :: ANALMETR:62
for POS being OrtAfSp
for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) ) holds
a,b _|_ c,d
proof
let POS be OrtAfSp; ::_thesis: for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) ) holds
a,b _|_ c,d
let p, q, a, b, c, d be Element of POS; ::_thesis: ( p <> q & ( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) ) implies a,b _|_ c,d )
assume that
A1: p <> q and
A2: ( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) ) ; ::_thesis: a,b _|_ c,d
A3: now__::_thesis:_(_(_(_p,q_//_a,b_&_p,q__|__c,d_)_or_(_p,q_//_a,b_&_c,d__|__p,q_)_or_(_a,b_//_p,q_&_c,d__|__p,q_)_or_(_a,b_//_p,q_&_p,q__|__c,d_)_)_implies_a,b__|__c,d_)
assume ( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // a,b & c,d _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) ) ; ::_thesis: a,b _|_ c,d
then ( p,q // a,b & p,q _|_ c,d ) by Th59, Th61;
then c,d _|_ a,b by A1, Def8;
hence a,b _|_ c,d by Th61; ::_thesis: verum
end;
now__::_thesis:_(_(_(_p,q_//_c,d_&_p,q__|__a,b_)_or_(_p,q_//_c,d_&_a,b__|__p,q_)_or_(_c,d_//_p,q_&_a,b__|__p,q_)_or_(_c,d_//_p,q_&_p,q__|__a,b_)_)_implies_a,b__|__c,d_)
assume ( ( p,q // c,d & p,q _|_ a,b ) or ( p,q // c,d & a,b _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( c,d // p,q & p,q _|_ a,b ) ) ; ::_thesis: a,b _|_ c,d
then ( p,q // c,d & p,q _|_ a,b ) by Th59, Th61;
hence a,b _|_ c,d by A1, Def8; ::_thesis: verum
end;
hence a,b _|_ c,d by A2, A3; ::_thesis: verum
end;
theorem Th63: :: ANALMETR:63
for POS being OrtAfPl
for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q _|_ a,b & p,q _|_ c,d ) or ( p,q _|_ a,b & c,d _|_ p,q ) or ( a,b _|_ p,q & c,d _|_ p,q ) or ( a,b _|_ p,q & p,q _|_ c,d ) ) holds
a,b // c,d
proof
let POS be OrtAfPl; ::_thesis: for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q _|_ a,b & p,q _|_ c,d ) or ( p,q _|_ a,b & c,d _|_ p,q ) or ( a,b _|_ p,q & c,d _|_ p,q ) or ( a,b _|_ p,q & p,q _|_ c,d ) ) holds
a,b // c,d
let p, q, a, b, c, d be Element of POS; ::_thesis: ( p <> q & ( ( p,q _|_ a,b & p,q _|_ c,d ) or ( p,q _|_ a,b & c,d _|_ p,q ) or ( a,b _|_ p,q & c,d _|_ p,q ) or ( a,b _|_ p,q & p,q _|_ c,d ) ) implies a,b // c,d )
assume that
A1: p <> q and
A2: ( ( p,q _|_ a,b & p,q _|_ c,d ) or ( p,q _|_ a,b & c,d _|_ p,q ) or ( a,b _|_ p,q & c,d _|_ p,q ) or ( a,b _|_ p,q & p,q _|_ c,d ) ) ; ::_thesis: a,b // c,d
( p,q _|_ a,b & p,q _|_ c,d ) by A2, Th61;
hence a,b // c,d by A1, Def9; ::_thesis: verum
end;
theorem :: ANALMETR:64
for POS being OrtAfPl
for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & a <> b & M is being_line & c in N & d in N & c <> d & N is being_line & a,b // c,d holds
M // N
proof
let POS be OrtAfPl; ::_thesis: for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & a <> b & M is being_line & c in N & d in N & c <> d & N is being_line & a,b // c,d holds
M // N
let M, N be Subset of POS; ::_thesis: for a, b, c, d being Element of POS st a in M & b in M & a <> b & M is being_line & c in N & d in N & c <> d & N is being_line & a,b // c,d holds
M // N
let a, b, c, d be Element of POS; ::_thesis: ( a in M & b in M & a <> b & M is being_line & c in N & d in N & c <> d & N is being_line & a,b // c,d implies M // N )
assume that
A1: ( a in M & b in M ) and
A2: a <> b and
A3: ( M is being_line & c in N & d in N ) and
A4: c <> d and
A5: N is being_line and
A6: a,b // c,d ; ::_thesis: M // N
( M = Line (a,b) & N = Line (c,d) ) by A1, A2, A3, A4, A5, Th54;
hence M // N by A2, A4, A6, Def15; ::_thesis: verum
end;
theorem :: ANALMETR:65
for POS being OrtAfPl
for M, K, N being Subset of POS st M _|_ K & N _|_ K holds
M // N
proof
let POS be OrtAfPl; ::_thesis: for M, K, N being Subset of POS st M _|_ K & N _|_ K holds
M // N
let M, K, N be Subset of POS; ::_thesis: ( M _|_ K & N _|_ K implies M // N )
assume that
A1: M _|_ K and
A2: N _|_ K ; ::_thesis: M // N
consider p1, q1, a, b being Element of POS such that
A3: p1 <> q1 and
A4: a <> b and
A5: K = Line (p1,q1) and
A6: M = Line (a,b) and
A7: p1,q1 _|_ a,b by A1, Th45;
consider p2, q2, c, d being Element of POS such that
A8: p2 <> q2 and
A9: c <> d and
A10: K = Line (p2,q2) and
A11: N = Line (c,d) and
A12: p2,q2 _|_ c,d by A2, Th45;
reconsider p19 = p1, p29 = p2, q19 = q1, q29 = q2 as Element of (Af POS) ;
A13: Line (p19,q19) = Line (p2,q2) by A5, A10, Th41
.= Line (p29,q29) by Th41 ;
then q29 in Line (p19,q19) by AFF_1:15;
then A14: LIN p19,q19,q29 by AFF_1:def_2;
p29 in Line (p19,q19) by A13, AFF_1:15;
then LIN p19,q19,p29 by AFF_1:def_2;
then p19,q19 // p29,q29 by A14, AFF_1:10;
then p1,q1 // p2,q2 by Th36;
then a,b _|_ p2,q2 by A3, A7, Th62;
then a,b // c,d by A8, A12, Th63;
hence M // N by A4, A6, A9, A11, Def15; ::_thesis: verum
end;
theorem Th66: :: ANALMETR:66
for POS being OrtAfPl
for M, N being Subset of POS st M _|_ N holds
ex p being Element of POS st
( p in M & p in N )
proof
let POS be OrtAfPl; ::_thesis: for M, N being Subset of POS st M _|_ N holds
ex p being Element of POS st
( p in M & p in N )
let M, N be Subset of POS; ::_thesis: ( M _|_ N implies ex p being Element of POS st
( p in M & p in N ) )
reconsider M9 = M, N9 = N as Subset of (Af POS) ;
assume A1: M _|_ N ; ::_thesis: ex p being Element of POS st
( p in M & p in N )
then M is being_line by Th44;
then A2: M9 is being_line by Th43;
N is being_line by A1, Th44;
then A3: N9 is being_line by Th43;
not M // N by A1, Th52;
then not M9 // N9 by Th46;
hence ex p being Element of POS st
( p in M & p in N ) by A2, A3, AFF_1:58; ::_thesis: verum
end;
theorem Th67: :: ANALMETR:67
for POS being OrtAfPl
for a, b, c, d being Element of POS st a,b _|_ c,d holds
ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
proof
let POS be OrtAfPl; ::_thesis: for a, b, c, d being Element of POS st a,b _|_ c,d holds
ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
let a, b, c, d be Element of POS; ::_thesis: ( a,b _|_ c,d implies ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) )
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ;
assume A1: a,b _|_ c,d ; ::_thesis: ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
A2: now__::_thesis:_(_a_<>_b_&_c_<>_d_implies_ex_p_being_Element_of_POS_st_
(_LIN_a,b,p_&_LIN_c,d,p_)_)
set M = Line (a,b);
set N = Line (c,d);
assume ( a <> b & c <> d ) ; ::_thesis: ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
then Line (a,b) _|_ Line (c,d) by A1, Th45;
then consider p being Element of POS such that
A3: ( p in Line (a,b) & p in Line (c,d) ) by Th66;
( LIN a,b,p & LIN c,d,p ) by A3, Def11;
hence ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) ; ::_thesis: verum
end;
LIN a9,b9,a9 by AFF_1:7;
then A4: LIN a,b,a by Th40;
A5: now__::_thesis:_(_c_=_d_implies_ex_p_being_Element_of_POS_st_
(_LIN_a,b,p_&_LIN_c,d,p_)_)
assume c = d ; ::_thesis: ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
then c,d // c,a by Th58;
then LIN c,d,a by Def10;
hence ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) by A4; ::_thesis: verum
end;
LIN c9,d9,c9 by AFF_1:7;
then A6: LIN c,d,c by Th40;
now__::_thesis:_(_a_=_b_implies_ex_p_being_Element_of_POS_st_
(_LIN_a,b,p_&_LIN_c,d,p_)_)
assume a = b ; ::_thesis: ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
then a,b // a,c by Th58;
then LIN a,b,c by Def10;
hence ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) by A6; ::_thesis: verum
end;
hence ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) by A5, A2; ::_thesis: verum
end;
theorem :: ANALMETR:68
for POS being OrtAfPl
for K being Subset of POS
for a, b being Element of POS st a,b _|_ K holds
ex p being Element of POS st
( LIN a,b,p & p in K )
proof
let POS be OrtAfPl; ::_thesis: for K being Subset of POS
for a, b being Element of POS st a,b _|_ K holds
ex p being Element of POS st
( LIN a,b,p & p in K )
let K be Subset of POS; ::_thesis: for a, b being Element of POS st a,b _|_ K holds
ex p being Element of POS st
( LIN a,b,p & p in K )
let a, b be Element of POS; ::_thesis: ( a,b _|_ K implies ex p being Element of POS st
( LIN a,b,p & p in K ) )
assume a,b _|_ K ; ::_thesis: ex p being Element of POS st
( LIN a,b,p & p in K )
then consider p, q being Element of POS such that
p <> q and
A1: K = Line (p,q) and
A2: a,b _|_ p,q by Def13;
consider c being Element of POS such that
A3: LIN a,b,c and
A4: LIN p,q,c by A2, Th67;
c in K by A1, A4, Def11;
hence ex p being Element of POS st
( LIN a,b,p & p in K ) by A3; ::_thesis: verum
end;
theorem Th69: :: ANALMETR:69
for POS being OrtAfPl
for a, p, q being Element of POS ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
proof
let POS be OrtAfPl; ::_thesis: for a, p, q being Element of POS ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
let a, p, q be Element of POS; ::_thesis: ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
A1: now__::_thesis:_(_p_<>_q_implies_ex_x_being_Element_of_POS_st_
(_a,x__|__p,q_&_LIN_p,q,x_)_)
assume p <> q ; ::_thesis: ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
then consider x being Element of POS such that
A2: ( p,q // p,x & p,q _|_ x,a ) by Def8;
take x = x; ::_thesis: ( a,x _|_ p,q & LIN p,q,x )
thus ( a,x _|_ p,q & LIN p,q,x ) by A2, Def10, Th61; ::_thesis: verum
end;
now__::_thesis:_(_p_=_q_implies_ex_x_being_Element_of_POS_st_
(_a,x__|__p,q_&_LIN_p,q,x_)_)
assume A3: p = q ; ::_thesis: ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
take x = a; ::_thesis: ( a,x _|_ p,q & LIN p,q,x )
p,q // p,a by A3, Th58;
hence ( a,x _|_ p,q & LIN p,q,x ) by Def10, Th58; ::_thesis: verum
end;
hence ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x ) by A1; ::_thesis: verum
end;
theorem :: ANALMETR:70
for POS being OrtAfPl
for K being Subset of POS
for a being Element of POS st K is being_line holds
ex x being Element of POS st
( a,x _|_ K & x in K )
proof
let POS be OrtAfPl; ::_thesis: for K being Subset of POS
for a being Element of POS st K is being_line holds
ex x being Element of POS st
( a,x _|_ K & x in K )
let K be Subset of POS; ::_thesis: for a being Element of POS st K is being_line holds
ex x being Element of POS st
( a,x _|_ K & x in K )
let a be Element of POS; ::_thesis: ( K is being_line implies ex x being Element of POS st
( a,x _|_ K & x in K ) )
assume K is being_line ; ::_thesis: ex x being Element of POS st
( a,x _|_ K & x in K )
then consider p, q being Element of POS such that
A1: p <> q and
A2: K = Line (p,q) by Def12;
consider x being Element of POS such that
A3: a,x _|_ p,q and
A4: LIN p,q,x by Th69;
take x ; ::_thesis: ( a,x _|_ K & x in K )
thus a,x _|_ K by A1, A2, A3, Def13; ::_thesis: x in K
thus x in K by A2, A4, Def11; ::_thesis: verum
end;