environ
vocabularies HIDDEN, NUMBERS, NAT_1, INT_1, XBOOLE_0, ALGSTR_0, SUBSET_1, BINOP_2, RELAT_1, REAL_1, ARYTM_3, CARD_1, ARYTM_1, BINOP_1, STRUCT_0, FUNCT_1, SETWISEO, FINSEQOP, ZFMISC_1, COMPLEX1, XXREAL_0, FINSET_1, TARSKI, RLVECT_1, SUPINF_2, GROUP_1, POLYNOM1, GROUP_1A, REALSET1, RLSUB_1, SETFAM_1, CQC_SIM1, GROUP_2, PRE_TOPC, GROUP_3, FUNCT_2, VALUED_1, ORDINAL2, CONNSP_2, TOPS_1, RCOMP_1, UNIALG_1, CARD_5, COMPTS_1, RLVECT_3, TOPGRP_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, RELAT_1, PARTFUN1, SETFAM_1, FINSUB_1, FINSET_1, REALSET1, WELLORD2, DOMAIN_1, NAT_D, MCART_1, XREAL_0, PRE_TOPC, TOPS_1, TOPS_2, FUNCT_1, RELSET_1, FUNCT_2, BINOP_2, BINOP_1, INT_1, NAT_1, INT_2, FINSEQOP, SETWISEO, STRUCT_0, ALGSTR_0, RLVECT_1, CONNSP_2, COMPTS_1, BORSUK_1, CANTOR_1, YELLOW_8, TOPGRP_1, IDEAL_1;
definitions FUNCT_2, BINOP_1, FINSEQOP, RLVECT_1, SETWISEO, ALGSTR_0, PRE_TOPC, TOPS_2, CONNSP_2, TOPGRP_1, FUNCT_1, STRUCT_0, TARSKI, XBOOLE_0;
theorems ABSVALUE, BINOP_1, CARD_1, FINSEQOP, INT_1, NAT_1, ZFMISC_1, BINOP_2, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, XREAL_0, GROUP_2, CARD_2, ENUMSET1, FINSET_1, FUNCT_1, FUNCT_2, TARSKI, WELLORD2, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, NAT_D, STRUCT_0, RLVECT_1, XTUPLE_0, PRE_TOPC, TOPS_1, TOPS_2, YELLOW_8, BORSUK_1, TEX_2, CONNSP_2, YELLOW_9, TOPGRP_1;
schemes FUNCT_2, INT_1, NAT_1, CLASSES1, BINOP_1, FUNCT_1, SUBSET_1, XBOOLE_0, XFAMILY;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, STRUCT_0, ALGSTR_0, CARD_1, SUBSET_1, FINSUB_1, MEMBERED, REALSET1, XCMPLX_0, XBOOLE_0, FUNCT_1, FUNCT_2, PRE_TOPC, TOPS_1, COMPTS_1, BORSUK_1, TOPGRP_1;
constructors HIDDEN, SETWISEO, NAT_1, NAT_D, BINOP_2, FINSEQOP, RLVECT_1, SETFAM_1, WELLORD2, MEMBERED, REALSET1, RELSET_1, INT_2, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, GRCAT_1, CANTOR_1, YELLOW_8, TOPGRP_1, IDEAL_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities BINOP_1, STRUCT_0, ALGSTR_0, XBOOLE_0, REALSET1, SUBSET_1, TARSKI, COMPTS_1, IDEAL_1;
expansions FUNCT_2, STRUCT_0, TARSKI, XBOOLE_0, RLVECT_1, BINOP_1, FINSEQOP;
Lm1:
now ( ( for h, g, f being Element of addMagma(# REAL,addreal #) holds (h + g) + f = h + (g + f) ) & ex e being Element of addMagma(# REAL,addreal #) st
for h being Element of addMagma(# REAL,addreal #) holds
( h + e = h & e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) ) )
set G =
addMagma(#
REAL,
addreal #);
thus
for
h,
g,
f being
Element of
addMagma(#
REAL,
addreal #) holds
(h + g) + f = h + (g + f)
ex e being Element of addMagma(# REAL,addreal #) st
for h being Element of addMagma(# REAL,addreal #) holds
( h + e = h & e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )
reconsider e =
0 as
Element of
addMagma(#
REAL,
addreal #)
by XREAL_0:def 1;
take e =
e;
for h being Element of addMagma(# REAL,addreal #) holds
( h + e = h & e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )let h be
Element of
addMagma(#
REAL,
addreal #);
( h + e = h & e + h = h & ex g being Element of addMagma(# 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
;
( e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )thus e + h =
0 + A
by BINOP_2:def 9
.=
h
;
ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e )reconsider g =
- A as
Element of
addMagma(#
REAL,
addreal #)
by XREAL_0:def 1;
take g =
g;
( h + g = e & g + h = e )thus h + g =
A + (- A)
by BINOP_2:def 9
.=
e
;
g + h = ethus g + h =
(- A) + A
by BINOP_2:def 9
.=
e
;
verum
end;
definition
let G be non
empty addMagma ;
existence
ex b1 being Function of [:NAT, the carrier of G:], the carrier of G st
for h being Element of G holds
( b1 . (0,h) = 0_ G & ( for n being Nat holds b1 . ((n + 1),h) = (b1 . (n,h)) + h ) )
uniqueness
for b1, b2 being Function of [:NAT, the carrier of G:], the carrier of G st ( for h being Element of G holds
( b1 . (0,h) = 0_ G & ( for n being Nat holds b1 . ((n + 1),h) = (b1 . (n,h)) + h ) ) ) & ( for h being Element of G holds
( b2 . (0,h) = 0_ G & ( for n being Nat holds b2 . ((n + 1),h) = (b2 . (n,h)) + h ) ) ) holds
b1 = b2
end;
Lm3:
for G being addGroup
for h being Element of G holds 0 * h = 0_ G
by Def7;
Lm4:
for n being Nat
for G being addGroup holds n * (0_ G) = 0_ G
Lm5:
for m, n being Nat
for G being addGroup
for h being Element of G holds (n + m) * h = (n * h) + (m * h)
Lm6:
for n being Nat
for G being addGroup
for h being Element of G holds
( (n + 1) * h = (n * h) + h & (n + 1) * h = h + (n * h) )
Lm9:
for n being Nat
for G being addGroup
for g, h being Element of G st g + h = h + g holds
g + (n * h) = (n * h) + g
Lm10:
for m, n being Nat
for G being addGroup
for g, h being Element of G st g + h = h + g holds
(n * g) + (m * h) = (m * h) + (n * g)
Lm11:
for n being Nat
for G being addGroup
for g, h being Element of G st g + h = h + g holds
n * (g + h) = (n * g) + (n * h)
Lm12:
for i being Integer
for G being addGroup
for h being Element of G holds (- i) * h = - (i * h)
Lm13:
for j being Integer holds
( j >= 1 or j = 0 or j < 0 )
Lm14:
for j being Integer
for G being addGroup
for h being Element of G holds (j - 1) * h = (j * h) + ((- 1) * h)
Lm15:
for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )
Lm16:
for j being Integer
for G being addGroup
for h being Element of G holds (j + 1) * h = (j * h) + (1 * h)
Lm1:
for x being object
for G being addGroup
for A being Subset of G st x in A holds
x is Element of G
;
Lm2:
for A being Abelian addGroup
for a, b being Element of A holds a + b = b + a
;
Lm3:
for G being addGroup
for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff addMagma(# the carrier of (H1 /\ H2), the addF of (H1 /\ H2) #) = addMagma(# the carrier of H1, the addF of H1 #) )
Lm4:
for G being addGroup
for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1
Lm1:
for A being Abelian addGroup
for a, b being Element of A holds a + b = b + a
;
Lm4:
for n being Nat
for G being addGroup
for a, b being Element of G holds (n * a) * b = n * (a * b)
Th75:
for G being addGroup
for a being Element of G holds a,a are_conjugated
Th76:
for G being addGroup
for a, b being Element of G st a,b are_conjugated holds
b,a are_conjugated
Lm5:
for G being addGroup
for N2 being normal Subgroup of G
for N1 being strict normal Subgroup of G holds (carr N1) + (carr N2) c= (carr N2) + (carr N1)
Lm1:
for G being addGroup
for A, B being Subset of G st A c= B holds
- A c= - B
Th59:
for G being TopologicaladdGroup holds G is regular