:: Linear Combinations in Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem VECTSP_6:def 1 :
canceled;
:: deftheorem VECTSP_6:def 2 :
canceled;
:: deftheorem VECTSP_6:def 3 :
canceled;
:: deftheorem Def4 defines Linear_Combination VECTSP_6:def 4 :
:: deftheorem defines Carrier VECTSP_6:def 5 :
theorem :: VECTSP_6:1
canceled;
theorem :: VECTSP_6:2
canceled;
theorem :: VECTSP_6:3
canceled;
theorem :: VECTSP_6:4
canceled;
theorem :: VECTSP_6:5
canceled;
theorem :: VECTSP_6:6
canceled;
theorem :: VECTSP_6:7
canceled;
theorem :: VECTSP_6:8
canceled;
theorem :: VECTSP_6:9
canceled;
theorem :: VECTSP_6:10
canceled;
theorem :: VECTSP_6:11
canceled;
theorem :: VECTSP_6:12
canceled;
theorem :: VECTSP_6:13
canceled;
theorem :: VECTSP_6:14
canceled;
theorem :: VECTSP_6:15
canceled;
theorem :: VECTSP_6:16
canceled;
theorem :: VECTSP_6:17
canceled;
theorem :: VECTSP_6:18
canceled;
theorem :: VECTSP_6:19
theorem :: VECTSP_6:20
:: deftheorem Def6 defines ZeroLC VECTSP_6:def 6 :
theorem :: VECTSP_6:21
canceled;
theorem Th22: :: VECTSP_6:22
:: deftheorem Def7 defines Linear_Combination VECTSP_6:def 7 :
theorem :: VECTSP_6:23
canceled;
theorem :: VECTSP_6:24
canceled;
theorem :: VECTSP_6:25
theorem Th26: :: VECTSP_6:26
theorem Th27: :: VECTSP_6:27
theorem :: VECTSP_6:28
:: deftheorem Def8 defines (#) VECTSP_6:def 8 :
theorem :: VECTSP_6:29
canceled;
theorem :: VECTSP_6:30
canceled;
theorem :: VECTSP_6:31
canceled;
theorem Th32: :: VECTSP_6:32
theorem :: VECTSP_6:33
theorem Th34: :: VECTSP_6:34
theorem Th35: :: VECTSP_6:35
theorem :: VECTSP_6:36
theorem Th37: :: VECTSP_6:37
:: deftheorem Def9 defines Sum VECTSP_6:def 9 :
Lm1:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF holds Sum (ZeroLC V) = 0. V
theorem :: VECTSP_6:38
canceled;
theorem :: VECTSP_6:39
canceled;
theorem :: VECTSP_6:40
theorem :: VECTSP_6:41
theorem :: VECTSP_6:42
theorem Th43: :: VECTSP_6:43
theorem Th44: :: VECTSP_6:44
theorem :: VECTSP_6:45
theorem :: VECTSP_6:46
theorem :: VECTSP_6:47
:: deftheorem defines = VECTSP_6:def 10 :
:: deftheorem Def11 defines + VECTSP_6:def 11 :
theorem :: VECTSP_6:48
canceled;
theorem :: VECTSP_6:49
canceled;
theorem :: VECTSP_6:50
canceled;
theorem Th51: :: VECTSP_6:51
theorem Th52: :: VECTSP_6:52
theorem Th53: :: VECTSP_6:53
theorem :: VECTSP_6:54
theorem :: VECTSP_6:55
:: deftheorem Def12 defines * VECTSP_6:def 12 :
theorem :: VECTSP_6:56
canceled;
theorem :: VECTSP_6:57
canceled;
theorem Th58: :: VECTSP_6:58
theorem Th59: :: VECTSP_6:59
theorem Th60: :: VECTSP_6:60
theorem Th61: :: VECTSP_6:61
theorem :: VECTSP_6:62
theorem :: VECTSP_6:63
theorem Th64: :: VECTSP_6:64
theorem :: VECTSP_6:65
:: deftheorem defines - VECTSP_6:def 13 :
Lm2:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of GF holds (- (1. GF)) * a = - a
theorem :: VECTSP_6:66
canceled;
theorem Th67: :: VECTSP_6:67
theorem :: VECTSP_6:68
Lm3:
for GF being Field holds - (1. GF) <> 0. GF
theorem Th69: :: VECTSP_6:69
theorem :: VECTSP_6:70
:: deftheorem defines - VECTSP_6:def 14 :
theorem :: VECTSP_6:71
canceled;
theorem :: VECTSP_6:72
canceled;
theorem Th73: :: VECTSP_6:73
theorem :: VECTSP_6:74
theorem :: VECTSP_6:75
theorem Th76: :: VECTSP_6:76
theorem Th77: :: VECTSP_6:77
theorem :: VECTSP_6:78
theorem Th79: :: VECTSP_6:79
theorem :: VECTSP_6:80
theorem :: VECTSP_6:81
theorem :: VECTSP_6:82