thus
REAL-US n is RealUnitarySpace-like
:: thesis: ( REAL-US n is RealLinearSpace-like & REAL-US n is Abelian & REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )proof
now let x,
y,
z be
Point of
(REAL-US n);
:: thesis: for a being Real holds
( 0 <= x .|. x & ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )let a be
Real;
:: thesis: ( 0 <= x .|. x & ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )reconsider x1 =
x,
y1 =
y,
z1 =
z as
Element of
REAL n by Def6;
reconsider x2 =
x1,
y2 =
y1,
z2 =
z1 as
Element of
n -tuples_on REAL by EUCLID:def 1;
A1:
(
len x2 = n &
len y2 = n &
len z2 = n )
by FINSEQ_1:def 18;
A2:
x .|. x =
(Euclid_scalar n) . x,
x
by Def6
.=
Sum (mlt x1,x1)
by Def5
;
A3:
x .|. z =
(Euclid_scalar n) . x,
z
by Def6
.=
Sum (mlt x1,z1)
by Def5
;
A4:
y .|. z =
(Euclid_scalar n) . y,
z
by Def6
.=
Sum (mlt y1,z1)
by Def5
;
A5:
for
k being
Nat st
k in dom (mlt x1,x1) holds
0 <= (mlt x1,x1) . k
hence
0 <= x .|. x
by A2, RVSUM_1:114;
:: thesis: ( ( x .|. x = 0 implies x = 0. (REAL-US n) ) & ( x = 0. (REAL-US n) implies x .|. x = 0 ) & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
(
x .|. x = 0 iff
x = 0. (REAL-US n) )
:: thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )proof
now assume A6:
(
x .|. x = 0 &
x <> 0. (REAL-US n) )
;
:: thesis: contradiction
for
k being
Element of
NAT st
k in dom x2 holds
x2 . k = 0
proof
let k be
Element of
NAT ;
:: thesis: ( k in dom x2 implies x2 . k = 0 )
assume A7:
k in dom x2
;
:: thesis: x2 . k = 0
dom multreal = [:REAL ,REAL :]
by FUNCT_2:def 1;
then
[:(rng x1),(rng x1):] c= dom multreal
by ZFMISC_1:119;
then
dom (multreal .: x1,x1) = (dom x1) /\ (dom x1)
by FUNCOP_1:84;
then A8:
k in dom (mlt x1,x1)
by A7, RVSUM_1:def 9;
then
(
0 <= (mlt x1,x1) . k &
(mlt x1,x1) . k <= 0 )
by A2, A5, A6, RVSUM_1:115;
then
(mlt x1,x1) . k = 0
;
then
(x1 . k) ^2 = 0
by A8, RVSUM_1:86;
hence
x2 . k = 0
by SQUARE_1:74;
:: thesis: verum
end; then
x1 = n |-> 0
by RFUNCT_4:4;
then
x = 0* n
by EUCLID:def 4;
hence
contradiction
by A6, Def6;
:: thesis: verum end;
hence
(
x .|. x = 0 implies
x = 0. (REAL-US n) )
;
:: thesis: ( x = 0. (REAL-US n) implies x .|. x = 0 )
assume
x = 0. (REAL-US n)
;
:: thesis: x .|. x = 0
then x =
0* n
by Def6
.=
n |-> 0
by EUCLID:def 4
;
then mlt x2,
x2 =
0 * x2
by RVSUM_1:92
.=
n |-> 0
by RVSUM_1:75
;
hence
x .|. x = 0
by A2, RVSUM_1:111;
:: thesis: verum
end; thus x .|. y =
(Euclid_scalar n) . x,
y
by Def6
.=
Sum (mlt y1,x1)
by Def5
.=
(Euclid_scalar n) . y,
x
by Def5
.=
y .|. x
by Def6
;
:: thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus (x + y) .|. z =
(Euclid_scalar n) . (x + y),
z
by Def6
.=
(Euclid_scalar n) . ((Euclid_add n) . x1,y1),
z1
by Def6
.=
(Euclid_scalar n) . (x1 + y1),
z1
by Def1
.=
Sum (mlt (x1 + y1),z1)
by Def5
.=
Sum ((mlt x1,z1) + (mlt y1,z1))
by A1, EUCLID_2:9
.=
(Sum (mlt x2,z2)) + (Sum (mlt y2,z2))
by RVSUM_1:119
.=
(x .|. z) + (y .|. z)
by A3, A4
;
:: thesis: (a * x) .|. y = a * (x .|. y)
a * x is
Element of
REAL n
by Def6;
then reconsider ax =
a * x as
Element of
n -tuples_on REAL by EUCLID:def 1;
A9:
a * x1 is
Element of
n -tuples_on REAL
by EUCLID:def 1;
A10:
for
k being
Nat st
k in Seg n holds
ax . k = (a * x1) . k
thus (a * x) .|. y =
(Euclid_scalar n) . (a * x),
y
by Def6
.=
(Euclid_scalar n) . (a * x1),
y1
by A9, A10, FINSEQ_2:139
.=
Sum (mlt (a * x1),y1)
by Def5
.=
Sum (a * (mlt x2,y2))
by RVSUM_1:94
.=
a * (Sum (mlt x2,y2))
by RVSUM_1:117
.=
a * ((Euclid_scalar n) . x1,y1)
by Def5
.=
a * (x .|. y)
by Def6
;
:: thesis: verum end;
hence
REAL-US n is
RealUnitarySpace-like
by BHSP_1:def 2;
:: thesis: verum
end;
thus
REAL-US n is RealLinearSpace-like
:: thesis: ( REAL-US n is Abelian & REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )proof
thus
for
a being
real number for
v,
w being
VECTOR of
(REAL-US n) holds
a * (v + w) = (a * v) + (a * w)
:: according to RLVECT_1:def 9 :: thesis: ( ( for b1, b2 being set
for b3 being Element of the carrier of (REAL-US n) holds (b1 + b2) * b3 = (b1 * b3) + (b2 * b3) ) & ( for b1, b2 being set
for b3 being Element of the carrier of (REAL-US n) holds (b1 * b2) * b3 = b1 * (b2 * b3) ) & ( for b1 being Element of the carrier of (REAL-US n) holds 1 * b1 = b1 ) )proof
let a be
real number ;
:: thesis: for v, w being VECTOR of (REAL-US n) holds a * (v + w) = (a * v) + (a * w)
reconsider a =
a as
Real by XREAL_0:def 1;
let v,
w be
VECTOR of
(REAL-US n);
:: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v1 =
v,
w1 =
w as
Element of
REAL n by Def6;
reconsider v2 =
v1,
w2 =
w1 as
Element of
n -tuples_on REAL by EUCLID:def 1;
A11:
a * (v + w) =
(Euclid_mult n) . a,
(v + w)
by Def6
.=
(Euclid_mult n) . a,
((Euclid_add n) . v1,w1)
by Def6
.=
(Euclid_mult n) . a,
(v1 + w1)
by Def1
.=
a * (v1 + w1)
by Def2
.=
(a * v2) + (a * w2)
by RVSUM_1:73
;
a * v is
Element of
REAL n
by Def6;
then reconsider av =
a * v as
Element of
n -tuples_on REAL by EUCLID:def 1;
A12:
a * v1 is
Element of
n -tuples_on REAL
by EUCLID:def 1;
A13:
for
k being
Nat st
k in Seg n holds
av . k = (a * v1) . k
a * w is
Element of
REAL n
by Def6;
then reconsider aw =
a * w as
Element of
n -tuples_on REAL by EUCLID:def 1;
A14:
a * w1 is
Element of
n -tuples_on REAL
by EUCLID:def 1;
for
k being
Nat st
k in Seg n holds
aw . k = (a * w1) . k
then A15:
a * w1 = a * w
by A14, FINSEQ_2:139;
(a * v) + (a * w) =
(Euclid_add n) . (a * v),
(a * w)
by Def6
.=
(Euclid_add n) . (a * v1),
(a * w1)
by A12, A13, A15, FINSEQ_2:139
.=
(a * v2) + (a * w2)
by Def1
;
hence
a * (v + w) = (a * v) + (a * w)
by A11;
:: thesis: verum
end;
thus
for
a,
b being
real number for
v being
VECTOR of
(REAL-US n) holds
(a + b) * v = (a * v) + (b * v)
:: thesis: ( ( for b1, b2 being set
for b3 being Element of the carrier of (REAL-US n) holds (b1 * b2) * b3 = b1 * (b2 * b3) ) & ( for b1 being Element of the carrier of (REAL-US n) holds 1 * b1 = b1 ) )
thus
for
a,
b being
real number for
v being
VECTOR of
(REAL-US n) holds
(a * b) * v = a * (b * v)
:: thesis: for b1 being Element of the carrier of (REAL-US n) holds 1 * b1 = b1
for
v being
VECTOR of
(REAL-US n) holds 1
* v = v
hence
for
b1 being
Element of the
carrier of
(REAL-US n) holds 1
* b1 = b1
;
:: thesis: verum
end;
thus
REAL-US n is Abelian
:: thesis: ( REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )
for u, v, w being Element of (REAL-US n) holds (u + v) + w = u + (v + w)
proof
let u,
v,
w be
Element of
(REAL-US n);
:: thesis: (u + v) + w = u + (v + w)
reconsider u1 =
u,
v1 =
v,
w1 =
w as
Element of
REAL n by Def6;
reconsider u2 =
u1,
v2 =
v1,
w2 =
w1 as
Element of
n -tuples_on REAL by EUCLID:def 1;
A24:
(u + v) + w =
(Euclid_add n) . (u + v),
w1
by Def6
.=
(Euclid_add n) . ((Euclid_add n) . u1,v1),
w1
by Def6
.=
(Euclid_add n) . (u1 + v1),
w1
by Def1
.=
(u1 + v1) + w2
by Def1
.=
u2 + (v2 + w2)
by RVSUM_1:32
;
u + (v + w) =
(Euclid_add n) . u1,
(v + w)
by Def6
.=
(Euclid_add n) . u2,
((Euclid_add n) . v2,w2)
by Def6
.=
(Euclid_add n) . u2,
(v1 + w1)
by Def1
;
hence
(u + v) + w = u + (v + w)
by A24, Def1;
:: thesis: verum
end;
hence
REAL-US n is add-associative
by RLVECT_1:def 6; :: thesis: ( REAL-US n is right_zeroed & REAL-US n is right_complementable )
for v being Element of (REAL-US n) holds v + (0. (REAL-US n)) = v
hence
REAL-US n is right_zeroed
by RLVECT_1:def 7; :: thesis: REAL-US n is right_complementable
let v be Element of (REAL-US n); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v1 = v as Element of REAL n by Def6;
reconsider w = - v1 as Element of (REAL-US n) by Def6;
take
w
; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. (REAL-US n)
thus v + w =
(Euclid_add n) . v1,(- v1)
by Def6
.=
v1 + (- v1)
by Def1
.=
0* n
by EUCLIDLP:7
.=
0. (REAL-US n)
by Def6
; :: thesis: verum