Copyright (c) 1992 Association of Mizar Users
environ
vocabulary FUNCSDOM, VECTSP_1, VECTSP_2, RLVECT_2, RLSUB_2, RMOD_3, FUNCT_1,
RLSUB_1, RELAT_1, RLVECT_1, REALSET1, QC_LANG1, SUBSET_1, RLVECT_3,
BOOLE, PARTFUN1, ARYTM_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, BINOP_1, REALSET1,
RLVECT_1, STRUCT_0, VECTSP_1, FUNCSDOM, VECTSP_2, VECTSP_4, VECTSP_5,
VECTSP_6, MOD_3, PRE_TOPC;
constructors BINOP_1, DOMAIN_1, REALSET1, VECTSP_5, VECTSP_6, MOD_3, PRE_TOPC,
VECTSP_2, MEMBERED, XBOOLE_0;
clusters VECTSP_1, VECTSP_2, VECTSP_4, STRUCT_0, RELSET_1, MEMBERED, ZFMISC_1,
XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
theorems FUNCT_2, MOD_3, TARSKI, VECTSP_1, VECTSP_2, RLVECT_1, ANPROJ_1,
VECTSP_4, VECTSP_5, VECTSP_6, PRE_TOPC, XBOOLE_1, RELAT_1;
begin
reserve x for set,
K for Ring,
r for Scalar of K,
V, M, M1, M2, N for LeftMod of K,
a for Vector of V,
m, m1, m2 for Vector of M,
n, n1, n2 for Vector of N,
A for Subset of V,
l for Linear_Combination of A,
W, W1, W2, W3 for Subspace of V;
definition let K, V;
redefine func Subspaces(V);
synonym Submodules(V);
end;
theorem
M1 = the VectSpStr of M2 implies (x in M1 iff x in M2)
proof assume A1: M1 = the VectSpStr of M2;
x in M1 iff x in the carrier of M1 by RLVECT_1:def 1;
hence thesis by A1,RLVECT_1:def 1;
end;
theorem
for v being Vector of the VectSpStr of V st a=v holds r*a = r*v
proof let v be Vector of (the VectSpStr of V)
such that
A1: a=v;
thus r*a = (the lmult of V).(r,a) by VECTSP_1:def 24
.= r*v by A1,VECTSP_1:def 24;
end;
theorem
Th3: the VectSpStr of V is strict Subspace of V
proof (Omega).V = the VectSpStr of V by VECTSP_4:def 4;hence thesis;end;
theorem
Th4: V is Subspace of (Omega).V
proof set W=(Omega).V;
A1: W = the VectSpStr of V by VECTSP_4:def 4;
A2: dom(the add of W) =
[:the carrier of W,the carrier of W:] by FUNCT_2:def 1;
dom(the lmult of W)
= [:the carrier of K, the carrier of W:] by FUNCT_2:def 1;
then the carrier of V c= the carrier of W &
the Zero of V = the Zero of W &
the add of V = (the add of W) |
[:the carrier of V,the carrier of V:] &
the lmult of V = (the lmult of W) |
[:the carrier of K, the carrier of V:] by A1,A2,RELAT_1:97;
hence thesis by VECTSP_4:def 2;
end;
begin
definition let K;
redefine canceled;
attr K is trivial means
:Def2:
0.K = 1_ K;
compatibility
proof thus K is trivial implies 0.K = 1_ K by ANPROJ_1:def 8;
assume
A1: 0.K = 1_ K;
now let x be Scalar of K;
thus x = x*(1_ K) by VECTSP_2:def 2
.= 0.K by A1,VECTSP_1:36;
end;
hence K is trivial by ANPROJ_1:def 8;
end;
end;
theorem Th5:
K is trivial implies (for r holds r = 0.K) & (for a holds a = 0.V)
proof assume K is trivial;
then A1: 0.K = 1_ K by Def2;
A2: now let r; thus r = r*1_ K by VECTSP_2:def 2
.= 0.K by A1,VECTSP_1:36;end;
now let a; thus a = 1_ K*a by VECTSP_1:def 26 .= 0.V by A1,VECTSP_1:59;
end;
hence thesis by A2;
end;
theorem
K is trivial implies V is trivial
proof assume
A1: K is trivial & V is non trivial;
then ex a st a <> 0.V by ANPROJ_1:def 8;
hence contradiction by A1,Th5;
end;
theorem
V is trivial iff the VectSpStr of V = (0).V
proof
reconsider W = the VectSpStr of V as strict Subspace of V by Th3;
reconsider Z=(0).V as Subspace of W by VECTSP_4:50;
set X = the carrier of (0).V;
A1: now assume V is non trivial;
then consider a such that
A2: a <> 0.V by ANPROJ_1:def 8;
not a in {0.V} by A2,TARSKI:def 1;
then not a in X by VECTSP_4:def 3;
hence W <> (0).V;end;
now assume
W <> Z;
then consider a such that
A3: not a in Z by VECTSP_4:40;
not a in X by A3,RLVECT_1:def 1;
then not a in {0.V} by VECTSP_4:def 3;
then a <> 0.V by TARSKI:def 1;
hence V is non trivial by ANPROJ_1:def 8;end;
hence thesis by A1;
end;
begin ::
:: 1. Submodules and subsets
::
definition let K,V; let W be strict Subspace of V;
func @W -> Element of Submodules(V) equals W;
coherence by VECTSP_5:def 3;
end;
canceled;
theorem Th9:
for A being Subset of W holds A is Subset of V
proof let A be Subset of W;
the carrier of W c= the carrier of V by VECTSP_4:def 2;
then A is Subset of V by XBOOLE_1:1;
hence thesis;
end;
definition let K,V,W; let A be Subset of W;
canceled;
func @A -> Subset of V equals
:Def5: A;
coherence by Th9;
end;
definition let K,V,W; let A be non empty Subset of W;
cluster @A -> non empty;
coherence by Def5;
end;
theorem Th10:
x in [#]V iff x in V
proof
[#]V = the carrier of V by PRE_TOPC:12;
hence thesis by RLVECT_1:def 1;
end;
theorem
x in @[#]W iff x in W
proof
@[#]W = [#]W by Def5;
hence thesis by Th10;
end;
theorem Th12:
A c= [#]Lin(A)
proof let x; assume x in A; then x in Lin(A) by MOD_3:12;
hence thesis by Th10;
end;
theorem Th13:
A<>{} & A is lineary-closed implies Sum(l) in A
proof assume
A1: A<>{} & A is lineary-closed;
now per cases;
suppose 0.K<>1_ K; hence thesis by A1,VECTSP_6:40;
suppose 0.K=1_ K; then K is trivial by Def2;
then Sum(l) = 0.V by Th5;
hence thesis by A1,VECTSP_4:4;end;
hence thesis;
end;
canceled;
theorem
0.V in A & A is lineary-closed implies A = [#]Lin(A)
proof assume
A1: 0.V in A & A is lineary-closed;
thus A c= [#]Lin(A) by Th12;
let x; assume x in [#]Lin(A); then x in Lin(A) by Th10;
then ex l st x = Sum(l) by MOD_3:11;
hence thesis by A1,Th13;
end;
begin ::
:: 2. Cyclic submodule
::
definition let K,V,a;
redefine func {a} -> Subset of V;
coherence
proof
thus {a} is Subset of V;
end;
end;
definition let K,V,a;
func <:a:> -> strict Subspace of V equals Lin({a});
correctness;
end;
begin ::
:: 3. Inclusion of left R-modules
::
definition let K,M,N;
pred M c= N means
:Def7: M is Subspace of N;
reflexivity by VECTSP_4:32;
end;
theorem Th16:
M c= N implies
(x in M implies x in N) & (x is Vector of M implies x is Vector of N)
proof assume
A1: M c= N;
thus x in M implies x in N
proof assume
A2: x in M;
reconsider M' = M as Subspace of N by A1,Def7;
x in M' by A2;
hence thesis by VECTSP_4:17;
end;
thus x is Vector of M implies x is Vector of N
proof assume
A3: x is Vector of M;
reconsider M' = M as Subspace of N by A1,Def7;
x is Vector of M' by A3;
hence thesis by VECTSP_4:18;
end;
end;
theorem
M c= N implies
0.M = 0.N
& (m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2)
& (m = n implies r * m = r * n)
& (m = n implies - n = - m)
& (m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2)
& 0.N in M
& 0.M in N
& (n1 in M & n2 in M implies n1 + n2 in M)
& (n in M implies r * n in M)
& (n in M implies - n in M)
& (n1 in M & n2 in M implies n1 - n2 in M)
proof assume
A1: M c= N;
thus 0.M = 0.N
proof
reconsider M' = M as Subspace of N by A1,Def7;
0.M' = 0.N by VECTSP_4:19;
hence thesis;
end;
thus m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2
proof assume
A2: m1 = n1 & m2 = n2;
reconsider M' = M as Subspace of N by A1,Def7;
reconsider m1'=m1, m2'=m2 as Vector of M';
m1' = n1 & m2' = n2 by A2;
hence thesis by VECTSP_4:21;
end;
thus m = n implies r * m = r * n
proof assume
A3: m = n;
reconsider M' = M as Subspace of N by A1,Def7;
reconsider m'=m as Vector of M';
m' = n by A3;
hence thesis by VECTSP_4:22;
end;
thus m = n implies - n = - m
proof assume
A4: m = n;
reconsider M' = M as Subspace of N by A1,Def7;
reconsider m'=m as Vector of M';
m' = n by A4;
hence thesis by VECTSP_4:23;
end;
thus m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2
proof assume
A5: m1 = n1 & m2 = n2;
reconsider M' = M as Subspace of N by A1,Def7;
reconsider m1'=m1, m2'=m2 as Vector of M';
m1' = n1 & m2' = n2 by A5;
hence thesis by VECTSP_4:24;
end;
thus 0.N in M
proof
reconsider M' = M as Subspace of N by A1,Def7;
0.N in M' by VECTSP_4:25;
hence thesis;
end;
thus 0.M in N
proof
reconsider M' = M as Subspace of N by A1,Def7;
0.M' in N by VECTSP_4:27;
hence thesis;
end;
thus n1 in M & n2 in M implies n1 + n2 in M
proof assume
A6: n1 in M & n2 in M;
reconsider M' = M as Subspace of N by A1,Def7;
n1 in M' & n2 in M' by A6;
hence thesis by VECTSP_4:28;
end;
thus n in M implies r * n in M
proof assume
A7: n in M;
reconsider M' = M as Subspace of N by A1,Def7;
n in M' by A7;
hence thesis by VECTSP_4:29;
end;
thus n in M implies - n in M
proof assume
A8: n in M;
reconsider M' = M as Subspace of N by A1,Def7;
n in M' by A8;
hence thesis by VECTSP_4:30;
end;
thus n1 in M & n2 in M implies n1 - n2 in M
proof assume
A9: n1 in M & n2 in M;
reconsider M' = M as Subspace of N by A1,Def7;
n1 in M' & n2 in M' by A9;
hence thesis by VECTSP_4:31;
end;
end;
theorem
M1 c= N & M2 c= N implies
0.M1 = 0.M2
& 0.M1 in M2
& (the carrier of M1 c= the carrier of M2
implies M1 c= M2)
& ((for n st n in M1 holds n in M2) implies M1 c= M2)
& (the carrier of M1 = the carrier of M2
& M1 is strict & M2 is strict implies M1 = M2)
& (0).M1 c= M2
proof assume
A1: M1 c= N & M2 c= N;
thus 0.M1 = 0.M2
proof
reconsider M1'=M1, M2'=M2 as Subspace of N by A1,Def7;
0.M1' = 0.M2' by VECTSP_4:20;
hence thesis;
end;
thus 0.M1 in M2
proof
reconsider M1'=M1, M2'=M2 as Subspace of N by A1,Def7;
0.M1' in M2' by VECTSP_4:26;
hence thesis;
end;
thus the carrier of M1 c= the carrier of M2
implies M1 c= M2
proof assume
A2: the carrier of M1 c= the carrier of M2;
reconsider M1'=M1, M2'=M2 as Subspace of N by A1,Def7;
M1' is Subspace of M2' by A2,VECTSP_4:35;
hence thesis by Def7;
end;
thus (for n st n in M1 holds n in M2) implies M1 c= M2
proof assume
A3: for n st n in M1 holds n in M2;
reconsider M1'=M1, M2'=M2 as Subspace of N by A1,Def7;
M1' is Subspace of M2' by A3,VECTSP_4:36;
hence thesis by Def7;
end;
thus the carrier of M1 = the carrier of M2
& M1 is strict & M2 is strict implies M1 = M2
proof assume that
A4: the carrier of M1 = the carrier of M2 and
A5: M1 is strict & M2 is strict;
reconsider M1'=M1 as strict Subspace of N by A1,A5,Def7;
reconsider M2'=M2 as strict Subspace of N by A1,A5,Def7;
M1' = M2' by A4,VECTSP_4:37;
hence thesis;
end;
thus (0).M1 c= M2
proof
reconsider M1'=M1, M2'=M2 as Subspace of N by A1,Def7;
(0).M1' is Subspace of M2' by VECTSP_4:51;
hence thesis by Def7;
end;
end;
canceled 2;
theorem
for V,M being strict LeftMod of K
holds V c= M & M c= V implies V = M
proof let V,M be strict LeftMod of K such that
A1: V c= M and
A2: M c= V;
A3: V is Subspace of M by A1,Def7;
M is Subspace of V by A2,Def7;
hence thesis by A3,VECTSP_4:33;
end;
theorem
V c= M & M c= N implies V c= N
proof assume V c= M & M c= N;
then V is Subspace of M & M is Subspace of N by Def7;
then V is Subspace of N by VECTSP_4:34;
hence thesis by Def7;
end;
theorem
M c= N implies (0).M c= N
proof assume M c= N;
then reconsider M' = M as Subspace of N by Def7;
(0).M' is Subspace of N by VECTSP_4:49;
hence thesis by Def7;
end;
theorem
M c= N implies (0).N c= M
proof assume M c= N;
then reconsider M' = M as Subspace of N by Def7;
(0).N is Subspace of M' by VECTSP_4:50;
hence thesis by Def7;
end;
theorem
M c= N implies M c= (Omega).N
proof assume M c= N;
then A1: M is Subspace of N by Def7;
N is Subspace of (Omega).N by Th4;
then M is Subspace of (Omega).N by A1,VECTSP_4:34;
hence thesis by Def7;
end;
theorem
W1 c= W1 + W2 & W2 c= W1 + W2
proof
W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2
by VECTSP_5:11;
hence thesis by Def7;
end;
theorem
W1 /\ W2 c= W1 & W1 /\ W2 c= W2
proof
W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2
by VECTSP_5:20;
hence thesis by Def7;
end;
theorem
W1 c= W2 implies W1 /\ W3 c= W2 /\ W3
proof
W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3
by VECTSP_5:22;
hence thesis by Def7;
end;
theorem
W1 c= W3 implies W1 /\ W2 c= W3
proof
W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3
by VECTSP_5:23;
hence thesis by Def7;
end;
theorem
W1 c= W2 & W1 c= W3 implies W1 c= W2 /\ W3
proof
W1 is Subspace of W2 & W1 is Subspace of W3 implies
W1 is Subspace of W2 /\ W3 by VECTSP_5:24;
hence thesis by Def7;
end;
theorem
W1 /\ W2 c= W1 + W2
proof
W1 /\ W2 is Subspace of W1 + W2 by VECTSP_5:29;
hence thesis by Def7;
end;
theorem
(W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3)
proof
(W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3)
by VECTSP_5:32;
hence thesis by Def7;
end;
theorem
W1 c= W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
proof
W1 is Subspace of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
by VECTSP_5:33;
hence thesis by Def7;
end;
theorem
W2 + (W1 /\ W3) c= (W1 + W2) /\ (W2 + W3)
proof
W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3)
by VECTSP_5:34;
hence thesis by Def7;
end;
theorem
W1 c= W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
proof
W1 is Subspace of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
by VECTSP_5:35;
hence thesis by Def7;
end;
theorem
W1 c= W2 implies W1 c= W2 + W3
proof
W1 is Subspace of W2 implies W1 is Subspace of W2 + W3
by VECTSP_5:39;
hence thesis by Def7;
end;
theorem
W1 c= W3 & W2 c= W3 implies W1 + W2 c= W3
proof
W1 is Subspace of W3 & W2 is Subspace of W3 implies
W1 + W2 is Subspace of W3 by VECTSP_5:40;
hence thesis by Def7;
end;
theorem
for A,B being Subset of V st A c= B holds Lin(A) c= Lin(B)
proof let A,B be Subset of V; assume A c= B;
then Lin(A) is Subspace of Lin(B) by MOD_3:17;
hence thesis by Def7;
end;
theorem
for A,B being Subset of V holds Lin(A /\ B) c= Lin(A) /\ Lin(B)
proof let A,B be Subset of V;
Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B) by MOD_3:20;
hence thesis by Def7;
end;
theorem Th40:
M1 c= M2 implies [#]M1 c= [#]M2
proof assume
A1: M1 c= M2;
let x; assume x in [#]M1; then x in M1 by Th10;
then x in M2 by A1,Th16;
hence thesis by Th10;
end;
theorem Th41:
W1 c= W2 iff for a st a in W1 holds a in W2
proof
W1 c= W2 iff W1 is Subspace of W2 by Def7;
hence thesis by VECTSP_4:16,36;
end;
theorem Th42:
W1 c= W2 iff [#]W1 c= [#]W2
proof
thus W1 c= W2 implies [#]W1 c= [#]W2 by Th40;
assume
A1: [#]W1 c= [#]W2;
now let a; assume a in W1; then a in [#]W1 by Th10;
hence a in W2 by A1,Th10;end;
hence thesis by Th41;
end;
theorem
W1 c= W2 iff @[#]W1 c= @[#]W2
proof
@[#]W1 = [#]W1 & @[#]W2 = [#]W2 by Def5;
hence thesis by Th42;
end;
theorem
(0).W c= V & (0).V c= W & (0).W1 c= W2
proof
A1: (0).W is Subspace of V by VECTSP_4:49;
A2: (0).V is Subspace of W by VECTSP_4:50;
A3: (0).W1 is Subspace of W2 by VECTSP_4:51;
thus (0).W c= V by A1,Def7;
thus (0).V c= W by A2,Def7;
thus (0).W1 c= W2 by A3,Def7;
end;