:: ALGSTR_1 semantic presentation

theorem Th1: :: ALGSTR_1:1

for L being non empty LoopStr
for a, b being Element of L st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & a + b = 0. L holds
b + a = 0. L

proof end;

theorem Th2: :: ALGSTR_1:2

for L being non empty LoopStr
for a being Element of L st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) holds
(0. L) + a = a + (0. L)

proof end;

theorem Th3: :: ALGSTR_1:3

for L being non empty LoopStr st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) holds
for a being Element of L ex x being Element of L st x + a = 0. L

proof end;

definition

let x be set ;
canceled;
canceled;
func Extract x -> Element of {x} equals :: ALGSTR_1:def 3
x;
coherence by TARSKI:def 1;

end;

:: deftheorem ALGSTR_1:def 1 :

:: deftheorem ALGSTR_1:def 2 :

:: deftheorem defines Extract ALGSTR_1:def 3 :

definition

func L_Trivial -> strict LoopStr equals :: ALGSTR_1:def 4
LoopStr(# {{} },op2 ,(Extract {} ) #);
correctness ;

end;

:: deftheorem defines L_Trivial ALGSTR_1:def 4 :

registration

cluster L_Trivial -> non empty strict ;
coherence

proof end;

end;

theorem :: ALGSTR_1:4

canceled;

theorem Th5: :: ALGSTR_1:5

for a, b being Element of L_Trivial holds a = b

proof end;

theorem :: ALGSTR_1:6

for a, b being Element of L_Trivial holds a + b = 0. L_Trivial by Th5;

Lm1: for a being Element of L_Trivial holds a + (0. L_Trivial ) = a
by Th5;

Lm2: for a being Element of L_Trivial holds (0. L_Trivial ) + a = a
by Th5;

Lm3: for a, b being Element of L_Trivial ex x being Element of L_Trivial st a + x = b

proof end;

Lm4: for a, b being Element of L_Trivial ex x being Element of L_Trivial st x + a = b

proof end;

Lm5: for a, x, y being Element of L_Trivial st a + x = a + y holds
x = y
by Th5;

Lm6: for a, x, y being Element of L_Trivial st x + a = y + a holds
x = y
by Th5;

definition

let IT be non empty LoopStr ;
attr IT is left_zeroed means :Def5: :: ALGSTR_1:def 5
for a being Element of IT holds (0. IT) + a = a;

end;

:: deftheorem Def5 defines left_zeroed ALGSTR_1:def 5 :

definition

let L be non empty LoopStr ;
attr L is add-left-cancelable means :Def6: :: ALGSTR_1:def 6
for a, b, c being Element of L st a + b = a + c holds
b = c;
attr L is add-right-cancelable means :Def7: :: ALGSTR_1:def 7
for a, b, c being Element of L st b + a = c + a holds
b = c;
attr L is add-left-invertible means :Def8: :: ALGSTR_1:def 8
for a, b being Element of L ex x being Element of L st x + a = b;
attr L is add-right-invertible means :Def9: :: ALGSTR_1:def 9
for a, b being Element of L ex x being Element of L st a + x = b;

end;

:: deftheorem Def6 defines add-left-cancelable ALGSTR_1:def 6 :

:: deftheorem Def7 defines add-right-cancelable ALGSTR_1:def 7 :

:: deftheorem Def8 defines add-left-invertible ALGSTR_1:def 8 :

:: deftheorem Def9 defines add-right-invertible ALGSTR_1:def 9 :

definition

let IT be non empty LoopStr ;
attr IT is Loop-like means :Def10: :: ALGSTR_1:def 10
( IT is add-left-cancelable & IT is add-right-cancelable & IT is add-left-invertible & IT is add-right-invertible );

end;

:: deftheorem Def10 defines Loop-like ALGSTR_1:def 10 :

registration

cluster non empty Loop-like -> non empty add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible LoopStr ;
coherence by Def10;
cluster non empty add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible -> non empty Loop-like LoopStr ;
coherence by Def10;

end;

theorem Th7: :: ALGSTR_1:7

for L being non empty LoopStr holds
( L is Loop-like iff ( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( for a, b being Element of L ex x being Element of L st x + a = b ) & ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) ) )

proof end;

Lm7: for a, b, c being Element of L_Trivial holds (a + b) + c = a + (b + c)
by Th5;

Lm8: for a, b being Element of L_Trivial holds a + b = b + a
by Th5;

registration end;

registration

cluster non empty strict right_zeroed left_zeroed add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible Loop-like LoopStr ;
existence

proof end;

end;

definition

mode Loop is non empty right_zeroed left_zeroed Loop-like LoopStr ;

end;

registration

cluster strict add-associative LoopStr ;
existence

proof end;

end;

definition

mode Group is add-associative Loop;

end;

registration

cluster non empty Loop-like -> non empty right_complementable LoopStr ;
coherence

proof end;

cluster non empty add-associative right_zeroed right_complementable -> non empty left_zeroed add-left-cancelable add-right-cancelable add-left-invertible add-right-invertible Loop-like LoopStr ;
coherence

proof end;

end;

theorem :: ALGSTR_1:8

canceled;

theorem Th9: :: ALGSTR_1:9

for L being non empty LoopStr holds
( L is Group iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) ) )

proof end;

registration end;

registration

cluster strict Abelian right_complementable LoopStr ;
existence

proof end;

end;

theorem :: ALGSTR_1:10

canceled;

theorem :: ALGSTR_1:11

for L being non empty LoopStr holds
( L is Abelian Group iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) ) ) by Th9, RLVECT_1:def 5;

definition

func multL_Trivial -> strict multLoopStr equals :: ALGSTR_1:def 11
multLoopStr(# {{} },op2 ,(Extract {} ) #);
correctness ;

end;

:: deftheorem defines multL_Trivial ALGSTR_1:def 11 :

registration

cluster multL_Trivial -> non empty strict ;
coherence

proof end;

end;

theorem :: ALGSTR_1:12

canceled;

theorem :: ALGSTR_1:13

canceled;

theorem :: ALGSTR_1:14

canceled;

theorem :: ALGSTR_1:15

canceled;

theorem :: ALGSTR_1:16

canceled;

theorem :: ALGSTR_1:17

canceled;

theorem Th18: :: ALGSTR_1:18

for a, b being Element of multL_Trivial holds a = b

proof end;

theorem :: ALGSTR_1:19

for a, b being Element of multL_Trivial holds a * b = 1. multL_Trivial by Th18;

Lm9: for a being Element of multL_Trivial holds a * (1. multL_Trivial ) = a
by Th18;

Lm10: for a being Element of multL_Trivial holds (1. multL_Trivial ) * a = a
by Th18;

Lm11: for a, b being Element of multL_Trivial ex x being Element of multL_Trivial st a * x = b

proof end;

Lm12: for a, b being Element of multL_Trivial ex x being Element of multL_Trivial st x * a = b

proof end;

Lm13: for a, x, y being Element of multL_Trivial st a * x = a * y holds
x = y
by Th18;

Lm14: for a, x, y being Element of multL_Trivial st x * a = y * a holds
x = y
by Th18;

definition

let IT be non empty multLoopStr ;
attr IT is invertible means :Def12: :: ALGSTR_1:def 12
( ( for a, b being Element of IT ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT ex x being Element of IT st x * a = b ) );
attr IT is cancelable means :Def13: :: ALGSTR_1:def 13
( ( for a, x, y being Element of IT st a * x = a * y holds
x = y ) & ( for a, x, y being Element of IT st x * a = y * a holds
x = y ) );

end;

:: deftheorem Def12 defines invertible ALGSTR_1:def 12 :

:: deftheorem Def13 defines cancelable ALGSTR_1:def 13 :

registration

cluster non empty unital strict invertible cancelable multLoopStr ;
existence

proof end;

end;

definition

mode multLoop is non empty unital invertible cancelable multLoopStr ;

end;

registration

cluster multL_Trivial -> non empty unital strict invertible cancelable ;
coherence by Def12, Def13, Lm9, Lm10, Lm11, Lm12, Lm13, Lm14, GROUP_1:def 2;

end;

Lm15: for a, b, c being Element of multL_Trivial holds (a * b) * c = a * (b * c)
by Th18;

registration

cluster associative strict multLoopStr ;
existence

proof end;

end;

definition

mode multGroup is associative multLoop;

end;

Lm16: for L being non empty multLoopStr
for a, b being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & a * b = 1. L holds
b * a = 1. L

proof end;

Lm17: for L being non empty multLoopStr
for a being Element of L st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) holds
(1. L) * a = a * (1. L)

proof end;

Lm18: for L being non empty multLoopStr st ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) holds
for a being Element of L ex x being Element of L st x * a = 1. L

proof end;

theorem :: ALGSTR_1:20

canceled;

theorem :: ALGSTR_1:21

canceled;

theorem Th22: :: ALGSTR_1:22

for L being non empty multLoopStr holds
( L is multGroup iff ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) ) )

proof end;

registration

cluster multL_Trivial -> non empty unital associative strict invertible cancelable ;
coherence by Lm15, GROUP_1:def 4;

end;

Lm19: for a, b being Element of multL_Trivial holds a * b = b * a
by Th18;

registration

cluster commutative strict multLoopStr ;
existence

proof end;

end;

theorem :: ALGSTR_1:23

canceled;

theorem :: ALGSTR_1:24

for L being non empty multLoopStr holds
( L is commutative multGroup iff ( ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) ) by Th22, GROUP_1:def 16;

definition

let L be non empty invertible cancelable multLoopStr ;
let a be Element of L;
canceled;
canceled;
func a " -> Element of L means :Def16: :: ALGSTR_1:def 16
a * it = 1. L;
existence by Def12;
uniqueness by Def13;

end;

:: deftheorem ALGSTR_1:def 14 :

:: deftheorem ALGSTR_1:def 15 :

:: deftheorem Def16 defines " ALGSTR_1:def 16 :

theorem :: ALGSTR_1:25

canceled;

theorem :: ALGSTR_1:26

for G being multGroup
for a being Element of G holds
( a * (a " ) = 1. G & (a " ) * a = 1. G )

proof end;

definition

let L be non empty invertible cancelable multLoopStr ;
let a, b be Element of L;
func a / b -> Element of L equals :: ALGSTR_1:def 17
a * (b " );
correctness ;

end;

:: deftheorem defines / ALGSTR_1:def 17 :

definition

canceled;
canceled;
canceled;
func multEX_0 -> strict multLoopStr_0 equals :: ALGSTR_1:def 21
multLoopStr_0(# REAL ,multreal ,1,0 #);
correctness ;

end;

:: deftheorem ALGSTR_1:def 18 :

:: deftheorem ALGSTR_1:def 19 :

:: deftheorem ALGSTR_1:def 20 :

:: deftheorem defines multEX_0 ALGSTR_1:def 21 :

registration

cluster multEX_0 -> non empty strict ;
coherence

proof end;

end;

Lm20: for a, b being Element of multEX_0
for x, y being Real st a = x & b = y holds
a * b = x * y
by BINOP_2:def 11;

Lm21: now

let x, e be Element of multEX_0 ; :: thesis:
assume A1: e = 1 ; :: thesis:
reconsider a = x as Real ;
thus x * e = multreal . a,1 by A1
.= a * 1 by BINOP_2:def 11
.= x ; :: thesis:
thus e * x = multreal . 1,a by A1
.= 1 * a by BINOP_2:def 11
.= x ; :: thesis:

end;

registration

cluster multEX_0 -> non empty unital strict ;
coherence

proof end;

end;

Lm22: 0 = 0. multEX_0
;

Lm23: 1 = 1. multEX_0

proof end;

theorem :: ALGSTR_1:27

canceled;

theorem :: ALGSTR_1:28

canceled;

theorem :: ALGSTR_1:29

canceled;

theorem :: ALGSTR_1:30

canceled;

theorem :: ALGSTR_1:31

canceled;

theorem Th32: :: ALGSTR_1:32

for q, p being Real st q <> 0 holds
ex y being Real st p = q * y

proof end;

theorem Th33: :: ALGSTR_1:33

for q, p being Real st q <> 0 holds
ex y being Real st p = y * q

proof end;

Lm24: for a, b being Element of multEX_0 st a <> 0. multEX_0 holds
ex x being Element of multEX_0 st a * x = b

proof end;

Lm25: for a, b being Element of multEX_0 st a <> 0. multEX_0 holds
ex x being Element of multEX_0 st x * a = b

proof end;

Lm26: for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & a * x = a * y holds
x = y

proof end;

Lm27: for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & x * a = y * a holds
x = y

proof end;

Lm28: for a being Element of multEX_0 holds a * (0. multEX_0 ) = 0. multEX_0

proof end;

Lm29: for a being Element of multEX_0 holds (0. multEX_0 ) * a = 0. multEX_0

proof end;

definition

let IT be non empty multLoopStr_0 ;
attr IT is almost_invertible means :Def22: :: ALGSTR_1:def 22
( ( for a, b being Element of IT st a <> 0. IT holds
ex x being Element of IT st a * x = b ) & ( for a, b being Element of IT st a <> 0. IT holds
ex x being Element of IT st x * a = b ) );
attr IT is almost_cancelable means :Def23: :: ALGSTR_1:def 23
( ( for a, x, y being Element of IT st a <> 0. IT & a * x = a * y holds
x = y ) & ( for a, x, y being Element of IT st a <> 0. IT & x * a = y * a holds
x = y ) );

end;

:: deftheorem Def22 defines almost_invertible ALGSTR_1:def 22 :

:: deftheorem Def23 defines almost_cancelable ALGSTR_1:def 23 :

definition

let IT be non empty multLoopStr_0 ;
attr IT is multLoop_0-like means :Def24: :: ALGSTR_1:def 24
( IT is almost_invertible & IT is almost_cancelable & ( for a being Element of IT holds a * (0. IT) = 0. IT ) & ( for a being Element of IT holds (0. IT) * a = 0. IT ) );

end;

:: deftheorem Def24 defines multLoop_0-like ALGSTR_1:def 24 :

theorem Th34: :: ALGSTR_1:34

for L being non empty multLoopStr_0 holds
( L is multLoop_0-like iff ( ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) )

proof end;

registration

cluster non empty multLoop_0-like -> non empty almost_invertible almost_cancelable multLoopStr_0 ;
coherence by Def24;

end;

registration

cluster non empty unital strict non degenerated almost_invertible almost_cancelable multLoop_0-like multLoopStr_0 ;
existence

proof end;

end;

definition

mode multLoop_0 is non empty unital non degenerated multLoop_0-like multLoopStr_0 ;

end;

registration

cluster multEX_0 -> non empty unital strict almost_invertible almost_cancelable multLoop_0-like ;
coherence by Lm24, Lm25, Lm26, Lm27, Lm28, Lm29, Th34;

end;

Lm30: for a, b, c being Element of multEX_0 holds (a * b) * c = a * (b * c)

proof end;

registration

cluster associative strict multLoopStr_0 ;
existence

proof end;

end;

definition

mode multGroup_0 is associative non degenerated multLoop_0;

end;

Lm31: for L being non empty multLoopStr_0
for a, b being Element of L st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) & a * b = 1. L holds
b * a = 1. L

proof end;

Lm32: for L being non empty multLoopStr_0
for a being Element of L st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) holds
(1. L) * a = a * (1. L)

proof end;

Lm33: for L being non empty multLoopStr_0 st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) holds
for a being Element of L st a <> 0. L holds
ex x being Element of L st x * a = 1. L

proof end;

theorem :: ALGSTR_1:35

canceled;

theorem Th36: :: ALGSTR_1:36

for L being non empty multLoopStr_0 holds
( L is multGroup_0 iff ( 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) )

proof end;

registration

cluster multEX_0 -> non empty unital associative strict almost_invertible almost_cancelable multLoop_0-like ;
coherence by Lm30, GROUP_1:def 4;

end;

Lm34: for a, b being Element of multEX_0 holds a * b = b * a

proof end;

registration

cluster commutative strict multLoopStr_0 ;
existence

proof end;

end;

theorem :: ALGSTR_1:37

canceled;

theorem :: ALGSTR_1:38

for L being non empty multLoopStr_0 holds
( L is commutative multGroup_0 iff ( 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b being Element of L holds a * b = b * a ) ) ) by Th36, GROUP_1:def 16;

definition

let L be non empty almost_invertible almost_cancelable multLoopStr_0 ;
let a be Element of L;
assume A1: a <> 0. L ;
func a " -> Element of L means :Def25: :: ALGSTR_1:def 25
a * it = 1. L;
existence by A1, Def22;
uniqueness by A1, Def23;

end;

:: deftheorem Def25 defines " ALGSTR_1:def 25 :

theorem :: ALGSTR_1:39

canceled;

theorem :: ALGSTR_1:40

for G being non empty unital associative almost_invertible almost_cancelable multLoopStr_0
for a being Element of G st a <> 0. G holds
( a * (a " ) = 1. G & (a " ) * a = 1. G )

proof end;

definition

let L be non empty almost_invertible almost_cancelable multLoopStr_0 ;
let a, b be Element of L;
func a / b -> Element of L equals :: ALGSTR_1:def 26
a * (b " );
correctness ;

end;

:: deftheorem defines / ALGSTR_1:def 26 :