let V be RealLinearSpace; for u1, u2, v, w, y being VECTOR of V st Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v <> 0. V holds
ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
let u1, u2, v, w, y be VECTOR of V; ( Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v <> 0. V implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )
assume that
A1:
Gen w,y
and
A2:
v,u1 are_Ort_wrt w,y
and
A3:
v,u2 are_Ort_wrt w,y
and
A4:
v <> 0. V
; ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
consider a1, a2, b1, b2 being Real such that
A5:
v = (a1 * w) + (a2 * y)
and
A6:
u1 = (b1 * w) + (b2 * y)
and
A7:
(a1 * b1) + (a2 * b2) = 0
by A2;
consider a19, a29, c1, c2 being Real such that
A8:
v = (a19 * w) + (a29 * y)
and
A9:
u2 = (c1 * w) + (c2 * y)
and
A10:
(a19 * c1) + (a29 * c2) = 0
by A3;
A11:
a2 = a29
by A1, A5, A8, Lm4;
A12:
a1 = a19
by A1, A5, A8, Lm4;
A13:
now ( a1 = 0 implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )assume A14:
a1 = 0
;
ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )then A15:
a2 <> 0
by A4, A5, Lm2;
then
c2 = 0
by A10, A12, A11, A14, XCMPLX_1:6;
then
u2 = (c1 * w) + (0. V)
by A9, RLVECT_1:10;
then A16:
u2 = c1 * w
by RLVECT_1:4;
b2 = 0
by A7, A14, A15, XCMPLX_1:6;
then A17:
u1 = (b1 * w) + (0. V)
by A6, RLVECT_1:10;
then A18:
u1 = b1 * w
by RLVECT_1:4;
A19:
now ( b1 = 0 implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )end; c1 * u1 =
c1 * (b1 * w)
by A17, RLVECT_1:4
.=
(b1 * c1) * w
by RLVECT_1:def 7
.=
b1 * u2
by A16, RLVECT_1:def 7
;
hence
ex
a,
b being
Real st
(
a * u1 = b * u2 & (
a <> 0 or
b <> 0 ) )
by A19;
verum end;
now ( a1 <> 0 implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )A20:
c2 * (((- a2) * b2) * (a1 ")) = b2 * (((- a2) * c2) * (a1 "))
;
assume A21:
a1 <> 0
;
ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )A22:
b1 =
1
* b1
.=
(a1 * (a1 ")) * b1
by A21, XCMPLX_0:def 7
.=
(a1 * b1) * (a1 ")
.=
((- a2) * b2) * (a1 ")
by A7
;
A23:
c1 =
1
* c1
.=
(a1 * (a1 ")) * c1
by A21, XCMPLX_0:def 7
.=
(a1 * c1) * (a1 ")
.=
((- a2) * c2) * (a1 ")
by A1, A5, A8, A10, A11, Lm4
;
then A24:
b2 * u2 = ((b2 * (((- a2) * c2) * (a1 "))) * w) + ((b2 * c2) * y)
by A9, Lm3;
A25:
now ( ( c2 <> 0 or b2 <> 0 ) implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )end; now ( b2 = 0 & c2 = 0 implies ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) ) )end; hence
ex
a,
b being
Real st
(
a * u1 = b * u2 & (
a <> 0 or
b <> 0 ) )
by A25;
verum end;
hence
ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
by A13; verum