:: ALGSTR_1 semantic presentation
begin
theorem Th1: :: ALGSTR_1:1
for L being non empty addLoopStr
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
let L be non empty addLoopStr ; ::_thesis: 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
let a, b be Element of L; ::_thesis: ( ( 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 implies b + a = 0. L )
assume that
A1: for a being Element of L holds a + (0. L) = a and
A2: for a being Element of L ex x being Element of L st a + x = 0. L and
A3: for a, b, c being Element of L holds (a + b) + c = a + (b + c) ; ::_thesis: ( not a + b = 0. L or b + a = 0. L )
consider x being Element of L such that
A4: b + x = 0. L by A2;
assume A5: a + b = 0. L ; ::_thesis: b + a = 0. L
thus b + a = (b + a) + (b + x) by A1, A4
.= ((b + a) + b) + x by A3
.= (b + (0. L)) + x by A3, A5
.= 0. L by A1, A4 ; ::_thesis: verum
end;
theorem :: ALGSTR_1:2
for L being non empty addLoopStr
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
let L be non empty addLoopStr ; ::_thesis: 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)
let a be Element of L; ::_thesis: ( ( 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) ) implies (0. L) + a = a + (0. L) )
assume that
A1: for a being Element of L holds a + (0. L) = a and
A2: for a being Element of L ex x being Element of L st a + x = 0. L and
A3: for a, b, c being Element of L holds (a + b) + c = a + (b + c) ; ::_thesis: (0. L) + a = a + (0. L)
consider x being Element of L such that
A4: a + x = 0. L by A2;
thus (0. L) + a = a + (x + a) by A3, A4
.= a + (0. L) by A1, A2, A3, A4, Th1 ; ::_thesis: verum
end;
theorem :: ALGSTR_1:3
for L being non empty addLoopStr 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
let L be non empty addLoopStr ; ::_thesis: ( ( 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) ) implies for a being Element of L ex x being Element of L st x + a = 0. L )
assume that
A1: for a being Element of L holds a + (0. L) = a and
A2: for a being Element of L ex x being Element of L st a + x = 0. L and
A3: for a, b, c being Element of L holds (a + b) + c = a + (b + c) ; ::_thesis: for a being Element of L ex x being Element of L st x + a = 0. L
let a be Element of L; ::_thesis: ex x being Element of L st x + a = 0. L
consider x being Element of L such that
A4: a + x = 0. L by A2;
x + a = 0. L by A1, A2, A3, A4, Th1;
hence ex x being Element of L st x + a = 0. L ; ::_thesis: verum
end;
definition
let x be set ;
func Extract x -> Element of {x} equals :: ALGSTR_1:def 1
x;
coherence
x is Element of {x} by TARSKI:def_1;
end;
:: deftheorem defines Extract ALGSTR_1:def_1_:_
for x being set holds Extract x = x;
theorem Th4: :: ALGSTR_1:4
for a, b being Element of Trivial-addLoopStr holds a = b
proof
let a, b be Element of Trivial-addLoopStr; ::_thesis: a = b
thus a = {} by CARD_1:49, TARSKI:def_1
.= b by CARD_1:49, TARSKI:def_1 ; ::_thesis: verum
end;
theorem :: ALGSTR_1:5
for a, b being Element of Trivial-addLoopStr holds a + b = 0. Trivial-addLoopStr by Th4;
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
proof
let a, b be Element of Trivial-addLoopStr; ::_thesis: ex x being Element of Trivial-addLoopStr st a + x = b
take 0. Trivial-addLoopStr ; ::_thesis: a + (0. Trivial-addLoopStr) = b
thus a + (0. Trivial-addLoopStr) = b by Th4; ::_thesis: verum
end;
Lm3: for a, b being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st x + a = b
proof
let a, b be Element of Trivial-addLoopStr; ::_thesis: ex x being Element of Trivial-addLoopStr st x + a = b
take 0. Trivial-addLoopStr ; ::_thesis: (0. Trivial-addLoopStr) + a = b
thus (0. Trivial-addLoopStr) + a = b by Th4; ::_thesis: verum
end;
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;
definition
let IT be non empty addLoopStr ;
attrIT is left_zeroed means :Def2: :: ALGSTR_1:def 2
for a being Element of IT holds (0. IT) + a = a;
end;
:: deftheorem Def2 defines left_zeroed ALGSTR_1:def_2_:_
for IT being non empty addLoopStr holds
( IT is left_zeroed iff for a being Element of IT holds (0. IT) + a = a );
definition
let L be non empty addLoopStr ;
attrL is add-left-invertible means :Def3: :: ALGSTR_1:def 3
for a, b being Element of L ex x being Element of L st x + a = b;
attrL is add-right-invertible means :Def4: :: ALGSTR_1:def 4
for a, b being Element of L ex x being Element of L st a + x = b;
end;
:: deftheorem Def3 defines add-left-invertible ALGSTR_1:def_3_:_
for L being non empty addLoopStr holds
( L is add-left-invertible iff for a, b being Element of L ex x being Element of L st x + a = b );
:: deftheorem Def4 defines add-right-invertible ALGSTR_1:def_4_:_
for L being non empty addLoopStr holds
( L is add-right-invertible iff for a, b being Element of L ex x being Element of L st a + x = b );
definition
let IT be non empty addLoopStr ;
attrIT is Loop-like means :Def5: :: ALGSTR_1:def 5
( IT is left_add-cancelable & IT is right_add-cancelable & IT is add-left-invertible & IT is add-right-invertible );
end;
:: deftheorem Def5 defines Loop-like ALGSTR_1:def_5_:_
for IT being non empty addLoopStr holds
( IT is Loop-like iff ( IT is left_add-cancelable & IT is right_add-cancelable & IT is add-left-invertible & IT is add-right-invertible ) );
registration
cluster non empty Loop-like -> non empty left_add-cancelable right_add-cancelable add-left-invertible add-right-invertible for addLoopStr ;
coherence
for b1 being non empty addLoopStr st b1 is Loop-like holds
( b1 is left_add-cancelable & b1 is right_add-cancelable & b1 is add-left-invertible & b1 is add-right-invertible ) by Def5;
cluster non empty left_add-cancelable right_add-cancelable add-left-invertible add-right-invertible -> non empty Loop-like for addLoopStr ;
coherence
for b1 being non empty addLoopStr st b1 is left_add-cancelable & b1 is right_add-cancelable & b1 is add-left-invertible & b1 is add-right-invertible holds
b1 is Loop-like by Def5;
end;
theorem Th6: :: ALGSTR_1:6
for L being non empty addLoopStr 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
let L be non empty addLoopStr ; ::_thesis: ( 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 ) ) )
thus ( L is Loop-like implies ( ( 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 ) ) ) by Def3, Def4, ALGSTR_0:def_3, ALGSTR_0:def_4; ::_thesis: ( ( 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 ) implies L is Loop-like )
assume that
A1: ( ( 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 ) ) and
A2: for a, x, y being Element of L st a + x = a + y holds
x = y and
A3: for a, x, y being Element of L st x + a = y + a holds
x = y ; ::_thesis: L is Loop-like
thus L is left_add-cancelable :: according to ALGSTR_1:def_5 ::_thesis: ( L is right_add-cancelable & L is add-left-invertible & L is add-right-invertible )
proof
let x, x, x be Element of L; :: according to ALGSTR_0:def_3,ALGSTR_0:def_6 ::_thesis: ( not x + x = x + x or x = x )
thus ( not x + x = x + x or x = x ) by A2; ::_thesis: verum
end;
thus L is right_add-cancelable ::_thesis: ( L is add-left-invertible & L is add-right-invertible )
proof
let x, x, x be Element of L; :: according to ALGSTR_0:def_4,ALGSTR_0:def_7 ::_thesis: ( not x + x = x + x or x = x )
thus ( not x + x = x + x or x = x ) by A3; ::_thesis: verum
end;
thus ( L is add-left-invertible & L is add-right-invertible ) by A1, Def3, Def4; ::_thesis: verum
end;
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;
registration
cluster Trivial-addLoopStr -> add-associative right_zeroed left_zeroed Loop-like ;
coherence
( Trivial-addLoopStr is add-associative & Trivial-addLoopStr is Loop-like & Trivial-addLoopStr is right_zeroed & Trivial-addLoopStr is left_zeroed ) by Def2, Lm1, Lm2, Lm3, Lm4, Lm5, Th6, RLVECT_1:def_3, RLVECT_1:def_4;
end;
registration
cluster non empty strict right_zeroed left_zeroed Loop-like for addLoopStr ;
existence
ex b1 being non empty addLoopStr st
( b1 is strict & b1 is left_zeroed & b1 is right_zeroed & b1 is Loop-like )
proof
take Trivial-addLoopStr ; ::_thesis: ( Trivial-addLoopStr is strict & Trivial-addLoopStr is left_zeroed & Trivial-addLoopStr is right_zeroed & Trivial-addLoopStr is Loop-like )
thus ( Trivial-addLoopStr is strict & Trivial-addLoopStr is left_zeroed & Trivial-addLoopStr is right_zeroed & Trivial-addLoopStr is Loop-like ) ; ::_thesis: verum
end;
end;
definition
mode Loop is non empty right_zeroed left_zeroed Loop-like addLoopStr ;
end;
registration
cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like for addLoopStr ;
existence
ex b1 being Loop st
( b1 is strict & b1 is add-associative )
proof
take Trivial-addLoopStr ; ::_thesis: ( Trivial-addLoopStr is strict & Trivial-addLoopStr is add-associative )
thus ( Trivial-addLoopStr is strict & Trivial-addLoopStr is add-associative ) ; ::_thesis: verum
end;
end;
registration
cluster non empty Loop-like -> non empty add-left-invertible for addLoopStr ;
coherence
for b1 being non empty addLoopStr st b1 is Loop-like holds
b1 is add-left-invertible ;
cluster non empty right_complementable add-associative right_zeroed -> non empty left_zeroed Loop-like for addLoopStr ;
coherence
for b1 being non empty addLoopStr st b1 is add-associative & b1 is right_zeroed & b1 is right_complementable holds
( b1 is left_zeroed & b1 is Loop-like )
proof
let L be non empty addLoopStr ; ::_thesis: ( L is add-associative & L is right_zeroed & L is right_complementable implies ( L is left_zeroed & L is Loop-like ) )
assume A1: ( L is add-associative & L is right_zeroed & L is right_complementable ) ; ::_thesis: ( L is left_zeroed & L is Loop-like )
then reconsider G = L as non empty right_complementable add-associative right_zeroed addLoopStr ;
A2: for a, x, y being Element of L st x + a = y + a holds
x = y by A1, RLVECT_1:8;
thus for a being Element of L holds (0. L) + a = a by A1, RLVECT_1:4; :: according to ALGSTR_1:def_2 ::_thesis: L is Loop-like
A3: for a, b being Element of L ex x being Element of L st x + a = b
proof
let a, b be Element of L; ::_thesis: ex x being Element of L st x + a = b
reconsider a9 = a, b9 = b as Element of G ;
reconsider x = b9 + (- a9) as Element of L ;
take x ; ::_thesis: x + a = b
(b9 + (- a9)) + a9 = b9 + ((- a9) + a9) by RLVECT_1:def_3
.= b9 + (0. G) by RLVECT_1:5
.= b by RLVECT_1:4 ;
hence x + a = b ; ::_thesis: verum
end;
( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( for a, x, y being Element of L st a + x = a + y holds
x = y ) ) by A1, RLVECT_1:7, RLVECT_1:8;
hence L is Loop-like by A3, A2, Th6; ::_thesis: verum
end;
end;
theorem Th7: :: ALGSTR_1:7
for L being non empty addLoopStr holds
( L is AddGroup 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
let L be non empty addLoopStr ; ::_thesis: ( L is AddGroup 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) ) ) )
thus ( L is AddGroup implies ( ( 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) ) ) ) by Th6, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: ( ( 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) ) implies L is AddGroup )
assume that
A1: for a being Element of L holds a + (0. L) = a and
A2: for a being Element of L ex x being Element of L st a + x = 0. L and
A3: for a, b, c being Element of L holds (a + b) + c = a + (b + c) ; ::_thesis: L is AddGroup
L is right_complementable
proof
let a be Element of L; :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable
thus ex x being Element of L st a + x = 0. L by A2; :: according to ALGSTR_0:def_11 ::_thesis: verum
end;
hence L is AddGroup by A1, A3, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: verum
end;
registration
cluster Trivial-addLoopStr -> Abelian ;
coherence
Trivial-addLoopStr is Abelian by Lm6, RLVECT_1:def_2;
end;
registration
cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like for addLoopStr ;
existence
ex b1 being AddGroup st
( b1 is strict & b1 is Abelian )
proof
take Trivial-addLoopStr ; ::_thesis: ( Trivial-addLoopStr is strict & Trivial-addLoopStr is Abelian )
thus ( Trivial-addLoopStr is strict & Trivial-addLoopStr is Abelian ) ; ::_thesis: verum
end;
end;
theorem :: ALGSTR_1:8
for L being non empty addLoopStr holds
( L is Abelian AddGroup 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 Th7, RLVECT_1:def_2;
registration
cluster Trivial-multLoopStr -> non empty ;
coherence
not Trivial-multLoopStr is empty ;
end;
theorem Th9: :: ALGSTR_1:9
for a, b being Element of Trivial-multLoopStr holds a = b
proof
let a, b be Element of Trivial-multLoopStr; ::_thesis: a = b
thus a = {} by CARD_1:49, TARSKI:def_1
.= b by CARD_1:49, TARSKI:def_1 ; ::_thesis: verum
end;
theorem :: ALGSTR_1:10
for a, b being Element of Trivial-multLoopStr holds a * b = 1. Trivial-multLoopStr by Th9;
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
proof
let a, b be Element of Trivial-multLoopStr; ::_thesis: ex x being Element of Trivial-multLoopStr st a * x = b
take 1_ Trivial-multLoopStr ; ::_thesis: a * (1_ Trivial-multLoopStr) = b
thus a * (1_ Trivial-multLoopStr) = b by Th9; ::_thesis: verum
end;
Lm9: for a, b being Element of Trivial-multLoopStr ex x being Element of Trivial-multLoopStr st x * a = b
proof
let a, b be Element of Trivial-multLoopStr; ::_thesis: ex x being Element of Trivial-multLoopStr st x * a = b
take 1_ Trivial-multLoopStr ; ::_thesis: (1_ Trivial-multLoopStr) * a = b
thus (1_ Trivial-multLoopStr) * a = b by Th9; ::_thesis: verum
end;
definition
let IT be non empty multLoopStr ;
attrIT is invertible means :Def6: :: ALGSTR_1:def 6
( ( 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 ) );
end;
:: deftheorem Def6 defines invertible ALGSTR_1:def_6_:_
for IT being non empty multLoopStr holds
( IT is invertible iff ( ( 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 ) ) );
notation
let L be non empty multLoopStr ;
synonym cancelable L for mult-cancelable ;
end;
registration
cluster non empty cancelable strict well-unital invertible for multLoopStr ;
existence
ex b1 being non empty multLoopStr st
( b1 is strict & b1 is well-unital & b1 is invertible & b1 is cancelable )
proof
( Trivial-multLoopStr is well-unital & Trivial-multLoopStr is invertible & Trivial-multLoopStr is cancelable ) by Def6, Lm7, Lm8, Lm9, VECTSP_1:def_6;
hence ex b1 being non empty multLoopStr st
( b1 is strict & b1 is well-unital & b1 is invertible & b1 is cancelable ) ; ::_thesis: verum
end;
end;
definition
mode multLoop is non empty cancelable well-unital invertible multLoopStr ;
end;
registration
cluster Trivial-multLoopStr -> cancelable well-unital invertible ;
coherence
( Trivial-multLoopStr is well-unital & Trivial-multLoopStr is invertible & Trivial-multLoopStr is cancelable ) by Def6, Lm7, Lm8, Lm9, VECTSP_1:def_6;
end;
Lm10: for a, b, c being Element of Trivial-multLoopStr holds (a * b) * c = a * (b * c)
by Th9;
registration
cluster non empty left_mult-cancelable right_mult-cancelable cancelable strict unital associative right_unital well-unital left_unital invertible for multLoopStr ;
existence
ex b1 being multLoop st
( b1 is strict & b1 is associative )
proof
Trivial-multLoopStr is associative by Lm10, GROUP_1:def_3;
hence ex b1 being multLoop st
( b1 is strict & b1 is associative ) ; ::_thesis: verum
end;
end;
definition
mode multGroup is associative multLoop;
end;
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
proof
let L be non empty multLoopStr ; ::_thesis: 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
let a, b be Element of L; ::_thesis: ( ( 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 implies b * a = 1. L )
assume that
A1: for a being Element of L holds a * (1. L) = a and
A2: for a being Element of L ex x being Element of L st a * x = 1. L and
A3: for a, b, c being Element of L holds (a * b) * c = a * (b * c) ; ::_thesis: ( not a * b = 1. L or b * a = 1. L )
consider x being Element of L such that
A4: b * x = 1. L by A2;
assume A5: a * b = 1. L ; ::_thesis: b * a = 1. L
thus b * a = (b * a) * (b * x) by A1, A4
.= ((b * a) * b) * x by A3
.= (b * (1. L)) * x by A3, A5
.= 1. L by A1, A4 ; ::_thesis: verum
end;
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)
proof
let L be non empty multLoopStr ; ::_thesis: 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)
let a be Element of L; ::_thesis: ( ( 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) ) implies (1. L) * a = a * (1. L) )
assume that
A1: for a being Element of L holds a * (1. L) = a and
A2: for a being Element of L ex x being Element of L st a * x = 1. L and
A3: for a, b, c being Element of L holds (a * b) * c = a * (b * c) ; ::_thesis: (1. L) * a = a * (1. L)
consider x being Element of L such that
A4: a * x = 1. L by A2;
thus (1. L) * a = a * (x * a) by A3, A4
.= a * (1. L) by A1, A2, A3, A4, Lm11 ; ::_thesis: verum
end;
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
proof
let L be non empty multLoopStr ; ::_thesis: ( ( 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) ) implies for a being Element of L ex x being Element of L st x * a = 1. L )
assume that
A1: for a being Element of L holds a * (1. L) = a and
A2: for a being Element of L ex x being Element of L st a * x = 1. L and
A3: for a, b, c being Element of L holds (a * b) * c = a * (b * c) ; ::_thesis: for a being Element of L ex x being Element of L st x * a = 1. L
let a be Element of L; ::_thesis: ex x being Element of L st x * a = 1. L
consider x being Element of L such that
A4: a * x = 1. L by A2;
x * a = 1. L by A1, A2, A3, A4, Lm11;
hence ex x being Element of L st x * a = 1. L ; ::_thesis: verum
end;
theorem Th11: :: ALGSTR_1:11
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
let L be non empty multLoopStr ; ::_thesis: ( 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) ) ) )
thus ( L is multGroup implies ( ( 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) ) ) ) by Def6, GROUP_1:def_3, VECTSP_1:def_6; ::_thesis: ( ( 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) ) implies L is multGroup )
assume that
A1: for a being Element of L holds a * (1. L) = a and
A2: for a being Element of L ex x being Element of L st a * x = 1. L and
A3: for a, b, c being Element of L holds (a * b) * c = a * (b * c) ; ::_thesis: L is multGroup
A4: for a, b being Element of L ex x being Element of L st x * a = b
proof
let a, b be Element of L; ::_thesis: ex x being Element of L st x * a = b
consider y being Element of L such that
A5: y * a = 1. L by A1, A2, A3, Lm13;
take x = b * y; ::_thesis: x * a = b
thus x * a = b * (1. L) by A3, A5
.= b by A1 ; ::_thesis: verum
end;
A6: for a being Element of L holds (1. L) * a = a
proof
let a be Element of L; ::_thesis: (1. L) * a = a
thus (1. L) * a = a * (1. L) by A1, A2, A3, Lm12
.= a by A1 ; ::_thesis: verum
end;
A7: L is left_mult-cancelable
proof
let a be Element of L; :: according to ALGSTR_0:def_23 ::_thesis: a is left_mult-cancelable
let x be Element of L; :: according to ALGSTR_0:def_20 ::_thesis: for b1 being Element of the carrier of L holds
( not a * x = a * b1 or x = b1 )
let y be Element of L; ::_thesis: ( not a * x = a * y or x = y )
consider z being Element of L such that
A8: z * a = 1. L by A1, A2, A3, Lm13;
assume a * x = a * y ; ::_thesis: x = y
then (z * a) * x = z * (a * y) by A3
.= (z * a) * y by A3 ;
hence x = (1. L) * y by A6, A8
.= y by A6 ;
::_thesis: verum
end;
A9: L is right_mult-cancelable
proof
let a be Element of L; :: according to ALGSTR_0:def_24 ::_thesis: a is right_mult-cancelable
let x be Element of L; :: according to ALGSTR_0:def_21 ::_thesis: for b1 being Element of the carrier of L holds
( not x * a = b1 * a or x = b1 )
let y be Element of L; ::_thesis: ( not x * a = y * a or x = y )
consider z being Element of L such that
A10: a * z = 1. L by A2;
assume x * a = y * a ; ::_thesis: x = y
then x * (a * z) = (y * a) * z by A3
.= y * (a * z) by A3 ;
hence x = y * (1. L) by A1, A10
.= y by A1 ;
::_thesis: verum
end;
for a, b being Element of L ex x being Element of L st a * x = b
proof
let a, b be Element of L; ::_thesis: ex x being Element of L st a * x = b
consider y being Element of L such that
A11: a * y = 1. L by A2;
take x = y * b; ::_thesis: a * x = b
thus a * x = (1. L) * b by A3, A11
.= b by A6 ; ::_thesis: verum
end;
hence L is multGroup by A1, A3, A6, A4, A7, A9, Def6, GROUP_1:def_3, VECTSP_1:def_6; ::_thesis: verum
end;
registration
cluster Trivial-multLoopStr -> associative ;
coherence
Trivial-multLoopStr is associative by Lm10, GROUP_1:def_3;
end;
Lm14: for a, b being Element of Trivial-multLoopStr holds a * b = b * a
by Th9;
registration
cluster non empty left_mult-cancelable right_mult-cancelable cancelable strict unital associative commutative right_unital well-unital left_unital invertible for multLoopStr ;
existence
ex b1 being multGroup st
( b1 is strict & b1 is commutative )
proof
Trivial-multLoopStr is commutative by Lm14, GROUP_1:def_12;
hence ex b1 being multGroup st
( b1 is strict & b1 is commutative ) ; ::_thesis: verum
end;
end;
theorem :: ALGSTR_1:12
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 Th11, GROUP_1:def_12;
notation
let L be non empty cancelable invertible multLoopStr ;
let x be Element of L;
synonym x " for / x;
end;
registration
let L be non empty cancelable invertible multLoopStr ;
cluster -> left_invertible for Element of the carrier of L;
coherence
for b1 being Element of L holds b1 is left_invertible
proof
let x be Element of L; ::_thesis: x is left_invertible
thus ex y being Element of L st y * x = 1. L by Def6; :: according to ALGSTR_0:def_27 ::_thesis: verum
end;
end;
theorem :: ALGSTR_1:13
for G being multGroup
for a being Element of G holds
( (a ") * a = 1. G & a * (a ") = 1. G )
proof
let G be multGroup; ::_thesis: for a being Element of G holds
( (a ") * a = 1. G & a * (a ") = 1. G )
let a be Element of G; ::_thesis: ( (a ") * a = 1. G & a * (a ") = 1. G )
thus A1: (a ") * a = 1. G by ALGSTR_0:def_30; ::_thesis: a * (a ") = 1. G
A2: for a, b, c being Element of G holds (a * b) * c = a * (b * c) by Th11;
( ( for a being Element of G holds a * (1. G) = a ) & ( for a being Element of G ex x being Element of G st a * x = 1. G ) ) by Th11;
hence a * (a ") = 1. G by A1, A2, Lm11; ::_thesis: verum
end;
definition
let L be non empty cancelable invertible multLoopStr ;
let a, b be Element of L;
funca / b -> Element of L equals :: ALGSTR_1:def 7
a * (b ");
correctness
coherence
a * (b ") is Element of L;
;
end;
:: deftheorem defines / ALGSTR_1:def_7_:_
for L being non empty cancelable invertible multLoopStr
for a, b being Element of L holds a / b = a * (b ");
definition
func multEX_0 -> strict multLoopStr_0 equals :: ALGSTR_1:def 8
multLoopStr_0(# REAL,multreal,0,1 #);
correctness
coherence
multLoopStr_0(# REAL,multreal,0,1 #) is strict multLoopStr_0 ;
;
end;
:: deftheorem defines multEX_0 ALGSTR_1:def_8_:_
multEX_0 = multLoopStr_0(# REAL,multreal,0,1 #);
registration
cluster multEX_0 -> non empty strict ;
coherence
not multEX_0 is empty ;
end;
Lm15: now__::_thesis:_for_x,_e_being_Element_of_multEX_0_st_e_=_1_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let x, e be Element of multEX_0; ::_thesis: ( e = 1 implies ( x * e = x & e * x = x ) )
reconsider a = x as Real ;
assume A1: e = 1 ; ::_thesis: ( x * e = x & e * x = x )
hence x * e = a * 1 by BINOP_2:def_11
.= x ;
::_thesis: e * x = x
thus e * x = 1 * a by A1, BINOP_2:def_11
.= x ; ::_thesis: verum
end;
registration
cluster multEX_0 -> strict well-unital ;
coherence
multEX_0 is well-unital
proof
let x be Element of multEX_0; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. multEX_0) = x & (1. multEX_0) * x = x )
thus ( x * (1. multEX_0) = x & (1. multEX_0) * x = x ) by Lm15; ::_thesis: verum
end;
end;
Lm16: 0 = 0. multEX_0
;
Lm17: 1 = 1_ multEX_0
;
theorem Th14: :: ALGSTR_1:14
for q, p being Real st q <> 0 holds
ex y being Real st p = q * y
proof
let q, p be Real; ::_thesis: ( q <> 0 implies ex y being Real st p = q * y )
reconsider y = p / q as Real ;
assume A1: q <> 0 ; ::_thesis: ex y being Real st p = q * y
take y ; ::_thesis: p = q * y
thus p = q * y by A1, XCMPLX_1:87; ::_thesis: verum
end;
theorem Th15: :: ALGSTR_1:15
for q, p being Real st q <> 0 holds
ex y being Real st p = y * q
proof
let q, p be Real; ::_thesis: ( q <> 0 implies ex y being Real st p = y * q )
reconsider y = p / q as Real ;
assume A1: q <> 0 ; ::_thesis: ex y being Real st p = y * q
take y ; ::_thesis: p = y * q
thus p = y * q by A1, XCMPLX_1:87; ::_thesis: verum
end;
Lm18: 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
let a, b be Element of multEX_0; ::_thesis: ( a <> 0. multEX_0 implies ex x being Element of multEX_0 st a * x = b )
assume A1: a <> 0. multEX_0 ; ::_thesis: ex x being Element of multEX_0 st a * x = b
reconsider p = a, q = b as Real ;
consider r being Real such that
A2: p * r = q by A1, Th14;
reconsider x = r as Element of multEX_0 ;
a * x = b by A2, BINOP_2:def_11;
hence ex x being Element of multEX_0 st a * x = b ; ::_thesis: verum
end;
Lm19: 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
let a, b be Element of multEX_0; ::_thesis: ( a <> 0. multEX_0 implies ex x being Element of multEX_0 st x * a = b )
assume A1: a <> 0. multEX_0 ; ::_thesis: ex x being Element of multEX_0 st x * a = b
reconsider p = a, q = b as Real ;
consider r being Real such that
A2: r * p = q by A1, Th15;
reconsider x = r as Element of multEX_0 ;
x * a = b by A2, BINOP_2:def_11;
hence ex x being Element of multEX_0 st x * a = b ; ::_thesis: verum
end;
Lm20: for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & a * x = a * y holds
x = y
proof
let a, x, y be Element of multEX_0; ::_thesis: ( a <> 0. multEX_0 & a * x = a * y implies x = y )
assume A1: a <> 0. multEX_0 ; ::_thesis: ( not a * x = a * y or x = y )
reconsider aa = a, p = x, q = y as Real ;
assume a * x = a * y ; ::_thesis: x = y
then aa * p = a * y by BINOP_2:def_11
.= aa * q by BINOP_2:def_11 ;
hence x = y by A1, XCMPLX_1:5; ::_thesis: verum
end;
Lm21: for a, x, y being Element of multEX_0 st a <> 0. multEX_0 & x * a = y * a holds
x = y
proof
let a, x, y be Element of multEX_0; ::_thesis: ( a <> 0. multEX_0 & x * a = y * a implies x = y )
assume A1: a <> 0. multEX_0 ; ::_thesis: ( not x * a = y * a or x = y )
reconsider aa = a, p = x, q = y as Real ;
assume x * a = y * a ; ::_thesis: x = y
then p * aa = y * a by BINOP_2:def_11
.= q * aa by BINOP_2:def_11 ;
hence x = y by A1, XCMPLX_1:5; ::_thesis: verum
end;
Lm22: for a being Element of multEX_0 holds a * (0. multEX_0) = 0. multEX_0
proof
let a be Element of multEX_0; ::_thesis: a * (0. multEX_0) = 0. multEX_0
reconsider aa = a as Real ;
thus a * (0. multEX_0) = aa * 0 by BINOP_2:def_11
.= 0. multEX_0 ; ::_thesis: verum
end;
Lm23: for a being Element of multEX_0 holds (0. multEX_0) * a = 0. multEX_0
proof
let a be Element of multEX_0; ::_thesis: (0. multEX_0) * a = 0. multEX_0
reconsider aa = a as Real ;
thus (0. multEX_0) * a = 0 * aa by BINOP_2:def_11
.= 0. multEX_0 ; ::_thesis: verum
end;
definition
let IT be non empty multLoopStr_0 ;
attrIT is almost_invertible means :Def9: :: ALGSTR_1:def 9
( ( 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 ) );
end;
:: deftheorem Def9 defines almost_invertible ALGSTR_1:def_9_:_
for IT being non empty multLoopStr_0 holds
( IT is almost_invertible iff ( ( 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 ) ) );
definition
let IT be non empty multLoopStr_0 ;
attrIT is multLoop_0-like means :Def10: :: ALGSTR_1:def 10
( 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 Def10 defines multLoop_0-like ALGSTR_1:def_10_:_
for IT being non empty multLoopStr_0 holds
( IT is multLoop_0-like iff ( 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 ) ) );
theorem Th16: :: ALGSTR_1:16
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
let L be non empty multLoopStr_0 ; ::_thesis: ( 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 ) ) )
hereby ::_thesis: ( ( 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 ) implies L is multLoop_0-like )
assume A1: L is multLoop_0-like ; ::_thesis: ( ( 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 ) )
then A2: ( L is almost_invertible & L is almost_cancelable ) by Def10;
hence ( ( 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 ) ) by Def9; ::_thesis: ( ( 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 ) )
thus for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ::_thesis: ( ( 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
let a, x, y be Element of L; ::_thesis: ( a <> 0. L & a * x = a * y implies x = y )
assume a <> 0. L ; ::_thesis: ( not a * x = a * y or x = y )
then a is left_mult-cancelable by A2, ALGSTR_0:def_36;
hence ( not a * x = a * y or x = y ) by ALGSTR_0:def_20; ::_thesis: verum
end;
thus for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ::_thesis: ( ( 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
let a, x, y be Element of L; ::_thesis: ( a <> 0. L & x * a = y * a implies x = y )
assume a <> 0. L ; ::_thesis: ( not x * a = y * a or x = y )
then a is right_mult-cancelable by A2, ALGSTR_0:def_37;
hence ( not x * a = y * a or x = y ) by ALGSTR_0:def_21; ::_thesis: verum
end;
thus ( ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) by A1, Def10; ::_thesis: verum
end;
assume that
A3: ( ( 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 ) ) and
A4: for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y and
A5: for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y and
A6: ( ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) ) ; ::_thesis: L is multLoop_0-like
A7: L is almost_right_cancelable
proof
let x be Element of L; :: according to ALGSTR_0:def_37 ::_thesis: ( x = 0. L or x is right_mult-cancelable )
assume A8: x <> 0. L ; ::_thesis: x is right_mult-cancelable
let y, z be Element of L; :: according to ALGSTR_0:def_21 ::_thesis: ( not y * x = z * x or y = z )
assume y * x = z * x ; ::_thesis: y = z
hence y = z by A5, A8; ::_thesis: verum
end;
L is almost_left_cancelable
proof
let x be Element of L; :: according to ALGSTR_0:def_36 ::_thesis: ( x = 0. L or x is left_mult-cancelable )
assume A9: x <> 0. L ; ::_thesis: x is left_mult-cancelable
let y, z be Element of L; :: according to ALGSTR_0:def_20 ::_thesis: ( not x * y = x * z or y = z )
assume x * y = x * z ; ::_thesis: y = z
hence y = z by A4, A9; ::_thesis: verum
end;
then ( L is almost_invertible & L is almost_cancelable ) by A3, A7, Def9;
hence L is multLoop_0-like by A6, Def10; ::_thesis: verum
end;
registration
cluster non empty multLoop_0-like -> non empty almost_cancelable almost_invertible for multLoopStr_0 ;
coherence
for b1 being non empty multLoopStr_0 st b1 is multLoop_0-like holds
( b1 is almost_invertible & b1 is almost_cancelable ) by Def10;
end;
registration
cluster non empty non degenerated strict well-unital multLoop_0-like for multLoopStr_0 ;
existence
ex b1 being non empty multLoopStr_0 st
( b1 is strict & b1 is well-unital & b1 is multLoop_0-like & not b1 is degenerated )
proof
( multEX_0 is well-unital & multEX_0 is multLoop_0-like & not multEX_0 is degenerated ) by Lm17, Lm18, Lm19, Lm20, Lm21, Lm22, Lm23, Th16, STRUCT_0:def_8;
hence ex b1 being non empty multLoopStr_0 st
( b1 is strict & b1 is well-unital & b1 is multLoop_0-like & not b1 is degenerated ) ; ::_thesis: verum
end;
end;
definition
mode multLoop_0 is non empty non degenerated well-unital multLoop_0-like multLoopStr_0 ;
end;
registration
cluster multEX_0 -> strict well-unital multLoop_0-like ;
coherence
( multEX_0 is well-unital & multEX_0 is multLoop_0-like ) by Lm18, Lm19, Lm20, Lm21, Lm22, Lm23, Th16;
end;
Lm24: for a, b, c being Element of multEX_0 holds (a * b) * c = a * (b * c)
proof
let a, b, c be Element of multEX_0; ::_thesis: (a * b) * c = a * (b * c)
reconsider p = a, q = b, r = c as Real ;
A1: b * c = q * r by BINOP_2:def_11;
a * b = p * q by BINOP_2:def_11;
hence (a * b) * c = (p * q) * r by BINOP_2:def_11
.= p * (q * r)
.= a * (b * c) by A1, BINOP_2:def_11 ;
::_thesis: verum
end;
registration
cluster non empty non degenerated non trivial strict almost_left_cancelable almost_right_cancelable almost_cancelable unital associative right_unital well-unital left_unital almost_invertible multLoop_0-like for multLoopStr_0 ;
existence
ex b1 being multLoop_0 st
( b1 is strict & b1 is associative & not b1 is degenerated )
proof
( multEX_0 is associative & not multEX_0 is degenerated ) by Lm16, Lm17, Lm24, GROUP_1:def_3, STRUCT_0:def_8;
hence ex b1 being multLoop_0 st
( b1 is strict & b1 is associative & not b1 is degenerated ) ; ::_thesis: verum
end;
end;
definition
mode multGroup_0 is associative multLoop_0;
end;
registration
cluster multEX_0 -> strict associative ;
coherence
multEX_0 is associative by Lm24, GROUP_1:def_3;
end;
Lm25: for a, b being Element of multEX_0 holds a * b = b * a
proof
let a, b be Element of multEX_0; ::_thesis: a * b = b * a
reconsider p = a, q = b as Real ;
thus a * b = q * p by BINOP_2:def_11
.= b * a by BINOP_2:def_11 ; ::_thesis: verum
end;
registration
cluster non empty non degenerated non trivial strict almost_left_cancelable almost_right_cancelable almost_cancelable unital associative commutative right_unital well-unital left_unital almost_invertible multLoop_0-like for multLoopStr_0 ;
existence
ex b1 being multGroup_0 st
( b1 is strict & b1 is commutative )
proof
( multEX_0 is commutative & not multEX_0 is degenerated ) by Lm16, Lm17, Lm25, GROUP_1:def_12, STRUCT_0:def_8;
hence ex b1 being multGroup_0 st
( b1 is strict & b1 is commutative ) ; ::_thesis: verum
end;
end;
definition
let L be non empty almost_cancelable almost_invertible multLoopStr_0 ;
let x be Element of L;
assume A1: x <> 0. L ;
redefine func x " means :Def11: :: ALGSTR_1:def 11
it * x = 1. L;
compatibility
for b1 being Element of the carrier of L holds
( b1 = x " iff b1 * x = 1. L )
proof
let IT be Element of L; ::_thesis: ( IT = x " iff IT * x = 1. L )
ex x1 being Element of L st x1 * x = 1. L by A1, Def9;
then A2: x is left_invertible by ALGSTR_0:def_27;
x is right_mult-cancelable by A1, ALGSTR_0:def_37;
hence ( IT = x " iff IT * x = 1. L ) by A2, ALGSTR_0:def_35; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines " ALGSTR_1:def_11_:_
for L being non empty almost_cancelable almost_invertible multLoopStr_0
for x being Element of L st x <> 0. L holds
for b3 being Element of the carrier of L holds
( b3 = x " iff b3 * x = 1. L );
theorem :: ALGSTR_1:17
for G being non empty almost_cancelable associative well-unital almost_invertible multLoopStr_0
for a being Element of G st a <> 0. G holds
( (a ") * a = 1. G & a * (a ") = 1. G )
proof
let G be non empty almost_cancelable associative well-unital almost_invertible multLoopStr_0 ; ::_thesis: for a being Element of G st a <> 0. G holds
( (a ") * a = 1. G & a * (a ") = 1. G )
let a be Element of G; ::_thesis: ( a <> 0. G implies ( (a ") * a = 1. G & a * (a ") = 1. G ) )
assume A1: a <> 0. G ; ::_thesis: ( (a ") * a = 1. G & a * (a ") = 1. G )
hence A2: (a ") * a = 1. G by Def11; ::_thesis: a * (a ") = 1. G
consider x being Element of G such that
A3: a * x = 1. G by A1, Def9;
((a ") * a) * x = (a ") * (1. G) by A3, GROUP_1:def_3;
then x = (a ") * (1. G) by A2, VECTSP_1:def_8;
hence a * (a ") = 1. G by A3, VECTSP_1:def_4; ::_thesis: verum
end;
definition
let L be non empty almost_cancelable almost_invertible multLoopStr_0 ;
let a, b be Element of L;
funca / b -> Element of L equals :: ALGSTR_1:def 12
a * (b ");
correctness
coherence
a * (b ") is Element of L;
;
end;
:: deftheorem defines / ALGSTR_1:def_12_:_
for L being non empty almost_cancelable almost_invertible multLoopStr_0
for a, b being Element of L holds a / b = a * (b ");
registration
cluster1 -element -> 1 -element right_complementable Abelian add-associative right_zeroed for addLoopStr ;
coherence
for b1 being 1 -element addLoopStr holds
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable )
proof
let S be 1 -element addLoopStr ; ::_thesis: ( S is Abelian & S is add-associative & S is right_zeroed & S is right_complementable )
thus ( ( for v, w being Element of S holds v + w = w + v ) & ( for u, v, w being Element of S holds (u + v) + w = u + (v + w) ) & ( for v being Element of S holds v + (0. S) = v ) ) by STRUCT_0:def_10; :: according to RLVECT_1:def_2,RLVECT_1:def_3,RLVECT_1:def_4 ::_thesis: S is right_complementable
let v be Element of S; :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
take v ; :: according to ALGSTR_0:def_11 ::_thesis: v + v = 0. S
thus v + v = 0. S by STRUCT_0:def_10; ::_thesis: verum
end;
cluster non empty trivial -> non empty right-distributive well-unital for doubleLoopStr ;
coherence
for b1 being non empty doubleLoopStr st b1 is trivial holds
( b1 is well-unital & b1 is right-distributive )
proof
let S be non empty doubleLoopStr ; ::_thesis: ( S is trivial implies ( S is well-unital & S is right-distributive ) )
assume A1: S is trivial ; ::_thesis: ( S is well-unital & S is right-distributive )
thus for x being Element of S holds
( x * (1. S) = x & (1. S) * x = x ) by A1, STRUCT_0:def_10; :: according to VECTSP_1:def_6 ::_thesis: S is right-distributive
let x, y, z be Element of S; :: according to VECTSP_1:def_2 ::_thesis: x * (y + z) = (x * y) + (x * z)
thus x * (y + z) = (x * y) + (x * z) by A1, STRUCT_0:def_10; ::_thesis: verum
end;
end;
registration
cluster1 -element -> 1 -element Group-like associative commutative for multMagma ;
coherence
for b1 being 1 -element multMagma holds
( b1 is Group-like & b1 is associative & b1 is commutative )
proof
let H be 1 -element multMagma ; ::_thesis: ( H is Group-like & H is associative & H is commutative )
hereby :: according to GROUP_1:def_2 ::_thesis: ( H is associative & H is commutative )
set e = the Element of H;
take e = the Element of H; ::_thesis: for h being Element of H holds
( h * e = h & e * h = h & ex g being Element of H st
( h * g = e & g * h = e ) )
let h be Element of H; ::_thesis: ( h * e = h & e * h = h & ex g being Element of H st
( h * g = e & g * h = e ) )
thus ( h * e = h & e * h = h ) by STRUCT_0:def_10; ::_thesis: ex g being Element of H st
( h * g = e & g * h = e )
take g = e; ::_thesis: ( h * g = e & g * h = e )
thus ( h * g = e & g * h = e ) by STRUCT_0:def_10; ::_thesis: verum
end;
thus for x, y, z being Element of H holds (x * y) * z = x * (y * z) by STRUCT_0:def_10; :: according to GROUP_1:def_3 ::_thesis: H is commutative
let x, y be Element of H; :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
thus x * y = y * x by STRUCT_0:def_10; ::_thesis: verum
end;
end;