:: RLVECT_3 semantic presentation
begin
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)
proof
let V be RealLinearSpace; ::_thesis: 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)
let F, G be FinSequence of the carrier of V; ::_thesis: for f being Function of the carrier of V,REAL holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let f be Function of the carrier of V,REAL; ::_thesis: f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
set H = (f (#) F) ^ (f (#) G);
set I = F ^ G;
A1: len ((f (#) F) ^ (f (#) G)) = (len (f (#) F)) + (len (f (#) G)) by FINSEQ_1:22
.= (len F) + (len (f (#) G)) by RLVECT_2:def_7
.= (len F) + (len G) by RLVECT_2:def_7
.= len (F ^ G) by FINSEQ_1:22 ;
A2: len F = len (f (#) F) by RLVECT_2:def_7;
A3: len G = len (f (#) G) by RLVECT_2:def_7;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_((f_(#)_F)_^_(f_(#)_G))_holds_
((f_(#)_F)_^_(f_(#)_G))_._k_=_(f_._((F_^_G)_/._k))_*_((F_^_G)_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom ((f (#) F) ^ (f (#) G)) implies ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) )
assume A4: k in dom ((f (#) F) ^ (f (#) G)) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)
now__::_thesis:_((f_(#)_F)_^_(f_(#)_G))_._k_=_(f_._((F_^_G)_/._k))_*_((F_^_G)_/._k)
percases ( k in dom (f (#) F) or ex n being Nat st
( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ) by A4, FINSEQ_1:25;
supposeA5: k in dom (f (#) F) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)
then A6: k in dom F by A2, FINSEQ_3:29;
then A7: k in dom (F ^ G) by FINSEQ_3:22;
A8: F /. k = F . k by A6, PARTFUN1:def_6
.= (F ^ G) . k by A6, FINSEQ_1:def_7
.= (F ^ G) /. k by A7, PARTFUN1:def_6 ;
thus ((f (#) F) ^ (f (#) G)) . k = (f (#) F) . k by A5, FINSEQ_1:def_7
.= (f . ((F ^ G) /. k)) * ((F ^ G) /. k) by A5, A8, RLVECT_2:def_7 ; ::_thesis: verum
end;
supposeA9: ex n being Nat st
( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ; ::_thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)
A10: k in dom (F ^ G) by A1, A4, FINSEQ_3:29;
consider n being Nat such that
A11: n in dom (f (#) G) and
A12: k = (len (f (#) F)) + n by A9;
A13: n in dom G by A3, A11, FINSEQ_3:29;
then A14: G /. n = G . n by PARTFUN1:def_6
.= (F ^ G) . k by A2, A12, A13, FINSEQ_1:def_7
.= (F ^ G) /. k by A10, PARTFUN1:def_6 ;
A15: n in NAT by ORDINAL1:def_12;
thus ((f (#) F) ^ (f (#) G)) . k = (f (#) G) . n by A11, A12, FINSEQ_1:def_7
.= (f . ((F ^ G) /. k)) * ((F ^ G) /. k) by A11, A15, A14, RLVECT_2:def_7 ; ::_thesis: verum
end;
end;
end;
hence ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) ; ::_thesis: verum
end;
hence f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by A1, RLVECT_2:def_7; ::_thesis: verum
end;
theorem Th1: :: RLVECT_3:1
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
proof
let V be RealLinearSpace; ::_thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
let L1, L2 be Linear_Combination of V; ::_thesis: Sum (L1 + L2) = (Sum L1) + (Sum L2)
consider F being FinSequence of the carrier of V such that
A1: F is one-to-one and
A2: rng F = Carrier (L1 + L2) and
A3: Sum ((L1 + L2) (#) F) = Sum (L1 + L2) by RLVECT_2:def_8;
set A = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2);
set C3 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2));
consider r being FinSequence such that
A4: rng r = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) and
A5: r is one-to-one by FINSEQ_4:58;
reconsider r = r as FinSequence of the carrier of V by A4, FINSEQ_1:def_4;
set FF = F ^ r;
A6: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier (L1 + L2)) \/ ((Carrier L1) \/ (Carrier L2)) by XBOOLE_1:4;
rng F misses rng r
proof
set x = the Element of (rng F) /\ (rng r);
assume not rng F misses rng r ; ::_thesis: contradiction
then (rng F) /\ (rng r) <> {} by XBOOLE_0:def_7;
then ( the Element of (rng F) /\ (rng r) in Carrier (L1 + L2) & the Element of (rng F) /\ (rng r) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) ) by A2, A4, XBOOLE_0:def_4;
hence contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
then A7: F ^ r is one-to-one by A1, A5, FINSEQ_3:91;
A8: len r = len ((L1 + L2) (#) r) by RLVECT_2:def_7;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_r_holds_
((L1_+_L2)_(#)_r)_._k_=_0_*_(r_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom r implies ((L1 + L2) (#) r) . k = 0 * (r /. k) )
assume A9: k in dom r ; ::_thesis: ((L1 + L2) (#) r) . k = 0 * (r /. k)
then r /. k = r . k by PARTFUN1:def_6;
then r /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) by A4, A9, FUNCT_1:def_3;
then A10: not r /. k in Carrier (L1 + L2) by XBOOLE_0:def_5;
k in dom ((L1 + L2) (#) r) by A8, A9, FINSEQ_3:29;
then ((L1 + L2) (#) r) . k = ((L1 + L2) . (r /. k)) * (r /. k) by RLVECT_2:def_7;
hence ((L1 + L2) (#) r) . k = 0 * (r /. k) by A10; ::_thesis: verum
end;
then A11: Sum ((L1 + L2) (#) r) = 0 * (Sum r) by A8, RLVECT_2:3
.= 0. V by RLVECT_1:10 ;
set f = (L1 + L2) (#) (F ^ r);
set C1 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1);
consider G being FinSequence of the carrier of V such that
A12: G is one-to-one and
A13: rng G = Carrier L1 and
A14: Sum (L1 (#) G) = Sum L1 by RLVECT_2:def_8;
consider p being FinSequence such that
A15: rng p = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) and
A16: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of the carrier of V by A15, FINSEQ_1:def_4;
set GG = G ^ p;
A17: Sum ((L1 + L2) (#) (F ^ r)) = Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Lm1
.= (Sum ((L1 + L2) (#) F)) + (0. V) by A11, RLVECT_1:41
.= Sum ((L1 + L2) (#) F) by RLVECT_1:4 ;
set C2 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2);
consider H being FinSequence of the carrier of V such that
A18: H is one-to-one and
A19: rng H = Carrier L2 and
A20: Sum (L2 (#) H) = Sum L2 by RLVECT_2:def_8;
consider q being FinSequence such that
A21: rng q = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) and
A22: q is one-to-one by FINSEQ_4:58;
reconsider q = q as FinSequence of the carrier of V by A21, FINSEQ_1:def_4;
set HH = H ^ q;
rng H misses rng q
proof
set x = the Element of (rng H) /\ (rng q);
assume not rng H misses rng q ; ::_thesis: contradiction
then (rng H) /\ (rng q) <> {} by XBOOLE_0:def_7;
then ( the Element of (rng H) /\ (rng q) in Carrier L2 & the Element of (rng H) /\ (rng q) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) ) by A19, A21, XBOOLE_0:def_4;
hence contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
then A23: H ^ q is one-to-one by A18, A22, FINSEQ_3:91;
set h = L2 (#) (H ^ q);
A24: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier L1) \/ ((Carrier (L1 + L2)) \/ (Carrier L2)) by XBOOLE_1:4;
rng (G ^ p) = (rng G) \/ (rng p) by FINSEQ_1:31;
then rng (G ^ p) = (Carrier L1) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A13, A15, XBOOLE_1:39;
then A25: rng (G ^ p) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A24, XBOOLE_1:7, XBOOLE_1:12;
A26: len q = len (L2 (#) q) by RLVECT_2:def_7;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_q_holds_
(L2_(#)_q)_._k_=_0_*_(q_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom q implies (L2 (#) q) . k = 0 * (q /. k) )
assume A27: k in dom q ; ::_thesis: (L2 (#) q) . k = 0 * (q /. k)
then q /. k = q . k by PARTFUN1:def_6;
then q /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) by A21, A27, FUNCT_1:def_3;
then A28: not q /. k in Carrier L2 by XBOOLE_0:def_5;
k in dom (L2 (#) q) by A26, A27, FINSEQ_3:29;
then (L2 (#) q) . k = (L2 . (q /. k)) * (q /. k) by RLVECT_2:def_7;
hence (L2 (#) q) . k = 0 * (q /. k) by A28; ::_thesis: verum
end;
then A29: Sum (L2 (#) q) = 0 * (Sum q) by A26, RLVECT_2:3
.= 0. V by RLVECT_1:10 ;
A30: Sum (L2 (#) (H ^ q)) = Sum ((L2 (#) H) ^ (L2 (#) q)) by Lm1
.= (Sum (L2 (#) H)) + (0. V) by A29, RLVECT_1:41
.= Sum (L2 (#) H) by RLVECT_1:4 ;
deffunc H1( Nat) -> set = (F ^ r) <- ((G ^ p) . $1);
set g = L1 (#) (G ^ p);
consider P being FinSequence such that
A31: len P = len (F ^ r) and
A32: for k being Nat st k in dom P holds
P . k = H1(k) from FINSEQ_1:sch_2();
A33: dom P = Seg (len (F ^ r)) by A31, FINSEQ_1:def_3;
A34: len p = len (L1 (#) p) by RLVECT_2:def_7;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_
(L1_(#)_p)_._k_=_0_*_(p_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom p implies (L1 (#) p) . k = 0 * (p /. k) )
assume A35: k in dom p ; ::_thesis: (L1 (#) p) . k = 0 * (p /. k)
then p /. k = p . k by PARTFUN1:def_6;
then p /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) by A15, A35, FUNCT_1:def_3;
then A36: not p /. k in Carrier L1 by XBOOLE_0:def_5;
k in dom (L1 (#) p) by A34, A35, FINSEQ_3:29;
then (L1 (#) p) . k = (L1 . (p /. k)) * (p /. k) by RLVECT_2:def_7;
hence (L1 (#) p) . k = 0 * (p /. k) by A36; ::_thesis: verum
end;
then A37: Sum (L1 (#) p) = 0 * (Sum p) by A34, RLVECT_2:3
.= 0. V by RLVECT_1:10 ;
A38: Sum (L1 (#) (G ^ p)) = Sum ((L1 (#) G) ^ (L1 (#) p)) by Lm1
.= (Sum (L1 (#) G)) + (0. V) by A37, RLVECT_1:41
.= Sum (L1 (#) G) by RLVECT_1:4 ;
rng (F ^ r) = (rng F) \/ (rng r) by FINSEQ_1:31;
then rng (F ^ r) = (Carrier (L1 + L2)) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A2, A4, XBOOLE_1:39;
then A39: rng (F ^ r) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A6, XBOOLE_1:7, XBOOLE_1:12;
rng G misses rng p
proof
set x = the Element of (rng G) /\ (rng p);
assume not rng G misses rng p ; ::_thesis: contradiction
then (rng G) /\ (rng p) <> {} by XBOOLE_0:def_7;
then ( the Element of (rng G) /\ (rng p) in Carrier L1 & the Element of (rng G) /\ (rng p) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) ) by A13, A15, XBOOLE_0:def_4;
hence contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
then A40: G ^ p is one-to-one by A12, A16, FINSEQ_3:91;
then A41: len (G ^ p) = len (F ^ r) by A7, A25, A39, FINSEQ_1:48;
A42: dom P = Seg (len (F ^ r)) by A31, FINSEQ_1:def_3;
A43: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_^_p)_holds_
(G_^_p)_._x_=_(F_^_r)_._(P_._x)
let x be set ; ::_thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (F ^ r) . (P . x) )
assume A44: x in dom (G ^ p) ; ::_thesis: (G ^ p) . x = (F ^ r) . (P . x)
then reconsider n = x as Element of NAT by FINSEQ_3:23;
(G ^ p) . n in rng (F ^ r) by A25, A39, A44, FUNCT_1:def_3;
then A45: F ^ r just_once_values (G ^ p) . n by A7, FINSEQ_4:8;
n in Seg (len (F ^ r)) by A41, A44, FINSEQ_1:def_3;
then (F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by A32, A42
.= (G ^ p) . n by A45, FINSEQ_4:def_3 ;
hence (G ^ p) . x = (F ^ r) . (P . x) ; ::_thesis: verum
end;
A46: rng P c= Seg (len (F ^ r))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P or x in Seg (len (F ^ r)) )
assume x in rng P ; ::_thesis: x in Seg (len (F ^ r))
then consider y being set such that
A47: y in dom P and
A48: P . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A47, FINSEQ_3:23;
y in Seg (len (F ^ r)) by A31, A47, FINSEQ_1:def_3;
then y in dom (G ^ p) by A41, FINSEQ_1:def_3;
then (G ^ p) . y in rng (F ^ r) by A25, A39, FUNCT_1:def_3;
then A49: F ^ r just_once_values (G ^ p) . y by A7, FINSEQ_4:8;
P . y = (F ^ r) <- ((G ^ p) . y) by A32, A47;
then P . y in dom (F ^ r) by A49, FINSEQ_4:def_3;
hence x in Seg (len (F ^ r)) by A48, FINSEQ_1:def_3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_(G_^_p)_implies_(_x_in_dom_P_&_P_._x_in_dom_(F_^_r)_)_)_&_(_x_in_dom_P_&_P_._x_in_dom_(F_^_r)_implies_x_in_dom_(G_^_p)_)_)
let x be set ; ::_thesis: ( ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) & ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) ) )
thus ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) ::_thesis: ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) )
proof
assume x in dom (G ^ p) ; ::_thesis: ( x in dom P & P . x in dom (F ^ r) )
then x in Seg (len P) by A41, A31, FINSEQ_1:def_3;
hence x in dom P by FINSEQ_1:def_3; ::_thesis: P . x in dom (F ^ r)
then P . x in rng P by FUNCT_1:def_3;
then P . x in Seg (len (F ^ r)) by A46;
hence P . x in dom (F ^ r) by FINSEQ_1:def_3; ::_thesis: verum
end;
assume that
A50: x in dom P and
P . x in dom (F ^ r) ; ::_thesis: x in dom (G ^ p)
x in Seg (len P) by A50, FINSEQ_1:def_3;
hence x in dom (G ^ p) by A41, A31, FINSEQ_1:def_3; ::_thesis: verum
end;
then A51: G ^ p = (F ^ r) * P by A43, FUNCT_1:10;
Seg (len (F ^ r)) c= rng P
proof
set f = ((F ^ r) ") * (G ^ p);
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg (len (F ^ r)) or x in rng P )
assume A52: x in Seg (len (F ^ r)) ; ::_thesis: x in rng P
dom ((F ^ r) ") = rng (G ^ p) by A7, A25, A39, FUNCT_1:33;
then A53: rng (((F ^ r) ") * (G ^ p)) = rng ((F ^ r) ") by RELAT_1:28
.= dom (F ^ r) by A7, FUNCT_1:33 ;
A54: rng P c= dom (F ^ r) by A46, FINSEQ_1:def_3;
((F ^ r) ") * (G ^ p) = (((F ^ r) ") * (F ^ r)) * P by A51, RELAT_1:36
.= (id (dom (F ^ r))) * P by A7, FUNCT_1:39
.= P by A54, RELAT_1:53 ;
hence x in rng P by A52, A53, FINSEQ_1:def_3; ::_thesis: verum
end;
then A55: Seg (len (F ^ r)) = rng P by A46, XBOOLE_0:def_10;
then A56: P is one-to-one by A33, FINSEQ_4:60;
reconsider P = P as Function of (Seg (len (F ^ r))),(Seg (len (F ^ r))) by A46, A33, FUNCT_2:2;
reconsider P = P as Permutation of (Seg (len (F ^ r))) by A55, A56, FUNCT_2:57;
A57: len ((L1 + L2) (#) (F ^ r)) = len (F ^ r) by RLVECT_2:def_7;
then A58: Seg (len (F ^ r)) = dom ((L1 + L2) (#) (F ^ r)) by FINSEQ_1:def_3;
then reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of the carrier of V by FINSEQ_2:47;
A59: len (L1 (#) (G ^ p)) = len (G ^ p) by RLVECT_2:def_7;
deffunc H2( Nat) -> set = (H ^ q) <- ((G ^ p) . $1);
consider R being FinSequence such that
A60: len R = len (H ^ q) and
A61: for k being Nat st k in dom R holds
R . k = H2(k) from FINSEQ_1:sch_2();
A62: dom R = Seg (len (H ^ q)) by A60, FINSEQ_1:def_3;
rng (H ^ q) = (rng H) \/ (rng q) by FINSEQ_1:31;
then rng (H ^ q) = (Carrier L2) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by A19, A21, XBOOLE_1:39;
then A63: rng (H ^ q) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by XBOOLE_1:7, XBOOLE_1:12;
then A64: len (G ^ p) = len (H ^ q) by A23, A40, A25, FINSEQ_1:48;
A65: dom R = Seg (len (H ^ q)) by A60, FINSEQ_1:def_3;
A66: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_^_p)_holds_
(G_^_p)_._x_=_(H_^_q)_._(R_._x)
let x be set ; ::_thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (H ^ q) . (R . x) )
assume A67: x in dom (G ^ p) ; ::_thesis: (G ^ p) . x = (H ^ q) . (R . x)
then reconsider n = x as Element of NAT by FINSEQ_3:23;
(G ^ p) . n in rng (H ^ q) by A25, A63, A67, FUNCT_1:def_3;
then A68: H ^ q just_once_values (G ^ p) . n by A23, FINSEQ_4:8;
n in Seg (len (H ^ q)) by A64, A67, FINSEQ_1:def_3;
then (H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by A61, A65
.= (G ^ p) . n by A68, FINSEQ_4:def_3 ;
hence (G ^ p) . x = (H ^ q) . (R . x) ; ::_thesis: verum
end;
A69: rng R c= Seg (len (H ^ q))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng R or x in Seg (len (H ^ q)) )
assume x in rng R ; ::_thesis: x in Seg (len (H ^ q))
then consider y being set such that
A70: y in dom R and
A71: R . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A70, FINSEQ_3:23;
y in Seg (len (H ^ q)) by A60, A70, FINSEQ_1:def_3;
then y in dom (G ^ p) by A64, FINSEQ_1:def_3;
then (G ^ p) . y in rng (H ^ q) by A25, A63, FUNCT_1:def_3;
then A72: H ^ q just_once_values (G ^ p) . y by A23, FINSEQ_4:8;
R . y = (H ^ q) <- ((G ^ p) . y) by A61, A70;
then R . y in dom (H ^ q) by A72, FINSEQ_4:def_3;
hence x in Seg (len (H ^ q)) by A71, FINSEQ_1:def_3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_(G_^_p)_implies_(_x_in_dom_R_&_R_._x_in_dom_(H_^_q)_)_)_&_(_x_in_dom_R_&_R_._x_in_dom_(H_^_q)_implies_x_in_dom_(G_^_p)_)_)
let x be set ; ::_thesis: ( ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) & ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) ) )
thus ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) ::_thesis: ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) )
proof
assume x in dom (G ^ p) ; ::_thesis: ( x in dom R & R . x in dom (H ^ q) )
then x in Seg (len R) by A64, A60, FINSEQ_1:def_3;
hence x in dom R by FINSEQ_1:def_3; ::_thesis: R . x in dom (H ^ q)
then R . x in rng R by FUNCT_1:def_3;
then R . x in Seg (len (H ^ q)) by A69;
hence R . x in dom (H ^ q) by FINSEQ_1:def_3; ::_thesis: verum
end;
assume that
A73: x in dom R and
R . x in dom (H ^ q) ; ::_thesis: x in dom (G ^ p)
x in Seg (len R) by A73, FINSEQ_1:def_3;
hence x in dom (G ^ p) by A64, A60, FINSEQ_1:def_3; ::_thesis: verum
end;
then A74: G ^ p = (H ^ q) * R by A66, FUNCT_1:10;
Seg (len (H ^ q)) c= rng R
proof
set f = ((H ^ q) ") * (G ^ p);
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg (len (H ^ q)) or x in rng R )
assume A75: x in Seg (len (H ^ q)) ; ::_thesis: x in rng R
dom ((H ^ q) ") = rng (G ^ p) by A23, A25, A63, FUNCT_1:33;
then A76: rng (((H ^ q) ") * (G ^ p)) = rng ((H ^ q) ") by RELAT_1:28
.= dom (H ^ q) by A23, FUNCT_1:33 ;
A77: rng R c= dom (H ^ q) by A69, FINSEQ_1:def_3;
((H ^ q) ") * (G ^ p) = (((H ^ q) ") * (H ^ q)) * R by A74, RELAT_1:36
.= (id (dom (H ^ q))) * R by A23, FUNCT_1:39
.= R by A77, RELAT_1:53 ;
hence x in rng R by A75, A76, FINSEQ_1:def_3; ::_thesis: verum
end;
then A78: Seg (len (H ^ q)) = rng R by A69, XBOOLE_0:def_10;
then A79: R is one-to-one by A62, FINSEQ_4:60;
reconsider R = R as Function of (Seg (len (H ^ q))),(Seg (len (H ^ q))) by A69, A62, FUNCT_2:2;
reconsider R = R as Permutation of (Seg (len (H ^ q))) by A78, A79, FUNCT_2:57;
A80: len (L2 (#) (H ^ q)) = len (H ^ q) by RLVECT_2:def_7;
then A81: Seg (len (H ^ q)) = dom (L2 (#) (H ^ q)) by FINSEQ_1:def_3;
then reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of the carrier of V by FINSEQ_2:47;
A82: len Hp = len (G ^ p) by A64, A80, A81, FINSEQ_2:44;
deffunc H3( Nat) -> Element of the carrier of V = ((L1 (#) (G ^ p)) /. $1) + (Hp /. $1);
consider I being FinSequence such that
A83: len I = len (G ^ p) and
A84: for k being Nat st k in dom I holds
I . k = H3(k) from FINSEQ_1:sch_2();
dom I = Seg (len (G ^ p)) by A83, FINSEQ_1:def_3;
then A85: for k being Element of NAT st k in Seg (len (G ^ p)) holds
I . k = H3(k) by A84;
rng I c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng I or x in the carrier of V )
assume x in rng I ; ::_thesis: x in the carrier of V
then consider y being set such that
A86: y in dom I and
A87: I . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A86, FINSEQ_3:23;
I . y = ((L1 (#) (G ^ p)) /. y) + (Hp /. y) by A84, A86;
hence x in the carrier of V by A87; ::_thesis: verum
end;
then reconsider I = I as FinSequence of the carrier of V by FINSEQ_1:def_4;
A88: len Fp = len I by A41, A57, A58, A83, FINSEQ_2:44;
A89: now__::_thesis:_for_x_being_set_st_x_in_dom_I_holds_
I_._x_=_Fp_._x
let x be set ; ::_thesis: ( x in dom I implies I . x = Fp . x )
assume A90: x in dom I ; ::_thesis: I . x = Fp . x
then reconsider k = x as Element of NAT by FINSEQ_3:23;
A91: x in dom Hp by A83, A82, A90, FINSEQ_3:29;
k in dom R by A64, A62, A83, A90, FINSEQ_1:def_3;
then A92: R . k in dom R by A78, A62, FUNCT_1:def_3;
then reconsider j = R . k as Element of NAT by FINSEQ_3:23;
set v = (G ^ p) /. k;
A93: R . k in dom (H ^ q) by A60, A92, FINSEQ_3:29;
A94: x in dom (G ^ p) by A83, A90, FINSEQ_3:29;
then (H ^ q) . j = (G ^ p) . k by A66
.= (G ^ p) /. k by A94, PARTFUN1:def_6 ;
then A95: (L2 (#) (H ^ q)) . j = (L2 . ((G ^ p) /. k)) * ((G ^ p) /. k) by A93, RLVECT_2:24;
k in dom P by A41, A33, A83, A90, FINSEQ_1:def_3;
then A96: P . k in dom P by A55, A33, FUNCT_1:def_3;
then reconsider l = P . k as Element of NAT by FINSEQ_3:23;
A97: P . k in dom (F ^ r) by A31, A96, FINSEQ_3:29;
x in dom Fp by A88, A90, FINSEQ_3:29;
then A98: Fp . k = ((L1 + L2) (#) (F ^ r)) . (P . k) by FUNCT_1:12;
k in dom Hp by A83, A82, A90, FINSEQ_3:29;
then A99: Hp /. k = ((L2 (#) (H ^ q)) * R) . k by PARTFUN1:def_6
.= (L2 (#) (H ^ q)) . (R . k) by A91, FUNCT_1:12 ;
A100: x in dom (L1 (#) (G ^ p)) by A83, A59, A90, FINSEQ_3:29;
(F ^ r) . l = (G ^ p) . k by A43, A94
.= (G ^ p) /. k by A94, PARTFUN1:def_6 ;
then A101: ((L1 + L2) (#) (F ^ r)) . l = ((L1 + L2) . ((G ^ p) /. k)) * ((G ^ p) /. k) by A97, RLVECT_2:24
.= ((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) * ((G ^ p) /. k) by RLVECT_2:def_10
.= ((L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)) + ((L2 . ((G ^ p) /. k)) * ((G ^ p) /. k)) by RLVECT_1:def_6 ;
k in dom (L1 (#) (G ^ p)) by A83, A59, A90, FINSEQ_3:29;
then (L1 (#) (G ^ p)) /. k = (L1 (#) (G ^ p)) . k by PARTFUN1:def_6
.= (L1 . ((G ^ p) /. k)) * ((G ^ p) /. k) by A100, RLVECT_2:def_7 ;
hence I . x = Fp . x by A84, A90, A99, A95, A98, A101; ::_thesis: verum
end;
dom (L2 (#) (H ^ q)) = Seg (len (L2 (#) (H ^ q))) by FINSEQ_1:def_3;
then A102: Sum Hp = Sum (L2 (#) (H ^ q)) by A80, RLVECT_2:7;
dom ((L1 + L2) (#) (F ^ r)) = Seg (len ((L1 + L2) (#) (F ^ r))) by FINSEQ_1:def_3;
then A103: Sum Fp = Sum ((L1 + L2) (#) (F ^ r)) by A57, RLVECT_2:7;
( dom I = Seg (len I) & dom Fp = Seg (len I) ) by A88, FINSEQ_1:def_3;
then A104: I = Fp by A89, FUNCT_1:2;
Seg (len (G ^ p)) = dom (L1 (#) (G ^ p)) by A59, FINSEQ_1:def_3;
hence Sum (L1 + L2) = (Sum L1) + (Sum L2) by A3, A14, A20, A38, A30, A17, A103, A102, A83, A85, A82, A59, A104, RLVECT_2:2; ::_thesis: verum
end;
theorem Th2: :: RLVECT_3:2
for a being Real
for V being RealLinearSpace
for L being Linear_Combination of V holds Sum (a * L) = a * (Sum L)
proof
let a be Real; ::_thesis: for V being RealLinearSpace
for L being Linear_Combination of V holds Sum (a * L) = a * (Sum L)
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds Sum (a * L) = a * (Sum L)
let L be Linear_Combination of V; ::_thesis: Sum (a * L) = a * (Sum L)
percases ( a <> 0 or a = 0 ) ;
supposeA1: a <> 0 ; ::_thesis: Sum (a * L) = a * (Sum L)
set l = a * L;
consider F being FinSequence of the carrier of V such that
A2: F is one-to-one and
A3: rng F = Carrier (a * L) and
A4: Sum (a * L) = Sum ((a * L) (#) F) by RLVECT_2:def_8;
set f = (a * L) (#) F;
consider G being FinSequence of the carrier of V such that
A5: G is one-to-one and
A6: rng G = Carrier L and
A7: Sum L = Sum (L (#) G) by RLVECT_2:def_8;
A8: len G = len F by A1, A2, A3, A5, A6, FINSEQ_1:48, RLVECT_2:42;
deffunc H1( Nat) -> set = F <- (G . $1);
consider P being FinSequence such that
A9: len P = len F and
A10: for k being Nat st k in dom P holds
P . k = H1(k) from FINSEQ_1:sch_2();
A11: Carrier (a * L) = Carrier L by A1, RLVECT_2:42;
A12: rng P c= Seg (len F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P or x in Seg (len F) )
assume x in rng P ; ::_thesis: x in Seg (len F)
then consider y being set such that
A13: y in dom P and
A14: P . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A13, FINSEQ_3:23;
y in Seg (len F) by A9, A13, FINSEQ_1:def_3;
then y in dom G by A8, FINSEQ_1:def_3;
then G . y in rng F by A3, A6, A11, FUNCT_1:def_3;
then A15: F just_once_values G . y by A2, FINSEQ_4:8;
P . y = F <- (G . y) by A10, A13;
then P . y in dom F by A15, FINSEQ_4:def_3;
hence x in Seg (len F) by A14, FINSEQ_1:def_3; ::_thesis: verum
end;
A16: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_dom_G_implies_(_x_in_dom_P_&_P_._x_in_dom_F_)_)_&_(_x_in_dom_P_&_P_._x_in_dom_F_implies_x_in_dom_G_)_)
let x be set ; ::_thesis: ( ( x in dom G implies ( x in dom P & P . x in dom F ) ) & ( x in dom P & P . x in dom F implies x in dom G ) )
thus ( x in dom G implies ( x in dom P & P . x in dom F ) ) ::_thesis: ( x in dom P & P . x in dom F implies x in dom G )
proof
assume x in dom G ; ::_thesis: ( x in dom P & P . x in dom F )
then x in Seg (len P) by A9, A8, FINSEQ_1:def_3;
hence x in dom P by FINSEQ_1:def_3; ::_thesis: P . x in dom F
then P . x in rng P by FUNCT_1:def_3;
then P . x in Seg (len F) by A12;
hence P . x in dom F by FINSEQ_1:def_3; ::_thesis: verum
end;
assume that
A17: x in dom P and
P . x in dom F ; ::_thesis: x in dom G
x in Seg (len P) by A17, FINSEQ_1:def_3;
hence x in dom G by A9, A8, FINSEQ_1:def_3; ::_thesis: verum
end;
A18: dom P = Seg (len F) by A9, FINSEQ_1:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_G_holds_
G_._x_=_F_._(P_._x)
let x be set ; ::_thesis: ( x in dom G implies G . x = F . (P . x) )
assume A19: x in dom G ; ::_thesis: G . x = F . (P . x)
then reconsider n = x as Element of NAT by FINSEQ_3:23;
G . n in rng F by A3, A6, A11, A19, FUNCT_1:def_3;
then A20: F just_once_values G . n by A2, FINSEQ_4:8;
n in Seg (len F) by A8, A19, FINSEQ_1:def_3;
then F . (P . n) = F . (F <- (G . n)) by A10, A18
.= G . n by A20, FINSEQ_4:def_3 ;
hence G . x = F . (P . x) ; ::_thesis: verum
end;
then A21: G = F * P by A16, FUNCT_1:10;
Seg (len F) c= rng P
proof
set f = (F ") * G;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg (len F) or x in rng P )
assume A22: x in Seg (len F) ; ::_thesis: x in rng P
dom (F ") = rng G by A2, A3, A6, A11, FUNCT_1:33;
then A23: rng ((F ") * G) = rng (F ") by RELAT_1:28
.= dom F by A2, FUNCT_1:33 ;
A24: rng P c= dom F by A12, FINSEQ_1:def_3;
(F ") * G = ((F ") * F) * P by A21, RELAT_1:36
.= (id (dom F)) * P by A2, FUNCT_1:39
.= P by A24, RELAT_1:53 ;
hence x in rng P by A22, A23, FINSEQ_1:def_3; ::_thesis: verum
end;
then A25: Seg (len F) = rng P by A12, XBOOLE_0:def_10;
A26: dom P = Seg (len F) by A9, FINSEQ_1:def_3;
then A27: P is one-to-one by A25, FINSEQ_4:60;
reconsider P = P as Function of (Seg (len F)),(Seg (len F)) by A12, A26, FUNCT_2:2;
reconsider P = P as Permutation of (Seg (len F)) by A25, A27, FUNCT_2:57;
A28: len ((a * L) (#) F) = len F by RLVECT_2:def_7;
then A29: dom ((a * L) (#) F) = Seg (len F) by FINSEQ_1:def_3;
then reconsider Fp = ((a * L) (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:47;
set g = L (#) G;
dom ((a * L) (#) F) = Seg (len ((a * L) (#) F)) by FINSEQ_1:def_3;
then A30: Sum Fp = Sum ((a * L) (#) F) by A28, RLVECT_2:7;
A31: len Fp = len ((a * L) (#) F) by A29, FINSEQ_2:44;
then A32: len Fp = len (L (#) G) by A8, A28, RLVECT_2:def_7;
A33: now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_VECTOR_of_V_st_k_in_dom_(L_(#)_G)_&_v_=_(L_(#)_G)_._k_holds_
Fp_._k_=_a_*_v
let k be Element of NAT ; ::_thesis: for v being VECTOR of V st k in dom (L (#) G) & v = (L (#) G) . k holds
Fp . k = a * v
let v be VECTOR of V; ::_thesis: ( k in dom (L (#) G) & v = (L (#) G) . k implies Fp . k = a * v )
assume that
A34: k in dom (L (#) G) and
A35: v = (L (#) G) . k ; ::_thesis: Fp . k = a * v
A36: k in Seg (len F) by A28, A31, A32, A34, FINSEQ_1:def_3;
A37: k in dom G by A8, A28, A31, A32, A34, FINSEQ_3:29;
then G . k in rng G by FUNCT_1:def_3;
then F just_once_values G . k by A2, A3, A6, A11, FINSEQ_4:8;
then A38: F <- (G . k) in dom F by FINSEQ_4:def_3;
then reconsider i = F <- (G . k) as Element of NAT by FINSEQ_3:23;
i in Seg (len ((a * L) (#) F)) by A28, A38, FINSEQ_1:def_3;
then A39: i in dom ((a * L) (#) F) by FINSEQ_1:def_3;
A40: k in dom P by A9, A28, A31, A32, A34, FINSEQ_3:29;
A41: G /. k = G . k by A37, PARTFUN1:def_6
.= F . (P . k) by A21, A40, FUNCT_1:13
.= F . i by A10, A18, A36
.= F /. i by A38, PARTFUN1:def_6 ;
thus Fp . k = ((a * L) (#) F) . (P . k) by A40, FUNCT_1:13
.= ((a * L) (#) F) . (F <- (G . k)) by A10, A18, A36
.= ((a * L) . (F /. i)) * (F /. i) by A39, RLVECT_2:def_7
.= (a * (L . (F /. i))) * (F /. i) by RLVECT_2:def_11
.= a * ((L . (F /. i)) * (F /. i)) by RLVECT_1:def_7
.= a * v by A34, A35, A41, RLVECT_2:def_7 ; ::_thesis: verum
end;
dom Fp = dom (L (#) G) by A32, FINSEQ_3:29;
hence Sum (a * L) = a * (Sum L) by A4, A7, A30, A32, A33, RLVECT_1:39; ::_thesis: verum
end;
supposeA42: a = 0 ; ::_thesis: Sum (a * L) = a * (Sum L)
hence Sum (a * L) = Sum (ZeroLC V) by RLVECT_2:43
.= 0. V by RLVECT_2:30
.= a * (Sum L) by A42, RLVECT_1:10 ;
::_thesis: verum
end;
end;
end;
theorem Th3: :: RLVECT_3:3
for V being RealLinearSpace
for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
let L be Linear_Combination of V; ::_thesis: Sum (- L) = - (Sum L)
thus Sum (- L) = (- 1) * (Sum L) by Th2
.= - (Sum L) by RLVECT_1:16 ; ::_thesis: verum
end;
theorem Th4: :: RLVECT_3:4
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
proof
let V be RealLinearSpace; ::_thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
let L1, L2 be Linear_Combination of V; ::_thesis: Sum (L1 - L2) = (Sum L1) - (Sum L2)
thus Sum (L1 - L2) = (Sum L1) + (Sum (- L2)) by Th1
.= (Sum L1) + (- (Sum L2)) by Th3
.= (Sum L1) - (Sum L2) by RLVECT_1:def_11 ; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
let A be Subset of V;
attrA is linearly-independent means :Def1: :: RLVECT_3:def 1
for l being Linear_Combination of A st Sum l = 0. V holds
Carrier l = {} ;
end;
:: deftheorem Def1 defines linearly-independent RLVECT_3:def_1_:_
for V being RealLinearSpace
for A being Subset of V holds
( A is linearly-independent iff for l being Linear_Combination of A st Sum l = 0. V holds
Carrier l = {} );
notation
let V be RealLinearSpace;
let A be Subset of V;
antonym linearly-dependent A for linearly-independent ;
end;
theorem :: RLVECT_3:5
for V being RealLinearSpace
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
proof
let V be RealLinearSpace; ::_thesis: for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
let A, B be Subset of V; ::_thesis: ( A c= B & B is linearly-independent implies A is linearly-independent )
assume that
A1: A c= B and
A2: B is linearly-independent ; ::_thesis: A is linearly-independent
let l be Linear_Combination of A; :: according to RLVECT_3:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
reconsider L = l as Linear_Combination of B by A1, RLVECT_2:21;
assume Sum l = 0. V ; ::_thesis: Carrier l = {}
then Carrier L = {} by A2, Def1;
hence Carrier l = {} ; ::_thesis: verum
end;
theorem Th6: :: RLVECT_3:6
for V being RealLinearSpace
for A being Subset of V st A is linearly-independent holds
not 0. V in A
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V st A is linearly-independent holds
not 0. V in A
let A be Subset of V; ::_thesis: ( A is linearly-independent implies not 0. V in A )
assume that
A1: A is linearly-independent and
A2: 0. V in A ; ::_thesis: contradiction
deffunc H1( Element of V) -> Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A3: f . (0. V) = 1 and
A4: for v being Element of V st v <> 0. V holds
f . v = H1(v) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
ex T being finite Subset of V st
for v being VECTOR of V st not v in T holds
f . v = 0
proof
take T = {(0. V)}; ::_thesis: for v being VECTOR of V st not v in T holds
f . v = 0
let v be VECTOR of V; ::_thesis: ( not v in T implies f . v = 0 )
assume not v in T ; ::_thesis: f . v = 0
then v <> 0. V by TARSKI:def_1;
hence f . v = 0 by A4; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
A5: Carrier f = {(0. V)}
proof
thus Carrier f c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= Carrier f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {(0. V)} )
assume x in Carrier f ; ::_thesis: x in {(0. V)}
then consider v being VECTOR of V such that
A6: v = x and
A7: f . v <> 0 ;
v = 0. V by A4, A7;
hence x in {(0. V)} by A6, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in Carrier f )
assume x in {(0. V)} ; ::_thesis: x in Carrier f
then x = 0. V by TARSKI:def_1;
hence x in Carrier f by A3; ::_thesis: verum
end;
then Carrier f c= A by A2, ZFMISC_1:31;
then reconsider f = f as Linear_Combination of A by RLVECT_2:def_6;
Sum f = (f . (0. V)) * (0. V) by A5, RLVECT_2:35
.= 0. V by RLVECT_1:10 ;
hence contradiction by A1, A5, Def1; ::_thesis: verum
end;
theorem Th7: :: RLVECT_3:7
for V being RealLinearSpace holds {} the carrier of V is linearly-independent
proof
let V be RealLinearSpace; ::_thesis: {} the carrier of V is linearly-independent
let l be Linear_Combination of {} the carrier of V; :: according to RLVECT_3:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
Carrier l c= {} by RLVECT_2:def_6;
hence ( Sum l = 0. V implies Carrier l = {} ) ; ::_thesis: verum
end;
registration
let V be RealLinearSpace;
cluster linearly-independent for Element of bool the carrier of V;
existence
ex b1 being Subset of V st b1 is linearly-independent
proof
take {} the carrier of V ; ::_thesis: {} the carrier of V is linearly-independent
thus {} the carrier of V is linearly-independent by Th7; ::_thesis: verum
end;
end;
theorem Th8: :: RLVECT_3:8
for V being RealLinearSpace
for v being VECTOR of V holds
( {v} is linearly-independent iff v <> 0. V )
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V holds
( {v} is linearly-independent iff v <> 0. V )
let v be VECTOR of V; ::_thesis: ( {v} is linearly-independent iff v <> 0. V )
thus ( {v} is linearly-independent implies v <> 0. V ) ::_thesis: ( v <> 0. V implies {v} is linearly-independent )
proof
assume {v} is linearly-independent ; ::_thesis: v <> 0. V
then not 0. V in {v} by Th6;
hence v <> 0. V by TARSKI:def_1; ::_thesis: verum
end;
assume A1: v <> 0. V ; ::_thesis: {v} is linearly-independent
let l be Linear_Combination of {v}; :: according to RLVECT_3:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
A2: Carrier l c= {v} by RLVECT_2:def_6;
assume A3: Sum l = 0. V ; ::_thesis: Carrier l = {}
now__::_thesis:_Carrier_l_=_{}
percases ( Carrier l = {} or Carrier l = {v} ) by A2, ZFMISC_1:33;
suppose Carrier l = {} ; ::_thesis: Carrier l = {}
hence Carrier l = {} ; ::_thesis: verum
end;
supposeA4: Carrier l = {v} ; ::_thesis: Carrier l = {}
A5: 0. V = (l . v) * v by A3, RLVECT_2:32;
now__::_thesis:_not_v_in_Carrier_l
assume v in Carrier l ; ::_thesis: contradiction
then ex u being VECTOR of V st
( v = u & l . u <> 0 ) ;
hence contradiction by A1, A5, RLVECT_1:11; ::_thesis: verum
end;
hence Carrier l = {} by A4, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence Carrier l = {} ; ::_thesis: verum
end;
theorem :: RLVECT_3:9
for V being RealLinearSpace holds {(0. V)} is linearly-dependent by Th8;
theorem Th10: :: RLVECT_3:10
for V being RealLinearSpace
for v1, v2 being VECTOR of V st {v1,v2} is linearly-independent holds
( v1 <> 0. V & v2 <> 0. V )
proof
let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V st {v1,v2} is linearly-independent holds
( v1 <> 0. V & v2 <> 0. V )
let v1, v2 be VECTOR of V; ::_thesis: ( {v1,v2} is linearly-independent implies ( v1 <> 0. V & v2 <> 0. V ) )
A1: ( v1 in {v1,v2} & v2 in {v1,v2} ) by TARSKI:def_2;
assume {v1,v2} is linearly-independent ; ::_thesis: ( v1 <> 0. V & v2 <> 0. V )
hence ( v1 <> 0. V & v2 <> 0. V ) by A1, Th6; ::_thesis: verum
end;
theorem :: RLVECT_3:11
for V being RealLinearSpace
for v being VECTOR of V holds
( {v,(0. V)} is linearly-dependent & {(0. V),v} is linearly-dependent ) by Th10;
theorem Th12: :: RLVECT_3:12
for V being RealLinearSpace
for v1, v2 being VECTOR of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) ) )
proof
let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) ) )
let v1, v2 be VECTOR of V; ::_thesis: ( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) ) )
thus ( v1 <> v2 & {v1,v2} is linearly-independent implies ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) ) ) ::_thesis: ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )
proof
deffunc H1( Element of V) -> Element of NAT = 0 ;
assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent ; ::_thesis: ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) )
thus v2 <> 0. V by A2, Th10; ::_thesis: for a being Real holds v1 <> a * v2
let a be Real; ::_thesis: v1 <> a * v2
consider f being Function of the carrier of V,REAL such that
A3: ( f . v1 = - 1 & f . v2 = a ) and
A4: for v being Element of V st v <> v1 & v <> v2 holds
f . v = H1(v) from FUNCT_2:sch_7(A1);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_{v1,v2}_holds_
f_._v_=_0
let v be VECTOR of V; ::_thesis: ( not v in {v1,v2} implies f . v = 0 )
assume not v in {v1,v2} ; ::_thesis: f . v = 0
then ( v <> v1 & v <> v2 ) by TARSKI:def_2;
hence f . v = 0 by A4; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
Carrier f c= {v1,v2}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v1,v2} )
assume x in Carrier f ; ::_thesis: x in {v1,v2}
then A5: ex u being VECTOR of V st
( x = u & f . u <> 0 ) ;
assume not x in {v1,v2} ; ::_thesis: contradiction
then ( x <> v1 & x <> v2 ) by TARSKI:def_2;
hence contradiction by A4, A5; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v1,v2} by RLVECT_2:def_6;
A6: v1 in Carrier f by A3;
set w = a * v2;
assume v1 = a * v2 ; ::_thesis: contradiction
then Sum f = ((- 1) * (a * v2)) + (a * v2) by A1, A3, RLVECT_2:33
.= (- (a * v2)) + (a * v2) by RLVECT_1:16
.= - ((a * v2) - (a * v2)) by RLVECT_1:33
.= - (0. V) by RLVECT_1:15
.= 0. V by RLVECT_1:12 ;
hence contradiction by A2, A6, Def1; ::_thesis: verum
end;
assume A7: v2 <> 0. V ; ::_thesis: ( ex a being Real st not v1 <> a * v2 or ( v1 <> v2 & {v1,v2} is linearly-independent ) )
assume A8: for a being Real holds v1 <> a * v2 ; ::_thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )
A9: 1 * v2 = v2 by RLVECT_1:def_8;
hence v1 <> v2 by A8; ::_thesis: {v1,v2} is linearly-independent
let l be Linear_Combination of {v1,v2}; :: according to RLVECT_3:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
assume that
A10: Sum l = 0. V and
A11: Carrier l <> {} ; ::_thesis: contradiction
A12: 0. V = ((l . v1) * v1) + ((l . v2) * v2) by A8, A9, A10, RLVECT_2:33;
set x = the Element of Carrier l;
Carrier l c= {v1,v2} by RLVECT_2:def_6;
then A13: the Element of Carrier l in {v1,v2} by A11, TARSKI:def_3;
the Element of Carrier l in Carrier l by A11;
then A14: ex u being VECTOR of V st
( the Element of Carrier l = u & l . u <> 0 ) ;
now__::_thesis:_contradiction
percases ( l . v1 <> 0 or ( l . v2 <> 0 & l . v1 = 0 ) ) by A14, A13, TARSKI:def_2;
supposeA15: l . v1 <> 0 ; ::_thesis: contradiction
0. V = ((l . v1) ") * (((l . v1) * v1) + ((l . v2) * v2)) by A12, RLVECT_1:10
.= (((l . v1) ") * ((l . v1) * v1)) + (((l . v1) ") * ((l . v2) * v2)) by RLVECT_1:def_5
.= ((((l . v1) ") * (l . v1)) * v1) + (((l . v1) ") * ((l . v2) * v2)) by RLVECT_1:def_7
.= ((((l . v1) ") * (l . v1)) * v1) + ((((l . v1) ") * (l . v2)) * v2) by RLVECT_1:def_7
.= (1 * v1) + ((((l . v1) ") * (l . v2)) * v2) by A15, XCMPLX_0:def_7
.= v1 + ((((l . v1) ") * (l . v2)) * v2) by RLVECT_1:def_8 ;
then v1 = - ((((l . v1) ") * (l . v2)) * v2) by RLVECT_1:6
.= (- 1) * ((((l . v1) ") * (l . v2)) * v2) by RLVECT_1:16
.= ((- 1) * (((l . v1) ") * (l . v2))) * v2 by RLVECT_1:def_7 ;
hence contradiction by A8; ::_thesis: verum
end;
supposeA16: ( l . v2 <> 0 & l . v1 = 0 ) ; ::_thesis: contradiction
0. V = ((l . v2) ") * (((l . v1) * v1) + ((l . v2) * v2)) by A12, RLVECT_1:10
.= (((l . v2) ") * ((l . v1) * v1)) + (((l . v2) ") * ((l . v2) * v2)) by RLVECT_1:def_5
.= ((((l . v2) ") * (l . v1)) * v1) + (((l . v2) ") * ((l . v2) * v2)) by RLVECT_1:def_7
.= ((((l . v2) ") * (l . v1)) * v1) + ((((l . v2) ") * (l . v2)) * v2) by RLVECT_1:def_7
.= ((((l . v2) ") * (l . v1)) * v1) + (1 * v2) by A16, XCMPLX_0:def_7
.= (0 * v1) + v2 by A16, RLVECT_1:def_8
.= (0. V) + v2 by RLVECT_1:10
.= v2 by RLVECT_1:4 ;
hence contradiction by A7; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem :: RLVECT_3:13
for V being RealLinearSpace
for v1, v2 being VECTOR of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) )
proof
let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) )
let v1, v2 be VECTOR of V; ::_thesis: ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) )
thus ( v1 <> v2 & {v1,v2} is linearly-independent implies for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) ) ::_thesis: ( ( for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )
proof
assume A1: ( v1 <> v2 & {v1,v2} is linearly-independent ) ; ::_thesis: for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 )
let a, b be Real; ::_thesis: ( (a * v1) + (b * v2) = 0. V implies ( a = 0 & b = 0 ) )
assume that
A2: (a * v1) + (b * v2) = 0. V and
A3: ( a <> 0 or b <> 0 ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( a <> 0 or b <> 0 ) by A3;
supposeA4: a <> 0 ; ::_thesis: contradiction
0. V = (a ") * ((a * v1) + (b * v2)) by A2, RLVECT_1:10
.= ((a ") * (a * v1)) + ((a ") * (b * v2)) by RLVECT_1:def_5
.= (((a ") * a) * v1) + ((a ") * (b * v2)) by RLVECT_1:def_7
.= (((a ") * a) * v1) + (((a ") * b) * v2) by RLVECT_1:def_7
.= (1 * v1) + (((a ") * b) * v2) by A4, XCMPLX_0:def_7
.= v1 + (((a ") * b) * v2) by RLVECT_1:def_8 ;
then v1 = - (((a ") * b) * v2) by RLVECT_1:6
.= (- 1) * (((a ") * b) * v2) by RLVECT_1:16
.= ((- 1) * ((a ") * b)) * v2 by RLVECT_1:def_7 ;
hence contradiction by A1, Th12; ::_thesis: verum
end;
supposeA5: b <> 0 ; ::_thesis: contradiction
0. V = (b ") * ((a * v1) + (b * v2)) by A2, RLVECT_1:10
.= ((b ") * (a * v1)) + ((b ") * (b * v2)) by RLVECT_1:def_5
.= (((b ") * a) * v1) + ((b ") * (b * v2)) by RLVECT_1:def_7
.= (((b ") * a) * v1) + (((b ") * b) * v2) by RLVECT_1:def_7
.= (((b ") * a) * v1) + (1 * v2) by A5, XCMPLX_0:def_7
.= (((b ") * a) * v1) + v2 by RLVECT_1:def_8 ;
then v2 = - (((b ") * a) * v1) by RLVECT_1:def_10
.= (- 1) * (((b ") * a) * v1) by RLVECT_1:16
.= ((- 1) * ((b ") * a)) * v1 by RLVECT_1:def_7 ;
hence contradiction by A1, Th12; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
assume A6: for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) ; ::_thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )
A7: now__::_thesis:_for_a_being_Real_holds_not_v1_=_a_*_v2
let a be Real; ::_thesis: not v1 = a * v2
assume v1 = a * v2 ; ::_thesis: contradiction
then v1 = (0. V) + (a * v2) by RLVECT_1:4;
then 0. V = v1 - (a * v2) by RLSUB_2:61
.= v1 + (- (a * v2)) by RLVECT_1:def_11
.= v1 + (a * (- v2)) by RLVECT_1:25
.= v1 + ((- a) * v2) by RLVECT_1:24
.= (1 * v1) + ((- a) * v2) by RLVECT_1:def_8 ;
hence contradiction by A6; ::_thesis: verum
end;
now__::_thesis:_not_v2_=_0._V
assume A8: v2 = 0. V ; ::_thesis: contradiction
0. V = (0. V) + (0. V) by RLVECT_1:4
.= (0 * v1) + (0. V) by RLVECT_1:10
.= (0 * v1) + (1 * v2) by A8, RLVECT_1:10 ;
hence contradiction by A6; ::_thesis: verum
end;
hence ( v1 <> v2 & {v1,v2} is linearly-independent ) by A7, Th12; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
let A be Subset of V;
func Lin A -> strict Subspace of V means :Def2: :: RLVECT_3:def 2
the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ;
existence
ex b1 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum }
proof
set A1 = { (Sum l) where l is Linear_Combination of A : verum } ;
{ (Sum l) where l is Linear_Combination of A : verum } c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Sum l) where l is Linear_Combination of A : verum } or x in the carrier of V )
assume x in { (Sum l) where l is Linear_Combination of A : verum } ; ::_thesis: x in the carrier of V
then ex l being Linear_Combination of A st x = Sum l ;
hence x in the carrier of V ; ::_thesis: verum
end;
then reconsider A1 = { (Sum l) where l is Linear_Combination of A : verum } as Subset of V ;
reconsider l = ZeroLC V as Linear_Combination of A by RLVECT_2:22;
A1: A1 is linearly-closed
proof
thus for v, u being VECTOR of V st v in A1 & u in A1 holds
v + u in A1 :: according to RLSUB_1:def_1 ::_thesis: for b1 being Element of REAL
for b2 being Element of the carrier of V holds
( not b2 in A1 or b1 * b2 in A1 )
proof
let v, u be VECTOR of V; ::_thesis: ( v in A1 & u in A1 implies v + u in A1 )
assume that
A2: v in A1 and
A3: u in A1 ; ::_thesis: v + u in A1
consider l1 being Linear_Combination of A such that
A4: v = Sum l1 by A2;
consider l2 being Linear_Combination of A such that
A5: u = Sum l2 by A3;
reconsider f = l1 + l2 as Linear_Combination of A by RLVECT_2:38;
v + u = Sum f by A4, A5, Th1;
hence v + u in A1 ; ::_thesis: verum
end;
let a be Real; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in A1 or a * b1 in A1 )
let v be VECTOR of V; ::_thesis: ( not v in A1 or a * v in A1 )
assume v in A1 ; ::_thesis: a * v in A1
then consider l being Linear_Combination of A such that
A6: v = Sum l ;
reconsider f = a * l as Linear_Combination of A by RLVECT_2:44;
a * v = Sum f by A6, Th2;
hence a * v in A1 ; ::_thesis: verum
end;
Sum l = 0. V by RLVECT_2:30;
then 0. V in A1 ;
hence ex b1 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } by A1, RLSUB_1:35; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b2 = { (Sum l) where l is Linear_Combination of A : verum } holds
b1 = b2 by RLSUB_1:30;
end;
:: deftheorem Def2 defines Lin RLVECT_3:def_2_:_
for V being RealLinearSpace
for A being Subset of V
for b3 being strict Subspace of V holds
( b3 = Lin A iff the carrier of b3 = { (Sum l) where l is Linear_Combination of A : verum } );
theorem Th14: :: RLVECT_3:14
for x being set
for V being RealLinearSpace
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let A be Subset of V; ::_thesis: ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
thus ( x in Lin A implies ex l being Linear_Combination of A st x = Sum l ) ::_thesis: ( ex l being Linear_Combination of A st x = Sum l implies x in Lin A )
proof
assume x in Lin A ; ::_thesis: ex l being Linear_Combination of A st x = Sum l
then x in the carrier of (Lin A) by STRUCT_0:def_5;
then x in { (Sum l) where l is Linear_Combination of A : verum } by Def2;
hence ex l being Linear_Combination of A st x = Sum l ; ::_thesis: verum
end;
given k being Linear_Combination of A such that A1: x = Sum k ; ::_thesis: x in Lin A
x in { (Sum l) where l is Linear_Combination of A : verum } by A1;
then x in the carrier of (Lin A) by Def2;
hence x in Lin A by STRUCT_0:def_5; ::_thesis: verum
end;
theorem Th15: :: RLVECT_3:15
for x being set
for V being RealLinearSpace
for A being Subset of V st x in A holds
x in Lin A
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for A being Subset of V st x in A holds
x in Lin A
let V be RealLinearSpace; ::_thesis: for A being Subset of V st x in A holds
x in Lin A
let A be Subset of V; ::_thesis: ( x in A implies x in Lin A )
deffunc H1( Element of V) -> Element of NAT = 0 ;
assume A1: x in A ; ::_thesis: x in Lin A
then reconsider v = x as VECTOR of V ;
consider f being Function of the carrier of V,REAL such that
A2: f . v = 1 and
A3: for u being VECTOR of V st u <> v holds
f . u = H1(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
ex T being finite Subset of V st
for u being VECTOR of V st not u in T holds
f . u = 0
proof
take T = {v}; ::_thesis: for u being VECTOR of V st not u in T holds
f . u = 0
let u be VECTOR of V; ::_thesis: ( not u in T implies f . u = 0 )
assume not u in T ; ::_thesis: f . u = 0
then u <> v by TARSKI:def_1;
hence f . u = 0 by A3; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
A4: Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume x in Carrier f ; ::_thesis: x in {v}
then consider u being VECTOR of V such that
A5: x = u and
A6: f . u <> 0 ;
u = v by A3, A6;
hence x in {v} by A5, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def_6;
A7: Sum f = 1 * v by A2, RLVECT_2:32
.= v by RLVECT_1:def_8 ;
{v} c= A by A1, ZFMISC_1:31;
then Carrier f c= A by A4, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by RLVECT_2:def_6;
Sum f = v by A7;
hence x in Lin A by Th14; ::_thesis: verum
end;
Lm2: for x being set
for V being RealLinearSpace holds
( x in (0). V iff x = 0. V )
proof
let x be set ; ::_thesis: for V being RealLinearSpace holds
( x in (0). V iff x = 0. V )
let V be RealLinearSpace; ::_thesis: ( x in (0). V iff x = 0. V )
thus ( x in (0). V implies x = 0. V ) ::_thesis: ( x = 0. V implies x in (0). V )
proof
assume x in (0). V ; ::_thesis: x = 0. V
then x in the carrier of ((0). V) by STRUCT_0:def_5;
then x in {(0. V)} by RLSUB_1:def_3;
hence x = 0. V by TARSKI:def_1; ::_thesis: verum
end;
thus ( x = 0. V implies x in (0). V ) by RLSUB_1:17; ::_thesis: verum
end;
theorem :: RLVECT_3:16
for V being RealLinearSpace holds Lin ({} the carrier of V) = (0). V
proof
let V be RealLinearSpace; ::_thesis: Lin ({} the carrier of V) = (0). V
set A = Lin ({} the carrier of V);
now__::_thesis:_for_v_being_VECTOR_of_V_holds_
(_(_v_in_Lin_({}_the_carrier_of_V)_implies_v_in_(0)._V_)_&_(_v_in_(0)._V_implies_v_in_Lin_({}_the_carrier_of_V)_)_)
let v be VECTOR of V; ::_thesis: ( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )
thus ( v in Lin ({} the carrier of V) implies v in (0). V ) ::_thesis: ( v in (0). V implies v in Lin ({} the carrier of V) )
proof
assume v in Lin ({} the carrier of V) ; ::_thesis: v in (0). V
then A1: v in the carrier of (Lin ({} the carrier of V)) by STRUCT_0:def_5;
the carrier of (Lin ({} the carrier of V)) = { (Sum l0) where l0 is Linear_Combination of {} the carrier of V : verum } by Def2;
then ex l0 being Linear_Combination of {} the carrier of V st v = Sum l0 by A1;
then v = 0. V by RLVECT_2:31;
hence v in (0). V by Lm2; ::_thesis: verum
end;
assume v in (0). V ; ::_thesis: v in Lin ({} the carrier of V)
then v = 0. V by Lm2;
hence v in Lin ({} the carrier of V) by RLSUB_1:17; ::_thesis: verum
end;
hence Lin ({} the carrier of V) = (0). V by RLSUB_1:31; ::_thesis: verum
end;
theorem :: RLVECT_3:17
for V being RealLinearSpace
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
let A be Subset of V; ::_thesis: ( not Lin A = (0). V or A = {} or A = {(0. V)} )
assume that
A1: Lin A = (0). V and
A2: A <> {} ; ::_thesis: A = {(0. V)}
thus A c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in {(0. V)} )
assume x in A ; ::_thesis: x in {(0. V)}
then x in Lin A by Th15;
then x = 0. V by A1, Lm2;
hence x in {(0. V)} by TARSKI:def_1; ::_thesis: verum
end;
set y = the Element of A;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in A )
assume x in {(0. V)} ; ::_thesis: x in A
then A3: x = 0. V by TARSKI:def_1;
( the Element of A in A & the Element of A in Lin A ) by A2, Th15;
hence x in A by A1, A3, Lm2; ::_thesis: verum
end;
theorem Th18: :: RLVECT_3:18
for V being RealLinearSpace
for A being Subset of V
for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V
for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
let A be Subset of V; ::_thesis: for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
let W be strict Subspace of V; ::_thesis: ( A = the carrier of W implies Lin A = W )
assume A1: A = the carrier of W ; ::_thesis: Lin A = W
now__::_thesis:_for_v_being_VECTOR_of_V_holds_
(_(_v_in_Lin_A_implies_v_in_W_)_&_(_v_in_W_implies_v_in_Lin_A_)_)
let v be VECTOR of V; ::_thesis: ( ( v in Lin A implies v in W ) & ( v in W implies v in Lin A ) )
thus ( v in Lin A implies v in W ) ::_thesis: ( v in W implies v in Lin A )
proof
assume v in Lin A ; ::_thesis: v in W
then A2: ex l being Linear_Combination of A st v = Sum l by Th14;
A is linearly-closed by A1, RLSUB_1:34;
then v in the carrier of W by A1, A2, RLVECT_2:29;
hence v in W by STRUCT_0:def_5; ::_thesis: verum
end;
( v in W iff v in the carrier of W ) by STRUCT_0:def_5;
hence ( v in W implies v in Lin A ) by A1, Th15; ::_thesis: verum
end;
hence Lin A = W by RLSUB_1:31; ::_thesis: verum
end;
theorem :: RLVECT_3:19
for V being strict RealLinearSpace
for A being Subset of V st A = the carrier of V holds
Lin A = V
proof
let V be strict RealLinearSpace; ::_thesis: for A being Subset of V st A = the carrier of V holds
Lin A = V
let A be Subset of V; ::_thesis: ( A = the carrier of V implies Lin A = V )
assume A = the carrier of V ; ::_thesis: Lin A = V
then A = the carrier of ((Omega). V) ;
hence Lin A = V by Th18; ::_thesis: verum
end;
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
proof
let V be RealLinearSpace; ::_thesis: for W1, W3, W2 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
let W1, W3, W2 be Subspace of V; ::_thesis: ( W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3 )
A1: W1 /\ W2 is Subspace of W1 by RLSUB_2:16;
assume W1 is Subspace of W3 ; ::_thesis: W1 /\ W2 is Subspace of W3
hence W1 /\ W2 is Subspace of W3 by A1, RLSUB_1:27; ::_thesis: verum
end;
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
proof
let V be RealLinearSpace; ::_thesis: 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
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of W2 /\ W3 )
assume A1: ( W1 is Subspace of W2 & W1 is Subspace of W3 ) ; ::_thesis: W1 is Subspace of W2 /\ W3
now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_W1_holds_
v_in_W2_/\_W3
let v be VECTOR of V; ::_thesis: ( v in W1 implies v in W2 /\ W3 )
assume v in W1 ; ::_thesis: v in W2 /\ W3
then ( v in W2 & v in W3 ) by A1, RLSUB_1:8;
hence v in W2 /\ W3 by RLSUB_2:3; ::_thesis: verum
end;
hence W1 is Subspace of W2 /\ W3 by RLSUB_1:29; ::_thesis: verum
end;
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
proof
let V be RealLinearSpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 implies W1 is Subspace of W2 + W3 )
A1: W2 is Subspace of W2 + W3 by RLSUB_2:7;
assume W1 is Subspace of W2 ; ::_thesis: W1 is Subspace of W2 + W3
hence W1 is Subspace of W2 + W3 by A1, RLSUB_1:27; ::_thesis: verum
end;
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
proof
let V be RealLinearSpace; ::_thesis: 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
let W1, W3, W2 be Subspace of V; ::_thesis: ( W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is Subspace of W3 )
assume A1: ( W1 is Subspace of W3 & W2 is Subspace of W3 ) ; ::_thesis: W1 + W2 is Subspace of W3
now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_W1_+_W2_holds_
v_in_W3
let v be VECTOR of V; ::_thesis: ( v in W1 + W2 implies v in W3 )
assume v in W1 + W2 ; ::_thesis: v in W3
then consider v1, v2 being VECTOR of V such that
A2: ( v1 in W1 & v2 in W2 ) and
A3: v = v1 + v2 by RLSUB_2:1;
( v1 in W3 & v2 in W3 ) by A1, A2, RLSUB_1:8;
hence v in W3 by A3, RLSUB_1:20; ::_thesis: verum
end;
hence W1 + W2 is Subspace of W3 by RLSUB_1:29; ::_thesis: verum
end;
theorem Th20: :: RLVECT_3:20
for V being RealLinearSpace
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
proof
let V be RealLinearSpace; ::_thesis: for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
let A, B be Subset of V; ::_thesis: ( A c= B implies Lin A is Subspace of Lin B )
assume A1: A c= B ; ::_thesis: Lin A is Subspace of Lin B
now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_Lin_A_holds_
v_in_Lin_B
let v be VECTOR of V; ::_thesis: ( v in Lin A implies v in Lin B )
assume v in Lin A ; ::_thesis: v in Lin B
then consider l being Linear_Combination of A such that
A2: v = Sum l by Th14;
reconsider l = l as Linear_Combination of B by A1, RLVECT_2:21;
Sum l = v by A2;
hence v in Lin B by Th14; ::_thesis: verum
end;
hence Lin A is Subspace of Lin B by RLSUB_1:29; ::_thesis: verum
end;
theorem :: RLVECT_3:21
for V being strict RealLinearSpace
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
proof
let V be strict RealLinearSpace; ::_thesis: for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let A, B be Subset of V; ::_thesis: ( Lin A = V & A c= B implies Lin B = V )
assume ( Lin A = V & A c= B ) ; ::_thesis: Lin B = V
then V is Subspace of Lin B by Th20;
hence Lin B = V by RLSUB_1:26; ::_thesis: verum
end;
theorem :: RLVECT_3:22
for V being RealLinearSpace
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proof
let V be RealLinearSpace; ::_thesis: for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
let A, B be Subset of V; ::_thesis: Lin (A \/ B) = (Lin A) + (Lin B)
now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_Lin_(A_\/_B)_holds_
v_in_(Lin_A)_+_(Lin_B)
deffunc H1( set ) -> Element of NAT = 0 ;
let v be VECTOR of V; ::_thesis: ( v in Lin (A \/ B) implies v in (Lin A) + (Lin B) )
assume v in Lin (A \/ B) ; ::_thesis: v in (Lin A) + (Lin B)
then consider l being Linear_Combination of A \/ B such that
A1: v = Sum l by Th14;
deffunc H2( set ) -> set = l . $1;
set D = (Carrier l) \ A;
set C = (Carrier l) /\ A;
defpred S1[ set ] means $1 in (Carrier l) /\ A;
defpred S2[ set ] means $1 in (Carrier l) \ A;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_
(_(_x_in_(Carrier_l)_/\_A_implies_l_._x_in_REAL_)_&_(_not_x_in_(Carrier_l)_/\_A_implies_0_in_REAL_)_)
let x be set ; ::_thesis: ( x in the carrier of V implies ( ( x in (Carrier l) /\ A implies l . x in REAL ) & ( not x in (Carrier l) /\ A implies 0 in REAL ) ) )
assume x in the carrier of V ; ::_thesis: ( ( x in (Carrier l) /\ A implies l . x in REAL ) & ( not x in (Carrier l) /\ A implies 0 in REAL ) )
then reconsider v = x as VECTOR of V ;
for f being Function of the carrier of V,REAL holds f . v in REAL ;
hence ( x in (Carrier l) /\ A implies l . x in REAL ) ; ::_thesis: ( not x in (Carrier l) /\ A implies 0 in REAL )
assume not x in (Carrier l) /\ A ; ::_thesis: 0 in REAL
thus 0 in REAL ; ::_thesis: verum
end;
then A2: for x being set st x in the carrier of V holds
( ( S1[x] implies H2(x) in REAL ) & ( not S1[x] implies H1(x) in REAL ) ) ;
consider f being Function of the carrier of V,REAL such that
A3: for x being set st x in the carrier of V holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch_5(A2);
reconsider C = (Carrier l) /\ A as finite Subset of V ;
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
for u being VECTOR of V st not u in C holds
f . u = 0 by A3;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
A4: Carrier f c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in C )
assume x in Carrier f ; ::_thesis: x in C
then A5: ex u being VECTOR of V st
( x = u & f . u <> 0 ) ;
assume not x in C ; ::_thesis: contradiction
hence contradiction by A3, A5; ::_thesis: verum
end;
C c= A by XBOOLE_1:17;
then Carrier f c= A by A4, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by RLVECT_2:def_6;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_
(_(_x_in_(Carrier_l)_\_A_implies_l_._x_in_REAL_)_&_(_not_x_in_(Carrier_l)_\_A_implies_0_in_REAL_)_)
let x be set ; ::_thesis: ( x in the carrier of V implies ( ( x in (Carrier l) \ A implies l . x in REAL ) & ( not x in (Carrier l) \ A implies 0 in REAL ) ) )
assume x in the carrier of V ; ::_thesis: ( ( x in (Carrier l) \ A implies l . x in REAL ) & ( not x in (Carrier l) \ A implies 0 in REAL ) )
then reconsider v = x as VECTOR of V ;
for g being Function of the carrier of V,REAL holds g . v in REAL ;
hence ( x in (Carrier l) \ A implies l . x in REAL ) ; ::_thesis: ( not x in (Carrier l) \ A implies 0 in REAL )
assume not x in (Carrier l) \ A ; ::_thesis: 0 in REAL
thus 0 in REAL ; ::_thesis: verum
end;
then A6: for x being set st x in the carrier of V holds
( ( S2[x] implies H2(x) in REAL ) & ( not S2[x] implies H1(x) in REAL ) ) ;
consider g being Function of the carrier of V,REAL such that
A7: for x being set st x in the carrier of V holds
( ( S2[x] implies g . x = H2(x) ) & ( not S2[x] implies g . x = H1(x) ) ) from FUNCT_2:sch_5(A6);
reconsider D = (Carrier l) \ A as finite Subset of V ;
reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
for u being VECTOR of V st not u in D holds
g . u = 0 by A7;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def_3;
A8: D c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in B )
assume x in D ; ::_thesis: x in B
then A9: ( x in Carrier l & not x in A ) by XBOOLE_0:def_5;
Carrier l c= A \/ B by RLVECT_2:def_6;
hence x in B by A9, XBOOLE_0:def_3; ::_thesis: verum
end;
Carrier g c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in D )
assume x in Carrier g ; ::_thesis: x in D
then A10: ex u being VECTOR of V st
( x = u & g . u <> 0 ) ;
assume not x in D ; ::_thesis: contradiction
hence contradiction by A7, A10; ::_thesis: verum
end;
then Carrier g c= B by A8, XBOOLE_1:1;
then reconsider g = g as Linear_Combination of B by RLVECT_2:def_6;
l = f + g
proof
let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: l . v = (f + g) . v
now__::_thesis:_(f_+_g)_._v_=_l_._v
percases ( v in C or not v in C ) ;
supposeA11: v in C ; ::_thesis: (f + g) . v = l . v
A12: now__::_thesis:_not_v_in_D
assume v in D ; ::_thesis: contradiction
then not v in A by XBOOLE_0:def_5;
hence contradiction by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def_10
.= (l . v) + (g . v) by A3, A11
.= (l . v) + 0 by A7, A12
.= l . v ; ::_thesis: verum
end;
supposeA13: not v in C ; ::_thesis: l . v = (f + g) . v
now__::_thesis:_(f_+_g)_._v_=_l_._v
percases ( v in Carrier l or not v in Carrier l ) ;
supposeA14: v in Carrier l ; ::_thesis: (f + g) . v = l . v
A15: now__::_thesis:_v_in_D
assume not v in D ; ::_thesis: contradiction
then ( not v in Carrier l or v in A ) by XBOOLE_0:def_5;
hence contradiction by A13, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def_10
.= 0 + (g . v) by A3, A13
.= l . v by A7, A15 ; ::_thesis: verum
end;
supposeA16: not v in Carrier l ; ::_thesis: (f + g) . v = l . v
then A17: not v in D by XBOOLE_0:def_5;
A18: not v in C by A16, XBOOLE_0:def_4;
thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def_10
.= 0 + (g . v) by A3, A18
.= 0 + 0 by A7, A17
.= l . v by A16 ; ::_thesis: verum
end;
end;
end;
hence l . v = (f + g) . v ; ::_thesis: verum
end;
end;
end;
hence l . v = (f + g) . v ; ::_thesis: verum
end;
then A19: v = (Sum f) + (Sum g) by A1, Th1;
( Sum f in Lin A & Sum g in Lin B ) by Th14;
hence v in (Lin A) + (Lin B) by A19, RLSUB_2:1; ::_thesis: verum
end;
then A20: Lin (A \/ B) is Subspace of (Lin A) + (Lin B) by RLSUB_1:29;
( Lin A is Subspace of Lin (A \/ B) & Lin B is Subspace of Lin (A \/ B) ) by Th20, XBOOLE_1:7;
then (Lin A) + (Lin B) is Subspace of Lin (A \/ B) by Lm6;
hence Lin (A \/ B) = (Lin A) + (Lin B) by A20, RLSUB_1:26; ::_thesis: verum
end;
theorem :: RLVECT_3:23
for V being RealLinearSpace
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
proof
let V be RealLinearSpace; ::_thesis: for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
let A, B be Subset of V; ::_thesis: Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
( Lin (A /\ B) is Subspace of Lin A & Lin (A /\ B) is Subspace of Lin B ) by Th20, XBOOLE_1:17;
hence Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) by Lm4; ::_thesis: verum
end;
Lm7: for M being non empty set
for CF being Choice_Function of M st not {} in M holds
dom CF = M
proof
let M be non empty set ; ::_thesis: for CF being Choice_Function of M st not {} in M holds
dom CF = M
let CF be Choice_Function of M; ::_thesis: ( not {} in M implies dom CF = M )
set x = the Element of M;
A1: the Element of M in M ;
assume not {} in M ; ::_thesis: dom CF = M
then union M <> {} by A1, ORDERS_1:6;
hence dom CF = M by FUNCT_2:def_1; ::_thesis: verum
end;
theorem Th24: :: RLVECT_3:24
for V being RealLinearSpace
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )
let A be Subset of V; ::_thesis: ( A is linearly-independent implies ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) )
defpred S1[ set ] means ex B being Subset of V st
( B = $1 & A c= B & B is linearly-independent );
consider Q being set such that
A1: for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) ) from XBOOLE_0:sch_1();
A2: now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=_Q_&_Z_is_c=-linear_holds_
union_Z_in_Q
let Z be set ; ::_thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )
assume that
A3: Z <> {} and
A4: Z c= Q and
A5: Z is c=-linear ; ::_thesis: union Z in Q
set W = union Z;
union Z c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Z or x in the carrier of V )
assume x in union Z ; ::_thesis: x in the carrier of V
then consider X being set such that
A6: x in X and
A7: X in Z by TARSKI:def_4;
X in bool the carrier of V by A1, A4, A7;
hence x in the carrier of V by A6; ::_thesis: verum
end;
then reconsider W = union Z as Subset of V ;
A8: W is linearly-independent
proof
deffunc H1( set ) -> set = { C where C is Subset of V : ( $1 in C & C in Z ) } ;
let l be Linear_Combination of W; :: according to RLVECT_3:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
assume that
A9: Sum l = 0. V and
A10: Carrier l <> {} ; ::_thesis: contradiction
consider f being Function such that
A11: dom f = Carrier l and
A12: for x being set st x in Carrier l holds
f . x = H1(x) from FUNCT_1:sch_3();
reconsider M = rng f as non empty set by A10, A11, RELAT_1:42;
set F = the Choice_Function of M;
set S = rng the Choice_Function of M;
A13: now__::_thesis:_not_{}_in_M
assume {} in M ; ::_thesis: contradiction
then consider x being set such that
A14: x in dom f and
A15: f . x = {} by FUNCT_1:def_3;
Carrier l c= W by RLVECT_2:def_6;
then consider X being set such that
A16: x in X and
A17: X in Z by A11, A14, TARSKI:def_4;
reconsider X = X as Subset of V by A1, A4, A17;
X in { C where C is Subset of V : ( x in C & C in Z ) } by A16, A17;
hence contradiction by A11, A12, A14, A15; ::_thesis: verum
end;
then A18: dom the Choice_Function of M = M by Lm7;
then dom the Choice_Function of M is finite by A11, FINSET_1:8;
then A19: rng the Choice_Function of M is finite by FINSET_1:8;
A20: now__::_thesis:_for_X_being_set_st_X_in_rng_the_Choice_Function_of_M_holds_
X_in_Z
let X be set ; ::_thesis: ( X in rng the Choice_Function of M implies X in Z )
assume X in rng the Choice_Function of M ; ::_thesis: X in Z
then consider x being set such that
A21: x in dom the Choice_Function of M and
A22: the Choice_Function of M . x = X by FUNCT_1:def_3;
consider y being set such that
A23: ( y in dom f & f . y = x ) by A18, A21, FUNCT_1:def_3;
A24: x = H1(y) by A11, A12, A23;
X in x by A13, A18, A21, A22, ORDERS_1:def_1;
then ex C being Subset of V st
( C = X & y in C & C in Z ) by A24;
hence X in Z ; ::_thesis: verum
end;
A25: now__::_thesis:_for_X,_Y_being_set_st_X_in_rng_the_Choice_Function_of_M_&_Y_in_rng_the_Choice_Function_of_M_&_not_X_c=_Y_holds_
Y_c=_X
let X, Y be set ; ::_thesis: ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y implies Y c= X )
assume ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; ::_thesis: ( X c= Y or Y c= X )
then ( X in Z & Y in Z ) by A20;
then X,Y are_c=-comparable by A5, ORDINAL1:def_8;
hence ( X c= Y or Y c= X ) by XBOOLE_0:def_9; ::_thesis: verum
end;
rng the Choice_Function of M <> {} by A18, RELAT_1:42;
then union (rng the Choice_Function of M) in rng the Choice_Function of M by A25, A19, CARD_2:62;
then union (rng the Choice_Function of M) in Z by A20;
then consider B being Subset of V such that
A26: B = union (rng the Choice_Function of M) and
A c= B and
A27: B is linearly-independent by A1, A4;
Carrier l c= union (rng the Choice_Function of M)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in union (rng the Choice_Function of M) )
set X = f . x;
assume A28: x in Carrier l ; ::_thesis: x in union (rng the Choice_Function of M)
then A29: f . x = { C where C is Subset of V : ( x in C & C in Z ) } by A12;
A30: f . x in M by A11, A28, FUNCT_1:def_3;
then the Choice_Function of M . (f . x) in f . x by A13, ORDERS_1:def_1;
then A31: ex C being Subset of V st
( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A29;
the Choice_Function of M . (f . x) in rng the Choice_Function of M by A18, A30, FUNCT_1:def_3;
hence x in union (rng the Choice_Function of M) by A31, TARSKI:def_4; ::_thesis: verum
end;
then l is Linear_Combination of B by A26, RLVECT_2:def_6;
hence contradiction by A9, A10, A27, Def1; ::_thesis: verum
end;
set x = the Element of Z;
the Element of Z in Q by A3, A4, TARSKI:def_3;
then A32: ex B being Subset of V st
( B = the Element of Z & A c= B & B is linearly-independent ) by A1;
the Element of Z c= W by A3, ZFMISC_1:74;
then A c= W by A32, XBOOLE_1:1;
hence union Z in Q by A1, A8; ::_thesis: verum
end;
A33: (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ;
assume A is linearly-independent ; ::_thesis: ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )
then Q <> {} by A1;
then consider X being set such that
A34: X in Q and
A35: for Z being set st Z in Q & Z <> X holds
not X c= Z by A2, ORDERS_1:67;
consider B being Subset of V such that
A36: B = X and
A37: A c= B and
A38: B is linearly-independent by A1, A34;
take B ; ::_thesis: ( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )
thus ( A c= B & B is linearly-independent ) by A37, A38; ::_thesis: Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #)
assume Lin B <> RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ; ::_thesis: contradiction
then consider v being VECTOR of V such that
A39: ( ( v in Lin B & not v in RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) or ( v in RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) & not v in Lin B ) ) by A33, RLSUB_1:31;
A40: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v}; :: according to RLVECT_3:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
assume A41: Sum l = 0. V ; ::_thesis: Carrier l = {}
now__::_thesis:_Carrier_l_=_{}
percases ( v in Carrier l or not v in Carrier l ) ;
suppose v in Carrier l ; ::_thesis: Carrier l = {}
then A42: - (l . v) <> 0 by RLVECT_2:19;
deffunc H1( VECTOR of V) -> Element of NAT = 0 ;
deffunc H2( VECTOR of V) -> Element of REAL = l . $1;
consider f being Function of the carrier of V,REAL such that
A43: f . v = 0 and
A44: for u being VECTOR of V st u <> v holds
f . u = H2(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_(Carrier_l)_\_{v}_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in (Carrier l) \ {v} implies f . u = 0 )
assume not u in (Carrier l) \ {v} ; ::_thesis: f . u = 0
then ( not u in Carrier l or u in {v} ) by XBOOLE_0:def_5;
then ( ( l . u = 0 & u <> v ) or u = v ) by TARSKI:def_1;
hence f . u = 0 by A43, A44; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
Carrier f c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in B )
A45: Carrier l c= B \/ {v} by RLVECT_2:def_6;
assume x in Carrier f ; ::_thesis: x in B
then consider u being VECTOR of V such that
A46: u = x and
A47: f . u <> 0 ;
f . u = l . u by A43, A44, A47;
then u in Carrier l by A47;
then ( u in B or u in {v} ) by A45, XBOOLE_0:def_3;
hence x in B by A43, A46, A47, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of B by RLVECT_2:def_6;
consider g being Function of the carrier of V,REAL such that
A48: g . v = - (l . v) and
A49: for u being VECTOR of V st u <> v holds
g . u = H1(u) from FUNCT_2:sch_6();
reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v}_holds_
g_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in {v} implies g . u = 0 )
assume not u in {v} ; ::_thesis: g . u = 0
then u <> v by TARSKI:def_1;
hence g . u = 0 by A49; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def_3;
Carrier g c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in {v} )
assume x in Carrier g ; ::_thesis: x in {v}
then ex u being VECTOR of V st
( x = u & g . u <> 0 ) ;
then x = v by A49;
hence x in {v} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of {v} by RLVECT_2:def_6;
A50: Sum g = (- (l . v)) * v by A48, RLVECT_2:32;
f - g = l
proof
let u be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (f - g) . u = l . u
now__::_thesis:_(f_-_g)_._u_=_l_._u
percases ( v = u or v <> u ) ;
supposeA51: v = u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= l . u by A43, A48, A51 ; ::_thesis: verum
end;
supposeA52: v <> u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= (l . u) - (g . u) by A44, A52
.= (l . u) - 0 by A49, A52
.= l . u ; ::_thesis: verum
end;
end;
end;
hence (f - g) . u = l . u ; ::_thesis: verum
end;
then 0. V = (Sum f) - (Sum g) by A41, Th4;
then Sum f = (0. V) + (Sum g) by RLSUB_2:61
.= (- (l . v)) * v by A50, RLVECT_1:4 ;
then A53: (- (l . v)) * v in Lin B by Th14;
((- (l . v)) ") * ((- (l . v)) * v) = (((- (l . v)) ") * (- (l . v))) * v by RLVECT_1:def_7
.= 1 * v by A42, XCMPLX_0:def_7
.= v by RLVECT_1:def_8 ;
hence Carrier l = {} by A39, A53, RLSUB_1:21, RLVECT_1:1; ::_thesis: verum
end;
supposeA54: not v in Carrier l ; ::_thesis: Carrier l = {}
Carrier l c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in B )
assume A55: x in Carrier l ; ::_thesis: x in B
Carrier l c= B \/ {v} by RLVECT_2:def_6;
then ( x in B or x in {v} ) by A55, XBOOLE_0:def_3;
hence x in B by A54, A55, TARSKI:def_1; ::_thesis: verum
end;
then l is Linear_Combination of B by RLVECT_2:def_6;
hence Carrier l = {} by A38, A41, Def1; ::_thesis: verum
end;
end;
end;
hence Carrier l = {} ; ::_thesis: verum
end;
v in {v} by TARSKI:def_1;
then A56: v in B \/ {v} by XBOOLE_0:def_3;
A57: not v in B by A39, Th15, RLVECT_1:1;
B c= B \/ {v} by XBOOLE_1:7;
then A c= B \/ {v} by A37, XBOOLE_1:1;
then B \/ {v} in Q by A1, A40;
hence contradiction by A35, A36, A56, A57, XBOOLE_1:7; ::_thesis: verum
end;
theorem Th25: :: RLVECT_3:25
for V being RealLinearSpace
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
let A be Subset of V; ::_thesis: ( Lin A = V implies ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V ) )
assume A1: Lin A = V ; ::_thesis: ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
defpred S1[ set ] means ex B being Subset of V st
( B = $1 & B c= A & B is linearly-independent );
consider Q being set such that
A2: for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) ) from XBOOLE_0:sch_1();
A3: now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=_Q_&_Z_is_c=-linear_holds_
union_Z_in_Q
let Z be set ; ::_thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )
assume that
Z <> {} and
A4: Z c= Q and
A5: Z is c=-linear ; ::_thesis: union Z in Q
set W = union Z;
union Z c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Z or x in the carrier of V )
assume x in union Z ; ::_thesis: x in the carrier of V
then consider X being set such that
A6: x in X and
A7: X in Z by TARSKI:def_4;
X in bool the carrier of V by A2, A4, A7;
hence x in the carrier of V by A6; ::_thesis: verum
end;
then reconsider W = union Z as Subset of V ;
A8: W is linearly-independent
proof
deffunc H1( set ) -> set = { C where C is Subset of V : ( $1 in C & C in Z ) } ;
let l be Linear_Combination of W; :: according to RLVECT_3:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
assume that
A9: Sum l = 0. V and
A10: Carrier l <> {} ; ::_thesis: contradiction
consider f being Function such that
A11: dom f = Carrier l and
A12: for x being set st x in Carrier l holds
f . x = H1(x) from FUNCT_1:sch_3();
reconsider M = rng f as non empty set by A10, A11, RELAT_1:42;
set F = the Choice_Function of M;
set S = rng the Choice_Function of M;
A13: now__::_thesis:_not_{}_in_M
assume {} in M ; ::_thesis: contradiction
then consider x being set such that
A14: x in dom f and
A15: f . x = {} by FUNCT_1:def_3;
Carrier l c= W by RLVECT_2:def_6;
then consider X being set such that
A16: x in X and
A17: X in Z by A11, A14, TARSKI:def_4;
reconsider X = X as Subset of V by A2, A4, A17;
X in { C where C is Subset of V : ( x in C & C in Z ) } by A16, A17;
hence contradiction by A11, A12, A14, A15; ::_thesis: verum
end;
then A18: dom the Choice_Function of M = M by Lm7;
then dom the Choice_Function of M is finite by A11, FINSET_1:8;
then A19: rng the Choice_Function of M is finite by FINSET_1:8;
A20: now__::_thesis:_for_X_being_set_st_X_in_rng_the_Choice_Function_of_M_holds_
X_in_Z
let X be set ; ::_thesis: ( X in rng the Choice_Function of M implies X in Z )
assume X in rng the Choice_Function of M ; ::_thesis: X in Z
then consider x being set such that
A21: x in dom the Choice_Function of M and
A22: the Choice_Function of M . x = X by FUNCT_1:def_3;
consider y being set such that
A23: ( y in dom f & f . y = x ) by A18, A21, FUNCT_1:def_3;
A24: x = { C where C is Subset of V : ( y in C & C in Z ) } by A11, A12, A23;
X in x by A13, A18, A21, A22, ORDERS_1:def_1;
then ex C being Subset of V st
( C = X & y in C & C in Z ) by A24;
hence X in Z ; ::_thesis: verum
end;
A25: now__::_thesis:_for_X,_Y_being_set_st_X_in_rng_the_Choice_Function_of_M_&_Y_in_rng_the_Choice_Function_of_M_&_not_X_c=_Y_holds_
Y_c=_X
let X, Y be set ; ::_thesis: ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y implies Y c= X )
assume ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; ::_thesis: ( X c= Y or Y c= X )
then ( X in Z & Y in Z ) by A20;
then X,Y are_c=-comparable by A5, ORDINAL1:def_8;
hence ( X c= Y or Y c= X ) by XBOOLE_0:def_9; ::_thesis: verum
end;
rng the Choice_Function of M <> {} by A18, RELAT_1:42;
then union (rng the Choice_Function of M) in rng the Choice_Function of M by A25, A19, CARD_2:62;
then union (rng the Choice_Function of M) in Z by A20;
then consider B being Subset of V such that
A26: B = union (rng the Choice_Function of M) and
B c= A and
A27: B is linearly-independent by A2, A4;
Carrier l c= union (rng the Choice_Function of M)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in union (rng the Choice_Function of M) )
set X = f . x;
assume A28: x in Carrier l ; ::_thesis: x in union (rng the Choice_Function of M)
then A29: f . x = { C where C is Subset of V : ( x in C & C in Z ) } by A12;
A30: f . x in M by A11, A28, FUNCT_1:def_3;
then the Choice_Function of M . (f . x) in f . x by A13, ORDERS_1:def_1;
then A31: ex C being Subset of V st
( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A29;
the Choice_Function of M . (f . x) in rng the Choice_Function of M by A18, A30, FUNCT_1:def_3;
hence x in union (rng the Choice_Function of M) by A31, TARSKI:def_4; ::_thesis: verum
end;
then l is Linear_Combination of B by A26, RLVECT_2:def_6;
hence contradiction by A9, A10, A27, Def1; ::_thesis: verum
end;
W c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W or x in A )
assume x in W ; ::_thesis: x in A
then consider X being set such that
A32: x in X and
A33: X in Z by TARSKI:def_4;
ex B being Subset of V st
( B = X & B c= A & B is linearly-independent ) by A2, A4, A33;
hence x in A by A32; ::_thesis: verum
end;
hence union Z in Q by A2, A8; ::_thesis: verum
end;
( {} the carrier of V c= A & {} the carrier of V is linearly-independent ) by Th7, XBOOLE_1:2;
then Q <> {} by A2;
then consider X being set such that
A34: X in Q and
A35: for Z being set st Z in Q & Z <> X holds
not X c= Z by A3, ORDERS_1:67;
consider B being Subset of V such that
A36: B = X and
A37: B c= A and
A38: B is linearly-independent by A2, A34;
take B ; ::_thesis: ( B c= A & B is linearly-independent & Lin B = V )
thus ( B c= A & B is linearly-independent ) by A37, A38; ::_thesis: Lin B = V
assume A39: Lin B <> V ; ::_thesis: contradiction
now__::_thesis:_ex_v_being_VECTOR_of_V_st_
(_v_in_A_&_not_v_in_Lin_B_)
assume A40: for v being VECTOR of V st v in A holds
v in Lin B ; ::_thesis: contradiction
now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_Lin_A_holds_
v_in_Lin_B
reconsider F = the carrier of (Lin B) as Subset of V by RLSUB_1:def_2;
let v be VECTOR of V; ::_thesis: ( v in Lin A implies v in Lin B )
assume v in Lin A ; ::_thesis: v in Lin B
then consider l being Linear_Combination of A such that
A41: v = Sum l by Th14;
Carrier l c= the carrier of (Lin B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in the carrier of (Lin B) )
assume A42: x in Carrier l ; ::_thesis: x in the carrier of (Lin B)
then reconsider a = x as VECTOR of V ;
Carrier l c= A by RLVECT_2:def_6;
then a in Lin B by A40, A42;
hence x in the carrier of (Lin B) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider l = l as Linear_Combination of F by RLVECT_2:def_6;
Sum l = v by A41;
then v in Lin F by Th14;
hence v in Lin B by Th18; ::_thesis: verum
end;
then Lin A is Subspace of Lin B by RLSUB_1:29;
hence contradiction by A1, A39, RLSUB_1:26; ::_thesis: verum
end;
then consider v being VECTOR of V such that
A43: v in A and
A44: not v in Lin B ;
A45: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v}; :: according to RLVECT_3:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
assume A46: Sum l = 0. V ; ::_thesis: Carrier l = {}
now__::_thesis:_Carrier_l_=_{}
percases ( v in Carrier l or not v in Carrier l ) ;
suppose v in Carrier l ; ::_thesis: Carrier l = {}
then A47: - (l . v) <> 0 by RLVECT_2:19;
deffunc H1( VECTOR of V) -> Element of NAT = 0 ;
deffunc H2( VECTOR of V) -> Element of REAL = l . $1;
consider f being Function of the carrier of V,REAL such that
A48: f . v = 0 and
A49: for u being VECTOR of V st u <> v holds
f . u = H2(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_(Carrier_l)_\_{v}_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in (Carrier l) \ {v} implies f . u = 0 )
assume not u in (Carrier l) \ {v} ; ::_thesis: f . u = 0
then ( not u in Carrier l or u in {v} ) by XBOOLE_0:def_5;
then ( ( l . u = 0 & u <> v ) or u = v ) by TARSKI:def_1;
hence f . u = 0 by A48, A49; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
Carrier f c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in B )
A50: Carrier l c= B \/ {v} by RLVECT_2:def_6;
assume x in Carrier f ; ::_thesis: x in B
then consider u being VECTOR of V such that
A51: u = x and
A52: f . u <> 0 ;
f . u = l . u by A48, A49, A52;
then u in Carrier l by A52;
then ( u in B or u in {v} ) by A50, XBOOLE_0:def_3;
hence x in B by A48, A51, A52, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of B by RLVECT_2:def_6;
consider g being Function of the carrier of V,REAL such that
A53: g . v = - (l . v) and
A54: for u being VECTOR of V st u <> v holds
g . u = H1(u) from FUNCT_2:sch_6();
reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v}_holds_
g_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in {v} implies g . u = 0 )
assume not u in {v} ; ::_thesis: g . u = 0
then u <> v by TARSKI:def_1;
hence g . u = 0 by A54; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def_3;
Carrier g c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in {v} )
assume x in Carrier g ; ::_thesis: x in {v}
then ex u being VECTOR of V st
( x = u & g . u <> 0 ) ;
then x = v by A54;
hence x in {v} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of {v} by RLVECT_2:def_6;
A55: Sum g = (- (l . v)) * v by A53, RLVECT_2:32;
f - g = l
proof
let u be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (f - g) . u = l . u
now__::_thesis:_(f_-_g)_._u_=_l_._u
percases ( v = u or v <> u ) ;
supposeA56: v = u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= l . u by A48, A53, A56 ; ::_thesis: verum
end;
supposeA57: v <> u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= (l . u) - (g . u) by A49, A57
.= (l . u) - 0 by A54, A57
.= l . u ; ::_thesis: verum
end;
end;
end;
hence (f - g) . u = l . u ; ::_thesis: verum
end;
then 0. V = (Sum f) - (Sum g) by A46, Th4;
then Sum f = (0. V) + (Sum g) by RLSUB_2:61
.= (- (l . v)) * v by A55, RLVECT_1:4 ;
then A58: (- (l . v)) * v in Lin B by Th14;
((- (l . v)) ") * ((- (l . v)) * v) = (((- (l . v)) ") * (- (l . v))) * v by RLVECT_1:def_7
.= 1 * v by A47, XCMPLX_0:def_7
.= v by RLVECT_1:def_8 ;
hence Carrier l = {} by A44, A58, RLSUB_1:21; ::_thesis: verum
end;
supposeA59: not v in Carrier l ; ::_thesis: Carrier l = {}
Carrier l c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in B )
assume A60: x in Carrier l ; ::_thesis: x in B
Carrier l c= B \/ {v} by RLVECT_2:def_6;
then ( x in B or x in {v} ) by A60, XBOOLE_0:def_3;
hence x in B by A59, A60, TARSKI:def_1; ::_thesis: verum
end;
then l is Linear_Combination of B by RLVECT_2:def_6;
hence Carrier l = {} by A38, A46, Def1; ::_thesis: verum
end;
end;
end;
hence Carrier l = {} ; ::_thesis: verum
end;
{v} c= A by A43, ZFMISC_1:31;
then B \/ {v} c= A by A37, XBOOLE_1:8;
then A61: B \/ {v} in Q by A2, A45;
v in {v} by TARSKI:def_1;
then A62: v in B \/ {v} by XBOOLE_0:def_3;
not v in B by A44, Th15;
hence contradiction by A35, A36, A62, A61, XBOOLE_1:7; ::_thesis: verum
end;
definition
let V be RealLinearSpace;
mode Basis of V -> Subset of V means :Def3: :: RLVECT_3:def 3
( it is linearly-independent & Lin it = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) );
existence
ex b1 being Subset of V st
( b1 is linearly-independent & Lin b1 = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )
proof
{} the carrier of V is linearly-independent by Th7;
then ex B being Subset of V st
( {} the carrier of V c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) by Th24;
hence ex b1 being Subset of V st
( b1 is linearly-independent & Lin b1 = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Basis RLVECT_3:def_3_:_
for V being RealLinearSpace
for b2 being Subset of V holds
( b2 is Basis of V iff ( b2 is linearly-independent & Lin b2 = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) );
theorem :: RLVECT_3:26
for V being strict RealLinearSpace
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
proof
let V be strict RealLinearSpace; ::_thesis: for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
let A be Subset of V; ::_thesis: ( A is linearly-independent implies ex I being Basis of V st A c= I )
assume A is linearly-independent ; ::_thesis: ex I being Basis of V st A c= I
then consider B being Subset of V such that
A1: A c= B and
A2: ( B is linearly-independent & Lin B = V ) by Th24;
reconsider B = B as Basis of V by A2, Def3;
take B ; ::_thesis: A c= B
thus A c= B by A1; ::_thesis: verum
end;
theorem :: RLVECT_3:27
for V being RealLinearSpace
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
let A be Subset of V; ::_thesis: ( Lin A = V implies ex I being Basis of V st I c= A )
assume Lin A = V ; ::_thesis: ex I being Basis of V st I c= A
then consider B being Subset of V such that
A1: B c= A and
A2: ( B is linearly-independent & Lin B = V ) by Th25;
reconsider B = B as Basis of V by A2, Def3;
take B ; ::_thesis: B c= A
thus B c= A by A1; ::_thesis: verum
end;
theorem :: RLVECT_3:28
for M being non empty set
for CF being Choice_Function of M st not {} in M holds
dom CF = M by Lm7;
theorem :: RLVECT_3:29
for x being set
for V being RealLinearSpace holds
( x in (0). V iff x = 0. V ) by Lm2;
theorem :: RLVECT_3:30
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 by Lm3;
theorem :: RLVECT_3:31
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 by Lm4;
theorem :: RLVECT_3:32
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 by Lm6;
theorem :: RLVECT_3:33
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 by Lm5;
theorem :: RLVECT_3:34
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) by Lm1;