:: Submodules and Cosets of Submodules in Right Module over Associative Ring
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines linearly-closed RMOD_2:def 1 :
theorem :: RMOD_2:1
canceled;
theorem :: RMOD_2:2
canceled;
theorem :: RMOD_2:3
canceled;
theorem Th4: :: RMOD_2:4
theorem Th5: :: RMOD_2:5
theorem :: RMOD_2:6
theorem Th7: :: RMOD_2:7
theorem :: RMOD_2:8
theorem :: RMOD_2:9
theorem :: RMOD_2:10
:: deftheorem Def2 defines Submodule RMOD_2:def 2 :
theorem :: RMOD_2:11
canceled;
theorem :: RMOD_2:12
canceled;
theorem :: RMOD_2:13
canceled;
theorem :: RMOD_2:14
canceled;
theorem :: RMOD_2:15
canceled;
theorem :: RMOD_2:16
theorem Th17: :: RMOD_2:17
theorem Th18: :: RMOD_2:18
theorem :: RMOD_2:19
theorem :: RMOD_2:20
theorem Th21: :: RMOD_2:21
theorem Th22: :: RMOD_2:22
theorem Th23: :: RMOD_2:23
theorem Th24: :: RMOD_2:24
Lm1:
for R being Ring
for V being RightMod of R
for V1 being Subset of V
for W being Submodule of V st the carrier of W = V1 holds
V1 is linearly-closed
theorem Th25: :: RMOD_2:25
theorem :: RMOD_2:26
theorem :: RMOD_2:27
theorem Th28: :: RMOD_2:28
theorem Th29: :: RMOD_2:29
theorem Th30: :: RMOD_2:30
theorem Th31: :: RMOD_2:31
theorem Th32: :: RMOD_2:32
theorem Th33: :: RMOD_2:33
theorem Th34: :: RMOD_2:34
theorem Th35: :: RMOD_2:35
theorem :: RMOD_2:36
theorem Th37: :: RMOD_2:37
theorem Th38: :: RMOD_2:38
theorem :: RMOD_2:39
theorem :: RMOD_2:40
theorem :: RMOD_2:41
theorem Th42: :: RMOD_2:42
:: deftheorem Def3 defines (0). RMOD_2:def 3 :
:: deftheorem defines (Omega). RMOD_2:def 4 :
theorem :: RMOD_2:43
canceled;
theorem :: RMOD_2:44
canceled;
theorem :: RMOD_2:45
canceled;
theorem :: RMOD_2:46
theorem Th47: :: RMOD_2:47
theorem Th48: :: RMOD_2:48
theorem :: RMOD_2:49
theorem :: RMOD_2:50
theorem :: RMOD_2:51
theorem :: RMOD_2:52
canceled;
theorem :: RMOD_2:53
:: deftheorem defines + RMOD_2:def 5 :
Lm2:
for R being Ring
for V being RightMod of R
for W being Submodule of V holds (0. V) + W = the carrier of W
:: deftheorem Def6 defines Coset RMOD_2:def 6 :
theorem :: RMOD_2:54
canceled;
theorem :: RMOD_2:55
canceled;
theorem :: RMOD_2:56
canceled;
theorem Th57: :: RMOD_2:57
theorem Th58: :: RMOD_2:58
theorem Th59: :: RMOD_2:59
theorem :: RMOD_2:60
theorem Th61: :: RMOD_2:61
Lm3:
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V holds
( v in W iff v + W = the carrier of W )
theorem Th62: :: RMOD_2:62
theorem Th63: :: RMOD_2:63
theorem :: RMOD_2:64
theorem :: RMOD_2:65
theorem Th66: :: RMOD_2:66
theorem :: RMOD_2:67
theorem Th68: :: RMOD_2:68
theorem Th69: :: RMOD_2:69
theorem Th70: :: RMOD_2:70
theorem :: RMOD_2:71
theorem Th72: :: RMOD_2:72
theorem :: RMOD_2:73
theorem :: RMOD_2:74
canceled;
theorem :: RMOD_2:75
theorem Th76: :: RMOD_2:76
theorem Th77: :: RMOD_2:77
theorem Th78: :: RMOD_2:78
theorem Th79: :: RMOD_2:79
theorem Th80: :: RMOD_2:80
theorem :: RMOD_2:81
theorem :: RMOD_2:82
theorem :: RMOD_2:83
theorem :: RMOD_2:84
theorem :: RMOD_2:85
theorem :: RMOD_2:86
theorem :: RMOD_2:87
theorem :: RMOD_2:88
theorem :: RMOD_2:89
theorem Th90: :: RMOD_2:90
theorem :: RMOD_2:91
theorem :: RMOD_2:92
theorem :: RMOD_2:93
theorem :: RMOD_2:94