environ
vocabularies HIDDEN, XBOOLE_0, ALGSTR_0, SUBSET_1, ARYTM_3, SUPINF_2, RLVECT_1, STRUCT_0, ARYTM_1, VECTSP_1, RELAT_1, MESFUNC1, GROUP_1, BINOP_1, NUMBERS, BINOP_2, CARD_1, REAL_1, ALGSTR_1, ZFMISC_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, BINOP_2, FUNCT_7, STRUCT_0, ALGSTR_0, GROUP_1, VECTSP_1, RLVECT_1;
definitions VECTSP_1, ALGSTR_0, RLVECT_1, GROUP_1;
theorems RLVECT_1, VECTSP_1, TARSKI, XCMPLX_1, BINOP_2, GROUP_1, ALGSTR_0, STRUCT_0;
schemes ;
registrations NUMBERS, VECTSP_1, ALGSTR_0, XREAL_0, ORDINAL1, STRUCT_0;
constructors HIDDEN, BINOP_1, BINOP_2, VECTSP_1, RLVECT_1, FUNCT_5, XXREAL_0, REAL_1, FUNCT_7, GROUP_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, ALGSTR_0, ORDINAL1;
expansions STRUCT_0, VECTSP_1, ALGSTR_0, RLVECT_1, GROUP_1;
Lm1:
( ( for a being Element of Trivial-addLoopStr holds a + (0. Trivial-addLoopStr) = a ) & ( for a being Element of Trivial-addLoopStr holds (0. Trivial-addLoopStr) + a = a ) )
by Th4;
Lm2:
for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st a + x = b
Lm3:
for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st x + a = b
Lm4:
( ( for a, x, y being Element of Trivial-addLoopStr st a + x = a + y holds
x = y ) & ( for a, x, y being Element of Trivial-addLoopStr st x + a = y + a holds
x = y ) )
by Th4;
Lm5:
for a, b, c being Element of Trivial-addLoopStr holds (a + b) + c = a + (b + c)
by Th4;
Lm6:
for a, b being Element of Trivial-addLoopStr holds a + b = b + a
by Th4;
Lm7:
( ( for a being Element of Trivial-multLoopStr holds a * (1. Trivial-multLoopStr) = a ) & ( for a being Element of Trivial-multLoopStr holds (1. Trivial-multLoopStr) * a = a ) )
by Th9;
Lm8:
for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st a * x = b
Lm9:
for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st x * a = b
Lm10:
for a, b, c being Element of Trivial-multLoopStr holds (a * b) * c = a * (b * c)
by Th9;
Lm11:
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
Lm12:
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)
Lm13:
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
Lm14:
for a, b being Element of Trivial-multLoopStr holds a * b = b * a
by Th9;
canceled;
Lm16:
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
Lm17:
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
Lm18:
for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & a * x = a * y holds
x = y
Lm19:
for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & x * a = y * a holds
x = y
Lm20:
for a being Element of multEX_0 holds a * (0. multEX_0) = 0. multEX_0
Lm21:
for a being Element of multEX_0 holds (0. multEX_0) * a = 0. multEX_0
Lm22:
for a, b, c being Element of multEX_0 holds (a * b) * c = a * (b * c)
Lm23:
for a, b being Element of multEX_0 holds a * b = b * a
:: let L be invertible cancelable non empty multLoopStr;
:: let a, b be Element of L;
:: func a/b -> Element of L equals
:: a*(b");
:: correctness;
:: end;
::$CD