:: Submodules
:: by Micha{\l} Muzalewski
::
:: Received June 19, 1992
:: Copyright (c) 1992 Association of Mizar Users
theorem :: LMOD_6:1
theorem :: LMOD_6:2
theorem Th3: :: LMOD_6:3
theorem Th4: :: LMOD_6:4
:: deftheorem LMOD_6:def 1 :
canceled;
:: deftheorem Def2 defines trivial LMOD_6:def 2 :
theorem Th5: :: LMOD_6:5
theorem :: LMOD_6:6
theorem :: LMOD_6:7
:: deftheorem defines @ LMOD_6:def 3 :
theorem :: LMOD_6:8
canceled;
theorem Th9: :: LMOD_6:9
:: deftheorem LMOD_6:def 4 :
canceled;
:: deftheorem defines @ LMOD_6:def 5 :
theorem :: LMOD_6:10
theorem :: LMOD_6:11
theorem Th12: :: LMOD_6:12
theorem Th13: :: LMOD_6:13
theorem :: LMOD_6:14
canceled;
theorem :: LMOD_6:15
:: deftheorem defines <: LMOD_6:def 6 :
:: deftheorem Def7 defines c= LMOD_6:def 7 :
theorem Th16: :: LMOD_6:16
theorem :: LMOD_6:17
for
K being
Ring for
r being
Scalar of
K for
M,
N being
LeftMod of
K for
m1,
m2,
m being
Vector of
M for
n1,
n2,
n being
Vector of
N st
M c= N holds
(
0. M = 0. N & (
m1 = n1 &
m2 = n2 implies
m1 + m2 = n1 + n2 ) & (
m = n implies
r * m = r * n ) & (
m = n implies
- n = - m ) & (
m1 = n1 &
m2 = n2 implies
m1 - m2 = n1 - n2 ) &
0. N in M &
0. M in N & (
n1 in M &
n2 in M implies
n1 + n2 in M ) & (
n in M implies
r * n in M ) & (
n in M implies
- n in M ) & (
n1 in M &
n2 in M implies
n1 - n2 in M ) )
theorem :: LMOD_6:18
theorem :: LMOD_6:19
canceled;
theorem :: LMOD_6:20
canceled;
theorem :: LMOD_6:21
theorem :: LMOD_6:22
theorem :: LMOD_6:23
theorem :: LMOD_6:24
theorem :: LMOD_6:25
theorem :: LMOD_6:26
theorem :: LMOD_6:27
theorem :: LMOD_6:28
theorem :: LMOD_6:29
theorem :: LMOD_6:30
theorem :: LMOD_6:31
theorem :: LMOD_6:32
theorem :: LMOD_6:33
theorem :: LMOD_6:34
theorem :: LMOD_6:35
theorem :: LMOD_6:36
theorem :: LMOD_6:37
theorem :: LMOD_6:38
theorem :: LMOD_6:39
theorem Th40: :: LMOD_6:40
theorem Th41: :: LMOD_6:41
theorem Th42: :: LMOD_6:42
theorem :: LMOD_6:43
theorem :: LMOD_6:44