:: Linear Combinations in Right Module over Associative Ring
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for R being Ring
for V being RightMod of R
for v being Vector of V
for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds
Sum F = (Sum G) + v
theorem Th1: :: RMOD_4:1
Lm2:
for R being Ring
for V being RightMod of R
for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * a
theorem :: RMOD_4:2
theorem :: RMOD_4:3
theorem :: RMOD_4:4
:: deftheorem RMOD_4:def 1 :
canceled;
:: deftheorem RMOD_4:def 2 :
canceled;
:: deftheorem Def3 defines Sum RMOD_4:def 3 :
theorem Th5: :: RMOD_4:5
theorem :: RMOD_4:6
theorem :: RMOD_4:7
theorem :: RMOD_4:8
theorem Th9: :: RMOD_4:9
theorem Th10: :: RMOD_4:10
theorem :: RMOD_4:11
theorem Th12: :: RMOD_4:12
theorem Th13: :: RMOD_4:13
theorem :: RMOD_4:14
theorem :: RMOD_4:15
:: deftheorem Def4 defines Linear_Combination RMOD_4:def 4 :
:: deftheorem defines Carrier RMOD_4:def 5 :
theorem :: RMOD_4:16
canceled;
theorem :: RMOD_4:17
canceled;
theorem :: RMOD_4:18
canceled;
theorem :: RMOD_4:19
theorem :: RMOD_4:20
:: deftheorem Def6 defines ZeroLC RMOD_4:def 6 :
theorem :: RMOD_4:21
canceled;
theorem Th22: :: RMOD_4:22
:: deftheorem Def7 defines Linear_Combination RMOD_4:def 7 :
theorem :: RMOD_4:23
canceled;
theorem :: RMOD_4:24
canceled;
theorem Th25: :: RMOD_4:25
theorem Th26: :: RMOD_4:26
theorem Th27: :: RMOD_4:27
theorem :: RMOD_4:28
:: deftheorem Def8 defines (#) RMOD_4:def 8 :
theorem :: RMOD_4:29
canceled;
theorem :: RMOD_4:30
canceled;
theorem :: RMOD_4:31
canceled;
theorem Th32: :: RMOD_4:32
theorem :: RMOD_4:33
theorem Th34: :: RMOD_4:34
theorem Th35: :: RMOD_4:35
theorem :: RMOD_4:36
theorem Th37: :: RMOD_4:37
:: deftheorem Def9 defines Sum RMOD_4:def 9 :
Lm3:
for R being Ring
for V being RightMod of R holds Sum (ZeroLC V) = 0. V
theorem :: RMOD_4:38
canceled;
theorem :: RMOD_4:39
canceled;
theorem Th40: :: RMOD_4:40
theorem Th41: :: RMOD_4:41
theorem Th42: :: RMOD_4:42
theorem Th43: :: RMOD_4:43
theorem Th44: :: RMOD_4:44
theorem :: RMOD_4:45
theorem Th46: :: RMOD_4:46
theorem :: RMOD_4:47
:: deftheorem defines = RMOD_4:def 10 :
:: deftheorem Def11 defines + RMOD_4:def 11 :
theorem :: RMOD_4:48
canceled;
theorem :: RMOD_4:49
canceled;
theorem :: RMOD_4:50
canceled;
theorem Th51: :: RMOD_4:51
theorem Th52: :: RMOD_4:52
theorem Th53: :: RMOD_4:53
theorem :: RMOD_4:54
theorem :: RMOD_4:55
:: deftheorem Def12 defines * RMOD_4:def 12 :
theorem :: RMOD_4:56
canceled;
theorem :: RMOD_4:57
canceled;
theorem Th58: :: RMOD_4:58
theorem Th59: :: RMOD_4:59
theorem Th60: :: RMOD_4:60
theorem Th61: :: RMOD_4:61
theorem :: RMOD_4:62
theorem :: RMOD_4:63
theorem Th64: :: RMOD_4:64
theorem :: RMOD_4:65
:: deftheorem defines - RMOD_4:def 13 :
theorem :: RMOD_4:66
canceled;
theorem Th67: :: RMOD_4:67
theorem :: RMOD_4:68
theorem Th69: :: RMOD_4:69
theorem :: RMOD_4:70
:: deftheorem defines - RMOD_4:def 14 :
theorem :: RMOD_4:71
canceled;
theorem :: RMOD_4:72
canceled;
theorem Th73: :: RMOD_4:73
theorem :: RMOD_4:74
theorem :: RMOD_4:75
theorem :: RMOD_4:76
theorem Th77: :: RMOD_4:77
theorem Th78: :: RMOD_4:78
theorem Th79: :: RMOD_4:79
theorem :: RMOD_4:80
:: deftheorem Def1 defines linearly-independent RMOD_4:def 15 :
theorem :: RMOD_4:81
theorem Th3: :: RMOD_4:82
theorem :: RMOD_4:83
theorem Th5: :: RMOD_4:84
theorem :: RMOD_4:85
:: deftheorem Def2 defines Lin RMOD_4:def 16 :
theorem Th9: :: RMOD_4:86
theorem Th10: :: RMOD_4:87
theorem :: RMOD_4:88
theorem :: RMOD_4:89
theorem Th13: :: RMOD_4:90
theorem :: RMOD_4:91
theorem Th15: :: RMOD_4:92
theorem :: RMOD_4:93
theorem :: RMOD_4:94
theorem :: RMOD_4:95