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 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 &
o <> a1 &
o <> b &
o <> b1 &
o <> c &
o <> c1 &
a <> b )
and A4:
(
o,
c _|_ o,
c1 &
o,
a _|_ o,
a1 &
o,
b _|_ o,
b1 )
and A5:
( not
LIN o,
c,
a &
LIN o,
a,
b &
LIN o,
a1,
b1 )
and A6:
(
a,
c _|_ a1,
c1 &
b,
c _|_ b1,
c1 )
;
:: thesis: a,a1 // b,b1A7:
not
LIN o,
c,
b
proof
assume A8:
LIN o,
c,
b
;
:: thesis: contradiction
reconsider o' =
o,
a' =
a,
b' =
b,
c' =
c as
Element of
(Af MS) by ANALMETR:47;
(
LIN o',
c',
b' &
LIN o',
a',
b' )
by A5, A8, ANALMETR:55;
then
(
LIN o',
b',
c' &
LIN o',
b',
a' &
LIN o',
b',
o' )
by AFF_1:15, AFF_1:16;
then
LIN o',
c',
a'
by A3, AFF_1:17;
hence
contradiction
by A5, ANALMETR:55;
:: thesis: verum
end; reconsider q =
o,
u1 =
a,
u2 =
b,
u3 =
c,
v1 =
a1,
v2 =
b1,
v3 =
c1 as
VECTOR of
V by A2, ANALMETR:28;
(
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, A4, 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;
A10:
(
u1 - q <> 0. V &
u2 - q <> 0. V &
u3 - q <> 0. V &
v3 - q <> 0. V )
by A3, RLVECT_1:35;
then consider r being
Real such that A11:
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)) - (u3 - q),
(((r * b') * w) + ((- (r * a')) * y)) - (v3 - q) are_Ort_wrt w,
y )
by A1, A9, Th19;
consider A1,
A2 being
Real such that A12:
u1 - q = (A1 * w) + (A2 * y)
by A1, ANALMETR:def 1;
consider B1,
B2 being
Real such that A13:
u2 - q = (B1 * w) + (B2 * y)
by A1, ANALMETR:def 1;
set v1' =
(((r * A2) * w) + ((- (r * A1)) * y)) + q;
set v2' =
(((r * B2) * w) + ((- (r * B1)) * y)) + q;
reconsider a1' =
(((r * A2) * w) + ((- (r * A1)) * y)) + q,
b1' =
(((r * B2) * w) + ((- (r * B1)) * y)) + q as
Element of
MS by A2, ANALMETR:28;
A14:
(
((((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
(
u1 - 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 A11, A12, A13;
then
(
q,
u1,
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 A15:
(
o,
a _|_ o,
a1' &
o,
b _|_ o,
b1' )
by A2, ANALMETR:31;
(
(u1 - q) - (u3 - q) = u1 - u3 &
(u2 - q) - (u3 - q) = u2 - u3 &
(((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q) - (v3 - q) = ((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v3 &
(((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q) - (v3 - q) = ((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v3 )
by Lm4;
then
(
u1 - u3,
((((r * A2) * w) + ((- (r * A1)) * y)) + q) - v3 are_Ort_wrt w,
y &
u2 - u3,
((((r * B2) * w) + ((- (r * B1)) * y)) + q) - v3 are_Ort_wrt w,
y )
by A11, A12, A13, A14;
then
(
u3,
u1,
v3,
(((r * A2) * w) + ((- (r * A1)) * y)) + q are_Ort_wrt w,
y &
u3,
u2,
v3,
(((r * B2) * w) + ((- (r * B1)) * y)) + q are_Ort_wrt w,
y )
by ANALMETR:def 3;
then A16:
(
c,
a _|_ c1,
a1' &
c,
b _|_ c1,
b1' )
by A2, ANALMETR:31;
(
c,
a _|_ c1,
a1 &
c,
b _|_ c1,
b1 )
by A6, ANALMETR:83;
then A17:
(
a1 = a1' &
b1 = b1' )
by A3, A4, A5, A7, A15, A16, Th16;
o,
a // o,
b
by A5, ANALMETR:def 11;
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 a',
b' being
Real such that A18:
a' * (u1 - q) = b' * (u2 - q)
and A19:
(
a' <> 0 or
b' <> 0 )
by ANALMETR:18;
set s =
(b' " ) * a';
A22:
u2 - q =
(b' " ) * (a' * (u1 - q))
by A18, A20, ANALOAF:12
.=
((b' " ) * a') * (u1 - q)
by RLVECT_1:def 9
;
then (B1 * w) + (B2 * y) =
(((b' " ) * a') * (A1 * w)) + (((b' " ) * a') * (A2 * y))
by A12, A13, RLVECT_1:def 9
.=
((((b' " ) * a') * A1) * w) + (((b' " ) * a') * (A2 * y))
by RLVECT_1:def 9
.=
((((b' " ) * a') * A1) * w) + ((((b' " ) * a') * A2) * y)
by RLVECT_1:def 9
;
then A23:
(
B1 = ((b' " ) * a') * A1 &
B2 = ((b' " ) * a') * A2 )
by A1, Lm7;
A24:
((((r * B2) * w) + ((- (r * B1)) * y)) + q) - q =
((r * B2) * w) + ((- (r * B1)) * y)
by RLSUB_2:78
.=
((r * B2) * w) + ((r * B1) * (- y))
by RLVECT_1:38
.=
((r * (((b' " ) * a') * A2)) * w) - ((r * (((b' " ) * a') * A1)) * y)
by A23, RLVECT_1:39
.=
(r * ((((b' " ) * a') * A2) * w)) - ((r * (((b' " ) * a') * A1)) * y)
by RLVECT_1:def 9
.=
(r * ((((b' " ) * a') * A2) * w)) - (r * ((((b' " ) * a') * A1) * y))
by RLVECT_1:def 9
.=
r * (((((b' " ) * a') * A2) * w) - ((((b' " ) * a') * A1) * y))
by RLVECT_1:48
.=
r * ((((b' " ) * a') * (A2 * w)) - ((((b' " ) * a') * A1) * y))
by RLVECT_1:def 9
.=
r * ((((b' " ) * a') * (A2 * w)) - (((b' " ) * a') * (A1 * y)))
by RLVECT_1:def 9
.=
r * (((b' " ) * a') * ((A2 * w) - (A1 * y)))
by RLVECT_1:48
.=
(((b' " ) * a') * r) * ((A2 * w) - (A1 * y))
by RLVECT_1:def 9
.=
((b' " ) * a') * (r * ((A2 * w) - (A1 * y)))
by RLVECT_1:def 9
.=
((b' " ) * a') * ((r * (A2 * w)) - (r * (A1 * y)))
by RLVECT_1:48
.=
((b' " ) * a') * (((r * A2) * w) - (r * (A1 * y)))
by RLVECT_1:def 9
.=
((b' " ) * a') * (((r * A2) * w) + (- ((r * A1) * y)))
by RLVECT_1:def 9
.=
((b' " ) * a') * (((r * A2) * w) + ((r * A1) * (- y)))
by RLVECT_1:39
.=
((b' " ) * a') * (((r * A2) * w) + ((- (r * A1)) * y))
by RLVECT_1:38
.=
((b' " ) * a') * (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q)
by RLSUB_2:78
;
1
* (u2 - ((((r * B2) * w) + ((- (r * B1)) * y)) + q)) =
u2 - ((((r * B2) * w) + ((- (r * B1)) * y)) + q)
by RLVECT_1:def 9
.=
(((b' " ) * a') * (u1 - q)) - (((b' " ) * a') * (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q))
by A22, A24, Lm4
.=
((b' " ) * a') * ((u1 - q) - (((((r * A2) * w) + ((- (r * A1)) * y)) + q) - q))
by RLVECT_1:48
.=
((b' " ) * a') * (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:18;
then
(((r * A2) * w) + ((- (r * A1)) * y)) + q,
u1 '||' (((r * B2) * w) + ((- (r * B1)) * y)) + q,
u2
by GEOMTRAP:def 1;
then
a1',
a // b1',
b
by A2, GEOMTRAP:4;
hence
a,
a1 // b,
b1
by A17, ANALMETR:81;
:: thesis: verum end;
hence
MS is satisfying_LIN
by CONAFFM:def 5; :: thesis: verum