:: MOD_1 semantic presentation

definition

mode AddGroup is non empty add-associative right_zeroed right_complementable LoopStr ;

end;

theorem :: MOD_1:1

canceled;

theorem :: MOD_1:2

canceled;

theorem :: MOD_1:3

canceled;

theorem :: MOD_1:4

canceled;

theorem :: MOD_1:5

canceled;

theorem :: MOD_1:6

canceled;

theorem :: MOD_1:7

canceled;

theorem :: MOD_1:8

canceled;

theorem :: MOD_1:9

canceled;

theorem :: MOD_1:10

canceled;

theorem :: MOD_1:11

canceled;

theorem :: MOD_1:12

canceled;

theorem :: MOD_1:13

for K being non empty add-associative right_zeroed right_complementable right-distributive right_unital doubleLoopStr
for a being Element of K holds a * (- (1. K)) = - a

proof end;

theorem :: MOD_1:14

for K being non empty add-associative right_zeroed right_complementable left-distributive left_unital doubleLoopStr
for a being Element of K holds (- (1. K)) * a = - a

proof end;

theorem :: MOD_1:15

canceled;

theorem :: MOD_1:16

canceled;

theorem :: MOD_1:17

canceled;

theorem :: MOD_1:18

canceled;

theorem :: MOD_1:19

canceled;

theorem :: MOD_1:20

canceled;

theorem :: MOD_1:21

canceled;

theorem :: MOD_1:22

canceled;

theorem :: MOD_1:23

canceled;

theorem :: MOD_1:24

canceled;

theorem :: MOD_1:25

for F being Field-like non degenerated Ring
for x being Scalar of F
for V being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of F
for v being Vector of V holds
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

proof end;

theorem :: MOD_1:26

proof end;

theorem :: MOD_1:27

canceled;

theorem :: MOD_1:28

canceled;

theorem :: MOD_1:29

canceled;

theorem :: MOD_1:30

canceled;

theorem :: MOD_1:31

canceled;

theorem :: MOD_1:32

canceled;

theorem :: MOD_1:33

canceled;

theorem :: MOD_1:34

canceled;

theorem :: MOD_1:35

canceled;

theorem :: MOD_1:36

canceled;

theorem Th37: :: MOD_1:37

for R being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr
for V being non empty add-associative right_zeroed right_complementable RightMod-like RightModStr of R
for x being Scalar of R
for v being Vector of V holds
( v * (0. R) = 0. V & v * (- (1. R)) = - v & (0. V) * x = 0. V )

proof end;

theorem Th38: :: MOD_1:38

for R being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr
for V being non empty add-associative right_zeroed right_complementable RightMod-like RightModStr of R
for x being Scalar of R
for v, w being Vector of V holds
( - (v * x) = v * (- x) & w - (v * x) = w + (v * (- x)) )

proof end;

theorem Th39: :: MOD_1:39

proof end;

theorem :: MOD_1:40

for R being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr
for V being non empty add-associative right_zeroed right_complementable RightMod-like RightModStr of R
for x being Scalar of R
for v, w being Vector of V holds (v - w) * x = (v * x) - (w * x)

proof end;

theorem :: MOD_1:41

canceled;

theorem :: MOD_1:42

for F being Field-like non degenerated Ring
for x being Scalar of F
for V being non empty add-associative right_zeroed right_complementable RightMod-like RightModStr of F
for v being Vector of V holds
( v * x = 0. V iff ( x = 0. F or v = 0. V ) )

proof end;

theorem :: MOD_1:43

proof end;