now :: thesis: 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); :: 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 ) by CARD_1:def 7;
A2: for k being Nat st k in dom (mlt (x1,x1)) holds
0 <= (mlt (x1,x1)) . k
proof
let k be Nat; :: thesis: ( k in dom (mlt (x1,x1)) implies 0 <= (mlt (x1,x1)) . k )
assume k in dom (mlt (x1,x1)) ; :: thesis: 0 <= (mlt (x1,x1)) . k
(mlt (x1,x1)) . k = (x1 . k) * (x1 . k) by RVSUM_1:59;
hence 0 <= (mlt (x1,x1)) . k by XREAL_1:63; :: thesis: verum
end;
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; :: 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 :: thesis: ( x .|. x = 0 implies not x <> 0. (REAL-US n) )
assume that
A4: x .|. x = 0 and
A5: 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 )
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 ; :: thesis: 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; :: thesis: verum
end;
then x1 = n |-> 0 by RFUNCT_4:4;
then x = 0* n by EUCLID:def 4;
hence contradiction by A5, 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:63
.= n |-> 0 by RVSUM_1:53 ;
hence x .|. x = 0 by A3, RVSUM_1:81; :: thesis: 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 ; :: thesis: ( (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
proof
reconsider a = a as Real ;
let k be Nat; :: thesis: ( k in Seg n implies ax . k = (a * x1) . k )
assume k in Seg n ; :: thesis: ax . k = (a * x1) . k
a * x = (Euclid_mult n) . (a,x1) by Def6
.= a * x1 by Def2 ;
hence ax . k = (a * x1) . k ; :: thesis: verum
end;
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 ; :: thesis: (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 ; :: thesis: verum
end;
hence REAL-US n is RealUnitarySpace-like ; :: thesis: ( 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)
proof
let a, b be Real; :: thesis: for v being VECTOR of (REAL-US n) holds (a * b) * v = a * (b * v)
let v be VECTOR of (REAL-US n); :: thesis: (a * b) * v = a * (b * v)
reconsider v1 = v as Element of REAL n by Def6;
reconsider a = a, b = b as Real ;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
b * v is Element of REAL n by Def6;
then reconsider bv = b * v as Element of n -tuples_on REAL by EUCLID:def 1;
for k being Nat st k in Seg n holds
bv . k = (b * v1) . k
proof
reconsider b = b as Element of REAL by XREAL_0:def 1;
let k be Nat; :: thesis: ( k in Seg n implies bv . k = (b * v1) . k )
assume k in Seg n ; :: thesis: bv . k = (b * v1) . k
b * v = (Euclid_mult n) . (b,v1) by Def6
.= b * v1 by Def2 ;
hence bv . k = (b * v1) . k ; :: thesis: verum
end;
then b * v1 = b * v by FINSEQ_2:119;
then A13: a * (b * v) = (Euclid_mult n) . (a,(b * v1)) by Def6
.= a * (b * v2) by Def2 ;
(a * b) * v = (Euclid_mult n) . ((a * b),v1) by Def6
.= (a * b) * v2 by Def2
.= a * (b * v2) by RVSUM_1:49 ;
hence (a * b) * v = a * (b * v) by A13; :: thesis: verum
end;
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; :: thesis: 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); :: thesis: 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
proof
let k be Nat; :: thesis: ( k in Seg n implies av . k = (a * v1) . k )
assume k in Seg n ; :: thesis: av . k = (a * v1) . k
a * v = (Euclid_mult n) . (a,v1) by Def6
.= a * v1 by Def2 ;
hence av . k = (a * v1) . k ; :: thesis: verum
end;
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
proof
reconsider a = a as Element of REAL by XREAL_0:def 1;
let k be Nat; :: thesis: ( k in Seg n implies aw . k = (a * w1) . k )
assume k in Seg n ; :: thesis: aw . k = (a * w1) . k
a * w = (Euclid_mult n) . (a,w1) by Def6
.= a * w1 by Def2 ;
hence aw . k = (a * w1) . k ; :: thesis: verum
end;
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; :: thesis: verum
end;
A18: for a, b being Real
for v being VECTOR of (REAL-US n) holds (a + b) * v = (a * v) + (b * v)
proof
let a, b be Real; :: thesis: for v being VECTOR of (REAL-US n) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of (REAL-US n); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v1 = v as Element of REAL n by Def6;
reconsider a = a, b = b as Real ;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
A19: (a + b) * v = (Euclid_mult n) . ((a + b),v1) by Def6
.= (a + b) * v2 by Def2
.= (a * v1) + (b * v1) by RVSUM_1:50 ;
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;
A20: for k being Nat st k in Seg n holds
av . k = (a * v1) . k
proof
reconsider a = a as Element of REAL by XREAL_0:def 1;
let k be Nat; :: thesis: ( k in Seg n implies av . k = (a * v1) . k )
assume k in Seg n ; :: thesis: av . k = (a * v1) . k
a * v = (Euclid_mult n) . (a,v1) by Def6
.= a * v1 by Def2 ;
hence av . k = (a * v1) . k ; :: thesis: verum
end;
b * v is Element of REAL n by Def6;
then reconsider bv = b * v as Element of n -tuples_on REAL by EUCLID:def 1;
for k being Nat st k in Seg n holds
bv . k = (b * v1) . k
proof
reconsider b = b as Element of REAL by XREAL_0:def 1;
let k be Nat; :: thesis: ( k in Seg n implies bv . k = (b * v1) . k )
assume k in Seg n ; :: thesis: bv . k = (b * v1) . k
b * v = (Euclid_mult n) . (b,v1) by Def6
.= b * v1 by Def2 ;
hence bv . k = (b * v1) . k ; :: thesis: verum
end;
then A21: ( a * v1 is Element of n -tuples_on REAL & b * v1 = b * v ) by EUCLID:def 1, FINSEQ_2:119;
(a * v) + (b * v) = (Euclid_add n) . ((a * v),(b * v)) by Def6
.= (Euclid_add n) . ((a * v1),(b * v1)) by A20, A21, FINSEQ_2:119
.= (a * v2) + (b * v2) by Def1 ;
hence (a + b) * v = (a * v) + (b * v) by A19; :: thesis: verum
end;
for v being VECTOR of (REAL-US n) holds 1 * v = v
proof
let v be VECTOR of (REAL-US n); :: thesis: 1 * v = v
reconsider v1 = v as Element of REAL n by Def6;
reconsider v2 = v1 as Element of n -tuples_on REAL by EUCLID:def 1;
1 * v = (Euclid_mult n) . (1,v1) by Def6
.= 1 * v2 by Def2
.= v2 by RVSUM_1:52 ;
hence 1 * v = v ; :: thesis: verum
end;
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; :: thesis: ( 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 :: thesis: ( REAL-US n is add-associative & REAL-US n is right_zeroed & REAL-US n is right_complementable )
proof
let v, w be VECTOR of (REAL-US n); :: according to RLVECT_1:def 2 :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as Element of REAL n by Def6;
thus v + w = (Euclid_add n) . (v,w) by Def6
.= (Euclid_add n) . (w1,v1) by BINOP_1:def 2
.= w + v by Def6 ; :: thesis: verum
end;
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;
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; :: thesis: verum
end;
hence REAL-US n is add-associative ; :: 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
proof
let v be Element of (REAL-US n); :: thesis: v + (0. (REAL-US n)) = v
reconsider v1 = v as Element of REAL n by Def6;
v + (0. (REAL-US n)) = (Euclid_add n) . (v,(0. (REAL-US n))) by Def6
.= (Euclid_add n) . (v1,(0* n)) by Def6
.= v1 + (0* n) by Def1 ;
hence v + (0. (REAL-US n)) = v by EUCLID_4:1; :: thesis: verum
end;
hence REAL-US n is right_zeroed ; :: 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:2
.= 0. (REAL-US n) by Def6 ; :: thesis: verum