let V be RealLinearSpace; for u, v, w, y being VECTOR of V st Gen w,y holds
( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 )
let u, v, w, y be VECTOR of V; ( Gen w,y implies ( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 ) )
assume A1:
Gen w,y
; ( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 )
hereby ( ( for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 ) implies u,v are_Ort_wrt w,y )
assume
u,
v are_Ort_wrt w,
y
;
for a19, a29, b19, b29 being Real st u = (a19 * w) + (a29 * y) & v = (b19 * w) + (b29 * y) holds
0 = (a19 * b19) + (a29 * b29)then consider a1,
a2,
b1,
b2 being
Real such that A2:
u = (a1 * w) + (a2 * y)
and A3:
v = (b1 * w) + (b2 * y)
and A4:
(a1 * b1) + (a2 * b2) = 0
;
let a19,
a29,
b19,
b29 be
Real;
( u = (a19 * w) + (a29 * y) & v = (b19 * w) + (b29 * y) implies 0 = (a19 * b19) + (a29 * b29) )assume that A5:
u = (a19 * w) + (a29 * y)
and A6:
v = (b19 * w) + (b29 * y)
;
0 = (a19 * b19) + (a29 * b29)A7:
b1 = b19
by A1, A3, A6, Lm4;
(
a1 = a19 &
a2 = a29 )
by A1, A2, A5, Lm4;
hence
0 = (a19 * b19) + (a29 * b29)
by A1, A3, A4, A6, A7, Lm4;
verum
end;
consider a1, a2 being Real such that
A8:
u = (a1 * w) + (a2 * y)
by A1;
consider b1, b2 being Real such that
A9:
v = (b1 * w) + (b2 * y)
by A1;
assume
for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0
; u,v are_Ort_wrt w,y
then
(a1 * b1) + (a2 * b2) = 0
by A8, A9;
hence
u,v are_Ort_wrt w,y
by A8, A9; verum