:: The Rank+Nullity Theorem
:: by Jesse Alama
::
:: Received July 31, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: RANKNULL:1
theorem Th2: :: RANKNULL:2
theorem Th3: :: RANKNULL:3
theorem Th4: :: RANKNULL:4
theorem :: RANKNULL:5
theorem :: RANKNULL:6
theorem Th7: :: RANKNULL:7
theorem Th8: :: RANKNULL:8
theorem Th9: :: RANKNULL:9
:: deftheorem Def1 defines ker RANKNULL:def 1 :
theorem Th10: :: RANKNULL:10
:: deftheorem Def2 defines im RANKNULL:def 2 :
theorem :: RANKNULL:11
theorem Th12: :: RANKNULL:12
theorem Th13: :: RANKNULL:13
theorem :: RANKNULL:14
theorem Th15: :: RANKNULL:15
theorem Th16: :: RANKNULL:16
theorem Th17: :: RANKNULL:17
theorem Th18: :: RANKNULL:18
theorem Th19: :: RANKNULL:19
theorem Th20: :: RANKNULL:20
theorem Th21: :: RANKNULL:21
theorem Th22: :: RANKNULL:22
theorem :: RANKNULL:23
:: deftheorem defines \ RANKNULL:def 3 :
:: deftheorem defines ! RANKNULL:def 4 :
theorem Th24: :: RANKNULL:24
Lm1:
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
theorem Th25: :: RANKNULL:25
theorem Th26: :: RANKNULL:26
theorem Th27: :: RANKNULL:27
theorem Th28: :: RANKNULL:28
:: deftheorem Def5 defines @ RANKNULL:def 5 :
theorem Th29: :: RANKNULL:29
theorem Th30: :: RANKNULL:30
theorem Th31: :: RANKNULL:31
theorem Th32: :: RANKNULL:32
theorem Th33: :: RANKNULL:33
theorem Th34: :: RANKNULL:34
theorem Th35: :: RANKNULL:35
theorem Th36: :: RANKNULL:36
theorem Th37: :: RANKNULL:37
theorem Th38: :: RANKNULL:38
theorem Th39: :: RANKNULL:39
theorem Th40: :: RANKNULL:40
theorem Th41: :: RANKNULL:41
:: deftheorem Def6 defines # RANKNULL:def 6 :
theorem Th42: :: RANKNULL:42
theorem Th43: :: RANKNULL:43
:: deftheorem defines rank RANKNULL:def 7 :
:: deftheorem defines nullity RANKNULL:def 8 :
theorem Th44: :: RANKNULL:44
theorem :: RANKNULL:45