let V be RealUnitarySpace; :: thesis: for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:REAL,D:],D
for S being Function of [:D,D:],REAL st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] & S = the scalar of V || V1 holds
UNITSTR(# D,d1,A,M,S #) is Subspace of V
let V1 be Subset of V; :: thesis: for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:REAL,D:],D
for S being Function of [:D,D:],REAL st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] & S = the scalar of V || V1 holds
UNITSTR(# D,d1,A,M,S #) is Subspace of V
let D be non empty set ; :: thesis: for d1 being Element of D
for A being BinOp of D
for M being Function of [:REAL,D:],D
for S being Function of [:D,D:],REAL st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] & S = the scalar of V || V1 holds
UNITSTR(# D,d1,A,M,S #) is Subspace of V
let d1 be Element of D; :: thesis: for A being BinOp of D
for M being Function of [:REAL,D:],D
for S being Function of [:D,D:],REAL st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] & S = the scalar of V || V1 holds
UNITSTR(# D,d1,A,M,S #) is Subspace of V
let A be BinOp of D; :: thesis: for M being Function of [:REAL,D:],D
for S being Function of [:D,D:],REAL st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] & S = the scalar of V || V1 holds
UNITSTR(# D,d1,A,M,S #) is Subspace of V
let M be Function of [:REAL,D:],D; :: thesis: for S being Function of [:D,D:],REAL st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] & S = the scalar of V || V1 holds
UNITSTR(# D,d1,A,M,S #) is Subspace of V
let S be Function of [:D,D:],REAL; :: thesis: ( V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] & S = the scalar of V || V1 implies UNITSTR(# D,d1,A,M,S #) is Subspace of V )
assume that
A1: V1 = D and
A2: d1 = 0. V and
A3: A = the addF of V || V1 and
A4: M = the Mult of V | [:REAL,V1:] and
A5: S = the scalar of V || V1 ; :: thesis: UNITSTR(# D,d1,A,M,S #) is Subspace of V
UNITSTR(# D,d1,A,M,S #) is Subspace of V
proof
set W = UNITSTR(# D,d1,A,M,S #);
A6: for a being Real
for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds a * x = the Mult of V . [a,x]
proof
let a be Real; :: thesis: for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds a * x = the Mult of V . [a,x]
let x be VECTOR of UNITSTR(# D,d1,A,M,S #); :: thesis: a * x = the Mult of V . [a,x]
reconsider a = a as Element of REAL by XREAL_0:def 1;
a * x = the Mult of V . [a,x] by A1, A4, FUNCT_1:49;
hence a * x = the Mult of V . [a,x] ; :: thesis: verum
end;
A7: for x, y being VECTOR of UNITSTR(# D,d1,A,M,S #) holds x .|. y = the scalar of V . [x,y] by A1, A5, FUNCT_1:49;
A8: for x, y being VECTOR of UNITSTR(# D,d1,A,M,S #) holds x + y = the addF of V . [x,y] by A1, A3, FUNCT_1:49;
A9: ( UNITSTR(# D,d1,A,M,S #) is RealUnitarySpace-like & UNITSTR(# D,d1,A,M,S #) is vector-distributive & UNITSTR(# D,d1,A,M,S #) is scalar-distributive & UNITSTR(# D,d1,A,M,S #) is scalar-associative & UNITSTR(# D,d1,A,M,S #) is scalar-unital & UNITSTR(# D,d1,A,M,S #) is Abelian & UNITSTR(# D,d1,A,M,S #) is add-associative & UNITSTR(# D,d1,A,M,S #) is right_zeroed & UNITSTR(# D,d1,A,M,S #) is right_complementable )
proof
set SV = the scalar of V;
set MV = the Mult of V;
set AV = the addF of V;
A10: for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds jj * x = x
proof
let x be VECTOR of UNITSTR(# D,d1,A,M,S #); :: thesis: jj * x = x
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
thus jj * x = jj * y by A6
.= x by RLVECT_1:def 8 ; :: thesis: verum
end;
A11: for a, b being Real
for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds (a * b) * x = a * (b * x)
proof
let a, b be Real; :: thesis: for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds (a * b) * x = a * (b * x)
let x be VECTOR of UNITSTR(# D,d1,A,M,S #); :: thesis: (a * b) * x = a * (b * x)
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
reconsider a = a, b = b as Element of REAL by XREAL_0:def 1;
(a * b) * x = (a * b) * y by A6
.= a * (b * y) by RLVECT_1:def 7
.= the Mult of V . [a,(b * x)] by A6
.= a * (b * x) by A1, A4, FUNCT_1:49 ;
hence (a * b) * x = a * (b * x) ; :: thesis: verum
end;
A12: for a being Real
for x, y being VECTOR of UNITSTR(# D,d1,A,M,S #) holds a * (x + y) = (a * x) + (a * y)
proof
let a be Real; :: thesis: for x, y being VECTOR of UNITSTR(# D,d1,A,M,S #) holds a * (x + y) = (a * x) + (a * y)
let x, y be VECTOR of UNITSTR(# D,d1,A,M,S #); :: thesis: a * (x + y) = (a * x) + (a * y)
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;
reconsider a = a as Element of REAL by XREAL_0:def 1;
a * (x + y) = the Mult of V . [a,(x + y)] by A1, A4, FUNCT_1:49
.= a * (x1 + y1) by A8
.= (a * x1) + (a * y1) by RLVECT_1:def 5
.= the addF of V . [( the Mult of V . [a,x1]),(a * y)] by A6
.= the addF of V . [(a * x),(a * y)] by A6
.= (a * x) + (a * y) by A1, A3, FUNCT_1:49 ;
hence a * (x + y) = (a * x) + (a * y) ; :: thesis: verum
end;
A13: for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds x + (0. UNITSTR(# D,d1,A,M,S #)) = x
proof
let x be VECTOR of UNITSTR(# D,d1,A,M,S #); :: thesis: x + (0. UNITSTR(# D,d1,A,M,S #)) = x
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
thus x + (0. UNITSTR(# D,d1,A,M,S #)) = y + (0. V) by A2, A8
.= x by RLVECT_1:4 ; :: thesis: verum
end;
thus UNITSTR(# D,d1,A,M,S #) is RealUnitarySpace-like :: thesis: ( UNITSTR(# D,d1,A,M,S #) is vector-distributive & UNITSTR(# D,d1,A,M,S #) is scalar-distributive & UNITSTR(# D,d1,A,M,S #) is scalar-associative & UNITSTR(# D,d1,A,M,S #) is scalar-unital & UNITSTR(# D,d1,A,M,S #) is Abelian & UNITSTR(# D,d1,A,M,S #) is add-associative & UNITSTR(# D,d1,A,M,S #) is right_zeroed & UNITSTR(# D,d1,A,M,S #) is right_complementable )
proof
let x, y, z be VECTOR of UNITSTR(# D,d1,A,M,S #); :: according to BHSP_1:def 2 :: thesis: for b1 being object holds
( ( not x .|. x = 0 or x = 0. UNITSTR(# D,d1,A,M,S #) ) & ( not x = 0. UNITSTR(# D,d1,A,M,S #) or x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (b1 * x) .|. y = b1 * (x .|. y) )
reconsider z1 = z as VECTOR of V by A1, TARSKI:def 3;
reconsider y1 = y as VECTOR of V by A1, TARSKI:def 3;
reconsider x1 = x as VECTOR of V by A1, TARSKI:def 3;
let a be Real; :: thesis: ( ( not x .|. x = 0 or x = 0. UNITSTR(# D,d1,A,M,S #) ) & ( not x = 0. UNITSTR(# D,d1,A,M,S #) or x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
A14: ( x = 0. UNITSTR(# D,d1,A,M,S #) implies x .|. x = 0 )
proof
assume x = 0. UNITSTR(# D,d1,A,M,S #) ; :: thesis: x .|. x = 0
then x1 .|. x1 = 0 by A2, BHSP_1:def 2;
then the scalar of V . [x1,x1] = 0 ;
hence x .|. x = 0 by A7; :: thesis: verum
end;
( x .|. x = 0 implies x = 0. UNITSTR(# D,d1,A,M,S #) )
proof
assume x .|. x = 0 ; :: thesis: x = 0. UNITSTR(# D,d1,A,M,S #)
then the scalar of V . [x1,x1] = 0 by A7;
then x1 .|. x1 = 0 ;
hence x = 0. UNITSTR(# D,d1,A,M,S #) by A2, BHSP_1:def 2; :: thesis: verum
end;
hence ( x .|. x = 0 iff x = 0. UNITSTR(# D,d1,A,M,S #) ) by A14; :: thesis: ( 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
0 <= x1 .|. x1 by BHSP_1:def 2;
then 0 <= the scalar of V . [x1,x1] ;
hence 0 <= x .|. x by A7; :: thesis: ( x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
the scalar of V . [x1,y1] = y1 .|. x1 by BHSP_1:def 1;
then the scalar of V . [x1,y1] = the scalar of V . [y1,x1] ;
then x .|. y = the scalar of V . [y1,x1] by A7;
hence x .|. y = y .|. x by A7; :: thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
A15: (x + y) .|. z = the scalar of V . [(x + y),z] by A7
.= the scalar of V . [(x1 + y1),z] by A8
.= (x1 + y1) .|. z1
.= (x1 .|. z1) + (y1 .|. z1) by BHSP_1:def 2 ;
(x .|. z) + (y .|. z) = ( the scalar of V . [x,z]) + (y .|. z) by A7
.= ( the scalar of V . [x,z]) + ( the scalar of V . [y,z]) by A7
.= (x1 .|. z1) + (y1 .|. z1) ;
hence (x + y) .|. z = (x .|. z) + (y .|. z) by A15; :: thesis: (a * x) .|. y = a * (x .|. y)
A16: a * (x .|. y) = a * ( the scalar of V . [x,y]) by A7
.= a * (x1 .|. y1) ;
(a * x) .|. y = the scalar of V . [(a * x),y] by A7
.= the scalar of V . [(a * x1),y] by A6
.= (a * x1) .|. y1
.= a * (x1 .|. y1) by BHSP_1:def 2 ;
hence (a * x) .|. y = a * (x .|. y) by A16; :: thesis: verum
end;
A17: for a, b being Real
for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds (a + b) * x = (a * x) + (b * x)
proof
let a, b be Real; :: thesis: for x being VECTOR of UNITSTR(# D,d1,A,M,S #) holds (a + b) * x = (a * x) + (b * x)
let x be VECTOR of UNITSTR(# D,d1,A,M,S #); :: thesis: (a + b) * x = (a * x) + (b * x)
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
reconsider a = a, b = b as Real ;
(a + b) * x = (a + b) * y by A6
.= (a * y) + (b * y) by RLVECT_1:def 6
.= the addF of V . [( the Mult of V . [a,y]),(b * x)] by A6
.= the addF of V . [(a * x),(b * x)] by A6
.= (a * x) + (b * x) by A1, A3, FUNCT_1:49 ;
hence (a + b) * x = (a * x) + (b * x) ; :: thesis: verum
end;
A18: UNITSTR(# D,d1,A,M,S #) is right_complementable
proof
let x be VECTOR of UNITSTR(# D,d1,A,M,S #); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x1 = x as VECTOR of V by A1, TARSKI:def 3;
consider v being VECTOR of V such that
A19: x1 + v = 0. V by ALGSTR_0:def 11;
v = - x1 by A19, RLVECT_1:def 10
.= (- 1) * x1 by RLVECT_1:16
.= (- jj) * x by A6 ;
then reconsider y = v as VECTOR of UNITSTR(# D,d1,A,M,S #) ;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. UNITSTR(# D,d1,A,M,S #)
thus x + y = 0. UNITSTR(# D,d1,A,M,S #) by A2, A8, A19; :: thesis: verum
end;
A20: for x, y being Element of UNITSTR(# D,d1,A,M,S #) holds x + y = y + x
proof
let x, y be Element of UNITSTR(# D,d1,A,M,S #); :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;
thus x + y = x1 + y1 by A8
.= y1 + x1
.= y + x by A8 ; :: thesis: verum
end;
for x, y, z being VECTOR of UNITSTR(# D,d1,A,M,S #) holds (x + y) + z = x + (y + z)
proof
let x, y, z be VECTOR of UNITSTR(# D,d1,A,M,S #); :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def 3;
thus (x + y) + z = the addF of V . [(x + y),z1] by A8
.= (x1 + y1) + z1 by A8
.= x1 + (y1 + z1) by RLVECT_1:def 3
.= the addF of V . [x1,(y + z)] by A8
.= x + (y + z) by A8 ; :: thesis: verum
end;
hence ( UNITSTR(# D,d1,A,M,S #) is vector-distributive & UNITSTR(# D,d1,A,M,S #) is scalar-distributive & UNITSTR(# D,d1,A,M,S #) is scalar-associative & UNITSTR(# D,d1,A,M,S #) is scalar-unital & UNITSTR(# D,d1,A,M,S #) is Abelian & UNITSTR(# D,d1,A,M,S #) is add-associative & UNITSTR(# D,d1,A,M,S #) is right_zeroed & UNITSTR(# D,d1,A,M,S #) is right_complementable ) by A20, A13, A18, A12, A17, A11, A10; :: thesis: verum
end;
0. UNITSTR(# D,d1,A,M,S #) = 0. V by A2;
hence UNITSTR(# D,d1,A,M,S #) is Subspace of V by A1, A3, A4, A5, A9, Def1; :: thesis: verum
end;
hence UNITSTR(# D,d1,A,M,S #) is Subspace of V ; :: thesis: verum