:: Linear Combinations in Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002 Association of Mizar Users
:: deftheorem Def1 defines Lin RUSUB_3:def 1 :
theorem Th1: :: RUSUB_3:1
theorem Th2: :: RUSUB_3:2
Lm1:
for V being RealUnitarySpace
for x being set holds
( x in (0). V iff x = 0. V )
theorem :: RUSUB_3:3
theorem :: RUSUB_3:4
theorem Th5: :: RUSUB_3:5
theorem :: RUSUB_3:6
Lm2:
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
Lm3:
for V being RealUnitarySpace
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
Lm4:
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
Lm5:
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
theorem Th7: :: RUSUB_3:7
theorem :: RUSUB_3:8
theorem :: RUSUB_3:9
theorem :: RUSUB_3:10
theorem Th11: :: RUSUB_3:11
theorem Th12: :: RUSUB_3:12
:: deftheorem Def2 defines Basis RUSUB_3:def 2 :
theorem :: RUSUB_3:13
theorem :: RUSUB_3:14
theorem Th15: :: RUSUB_3:15
theorem Th16: :: RUSUB_3:16
theorem :: RUSUB_3:17
theorem Th18: :: RUSUB_3:18
theorem Th19: :: RUSUB_3:19
theorem Th20: :: RUSUB_3:20
theorem Th21: :: RUSUB_3:21
theorem Th22: :: RUSUB_3:22
theorem :: RUSUB_3:23
theorem :: RUSUB_3:24
theorem Th25: :: RUSUB_3:25
Lm6:
for X, x being set st not x in X holds
X \ {x} = X
theorem :: RUSUB_3:26
theorem :: RUSUB_3:27
theorem :: RUSUB_3:28
theorem Th29: :: RUSUB_3:29
theorem :: RUSUB_3:30
theorem :: RUSUB_3:31
theorem Th32: :: RUSUB_3:32
theorem :: RUSUB_3:33
theorem :: RUSUB_3:34
theorem Th35: :: RUSUB_3:35
theorem :: RUSUB_3:36
theorem :: RUSUB_3:37
theorem :: RUSUB_3:38
theorem :: RUSUB_3:39
theorem :: RUSUB_3:40
theorem :: RUSUB_3:41
theorem :: RUSUB_3:42
theorem :: RUSUB_3:43
theorem :: RUSUB_3:44
theorem :: RUSUB_3:45