let MS be OrtAfPl; 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; 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; ( 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)
; MS is Homogeneous
now 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,c1let o,
a,
a1,
b,
b1,
c,
c1 be
Element of
MS;
( 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 )
;
b,c _|_ b1,c1reconsider 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 )
then A10:
o <> a
by Th1;
now ( 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
;
b,c _|_ b1,c1then
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;
verum end; hence
b,
c _|_ b1,
c1
by A4, A5, A6, A7, A8, Th21;
verum end;
hence
MS is Homogeneous
; verum