now for x, y, z being Point of (REAL-US n)
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 x,
y,
z be
Point of
(REAL-US n);
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;
( 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 )
by CARD_1:def 7;
A2:
for
k being
Nat st
k in dom (mlt (x1,x1)) holds
0 <= (mlt (x1,x1)) . k
A3:
x .|. x =
(Euclid_scalar n) . (
x,
x)
by Def6
.=
Sum (mlt (x1,x1))
by Def5
;
hence
0 <= x .|. x
by A2, RVSUM_1:84;
( ( 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) )
( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )proof
now ( x .|. x = 0 implies not x <> 0. (REAL-US n) )assume that A4:
x .|. x = 0
and A5:
x <> 0. (REAL-US n)
;
contradiction
for
k being
Element of
NAT st
k in dom x2 holds
x2 . k = 0
proof
let k be
Element of
NAT ;
( k in dom x2 implies x2 . k = 0 )
dom multreal = [:REAL,REAL:]
by FUNCT_2:def 1;
then
[:(rng x1),(rng x1):] c= dom multreal
by ZFMISC_1:96;
then A6:
dom (multreal .: (x1,x1)) = (dom x1) /\ (dom x1)
by FUNCOP_1:69;
assume
k in dom x2
;
x2 . k = 0
then A7:
k in dom (mlt (x1,x1))
by A6, RVSUM_1:def 9;
then
0 <= (mlt (x1,x1)) . k
by A2;
then
(mlt (x1,x1)) . k = 0
by A3, A2, A4, A7, RVSUM_1:85;
then
(x1 . k) ^2 = 0
by RVSUM_1:59;
hence
x2 . k = 0
by SQUARE_1:12;
verum
end; then
x1 = n |-> 0
by RFUNCT_4:4;
then
x = 0* n
by EUCLID:def 4;
hence
contradiction
by A5, Def6;
verum end;
hence
(
x .|. x = 0 implies
x = 0. (REAL-US n) )
;
( x = 0. (REAL-US n) implies x .|. x = 0 )
assume
x = 0. (REAL-US n)
;
x .|. x = 0
then x =
0* n
by Def6
.=
n |-> 0
by EUCLID:def 4
;
then mlt (
x2,
x2) =
0 * x2
by RVSUM_1:63
.=
n |-> 0
by RVSUM_1:53
;
hence
x .|. x = 0
by A3, RVSUM_1:81;
verum
end; A8:
len z2 = n
by CARD_1:def 7;
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
;
( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )A9:
x .|. z =
(Euclid_scalar n) . (
x,
z)
by Def6
.=
Sum (mlt (x1,z1))
by Def5
;
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;
A10:
for
k being
Nat st
k in Seg n holds
ax . k = (a * x1) . k
A11:
y .|. z =
(Euclid_scalar n) . (
y,
z)
by Def6
.=
Sum (mlt (y1,z1))
by Def5
;
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, A8, RVSUM_1:118
.=
(Sum (mlt (x2,z2))) + (Sum (mlt (y2,z2)))
by RVSUM_1:89
.=
(x .|. z) + (y .|. z)
by A9, A11
;
(a * x) .|. y = a * (x .|. y)thus (a * x) .|. y =
(Euclid_scalar n) . (
(a * x),
y)
by Def6
.=
(Euclid_scalar n) . (
(a * x1),
y1)
by A10, FINSEQ_2:119
.=
Sum (mlt ((a * x1),y1))
by Def5
.=
Sum (a * (mlt (x2,y2)))
by RVSUM_1:65
.=
a * (Sum (mlt (x2,y2)))
by RVSUM_1:87
.=
a * ((Euclid_scalar n) . (x1,y1))
by Def5
.=
a * (x .|. y)
by Def6
;
verum end;
hence
REAL-US n is RealUnitarySpace-like
; ( REAL-US n is vector-distributive & REAL-US n is scalar-distributive & REAL-US n is scalar-associative & REAL-US n is scalar-unital & REAL-US n is Abelian & REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )
A12:
for a, b being Real
for v being VECTOR of (REAL-US n) holds (a * b) * v = a * (b * v)
A14:
for a being Real
for v, w being VECTOR of (REAL-US n) holds a * (v + w) = (a * v) + (a * w)
proof
let a be
Real;
for v, w being VECTOR of (REAL-US n) holds a * (v + w) = (a * v) + (a * w)let v,
w be
VECTOR of
(REAL-US n);
a * (v + w) = (a * v) + (a * w)
reconsider v1 =
v,
w1 =
w as
Element of
REAL n by Def6;
reconsider a =
a as
Real ;
reconsider v2 =
v1,
w2 =
w1 as
Element of
n -tuples_on REAL by EUCLID:def 1;
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;
A15:
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;
for
k being
Nat st
k in Seg n holds
aw . k = (a * w1) . k
then A16:
(
a * v1 is
Element of
n -tuples_on REAL &
a * w1 = a * w )
by EUCLID:def 1, FINSEQ_2:119;
A17:
(a * v) + (a * w) =
(Euclid_add n) . (
(a * v),
(a * w))
by Def6
.=
(Euclid_add n) . (
(a * v1),
(a * w1))
by A15, A16, FINSEQ_2:119
.=
(a * v2) + (a * w2)
by Def1
;
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:51
;
hence
a * (v + w) = (a * v) + (a * w)
by A17;
verum
end;
A18:
for a, b being Real
for v being VECTOR of (REAL-US n) holds (a + b) * v = (a * v) + (b * v)
for v being VECTOR of (REAL-US n) holds 1 * v = v
hence
( REAL-US n is vector-distributive & REAL-US n is scalar-distributive & REAL-US n is scalar-associative & REAL-US n is scalar-unital )
by A14, A18, A12; ( REAL-US n is Abelian & REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )
thus
REAL-US n is Abelian
( 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);
(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;
A22:
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
;
(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:15
;
hence
(u + v) + w = u + (v + w)
by A22, Def1;
verum
end;
hence
REAL-US n is add-associative
; ( 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
; REAL-US n is right_complementable
let v be Element of (REAL-US n); ALGSTR_0:def 16 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
; ALGSTR_0:def 11 v + w = 0. (REAL-US n)
thus v + w =
(Euclid_add n) . (v1,(- v1))
by Def6
.=
v1 + (- v1)
by Def1
.=
0* n
by EUCLIDLP:2
.=
0. (REAL-US n)
by Def6
; verum