:: Subgroup and Cosets of Subgroups. Lagrange theorem
:: by Wojciech A. Trybulec
::
:: Received July 23, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for x being set
for G being non empty 1-sorted
for A being Subset of G st x in A holds
x is Element of G
;
theorem :: GROUP_2:1
canceled;
theorem :: GROUP_2:2
canceled;
theorem :: GROUP_2:3
:: deftheorem defines " GROUP_2:def 1 :
theorem :: GROUP_2:4
canceled;
theorem Th5: :: GROUP_2:5
theorem :: GROUP_2:6
theorem :: GROUP_2:7
theorem :: GROUP_2:8
theorem :: GROUP_2:9
theorem :: GROUP_2:10
:: deftheorem defines * GROUP_2:def 2 :
theorem :: GROUP_2:11
canceled;
theorem Th12: :: GROUP_2:12
theorem Th13: :: GROUP_2:13
theorem Th14: :: GROUP_2:14
theorem :: GROUP_2:15
theorem :: GROUP_2:16
theorem :: GROUP_2:17
theorem :: GROUP_2:18
theorem :: GROUP_2:19
theorem Th20: :: GROUP_2:20
theorem Th21: :: GROUP_2:21
theorem Th22: :: GROUP_2:22
theorem :: GROUP_2:23
theorem :: GROUP_2:24
theorem :: GROUP_2:25
theorem Th26: :: GROUP_2:26
theorem Th27: :: GROUP_2:27
theorem :: GROUP_2:28
Lm2:
for A being commutative Group
for a, b being Element of A holds a * b = b * a
;
theorem Th29: :: GROUP_2:29
theorem :: GROUP_2:30
:: deftheorem defines * GROUP_2:def 3 :
:: deftheorem defines * GROUP_2:def 4 :
theorem :: GROUP_2:31
canceled;
theorem :: GROUP_2:32
canceled;
theorem Th33: :: GROUP_2:33
theorem Th34: :: GROUP_2:34
theorem :: GROUP_2:35
theorem :: GROUP_2:36
theorem :: GROUP_2:37
theorem Th38: :: GROUP_2:38
theorem :: GROUP_2:39
theorem Th40: :: GROUP_2:40
theorem :: GROUP_2:41
theorem :: GROUP_2:42
theorem Th43: :: GROUP_2:43
theorem :: GROUP_2:44
:: deftheorem Def5 defines Subgroup GROUP_2:def 5 :
theorem :: GROUP_2:45
canceled;
theorem :: GROUP_2:46
canceled;
theorem :: GROUP_2:47
canceled;
theorem Th48: :: GROUP_2:48
theorem Th49: :: GROUP_2:49
theorem Th50: :: GROUP_2:50
theorem Th51: :: GROUP_2:51
theorem Th52: :: GROUP_2:52
theorem Th53: :: GROUP_2:53
theorem :: GROUP_2:54
theorem Th55: :: GROUP_2:55
theorem :: GROUP_2:56
theorem Th57: :: GROUP_2:57
theorem :: GROUP_2:58
theorem Th59: :: GROUP_2:59
theorem Th60: :: GROUP_2:60
theorem Th61: :: GROUP_2:61
theorem Th62: :: GROUP_2:62
theorem Th63: :: GROUP_2:63
theorem Th64: :: GROUP_2:64
theorem Th65: :: GROUP_2:65
theorem Th66: :: GROUP_2:66
theorem Th67: :: GROUP_2:67
theorem Th68: :: GROUP_2:68
theorem Th69: :: GROUP_2:69
:: deftheorem defines = GROUP_2:def 6 :
theorem Th70: :: GROUP_2:70
theorem Th71: :: GROUP_2:71
:: deftheorem Def7 defines (1). GROUP_2:def 7 :
:: deftheorem defines (Omega). GROUP_2:def 8 :
theorem :: GROUP_2:72
canceled;
theorem :: GROUP_2:73
canceled;
theorem :: GROUP_2:74
canceled;
theorem Th75: :: GROUP_2:75
theorem :: GROUP_2:76
theorem Th77: :: GROUP_2:77
theorem :: GROUP_2:78
theorem :: GROUP_2:79
theorem Th80: :: GROUP_2:80
theorem Th81: :: GROUP_2:81
theorem Th82: :: GROUP_2:82
theorem :: GROUP_2:83
theorem :: GROUP_2:84
theorem :: GROUP_2:85
:: deftheorem defines carr GROUP_2:def 9 :
theorem :: GROUP_2:86
canceled;
theorem :: GROUP_2:87
canceled;
theorem :: GROUP_2:88
canceled;
theorem Th89: :: GROUP_2:89
theorem Th90: :: GROUP_2:90
theorem :: GROUP_2:91
theorem :: GROUP_2:92
theorem Th93: :: GROUP_2:93
theorem :: GROUP_2:94
:: deftheorem Def10 defines /\ GROUP_2:def 10 :
theorem :: GROUP_2:95
canceled;
theorem :: GROUP_2:96
canceled;
theorem Th97: :: GROUP_2:97
theorem :: GROUP_2:98
theorem Th99: :: GROUP_2:99
theorem :: GROUP_2:100
theorem Th101: :: GROUP_2:101
theorem :: GROUP_2:102
Lm3:
for G being Group
for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2),the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1,the multF of H1 #) )
theorem :: GROUP_2:103
theorem :: GROUP_2:104
theorem :: GROUP_2:105
Lm4:
for G being Group
for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1
theorem :: GROUP_2:106
theorem :: GROUP_2:107
theorem :: GROUP_2:108
theorem :: GROUP_2:109
theorem :: GROUP_2:110
theorem :: GROUP_2:111
:: deftheorem defines * GROUP_2:def 11 :
:: deftheorem defines * GROUP_2:def 12 :
theorem :: GROUP_2:112
canceled;
theorem :: GROUP_2:113
canceled;
theorem :: GROUP_2:114
theorem :: GROUP_2:115
theorem :: GROUP_2:116
theorem :: GROUP_2:117
theorem :: GROUP_2:118
theorem :: GROUP_2:119
theorem :: GROUP_2:120
theorem :: GROUP_2:121
theorem :: GROUP_2:122
:: deftheorem defines * GROUP_2:def 13 :
:: deftheorem defines * GROUP_2:def 14 :
theorem :: GROUP_2:123
canceled;
theorem :: GROUP_2:124
canceled;
theorem Th125: :: GROUP_2:125
theorem Th126: :: GROUP_2:126
theorem :: GROUP_2:127
theorem :: GROUP_2:128
theorem :: GROUP_2:129
theorem Th130: :: GROUP_2:130
theorem :: GROUP_2:131
canceled;
theorem :: GROUP_2:132
theorem Th133: :: GROUP_2:133
theorem Th134: :: GROUP_2:134
theorem :: GROUP_2:135
theorem Th136: :: GROUP_2:136
theorem Th137: :: GROUP_2:137
theorem Th138: :: GROUP_2:138
theorem Th139: :: GROUP_2:139
theorem :: GROUP_2:140
theorem :: GROUP_2:141
theorem Th142: :: GROUP_2:142
theorem Th143: :: GROUP_2:143
theorem :: GROUP_2:144
theorem Th145: :: GROUP_2:145
theorem :: GROUP_2:146
theorem :: GROUP_2:147
theorem :: GROUP_2:148
theorem :: GROUP_2:149
theorem :: GROUP_2:150
theorem Th151: :: GROUP_2:151
theorem Th152: :: GROUP_2:152
theorem Th153: :: GROUP_2:153
theorem Th154: :: GROUP_2:154
theorem :: GROUP_2:155
theorem Th156: :: GROUP_2:156
:: deftheorem Def15 defines Left_Cosets GROUP_2:def 15 :
:: deftheorem Def16 defines Right_Cosets GROUP_2:def 16 :
theorem :: GROUP_2:157
canceled;
theorem :: GROUP_2:158
canceled;
theorem :: GROUP_2:159
canceled;
theorem :: GROUP_2:160
canceled;
theorem :: GROUP_2:161
canceled;
theorem :: GROUP_2:162
canceled;
theorem :: GROUP_2:163
canceled;
theorem :: GROUP_2:164
theorem :: GROUP_2:165
theorem Th166: :: GROUP_2:166
theorem Th167: :: GROUP_2:167
theorem Th168: :: GROUP_2:168
theorem :: GROUP_2:169
theorem :: GROUP_2:170
theorem :: GROUP_2:171
theorem Th172: :: GROUP_2:172
theorem Th173: :: GROUP_2:173
theorem :: GROUP_2:174
:: deftheorem defines Index GROUP_2:def 17 :
theorem :: GROUP_2:175
:: deftheorem Def18 defines index GROUP_2:def 18 :
theorem :: GROUP_2:176
Lm5:
for k being Element of NAT
for X being finite set st ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X & card C = k * (card X) )
theorem Th177: :: GROUP_2:177
theorem :: GROUP_2:178
theorem :: GROUP_2:179
theorem :: GROUP_2:180
theorem :: GROUP_2:181
theorem :: GROUP_2:182
theorem :: GROUP_2:183
theorem Th184: :: GROUP_2:184
theorem :: GROUP_2:185
theorem :: GROUP_2:186