:: Linear Combinations in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines vector RLVECT_2:def 1 :
theorem :: RLVECT_2:1
canceled;
theorem :: RLVECT_2:2
canceled;
theorem :: RLVECT_2:3
theorem Th4: :: RLVECT_2:4
theorem :: RLVECT_2:5
theorem Th6: :: RLVECT_2:6
theorem :: RLVECT_2:7
theorem Th8: :: RLVECT_2:8
theorem :: RLVECT_2:9
:: deftheorem RLVECT_2:def 2 :
canceled;
:: deftheorem RLVECT_2:def 3 :
canceled;
:: deftheorem Def4 defines Sum RLVECT_2:def 4 :
theorem :: RLVECT_2:10
canceled;
theorem :: RLVECT_2:11
canceled;
theorem :: RLVECT_2:12
canceled;
theorem :: RLVECT_2:13
canceled;
theorem Th14: :: RLVECT_2:14
theorem :: RLVECT_2:15
theorem :: RLVECT_2:16
theorem :: RLVECT_2:17
theorem Th18: :: RLVECT_2:18
theorem Th19: :: RLVECT_2:19
theorem :: RLVECT_2:20
theorem Th21: :: RLVECT_2:21
theorem Th22: :: RLVECT_2:22
theorem :: RLVECT_2:23
theorem :: RLVECT_2:24
:: deftheorem Def5 defines Linear_Combination RLVECT_2:def 5 :
:: deftheorem defines Carrier RLVECT_2:def 6 :
theorem :: RLVECT_2:25
canceled;
theorem :: RLVECT_2:26
canceled;
theorem :: RLVECT_2:27
canceled;
theorem :: RLVECT_2:28
:: deftheorem Def7 defines ZeroLC RLVECT_2:def 7 :
theorem :: RLVECT_2:29
canceled;
theorem Th30: :: RLVECT_2:30
:: deftheorem Def8 defines Linear_Combination RLVECT_2:def 8 :
theorem :: RLVECT_2:31
canceled;
theorem :: RLVECT_2:32
canceled;
theorem :: RLVECT_2:33
theorem Th34: :: RLVECT_2:34
theorem Th35: :: RLVECT_2:35
:: deftheorem Def9 defines (#) RLVECT_2:def 9 :
theorem :: RLVECT_2:36
canceled;
theorem :: RLVECT_2:37
canceled;
theorem :: RLVECT_2:38
canceled;
theorem :: RLVECT_2:39
canceled;
theorem Th40: :: RLVECT_2:40
theorem :: RLVECT_2:41
theorem Th42: :: RLVECT_2:42
theorem Th43: :: RLVECT_2:43
theorem :: RLVECT_2:44
:: deftheorem Def10 defines Sum RLVECT_2:def 10 :
Lm1:
for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V
theorem :: RLVECT_2:45
canceled;
theorem :: RLVECT_2:46
canceled;
theorem :: RLVECT_2:47
theorem :: RLVECT_2:48
theorem :: RLVECT_2:49
theorem Th50: :: RLVECT_2:50
theorem Th51: :: RLVECT_2:51
theorem :: RLVECT_2:52
theorem :: RLVECT_2:53
theorem :: RLVECT_2:54
:: deftheorem defines = RLVECT_2:def 11 :
:: deftheorem Def12 defines + RLVECT_2:def 12 :
theorem :: RLVECT_2:55
canceled;
theorem :: RLVECT_2:56
canceled;
theorem :: RLVECT_2:57
canceled;
theorem Th58: :: RLVECT_2:58
theorem Th59: :: RLVECT_2:59
theorem :: RLVECT_2:60
theorem Th61: :: RLVECT_2:61
theorem Th62: :: RLVECT_2:62
:: deftheorem Def13 defines * RLVECT_2:def 13 :
theorem :: RLVECT_2:63
canceled;
theorem :: RLVECT_2:64
canceled;
theorem Th65: :: RLVECT_2:65
theorem Th66: :: RLVECT_2:66
theorem Th67: :: RLVECT_2:67
theorem Th68: :: RLVECT_2:68
theorem Th69: :: RLVECT_2:69
theorem Th70: :: RLVECT_2:70
theorem Th71: :: RLVECT_2:71
:: deftheorem defines - RLVECT_2:def 14 :
theorem :: RLVECT_2:72
canceled;
theorem Th73: :: RLVECT_2:73
theorem :: RLVECT_2:74
theorem :: RLVECT_2:75
theorem :: RLVECT_2:76
theorem :: RLVECT_2:77
:: deftheorem defines - RLVECT_2:def 15 :
theorem :: RLVECT_2:78
canceled;
theorem Th79: :: RLVECT_2:79
theorem :: RLVECT_2:80
theorem :: RLVECT_2:81
theorem Th82: :: RLVECT_2:82
:: deftheorem Def16 defines LinComb RLVECT_2:def 16 :
:: deftheorem defines @ RLVECT_2:def 17 :
:: deftheorem defines @ RLVECT_2:def 18 :
:: deftheorem Def19 defines LCAdd RLVECT_2:def 19 :
definition
let V be
RealLinearSpace;
func LCMult V -> Function of
[:REAL ,(LinComb V):],
(LinComb V) means :
Def20:
:: RLVECT_2:def 20
for
a being
Real for
e being
Element of
LinComb V holds
it . [a,e] = a * (@ e);
existence
ex b1 being Function of [:REAL ,(LinComb V):],(LinComb V) st
for a being Real
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e)
uniqueness
for b1, b2 being Function of [:REAL ,(LinComb V):],(LinComb V) st ( for a being Real
for e being Element of LinComb V holds b1 . [a,e] = a * (@ e) ) & ( for a being Real
for e being Element of LinComb V holds b2 . [a,e] = a * (@ e) ) holds
b1 = b2
end;
:: deftheorem Def20 defines LCMult RLVECT_2:def 20 :
:: deftheorem defines LC_RLSpace RLVECT_2:def 21 :
theorem :: RLVECT_2:83
canceled;
theorem :: RLVECT_2:84
canceled;
theorem :: RLVECT_2:85
canceled;
theorem :: RLVECT_2:86
canceled;
theorem :: RLVECT_2:87
canceled;
theorem :: RLVECT_2:88
canceled;
theorem :: RLVECT_2:89
canceled;
theorem :: RLVECT_2:90
canceled;
theorem :: RLVECT_2:91
canceled;
theorem :: RLVECT_2:92
theorem :: RLVECT_2:93
theorem :: RLVECT_2:94
theorem :: RLVECT_2:95
theorem Th96: :: RLVECT_2:96
theorem Th97: :: RLVECT_2:97
theorem Th98: :: RLVECT_2:98
theorem :: RLVECT_2:99
:: deftheorem defines LC_RLSpace RLVECT_2:def 22 :