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 satisfying_LIN
let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is satisfying_LIN
let w, y be VECTOR of V; :: thesis: ( Gen w,y & MS = AMSpace (V,w,y) implies MS is satisfying_LIN )
assume that
A1: Gen w,y and
A2: MS = AMSpace (V,w,y) ; :: thesis: MS is satisfying_LIN
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 & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 holds
a,a1 // b,b1
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 & o,c _|_ o,c1 & o,a _|_ o,a1 & o,b _|_ o,b1 & not LIN o,c,a & LIN o,a,b & LIN o,a1,b1 & a,c _|_ a1,c1 & b,c _|_ b1,c1 implies a,a1 // b,b1 )
assume that
A3: o <> a and
o <> a1 and
A4: o <> b and
o <> b1 and
A5: o <> c and
A6: o <> c1 and
a <> b and
A7: o,c _|_ o,c1 and
A8: o,a _|_ o,a1 and
A9: o,b _|_ o,b1 and
A10: not LIN o,c,a and
A11: LIN o,a,b and
LIN o,a1,b1 and
A12: a,c _|_ a1,c1 and
A13: b,c _|_ b1,c1 ; :: thesis: a,a1 // b,b1
reconsider q = o, u1 = a, u2 = b, u3 = c, v3 = c1 as VECTOR of V by A2, ANALMETR:19;
consider A1, A2 being Real such that
A14: u1 - q = (A1 * w) + (A2 * y) by A1, ANALMETR:def 1;
reconsider A1 = A1, A2 = A2 as Real ;
A15: not LIN o,c,b
proof
reconsider o9 = o, a9 = a, b9 = b, c9 = c as Element of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
assume LIN o,c,b ; :: thesis: contradiction
then LIN o9,c9,b9 by ANALMETR:40;
then A16: LIN o9,b9,c9 by AFF_1:6;
LIN o9,a9,b9 by A11, ANALMETR:40;
then A17: LIN o9,b9,a9 by AFF_1:6;
LIN o9,b9,o9 by AFF_1:7;
then LIN o9,c9,a9 by A4, A16, A17, AFF_1:8;
hence contradiction by A10, ANALMETR:40; :: thesis: verum
end;
q,u3,q,v3 are_Ort_wrt w,y by A2, A7, ANALMETR:21;
then A18: u3 - q,v3 - q are_Ort_wrt w,y by ANALMETR:def 3;
( u3 - q <> 0. V & v3 - q <> 0. V ) by A5, A6, RLVECT_1:21;
then consider r being Real such that
A19: 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)) - (u3 - q),(((r * b9) * w) + ((- (r * a9)) * y)) - (v3 - q) are_Ort_wrt w,y ) by A1, A18, Th19;
o,a // o,b by A11, ANALMETR:def 10;
then q,u1 '||' q,u2 by A2, GEOMTRAP:4;
then ( q,u1 // q,u2 or q,u1 // u2,q ) by GEOMTRAP:def 1;
then consider a9, b9 being Real such that
A20: a9 * (u1 - q) = b9 * (u2 - q) and
A21: ( a9 <> 0 or b9 <> 0 ) by ANALMETR:14;
consider B1, B2 being Real such that
A22: u2 - q = (B1 * w) + (B2 * y) by A1, ANALMETR:def 1;
reconsider a9 = a9, b9 = b9, B1 = B1, B2 = B2 as Real ;
set s = (b9 ") * a9;
A23: u1 - q <> 0. V by A3, RLVECT_1:21;
now :: thesis: not b9 = 0
assume A24: b9 = 0 ; :: thesis: contradiction
then 0. V = a9 * (u1 - q) by A20, RLVECT_1:10;
hence contradiction by A23, A21, A24, RLVECT_1:11; :: thesis: verum
end;
then A25: u2 - q = (b9 ") * (a9 * (u1 - q)) by A20, ANALOAF:5
.= ((b9 ") * a9) * (u1 - q) by RLVECT_1:def 7 ;
then (B1 * w) + (B2 * y) = (((b9 ") * a9) * (A1 * w)) + (((b9 ") * a9) * (A2 * y)) by A14, A22, RLVECT_1:def 5
.= ((((b9 ") * a9) * A1) * w) + (((b9 ") * a9) * (A2 * y)) by RLVECT_1:def 7
.= ((((b9 ") * a9) * A1) * w) + ((((b9 ") * a9) * A2) * y) by RLVECT_1:def 7 ;
then A26: ( B1 = ((b9 ") * a9) * A1 & B2 = ((b9 ") * a9) * A2 ) by A1, Lm7;
set v19 = (((r * A2) * w) + ((- (r * A1)) * y)) + q;
set v29 = (((r * B2) * w) + ((- (r * B1)) * y)) + q;
reconsider a19 = (((r * A2) * w) + ((- (r * A1)) * y)) + q, b19 = (((r * B2) * w) + ((- (r * B1)) * y)) + q as Element of MS by A2, ANALMETR:19;
A27: ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q = ((r * B2) * w) + ((- (r * B1)) * y) by RLSUB_2:61
.= ((r * B2) * w) + ((r * B1) * (- y)) by RLVECT_1:24
.= ((r * (((b9 ") * a9) * A2)) * w) - ((r * (((b9 ") * a9) * A1)) * y) by A26, RLVECT_1:25
.= (r * ((((b9 ") * a9) * A2) * w)) - ((r * (((b9 ") * a9) * A1)) * y) by RLVECT_1:def 7
.= (r * ((((b9 ") * a9) * A2) * w)) - (r * ((((b9 ") * a9) * A1) * y)) by RLVECT_1:def 7
.= r * (((((b9 ") * a9) * A2) * w) - ((((b9 ") * a9) * A1) * y)) by RLVECT_1:34
.= r * ((((b9 ") * a9) * (A2 * w)) - ((((b9 ") * a9) * A1) * y)) by RLVECT_1:def 7
.= r * ((((b9 ") * a9) * (A2 * w)) - (((b9 ") * a9) * (A1 * y))) by RLVECT_1:def 7
.= r * (((b9 ") * a9) * ((A2 * w) - (A1 * y))) by RLVECT_1:34
.= (((b9 ") * a9) * r) * ((A2 * w) - (A1 * y)) by RLVECT_1:def 7
.= ((b9 ") * a9) * (r * ((A2 * w) - (A1 * y))) by RLVECT_1:def 7
.= ((b9 ") * a9) * ((r * (A2 * w)) - (r * (A1 * y))) by RLVECT_1:34
.= ((b9 ") * a9) * (((r * A2) * w) - (r * (A1 * y))) by RLVECT_1:def 7
.= ((b9 ") * a9) * (((r * A2) * w) + (- ((r * A1) * y))) by RLVECT_1:def 7
.= ((b9 ") * a9) * (((r * A2) * w) + ((r * A1) * (- y))) by RLVECT_1:25
.= ((b9 ") * a9) * (((r * A2) * w) + ((- (r * A1)) * y)) by RLVECT_1:24
.= ((b9 ") * a9) * (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q) by RLSUB_2:61 ;
A28: ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q = ((r * B2) * w) + ((- (r * B1)) * y) by RLSUB_2:61;
then u2 - q,((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q are_Ort_wrt w,y by A19, A22;
then q,u2,q,(((r * B2) * w) + ((- (r * B1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def 3;
then A29: o,b _|_ o,b19 by A2, ANALMETR:21;
1 * (u2 - ((((r * B2) * w) + ((- (r * B1)) * y)) + q)) = u2 - ((((r * B2) * w) + ((- (r * B1)) * y)) + q) by RLVECT_1:def 8
.= (((b9 ") * a9) * (u1 - q)) - (((b9 ") * a9) * (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q)) by A25, A27, Lm4
.= ((b9 ") * a9) * ((u1 - q) - (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q)) by RLVECT_1:34
.= ((b9 ") * a9) * (u1 - ((((r * A2) * w) + ((- (r * A1)) * y)) + q)) by Lm4 ;
then ( (((r * A2) * w) + ((- (r * A1)) * y)) + q,u1 // (((r * B2) * w) + ((- (r * B1)) * y)) + q,u2 or (((r * A2) * w) + ((- (r * A1)) * y)) + q,u1 // u2,(((r * B2) * w) + ((- (r * B1)) * y)) + q ) by ANALMETR:14;
then (((r * A2) * w) + ((- (r * A1)) * y)) + q,u1 '||' (((r * B2) * w) + ((- (r * B1)) * y)) + q,u2 by GEOMTRAP:def 1;
then A30: a19,a // b19,b by A2, GEOMTRAP:4;
A31: ((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q = ((r * A2) * w) + ((- (r * A1)) * y) by RLSUB_2:61;
then u1 - q,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q are_Ort_wrt w,y by A19, A14;
then q,u1,q,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def 3;
then A32: o,a _|_ o,a19 by A2, ANALMETR:21;
( (u2 - q) - (u3 - q) = u2 - u3 & (((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q) - (v3 - q) = ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v3 ) by Lm4;
then u2 - u3,((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v3 are_Ort_wrt w,y by A19, A22, A28;
then u3,u2,v3,(((r * B2) * w) + ((- (r * B1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def 3;
then A33: c,b _|_ c1,b19 by A2, ANALMETR:21;
c,b _|_ c1,b1 by A13, ANALMETR:61;
then A34: b1 = b19 by A6, A7, A9, A15, A29, A33, Th16;
( (u1 - q) - (u3 - q) = u1 - u3 & (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q) - (v3 - q) = ((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v3 ) by Lm4;
then u1 - u3,((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v3 are_Ort_wrt w,y by A19, A14, A31;
then u3,u1,v3,(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,y by ANALMETR:def 3;
then A35: c,a _|_ c1,a19 by A2, ANALMETR:21;
c,a _|_ c1,a1 by A12, ANALMETR:61;
then a1 = a19 by A6, A7, A8, A10, A32, A35, Th16;
hence a,a1 // b,b1 by A34, A30, ANALMETR:59; :: thesis: verum
end;
hence MS is satisfying_LIN by CONAFFM:def 5; :: thesis: verum