:: Homomorphisms and Isomorphisms of Groups. Quotient Group
:: by Wojciech A. Trybulec and Micha{\l} J. Trybulec
::
:: Received October 3, 1991
:: Copyright (c) 1991 Association of Mizar Users
theorem Th1: :: GROUP_6:1
theorem Th2: :: GROUP_6:2
theorem :: GROUP_6:3
theorem Th4: :: GROUP_6:4
theorem :: GROUP_6:5
canceled;
theorem Th6: :: GROUP_6:6
theorem Th7: :: GROUP_6:7
theorem Th8: :: GROUP_6:8
theorem Th9: :: GROUP_6:9
:: deftheorem Def1 defines `*` GROUP_6:def 1 :
theorem Th10: :: GROUP_6:10
:: deftheorem Def2 defines trivial GROUP_6:def 2 :
theorem Th11: :: GROUP_6:11
theorem Th12: :: GROUP_6:12
theorem Th13: :: GROUP_6:13
theorem :: GROUP_6:14
canceled;
theorem Th15: :: GROUP_6:15
theorem Th16: :: GROUP_6:16
theorem Th17: :: GROUP_6:17
theorem Th18: :: GROUP_6:18
definition
canceled;let G be
Group;
let N be
normal Subgroup of
G;
func CosOp N -> BinOp of
Cosets N means :
Def4:
:: GROUP_6:def 4
for
W1,
W2 being
Element of
Cosets N for
A1,
A2 being
Subset of
G st
W1 = A1 &
W2 = A2 holds
it . W1,
W2 = A1 * A2;
existence
ex b1 being BinOp of Cosets N st
for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b1 . W1,W2 = A1 * A2
uniqueness
for b1, b2 being BinOp of Cosets N st ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b1 . W1,W2 = A1 * A2 ) & ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b2 . W1,W2 = A1 * A2 ) holds
b1 = b2
end;
:: deftheorem GROUP_6:def 3 :
canceled;
:: deftheorem Def4 defines CosOp GROUP_6:def 4 :
:: deftheorem defines ./. GROUP_6:def 5 :
theorem :: GROUP_6:19
canceled;
theorem :: GROUP_6:20
canceled;
theorem :: GROUP_6:21
canceled;
theorem :: GROUP_6:22
theorem :: GROUP_6:23
:: deftheorem defines @ GROUP_6:def 6 :
theorem :: GROUP_6:24
theorem :: GROUP_6:25
theorem :: GROUP_6:26
theorem :: GROUP_6:27
theorem Th28: :: GROUP_6:28
theorem Th29: :: GROUP_6:29
theorem Th30: :: GROUP_6:30
theorem :: GROUP_6:31
canceled;
theorem :: GROUP_6:32
theorem :: GROUP_6:33
theorem Th34: :: GROUP_6:34
theorem :: GROUP_6:35
theorem :: GROUP_6:36
Lm1:
for G, H being Group
for a, b being Element of G
for f being Function of the carrier of G,the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds
f . (a * b) = (f . a) * (f . b)
:: deftheorem Def7 defines multiplicative GROUP_6:def 7 :
theorem :: GROUP_6:37
canceled;
theorem :: GROUP_6:38
canceled;
theorem :: GROUP_6:39
canceled;
theorem Th40: :: GROUP_6:40
theorem Th41: :: GROUP_6:41
theorem Th42: :: GROUP_6:42
theorem Th43: :: GROUP_6:43
theorem :: GROUP_6:44
theorem Th45: :: GROUP_6:45
theorem :: GROUP_6:46
theorem Th47: :: GROUP_6:47
theorem Th48: :: GROUP_6:48
:: deftheorem Def8 defines 1: GROUP_6:def 8 :
theorem :: GROUP_6:49
:: deftheorem Def9 defines nat_hom GROUP_6:def 9 :
:: deftheorem Def10 defines Ker GROUP_6:def 10 :
theorem Th50: :: GROUP_6:50
theorem :: GROUP_6:51
theorem Th52: :: GROUP_6:52
:: deftheorem Def11 defines Image GROUP_6:def 11 :
theorem Th53: :: GROUP_6:53
theorem Th54: :: GROUP_6:54
theorem :: GROUP_6:55
theorem :: GROUP_6:56
theorem Th57: :: GROUP_6:57
theorem Th58: :: GROUP_6:58
theorem Th59: :: GROUP_6:59
Lm2:
for A being commutative Group
for a, b being Element of A holds a * b = b * a
;
theorem :: GROUP_6:60
theorem Th61: :: GROUP_6:61
theorem :: GROUP_6:62
theorem :: GROUP_6:63
theorem :: GROUP_6:64
canceled;
theorem Th65: :: GROUP_6:65
theorem Th66: :: GROUP_6:66
theorem Th67: :: GROUP_6:67
theorem Th68: :: GROUP_6:68
theorem Th69: :: GROUP_6:69
theorem Th70: :: GROUP_6:70
theorem :: GROUP_6:71
theorem Th72: :: GROUP_6:72
theorem Th73: :: GROUP_6:73
theorem Th74: :: GROUP_6:74
theorem Th75: :: GROUP_6:75
:: deftheorem GROUP_6:def 12 :
canceled;
:: deftheorem GROUP_6:def 13 :
canceled;
:: deftheorem GROUP_6:def 14 :
canceled;
:: deftheorem Def15 defines are_isomorphic GROUP_6:def 15 :
theorem :: GROUP_6:76
canceled;
theorem Th77: :: GROUP_6:77
theorem :: GROUP_6:78
theorem :: GROUP_6:79
theorem Th80: :: GROUP_6:80
theorem :: GROUP_6:81
theorem :: GROUP_6:82
theorem :: GROUP_6:83
theorem Th84: :: GROUP_6:84
theorem Th85: :: GROUP_6:85
theorem :: GROUP_6:86
theorem :: GROUP_6:87
theorem :: GROUP_6:88
canceled;
theorem :: GROUP_6:89
Lm3:
for H, G being Group
for g being Homomorphism of G,H holds
( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) ) )
theorem :: GROUP_6:90
theorem :: GROUP_6:91
theorem :: GROUP_6:92
theorem :: GROUP_6:93