:: Vectors in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received July 24, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem :: RLVECT_1:1
canceled;
theorem :: RLVECT_1:2
canceled;
theorem :: RLVECT_1:3
:: deftheorem RLVECT_1:def 1 :
canceled;
:: deftheorem RLVECT_1:def 2 :
canceled;
:: deftheorem RLVECT_1:def 3 :
canceled;
:: deftheorem defines * RLVECT_1:def 4 :
theorem :: RLVECT_1:4
canceled;
theorem :: RLVECT_1:5
:: deftheorem Def5 defines Abelian RLVECT_1:def 5 :
:: deftheorem Def6 defines add-associative RLVECT_1:def 6 :
:: deftheorem Def7 defines right_zeroed RLVECT_1:def 7 :
:: deftheorem RLVECT_1:def 8 :
canceled;
:: deftheorem Def9 defines RealLinearSpace-like RLVECT_1:def 9 :
:: deftheorem defines Trivial-RLSStruct RLVECT_1:def 10 :
theorem :: RLVECT_1:6
canceled;
theorem :: RLVECT_1:7
canceled;
Lm1:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V st v + w = 0. V holds
w + v = 0. V
theorem :: RLVECT_1:8
canceled;
theorem Th9: :: RLVECT_1:9
theorem Th10: :: RLVECT_1:10
:: deftheorem Def11 defines - RLVECT_1:def 11 :
Lm2:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, u being Element of V ex w being Element of V st v + w = u
:: deftheorem defines - RLVECT_1:def 12 :
theorem :: RLVECT_1:11
canceled;
theorem :: RLVECT_1:12
canceled;
theorem :: RLVECT_1:13
canceled;
theorem :: RLVECT_1:14
canceled;
theorem :: RLVECT_1:15
canceled;
theorem Th16: :: RLVECT_1:16
theorem :: RLVECT_1:17
canceled;
theorem :: RLVECT_1:18
canceled;
theorem Th19: :: RLVECT_1:19
theorem :: RLVECT_1:20
theorem Th21: :: RLVECT_1:21
theorem :: RLVECT_1:22
theorem Th23: :: RLVECT_1:23
theorem Th24: :: RLVECT_1:24
theorem Th25: :: RLVECT_1:25
theorem :: RLVECT_1:26
theorem :: RLVECT_1:27
theorem :: RLVECT_1:28
theorem Th29: :: RLVECT_1:29
theorem Th30: :: RLVECT_1:30
theorem Th31: :: RLVECT_1:31
theorem :: RLVECT_1:32
canceled;
theorem Th33: :: RLVECT_1:33
theorem :: RLVECT_1:34
theorem Th35: :: RLVECT_1:35
theorem :: RLVECT_1:36
theorem :: RLVECT_1:37
theorem Th38: :: RLVECT_1:38
theorem Th39: :: RLVECT_1:39
theorem :: RLVECT_1:40
Lm3:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, w being Element of V holds - (u + w) = (- w) + (- u)
theorem Th41: :: RLVECT_1:41
theorem :: RLVECT_1:42
theorem :: RLVECT_1:43
theorem Th44: :: RLVECT_1:44
theorem :: RLVECT_1:45
theorem :: RLVECT_1:46
theorem :: RLVECT_1:47
theorem Th48: :: RLVECT_1:48
theorem Th49: :: RLVECT_1:49
theorem :: RLVECT_1:50
theorem :: RLVECT_1:51
:: deftheorem Def13 defines Sum RLVECT_1:def 13 :
Lm4:
for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V
Lm5:
for V being non empty addLoopStr
for F being FinSequence of the carrier of V st len F = 0 holds
Sum F = 0. V
theorem :: RLVECT_1:52
canceled;
theorem :: RLVECT_1:53
canceled;
theorem Th54: :: RLVECT_1:54
theorem Th55: :: RLVECT_1:55
theorem :: RLVECT_1:56
theorem :: RLVECT_1:57
theorem Th58: :: RLVECT_1:58
Lm6:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds Sum <*v*> = v
theorem :: RLVECT_1:59
theorem :: RLVECT_1:60
theorem :: RLVECT_1:61
theorem Th62: :: RLVECT_1:62
theorem Th63: :: RLVECT_1:63
theorem :: RLVECT_1:64
theorem :: RLVECT_1:65
canceled;
theorem :: RLVECT_1:66
theorem :: RLVECT_1:67
theorem :: RLVECT_1:68
theorem :: RLVECT_1:69
theorem :: RLVECT_1:70
theorem :: RLVECT_1:71
theorem :: RLVECT_1:72
theorem :: RLVECT_1:73
theorem :: RLVECT_1:74
theorem :: RLVECT_1:75
theorem :: RLVECT_1:76
theorem :: RLVECT_1:77
theorem Th78: :: RLVECT_1:78
theorem Th79: :: RLVECT_1:79
theorem :: RLVECT_1:80
theorem :: RLVECT_1:81
theorem :: RLVECT_1:82
theorem :: RLVECT_1:83
theorem Th84: :: RLVECT_1:84
theorem Th85: :: RLVECT_1:85
theorem Th86: :: RLVECT_1:86
theorem Th87: :: RLVECT_1:87
theorem :: RLVECT_1:88
canceled;
theorem :: RLVECT_1:89
theorem :: RLVECT_1:90
theorem :: RLVECT_1:91
theorem :: RLVECT_1:92
theorem :: RLVECT_1:93
theorem :: RLVECT_1:94
theorem :: RLVECT_1:95
theorem :: RLVECT_1:96
theorem :: RLVECT_1:97
:: deftheorem RLVECT_1:def 14 :
canceled;
:: deftheorem Def15 defines zeroed RLVECT_1:def 15 :