let V be RealLinearSpace; for u, u1, v, v1, x, y being VECTOR of V
for p, q, r, s being Element of (CMSpace (V,x,y)) st u = p & v = q & u1 = r & v1 = s holds
( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
let u, u1, v, v1, x, y be VECTOR of V; for p, q, r, s being Element of (CMSpace (V,x,y)) st u = p & v = q & u1 = r & v1 = s holds
( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
let p, q, r, s be Element of (CMSpace (V,x,y)); ( u = p & v = q & u1 = r & v1 = s implies ( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y ) )
assume that
A1:
u = p
and
A2:
v = q
and
A3:
u1 = r
and
A4:
v1 = s
; ( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
A5:
( p,q _|_ r,s implies u,v,u1,v1 are_COrtm_wrt x,y )
proof
assume
p,
q _|_ r,
s
;
u,v,u1,v1 are_COrtm_wrt x,y
then
[[p,q],[r,s]] in the
orthogonality of
(CMSpace (V,x,y))
by ANALMETR:def 5;
then consider u19,
u29,
v19,
v29 being
VECTOR of
V such that A6:
[u,v] = [u19,u29]
and A7:
[u1,v1] = [v19,v29]
and A8:
u19,
u29,
v19,
v29 are_COrtm_wrt x,
y
by A1, A2, A3, A4, Def6;
A9:
u = u19
by A6, XTUPLE_0:1;
A10:
v = u29
by A6, XTUPLE_0:1;
u1 = v19
by A7, XTUPLE_0:1;
hence
u,
v,
u1,
v1 are_COrtm_wrt x,
y
by A7, A8, A9, A10, XTUPLE_0:1;
verum
end;
( u,v,u1,v1 are_COrtm_wrt x,y implies p,q _|_ r,s )
proof
assume
u,
v,
u1,
v1 are_COrtm_wrt x,
y
;
p,q _|_ r,s
then
[[u,v],[u1,v1]] in the
orthogonality of
OrtStr(# the
carrier of
V,
(CORTM (V,x,y)) #)
by Def6;
hence
p,
q _|_ r,
s
by A1, A2, A3, A4, ANALMETR:def 5;
verum
end;
hence
( p,q _|_ r,s iff u,v,u1,v1 are_COrtm_wrt x,y )
by A5; verum