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 :: thesis: for o, a, a1, b, b1, c, c1 being Element of MS st 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 holds
b,c _|_ b1,c1

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 and
A4: o,b _|_ o,b1 and
A5: o,c _|_ o,c1 and
A6: a,b _|_ a1,b1 and
A7: a,c _|_ a1,c1 and
A8: ( 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 as VECTOR of V by A2, ANALMETR:19;
A9: ( 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 10;
hence contradiction by A8, ANALMETR:59; :: thesis: verum

end;

then A10: o <> a by Th1;

now :: thesis: ( o <> a1 implies b,c _|_ b1,c1 )

q,u1,q,v1 are_Ort_wrt w,y by A2, A3, ANALMETR:21;
then A11: u1 - q,v1 - q are_Ort_wrt w,y by ANALMETR:def 3;
A12: u1 - q <> 0. V by A10, RLVECT_1:21;
assume A13: o <> a1 ; :: thesis: b,c _|_ b1,c1
then v1 - q <> 0. V by RLVECT_1:21;
then consider r being Real such that
A14: for a9, b9 being Real holds
( (a9 * w) + (b9 * y),((r * b9) * w) + ((- (r * a9)) * y) are_Ort_wrt w,y & ((a9 * w) + (b9 * y)) - (u1 - q),(((r * b9) * w) + ((- (r * a9)) * y)) - (v1 - q) are_Ort_wrt w,y ) by A1, A11, A12, Th19;
consider B1, B2 being Real such that
A15: u2 - q = (B1 * w) + (B2 * y) by A1, ANALMETR:def 1;
consider A1, A2 being Real such that
A16: u3 - q = (A1 * w) + (A2 * y) by A1, ANALMETR:def 1;
reconsider B1 = B1, B2 = B2, A1 = A1, A2 = A2 as Real ;
set v39 = (((r * A2) * w) + ((- (r * A1)) * y)) + q;
set v29 = (((r * B2) * w) + ((- (r * B1)) * y)) + q;
reconsider c19 = (((r * A2) * w) + ((- (r * A1)) * y)) + q, b19 = (((r * B2) * w) + ((- (r * B1)) * y)) + q as Element of MS by A2, ANALMETR:19;
A17: ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q = ((r * B2) * w) + ((- (r * B1)) * y) by RLSUB_2:61;
( (u2 - q) - (u1 - q) = u2 - u1 & (((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q) - (v1 - q) = ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v1 ) by Lm4;
then u2 - u1,((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v1 are_Ort_wrt w,y by A14, A15, A17;
then u1,u2,v1,(((r * B2) * w) + ((- (r * B1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def 3;
then A18: a,b _|_ a1,b19 by A2, ANALMETR:21;
u2 - q,((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q are_Ort_wrt w,y by A14, A15, A17;
then q,u2,q,(((r * B2) * w) + ((- (r * B1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def 3;
then o,b _|_ o,b19 by A2, ANALMETR:21;
then A19: b1 = b19 by A3, A4, A6, A9, A13, A18, Th16;
A20: ((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q = ((r * A2) * w) + ((- (r * A1)) * y) by RLSUB_2:61;
u3 - u2 = ((A1 * w) + (A2 * y)) - ((B1 * w) + (B2 * y)) by A16, A15, Lm4
.= ((A1 - B1) * w) + ((A2 - B2) * y) by Lm6 ;
then A21: ( 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 A21, 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:32;
then A22: 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;
( (u3 - q) - (u1 - q) = u3 - u1 & (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q) - (v1 - q) = ((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v1 ) by Lm4;
then u3 - u1,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v1 are_Ort_wrt w,y by A14, A16, A20;
then u1,u3,v1,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def 3;
then A23: a,c _|_ a1,c19 by A2, ANALMETR:21;
u3 - q,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q are_Ort_wrt w,y by A14, A16, A20;
then q,u3,q,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def 3;
then o,c _|_ o,c19 by A2, ANALMETR:21;
then c1 = c19 by A3, A5, A7, A9, A13, A23, Th16;
hence b,c _|_ b1,c1 by A2, A19, A22, ANALMETR:21; :: thesis: verum

end;

hence b,c _|_ b1,c1 by A4, A5, A6, A7, A8, Th21; :: thesis: verum

end;

hence MS is Homogeneous ; :: thesis: verum