:: ALGSTR_2 semantic presentation

Lemma1: for b₁, b₂ being Element of F_Real
for b₃, b₄ being Real st b₁ = b₃ & b₂ = b₄ holds
b₁ * b₂ = b₃ * b₄

proof end;

Lemma2: 0 = 0. F_Real
by RLVECT_1:def 2, VECTSP_1:def 15;

Lemma3: for b₁, b₂ being Element of F_Real st b₁ <> 0. F_Real holds
ex b₃ being Element of F_Real st b₁ * b₃ = b₂

proof end;

Lemma4: for b₁, b₂ being Element of F_Real st b₁ <> 0. F_Real holds
ex b₃ being Element of F_Real st b₃ * b₁ = b₂

proof end;

Lemma5: for b₁, b₂, b₃ being Element of F_Real st b₁ <> 0. F_Real & b₁ * b₂ = b₁ * b₃ holds
b₂ = b₃
by VECTSP_1:33;

Lemma6: for b₁, b₂, b₃ being Element of F_Real st b₁ <> 0. F_Real & b₂ * b₁ = b₃ * b₁ holds
b₂ = b₃
by VECTSP_1:33;

Lemma7: for b₁ being Element of F_Real holds b₁ * (0. F_Real ) = 0. F_Real
by VECTSP_1:44;

Lemma8: for b₁ being Element of F_Real holds (0. F_Real ) * b₁ = 0. F_Real
by VECTSP_1:44;

registration

cluster F_Real -> multLoop_0-like ;
coherence by Lemma3, Lemma4, Lemma5, Lemma6, Lemma7, Lemma8, ALGSTR_1:34;

end;

definition

let c₁ be non empty add-left-cancelable add-right-invertible LoopStr ;
let c₂ be Element of c₁;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
func - c₂ -> Element of a₁ means :Def7: :: ALGSTR_2:def 7
a₂ + a₃ = 0. a₁;
existence by ALGSTR_1:def 9;
uniqueness by ALGSTR_1:def 6;

end;

:: deftheorem Def1 ALGSTR_2:def 1 :

:: deftheorem Def2 ALGSTR_2:def 2 :

:: deftheorem Def3 ALGSTR_2:def 3 :

:: deftheorem Def4 ALGSTR_2:def 4 :

:: deftheorem Def5 ALGSTR_2:def 5 :

:: deftheorem Def6 ALGSTR_2:def 6 :

:: deftheorem Def7 defines - ALGSTR_2:def 7 :

definition

let c₁ be non empty add-left-cancelable add-right-invertible LoopStr ;
let c₂, c₃ be Element of c₁;
func c₂ - c₃ -> Element of a₁ equals :: ALGSTR_2:def 8
a₂ + (- a₃);
correctness ;

end;

:: deftheorem Def8 defines - ALGSTR_2:def 8 :

registration

cluster non empty Abelian add-associative right_zeroed unital associative commutative strict distributive non degenerated left_zeroed Loop-like multLoop_0-like doubleLoopStr ;
existence

proof end;

end;

definition

mode doubleLoop is non empty right_zeroed unital left_zeroed Loop-like multLoop_0-like doubleLoopStr ;

end;

definition

mode leftQuasi-Field is Abelian add-associative right-distributive non degenerated doubleLoop;

end;

theorem Th1: :: ALGSTR_2:1

canceled;

theorem Th2: :: ALGSTR_2:2

canceled;

theorem Th3: :: ALGSTR_2:3

canceled;

theorem Th4: :: ALGSTR_2:4

canceled;

theorem Th5: :: ALGSTR_2:5

canceled;

theorem Th6: :: ALGSTR_2:6

canceled;

theorem Th7: :: ALGSTR_2:7

canceled;

theorem Th8: :: ALGSTR_2:8

canceled;

theorem Th9: :: ALGSTR_2:9

canceled;

theorem Th10: :: ALGSTR_2:10

canceled;

theorem Th11: :: ALGSTR_2:11

canceled;

theorem Th12: :: ALGSTR_2:12

for b₁ being non empty doubleLoopStr holds
( b₁ is leftQuasi-Field iff ( ( for b₂ being Element of b₁ holds b₂ + (0. b₁) = b₂ ) & ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ + b₃ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) ) & ( for b₂, b₃ being Element of b₁ holds b₂ + b₃ = b₃ + b₂ ) & 0. b₁ <> 1. b₁ & ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ holds (1. b₁) * b₂ = b₂ ) & ( for b₂, b₃ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₄ being Element of b₁ st b₂ * b₄ = b₃ ) & ( for b₂, b₃ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₄ being Element of b₁ st b₄ * b₂ = b₃ ) & ( for b₂, b₃, b₄ being Element of b₁ st b₂ <> 0. b₁ & b₂ * b₃ = b₂ * b₄ holds
b₃ = b₄ ) & ( for b₂, b₃, b₄ being Element of b₁ st b₂ <> 0. b₁ & b₃ * b₂ = b₄ * b₂ holds
b₃ = b₄ ) & ( for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁ ) & ( for b₂ being Element of b₁ holds (0. b₁) * b₂ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) ) ) )

proof end;

theorem Th13: :: ALGSTR_2:13

canceled;

theorem Th14: :: ALGSTR_2:14

for b₁ being Abelian right-distributive doubleLoop
for b₂, b₃ being Element of b₁ holds b₂ * (- b₃) = - (b₂ * b₃)

proof end;

theorem Th15: :: ALGSTR_2:15

for b₁ being non empty Abelian add-left-cancelable add-right-invertible LoopStr
for b₂ being Element of b₁ holds - (- b₂) = b₂

proof end;

theorem Th16: :: ALGSTR_2:16

for b₁ being Abelian right-distributive doubleLoop holds (- (1. b₁)) * (- (1. b₁)) = 1. b₁

proof end;

theorem Th17: :: ALGSTR_2:17

for b₁ being Abelian right-distributive doubleLoop
for b₂, b₃, b₄ being Element of b₁ holds b₂ * (b₃ - b₄) = (b₂ * b₃) - (b₂ * b₄)

proof end;

definition

mode rightQuasi-Field is Abelian add-associative left-distributive non degenerated doubleLoop;

end;

theorem Th18: :: ALGSTR_2:18

canceled;

theorem Th19: :: ALGSTR_2:19

for b₁ being non empty doubleLoopStr holds
( b₁ is rightQuasi-Field iff ( ( for b₂ being Element of b₁ holds b₂ + (0. b₁) = b₂ ) & ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ + b₃ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) ) & ( for b₂, b₃ being Element of b₁ holds b₂ + b₃ = b₃ + b₂ ) & 0. b₁ <> 1. b₁ & ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ holds (1. b₁) * b₂ = b₂ ) & ( for b₂, b₃ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₄ being Element of b₁ st b₂ * b₄ = b₃ ) & ( for b₂, b₃ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₄ being Element of b₁ st b₄ * b₂ = b₃ ) & ( for b₂, b₃, b₄ being Element of b₁ st b₂ <> 0. b₁ & b₂ * b₃ = b₂ * b₄ holds
b₃ = b₄ ) & ( for b₂, b₃, b₄ being Element of b₁ st b₂ <> 0. b₁ & b₃ * b₂ = b₄ * b₂ holds
b₃ = b₄ ) & ( for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁ ) & ( for b₂ being Element of b₁ holds (0. b₁) * b₂ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂) ) ) )

proof end;

theorem Th20: :: ALGSTR_2:20

canceled;

theorem Th21: :: ALGSTR_2:21

for b₁ being left-distributive doubleLoop
for b₂, b₃ being Element of b₁ holds (- b₂) * b₃ = - (b₂ * b₃)

proof end;

theorem Th22: :: ALGSTR_2:22

canceled;

theorem Th23: :: ALGSTR_2:23

for b₁ being Abelian left-distributive doubleLoop holds (- (1. b₁)) * (- (1. b₁)) = 1. b₁

proof end;

theorem Th24: :: ALGSTR_2:24

for b₁ being left-distributive doubleLoop
for b₂, b₃, b₄ being Element of b₁ holds (b₂ - b₃) * b₄ = (b₂ * b₄) - (b₃ * b₄)

proof end;

definition

mode doublesidedQuasi-Field is Abelian add-associative distributive non degenerated doubleLoop;

end;

theorem Th25: :: ALGSTR_2:25

canceled;

theorem Th26: :: ALGSTR_2:26

for b₁ being non empty doubleLoopStr holds
( b₁ is doublesidedQuasi-Field iff ( ( for b₂ being Element of b₁ holds b₂ + (0. b₁) = b₂ ) & ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ + b₃ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) ) & ( for b₂, b₃ being Element of b₁ holds b₂ + b₃ = b₃ + b₂ ) & 0. b₁ <> 1. b₁ & ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ holds (1. b₁) * b₂ = b₂ ) & ( for b₂, b₃ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₄ being Element of b₁ st b₂ * b₄ = b₃ ) & ( for b₂, b₃ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₄ being Element of b₁ st b₄ * b₂ = b₃ ) & ( for b₂, b₃, b₄ being Element of b₁ st b₂ <> 0. b₁ & b₂ * b₃ = b₂ * b₄ holds
b₃ = b₄ ) & ( for b₂, b₃, b₄ being Element of b₁ st b₂ <> 0. b₁ & b₃ * b₂ = b₄ * b₂ holds
b₃ = b₄ ) & ( for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁ ) & ( for b₂ being Element of b₁ holds (0. b₁) * b₂ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂) ) ) )

proof end;

definition

mode _Skew-Field is associative doublesidedQuasi-Field;

end;

Lemma13: for b₁ being non empty doubleLoopStr
for b₂, b₃ being Element of b₁ st 0. b₁ <> 1. b₁ & ( for b₄ being Element of b₁ holds b₄ * (1. b₁) = b₄ ) & ( for b₄ being Element of b₁ st b₄ <> 0. b₁ holds
ex b₅ being Element of b₁ st b₄ * b₅ = 1. b₁ ) & ( for b₄, b₅, b₆ being Element of b₁ holds (b₄ * b₅) * b₆ = b₄ * (b₅ * b₆) ) & ( for b₄ being Element of b₁ holds b₄ * (0. b₁) = 0. b₁ ) & ( for b₄ being Element of b₁ holds (0. b₁) * b₄ = 0. b₁ ) & b₂ * b₃ = 1. b₁ holds
b₃ * b₂ = 1. b₁

proof end;

Lemma14: for b₁ being non empty doubleLoopStr
for b₂ being Element of b₁ st 0. b₁ <> 1. b₁ & ( for b₃ being Element of b₁ holds b₃ * (1. b₁) = b₃ ) & ( for b₃ being Element of b₁ st b₃ <> 0. b₁ holds
ex b₄ being Element of b₁ st b₃ * b₄ = 1. b₁ ) & ( for b₃, b₄, b₅ being Element of b₁ holds (b₃ * b₄) * b₅ = b₃ * (b₄ * b₅) ) & ( for b₃ being Element of b₁ holds b₃ * (0. b₁) = 0. b₁ ) & ( for b₃ being Element of b₁ holds (0. b₁) * b₃ = 0. b₁ ) holds
(1. b₁) * b₂ = b₂ * (1. b₁)

proof end;

Lemma15: for b₁ being non empty doubleLoopStr st 0. b₁ <> 1. b₁ & ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₃ being Element of b₁ st b₂ * b₃ = 1. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) & ( for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁ ) & ( for b₂ being Element of b₁ holds (0. b₁) * b₂ = 0. b₁ ) holds
for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₃ being Element of b₁ st b₃ * b₂ = 1. b₁

proof end;

theorem Th27: :: ALGSTR_2:27

canceled;

theorem Th28: :: ALGSTR_2:28

canceled;

theorem Th29: :: ALGSTR_2:29

canceled;

theorem Th30: :: ALGSTR_2:30

canceled;

theorem Th31: :: ALGSTR_2:31

canceled;

theorem Th32: :: ALGSTR_2:32

for b₁ being non empty doubleLoopStr holds
( b₁ is _Skew-Field iff ( ( for b₂ being Element of b₁ holds b₂ + (0. b₁) = b₂ ) & ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ + b₃ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) ) & ( for b₂, b₃ being Element of b₁ holds b₂ + b₃ = b₃ + b₂ ) & 0. b₁ <> 1. b₁ & ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₃ being Element of b₁ st b₂ * b₃ = 1. b₁ ) & ( for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁ ) & ( for b₂ being Element of b₁ holds (0. b₁) * b₂ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) & ( for b₂, b₃, b₄ being Element of b₁ holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₃ + b₄) * b₂ = (b₃ * b₂) + (b₄ * b₂) ) ) )

proof end;

definition

mode _Field is commutative _Skew-Field;

end;

theorem Th33: :: ALGSTR_2:33

canceled;

theorem Th34: :: ALGSTR_2:34

for b₁ being non empty doubleLoopStr holds
( b₁ is _Field iff ( ( for b₂ being Element of b₁ holds b₂ + (0. b₁) = b₂ ) & ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st b₂ + b₃ = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) ) & ( for b₂, b₃ being Element of b₁ holds b₂ + b₃ = b₃ + b₂ ) & 0. b₁ <> 1. b₁ & ( for b₂ being Element of b₁ holds b₂ * (1. b₁) = b₂ ) & ( for b₂ being Element of b₁ st b₂ <> 0. b₁ holds
ex b₃ being Element of b₁ st b₂ * b₃ = 1. b₁ ) & ( for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁ ) & ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) & ( for b₂, b₃, b₄ being Element of b₁ holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) ) & ( for b₂, b₃ being Element of b₁ holds b₂ * b₃ = b₃ * b₂ ) ) )

proof end;