:: Classes of Conjugation. Normal Subgroups
:: by Wojciech A. Trybulec
::
:: Received August 10, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: GROUP_3:1
for
G being
Group for
a,
b being
Element of
G holds
(
(a * b) * (b " ) = a &
(a * (b " )) * b = a &
((b " ) * b) * a = a &
(b * (b " )) * a = a &
a * (b * (b " )) = a &
a * ((b " ) * b) = a &
(b " ) * (b * a) = a &
b * ((b " ) * a) = a )
Lm1:
for A being commutative Group
for a, b being Element of A holds a * b = b * a
;
theorem :: GROUP_3:2
theorem :: GROUP_3:3
theorem Th4: :: GROUP_3:4
theorem :: GROUP_3:5
theorem Th6: :: GROUP_3:6
theorem :: GROUP_3:7
theorem :: GROUP_3:8
theorem :: GROUP_3:9
canceled;
theorem Th10: :: GROUP_3:10
theorem :: GROUP_3:11
theorem :: GROUP_3:12
theorem :: GROUP_3:13
theorem :: GROUP_3:14
canceled;
theorem :: GROUP_3:15
:: deftheorem Def1 defines Subgroups GROUP_3:def 1 :
theorem :: GROUP_3:16
canceled;
theorem :: GROUP_3:17
canceled;
theorem :: GROUP_3:18
theorem Th19: :: GROUP_3:19
:: deftheorem defines |^ GROUP_3:def 2 :
theorem :: GROUP_3:20
canceled;
theorem Th21: :: GROUP_3:21
theorem Th22: :: GROUP_3:22
theorem Th23: :: GROUP_3:23
theorem Th24: :: GROUP_3:24
theorem Th25: :: GROUP_3:25
theorem Th26: :: GROUP_3:26
theorem Th27: :: GROUP_3:27
theorem Th28: :: GROUP_3:28
theorem Th29: :: GROUP_3:29
theorem Th30: :: GROUP_3:30
theorem :: GROUP_3:31
canceled;
theorem Th32: :: GROUP_3:32
Lm4:
for n being Nat
for G being Group
for a, b being Element of G holds (a |^ n) |^ b = (a |^ b) |^ n
theorem :: GROUP_3:33
theorem :: GROUP_3:34
theorem Th35: :: GROUP_3:35
theorem Th36: :: GROUP_3:36
:: deftheorem defines |^ GROUP_3:def 3 :
theorem :: GROUP_3:37
canceled;
theorem Th38: :: GROUP_3:38
theorem Th39: :: GROUP_3:39
theorem Th40: :: GROUP_3:40
theorem Th41: :: GROUP_3:41
theorem Th42: :: GROUP_3:42
theorem :: GROUP_3:43
theorem Th44: :: GROUP_3:44
theorem :: GROUP_3:45
theorem :: GROUP_3:46
theorem :: GROUP_3:47
:: deftheorem defines |^ GROUP_3:def 4 :
:: deftheorem defines |^ GROUP_3:def 5 :
theorem :: GROUP_3:48
canceled;
theorem :: GROUP_3:49
canceled;
theorem Th50: :: GROUP_3:50
theorem Th51: :: GROUP_3:51
theorem :: GROUP_3:52
theorem :: GROUP_3:53
theorem :: GROUP_3:54
theorem :: GROUP_3:55
theorem Th56: :: GROUP_3:56
theorem :: GROUP_3:57
theorem :: GROUP_3:58
theorem Th59: :: GROUP_3:59
theorem :: GROUP_3:60
theorem Th61: :: GROUP_3:61
theorem :: GROUP_3:62
theorem Th63: :: GROUP_3:63
theorem :: GROUP_3:64
canceled;
theorem Th65: :: GROUP_3:65
theorem :: GROUP_3:66
theorem :: GROUP_3:67
:: deftheorem Def6 defines |^ GROUP_3:def 6 :
theorem :: GROUP_3:68
canceled;
theorem :: GROUP_3:69
canceled;
theorem Th70: :: GROUP_3:70
theorem Th71: :: GROUP_3:71
theorem Th72: :: GROUP_3:72
theorem Th73: :: GROUP_3:73
theorem Th74: :: GROUP_3:74
theorem :: GROUP_3:75
canceled;
theorem Th76: :: GROUP_3:76
theorem Th77: :: GROUP_3:77
theorem Th78: :: GROUP_3:78
theorem :: GROUP_3:79
theorem Th80: :: GROUP_3:80
theorem :: GROUP_3:81
theorem Th82: :: GROUP_3:82
theorem :: GROUP_3:83
theorem Th84: :: GROUP_3:84
theorem :: GROUP_3:85
theorem Th86: :: GROUP_3:86
:: deftheorem Def7 defines are_conjugated GROUP_3:def 7 :
theorem :: GROUP_3:87
canceled;
theorem Th88: :: GROUP_3:88
theorem Th89: :: GROUP_3:89
theorem Th90: :: GROUP_3:90
theorem Th91: :: GROUP_3:91
theorem Th92: :: GROUP_3:92
theorem Th93: :: GROUP_3:93
:: deftheorem defines con_class GROUP_3:def 8 :
theorem :: GROUP_3:94
canceled;
theorem Th95: :: GROUP_3:95
theorem Th96: :: GROUP_3:96
theorem Th97: :: GROUP_3:97
theorem :: GROUP_3:98
theorem :: GROUP_3:99
theorem :: GROUP_3:100
theorem :: GROUP_3:101
theorem :: GROUP_3:102
:: deftheorem Def9 defines are_conjugated GROUP_3:def 9 :
theorem :: GROUP_3:103
canceled;
theorem Th104: :: GROUP_3:104
theorem Th105: :: GROUP_3:105
theorem Th106: :: GROUP_3:106
theorem Th107: :: GROUP_3:107
theorem Th108: :: GROUP_3:108
theorem Th109: :: GROUP_3:109
:: deftheorem defines con_class GROUP_3:def 10 :
theorem :: GROUP_3:110
canceled;
theorem :: GROUP_3:111
theorem :: GROUP_3:112
canceled;
theorem Th113: :: GROUP_3:113
theorem :: GROUP_3:114
theorem :: GROUP_3:115
theorem :: GROUP_3:116
theorem :: GROUP_3:117
theorem Th118: :: GROUP_3:118
theorem :: GROUP_3:119
:: deftheorem Def11 defines are_conjugated GROUP_3:def 11 :
theorem :: GROUP_3:120
canceled;
theorem Th121: :: GROUP_3:121
theorem Th122: :: GROUP_3:122
theorem Th123: :: GROUP_3:123
theorem Th124: :: GROUP_3:124
:: deftheorem Def12 defines con_class GROUP_3:def 12 :
theorem :: GROUP_3:125
canceled;
theorem :: GROUP_3:126
canceled;
theorem Th127: :: GROUP_3:127
theorem Th128: :: GROUP_3:128
theorem Th129: :: GROUP_3:129
theorem Th130: :: GROUP_3:130
theorem :: GROUP_3:131
theorem :: GROUP_3:132
theorem :: GROUP_3:133
theorem Th134: :: GROUP_3:134
:: deftheorem Def13 defines normal GROUP_3:def 13 :
theorem :: GROUP_3:135
canceled;
theorem :: GROUP_3:136
canceled;
theorem Th137: :: GROUP_3:137
theorem :: GROUP_3:138
theorem :: GROUP_3:139
theorem Th140: :: GROUP_3:140
theorem Th141: :: GROUP_3:141
theorem Th142: :: GROUP_3:142
theorem :: GROUP_3:143
theorem :: GROUP_3:144
theorem :: GROUP_3:145
theorem :: GROUP_3:146
theorem :: GROUP_3:147
Lm5:
for G being Group
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)
theorem Th148: :: GROUP_3:148
theorem :: GROUP_3:149
theorem :: GROUP_3:150
theorem :: GROUP_3:151
:: deftheorem Def14 defines Normalizator GROUP_3:def 14 :
theorem :: GROUP_3:152
canceled;
theorem :: GROUP_3:153
canceled;
theorem Th154: :: GROUP_3:154
theorem Th155: :: GROUP_3:155
theorem :: GROUP_3:156
theorem Th157: :: GROUP_3:157
theorem :: GROUP_3:158
:: deftheorem defines Normalizator GROUP_3:def 15 :
theorem :: GROUP_3:159
canceled;
theorem Th160: :: GROUP_3:160
theorem Th161: :: GROUP_3:161
theorem :: GROUP_3:162
theorem Th163: :: GROUP_3:163
theorem :: GROUP_3:164
theorem :: GROUP_3:165