:: Subspaces and Cosets of Subspaces in Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for GF being non empty right_complementable associative commutative 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
for a, b being Element of GF
for v being Element of V holds (a - b) * v = (a * v) - (b * v)
:: deftheorem Def1 defines linearly-closed VECTSP_4:def 1 :
theorem :: VECTSP_4:1
canceled;
theorem :: VECTSP_4:2
canceled;
theorem :: VECTSP_4:3
canceled;
theorem Th4: :: VECTSP_4:4
theorem Th5: :: VECTSP_4:5
theorem :: VECTSP_4:6
theorem Th7: :: VECTSP_4:7
theorem :: VECTSP_4:8
theorem :: VECTSP_4:9
theorem :: VECTSP_4:10
:: deftheorem Def2 defines Subspace VECTSP_4:def 2 :
theorem :: VECTSP_4:11
canceled;
theorem :: VECTSP_4:12
canceled;
theorem :: VECTSP_4:13
canceled;
theorem :: VECTSP_4:14
canceled;
theorem :: VECTSP_4:15
canceled;
theorem :: VECTSP_4:16
theorem Th17: :: VECTSP_4:17
theorem Th18: :: VECTSP_4:18
theorem :: VECTSP_4:19
theorem :: VECTSP_4:20
theorem Th21: :: VECTSP_4:21
theorem Th22: :: VECTSP_4:22
theorem Th23: :: VECTSP_4:23
theorem Th24: :: VECTSP_4:24
Lm2:
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
for W being Subspace of V
for V1 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed
theorem Th25: :: VECTSP_4:25
theorem :: VECTSP_4:26
theorem :: VECTSP_4:27
theorem Th28: :: VECTSP_4:28
theorem Th29: :: VECTSP_4:29
theorem Th30: :: VECTSP_4:30
theorem Th31: :: VECTSP_4:31
theorem Th32: :: VECTSP_4:32
theorem Th33: :: VECTSP_4:33
theorem Th34: :: VECTSP_4:34
theorem Th35: :: VECTSP_4:35
theorem :: VECTSP_4:36
theorem Th37: :: VECTSP_4:37
theorem Th38: :: VECTSP_4:38
theorem :: VECTSP_4:39
theorem :: VECTSP_4:40
theorem :: VECTSP_4:41
theorem Th42: :: VECTSP_4:42
:: deftheorem Def3 defines (0). VECTSP_4:def 3 :
:: deftheorem defines (Omega). VECTSP_4:def 4 :
theorem :: VECTSP_4:43
canceled;
theorem :: VECTSP_4:44
canceled;
theorem :: VECTSP_4:45
canceled;
theorem :: VECTSP_4:46
theorem Th47: :: VECTSP_4:47
theorem Th48: :: VECTSP_4:48
theorem :: VECTSP_4:49
theorem :: VECTSP_4:50
theorem :: VECTSP_4:51
theorem :: VECTSP_4:52
canceled;
theorem :: VECTSP_4:53
:: deftheorem defines + VECTSP_4:def 5 :
Lm3:
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
for W being Subspace of V holds (0. V) + W = the carrier of W
:: deftheorem Def6 defines Coset VECTSP_4:def 6 :
theorem :: VECTSP_4:54
canceled;
theorem :: VECTSP_4:55
canceled;
theorem :: VECTSP_4:56
canceled;
theorem Th57: :: VECTSP_4:57
theorem Th58: :: VECTSP_4:58
theorem Th59: :: VECTSP_4:59
theorem :: VECTSP_4:60
theorem Th61: :: VECTSP_4:61
Lm4:
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
for v being Element of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
theorem Th62: :: VECTSP_4:62
theorem Th63: :: VECTSP_4:63
theorem :: VECTSP_4:64
theorem Th65: :: VECTSP_4:65
theorem Th66: :: VECTSP_4:66
theorem :: VECTSP_4:67
theorem Th68: :: VECTSP_4:68
theorem :: VECTSP_4:69
theorem Th70: :: VECTSP_4:70
theorem Th71: :: VECTSP_4:71
theorem :: VECTSP_4:72
theorem Th73: :: VECTSP_4:73
theorem :: VECTSP_4:74
theorem Th75: :: VECTSP_4:75
theorem :: VECTSP_4:76
theorem :: VECTSP_4:77
canceled;
theorem :: VECTSP_4:78
theorem Th79: :: VECTSP_4:79
theorem Th80: :: VECTSP_4:80
theorem Th81: :: VECTSP_4:81
theorem Th82: :: VECTSP_4:82
theorem Th83: :: VECTSP_4:83
theorem :: VECTSP_4:84
theorem :: VECTSP_4:85
theorem :: VECTSP_4:86
theorem :: VECTSP_4:87
theorem :: VECTSP_4:88
theorem :: VECTSP_4:89
theorem :: VECTSP_4:90
theorem :: VECTSP_4:91
theorem :: VECTSP_4:92
theorem Th93: :: VECTSP_4:93
theorem :: VECTSP_4:94
theorem :: VECTSP_4:95
theorem :: VECTSP_4:96
theorem :: VECTSP_4:97
theorem :: VECTSP_4:98
canceled;
theorem :: VECTSP_4:99
canceled;
theorem :: VECTSP_4:100
canceled;
theorem :: VECTSP_4:101
canceled;
theorem :: VECTSP_4:102
canceled;
theorem :: VECTSP_4:103