:: VECTSP_6 semantic presentation
:: deftheorem Def1 VECTSP_6:def 1 :
canceled;
:: deftheorem Def2 VECTSP_6:def 2 :
canceled;
:: deftheorem Def3 VECTSP_6:def 3 :
canceled;
:: deftheorem Def4 defines Linear_Combination VECTSP_6:def 4 :
:: deftheorem Def5 defines Carrier VECTSP_6:def 5 :
theorem Th1: :: VECTSP_6:1
canceled;
theorem Th2: :: VECTSP_6:2
canceled;
theorem Th3: :: VECTSP_6:3
canceled;
theorem Th4: :: VECTSP_6:4
canceled;
theorem Th5: :: VECTSP_6:5
canceled;
theorem Th6: :: VECTSP_6:6
canceled;
theorem Th7: :: VECTSP_6:7
canceled;
theorem Th8: :: VECTSP_6:8
canceled;
theorem Th9: :: VECTSP_6:9
canceled;
theorem Th10: :: VECTSP_6:10
canceled;
theorem Th11: :: VECTSP_6:11
canceled;
theorem Th12: :: VECTSP_6:12
canceled;
theorem Th13: :: VECTSP_6:13
canceled;
theorem Th14: :: VECTSP_6:14
canceled;
theorem Th15: :: VECTSP_6:15
canceled;
theorem Th16: :: VECTSP_6:16
canceled;
theorem Th17: :: VECTSP_6:17
canceled;
theorem Th18: :: VECTSP_6:18
canceled;
theorem Th19: :: VECTSP_6:19
theorem Th20: :: VECTSP_6:20
:: deftheorem Def6 defines ZeroLC VECTSP_6:def 6 :
theorem Th21: :: VECTSP_6:21
canceled;
theorem Th22: :: VECTSP_6:22
:: deftheorem Def7 defines Linear_Combination VECTSP_6:def 7 :
theorem Th23: :: VECTSP_6:23
canceled;
theorem Th24: :: VECTSP_6:24
canceled;
theorem Th25: :: VECTSP_6:25
theorem Th26: :: VECTSP_6:26
theorem Th27: :: VECTSP_6:27
theorem Th28: :: VECTSP_6:28
:: deftheorem Def8 defines (#) VECTSP_6:def 8 :
theorem Th29: :: VECTSP_6:29
canceled;
theorem Th30: :: VECTSP_6:30
canceled;
theorem Th31: :: VECTSP_6:31
canceled;
theorem Th32: :: VECTSP_6:32
theorem Th33: :: VECTSP_6:33
theorem Th34: :: VECTSP_6:34
theorem Th35: :: VECTSP_6:35
theorem Th36: :: VECTSP_6:36
theorem Th37: :: VECTSP_6:37
:: deftheorem Def9 defines Sum VECTSP_6:def 9 :
Lemma13:
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1 holds Sum (ZeroLC b2) = 0. b2
theorem Th38: :: VECTSP_6:38
canceled;
theorem Th39: :: VECTSP_6:39
canceled;
theorem Th40: :: VECTSP_6:40
theorem Th41: :: VECTSP_6:41
theorem Th42: :: VECTSP_6:42
theorem Th43: :: VECTSP_6:43
theorem Th44: :: VECTSP_6:44
theorem Th45: :: VECTSP_6:45
theorem Th46: :: VECTSP_6:46
theorem Th47: :: VECTSP_6:47
:: deftheorem Def10 defines = VECTSP_6:def 10 :
:: deftheorem Def11 defines + VECTSP_6:def 11 :
theorem Th48: :: VECTSP_6:48
canceled;
theorem Th49: :: VECTSP_6:49
canceled;
theorem Th50: :: VECTSP_6:50
canceled;
theorem Th51: :: VECTSP_6:51
theorem Th52: :: VECTSP_6:52
theorem Th53: :: VECTSP_6:53
theorem Th54: :: VECTSP_6:54
theorem Th55: :: VECTSP_6:55
:: deftheorem Def12 defines * VECTSP_6:def 12 :
theorem Th56: :: VECTSP_6:56
canceled;
theorem Th57: :: 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 Th62: :: VECTSP_6:62
theorem Th63: :: VECTSP_6:63
theorem Th64: :: VECTSP_6:64
theorem Th65: :: VECTSP_6:65
:: deftheorem Def13 defines - VECTSP_6:def 13 :
Lemma26:
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being Element of b1 holds (- (1. b1)) * b2 = - b2
theorem Th66: :: VECTSP_6:66
canceled;
theorem Th67: :: VECTSP_6:67
theorem Th68: :: VECTSP_6:68
Lemma28:
for b1 being Field holds - (1. b1) <> 0. b1
Lemma29:
for b1 being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b2 being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b1
for b3 being Linear_Combination of b2 holds Carrier (- b3) c= Carrier b3
by Th58;
theorem Th69: :: VECTSP_6:69
theorem Th70: :: VECTSP_6:70
:: deftheorem Def14 defines - VECTSP_6:def 14 :
theorem Th71: :: VECTSP_6:71
canceled;
theorem Th72: :: VECTSP_6:72
canceled;
theorem Th73: :: VECTSP_6:73
theorem Th74: :: VECTSP_6:74
theorem Th75: :: VECTSP_6:75
theorem Th76: :: VECTSP_6:76
theorem Th77: :: VECTSP_6:77
theorem Th78: :: VECTSP_6:78
theorem Th79: :: VECTSP_6:79
theorem Th80: :: VECTSP_6:80
theorem Th81: :: VECTSP_6:81
theorem Th82: :: VECTSP_6:82