:: 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;