:: Basis of Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received July 10, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for V being RealLinearSpace
for F, G being FinSequence of the carrier of V
for f being Function of the carrier of V, REAL holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
theorem Th1: :: RLVECT_3:1
theorem Th2: :: RLVECT_3:2
theorem Th3: :: RLVECT_3:3
theorem Th4: :: RLVECT_3:4
:: deftheorem Def1 defines linearly-independent RLVECT_3:def 1 :
theorem :: RLVECT_3:5
canceled;
theorem :: RLVECT_3:6
theorem Th7: :: RLVECT_3:7
theorem Th8: :: RLVECT_3:8
theorem Th9: :: RLVECT_3:9
theorem :: RLVECT_3:10
theorem Th11: :: RLVECT_3:11
theorem :: RLVECT_3:12
theorem Th13: :: RLVECT_3:13
theorem :: RLVECT_3:14
:: deftheorem Def2 defines Lin RLVECT_3:def 2 :
theorem :: RLVECT_3:15
canceled;
theorem :: RLVECT_3:16
canceled;
theorem Th17: :: RLVECT_3:17
theorem Th18: :: RLVECT_3:18
Lm2:
for x being set
for V being RealLinearSpace holds
( x in (0). V iff x = 0. V )
theorem :: RLVECT_3:19
theorem :: RLVECT_3:20
theorem Th21: :: RLVECT_3:21
theorem :: RLVECT_3:22
Lm3:
for V being RealLinearSpace
for W1, W3, W2 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
Lm4:
for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds
W1 is Subspace of W2 /\ W3
Lm5:
for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
Lm6:
for V being RealLinearSpace
for W1, W3, W2 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
theorem Th23: :: RLVECT_3:23
theorem :: RLVECT_3:24
theorem :: RLVECT_3:25
theorem :: RLVECT_3:26
Lm7:
for M being non empty set
for CF being Choice_Function of M st not {} in M holds
dom CF = M
theorem Th27: :: RLVECT_3:27
theorem Th28: :: RLVECT_3:28
:: deftheorem Def3 defines Basis RLVECT_3:def 3 :
theorem :: RLVECT_3:29
canceled;
theorem :: RLVECT_3:30
canceled;
theorem :: RLVECT_3:31
canceled;
theorem :: RLVECT_3:32
theorem :: RLVECT_3:33
theorem :: RLVECT_3:34
canceled;
theorem :: RLVECT_3:35
theorem :: RLVECT_3:36
theorem :: RLVECT_3:37
theorem :: RLVECT_3:38
theorem :: RLVECT_3:39
theorem :: RLVECT_3:40
theorem :: RLVECT_3:41