:: Groups :: by Wojciech A. Trybulec :: :: Received July 3, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin 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_)_)_) 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 ) ) proof 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 e = 0 as Element of multMagma(# REAL,addreal #) ; 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 #) ; 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; definition let IT be multMagma ; attrIT is unital means :Def1: :: GROUP_1:def 1 ex e being Element of IT st for h being Element of IT holds ( h * e = h & e * h = h ); attrIT 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 ) ); attrIT is associative means :Def3: :: GROUP_1:def 3 for x, y, z being Element of IT holds (x * y) * z = x * (y * z); end; :: deftheorem Def1 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 ) ); :: 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 ) ) ); :: 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) ); registration cluster Group-like -> unital for multMagma ; coherence for b1 being multMagma st b1 is Group-like holds b1 is unital proofend; end; registration cluster non empty strict Group-like associative for multMagma ; existence ex b1 being multMagma st ( b1 is strict & b1 is Group-like & b1 is associative & not b1 is empty ) proofend; end; definition mode Group is non empty Group-like associative multMagma ; end; theorem :: GROUP_1:1 for S being non empty multMagma st ( for r, s, t being Element of S holds (r * s) * t = r * (s * t) ) & ex t being Element of S st for s1 being Element of S holds ( s1 * t = s1 & t * s1 = s1 & ex s2 being Element of S st ( s1 * s2 = t & s2 * s1 = t ) ) holds S is Group by Def2, Def3; 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 ) proofend; theorem Th3: :: GROUP_1:3 ( multMagma(# REAL,addreal #) is associative & multMagma(# REAL,addreal #) is Group-like ) proofend; definition let G be multMagma ; 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 ex b1 being Element of G st for h being Element of G holds ( h * b1 = h & b1 * h = h ) by A1, Def1; uniqueness for b1, b2 being Element of G st ( for h being Element of G holds ( h * b1 = h & b1 * h = h ) ) & ( for h being Element of G holds ( h * b2 = h & b2 * h = h ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines 1_ GROUP_1:def_4_:_ for G being multMagma st G is unital holds for b2 being Element of G holds ( b2 = 1_ G iff for h being Element of G holds ( h * b2 = h & b2 * h = h ) ); theorem :: GROUP_1:4 for G being non empty Group-like multMagma for e being Element of G st ( for h being Element of G holds ( h * e = h & e * h = h ) ) holds e = 1_ G by Def4; definition let G be Group; let h be Element of G; funch " -> Element of G means :Def5: :: GROUP_1:def 5 ( h * it = 1_ G & it * h = 1_ G ); existence ex b1 being Element of G st ( h * b1 = 1_ G & b1 * h = 1_ G ) proofend; uniqueness for b1, b2 being Element of G st h * b1 = 1_ G & b1 * h = 1_ G & h * b2 = 1_ G & b2 * h = 1_ G holds b1 = b2 proofend; involutiveness for b1, b2 being Element of G st b2 * b1 = 1_ G & b1 * b2 = 1_ G holds ( b1 * b2 = 1_ G & b2 * b1 = 1_ G ) ; end; :: deftheorem Def5 defines " GROUP_1:def_5_:_ for G being Group for h, b3 being Element of G holds ( b3 = h " iff ( h * b3 = 1_ G & b3 * h = 1_ G ) ); theorem :: GROUP_1:5 for G being Group for h, g being Element of G st h * g = 1_ G & g * h = 1_ G holds g = h " by Def5; theorem Th6: :: GROUP_1:6 for G being Group for h, g, f being Element of G st ( h * g = h * f or g * h = f * h ) holds g = f proofend; theorem :: GROUP_1:7 for G being Group for h, g being Element of G st ( h * g = h or g * h = h ) holds g = 1_ G proofend; theorem Th8: :: GROUP_1:8 for G being Group holds (1_ G) " = 1_ G proofend; theorem :: GROUP_1:9 for G being Group for h, g being Element of G st h " = g " holds h = g proofend; theorem :: GROUP_1:10 for G being Group for h being Element of G st h " = 1_ G holds h = 1_ G proofend; theorem :: GROUP_1:11 canceled; theorem Th12: :: GROUP_1:12 for G being Group for h, g being Element of G st h * g = 1_ G holds ( h = g " & g = h " ) proofend; theorem Th13: :: GROUP_1:13 for G being Group for h, f, g being Element of G holds ( h * f = g iff f = (h ") * g ) proofend; theorem Th14: :: GROUP_1:14 for G being Group for f, h, g being Element of G holds ( f * h = g iff f = g * (h ") ) proofend; theorem :: GROUP_1:15 for G being Group for g, h being Element of G ex f being Element of G st g * f = h proofend; theorem :: GROUP_1:16 for G being Group for g, h being Element of G ex f being Element of G st f * g = h proofend; theorem Th17: :: GROUP_1:17 for G being Group for h, g being Element of G holds (h * g) " = (g ") * (h ") proofend; theorem Th18: :: GROUP_1:18 for G being Group for g, h being Element of G holds ( g * h = h * g iff (g * h) " = (g ") * (h ") ) proofend; theorem Th19: :: GROUP_1:19 for G being Group for g, h being Element of G holds ( g * h = h * g iff (g ") * (h ") = (h ") * (g ") ) proofend; theorem Th20: :: GROUP_1:20 for G being Group for g, h being Element of G holds ( g * h = h * g iff g * (h ") = (h ") * g ) proofend; definition let G be Group; func inverse_op G -> UnOp of G means :Def6: :: GROUP_1:def 6 for h being Element of G holds it . h = h " ; existence ex b1 being UnOp of G st for h being Element of G holds b1 . h = h " proofend; uniqueness for b1, b2 being UnOp of G st ( for h being Element of G holds b1 . h = h " ) & ( for h being Element of G holds b2 . h = h " ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines inverse_op GROUP_1:def_6_:_ for G being Group for b2 being UnOp of G holds ( b2 = inverse_op G iff for h being Element of G holds b2 . h = h " ); registration let G be non empty associative multMagma ; cluster the multF of G -> associative ; coherence the multF of G is associative proofend; end; theorem Th21: :: GROUP_1:21 for G being non empty unital multMagma holds 1_ G is_a_unity_wrt the multF of G proofend; theorem Th22: :: GROUP_1:22 for G being non empty unital multMagma holds the_unity_wrt the multF of G = 1_ G proofend; registration let G be non empty unital multMagma ; cluster the multF of G -> having_a_unity ; coherence the multF of G is having_a_unity proofend; end; theorem Th23: :: GROUP_1:23 for G being Group holds inverse_op G is_an_inverseOp_wrt the multF of G proofend; registration let G be Group; cluster the multF of G -> having_an_inverseOp ; coherence the multF of G is having_an_inverseOp proofend; end; theorem :: GROUP_1:24 for G being Group holds the_inverseOp_wrt the multF of G = inverse_op G proofend; definition let G be non empty multMagma ; 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 Element of NAT holds it . (h,(n + 1)) = (it . (h,n)) * h ) ); existence ex b1 being Function of [: the carrier of G,NAT:], the carrier of G st for h being Element of G holds ( b1 . (h,0) = 1_ G & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) ) proofend; uniqueness for b1, b2 being Function of [: the carrier of G,NAT:], the carrier of G st ( for h being Element of G holds ( b1 . (h,0) = 1_ G & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) ) ) & ( for h being Element of G holds ( b2 . (h,0) = 1_ G & ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines power GROUP_1:def_7_:_ for G being non empty multMagma for b2 being Function of [: the carrier of G,NAT:], the carrier of G holds ( b2 = power G iff for h being Element of G holds ( b2 . (h,0) = 1_ G & ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) ); definition let G be Group; let i be Integer; let h be Element of G; funch |^ i -> Element of G equals :Def8: :: GROUP_1:def 8 (power G) . (h,(abs i)) if 0 <= i otherwise ((power G) . (h,(abs i))) " ; correctness coherence ( ( 0 <= i implies (power G) . (h,(abs i)) is Element of G ) & ( not 0 <= i implies ((power G) . (h,(abs i))) " is Element of G ) ); consistency for b1 being Element of G holds verum; ; end; :: deftheorem Def8 defines |^ GROUP_1:def_8_:_ for G being Group for i being Integer for h being Element of G holds ( ( 0 <= i implies h |^ i = (power G) . (h,(abs i)) ) & ( not 0 <= i implies h |^ i = ((power G) . (h,(abs i))) " ) ); definition let G be Group; let n be Nat; let h be Element of G; redefine func h |^ n equals :: GROUP_1:def 9 (power G) . (h,n); compatibility for b1 being Element of G holds ( b1 = h |^ n iff b1 = (power G) . (h,n) ) proofend; end; :: deftheorem defines |^ GROUP_1:def_9_:_ for G being Group for n being Nat for h being Element of G 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 proofend; 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 proofend; theorem :: GROUP_1:25 for G being Group for h being Element of G holds h |^ 0 = 1_ G by Def7; theorem Th26: :: GROUP_1:26 for G being Group for h being Element of G holds h |^ 1 = h proofend; theorem Th27: :: GROUP_1:27 for G being Group for h being Element of G holds h |^ 2 = h * h proofend; theorem :: GROUP_1:28 for G being Group for h being Element of G holds h |^ 3 = (h * h) * h proofend; theorem :: GROUP_1:29 for G being Group for h being Element of G holds ( h |^ 2 = 1_ G iff h " = h ) proofend; Lm5: for n, m being Nat for G being Group for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m) proofend; 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) ) proofend; Lm7: for n, m being Nat for G being Group for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m proofend; Lm8: for n being Nat for G being Group for h being Element of G holds (h ") |^ n = (h |^ n) " proofend; 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 proofend; Lm10: for n, m 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) proofend; 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) proofend; theorem Th30: :: GROUP_1:30 for i being Integer for G being Group for h being Element of G st i <= 0 holds h |^ i = (h |^ (abs i)) " proofend; theorem :: GROUP_1:31 for i being Integer for G being Group holds (1_ G) |^ i = 1_ G proofend; theorem Th32: :: GROUP_1:32 for G being Group for h being Element of G holds h |^ (- 1) = h " proofend; Lm12: for i being Integer for G being Group for h being Element of G holds h |^ (- i) = (h |^ i) " proofend; Lm13: for j being Integer holds ( j >= 1 or j = 0 or j < 0 ) proofend; Lm14: for j being Integer for G being Group for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1)) proofend; Lm15: for j being Integer holds ( j >= 0 or j = - 1 or j < - 1 ) proofend; Lm16: for j being Integer for G being Group for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1) proofend; theorem Th33: :: 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) proofend; 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) ) proofend; Lm17: for i being Integer for G being Group for h being Element of G holds (h ") |^ i = (h |^ i) " proofend; 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 proofend; theorem :: GROUP_1:36 for i being Integer for G being Group for h being Element of G holds h |^ (- i) = (h |^ i) " by Lm12; theorem :: GROUP_1:37 for i being Integer for G being Group for h being Element of G holds (h ") |^ i = (h |^ i) " by Lm17; theorem Th38: :: 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) proofend; theorem Th39: :: 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) proofend; 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 proofend; definition let G be Group; let h be Element of G; attrh is being_of_order_0 means :Def10: :: GROUP_1:def 10 for n being Nat st h |^ n = 1_ G holds n = 0 ; end; :: deftheorem Def10 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 ); registration let G be Group; cluster 1_ G -> non being_of_order_0 ; coherence not 1_ G is being_of_order_0 proofend; end; definition let G be Group; 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 ( ( h is being_of_order_0 implies ex b1 being Element of NAT st b1 = 0 ) & ( not h is being_of_order_0 implies ex b1 being Element of NAT st ( h |^ b1 = 1_ G & b1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds b1 <= m ) ) ) ) proofend; uniqueness for b1, b2 being Element of NAT holds ( ( h is being_of_order_0 & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not h is being_of_order_0 & h |^ b1 = 1_ G & b1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds b1 <= m ) & h |^ b2 = 1_ G & b2 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds b2 <= m ) implies b1 = b2 ) ) proofend; correctness consistency for b1 being Element of NAT holds verum; ; end; :: deftheorem Def11 defines ord GROUP_1:def_11_:_ for G being Group for h being Element of G for b3 being Element of NAT holds ( ( h is being_of_order_0 implies ( b3 = ord h iff b3 = 0 ) ) & ( not h is being_of_order_0 implies ( b3 = ord h iff ( h |^ b3 = 1_ G & b3 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds b3 <= m ) ) ) ) ); theorem Th41: :: GROUP_1:41 for G being Group for h being Element of G holds h |^ (ord h) = 1_ G proofend; theorem :: GROUP_1:42 for G being Group holds ord (1_ G) = 1 proofend; theorem :: GROUP_1:43 for G being Group for h being Element of G st ord h = 1 holds h = 1_ G proofend; theorem :: GROUP_1:44 for n being Nat for G being Group for h being Element of G st h |^ n = 1_ G holds ord h divides n proofend; definition let G be finite 1-sorted ; :: original:card redefine func card G -> Element of NAT ; coherence card G is Element of NAT proofend; end; theorem :: GROUP_1:45 for G being non empty finite 1-sorted holds card G >= 1 proofend; definition let IT be multMagma ; attrIT is commutative means :Def12: :: GROUP_1:def 12 for x, y being Element of IT holds x * y = y * x; end; :: 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 ); registration cluster non empty strict unital Group-like associative commutative for multMagma ; existence ex b1 being Group st ( b1 is strict & b1 is commutative ) proofend; end; definition let FS be non empty commutative multMagma ; let x, y be Element of FS; :: original:* redefine funcx * y -> Element of the carrier of FS; commutativity for x, y being Element of FS holds x * y = y * x by Def12; end; theorem :: GROUP_1:46 multMagma(# REAL,addreal #) is commutative Group proofend; theorem :: GROUP_1:47 for A being commutative Group for a, b being Element of A holds (a * b) " = (a ") * (b ") by Th17; theorem :: GROUP_1:48 for i being Integer for A being commutative Group for a, b being Element of A holds (a * b) |^ i = (a |^ i) * (b |^ i) by Th38; 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 ) proofend; begin :: from COMPTRIG, 2006.08.12, A.T. theorem Th50: :: GROUP_1:50 for L being non empty unital multMagma for x being Element of L holds (power L) . (x,1) = x proofend; theorem :: GROUP_1:51 for L being non empty unital multMagma for x being Element of L holds (power L) . (x,2) = x * x proofend; theorem :: GROUP_1:52 for L being non empty unital associative commutative multMagma for x, y being Element of L for n being Element of NAT holds (power L) . ((x * y),n) = ((power L) . (x,n)) * ((power L) . (y,n)) proofend; :: Moved from ENDALG, 17.01_2006, AK definition let G, H be multMagma ; let IT be Function of G,H; attrIT is unity-preserving means :: GROUP_1:def 13 IT . (1_ G) = 1_ H; end; :: 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 );