thus REAL-NS n is RealNormSpace-like :: thesis: ( REAL-NS n is RealLinearSpace-like & REAL-NS n is Abelian & REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )

proof

for x, y being Point of (REAL-NS n)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (REAL-NS n) ) & ( x = 0. (REAL-NS n) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

proof

let x, y be Point of (REAL-NS n); :: thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (REAL-NS n) ) & ( x = 0. (REAL-NS n) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = 0. (REAL-NS n) ) & ( x = 0. (REAL-NS n) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
thus ( ||.x.|| = 0 iff x = 0. (REAL-NS n) ) :: thesis: ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

proof

reconsider x1 = x as Element of REAL n by Def4;
( |.x1.| = 0 iff x1 = 0* n ) by EUCLID:10, EUCLID:11;
hence ( ||.x.|| = 0 iff x = 0. (REAL-NS n) ) by Def4, Th1; :: thesis: verum

end;

thus ||.(a * x).|| = (abs a) * ||.x.|| :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||

proof

reconsider x1 = x as Element of REAL n by Def4;
thus ||.(a * x).|| = |.(a * x1).| by Th1, Th3
.= (abs a) * |.x1.| by EUCLID:14
.= (abs a) * ||.x.|| by Th1 ; :: thesis: verum

end;

thus ||.(x + y).|| <= ||.x.|| + ||.y.|| :: thesis: verum

proof

reconsider x1 = x, y1 = y as Element of REAL n by Def4;
A1: ||.(x + y).|| = |.(x1 + y1).| by Th1, Th2;
|.(x1 + y1).| <= |.x1.| + |.y1.| by EUCLID:15;
then |.(x1 + y1).| <= ||.x.|| + |.y1.| by Th1;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A1, Th1; :: thesis: verum

end;

end;

hence REAL-NS n is RealNormSpace-like by NORMSP_1:def 2; :: thesis: verum

end;

thus REAL-NS n is RealLinearSpace-like :: thesis: ( REAL-NS n is Abelian & REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )

proof

A2: for a being real number
for v, w being VECTOR of (REAL-NS n) holds a * (v + w) = (a * v) + (a * w)

proof

let a be real number ; :: thesis: for v, w being VECTOR of (REAL-NS 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-NS n); :: thesis: a * (v + w) = (a * v) + (a * w)
a * (v + w) = (a * v) + (a * w)

proof

reconsider v1 = v, w1 = w as Element of REAL n by Def4;
A3: a * v = a * v1 by Th3;
A4: a * w = a * w1 by Th3;
reconsider v2 = v1, w2 = w1 as Element of n -tuples_on REAL by EUCLID:def 1;
thus a * (v + w) = (Euclid_mult n) . a,(v + w) by Def4
.= (Euclid_mult n) . a,(v1 + w1) by Th2
.= a * (v2 + w2) by Def2
.= (a * v2) + (a * w2) by RVSUM_1:73
.= (a * v) + (a * w) by A3, A4, Th2 ; :: thesis: verum

end;

hence a * (v + w) = (a * v) + (a * w) ; :: thesis: verum

end;

A5: for a, b being real number
for v being VECTOR of (REAL-NS n) holds (a + b) * v = (a * v) + (b * v)

proof

let a, b be real number ; :: thesis: for v being VECTOR of (REAL-NS n) holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real by XREAL_0:def 1;
let v be VECTOR of (REAL-NS n); :: thesis: (a + b) * v = (a * v) + (b * v)
(a + b) * v = (a * v) + (b * v)

proof

reconsider v1 = v as Element of REAL n by Def4;
A6: a * v = a * v1 by Th3;
A7: b * v = b * v1 by Th3;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
thus (a + b) * v = (Euclid_mult n) . (a + b),v by Def4
.= (a + b) * v2 by Def2
.= (a * v2) + (b * v2) by RVSUM_1:72
.= (a * v) + (b * v) by A6, A7, Th2 ; :: thesis: verum

end;

hence (a + b) * v = (a * v) + (b * v) ; :: thesis: verum

end;

A8: for a, b being real number
for v being VECTOR of (REAL-NS n) holds (a * b) * v = a * (b * v)

proof

let a, b be real number ; :: thesis: for v being VECTOR of (REAL-NS n) holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real by XREAL_0:def 1;
let v be VECTOR of (REAL-NS n); :: thesis: (a * b) * v = a * (b * v)
(a * b) * v = a * (b * v)

proof

reconsider v1 = v as Element of REAL n by Def4;
A9: b * v = b * v1 by Th3;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
(a * b) * v = (Euclid_mult n) . (a * b),v by Def4
.= (a * b) * v1 by Def2
.= a * (b * v2) by RVSUM_1:71 ;
hence (a * b) * v = a * (b * v) by A9, Th3; :: thesis: verum

end;

hence (a * b) * v = a * (b * v) ; :: thesis: verum

end;

for v being VECTOR of (REAL-NS n) holds 1 * v = v

proof

let v be VECTOR of (REAL-NS n); :: thesis: 1 * v = v
thus 1 * v = v :: thesis: verum

proof

reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
thus 1 * v = (Euclid_mult n) . 1,v by Def4
.= 1 * v2 by Def2
.= v by RVSUM_1:74 ; :: thesis: verum

end;

end;

hence REAL-NS n is RealLinearSpace-like by A2, A5, A8, RLVECT_1:def 9; :: thesis: verum

end;

thus REAL-NS n is Abelian :: thesis: ( REAL-NS n is add-associative & REAL-NS n is right_zeroed & REAL-NS n is right_complementable )

proof

for v, w being VECTOR of (REAL-NS n) holds v + w = w + v

proof

let v, w be VECTOR of (REAL-NS n); :: thesis: v + w = w + v
thus v + w = w + v :: thesis: verum

proof

reconsider v1 = v, w1 = w as Element of REAL n by Def4;
thus v + w = (Euclid_add n) . v,w by Def4
.= (Euclid_add n) . w1,v1 by BINOP_1:def 2
.= w + v by Def4 ; :: thesis: verum

end;

end;

hence REAL-NS n is Abelian by RLVECT_1:def 5; :: thesis: verum

end;

thus REAL-NS n is add-associative :: thesis: ( REAL-NS n is right_zeroed & REAL-NS n is right_complementable )

proof

for u, v, w being VECTOR of (REAL-NS n) holds (u + v) + w = u + (v + w)

proof

let u, v, w be VECTOR of (REAL-NS n); :: thesis: (u + v) + w = u + (v + w)
thus (u + v) + w = u + (v + w) :: thesis: verum

proof

reconsider u1 = u, v1 = v, w1 = w as Element of REAL n by Def4;
A10: v + w = v1 + w1 by Th2;
thus (u + v) + w = (Euclid_add n) . (the addF of (REAL-NS n) . u,v),w by Def4
.= (Euclid_add n) . ((Euclid_add n) . u1,v1),w1 by Def4
.= (Euclid_add n) . u1,((Euclid_add n) . v1,w1) by BINOP_1:def 3
.= (Euclid_add n) . u1,(v1 + w1) by Def1
.= u1 + (v1 + w1) by Def1
.= u + (v + w) by A10, Th2 ; :: thesis: verum

end;

end;

hence REAL-NS n is add-associative by RLVECT_1:def 6; :: thesis: verum

end;

thus REAL-NS n is right_zeroed :: thesis: REAL-NS n is right_complementable

proof

for v being VECTOR of (REAL-NS n) holds v + (0. (REAL-NS n)) = v

proof

let v be VECTOR of (REAL-NS n); :: thesis: v + (0. (REAL-NS n)) = v
thus v + (0. (REAL-NS n)) = v :: thesis: verum

proof

reconsider v1 = v as Element of REAL n by Def4;
A11: 0. (REAL-NS n) = 0* n by Def4;
reconsider zero = n |-> 0 as Element of n -tuples_on REAL by FINSEQ_2:132;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
thus v + (0. (REAL-NS n)) = v1 + (0* n) by A11, Th2
.= v2 + zero by EUCLID:def 4
.= v by RVSUM_1:33 ; :: thesis: verum

end;

end;

hence REAL-NS n is right_zeroed by RLVECT_1:def 7; :: thesis: verum

end;

REAL-NS n is right_complementable

proof

let v be VECTOR of (REAL-NS n); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
thus ex w being VECTOR of (REAL-NS n) st v + w = 0. (REAL-NS n) :: according to ALGSTR_0:def 11 :: thesis: verum

proof

reconsider v1 = v as Element of REAL n by Def4;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
A12: 0. (REAL-NS n) = 0* n by Def4
.= n |-> 0 by EUCLID:def 4 ;
reconsider w = - v1 as VECTOR of (REAL-NS n) by Def4;
take w ; :: thesis: v + w = 0. (REAL-NS n)
thus v + w = v2 + (- v2) by Th2
.= 0. (REAL-NS n) by A12, RVSUM_1:40 ; :: thesis: verum

end;

end;

hence REAL-NS n is right_complementable ; :: thesis: verum