set W = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #);
A1:
for u, v, w being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds (u + v) + w = u + (v + w)
A2:
for v being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds v + (0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)) = v
proof
let v be
VECTOR of
UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V, the
scalar of
V #);
v + (0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)) = v
reconsider v9 =
v as
VECTOR of
V ;
thus v + (0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)) =
v9 + (0. V)
.=
v
by RLVECT_1:4
;
verum
end;
A3:
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is right_complementable
proof
let v be
VECTOR of
UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V, the
scalar of
V #);
ALGSTR_0:def 16 v is right_complementable
reconsider v9 =
v as
VECTOR of
V ;
consider w9 being
VECTOR of
V such that A4:
v9 + w9 = 0. V
by ALGSTR_0:def 11;
reconsider w =
w9 as
VECTOR of
UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V, the
scalar of
V #) ;
take
w
;
ALGSTR_0:def 11 v + w = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)
thus
v + w = 0. UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V, the
scalar of
V #)
by A4;
verum
end;
A5:
for v being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds jj * v = v
A6:
for a, b being Real
for v being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds (a + b) * v = (a * v) + (b * v)
A7:
for a being Real
for v, w being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds a * (v + w) = (a * v) + (a * w)
proof
let a be
Real;
for v, w being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds a * (v + w) = (a * v) + (a * w)let v,
w be
VECTOR of
UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V, the
scalar of
V #);
a * (v + w) = (a * v) + (a * w)
reconsider v9 =
v,
w9 =
w as
VECTOR of
V ;
thus a * (v + w) =
a * (v9 + w9)
.=
(a * v9) + (a * w9)
by RLVECT_1:def 5
.=
(a * v) + (a * w)
;
verum
end;
A8:
for a being Real
for v, w being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #)
for v9, w9 being VECTOR of V st v = v9 & w = w9 holds
( v + w = v9 + w9 & a * v = a * v9 & v .|. w = v9 .|. w9 )
;
A9:
for v, w being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds v + w = w + v
A10:
0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = 0. V
;
A11:
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is RealUnitarySpace-like
proof
let x,
y,
z be
VECTOR of
UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V, the
scalar of
V #);
BHSP_1:def 2 for b1 being object holds
( ( not x .|. x = 0 or x = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ) & ( not x = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) or x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (b1 * x) .|. y = b1 * (x .|. y) )let a be
Real;
( ( not x .|. x = 0 or x = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ) & ( not x = 0. UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) or x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
reconsider x9 =
x as
VECTOR of
V ;
reconsider y9 =
y as
VECTOR of
V ;
reconsider z9 =
z as
VECTOR of
V ;
A12:
(x + y) .|. z =
(x9 + y9) .|. z9
.=
(x9 .|. z9) + (y9 .|. z9)
by BHSP_1:def 2
;
x9 .|. x9 = x .|. x
;
hence
(
x .|. x = 0 iff
x = 0. UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V, the
scalar of
V #) )
by A10, BHSP_1:def 2;
( 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
x9 .|. x9 = x .|. x
;
hence
0 <= x .|. x
by BHSP_1:def 2;
( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
x9 .|. y9 = x .|. y
;
hence
x .|. y = y .|. x
by A8;
( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
thus
(x + y) .|. z = (x .|. z) + (y .|. z)
by A12;
(a * x) .|. y = a * (x .|. y)
(a * x) .|. y =
(a * x9) .|. y9
.=
a * (x9 .|. y9)
by BHSP_1:def 2
;
hence
(a * x) .|. y = a * (x .|. y)
;
verum
end;
for a, b being Real
for v being VECTOR of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) holds (a * b) * v = a * (b * v)
then reconsider W = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) as RealUnitarySpace by A9, A1, A2, A3, A7, A6, A5, A11, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;
A13:
( the scalar of W = the scalar of V || the carrier of W & the addF of W = the addF of V || the carrier of W )
by RELSET_1:19;
( 0. W = 0. V & the Mult of W = the Mult of V | [:REAL, the carrier of W:] )
by RELSET_1:19;
hence
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict Subspace of V
by A13, Def1; verum