:: ALGSTR_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for a, b being Element of F_Real
for x, y being Real st a = x & b = y holds
a * b = x * y
proof end;

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

Lm3: for a, b being Element of F_Real st a <> 0. F_Real holds
ex x being Element of F_Real st a * x = b
proof end;

Lm4: for a, b being Element of F_Real st a <> 0. F_Real holds
ex x being Element of F_Real st x * a = b
proof end;

Lm5: for a, x, y being Element of F_Real st a <> 0. F_Real & a * x = a * y holds
x = y
by VECTSP_1:33;

Lm6: for a, x, y being Element of F_Real st a <> 0. F_Real & x * a = y * a holds
x = y
by VECTSP_1:33;

Lm7: for a being Element of F_Real holds a * (0. F_Real ) = 0. F_Real
by VECTSP_1:44;

Lm8: for a being Element of F_Real holds (0. F_Real ) * a = 0. F_Real
by VECTSP_1:44;

registration
cluster F_Real -> multLoop_0-like ;
coherence
F_Real is multLoop_0-like by Lm3, Lm4, Lm5, Lm6, Lm7, Lm8, ALGSTR_1:34;
end;

definition
let L be non empty add-left-cancelable add-right-invertible LoopStr ;
let a be Element of L;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
func - a -> Element of L means :Def7: :: ALGSTR_2:def 7
a + it = 0. L;
existence
ex b1 being Element of L st a + b1 = 0. L by ALGSTR_1:def 9;
uniqueness
for b1, b2 being Element of L st a + b1 = 0. L & a + b2 = 0. L holds
b1 = b2 by ALGSTR_1:def 6;
end;

:: deftheorem ALGSTR_2:def 1 :
canceled;

:: deftheorem ALGSTR_2:def 2 :
canceled;

:: deftheorem ALGSTR_2:def 3 :
canceled;

:: deftheorem ALGSTR_2:def 4 :
canceled;

:: deftheorem ALGSTR_2:def 5 :
canceled;

:: deftheorem ALGSTR_2:def 6 :
canceled;

:: deftheorem Def7 defines - ALGSTR_2:def 7 :
for L being non empty add-left-cancelable add-right-invertible LoopStr
for a, b3 being Element of L holds
( b3 = - a iff a + b3 = 0. L );

definition
let L be non empty add-left-cancelable add-right-invertible LoopStr ;
let a, b be Element of L;
func a - b -> Element of L equals :: ALGSTR_2:def 8
a + (- b);
correctness
coherence
a + (- b) is Element of L;
;
end;

:: deftheorem defines - ALGSTR_2:def 8 :
for L being non empty add-left-cancelable add-right-invertible LoopStr
for a, b being Element of L holds a - b = a + (- b);

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
ex b1 being non empty doubleLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is commutative & b1 is associative & b1 is distributive & not b1 is degenerated & b1 is left_zeroed & b1 is right_zeroed & b1 is Loop-like & b1 is unital & b1 is multLoop_0-like )
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 :: ALGSTR_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr holds
( L is leftQuasi-Field 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 ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( 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 ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) ) )
proof end;

theorem :: ALGSTR_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th14: :: ALGSTR_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Abelian right-distributive doubleLoop
for a, b being Element of G holds a * (- b) = - (a * b)
proof end;

theorem Th15: :: ALGSTR_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non empty Abelian add-left-cancelable add-right-invertible LoopStr
for a being Element of G holds - (- a) = a
proof end;

theorem :: ALGSTR_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Abelian right-distributive doubleLoop holds (- (1. G)) * (- (1. G)) = 1. G
proof end;

theorem :: ALGSTR_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Abelian right-distributive doubleLoop
for a, x, y being Element of G holds a * (x - y) = (a * x) - (a * y)
proof end;

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

theorem :: ALGSTR_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr holds
( L is rightQuasi-Field 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 ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( 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 ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )
proof end;

theorem :: ALGSTR_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th21: :: ALGSTR_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being left-distributive doubleLoop
for b, a being Element of G holds (- b) * a = - (b * a)
proof end;

theorem :: ALGSTR_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Abelian left-distributive doubleLoop holds (- (1. G)) * (- (1. G)) = 1. G
proof end;

theorem :: ALGSTR_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being left-distributive doubleLoop
for x, y, a being Element of G holds (x - y) * a = (x * a) - (y * a)
proof end;

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

theorem :: ALGSTR_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr holds
( L is doublesidedQuasi-Field 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 ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( 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 ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )
proof end;

definition
mode _Skew-Field is associative doublesidedQuasi-Field;
end;

Lm9: for L being non empty doubleLoopStr
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 ) & ( for a being Element of L holds (0. L) * a = 0. L ) & a * b = 1. L holds
b * a = 1. L
proof end;

Lm10: for L being non empty doubleLoopStr
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 ) & ( for a being Element of L holds (0. L) * a = 0. L ) holds
(1. L) * a = a * (1. L)
proof end;

Lm11: for L being non empty doubleLoopStr 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 ) & ( for a being Element of L holds (0. L) * a = 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_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th32: :: ALGSTR_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr holds
( L is _Skew-Field 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 ) & 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 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, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )
proof end;

definition
mode _Field is commutative _Skew-Field;
end;

theorem :: ALGSTR_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALGSTR_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty doubleLoopStr holds
( L is _Field 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 ) & 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 being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) )
proof end;