:: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski

::

:: Received November 23, 1989

:: Copyright (c) 1990-2017 Association of Mizar Users

definition

addLoopStr(# REAL,addreal,(In (0,REAL)) #) is strict addLoopStr ;

end;

func G_Real -> strict addLoopStr equals :: VECTSP_1:def 1

addLoopStr(# REAL,addreal,(In (0,REAL)) #);

coherence addLoopStr(# REAL,addreal,(In (0,REAL)) #);

addLoopStr(# REAL,addreal,(In (0,REAL)) #) is strict addLoopStr ;

registration
end;

registration

let a, b be Element of G_Real;

let x, y be Real;

compatibility

( a = x & b = y implies a + b = x + y ) by BINOP_2:def 9;

end;
let x, y be Real;

compatibility

( a = x & b = y implies a + b = x + y ) by BINOP_2:def 9;

registration

coherence

( G_Real is Abelian & G_Real is add-associative & G_Real is right_zeroed & G_Real is right_complementable )

end;
( G_Real is Abelian & G_Real is add-associative & G_Real is right_zeroed & G_Real is right_complementable )

proof end;

registration
end;

registration

let a, b be Element of G_Real;

let x, y be Real;

compatibility

( a = x & b = y implies a - b = x - y ) ;

end;
let x, y be Real;

compatibility

( a = x & b = y implies a - b = x - y ) ;

registration

existence

ex b_{1} being non empty addLoopStr st

( b_{1} is strict & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is Abelian )

end;
ex b

( b

proof end;

definition
end;

:: 4. FIELD STRUCTURE

definition

let IT be non empty doubleLoopStr ;

end;
attr IT is right-distributive means :Def2: :: VECTSP_1:def 2

for a, b, c being Element of IT holds a * (b + c) = (a * b) + (a * c);

for a, b, c being Element of IT holds a * (b + c) = (a * b) + (a * c);

attr IT is left-distributive means :Def3: :: VECTSP_1:def 3

for a, b, c being Element of IT holds (b + c) * a = (b * a) + (c * a);

for a, b, c being Element of IT holds (b + c) * a = (b * a) + (c * a);

:: deftheorem Def2 defines right-distributive VECTSP_1:def 2 :

for IT being non empty doubleLoopStr holds

( IT is right-distributive iff for a, b, c being Element of IT holds a * (b + c) = (a * b) + (a * c) );

for IT being non empty doubleLoopStr holds

( IT is right-distributive iff for a, b, c being Element of IT holds a * (b + c) = (a * b) + (a * c) );

:: deftheorem Def3 defines left-distributive VECTSP_1:def 3 :

for IT being non empty doubleLoopStr holds

( IT is left-distributive iff for a, b, c being Element of IT holds (b + c) * a = (b * a) + (c * a) );

for IT being non empty doubleLoopStr holds

( IT is left-distributive iff for a, b, c being Element of IT holds (b + c) * a = (b * a) + (c * a) );

definition

let IT be non empty multLoopStr ;

end;
attr IT is right_unital means :Def4: :: VECTSP_1:def 4

for x being Element of IT holds x * (1. IT) = x;

for x being Element of IT holds x * (1. IT) = x;

:: deftheorem Def4 defines right_unital VECTSP_1:def 4 :

for IT being non empty multLoopStr holds

( IT is right_unital iff for x being Element of IT holds x * (1. IT) = x );

for IT being non empty multLoopStr holds

( IT is right_unital iff for x being Element of IT holds x * (1. IT) = x );

definition

coherence

doubleLoopStr(# REAL,addreal,multreal,(In (1,REAL)),(In (0,REAL)) #) is strict doubleLoopStr ;

;

end;

func F_Real -> strict doubleLoopStr equals :: VECTSP_1:def 5

doubleLoopStr(# REAL,addreal,multreal,(In (1,REAL)),(In (0,REAL)) #);

correctness doubleLoopStr(# REAL,addreal,multreal,(In (1,REAL)),(In (0,REAL)) #);

coherence

doubleLoopStr(# REAL,addreal,multreal,(In (1,REAL)),(In (0,REAL)) #) is strict doubleLoopStr ;

;

:: deftheorem defines F_Real VECTSP_1:def 5 :

F_Real = doubleLoopStr(# REAL,addreal,multreal,(In (1,REAL)),(In (0,REAL)) #);

F_Real = doubleLoopStr(# REAL,addreal,multreal,(In (1,REAL)),(In (0,REAL)) #);

registration
end;

registration

let a, b be Element of F_Real;

let x, y be Real;

compatibility

( a = x & b = y implies a + b = x + y ) by BINOP_2:def 9;

end;
let x, y be Real;

compatibility

( a = x & b = y implies a + b = x + y ) by BINOP_2:def 9;

registration

let a, b be Element of F_Real;

let x, y be Real;

compatibility

( a = x & b = y implies a * b = x * y ) by BINOP_2:def 11;

end;
let x, y be Real;

compatibility

( a = x & b = y implies a * b = x * y ) by BINOP_2:def 11;

definition

let IT be non empty multLoopStr ;

end;
attr IT is well-unital means :Def6: :: VECTSP_1:def 6

for x being Element of IT holds

( x * (1. IT) = x & (1. IT) * x = x );

for x being Element of IT holds

( x * (1. IT) = x & (1. IT) * x = x );

:: deftheorem Def6 defines well-unital VECTSP_1:def 6 :

for IT being non empty multLoopStr holds

( IT is well-unital iff for x being Element of IT holds

( x * (1. IT) = x & (1. IT) * x = x ) );

for IT being non empty multLoopStr holds

( IT is well-unital iff for x being Element of IT holds

( x * (1. IT) = x & (1. IT) * x = x ) );

Lm1: for L being non empty multLoopStr st L is well-unital holds

1. L = 1_ L

proof end;

registration
end;

registration

let L be non empty well-unital multLoopStr_0 ;

let x be Element of L;

reducibility

x * (1. L) = x by Def6;

reducibility

(1. L) * x = x by Def6;

end;
let x be Element of L;

reducibility

x * (1. L) = x by Def6;

reducibility

(1. L) * x = x by Def6;

:: deftheorem Def7 defines distributive VECTSP_1:def 7 :

for IT being non empty doubleLoopStr holds

( IT is distributive iff for x, y, z being Element of IT holds

( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) );

for IT being non empty doubleLoopStr holds

( IT is distributive iff for x, y, z being Element of IT holds

( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) );

definition

let IT be non empty multLoopStr ;

end;
attr IT is left_unital means :Def8: :: VECTSP_1:def 8

for x being Element of IT holds (1. IT) * x = x;

for x being Element of IT holds (1. IT) * x = x;

:: deftheorem Def8 defines left_unital VECTSP_1:def 8 :

for IT being non empty multLoopStr holds

( IT is left_unital iff for x being Element of IT holds (1. IT) * x = x );

for IT being non empty multLoopStr holds

( IT is left_unital iff for x being Element of IT holds (1. IT) * x = x );

definition

let IT be non empty multLoopStr_0 ;

( IT is almost_left_invertible iff for x being Element of IT st x <> 0. IT holds

ex y being Element of IT st y * x = 1. IT )

end;
redefine attr IT is almost_left_invertible means :Def9: :: VECTSP_1:def 9

for x being Element of IT st x <> 0. IT holds

ex y being Element of IT st y * x = 1. IT;

compatibility for x being Element of IT st x <> 0. IT holds

ex y being Element of IT st y * x = 1. IT;

( IT is almost_left_invertible iff for x being Element of IT st x <> 0. IT holds

ex y being Element of IT st y * x = 1. IT )

proof end;

:: deftheorem Def9 defines almost_left_invertible VECTSP_1:def 9 :

for IT being non empty multLoopStr_0 holds

( IT is almost_left_invertible iff for x being Element of IT st x <> 0. IT holds

ex y being Element of IT st y * x = 1. IT );

for IT being non empty multLoopStr_0 holds

( IT is almost_left_invertible iff for x being Element of IT st x <> 0. IT holds

ex y being Element of IT st y * x = 1. IT );

set FR = F_Real ;

reconsider jj = 1 as Real ;

registration

( F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )
end;

cluster F_Real -> non degenerated right_complementable almost_left_invertible strict Abelian add-associative right_zeroed associative commutative right_unital distributive left_unital ;

coherence ( F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is Abelian & F_Real is commutative & F_Real is associative & F_Real is left_unital & F_Real is right_unital & F_Real is distributive & F_Real is almost_left_invertible & not F_Real is degenerated )

proof end;

registration
end;

registration

let a, b be Element of F_Real;

let x, y be Real;

compatibility

( a = x & b = y implies a - b = x - y ) ;

end;
let x, y be Real;

compatibility

( a = x & b = y implies a - b = x - y ) ;

registration

for b_{1} being non empty doubleLoopStr st b_{1} is distributive holds

( b_{1} is left-distributive & b_{1} is right-distributive )
;

for b_{1} being non empty doubleLoopStr st b_{1} is left-distributive & b_{1} is right-distributive holds

b_{1} is distributive
;

end;

cluster non empty distributive -> non empty right-distributive left-distributive for doubleLoopStr ;

coherence for b

( b

cluster non empty right-distributive left-distributive -> non empty distributive for doubleLoopStr ;

coherence for b

b

registration

coherence

for b_{1} being non empty multLoopStr st b_{1} is well-unital holds

( b_{1} is left_unital & b_{1} is right_unital )
;

coherence

for b_{1} being non empty multLoopStr st b_{1} is left_unital & b_{1} is right_unital holds

b_{1} is unital
;

end;
for b

( b

coherence

for b

b

registration

existence

ex b_{1} being non empty multMagma st

( b_{1} is commutative & b_{1} is associative )

end;
ex b

( b

proof end;

registration

existence

ex b_{1} being non empty multLoopStr st

( b_{1} is commutative & b_{1} is associative & b_{1} is unital )

end;
ex b

( b

proof end;

registration

ex b_{1} being non empty doubleLoopStr st

( b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is Abelian & b_{1} is commutative & b_{1} is associative & b_{1} is left_unital & b_{1} is right_unital & b_{1} is distributive & b_{1} is almost_left_invertible & not b_{1} is degenerated & b_{1} is well-unital & b_{1} is strict )
end;

cluster non empty non degenerated right_complementable almost_left_invertible strict Abelian add-associative right_zeroed associative commutative right_unital well-unital distributive left_unital for doubleLoopStr ;

existence ex b

( b

proof end;

definition

mode Ring is non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;

end;
:: 6. AXIOMS OF FIELD

registration
end;

::$CT 4

theorem :: VECTSP_1:5

for F being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr

for x, y, z being Element of F st x <> 0. F & x * y = x * z holds

y = z

for x, y, z being Element of F st x <> 0. F & x * y = x * z holds

y = z

proof end;

notation

let F be non empty almost_left_invertible associative commutative well-unital doubleLoopStr ;

let x be Element of F;

synonym x " for / x;

end;
let x be Element of F;

synonym x " for / x;

definition

let F be non empty almost_left_invertible associative commutative well-unital doubleLoopStr ;

let x be Element of F;

assume A1: x <> 0. F ;

compatibility

for b_{1} being Element of the carrier of F holds

( b_{1} = x " iff b_{1} * x = 1. F )

end;
let x be Element of F;

assume A1: x <> 0. F ;

compatibility

for b

( b

proof end;

:: deftheorem Def10 defines " VECTSP_1:def 10 :

for F being non empty almost_left_invertible associative commutative well-unital doubleLoopStr

for x being Element of F st x <> 0. F holds

for b_{3} being Element of the carrier of F holds

( b_{3} = x " iff b_{3} * x = 1. F );

for F being non empty almost_left_invertible associative commutative well-unital doubleLoopStr

for x being Element of F st x <> 0. F holds

for b

( b

registration

let a be non zero Element of F_Real;

let x be Real;

compatibility

( a = x implies a " = x " )

end;
let x be Real;

compatibility

( a = x implies a " = x " )

proof end;

registration

let a, b be non zero Element of F_Real;

let x, y be Real;

compatibility

( a = x & b = y implies a / b = x / y ) ;

end;
let x, y be Real;

compatibility

( a = x & b = y implies a / b = x / y ) ;

canceled;

:: definition

:: let F be associative commutative well-unital distributive

:: almost_left_invertible non empty doubleLoopStr, x,y be Element of F;

:: func x/y ->Element of F equals

:: x*y";

:: coherence;

:: end;

::$CD

:: let F be associative commutative well-unital distributive

:: almost_left_invertible non empty doubleLoopStr, x,y be Element of F;

:: func x/y ->Element of F equals

:: x*y";

:: coherence;

:: end;

::$CD

theorem Th2: :: VECTSP_1:6

for F being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr

for x being Element of F holds x * (0. F) = 0. F

for x being Element of F holds x * (0. F) = 0. F

proof end;

registration

let F be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;

let x be Element of F;

let y be zero Element of F;

reducibility

x * y = y

end;
let x be Element of F;

let y be zero Element of F;

reducibility

x * y = y

proof end;

theorem Th3: :: VECTSP_1:7

for F being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr

for x being Element of F holds (0. F) * x = 0. F

for x being Element of F holds (0. F) * x = 0. F

proof end;

registration

let F be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ;

let x be zero Element of F;

let y be Element of F;

reducibility

x * y = x

end;
let x be zero Element of F;

let y be Element of F;

reducibility

x * y = x

proof end;

theorem Th4: :: VECTSP_1:8

for F being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr

for x, y being Element of F holds x * (- y) = - (x * y)

for x, y being Element of F holds x * (- y) = - (x * y)

proof end;

theorem Th5: :: VECTSP_1:9

for F being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr

for x, y being Element of F holds (- x) * y = - (x * y)

for x, y being Element of F holds (- x) * y = - (x * y)

proof end;

theorem Th6: :: VECTSP_1:10

for F being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr

for x, y being Element of F holds (- x) * (- y) = x * y

for x, y being Element of F holds (- x) * (- y) = x * y

proof end;

theorem :: VECTSP_1:11

for F being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr

for x, y, z being Element of F holds x * (y - z) = (x * y) - (x * z)

for x, y, z being Element of F holds x * (y - z) = (x * y) - (x * z)

proof end;

theorem Th8: :: VECTSP_1:12

for F being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr

for x, y being Element of F holds

( x * y = 0. F iff ( x = 0. F or y = 0. F ) )

for x, y being Element of F holds

( x * y = 0. F iff ( x = 0. F or y = 0. F ) )

proof end;

theorem :: VECTSP_1:13

for K being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr

for a, b, c being Element of K holds (a - b) * c = (a * c) - (b * c)

for a, b, c being Element of K holds (a - b) * c = (a * c) - (b * c)

proof end;

:: 8. VECTOR SPACE STRUCTURE

definition

let F be 1-sorted ;

attr c_{2} is strict ;

struct ModuleStr over F -> addLoopStr ;

aggr ModuleStr(# carrier, addF, ZeroF, lmult #) -> ModuleStr over F;

sel lmult c_{2} -> Function of [: the carrier of F, the carrier of c_{2}:], the carrier of c_{2};

end;
attr c

struct ModuleStr over F -> addLoopStr ;

aggr ModuleStr(# carrier, addF, ZeroF, lmult #) -> ModuleStr over F;

sel lmult c

registration

let F be 1-sorted ;

existence

ex b_{1} being ModuleStr over F st

( not b_{1} is empty & b_{1} is strict )

end;
existence

ex b

( not b

proof end;

registration

let F be 1-sorted ;

let A be non empty set ;

let a be BinOp of A;

let Z be Element of A;

let l be Function of [: the carrier of F,A:],A;

coherence

not ModuleStr(# A,a,Z,l #) is empty ;

end;
let A be non empty set ;

let a be BinOp of A;

let Z be Element of A;

let l be Function of [: the carrier of F,A:],A;

coherence

not ModuleStr(# A,a,Z,l #) is empty ;

definition

let F be 1-sorted ;

let VS be ModuleStr over F;

mode Scalar of VS is Scalar of F;

mode Vector of VS is Element of VS;

end;
let VS be ModuleStr over F;

mode Scalar of VS is Scalar of F;

mode Vector of VS is Element of VS;

definition

let F be non empty 1-sorted ;

let V be non empty ModuleStr over F;

let x be Element of F;

let v be Element of V;

coherence

the lmult of V . (x,v) is Element of V ;

end;
let V be non empty ModuleStr over F;

let x be Element of F;

let v be Element of V;

coherence

the lmult of V . (x,v) is Element of V ;

:: deftheorem defines * VECTSP_1:def 11 :

for F being non empty 1-sorted

for V being non empty ModuleStr over F

for x being Element of F

for v being Element of V holds x * v = the lmult of V . (x,v);

for F being non empty 1-sorted

for V being non empty ModuleStr over F

for x being Element of F

for v being Element of V holds x * v = the lmult of V . (x,v);

definition

let F be non empty addLoopStr ;

ex b_{1} being UnOp of the carrier of F st

for x being Element of F holds b_{1} . x = - x

for b_{1}, b_{2} being UnOp of the carrier of F st ( for x being Element of F holds b_{1} . x = - x ) & ( for x being Element of F holds b_{2} . x = - x ) holds

b_{1} = b_{2}

end;
func comp F -> UnOp of the carrier of F means :: VECTSP_1:def 12

for x being Element of F holds it . x = - x;

existence for x being Element of F holds it . x = - x;

ex b

for x being Element of F holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines comp VECTSP_1:def 12 :

for F being non empty addLoopStr

for b_{2} being UnOp of the carrier of F holds

( b_{2} = comp F iff for x being Element of F holds b_{2} . x = - x );

for F being non empty addLoopStr

for b

( b

Lm2: now :: thesis: for F being non empty right_complementable Abelian add-associative right_zeroed associative distributive left_unital doubleLoopStr

for MLT being Function of [: the carrier of F, the carrier of F:], the carrier of F holds

( ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is Abelian & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )

for MLT being Function of [: the carrier of F, the carrier of F:], the carrier of F holds

( ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is Abelian & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )

let F be non empty right_complementable Abelian add-associative right_zeroed associative distributive left_unital doubleLoopStr ; :: thesis: for MLT being Function of [: the carrier of F, the carrier of F:], the carrier of F holds

( ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is Abelian & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )

let MLT be Function of [: the carrier of F, the carrier of F:], the carrier of F; :: thesis: ( ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is Abelian & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )

set GF = ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #);

thus ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is Abelian :: thesis: ( ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )

end;
( ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is Abelian & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )

let MLT be Function of [: the carrier of F, the carrier of F:], the carrier of F; :: thesis: ( ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is Abelian & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )

set GF = ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #);

thus ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is Abelian :: thesis: ( ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )

proof

thus
ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is add-associative
:: thesis: ( ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed & ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable )
let x, y be Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x

reconsider x9 = x, y9 = y as Element of F ;

thus x + y = y9 + x9 by RLVECT_1:2

.= y + x ; :: thesis: verum

end;
reconsider x9 = x, y9 = y as Element of F ;

thus x + y = y9 + x9 by RLVECT_1:2

.= y + x ; :: thesis: verum

proof

thus
ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_zeroed
:: thesis: ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable
let x, y, z be Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #); :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)

reconsider x9 = x, y9 = y, z9 = z as Element of F ;

thus (x + y) + z = (x9 + y9) + z9

.= x9 + (y9 + z9) by RLVECT_1:def 3

.= x + (y + z) ; :: thesis: verum

end;
reconsider x9 = x, y9 = y, z9 = z as Element of F ;

thus (x + y) + z = (x9 + y9) + z9

.= x9 + (y9 + z9) by RLVECT_1:def 3

.= x + (y + z) ; :: thesis: verum

proof

thus
ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) is right_complementable
:: thesis: verum
let x be Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #); :: according to RLVECT_1:def 4 :: thesis: x + (0. ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #)) = x

reconsider x9 = x as Element of F ;

thus x + (0. ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #)) = x9 + (0. F)

.= x by RLVECT_1:4 ; :: thesis: verum

end;
reconsider x9 = x as Element of F ;

thus x + (0. ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #)) = x9 + (0. F)

.= x by RLVECT_1:4 ; :: thesis: verum

proof

let x be Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

reconsider x9 = x as Element of F ;

consider t being Element of F such that

A1: x9 + t = 0. F by ALGSTR_0:def 11;

reconsider t9 = t as Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) ;

take t9 ; :: according to ALGSTR_0:def 11 :: thesis: x + t9 = 0. ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #)

thus x + t9 = 0. ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) by A1; :: thesis: verum

end;
reconsider x9 = x as Element of F ;

consider t being Element of F such that

A1: x9 + t = 0. F by ALGSTR_0:def 11;

reconsider t9 = t as Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) ;

take t9 ; :: according to ALGSTR_0:def 11 :: thesis: x + t9 = 0. ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #)

thus x + t9 = 0. ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) by A1; :: thesis: verum

Lm3: now :: thesis: for F being non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr

for MLT being Function of [: the carrier of F, the carrier of F:], the carrier of F st MLT = the multF of F holds

for x, y being Element of F

for v, w being Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

for MLT being Function of [: the carrier of F, the carrier of F:], the carrier of F st MLT = the multF of F holds

for x, y being Element of F

for v, w being Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

let F be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ; :: thesis: for MLT being Function of [: the carrier of F, the carrier of F:], the carrier of F st MLT = the multF of F holds

for x, y being Element of F

for v, w being Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

let MLT be Function of [: the carrier of F, the carrier of F:], the carrier of F; :: thesis: ( MLT = the multF of F implies for x, y being Element of F

for v, w being Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v ) )

assume A1: MLT = the multF of F ; :: thesis: for x, y being Element of F

for v, w being Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

let x, y be Element of F; :: thesis: for v, w being Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

set LS = ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #);

let v, w be Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #); :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

reconsider v9 = v, w9 = w as Element of F ;

thus x * (v + w) = x * (v9 + w9) by A1

.= (x * v9) + (x * w9) by Def7

.= (x * v) + (x * w) by A1 ; :: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

thus (x + y) * v = (x + y) * v9 by A1

.= (x * v9) + (y * v9) by Def7

.= (x * v) + (y * v) by A1 ; :: thesis: ( (x * y) * v = x * (y * v) & (1. F) * v = v )

thus (x * y) * v = (x * y) * v9 by A1

.= x * (y * v9) by GROUP_1:def 3

.= x * (y * v) by A1 ; :: thesis: (1. F) * v = v

thus (1. F) * v = (1. F) * v9 by A1

.= v ; :: thesis: verum

end;
for x, y being Element of F

for v, w being Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

let MLT be Function of [: the carrier of F, the carrier of F:], the carrier of F; :: thesis: ( MLT = the multF of F implies for x, y being Element of F

for v, w being Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v ) )

assume A1: MLT = the multF of F ; :: thesis: for x, y being Element of F

for v, w being Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

let x, y be Element of F; :: thesis: for v, w being Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

set LS = ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #);

let v, w be Element of ModuleStr(# the carrier of F, the addF of F,(0. F),MLT #); :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

reconsider v9 = v, w9 = w as Element of F ;

thus x * (v + w) = x * (v9 + w9) by A1

.= (x * v9) + (x * w9) by Def7

.= (x * v) + (x * w) by A1 ; :: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v )

thus (x + y) * v = (x + y) * v9 by A1

.= (x * v9) + (y * v9) by Def7

.= (x * v) + (y * v) by A1 ; :: thesis: ( (x * y) * v = x * (y * v) & (1. F) * v = v )

thus (x * y) * v = (x * y) * v9 by A1

.= x * (y * v9) by GROUP_1:def 3

.= x * (y * v) by A1 ; :: thesis: (1. F) * v = v

thus (1. F) * v = (1. F) * v9 by A1

.= v ; :: thesis: verum

definition

let F be non empty doubleLoopStr ;

let IT be non empty ModuleStr over F;

end;
let IT be non empty ModuleStr over F;

attr IT is vector-distributive means :Def13: :: VECTSP_1:def 13

for x being Element of F

for v, w being Element of IT holds x * (v + w) = (x * v) + (x * w);

for x being Element of F

for v, w being Element of IT holds x * (v + w) = (x * v) + (x * w);

attr IT is scalar-distributive means :Def14: :: VECTSP_1:def 14

for x, y being Element of F

for v being Element of IT holds (x + y) * v = (x * v) + (y * v);

for x, y being Element of F

for v being Element of IT holds (x + y) * v = (x * v) + (y * v);

attr IT is scalar-associative means :Def15: :: VECTSP_1:def 15

for x, y being Element of F

for v being Element of IT holds (x * y) * v = x * (y * v);

for x, y being Element of F

for v being Element of IT holds (x * y) * v = x * (y * v);

attr IT is scalar-unital means :Def16: :: VECTSP_1:def 16

for v being Element of IT holds (1. F) * v = v;

for v being Element of IT holds (1. F) * v = v;

:: deftheorem Def13 defines vector-distributive VECTSP_1:def 13 :

for F being non empty doubleLoopStr

for IT being non empty ModuleStr over F holds

( IT is vector-distributive iff for x being Element of F

for v, w being Element of IT holds x * (v + w) = (x * v) + (x * w) );

for F being non empty doubleLoopStr

for IT being non empty ModuleStr over F holds

( IT is vector-distributive iff for x being Element of F

for v, w being Element of IT holds x * (v + w) = (x * v) + (x * w) );

:: deftheorem Def14 defines scalar-distributive VECTSP_1:def 14 :

for F being non empty doubleLoopStr

for IT being non empty ModuleStr over F holds

( IT is scalar-distributive iff for x, y being Element of F

for v being Element of IT holds (x + y) * v = (x * v) + (y * v) );

for F being non empty doubleLoopStr

for IT being non empty ModuleStr over F holds

( IT is scalar-distributive iff for x, y being Element of F

for v being Element of IT holds (x + y) * v = (x * v) + (y * v) );

:: deftheorem Def15 defines scalar-associative VECTSP_1:def 15 :

for F being non empty doubleLoopStr

for IT being non empty ModuleStr over F holds

( IT is scalar-associative iff for x, y being Element of F

for v being Element of IT holds (x * y) * v = x * (y * v) );

for F being non empty doubleLoopStr

for IT being non empty ModuleStr over F holds

( IT is scalar-associative iff for x, y being Element of F

for v being Element of IT holds (x * y) * v = x * (y * v) );

:: deftheorem Def16 defines scalar-unital VECTSP_1:def 16 :

for F being non empty doubleLoopStr

for IT being non empty ModuleStr over F holds

( IT is scalar-unital iff for v being Element of IT holds (1. F) * v = v );

for F being non empty doubleLoopStr

for IT being non empty ModuleStr over F holds

( IT is scalar-unital iff for v being Element of IT holds (1. F) * v = v );

registration

let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;

ex b_{1} being non empty ModuleStr over F st

( b_{1} is scalar-distributive & b_{1} is vector-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is Abelian & b_{1} is strict )

end;
cluster non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for ModuleStr over F;

existence ex b

( b

proof end;

definition

let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;

mode VectSp of F is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F;

end;
mode VectSp of F is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F;

theorem Th10: :: VECTSP_1:14

for F being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr

for x being Element of F

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F

for v being Element of V holds

( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. V )

for x being Element of F

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F

for v being Element of V holds

( (0. F) * v = 0. V & (- (1. F)) * v = - v & x * (0. V) = 0. V )

proof end;

theorem :: VECTSP_1:15

for F being Field

for x being Element of F

for V being VectSp of F

for v being Element of V holds

( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

for x being Element of F

for V being VectSp of F

for v being Element of V holds

( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

proof end;

:: 13. APPENDIX

theorem :: VECTSP_1:16

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V holds

( v + w = 0. V iff - v = w )

for v, w being Element of V holds

( v + w = 0. V iff - v = w )

proof end;

Lm4: for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V holds - (w + (- v)) = v - w

proof end;

Lm5: for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of V holds - ((- v) - w) = w + v

proof end;

theorem :: VECTSP_1:17

theorem :: VECTSP_1:18

for V being non empty right_complementable add-associative right_zeroed addLoopStr

for v being Element of V holds

( (0. V) - v = - v & v - (0. V) = v ) by RLVECT_1:13, RLVECT_1:14;

for v being Element of V holds

( (0. V) - v = - v & v - (0. V) = v ) by RLVECT_1:13, RLVECT_1:14;

theorem Th15: :: VECTSP_1:19

for F being non empty right_complementable add-associative right_zeroed addLoopStr

for x, y being Element of F holds

( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) )

for x, y being Element of F holds

( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) )

proof end;

theorem :: VECTSP_1:20

for F being Field

for x being Element of F

for V being VectSp of F

for v being Element of V st x <> 0. F holds

(x ") * (x * v) = v

for x being Element of F

for V being VectSp of F

for v being Element of V st x <> 0. F holds

(x ") * (x * v) = v

proof end;

theorem Th17: :: VECTSP_1:21

for F being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F

for x being Element of F

for v, w being Element of V holds

( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F

for x being Element of F

for v, w being Element of V holds

( - (x * v) = (- x) * v & w - (x * v) = w + ((- x) * v) )

proof end;

registration

coherence

for b_{1} being non empty multLoopStr st b_{1} is commutative & b_{1} is left_unital holds

b_{1} is right_unital

end;
for b

b

proof end;

theorem Th18: :: VECTSP_1:22

for F being non empty right_complementable Abelian add-associative right_zeroed associative right_unital well-unital distributive doubleLoopStr

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F

for x being Element of F

for v being Element of V holds x * (- v) = - (x * v)

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F

for x being Element of F

for v being Element of V holds x * (- v) = - (x * v)

proof end;

theorem :: VECTSP_1:23

for F being non empty right_complementable Abelian add-associative right_zeroed associative right_unital well-unital distributive doubleLoopStr

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F

for x being Element of F

for v, w being Element of V holds x * (v - w) = (x * v) - (x * w)

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F

for x being Element of F

for v, w being Element of V holds x * (v - w) = (x * v) - (x * w)

proof end;

theorem Th20: :: VECTSP_1:24

for F being non empty non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr

for x being Element of F st x <> 0. F holds

(x ") " = x

for x being Element of F st x <> 0. F holds

(x ") " = x

proof end;

registration

let F be non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;

let x be non zero Element of F;

reducibility

(x ") " = x

end;
let x be non zero Element of F;

reducibility

(x ") " = x

proof end;

:: deftheorem defines Fanoian VECTSP_1:def 17 :

for IT being non empty addLoopStr holds

( IT is Fanoian iff for a being Element of IT st a + a = 0. IT holds

a = 0. IT );

for IT being non empty addLoopStr holds

( IT is Fanoian iff for a being Element of IT st a + a = 0. IT holds

a = 0. IT );

definition

let F be non empty non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;

compatibility

( F is Fanoian iff (1. F) + (1. F) <> 0. F )

end;
compatibility

( F is Fanoian iff (1. F) + (1. F) <> 0. F )

proof end;

:: deftheorem defines Fanoian VECTSP_1:def 18 :

for F being non empty non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr holds

( F is Fanoian iff (1. F) + (1. F) <> 0. F );

for F being non empty non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr holds

( F is Fanoian iff (1. F) + (1. F) <> 0. F );

registration

ex b_{1} being Field st

( b_{1} is strict & b_{1} is Fanoian )
end;

cluster non empty non degenerated non trivial right_complementable almost_left_invertible strict Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Fanoian for doubleLoopStr ;

existence ex b

( b

proof end;

theorem :: VECTSP_1:27

for F being non empty right_complementable add-associative right_zeroed addLoopStr

for a, b being Element of F st a - b = 0. F holds

a = b by Th15;

for a, b being Element of F st a - b = 0. F holds

a = b by Th15;

theorem Th24: :: VECTSP_1:28

for F being non empty right_complementable add-associative right_zeroed addLoopStr

for a being Element of F st - a = 0. F holds

a = 0. F

for a being Element of F st - a = 0. F holds

a = 0. F

proof end;

theorem :: VECTSP_1:29

for F being non empty right_complementable add-associative right_zeroed addLoopStr

for a, b being Element of F st a - b = 0. F holds

b - a = 0. F

for a, b being Element of F st a - b = 0. F holds

b - a = 0. F

proof end;

theorem :: VECTSP_1:30

for F being Field

for a, b, c being Element of F holds

( ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) & ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") ) )

for a, b, c being Element of F holds

( ( a <> 0. F & (a * c) - b = 0. F implies c = b * (a ") ) & ( a <> 0. F & b - (c * a) = 0. F implies c = b * (a ") ) )

proof end;

theorem :: VECTSP_1:31

for F being non empty right_complementable add-associative right_zeroed addLoopStr

for a, b being Element of F holds a + b = - ((- b) + (- a))

for a, b being Element of F holds a + b = - ((- b) + (- a))

proof end;

theorem :: VECTSP_1:32

for F being non empty right_complementable add-associative right_zeroed addLoopStr

for a, b, c being Element of F holds (b + a) - (c + a) = b - c

for a, b, c being Element of F holds (b + a) - (c + a) = b - c

proof end;

theorem :: VECTSP_1:33

for G being non empty right_complementable add-associative right_zeroed addLoopStr

for v, w being Element of G holds - ((- v) + w) = (- w) + v

for v, w being Element of G holds - ((- v) + w) = (- w) + v

proof end;

theorem :: VECTSP_1:34

for G being non empty Abelian add-associative addLoopStr

for u, v, w being Element of G holds (u - v) - w = (u - w) - v

for u, v, w being Element of G holds (u - v) - w = (u - w) - v

proof end;

:: from COMPTRIG, 2006.08.12, A.T.

theorem :: VECTSP_1:36

for L being non empty right_complementable add-associative right_zeroed unital right-distributive doubleLoopStr

for n being Element of NAT st n > 0 holds

(power L) . ((0. L),n) = 0. L

for n being Element of NAT st n > 0 holds

(power L) . ((0. L),n) = 0. L

proof end;

:: 2007.02.14, A.T.

theorem :: VECTSP_1:37

:: deftheorem defines additive VECTSP_1:def 19 :

for G, H being non empty addMagma

for f being Function of G,H holds

( f is additive iff for x, y being Element of G holds f . (x + y) = (f . x) + (f . y) );

for G, H being non empty addMagma

for f being Function of G,H holds

( f is additive iff for x, y being Element of G holds f . (x + y) = (f . x) + (f . y) );

registration

let L be non empty right_unital multLoopStr ;

let x be Element of L;

reducibility

x * (1. L) = x by Def4;

end;
let x be Element of L;

reducibility

x * (1. L) = x by Def4;

registration

let L be non empty left_unital multLoopStr ;

let x be Element of L;

reducibility

(1. L) * x = x by Def8;

end;
let x be Element of L;

reducibility

(1. L) * x = x by Def8;