:: Linear Combinations in Right Module over Associative Ring
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCSDOM, VECTSP_2, VECTSP_1, FINSEQ_1, NAT_1, SUBSET_1,
FUNCT_1, FINSET_1, ARYTM_3, RELAT_1, CARD_3, XXREAL_0, TARSKI, CARD_1,
STRUCT_0, SUPINF_2, PARTFUN1, XBOOLE_0, ORDINAL4, ARYTM_1, RLVECT_2,
FUNCT_2, FUNCOP_1, VALUED_1, GROUP_1, RLSUB_1, FINSEQ_4, RLVECT_3,
RMOD_2;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, FINSET_1, FINSEQ_1, ORDINAL1,
NUMBERS, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, CARD_1, DOMAIN_1,
STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, FINSEQ_4, VECTSP_2,
RMOD_2, RMOD_3, FUNCOP_1, XXREAL_0;
constructors PARTFUN1, DOMAIN_1, FUNCOP_1, XXREAL_0, NAT_1, FINSEQ_4,
RLVECT_2, RMOD_2, RMOD_3, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, XREAL_0,
STRUCT_0, VECTSP_1, ORDINAL1, FINSEQ_1, VECTSP_2, RMOD_2, CARD_1;
requirements NUMERALS, REAL, BOOLE, SUBSET;
begin
reserve R for Ring,
V for RightMod of R,
a,b for Scalar of R,
x,y for set,
p,q ,r for FinSequence,
i,k for Nat,
u,v,v1,v2,v3,w for Vector of V,
F,G,H for FinSequence of V,
A,B for Subset of V,
f for Function of V, R,
S,T for finite Subset of V;
theorem :: RMOD_4:1
len F = len G & (for k,v st k in dom F & v = G.k holds F.k = v *
a) implies Sum(F) = Sum(G) * a;
theorem :: RMOD_4:2
Sum(<*>(the carrier of V)) * a = 0.V;
theorem :: RMOD_4:3
Sum<* v,u *> * a = v * a + u * a;
theorem :: RMOD_4:4
Sum<* v,u,w *> * a = v * a + u * a + w * a;
definition
let R, V, T;
func Sum(T) -> Vector of V means
:: RMOD_4:def 1
ex F st rng F = T & F is one-to-one & it = Sum(F);
end;
theorem :: RMOD_4:5
Sum({}V) = 0.V;
theorem :: RMOD_4:6
Sum{v} = v;
theorem :: RMOD_4:7
v1 <> v2 implies Sum{v1,v2} = v1 + v2;
theorem :: RMOD_4:8
v1 <> v2 & v2 <> v3 & v1 <> v3 implies Sum{v1,v2,v3} = v1 + v2 + v3;
theorem :: RMOD_4:9
T misses S implies Sum(T \/ S) = Sum(T) + Sum(S);
theorem :: RMOD_4:10
Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S);
theorem :: RMOD_4:11
Sum(T /\ S) = Sum(T) + Sum(S) - Sum(T \/ S);
theorem :: RMOD_4:12
Sum(T \ S) = Sum(T \/ S) - Sum(S);
theorem :: RMOD_4:13
Sum(T \ S) = Sum(T) - Sum(T /\ S);
theorem :: RMOD_4:14
Sum(T \+\ S) = Sum(T \/ S) - Sum(T /\ S);
theorem :: RMOD_4:15
Sum(T \+\ S) = Sum(T \ S) + Sum(S \ T);
definition
let R, V;
mode Linear_Combination of V -> Element of Funcs(the carrier of V, the
carrier of R) means
:: RMOD_4:def 2
ex T st for v st not v in T holds it.v = 0.R;
end;
reserve L,L1,L2,L3 for Linear_Combination of V;
definition
let R, V, L;
func Carrier(L) -> finite Subset of V equals
:: RMOD_4:def 3
{v : L.v <> 0.R};
end;
theorem :: RMOD_4:16
x in Carrier(L) iff ex v st x = v & L.v <> 0.R;
theorem :: RMOD_4:17
L.v = 0.R iff not v in Carrier(L);
definition
let R, V;
func ZeroLC(V) -> Linear_Combination of V means
:: RMOD_4:def 4
Carrier(it) = {};
end;
theorem :: RMOD_4:18
ZeroLC(V).v = 0.R;
definition
let R, V, A;
mode Linear_Combination of A -> Linear_Combination of V means
:: RMOD_4:def 5
Carrier (it) c= A;
end;
reserve l for Linear_Combination of A;
theorem :: RMOD_4:19
A c= B implies l is Linear_Combination of B;
theorem :: RMOD_4:20
ZeroLC(V) is Linear_Combination of A;
theorem :: RMOD_4:21
for l being Linear_Combination of {}(the carrier of V) holds l = ZeroLC(V);
theorem :: RMOD_4:22
L is Linear_Combination of Carrier(L);
definition
let R, V, F, f;
func f (#) F -> FinSequence of V means
:: RMOD_4:def 6
len it = len F & for i being
Nat st i in dom it holds it.i = (F/.i) * f.(F/.i);
end;
theorem :: RMOD_4:23
i in dom F & v = F.i implies (f (#) F).i = v * f.v;
theorem :: RMOD_4:24
f (#) <*>(the carrier of V) = <*>(the carrier of V);
theorem :: RMOD_4:25
f (#) <* v *> = <* v * f.v *>;
theorem :: RMOD_4:26
f (#) <* v1,v2 *> = <* v1 * f.v1, v2 * f.v2 *>;
theorem :: RMOD_4:27
f (#) <* v1,v2,v3 *> = <* v1 * f.v1, v2 * f.v2, v3 * f.v3 *>;
theorem :: RMOD_4:28
f (#) (F ^ G) = (f (#) F) ^ (f (#) G);
definition
let R, V, L;
func Sum(L) -> Vector of V means
:: RMOD_4:def 7
ex F st F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
end;
theorem :: RMOD_4:29
0.R <> 1_R implies (A <> {} & A is linearly-closed iff for l
holds Sum l in A);
theorem :: RMOD_4:30
Sum(ZeroLC(V)) = 0.V;
theorem :: RMOD_4:31
for l being Linear_Combination of {}(the carrier of V) holds Sum (l) = 0.V;
theorem :: RMOD_4:32
for l being Linear_Combination of {v} holds Sum(l) = v * l.v;
theorem :: RMOD_4:33
v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds
Sum (l) = v1 * l.v1 + v2 * l.v2;
theorem :: RMOD_4:34
Carrier(L) = {} implies Sum(L) = 0.V;
theorem :: RMOD_4:35
Carrier(L) = {v} implies Sum(L) = v * L.v;
theorem :: RMOD_4:36
Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = v1 * L.v1 + v2 * L.v2;
definition
let R, V, L1, L2;
redefine pred L1 = L2 means
:: RMOD_4:def 8
for v holds L1.v = L2.v;
end;
definition
let R, V, L1, L2;
func L1 + L2 -> Linear_Combination of V means
:: RMOD_4:def 9
for v holds it.v = L1. v + L2.v;
end;
theorem :: RMOD_4:37
Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2);
theorem :: RMOD_4:38
L1 is Linear_Combination of A & L2 is Linear_Combination of A
implies L1 + L2 is Linear_Combination of A;
theorem :: RMOD_4:39
for R being comRing for V being RightMod of R for L1, L2 being
Linear_Combination of V holds L1 + L2 = L2 + L1;
theorem :: RMOD_4:40
L1 + (L2 + L3) = L1 + L2 + L3;
theorem :: RMOD_4:41
for R being comRing for V being RightMod of R for L being
Linear_Combination of V holds L + ZeroLC(V) = L & ZeroLC(V) + L = L;
definition
let R, V, a, L;
func L * a -> Linear_Combination of V means
:: RMOD_4:def 10
for v holds it.v = L.v * a;
end;
theorem :: RMOD_4:42
Carrier(L * a) c= Carrier(L);
reserve RR for domRing;
reserve VV for RightMod of RR;
reserve LL for Linear_Combination of VV;
reserve aa for Scalar of RR;
reserve uu, vv for Vector of VV;
theorem :: RMOD_4:43
aa <> 0.RR implies Carrier(LL * aa) = Carrier(LL);
theorem :: RMOD_4:44
L * 0.R = ZeroLC(V);
theorem :: RMOD_4:45
L is Linear_Combination of A implies L * a is Linear_Combination of A;
theorem :: RMOD_4:46
L * (a + b) = L * a + L * b;
theorem :: RMOD_4:47
(L1 + L2) * a = L1 * a + L2 * a;
theorem :: RMOD_4:48
(L * b) * a = L * (b * a);
theorem :: RMOD_4:49
L * 1_R = L;
definition
let R, V, L;
func - L -> Linear_Combination of V equals
:: RMOD_4:def 11
L * (- 1_R);
involutiveness;
end;
theorem :: RMOD_4:50
(- L).v = - L.v;
theorem :: RMOD_4:51
L1 + L2 = ZeroLC(V) implies L2 = - L1;
theorem :: RMOD_4:52
Carrier(- L) = Carrier(L);
theorem :: RMOD_4:53
L is Linear_Combination of A implies - L is Linear_Combination of A;
definition
let R, V, L1, L2;
func L1 - L2 -> Linear_Combination of V equals
:: RMOD_4:def 12
L1 + (- L2);
end;
theorem :: RMOD_4:54
(L1 - L2).v = L1.v - L2.v;
theorem :: RMOD_4:55
Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2);
theorem :: RMOD_4:56
L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
L1 - L2 is Linear_Combination of A;
theorem :: RMOD_4:57
L - L = ZeroLC(V);
theorem :: RMOD_4:58
Sum(L1 + L2) = Sum(L1) + Sum(L2);
reserve R for domRing;
reserve V for RightMod of R;
reserve L,L1,L2 for Linear_Combination of V;
reserve a for Scalar of R;
theorem :: RMOD_4:59
Sum(L * a) = Sum(L) * a;
theorem :: RMOD_4:60
Sum(- L) = - Sum(L);
theorem :: RMOD_4:61
Sum(L1 - L2) = Sum(L1) - Sum(L2);
begin :: RMOD_5
reserve x for set;
reserve R for Ring;
reserve V for RightMod of R;
reserve v,v1,v2 for Vector of V;
reserve A,B for Subset of V;
definition
let R, V;
let IT be Subset of V;
attr IT is linearly-independent means
:: RMOD_4:def 13
for l being Linear_Combination of IT st Sum(l) = 0.V holds Carrier(l) = {};
end;
notation
let R, V;
let IT be Subset of V;
antonym IT is linearly-dependent for IT is linearly-independent;
end;
theorem :: RMOD_4:62
A c= B & B is linearly-independent implies A is linearly-independent;
theorem :: RMOD_4:63
0.R <> 1_R & A is linearly-independent implies not 0.V in A;
theorem :: RMOD_4:64
{}(the carrier of V) is linearly-independent;
theorem :: RMOD_4:65
0.R <> 1_R & {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V;
theorem :: RMOD_4:66
0.R <> 1_R implies {v,0.V} is linearly-dependent & {0.V,v} is
linearly-dependent;
reserve R for domRing;
reserve V for RightMod of R;
reserve v,u for Vector of V;
reserve A,B for Subset of V;
reserve l for Linear_Combination of A;
reserve f,g for Function of the carrier of V, the carrier of R;
definition
let R, V, A;
func Lin(A) -> strict Submodule of V means
:: RMOD_4:def 14
the carrier of it = the set of all Sum( l) ;
end;
theorem :: RMOD_4:67
x in Lin(A) iff ex l st x = Sum(l);
theorem :: RMOD_4:68
x in A implies x in Lin(A);
theorem :: RMOD_4:69
Lin({}(the carrier of V)) = (0).V;
theorem :: RMOD_4:70
Lin(A) = (0).V implies A = {} or A = {0.V};
theorem :: RMOD_4:71
for W being strict Submodule of V st 0.R <> 1_R & A = the
carrier of W holds Lin(A) = W;
theorem :: RMOD_4:72
for V being strict RightMod of R, A being Subset of V st 0.R <> 1_R &
A = the carrier of V holds Lin(A) = V;
theorem :: RMOD_4:73
A c= B implies Lin(A) is Submodule of Lin(B);
theorem :: RMOD_4:74
for V being strict RightMod of R, A,B being Subset of V st Lin(A) = V
& A c= B holds Lin(B) = V;
theorem :: RMOD_4:75
Lin(A \/ B) = Lin(A) + Lin(B);
theorem :: RMOD_4:76
Lin(A /\ B) is Submodule of Lin(A) /\ Lin(B);