:: MOD_1 semantic presentation

definition

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

end;

theorem Th1: :: MOD_1:1

canceled;

theorem Th2: :: MOD_1:2

canceled;

theorem Th3: :: MOD_1:3

canceled;

theorem Th4: :: MOD_1:4

canceled;

theorem Th5: :: MOD_1:5

canceled;

theorem Th6: :: MOD_1:6

canceled;

theorem Th7: :: MOD_1:7

canceled;

theorem Th8: :: MOD_1:8

canceled;

theorem Th9: :: MOD_1:9

canceled;

theorem Th10: :: MOD_1:10

canceled;

theorem Th11: :: MOD_1:11

canceled;

theorem Th12: :: MOD_1:12

canceled;

theorem Th13: :: MOD_1:13

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

proof end;

theorem Th14: :: MOD_1:14

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

proof end;

theorem Th15: :: MOD_1:15

canceled;

theorem Th16: :: MOD_1:16

canceled;

theorem Th17: :: MOD_1:17

canceled;

theorem Th18: :: MOD_1:18

canceled;

theorem Th19: :: MOD_1:19

canceled;

theorem Th20: :: MOD_1:20

canceled;

theorem Th21: :: MOD_1:21

canceled;

theorem Th22: :: MOD_1:22

canceled;

theorem Th23: :: MOD_1:23

canceled;

theorem Th24: :: MOD_1:24

canceled;

theorem Th25: :: MOD_1:25

for b₁ being Field-like non degenerated Ring
for b₂ being Scalar of b₁
for b₃ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₄ being Vector of b₃ holds
( b₂ * b₄ = 0. b₃ iff ( b₂ = 0. b₁ or b₄ = 0. b₃ ) )

proof end;

theorem Th26: :: MOD_1:26

for b₁ being Field-like non degenerated Ring
for b₂ being Scalar of b₁
for b₃ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₄ being Vector of b₃ st b₂ <> 0. b₁ holds
(b₂ " ) * (b₂ * b₄) = b₄

proof end;

theorem Th27: :: MOD_1:27

canceled;

theorem Th28: :: MOD_1:28

canceled;

theorem Th29: :: MOD_1:29

canceled;

theorem Th30: :: MOD_1:30

canceled;

theorem Th31: :: MOD_1:31

canceled;

theorem Th32: :: MOD_1:32

canceled;

theorem Th33: :: MOD_1:33

canceled;

theorem Th34: :: MOD_1:34

canceled;

theorem Th35: :: MOD_1:35

canceled;

theorem Th36: :: MOD_1:36

canceled;

theorem Th37: :: MOD_1:37

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr
for b₂ being non empty add-associative right_zeroed right_complementable RightMod-like RightModStr of b₁
for b₃ being Scalar of b₁
for b₄ being Vector of b₂ holds
( b₄ * (0. b₁) = 0. b₂ & b₄ * (- (1. b₁)) = - b₄ & (0. b₂) * b₃ = 0. b₂ )

proof end;

theorem Th38: :: MOD_1:38

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr
for b₂ being non empty add-associative right_zeroed right_complementable RightMod-like RightModStr of b₁
for b₃ being Scalar of b₁
for b₄, b₅ being Vector of b₂ holds
( - (b₄ * b₃) = b₄ * (- b₃) & b₅ - (b₄ * b₃) = b₅ + (b₄ * (- b₃)) )

proof end;

theorem Th39: :: MOD_1:39

proof end;

theorem Th40: :: MOD_1:40

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative right_unital distributive left_unital doubleLoopStr
for b₂ being non empty add-associative right_zeroed right_complementable RightMod-like RightModStr of b₁
for b₃ being Scalar of b₁
for b₄, b₅ being Vector of b₂ holds (b₄ - b₅) * b₃ = (b₄ * b₃) - (b₅ * b₃)

proof end;

theorem Th41: :: MOD_1:41

canceled;

theorem Th42: :: MOD_1:42

for b₁ being Field-like non degenerated Ring
for b₂ being Scalar of b₁
for b₃ being non empty add-associative right_zeroed right_complementable RightMod-like RightModStr of b₁
for b₄ being Vector of b₃ holds
( b₄ * b₂ = 0. b₃ iff ( b₂ = 0. b₁ or b₄ = 0. b₃ ) )

proof end;

theorem Th43: :: MOD_1:43

for b₁ being Field-like non degenerated Ring
for b₂ being Scalar of b₁
for b₃ being non empty add-associative right_zeroed right_complementable RightMod-like RightModStr of b₁
for b₄ being Vector of b₃ st b₂ <> 0. b₁ holds
(b₄ * b₂) * (b₂ " ) = b₄

proof end;