:: by Wojciech A. Trybulec

::

:: Received July 3, 1990

:: Copyright (c) 1990-2019 Association of Mizar Users

Lm1: now :: thesis: ( ( for h, g, f being Element of multMagma(# REAL,addreal #) holds (h * g) * f = h * (g * f) ) & ex e being Element of multMagma(# REAL,addreal #) st

for h being Element of multMagma(# REAL,addreal #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e ) ) )

for h being Element of multMagma(# REAL,addreal #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e ) ) )

set G = multMagma(# REAL,addreal #);

thus for h, g, f being Element of multMagma(# REAL,addreal #) holds (h * g) * f = h * (g * f) :: thesis: ex e being Element of multMagma(# REAL,addreal #) st

for h being Element of multMagma(# REAL,addreal #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e ) )

take e = e; :: thesis: for h being Element of multMagma(# REAL,addreal #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e ) )

let h be Element of multMagma(# REAL,addreal #); :: thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e ) )

reconsider A = h as Real ;

thus h * e = A + 0 by BINOP_2:def 9

.= h ; :: thesis: ( e * h = h & ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e ) )

thus e * h = 0 + A by BINOP_2:def 9

.= h ; :: thesis: ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e )

reconsider g = - A as Element of multMagma(# REAL,addreal #) by XREAL_0:def 1;

take g = g; :: thesis: ( h * g = e & g * h = e )

thus h * g = A + (- A) by BINOP_2:def 9

.= e ; :: thesis: g * h = e

thus g * h = (- A) + A by BINOP_2:def 9

.= e ; :: thesis: verum

end;
thus for h, g, f being Element of multMagma(# REAL,addreal #) holds (h * g) * f = h * (g * f) :: thesis: ex e being Element of multMagma(# REAL,addreal #) st

for h being Element of multMagma(# REAL,addreal #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e ) )

proof

reconsider e = 0 as Element of multMagma(# REAL,addreal #) by XREAL_0:def 1;
let h, g, f be Element of multMagma(# REAL,addreal #); :: thesis: (h * g) * f = h * (g * f)

reconsider A = h, B = g, C = f as Real ;

A1: g * f = B + C by BINOP_2:def 9;

h * g = A + B by BINOP_2:def 9;

hence (h * g) * f = (A + B) + C by BINOP_2:def 9

.= A + (B + C)

.= h * (g * f) by A1, BINOP_2:def 9 ;

:: thesis: verum

end;
reconsider A = h, B = g, C = f as Real ;

A1: g * f = B + C by BINOP_2:def 9;

h * g = A + B by BINOP_2:def 9;

hence (h * g) * f = (A + B) + C by BINOP_2:def 9

.= A + (B + C)

.= h * (g * f) by A1, BINOP_2:def 9 ;

:: thesis: verum

take e = e; :: thesis: for h being Element of multMagma(# REAL,addreal #) holds

( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e ) )

let h be Element of multMagma(# REAL,addreal #); :: thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e ) )

reconsider A = h as Real ;

thus h * e = A + 0 by BINOP_2:def 9

.= h ; :: thesis: ( e * h = h & ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e ) )

thus e * h = 0 + A by BINOP_2:def 9

.= h ; :: thesis: ex g being Element of multMagma(# REAL,addreal #) st

( h * g = e & g * h = e )

reconsider g = - A as Element of multMagma(# REAL,addreal #) by XREAL_0:def 1;

take g = g; :: thesis: ( h * g = e & g * h = e )

thus h * g = A + (- A) by BINOP_2:def 9

.= e ; :: thesis: g * h = e

thus g * h = (- A) + A by BINOP_2:def 9

.= e ; :: thesis: verum

definition

let IT be multMagma ;

end;
attr IT is unital means :: GROUP_1:def 1

ex e being Element of IT st

for h being Element of IT holds

( h * e = h & e * h = h );

ex e being Element of IT st

for h being Element of IT holds

( h * e = h & e * h = h );

attr IT is Group-like means :Def2: :: GROUP_1:def 2

ex e being Element of IT st

for h being Element of IT holds

( h * e = h & e * h = h & ex g being Element of IT st

( h * g = e & g * h = e ) );

ex e being Element of IT st

for h being Element of IT holds

( h * e = h & e * h = h & ex g being Element of IT st

( h * g = e & g * h = e ) );

attr IT is associative means :Def3: :: GROUP_1:def 3

for x, y, z being Element of IT holds (x * y) * z = x * (y * z);

for x, y, z being Element of IT holds (x * y) * z = x * (y * z);

:: deftheorem defines unital GROUP_1:def 1 :

for IT being multMagma holds

( IT is unital iff ex e being Element of IT st

for h being Element of IT holds

( h * e = h & e * h = h ) );

for IT being multMagma holds

( IT is unital iff ex e being Element of IT st

for h being Element of IT holds

( h * e = h & e * h = h ) );

:: deftheorem Def2 defines Group-like GROUP_1:def 2 :

for IT being multMagma holds

( IT is Group-like iff ex e being Element of IT st

for h being Element of IT holds

( h * e = h & e * h = h & ex g being Element of IT st

( h * g = e & g * h = e ) ) );

for IT being multMagma holds

( IT is Group-like iff ex e being Element of IT st

for h being Element of IT holds

( h * e = h & e * h = h & ex g being Element of IT st

( h * g = e & g * h = e ) ) );

:: deftheorem Def3 defines associative GROUP_1:def 3 :

for IT being multMagma holds

( IT is associative iff for x, y, z being Element of IT holds (x * y) * z = x * (y * z) );

for IT being multMagma holds

( IT is associative iff for x, y, z being Element of IT holds (x * y) * z = x * (y * z) );

registration
end;

registration

existence

ex b_{1} being multMagma st

( b_{1} is strict & b_{1} is Group-like & b_{1} is associative & not b_{1} is empty )

end;
ex b

( b

proof end;

theorem :: GROUP_1:1

theorem :: GROUP_1:2

for S being non empty multMagma st ( for r, s, t being Element of S holds (r * s) * t = r * (s * t) ) & ( for r, s being Element of S holds

( ex t being Element of S st r * t = s & ex t being Element of S st t * r = s ) ) holds

( S is associative & S is Group-like )

( ex t being Element of S st r * t = s & ex t being Element of S st t * r = s ) ) holds

( S is associative & S is Group-like )

proof end;

definition

let G be multMagma ;

assume A1: G is unital ;

ex b_{1} being Element of G st

for h being Element of G holds

( h * b_{1} = h & b_{1} * h = h )
by A1;

uniqueness

for b_{1}, b_{2} being Element of G st ( for h being Element of G holds

( h * b_{1} = h & b_{1} * h = h ) ) & ( for h being Element of G holds

( h * b_{2} = h & b_{2} * h = h ) ) holds

b_{1} = b_{2}

end;
assume A1: G is unital ;

func 1_ G -> Element of G means :Def4: :: GROUP_1:def 4

for h being Element of G holds

( h * it = h & it * h = h );

existence for h being Element of G holds

( h * it = h & it * h = h );

ex b

for h being Element of G holds

( h * b

uniqueness

for b

( h * b

( h * b

b

proof end;

:: deftheorem Def4 defines 1_ GROUP_1:def 4 :

for G being multMagma st G is unital holds

for b_{2} being Element of G holds

( b_{2} = 1_ G iff for h being Element of G holds

( h * b_{2} = h & b_{2} * h = h ) );

for G being multMagma st G is unital holds

for b

( b

( h * b

theorem :: GROUP_1:4

definition

let G be Group;

let h be Element of G;

existence

ex b_{1} being Element of G st

( h * b_{1} = 1_ G & b_{1} * h = 1_ G )

for b_{1}, b_{2} being Element of G st h * b_{1} = 1_ G & b_{1} * h = 1_ G & h * b_{2} = 1_ G & b_{2} * h = 1_ G holds

b_{1} = b_{2}

for b_{1}, b_{2} being Element of G st b_{2} * b_{1} = 1_ G & b_{1} * b_{2} = 1_ G holds

( b_{1} * b_{2} = 1_ G & b_{2} * b_{1} = 1_ G )
;

end;
let h be Element of G;

existence

ex b

( h * b

proof end;

uniqueness for b

b

proof end;

involutiveness for b

( b

:: deftheorem Def5 defines " GROUP_1:def 5 :

for G being Group

for h, b_{3} being Element of G holds

( b_{3} = h " iff ( h * b_{3} = 1_ G & b_{3} * h = 1_ G ) );

for G being Group

for h, b

( b

theorem :: GROUP_1:5

::$CT

theorem Th18: :: GROUP_1:19

for G being Group

for g, h being Element of G holds

( g * h = h * g iff (g ") * (h ") = (h ") * (g ") )

for g, h being Element of G holds

( g * h = h * g iff (g ") * (h ") = (h ") * (g ") )

proof end;

definition

let G be Group;

ex b_{1} being UnOp of G st

for h being Element of G holds b_{1} . h = h "

for b_{1}, b_{2} being UnOp of G st ( for h being Element of G holds b_{1} . h = h " ) & ( for h being Element of G holds b_{2} . h = h " ) holds

b_{1} = b_{2}

end;
func inverse_op G -> UnOp of G means :Def6: :: GROUP_1:def 6

for h being Element of G holds it . h = h " ;

existence for h being Element of G holds it . h = h " ;

ex b

for h being Element of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines inverse_op GROUP_1:def 6 :

for G being Group

for b_{2} being UnOp of G holds

( b_{2} = inverse_op G iff for h being Element of G holds b_{2} . h = h " );

for G being Group

for b

( b

registration
end;

registration
end;

definition

let G be non empty multMagma ;

ex b_{1} being Function of [: the carrier of G,NAT:], the carrier of G st

for h being Element of G holds

( b_{1} . (h,0) = 1_ G & ( for n being Nat holds b_{1} . (h,(n + 1)) = (b_{1} . (h,n)) * h ) )

for b_{1}, b_{2} being Function of [: the carrier of G,NAT:], the carrier of G st ( for h being Element of G holds

( b_{1} . (h,0) = 1_ G & ( for n being Nat holds b_{1} . (h,(n + 1)) = (b_{1} . (h,n)) * h ) ) ) & ( for h being Element of G holds

( b_{2} . (h,0) = 1_ G & ( for n being Nat holds b_{2} . (h,(n + 1)) = (b_{2} . (h,n)) * h ) ) ) holds

b_{1} = b_{2}

end;
func power G -> Function of [: the carrier of G,NAT:], the carrier of G means :Def7: :: GROUP_1:def 7

for h being Element of G holds

( it . (h,0) = 1_ G & ( for n being Nat holds it . (h,(n + 1)) = (it . (h,n)) * h ) );

existence for h being Element of G holds

( it . (h,0) = 1_ G & ( for n being Nat holds it . (h,(n + 1)) = (it . (h,n)) * h ) );

ex b

for h being Element of G holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def7 defines power GROUP_1:def 7 :

for G being non empty multMagma

for b_{2} being Function of [: the carrier of G,NAT:], the carrier of G holds

( b_{2} = power G iff for h being Element of G holds

( b_{2} . (h,0) = 1_ G & ( for n being Nat holds b_{2} . (h,(n + 1)) = (b_{2} . (h,n)) * h ) ) );

for G being non empty multMagma

for b

( b

( b

definition

let G be Group;

let h be Element of G;

let i be Integer;

coherence

( ( 0 <= i implies (power G) . (h,|.i.|) is Element of G ) & ( not 0 <= i implies ((power G) . (h,|.i.|)) " is Element of G ) );

consistency

for b_{1} being Element of G holds verum;

;

end;
let h be Element of G;

let i be Integer;

func h |^ i -> Element of G equals :Def8: :: GROUP_1:def 8

(power G) . (h,|.i.|) if 0 <= i

otherwise ((power G) . (h,|.i.|)) " ;

correctness (power G) . (h,|.i.|) if 0 <= i

otherwise ((power G) . (h,|.i.|)) " ;

coherence

( ( 0 <= i implies (power G) . (h,|.i.|) is Element of G ) & ( not 0 <= i implies ((power G) . (h,|.i.|)) " is Element of G ) );

consistency

for b

;

:: deftheorem Def8 defines |^ GROUP_1:def 8 :

for G being Group

for h being Element of G

for i being Integer holds

( ( 0 <= i implies h |^ i = (power G) . (h,|.i.|) ) & ( not 0 <= i implies h |^ i = ((power G) . (h,|.i.|)) " ) );

for G being Group

for h being Element of G

for i being Integer holds

( ( 0 <= i implies h |^ i = (power G) . (h,|.i.|) ) & ( not 0 <= i implies h |^ i = ((power G) . (h,|.i.|)) " ) );

definition

let G be Group;

let h be Element of G;

let n be natural Number ;

compatibility

for b_{1} being Element of G holds

( b_{1} = h |^ n iff b_{1} = (power G) . (h,n) )

end;
let h be Element of G;

let n be natural Number ;

compatibility

for b

( b

proof end;

:: deftheorem defines |^ GROUP_1:def 9 :

for G being Group

for h being Element of G

for n being natural Number holds h |^ n = (power G) . (h,n);

for G being Group

for h being Element of G

for n being natural Number holds h |^ n = (power G) . (h,n);

Lm2: for n being Nat

for G being Group

for h being Element of G holds h |^ (n + 1) = (h |^ n) * h

by Def7;

Lm3: for G being Group

for h being Element of G holds h |^ 0 = 1_ G

by Def7;

Lm4: for n being Nat

for G being Group holds (1_ G) |^ n = 1_ G

proof end;

Lm5: for m, n being Nat

for G being Group

for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m)

proof end;

Lm6: for n being Nat

for G being Group

for h being Element of G holds

( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )

proof end;

Lm7: for m, n being Nat

for G being Group

for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m

proof end;

Lm8: for n being Nat

for G being Group

for h being Element of G holds (h ") |^ n = (h |^ n) "

proof end;

Lm9: for n being Nat

for G being Group

for g, h being Element of G st g * h = h * g holds

g * (h |^ n) = (h |^ n) * g

proof end;

Lm10: for m, n being Nat

for G being Group

for g, h being Element of G st g * h = h * g holds

(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n)

proof end;

Lm11: for n being Nat

for G being Group

for g, h being Element of G st g * h = h * g holds

(g * h) |^ n = (g |^ n) * (h |^ n)

proof end;

theorem Th29: :: GROUP_1:30

for i being Integer

for G being Group

for h being Element of G st i <= 0 holds

h |^ i = (h |^ |.i.|) "

for G being Group

for h being Element of G st i <= 0 holds

h |^ i = (h |^ |.i.|) "

proof end;

Lm12: for i being Integer

for G being Group

for h being Element of G holds h |^ (- i) = (h |^ i) "

proof end;

Lm13: for j being Integer holds

( j >= 1 or j = 0 or j < 0 )

proof end;

Lm14: for j being Integer

for G being Group

for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))

proof end;

Lm15: for j being Integer holds

( j >= 0 or j = - 1 or j < - 1 )

proof end;

Lm16: for j being Integer

for G being Group

for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)

proof end;

theorem Th32: :: GROUP_1:33

for i, j being Integer

for G being Group

for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)

for G being Group

for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)

proof end;

theorem :: GROUP_1:34

for i being Integer

for G being Group

for h being Element of G holds

( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )

for G being Group

for h being Element of G holds

( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )

proof end;

Lm17: for i being Integer

for G being Group

for h being Element of G holds (h ") |^ i = (h |^ i) "

proof end;

theorem :: GROUP_1:35

for i, j being Integer

for G being Group

for h being Element of G holds h |^ (i * j) = (h |^ i) |^ j

for G being Group

for h being Element of G holds h |^ (i * j) = (h |^ i) |^ j

proof end;

theorem :: GROUP_1:36

theorem :: GROUP_1:37

theorem Th37: :: GROUP_1:38

for i being Integer

for G being Group

for g, h being Element of G st g * h = h * g holds

(g * h) |^ i = (g |^ i) * (h |^ i)

for G being Group

for g, h being Element of G st g * h = h * g holds

(g * h) |^ i = (g |^ i) * (h |^ i)

proof end;

theorem Th38: :: GROUP_1:39

for i, j being Integer

for G being Group

for g, h being Element of G st g * h = h * g holds

(g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)

for G being Group

for g, h being Element of G st g * h = h * g holds

(g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)

proof end;

theorem :: GROUP_1:40

for i being Integer

for G being Group

for g, h being Element of G st g * h = h * g holds

g * (h |^ i) = (h |^ i) * g

for G being Group

for g, h being Element of G st g * h = h * g holds

g * (h |^ i) = (h |^ i) * g

proof end;

:: deftheorem defines being_of_order_0 GROUP_1:def 10 :

for G being Group

for h being Element of G holds

( h is being_of_order_0 iff for n being Nat st h |^ n = 1_ G holds

n = 0 );

for G being Group

for h being Element of G holds

( h is being_of_order_0 iff for n being Nat st h |^ n = 1_ G holds

n = 0 );

definition

let G be Group;

let h be Element of G;

( ( h is being_of_order_0 implies ex b_{1} being Element of NAT st b_{1} = 0 ) & ( not h is being_of_order_0 implies ex b_{1} being Element of NAT st

( h |^ b_{1} = 1_ G & b_{1} <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds

b_{1} <= m ) ) ) )

for b_{1}, b_{2} being Element of NAT holds

( ( h is being_of_order_0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) & ( not h is being_of_order_0 & h |^ b_{1} = 1_ G & b_{1} <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds

b_{1} <= m ) & h |^ b_{2} = 1_ G & b_{2} <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds

b_{2} <= m ) implies b_{1} = b_{2} ) )

consistency

for b_{1} being Element of NAT holds verum;

;

end;
let h be Element of G;

func ord h -> Element of NAT means :Def11: :: GROUP_1:def 11

it = 0 if h is being_of_order_0

otherwise ( h |^ it = 1_ G & it <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds

it <= m ) );

existence it = 0 if h is being_of_order_0

otherwise ( h |^ it = 1_ G & it <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds

it <= m ) );

( ( h is being_of_order_0 implies ex b

( h |^ b

b

proof end;

uniqueness for b

( ( h is being_of_order_0 & b

b

b

proof end;

correctness consistency

for b

;

:: deftheorem Def11 defines ord GROUP_1:def 11 :

for G being Group

for h being Element of G

for b_{3} being Element of NAT holds

( ( h is being_of_order_0 implies ( b_{3} = ord h iff b_{3} = 0 ) ) & ( not h is being_of_order_0 implies ( b_{3} = ord h iff ( h |^ b_{3} = 1_ G & b_{3} <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds

b_{3} <= m ) ) ) ) );

for G being Group

for h being Element of G

for b

( ( h is being_of_order_0 implies ( b

b

definition

let G be finite 1-sorted ;

:: original: card

redefine func card G -> Element of NAT ;

coherence

card G is Element of NAT

end;
:: original: card

redefine func card G -> Element of NAT ;

coherence

card G is Element of NAT

proof end;

definition

let IT be multMagma ;

end;
attr IT is commutative means :Def12: :: GROUP_1:def 12

for x, y being Element of IT holds x * y = y * x;

for x, y being Element of IT holds x * y = y * x;

:: deftheorem Def12 defines commutative GROUP_1:def 12 :

for IT being multMagma holds

( IT is commutative iff for x, y being Element of IT holds x * y = y * x );

for IT being multMagma holds

( IT is commutative iff for x, y being Element of IT holds x * y = y * x );

registration
end;

definition

let FS be non empty commutative multMagma ;

let x, y be Element of FS;

:: original: *

redefine func x * y -> Element of the carrier of FS;

commutativity

for x, y being Element of FS holds x * y = y * x by Def12;

end;
let x, y be Element of FS;

:: original: *

redefine func x * y -> Element of the carrier of FS;

commutativity

for x, y being Element of FS holds x * y = y * x by Def12;

theorem :: GROUP_1:47

theorem :: GROUP_1:48

theorem :: GROUP_1:49

for A being commutative Group holds

( addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is Abelian & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is add-associative & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_complementable )

( addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is Abelian & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is add-associative & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_complementable )

proof end;

:: from COMPTRIG, 2006.08.12, A.T.

theorem :: GROUP_1:52

for L being non empty unital associative commutative multMagma

for x, y being Element of L

for n being Nat holds (power L) . ((x * y),n) = ((power L) . (x,n)) * ((power L) . (y,n))

for x, y being Element of L

for n being Nat holds (power L) . ((x * y),n) = ((power L) . (x,n)) * ((power L) . (y,n))

proof end;

:: Moved from ENDALG, 17.01_2006, AK

:: deftheorem defines unity-preserving GROUP_1:def 13 :

for G, H being multMagma

for IT being Function of G,H holds

( IT is unity-preserving iff IT . (1_ G) = 1_ H );

for G, H being multMagma

for IT being Function of G,H holds

( IT is unity-preserving iff IT . (1_ G) = 1_ H );