let MS be OrtAfPl; :: thesis: for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace V,w,y holds
MS is Homogeneous
let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y & MS = AMSpace V,w,y holds
MS is Homogeneous
let w, y be VECTOR of V; :: thesis: ( Gen w,y & MS = AMSpace V,w,y implies MS is Homogeneous )
assume that
A1: Gen w,y and
A2: MS = AMSpace V,w,y ; :: thesis: MS is Homogeneous

now

let o, a, a1, b, b1, c, c1 be Element of MS; :: thesis: ( o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b implies b,c _|_ b1,c1 )
assume that
A3: ( o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 ) and
A4: ( a,b _|_ a1,b1 & a,c _|_ a1,c1 ) and
A5: ( not o,c // o,a & not o,a // o,b ) ; :: thesis: b,c _|_ b1,c1
reconsider q = o, u1 = a, u2 = b, u3 = c, v1 = a1, v2 = b1, v3 = c1 as VECTOR of V by A2, ANALMETR:28;
A6: ( not LIN o,a,b & not LIN o,a,c )

proof

assume ( LIN o,a,b or LIN o,a,c ) ; :: thesis: contradiction
then ( o,a // o,b or o,a // o,c ) by ANALMETR:def 11;
hence contradiction by A5, ANALMETR:81; :: thesis: verum

end;

then A7: ( o <> a & o <> b & o <> c ) by Th1;

now

assume A8: o <> a1 ; :: thesis: b,c _|_ b1,c1
( q,u3,q,v3 are_Ort_wrt w,y & q,u1,q,v1 are_Ort_wrt w,y & q,u2,q,v2 are_Ort_wrt w,y ) by A2, A3, ANALMETR:31;
then A9: ( u1 - q,v1 - q are_Ort_wrt w,y & u2 - q,v2 - q are_Ort_wrt w,y & u3 - q,v3 - q are_Ort_wrt w,y ) by ANALMETR:def 3;
( u1 - q <> 0. V & v1 - q <> 0. V ) by A7, A8, RLVECT_1:35;
then consider r being Real such that
A10: for a', b' being Real holds
( (a' * w) + (b' * y),((r * b') * w) + ((- (r * a')) * y) are_Ort_wrt w,y & ((a' * w) + (b' * y)) - (u1 - q),(((r * b') * w) + ((- (r * a')) * y)) - (v1 - q) are_Ort_wrt w,y ) by A1, A9, Th19;
consider A1, A2 being Real such that
A11: u3 - q = (A1 * w) + (A2 * y) by A1, ANALMETR:def 1;
consider B1, B2 being Real such that
A12: u2 - q = (B1 * w) + (B2 * y) by A1, ANALMETR:def 1;
set v3' = (((r * A2) * w) + ((- (r * A1)) * y)) + q;
set v2' = (((r * B2) * w) + ((- (r * B1)) * y)) + q;
reconsider c1' = (((r * A2) * w) + ((- (r * A1)) * y)) + q, b1' = (((r * B2) * w) + ((- (r * B1)) * y)) + q as Element of MS by A2, ANALMETR:28;
A13: ( ((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q = ((r * A2) * w) + ((- (r * A1)) * y) & ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q = ((r * B2) * w) + ((- (r * B1)) * y) ) by RLSUB_2:78;
then ( u3 - q,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q are_Ort_wrt w,y & u2 - q,((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q are_Ort_wrt w,y ) by A10, A11, A12;
then ( q,u3,q,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y & q,u2,q,(((r * B2) * w) + ((- (r * B1)) * y)) + q are_Ort_wrt w,y ) by ANALMETR:def 3;
then A14: ( o,c _|_ o,c1' & o,b _|_ o,b1' ) by A2, ANALMETR:31;
( (u3 - q) - (u1 - q) = u3 - u1 & (u2 - q) - (u1 - q) = u2 - u1 & (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q) - (v1 - q) = ((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v1 & (((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q) - (v1 - q) = ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v1 ) by Lm4;
then ( u3 - u1,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v1 are_Ort_wrt w,y & u2 - u1,((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v1 are_Ort_wrt w,y ) by A10, A11, A12, A13;
then ( u1,u3,v1,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y & u1,u2,v1,(((r * B2) * w) + ((- (r * B1)) * y)) + q are_Ort_wrt w,y ) by ANALMETR:def 3;
then ( a,c _|_ a1,c1' & a,b _|_ a1,b1' ) by A2, ANALMETR:31;
then A15: ( c1 = c1' & b1 = b1' ) by A3, A4, A6, A8, A14, Th16;
u3 - u2 = ((A1 * w) + (A2 * y)) - ((B1 * w) + (B2 * y)) by A11, A12, Lm4
.= ((A1 - B1) * w) + ((A2 - B2) * y) by Lm6 ;
then A16: ( pr1 w,y,(u3 - u2) = A1 - B1 & pr2 w,y,(u3 - u2) = A2 - B2 ) by A1, GEOMTRAP:def 4, GEOMTRAP:def 5;
((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q) = (((r * A2) * w) + ((r * (- A1)) * y)) - (((r * B2) * w) + ((- (r * B1)) * y)) by Lm4
.= (((r * A2) - (r * B2)) * w) + (((r * (- A1)) - (r * (- B1))) * y) by Lm6
.= ((r * (A2 - B2)) * w) + ((r * (B1 - A1)) * y) ;
then ( pr1 w,y,(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q)) = r * (A2 - B2) & pr2 w,y,(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q)) = r * (B1 - A1) ) by A1, GEOMTRAP:def 4, GEOMTRAP:def 5;
then PProJ w,y,(u3 - u2),(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q)) = ((A1 - B1) * (r * (A2 - B2))) + ((A2 - B2) * (r * (B1 - A1))) by A16, GEOMTRAP:def 6
.= 0 ;
then u3 - u2,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - ((((r * B2) * w) + ((- (r * B1)) * y)) + q) are_Ort_wrt w,y by A1, GEOMTRAP:34;
then u2,u3,(((r * B2) * w) + ((- (r * B1)) * y)) + q,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def 3;
hence b,c _|_ b1,c1 by A2, A15, ANALMETR:31; :: thesis: verum

end;

hence b,c _|_ b1,c1 by A3, A4, A5, Th22; :: thesis: verum

end;

hence MS is Homogeneous by Def7; :: thesis: verum