vectsp_5.miz
begin
reserve GF for
add-associative
right_zeroed
right_complementable
Abelian
associative
well-unital
distributive non
empty
doubleLoopStr;
reserve M for
Abelian
add-associative
right_zeroed
right_complementable
vector-distributive
scalar-distributive
scalar-associative
scalar-unital non
empty
ModuleStr over GF;
reserve W,W1,W2,W3 for
Subspace of M;
reserve u,u1,u2,v,v1,v2 for
Element of M;
reserve X,Y for
set,
x,y,y1,y2 for
object;
definition
let GF;
let M;
let W1, W2;
::
VECTSP_5:def1
func W1
+ W2 ->
strict
Subspace of M means
:
Def1: the
carrier of it
= { (v
+ u) : v
in W1 & u
in W2 };
existence
proof
reconsider V1 = the
carrier of W1, V2 = the
carrier of W2 as
Subset of M by
VECTSP_4:def 2;
set VS = { (v
+ u) where u,v be
Element of M : v
in W1 & u
in W2 };
VS
c= the
carrier of M
proof
let x be
object;
assume x
in VS;
then ex v2, v1 st x
= (v1
+ v2) & v1
in W1 & v2
in W2;
hence thesis;
end;
then
reconsider VS as
Subset of M;
A1: (
0. M)
= ((
0. M)
+ (
0. M)) by
RLVECT_1: 4;
(
0. M)
in W1 & (
0. M)
in W2 by
VECTSP_4: 17;
then
A2: (
0. M)
in VS by
A1;
A3: VS
= { (v
+ u) where v, u : v
in V1 & u
in V2 }
proof
thus VS
c= { (v
+ u) where v, u : v
in V1 & u
in V2 }
proof
let x be
object;
assume x
in VS;
then
consider u, v such that
A4: x
= (v
+ u) and
A5: v
in W1 & u
in W2;
v
in V1 & u
in V2 by
A5,
STRUCT_0:def 5;
hence thesis by
A4;
end;
let x be
object;
assume x
in { (v
+ u) where v, u : v
in V1 & u
in V2 };
then
consider v, u such that
A6: x
= (v
+ u) and
A7: v
in V1 & u
in V2;
v
in W1 & u
in W2 by
A7,
STRUCT_0:def 5;
hence thesis by
A6;
end;
V1 is
linearly-closed & V2 is
linearly-closed by
VECTSP_4: 33;
hence thesis by
A2,
A3,
VECTSP_4: 6,
VECTSP_4: 34;
end;
uniqueness by
VECTSP_4: 29;
end
Lm1: (W1
+ W2)
= (W2
+ W1)
proof
set A = { (v
+ u) : v
in W1 & u
in W2 };
set B = { (v
+ u) : v
in W2 & u
in W1 };
A1: B
c= A
proof
let x be
object;
assume x
in B;
then ex u, v st x
= (v
+ u) & v
in W2 & u
in W1;
hence thesis;
end;
A2: the
carrier of (W1
+ W2)
= A by
Def1;
A
c= B
proof
let x be
object;
assume x
in A;
then ex u, v st x
= (v
+ u) & v
in W1 & u
in W2;
hence thesis;
end;
then A
= B by
A1;
hence thesis by
A2,
Def1;
end;
definition
let GF;
let M;
let W1, W2;
::
VECTSP_5:def2
func W1
/\ W2 ->
strict
Subspace of M means
:
Def2: the
carrier of it
= (the
carrier of W1
/\ the
carrier of W2);
existence
proof
set VW2 = the
carrier of W2;
set VW1 = the
carrier of W1;
set VV = the
carrier of M;
(
0. M)
in W2 by
VECTSP_4: 17;
then
A1: (
0. M)
in VW2 by
STRUCT_0:def 5;
VW1
c= VV & VW2
c= VV by
VECTSP_4:def 2;
then (VW1
/\ VW2)
c= (VV
/\ VV) by
XBOOLE_1: 27;
then
reconsider V1 = VW1, V2 = VW2, V3 = (VW1
/\ VW2) as
Subset of M by
VECTSP_4:def 2;
V1 is
linearly-closed & V2 is
linearly-closed by
VECTSP_4: 33;
then
A2: V3 is
linearly-closed by
VECTSP_4: 7;
(
0. M)
in W1 by
VECTSP_4: 17;
then (
0. M)
in VW1 by
STRUCT_0:def 5;
then (VW1
/\ VW2)
<>
{} by
A1,
XBOOLE_0:def 4;
hence thesis by
A2,
VECTSP_4: 34;
end;
uniqueness by
VECTSP_4: 29;
commutativity ;
end
theorem ::
VECTSP_5:1
Th1: x
in (W1
+ W2) iff ex v1, v2 st v1
in W1 & v2
in W2 & x
= (v1
+ v2)
proof
thus x
in (W1
+ W2) implies ex v1, v2 st v1
in W1 & v2
in W2 & x
= (v1
+ v2)
proof
assume x
in (W1
+ W2);
then x
in the
carrier of (W1
+ W2) by
STRUCT_0:def 5;
then x
in { (v
+ u) : v
in W1 & u
in W2 } by
Def1;
then
consider v2, v1 such that
A1: x
= (v1
+ v2) & v1
in W1 & v2
in W2;
take v1, v2;
thus thesis by
A1;
end;
given v1, v2 such that
A2: v1
in W1 & v2
in W2 & x
= (v1
+ v2);
x
in { (v
+ u) : v
in W1 & u
in W2 } by
A2;
then x
in the
carrier of (W1
+ W2) by
Def1;
hence thesis by
STRUCT_0:def 5;
end;
theorem ::
VECTSP_5:2
Th2: v
in W1 or v
in W2 implies v
in (W1
+ W2)
proof
assume
A1: v
in W1 or v
in W2;
now
per cases by
A1;
suppose
A2: v
in W1;
v
= (v
+ (
0. M)) & (
0. M)
in W2 by
RLVECT_1: 4,
VECTSP_4: 17;
hence thesis by
A2,
Th1;
end;
suppose
A3: v
in W2;
v
= ((
0. M)
+ v) & (
0. M)
in W1 by
RLVECT_1: 4,
VECTSP_4: 17;
hence thesis by
A3,
Th1;
end;
end;
hence thesis;
end;
theorem ::
VECTSP_5:3
Th3: x
in (W1
/\ W2) iff x
in W1 & x
in W2
proof
x
in (W1
/\ W2) iff x
in the
carrier of (W1
/\ W2) by
STRUCT_0:def 5;
then x
in (W1
/\ W2) iff x
in (the
carrier of W1
/\ the
carrier of W2) by
Def2;
then x
in (W1
/\ W2) iff x
in the
carrier of W1 & x
in the
carrier of W2 by
XBOOLE_0:def 4;
hence thesis by
STRUCT_0:def 5;
end;
Lm2: the
carrier of W1
c= the
carrier of (W1
+ W2)
proof
let x be
object;
set A = { (v
+ u) : v
in W1 & u
in W2 };
assume x
in the
carrier of W1;
then
reconsider v = x as
Element of W1;
reconsider v as
Element of M by
VECTSP_4: 10;
A1: v
= (v
+ (
0. M)) by
RLVECT_1: 4;
v
in W1 & (
0. M)
in W2 by
STRUCT_0:def 5,
VECTSP_4: 17;
then x
in A by
A1;
hence thesis by
Def1;
end;
Lm3: for W2 be
strict
Subspace of M holds the
carrier of W1
c= the
carrier of W2 implies (W1
+ W2)
= W2
proof
let W2 be
strict
Subspace of M;
assume
A1: the
carrier of W1
c= the
carrier of W2;
A2: the
carrier of (W1
+ W2)
c= the
carrier of W2
proof
let x be
object;
assume x
in the
carrier of (W1
+ W2);
then x
in { (v
+ u) : v
in W1 & u
in W2 } by
Def1;
then
consider u, v such that
A3: x
= (v
+ u) and
A4: v
in W1 and
A5: u
in W2;
W1 is
Subspace of W2 by
A1,
VECTSP_4: 27;
then v
in W2 by
A4,
VECTSP_4: 8;
then (v
+ u)
in W2 by
A5,
VECTSP_4: 20;
hence thesis by
A3,
STRUCT_0:def 5;
end;
(W1
+ W2)
= (W2
+ W1) by
Lm1;
then the
carrier of W2
c= the
carrier of (W1
+ W2) by
Lm2;
then the
carrier of (W1
+ W2)
= the
carrier of W2 by
A2;
hence thesis by
VECTSP_4: 29;
end;
theorem ::
VECTSP_5:4
for W be
strict
Subspace of M holds (W
+ W)
= W by
Lm3;
theorem ::
VECTSP_5:5
(W1
+ W2)
= (W2
+ W1) by
Lm1;
theorem ::
VECTSP_5:6
Th6: (W1
+ (W2
+ W3))
= ((W1
+ W2)
+ W3)
proof
set A = { (v
+ u) : v
in W1 & u
in W2 };
set B = { (v
+ u) : v
in W2 & u
in W3 };
set C = { (v
+ u) : v
in (W1
+ W2) & u
in W3 };
set D = { (v
+ u) : v
in W1 & u
in (W2
+ W3) };
A1: the
carrier of (W1
+ (W2
+ W3))
= D by
Def1;
A2: C
c= D
proof
let x be
object;
assume x
in C;
then
consider u, v such that
A3: x
= (v
+ u) and
A4: v
in (W1
+ W2) and
A5: u
in W3;
v
in the
carrier of (W1
+ W2) by
A4,
STRUCT_0:def 5;
then v
in A by
Def1;
then
consider u2, u1 such that
A6: v
= (u1
+ u2) and
A7: u1
in W1 and
A8: u2
in W2;
(u2
+ u)
in B by
A5,
A8;
then (u2
+ u)
in the
carrier of (W2
+ W3) by
Def1;
then
A9: (u2
+ u)
in (W2
+ W3) by
STRUCT_0:def 5;
(v
+ u)
= (u1
+ (u2
+ u)) by
A6,
RLVECT_1:def 3;
hence thesis by
A3,
A7,
A9;
end;
D
c= C
proof
let x be
object;
assume x
in D;
then
consider u, v such that
A10: x
= (v
+ u) and
A11: v
in W1 and
A12: u
in (W2
+ W3);
u
in the
carrier of (W2
+ W3) by
A12,
STRUCT_0:def 5;
then u
in B by
Def1;
then
consider u2, u1 such that
A13: u
= (u1
+ u2) and
A14: u1
in W2 and
A15: u2
in W3;
(v
+ u1)
in A by
A11,
A14;
then (v
+ u1)
in the
carrier of (W1
+ W2) by
Def1;
then
A16: (v
+ u1)
in (W1
+ W2) by
STRUCT_0:def 5;
(v
+ u)
= ((v
+ u1)
+ u2) by
A13,
RLVECT_1:def 3;
hence thesis by
A10,
A15,
A16;
end;
then D
= C by
A2;
hence thesis by
A1,
Def1;
end;
theorem ::
VECTSP_5:7
Th7: W1 is
Subspace of (W1
+ W2) & W2 is
Subspace of (W1
+ W2)
proof
the
carrier of W1
c= the
carrier of (W1
+ W2) by
Lm2;
hence W1 is
Subspace of (W1
+ W2) by
VECTSP_4: 27;
the
carrier of W2
c= the
carrier of (W2
+ W1) by
Lm2;
then the
carrier of W2
c= the
carrier of (W1
+ W2) by
Lm1;
hence thesis by
VECTSP_4: 27;
end;
theorem ::
VECTSP_5:8
Th8: for W2 be
strict
Subspace of M holds W1 is
Subspace of W2 iff (W1
+ W2)
= W2
proof
let W2 be
strict
Subspace of M;
thus W1 is
Subspace of W2 implies (W1
+ W2)
= W2
proof
assume W1 is
Subspace of W2;
then the
carrier of W1
c= the
carrier of W2 by
VECTSP_4:def 2;
hence thesis by
Lm3;
end;
thus thesis by
Th7;
end;
theorem ::
VECTSP_5:9
Th9: for W be
strict
Subspace of M holds ((
(0). M)
+ W)
= W & (W
+ (
(0). M))
= W
proof
let W be
strict
Subspace of M;
(
(0). M) is
Subspace of W by
VECTSP_4: 39;
then the
carrier of (
(0). M)
c= the
carrier of W by
VECTSP_4:def 2;
hence ((
(0). M)
+ W)
= W by
Lm3;
hence thesis by
Lm1;
end;
Lm4: for W holds ex W9 be
strict
Subspace of M st the
carrier of W
= the
carrier of W9
proof
let W;
take W9 = (W
+ W);
thus the
carrier of W
c= the
carrier of W9 by
Lm2;
let x be
object;
assume x
in the
carrier of W9;
then x
in { (v
+ u) : v
in W & u
in W } by
Def1;
then ex v2, v1 st x
= (v1
+ v2) & v1
in W & v2
in W;
then x
in W by
VECTSP_4: 20;
hence thesis by
STRUCT_0:def 5;
end;
Lm5: for W,W9,W1 be
Subspace of M st the
carrier of W
= the
carrier of W9 holds (W1
+ W)
= (W1
+ W9) & (W
+ W1)
= (W9
+ W1)
proof
let W,W9,W1 be
Subspace of M such that
A1: the
carrier of W
= the
carrier of W9;
A2:
now
let v;
set W1W9 = { (v1
+ v2) where v2, v1 : v1
in W1 & v2
in W9 };
set W1W = { (v1
+ v2) where v2, v1 : v1
in W1 & v2
in W };
thus v
in (W1
+ W) implies v
in (W1
+ W9)
proof
assume v
in (W1
+ W);
then v
in the
carrier of (W1
+ W) by
STRUCT_0:def 5;
then v
in W1W by
Def1;
then
consider v2, v1 such that
A3: v
= (v1
+ v2) & v1
in W1 and
A4: v2
in W;
v2
in the
carrier of W9 by
A1,
A4,
STRUCT_0:def 5;
then v2
in W9 by
STRUCT_0:def 5;
then v
in W1W9 by
A3;
then v
in the
carrier of (W1
+ W9) by
Def1;
hence thesis by
STRUCT_0:def 5;
end;
assume v
in (W1
+ W9);
then v
in the
carrier of (W1
+ W9) by
STRUCT_0:def 5;
then v
in W1W9 by
Def1;
then
consider v2, v1 such that
A5: v
= (v1
+ v2) & v1
in W1 and
A6: v2
in W9;
v2
in the
carrier of W by
A1,
A6,
STRUCT_0:def 5;
then v2
in W by
STRUCT_0:def 5;
then v
in W1W by
A5;
then v
in the
carrier of (W1
+ W) by
Def1;
hence v
in (W1
+ W) by
STRUCT_0:def 5;
end;
hence (W1
+ W)
= (W1
+ W9) by
VECTSP_4: 30;
(W1
+ W)
= (W
+ W1) & (W1
+ W9)
= (W9
+ W1) by
Lm1;
hence thesis by
A2,
VECTSP_4: 30;
end;
Lm6: for W be
Subspace of M holds W is
Subspace of (
(Omega). M)
proof
let W be
Subspace of M;
thus the
carrier of W
c= the
carrier of (
(Omega). M) by
VECTSP_4:def 2;
thus (
0. W)
= (
0. M) by
VECTSP_4:def 2
.= (
0. (
(Omega). M)) by
VECTSP_4:def 2;
thus thesis by
VECTSP_4:def 2;
end;
theorem ::
VECTSP_5:10
((
(0). M)
+ (
(Omega). M))
= the ModuleStr of M & ((
(Omega). M)
+ (
(0). M))
= the ModuleStr of M by
Th9;
theorem ::
VECTSP_5:11
Th11: ((
(Omega). M)
+ W)
= the ModuleStr of M & (W
+ (
(Omega). M))
= the ModuleStr of M
proof
consider W9 be
strict
Subspace of M such that
A1: the
carrier of W9
= the
carrier of (
(Omega). M);
A2: the
carrier of W
c= the
carrier of W9 by
A1,
VECTSP_4:def 2;
A3: W9 is
Subspace of (
(Omega). M) by
Lm6;
(W
+ (
(Omega). M))
= (W
+ W9) by
A1,
Lm5
.= W9 by
A2,
Lm3
.= the ModuleStr of M by
A1,
A3,
VECTSP_4: 31;
hence thesis by
Lm1;
end;
theorem ::
VECTSP_5:12
for M be
strict
Abelian
add-associative
right_zeroed
right_complementable
vector-distributive
scalar-distributive
scalar-associative
scalar-unital non
empty
ModuleStr over GF holds ((
(Omega). M)
+ (
(Omega). M))
= M by
Th11;
theorem ::
VECTSP_5:13
for W be
strict
Subspace of M holds (W
/\ W)
= W
proof
let W be
strict
Subspace of M;
the
carrier of W
= (the
carrier of W
/\ the
carrier of W);
hence thesis by
Def2;
end;
theorem ::
VECTSP_5:14
Th14: (W1
/\ (W2
/\ W3))
= ((W1
/\ W2)
/\ W3)
proof
set V1 = the
carrier of W1;
set V2 = the
carrier of W2;
set V3 = the
carrier of W3;
the
carrier of (W1
/\ (W2
/\ W3))
= (V1
/\ the
carrier of (W2
/\ W3)) by
Def2
.= (V1
/\ (V2
/\ V3)) by
Def2
.= ((V1
/\ V2)
/\ V3) by
XBOOLE_1: 16
.= (the
carrier of (W1
/\ W2)
/\ V3) by
Def2;
hence thesis by
Def2;
end;
Lm7: the
carrier of (W1
/\ W2)
c= the
carrier of W1
proof
the
carrier of (W1
/\ W2)
= (the
carrier of W1
/\ the
carrier of W2) by
Def2;
hence thesis by
XBOOLE_1: 17;
end;
theorem ::
VECTSP_5:15
Th15: (W1
/\ W2) is
Subspace of W1 & (W1
/\ W2) is
Subspace of W2
proof
the
carrier of (W1
/\ W2)
c= the
carrier of W1 by
Lm7;
hence (W1
/\ W2) is
Subspace of W1 by
VECTSP_4: 27;
the
carrier of (W2
/\ W1)
c= the
carrier of W2 by
Lm7;
hence thesis by
VECTSP_4: 27;
end;
Lm8: for W,W9,W1 be
Subspace of M st the
carrier of W
= the
carrier of W9 holds (W1
/\ W)
= (W1
/\ W9) & (W
/\ W1)
= (W9
/\ W1)
proof
let W,W9,W1 be
Subspace of M;
assume the
carrier of W
= the
carrier of W9;
then
A1: the
carrier of (W1
/\ W)
= (the
carrier of W1
/\ the
carrier of W9) by
Def2
.= the
carrier of (W1
/\ W9) by
Def2;
hence (W1
/\ W)
= (W1
/\ W9) by
VECTSP_4: 29;
thus thesis by
A1,
VECTSP_4: 29;
end;
theorem ::
VECTSP_5:16
Th16: (for W1 be
strict
Subspace of M holds W1 is
Subspace of W2 implies (W1
/\ W2)
= W1) & for W1 st (W1
/\ W2)
= W1 holds W1 is
Subspace of W2
proof
thus for W1 be
strict
Subspace of M holds W1 is
Subspace of W2 implies (W1
/\ W2)
= W1
proof
let W1 be
strict
Subspace of M;
assume W1 is
Subspace of W2;
then
A1: the
carrier of W1
c= the
carrier of W2 by
VECTSP_4:def 2;
the
carrier of (W1
/\ W2)
= (the
carrier of W1
/\ the
carrier of W2) by
Def2;
hence thesis by
A1,
VECTSP_4: 29,
XBOOLE_1: 28;
end;
thus thesis by
Th15;
end;
theorem ::
VECTSP_5:17
W1 is
Subspace of W2 implies (W1
/\ W3) is
Subspace of (W2
/\ W3)
proof
set A1 = the
carrier of W1;
set A2 = the
carrier of W2;
set A3 = the
carrier of W3;
set A4 = the
carrier of (W1
/\ W3);
assume W1 is
Subspace of W2;
then A1
c= A2 by
VECTSP_4:def 2;
then (A1
/\ A3)
c= (A2
/\ A3) by
XBOOLE_1: 26;
then A4
c= (A2
/\ A3) by
Def2;
then A4
c= the
carrier of (W2
/\ W3) by
Def2;
hence thesis by
VECTSP_4: 27;
end;
theorem ::
VECTSP_5:18
W1 is
Subspace of W3 implies (W1
/\ W2) is
Subspace of W3
proof
assume
A1: W1 is
Subspace of W3;
(W1
/\ W2) is
Subspace of W1 by
Th15;
hence thesis by
A1,
VECTSP_4: 26;
end;
theorem ::
VECTSP_5:19
W1 is
Subspace of W2 & W1 is
Subspace of W3 implies W1 is
Subspace of (W2
/\ W3)
proof
assume
A1: W1 is
Subspace of W2 & W1 is
Subspace of W3;
now
let v;
assume v
in W1;
then v
in W2 & v
in W3 by
A1,
VECTSP_4: 8;
hence v
in (W2
/\ W3) by
Th3;
end;
hence thesis by
VECTSP_4: 28;
end;
theorem ::
VECTSP_5:20
Th20: ((
(0). M)
/\ W)
= (
(0). M) & (W
/\ (
(0). M))
= (
(0). M)
proof
(
0. M)
in W by
VECTSP_4: 17;
then (
0. M)
in the
carrier of W by
STRUCT_0:def 5;
then
{(
0. M)}
c= the
carrier of W by
ZFMISC_1: 31;
then
A1: (
{(
0. M)}
/\ the
carrier of W)
=
{(
0. M)} by
XBOOLE_1: 28;
A2: the
carrier of ((
(0). M)
/\ W)
= (the
carrier of (
(0). M)
/\ the
carrier of W) by
Def2
.= (
{(
0. M)}
/\ the
carrier of W) by
VECTSP_4:def 3;
hence ((
(0). M)
/\ W)
= (
(0). M) by
A1,
VECTSP_4:def 3;
thus thesis by
A2,
A1,
VECTSP_4:def 3;
end;
theorem ::
VECTSP_5:21
Th21: for W be
strict
Subspace of M holds ((
(Omega). M)
/\ W)
= W & (W
/\ (
(Omega). M))
= W
proof
let W be
strict
Subspace of M;
A1: the
carrier of ((
(Omega). M)
/\ W)
= (the
carrier of the ModuleStr of M
/\ the
carrier of W) & the
carrier of W
c= the
carrier of M by
Def2,
VECTSP_4:def 2;
hence ((
(Omega). M)
/\ W)
= W by
VECTSP_4: 29,
XBOOLE_1: 28;
thus thesis by
A1,
VECTSP_4: 29,
XBOOLE_1: 28;
end;
theorem ::
VECTSP_5:22
for M be
strict
Abelian
add-associative
right_zeroed
right_complementable
vector-distributive
scalar-distributive
scalar-associative
scalar-unital non
empty
ModuleStr over GF holds ((
(Omega). M)
/\ (
(Omega). M))
= M by
Th21;
Lm9: the
carrier of (W1
/\ W2)
c= the
carrier of (W1
+ W2)
proof
the
carrier of (W1
/\ W2)
c= the
carrier of W1 & the
carrier of W1
c= the
carrier of (W1
+ W2) by
Lm2,
Lm7;
hence thesis;
end;
theorem ::
VECTSP_5:23
(W1
/\ W2) is
Subspace of (W1
+ W2) by
Lm9,
VECTSP_4: 27;
Lm10: the
carrier of ((W1
/\ W2)
+ W2)
= the
carrier of W2
proof
thus the
carrier of ((W1
/\ W2)
+ W2)
c= the
carrier of W2
proof
let x be
object;
assume x
in the
carrier of ((W1
/\ W2)
+ W2);
then x
in { (u
+ v) where v, u : u
in (W1
/\ W2) & v
in W2 } by
Def1;
then
consider v, u such that
A1: x
= (u
+ v) and
A2: u
in (W1
/\ W2) and
A3: v
in W2;
u
in W2 by
A2,
Th3;
then (u
+ v)
in W2 by
A3,
VECTSP_4: 20;
hence thesis by
A1,
STRUCT_0:def 5;
end;
let x be
object;
the
carrier of W2
c= the
carrier of (W2
+ (W1
/\ W2)) by
Lm2;
then
A4: the
carrier of W2
c= the
carrier of ((W1
/\ W2)
+ W2) by
Lm1;
assume x
in the
carrier of W2;
hence thesis by
A4;
end;
theorem ::
VECTSP_5:24
for W2 be
strict
Subspace of M holds ((W1
/\ W2)
+ W2)
= W2 by
Lm10,
VECTSP_4: 29;
Lm11: the
carrier of (W1
/\ (W1
+ W2))
= the
carrier of W1
proof
thus the
carrier of (W1
/\ (W1
+ W2))
c= the
carrier of W1
proof
let x be
object;
assume
A1: x
in the
carrier of (W1
/\ (W1
+ W2));
the
carrier of (W1
/\ (W1
+ W2))
= (the
carrier of W1
/\ the
carrier of (W1
+ W2)) by
Def2;
hence thesis by
A1,
XBOOLE_0:def 4;
end;
let x be
object;
assume
A2: x
in the
carrier of W1;
the
carrier of W1
c= the
carrier of M by
VECTSP_4:def 2;
then
reconsider x1 = x as
Element of M by
A2;
A3: (x1
+ (
0. M))
= x1 & (
0. M)
in W2 by
RLVECT_1: 4,
VECTSP_4: 17;
x
in W1 by
A2,
STRUCT_0:def 5;
then x
in { (u
+ v) where v, u : u
in W1 & v
in W2 } by
A3;
then x
in the
carrier of (W1
+ W2) by
Def1;
then x
in (the
carrier of W1
/\ the
carrier of (W1
+ W2)) by
A2,
XBOOLE_0:def 4;
hence thesis by
Def2;
end;
theorem ::
VECTSP_5:25
for W1 be
strict
Subspace of M holds (W1
/\ (W1
+ W2))
= W1 by
Lm11,
VECTSP_4: 29;
Lm12: the
carrier of ((W1
/\ W2)
+ (W2
/\ W3))
c= the
carrier of (W2
/\ (W1
+ W3))
proof
let x be
object;
assume x
in the
carrier of ((W1
/\ W2)
+ (W2
/\ W3));
then x
in { (u
+ v) where v, u : u
in (W1
/\ W2) & v
in (W2
/\ W3) } by
Def1;
then
consider v, u such that
A1: x
= (u
+ v) and
A2: u
in (W1
/\ W2) & v
in (W2
/\ W3);
u
in W2 & v
in W2 by
A2,
Th3;
then
A3: x
in W2 by
A1,
VECTSP_4: 20;
u
in W1 & v
in W3 by
A2,
Th3;
then x
in (W1
+ W3) by
A1,
Th1;
then x
in (W2
/\ (W1
+ W3)) by
A3,
Th3;
hence thesis by
STRUCT_0:def 5;
end;
theorem ::
VECTSP_5:26
((W1
/\ W2)
+ (W2
/\ W3)) is
Subspace of (W2
/\ (W1
+ W3)) by
Lm12,
VECTSP_4: 27;
Lm13: W1 is
Subspace of W2 implies the
carrier of (W2
/\ (W1
+ W3))
= the
carrier of ((W1
/\ W2)
+ (W2
/\ W3))
proof
assume
A1: W1 is
Subspace of W2;
thus the
carrier of (W2
/\ (W1
+ W3))
c= the
carrier of ((W1
/\ W2)
+ (W2
/\ W3))
proof
let x be
object;
assume x
in the
carrier of (W2
/\ (W1
+ W3));
then
A2: x
in (the
carrier of W2
/\ the
carrier of (W1
+ W3)) by
Def2;
then x
in the
carrier of (W1
+ W3) by
XBOOLE_0:def 4;
then x
in { (u
+ v) where v, u : u
in W1 & v
in W3 } by
Def1;
then
consider v1, u1 such that
A3: x
= (u1
+ v1) and
A4: u1
in W1 and
A5: v1
in W3;
A6: u1
in W2 by
A1,
A4,
VECTSP_4: 8;
x
in the
carrier of W2 by
A2,
XBOOLE_0:def 4;
then (u1
+ v1)
in W2 by
A3,
STRUCT_0:def 5;
then ((v1
+ u1)
- u1)
in W2 by
A6,
VECTSP_4: 23;
then (v1
+ (u1
- u1))
in W2 by
RLVECT_1:def 3;
then (v1
+ (
0. M))
in W2 by
VECTSP_1: 19;
then v1
in W2 by
RLVECT_1: 4;
then
A7: v1
in (W2
/\ W3) by
A5,
Th3;
u1
in (W1
/\ W2) by
A4,
A6,
Th3;
then x
in ((W1
/\ W2)
+ (W2
/\ W3)) by
A3,
A7,
Th1;
hence thesis by
STRUCT_0:def 5;
end;
thus thesis by
Lm12;
end;
theorem ::
VECTSP_5:27
W1 is
Subspace of W2 implies (W2
/\ (W1
+ W3))
= ((W1
/\ W2)
+ (W2
/\ W3)) by
Lm13,
VECTSP_4: 29;
Lm14: the
carrier of (W2
+ (W1
/\ W3))
c= the
carrier of ((W1
+ W2)
/\ (W2
+ W3))
proof
let x be
object;
assume x
in the
carrier of (W2
+ (W1
/\ W3));
then x
in { (u
+ v) where v, u : u
in W2 & v
in (W1
/\ W3) } by
Def1;
then
consider v, u such that
A1: x
= (u
+ v) & u
in W2 and
A2: v
in (W1
/\ W3);
v
in W3 by
A2,
Th3;
then x
in { (u1
+ u2) where u2, u1 : u1
in W2 & u2
in W3 } by
A1;
then
A3: x
in the
carrier of (W2
+ W3) by
Def1;
v
in W1 by
A2,
Th3;
then x
in { (v1
+ v2) where v2, v1 : v1
in W1 & v2
in W2 } by
A1;
then x
in the
carrier of (W1
+ W2) by
Def1;
then x
in (the
carrier of (W1
+ W2)
/\ the
carrier of (W2
+ W3)) by
A3,
XBOOLE_0:def 4;
hence thesis by
Def2;
end;
theorem ::
VECTSP_5:28
(W2
+ (W1
/\ W3)) is
Subspace of ((W1
+ W2)
/\ (W2
+ W3)) by
Lm14,
VECTSP_4: 27;
Lm15: W1 is
Subspace of W2 implies the
carrier of (W2
+ (W1
/\ W3))
= the
carrier of ((W1
+ W2)
/\ (W2
+ W3))
proof
reconsider V2 = the
carrier of W2 as
Subset of M by
VECTSP_4:def 2;
A1: V2 is
linearly-closed by
VECTSP_4: 33;
assume W1 is
Subspace of W2;
then
A2: the
carrier of W1
c= the
carrier of W2 by
VECTSP_4:def 2;
thus the
carrier of (W2
+ (W1
/\ W3))
c= the
carrier of ((W1
+ W2)
/\ (W2
+ W3)) by
Lm14;
let x be
object;
assume x
in the
carrier of ((W1
+ W2)
/\ (W2
+ W3));
then x
in (the
carrier of (W1
+ W2)
/\ the
carrier of (W2
+ W3)) by
Def2;
then x
in the
carrier of (W1
+ W2) by
XBOOLE_0:def 4;
then x
in { (u1
+ u2) where u2, u1 : u1
in W1 & u2
in W2 } by
Def1;
then
consider u2, u1 such that
A3: x
= (u1
+ u2) and
A4: u1
in W1 & u2
in W2;
u1
in the
carrier of W1 & u2
in the
carrier of W2 by
A4,
STRUCT_0:def 5;
then (u1
+ u2)
in V2 by
A2,
A1;
then
A5: (u1
+ u2)
in W2 by
STRUCT_0:def 5;
(
0. M)
in (W1
/\ W3) & ((u1
+ u2)
+ (
0. M))
= (u1
+ u2) by
RLVECT_1: 4,
VECTSP_4: 17;
then x
in { (u
+ v) where v, u : u
in W2 & v
in (W1
/\ W3) } by
A3,
A5;
hence thesis by
Def1;
end;
theorem ::
VECTSP_5:29
W1 is
Subspace of W2 implies (W2
+ (W1
/\ W3))
= ((W1
+ W2)
/\ (W2
+ W3)) by
Lm15,
VECTSP_4: 29;
theorem ::
VECTSP_5:30
Th30: for W1 be
strict
Subspace of M holds W1 is
Subspace of W3 implies (W1
+ (W2
/\ W3))
= ((W1
+ W2)
/\ W3)
proof
let W1 be
strict
Subspace of M;
assume
A1: W1 is
Subspace of W3;
hence ((W1
+ W2)
/\ W3)
= ((W1
/\ W3)
+ (W3
/\ W2)) by
Lm13,
VECTSP_4: 29
.= (W1
+ (W2
/\ W3)) by
A1,
Th16;
end;
theorem ::
VECTSP_5:31
for W1,W2 be
strict
Subspace of M holds (W1
+ W2)
= W2 iff (W1
/\ W2)
= W1
proof
let W1,W2 be
strict
Subspace of M;
(W1
+ W2)
= W2 iff W1 is
Subspace of W2 by
Th8;
hence thesis by
Th16;
end;
theorem ::
VECTSP_5:32
for W2,W3 be
strict
Subspace of M holds W1 is
Subspace of W2 implies (W1
+ W3) is
Subspace of (W2
+ W3)
proof
let W2,W3 be
strict
Subspace of M;
assume
A1: W1 is
Subspace of W2;
((W1
+ W3)
+ (W2
+ W3))
= ((W1
+ W3)
+ (W3
+ W2)) by
Lm1
.= (((W1
+ W3)
+ W3)
+ W2) by
Th6
.= ((W1
+ (W3
+ W3))
+ W2) by
Th6
.= ((W1
+ W3)
+ W2) by
Lm3
.= (W1
+ (W3
+ W2)) by
Th6
.= (W1
+ (W2
+ W3)) by
Lm1
.= ((W1
+ W2)
+ W3) by
Th6
.= (W2
+ W3) by
A1,
Th8;
hence thesis by
Th8;
end;
theorem ::
VECTSP_5:33
W1 is
Subspace of W2 implies W1 is
Subspace of (W2
+ W3)
proof
assume
A1: W1 is
Subspace of W2;
W2 is
Subspace of (W2
+ W3) by
Th7;
hence thesis by
A1,
VECTSP_4: 26;
end;
theorem ::
VECTSP_5:34
W1 is
Subspace of W3 & W2 is
Subspace of W3 implies (W1
+ W2) is
Subspace of W3
proof
assume
A1: W1 is
Subspace of W3 & W2 is
Subspace of W3;
now
let v;
assume v
in (W1
+ W2);
then
consider v1, v2 such that
A2: v1
in W1 & v2
in W2 and
A3: v
= (v1
+ v2) by
Th1;
v1
in W3 & v2
in W3 by
A1,
A2,
VECTSP_4: 8;
hence v
in W3 by
A3,
VECTSP_4: 20;
end;
hence thesis by
VECTSP_4: 28;
end;
theorem ::
VECTSP_5:35
(ex W st the
carrier of W
= (the
carrier of W1
\/ the
carrier of W2)) iff W1 is
Subspace of W2 or W2 is
Subspace of W1
proof
set VW1 = the
carrier of W1;
set VW2 = the
carrier of W2;
thus (ex W st the
carrier of W
= (the
carrier of W1
\/ the
carrier of W2)) implies W1 is
Subspace of W2 or W2 is
Subspace of W1
proof
given W such that
A1: the
carrier of W
= (the
carrier of W1
\/ the
carrier of W2);
set VW = the
carrier of W;
assume that
A2: not W1 is
Subspace of W2 and
A3: not W2 is
Subspace of W1;
not VW2
c= VW1 by
A3,
VECTSP_4: 27;
then
consider y be
object such that
A4: y
in VW2 and
A5: not y
in VW1;
reconsider y as
Element of VW2 by
A4;
reconsider y as
Element of M by
VECTSP_4: 10;
reconsider A1 = VW as
Subset of M by
VECTSP_4:def 2;
A6: A1 is
linearly-closed by
VECTSP_4: 33;
not VW1
c= VW2 by
A2,
VECTSP_4: 27;
then
consider x be
object such that
A7: x
in VW1 and
A8: not x
in VW2;
reconsider x as
Element of VW1 by
A7;
reconsider x as
Element of M by
VECTSP_4: 10;
A9:
now
reconsider A2 = VW2 as
Subset of M by
VECTSP_4:def 2;
A10: A2 is
linearly-closed by
VECTSP_4: 33;
assume (x
+ y)
in VW2;
then ((x
+ y)
- y)
in VW2 by
A10,
VECTSP_4: 3;
then (x
+ (y
- y))
in VW2 by
RLVECT_1:def 3;
then (x
+ (
0. M))
in VW2 by
VECTSP_1: 19;
hence contradiction by
A8,
RLVECT_1: 4;
end;
A11:
now
reconsider A2 = VW1 as
Subset of M by
VECTSP_4:def 2;
A12: A2 is
linearly-closed by
VECTSP_4: 33;
assume (x
+ y)
in VW1;
then ((y
+ x)
- x)
in VW1 by
A12,
VECTSP_4: 3;
then (y
+ (x
- x))
in VW1 by
RLVECT_1:def 3;
then (y
+ (
0. M))
in VW1 by
VECTSP_1: 19;
hence contradiction by
A5,
RLVECT_1: 4;
end;
x
in VW & y
in VW by
A1,
XBOOLE_0:def 3;
then (x
+ y)
in VW by
A6;
hence thesis by
A1,
A11,
A9,
XBOOLE_0:def 3;
end;
A13:
now
assume W1 is
Subspace of W2;
then VW1
c= VW2 by
VECTSP_4:def 2;
then (VW1
\/ VW2)
= VW2 by
XBOOLE_1: 12;
hence thesis;
end;
A14:
now
assume W2 is
Subspace of W1;
then VW2
c= VW1 by
VECTSP_4:def 2;
then (VW1
\/ VW2)
= VW1 by
XBOOLE_1: 12;
hence thesis;
end;
assume W1 is
Subspace of W2 or W2 is
Subspace of W1;
hence thesis by
A13,
A14;
end;
definition
let GF;
let M;
::
VECTSP_5:def3
func
Subspaces (M) ->
set means
:
Def3: for x be
object holds x
in it iff ex W be
strict
Subspace of M st W
= x;
existence
proof
defpred
R[
object,
object] means ex W be
strict
Subspace of M st $2
= W & $1
= the
carrier of W;
defpred
P[
object] means ex W be
strict
Subspace of M st $1
= the
carrier of W;
consider B be
set such that
A1: for x be
set holds x
in B iff x
in (
bool the
carrier of M) &
P[x] from
XFAMILY:sch 1;
A2: for x,y1,y2 be
object st
R[x, y1] &
R[x, y2] holds y1
= y2 by
VECTSP_4: 29;
consider f be
Function such that
A3: for x,y be
object holds
[x, y]
in f iff x
in B &
R[x, y] from
FUNCT_1:sch 1(
A2);
for x be
object holds x
in B iff ex y be
object st
[x, y]
in f
proof
let x be
object;
thus x
in B implies ex y be
object st
[x, y]
in f
proof
assume
A4: x
in B;
then
consider W be
strict
Subspace of M such that
A5: x
= the
carrier of W by
A1;
take W;
thus thesis by
A3,
A4,
A5;
end;
thus thesis by
A3;
end;
then
A6: B
= (
dom f) by
XTUPLE_0:def 12;
for y holds y
in (
rng f) iff ex W be
strict
Subspace of M st y
= W
proof
let y;
thus y
in (
rng f) implies ex W be
strict
Subspace of M st y
= W
proof
assume y
in (
rng f);
then
consider x be
object such that
A7: x
in (
dom f) & y
= (f
. x) by
FUNCT_1:def 3;
[x, y]
in f by
A7,
FUNCT_1:def 2;
then ex W be
strict
Subspace of M st y
= W & x
= the
carrier of W by
A3;
hence thesis;
end;
given W be
strict
Subspace of M such that
A8: y
= W;
reconsider W = y as
Subspace of M by
A8;
reconsider x = the
carrier of W as
set;
A9: y is
set by
TARSKI: 1;
the
carrier of W
c= the
carrier of M by
VECTSP_4:def 2;
then
A10: x
in (
dom f) by
A1,
A6,
A8;
then
[x, y]
in f by
A3,
A6,
A8;
then y
= (f
. x) by
A10,
FUNCT_1:def 2,
A9;
hence thesis by
A10,
FUNCT_1:def 3;
end;
hence thesis;
end;
uniqueness
proof
let D1,D2 be
set;
assume
A11: for x holds x
in D1 iff ex W be
strict
Subspace of M st x
= W;
assume
A12: for x holds x
in D2 iff ex W be
strict
Subspace of M st x
= W;
now
let x be
object;
thus x
in D1 implies x
in D2
proof
assume x
in D1;
then ex W be
strict
Subspace of M st x
= W by
A11;
hence thesis by
A12;
end;
assume x
in D2;
then ex W be
strict
Subspace of M st x
= W by
A12;
hence x
in D1 by
A11;
end;
hence thesis by
TARSKI: 2;
end;
end
registration
let GF;
let M;
cluster (
Subspaces M) -> non
empty;
coherence
proof
set W = the
strict
Subspace of M;
W
in (
Subspaces M) by
Def3;
hence thesis;
end;
end
theorem ::
VECTSP_5:36
for M be
strict
Abelian
add-associative
right_zeroed
right_complementable
vector-distributive
scalar-distributive
scalar-associative
scalar-unital non
empty
ModuleStr over GF holds M
in (
Subspaces M)
proof
let M be
strict
Abelian
add-associative
right_zeroed
right_complementable
vector-distributive
scalar-distributive
scalar-associative
scalar-unital non
empty
ModuleStr over GF;
ex W9 be
strict
Subspace of M st the
carrier of (
(Omega). M)
= the
carrier of W9;
hence thesis by
Def3;
end;
definition
let GF;
let M;
let W1, W2;
::
VECTSP_5:def4
pred M
is_the_direct_sum_of W1,W2 means the ModuleStr of M
= (W1
+ W2) & (W1
/\ W2)
= (
(0). M);
end
Lm16: (W1
+ W2)
= the ModuleStr of M iff for v be
Element of M holds ex v1,v2 be
Element of M st v1
in W1 & v2
in W2 & v
= (v1
+ v2)
proof
thus (W1
+ W2)
= the ModuleStr of M implies for v be
Element of M holds ex v1,v2 be
Element of M st v1
in W1 & v2
in W2 & v
= (v1
+ v2) by
RLVECT_1: 1,
Th1;
assume
A1: for v be
Element of M holds ex v1,v2 be
Element of M st v1
in W1 & v2
in W2 & v
= (v1
+ v2);
now
thus (W1
+ W2) is
Subspace of (
(Omega). M) by
Lm6;
let u be
Element of M;
ex v1,v2 be
Element of M st v1
in W1 & v2
in W2 & u
= (v1
+ v2) by
A1;
hence u
in (W1
+ W2) by
Th1;
end;
hence thesis by
VECTSP_4: 32;
end;
reserve F for
Field;
reserve V for
VectSp of F;
reserve W for
Subspace of V;
definition
let F, V, W;
::
VECTSP_5:def5
mode
Linear_Compl of W ->
Subspace of V means
:
Def5: V
is_the_direct_sum_of (it ,W);
existence
proof
defpred
P[
set,
set] means ex W1,W2 be
strict
Subspace of V st $1
= W1 & $2
= W2 & W1 is
Subspace of W2;
defpred
P[
set] means ex W1 be
strict
Subspace of V st $1
= W1 & (W
/\ W1)
= (
(0). V);
consider X such that
A1: for x be
set holds x
in X iff x
in (
Subspaces V) &
P[x] from
XFAMILY:sch 1;
(W
/\ (
(0). V))
= (
(0). V) & (
(0). V)
in (
Subspaces V) by
Def3,
Th20;
then
reconsider X as non
empty
set by
A1;
consider R be
Relation of X such that
A2: for x,y be
Element of X holds
[x, y]
in R iff
P[x, y] from
RELSET_1:sch 2;
defpred
Z[
set,
set] means
[$1, $2]
in R;
A3:
now
let x,y be
Element of X;
assume
Z[x, y] &
Z[y, x];
then (ex W1,W2 be
strict
Subspace of V st x
= W1 & y
= W2 & W1 is
Subspace of W2) & ex W3,W4 be
strict
Subspace of V st y
= W3 & x
= W4 & W3 is
Subspace of W4 by
A2;
hence x
= y by
VECTSP_4: 25;
end;
A4: for Y st Y
c= X & (for x,y be
Element of X st x
in Y & y
in Y holds
Z[x, y] or
Z[y, x]) holds ex y be
Element of X st for x be
Element of X st x
in Y holds
Z[x, y]
proof
let Y;
assume that
A5: Y
c= X and
A6: for x,y be
Element of X st x
in Y & y
in Y holds
[x, y]
in R or
[y, x]
in R;
now
per cases ;
suppose
A7: Y
=
{} ;
set y = the
Element of X;
take y9 = y;
let x be
Element of X;
assume x
in Y;
hence
[x, y9]
in R by
A7;
end;
suppose
A8: Y
<>
{} ;
defpred
P[
object,
object] means ex W1 be
strict
Subspace of V st $1
= W1 & $2
= the
carrier of W1;
A9: for x be
object st x
in Y holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in Y;
then
consider W1 be
strict
Subspace of V such that
A10: x
= W1 and (W
/\ W1)
= (
(0). V) by
A1,
A5;
reconsider y = the
carrier of W1 as
set;
take y;
take W1;
thus thesis by
A10;
end;
consider f be
Function such that
A11: (
dom f)
= Y and
A12: for x be
object st x
in Y holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A9);
set Z = (
union (
rng f));
now
let x be
object;
assume x
in Z;
then
consider Y9 be
set such that
A13: x
in Y9 and
A14: Y9
in (
rng f) by
TARSKI:def 4;
consider y be
object such that
A15: y
in (
dom f) and
A16: (f
. y)
= Y9 by
A14,
FUNCT_1:def 3;
consider W1 be
strict
Subspace of V such that y
= W1 and
A17: (f
. y)
= the
carrier of W1 by
A11,
A12,
A15;
the
carrier of W1
c= the
carrier of V by
VECTSP_4:def 2;
hence x
in the
carrier of V by
A13,
A16,
A17;
end;
then
reconsider Z as
Subset of V by
TARSKI:def 3;
A18: Z is
linearly-closed
proof
thus for v1,v2 be
Element of V st v1
in Z & v2
in Z holds (v1
+ v2)
in Z
proof
let v1,v2 be
Element of V;
assume that
A19: v1
in Z and
A20: v2
in Z;
consider Y1 be
set such that
A21: v1
in Y1 and
A22: Y1
in (
rng f) by
A19,
TARSKI:def 4;
consider y1 be
object such that
A23: y1
in (
dom f) and
A24: (f
. y1)
= Y1 by
A22,
FUNCT_1:def 3;
consider Y2 be
set such that
A25: v2
in Y2 and
A26: Y2
in (
rng f) by
A20,
TARSKI:def 4;
consider y2 be
object such that
A27: y2
in (
dom f) and
A28: (f
. y2)
= Y2 by
A26,
FUNCT_1:def 3;
consider W1 be
strict
Subspace of V such that
A29: y1
= W1 and
A30: (f
. y1)
= the
carrier of W1 by
A11,
A12,
A23;
consider W2 be
strict
Subspace of V such that
A31: y2
= W2 and
A32: (f
. y2)
= the
carrier of W2 by
A11,
A12,
A27;
reconsider y1, y2 as
Element of X by
A5,
A11,
A23,
A27;
now
per cases by
A6,
A11,
A23,
A27;
suppose
[y1, y2]
in R;
then ex W3,W4 be
strict
Subspace of V st y1
= W3 & y2
= W4 & W3 is
Subspace of W4 by
A2;
then the
carrier of W1
c= the
carrier of W2 by
A29,
A31,
VECTSP_4:def 2;
then
A33: v1
in W2 by
A21,
A24,
A30,
STRUCT_0:def 5;
v2
in W2 by
A25,
A28,
A32,
STRUCT_0:def 5;
then (v1
+ v2)
in W2 by
A33,
VECTSP_4: 20;
then
A34: (v1
+ v2)
in the
carrier of W2 by
STRUCT_0:def 5;
(f
. y2)
in (
rng f) by
A27,
FUNCT_1:def 3;
hence thesis by
A32,
A34,
TARSKI:def 4;
end;
suppose
[y2, y1]
in R;
then ex W3,W4 be
strict
Subspace of V st y2
= W3 & y1
= W4 & W3 is
Subspace of W4 by
A2;
then the
carrier of W2
c= the
carrier of W1 by
A29,
A31,
VECTSP_4:def 2;
then
A35: v2
in W1 by
A25,
A28,
A32,
STRUCT_0:def 5;
v1
in W1 by
A21,
A24,
A30,
STRUCT_0:def 5;
then (v1
+ v2)
in W1 by
A35,
VECTSP_4: 20;
then
A36: (v1
+ v2)
in the
carrier of W1 by
STRUCT_0:def 5;
(f
. y1)
in (
rng f) by
A23,
FUNCT_1:def 3;
hence thesis by
A30,
A36,
TARSKI:def 4;
end;
end;
hence thesis;
end;
let a be
Element of F, v1 be
Element of V;
assume v1
in Z;
then
consider Y1 be
set such that
A37: v1
in Y1 and
A38: Y1
in (
rng f) by
TARSKI:def 4;
consider y1 be
object such that
A39: y1
in (
dom f) and
A40: (f
. y1)
= Y1 by
A38,
FUNCT_1:def 3;
consider W1 be
strict
Subspace of V such that y1
= W1 and
A41: (f
. y1)
= the
carrier of W1 by
A11,
A12,
A39;
v1
in W1 by
A37,
A40,
A41,
STRUCT_0:def 5;
then (a
* v1)
in W1 by
VECTSP_4: 21;
then
A42: (a
* v1)
in the
carrier of W1 by
STRUCT_0:def 5;
(f
. y1)
in (
rng f) by
A39,
FUNCT_1:def 3;
hence thesis by
A41,
A42,
TARSKI:def 4;
end;
set z = the
Element of (
rng f);
A43: (
rng f)
<>
{} by
A8,
A11,
RELAT_1: 42;
then
consider z1 be
object such that
A44: z1
in (
dom f) and
A45: (f
. z1)
= z by
FUNCT_1:def 3;
ex W3 be
strict
Subspace of V st z1
= W3 & (f
. z1)
= the
carrier of W3 by
A11,
A12,
A44;
then Z
<>
{} by
A43,
A45,
ORDERS_1: 6;
then
consider E be
strict
Subspace of V such that
A46: Z
= the
carrier of E by
A18,
VECTSP_4: 34;
now
let u be
Element of V;
thus u
in (W
/\ E) implies u
in (
(0). V)
proof
assume
A47: u
in (W
/\ E);
then
A48: u
in W by
Th3;
u
in E by
A47,
Th3;
then u
in Z by
A46,
STRUCT_0:def 5;
then
consider Y1 be
set such that
A49: u
in Y1 and
A50: Y1
in (
rng f) by
TARSKI:def 4;
consider y1 be
object such that
A51: y1
in (
dom f) and
A52: (f
. y1)
= Y1 by
A50,
FUNCT_1:def 3;
A53: ex W2 be
strict
Subspace of V st y1
= W2 & (W
/\ W2)
= (
(0). V) by
A1,
A5,
A11,
A51;
consider W1 be
strict
Subspace of V such that
A54: y1
= W1 and
A55: (f
. y1)
= the
carrier of W1 by
A11,
A12,
A51;
u
in W1 by
A49,
A52,
A55,
STRUCT_0:def 5;
hence thesis by
A54,
A48,
A53,
Th3;
end;
assume u
in (
(0). V);
then u
in the
carrier of (
(0). V) by
STRUCT_0:def 5;
then u
in
{(
0. V)} by
VECTSP_4:def 3;
then u
= (
0. V) by
TARSKI:def 1;
hence u
in (W
/\ E) by
VECTSP_4: 17;
end;
then
A56: (W
/\ E)
= (
(0). V) by
VECTSP_4: 30;
E
in (
Subspaces V) by
Def3;
then
reconsider y9 = E as
Element of X by
A1,
A56;
take y = y9;
let x be
Element of X;
assume
A57: x
in Y;
then
consider W1 be
strict
Subspace of V such that
A58: x
= W1 and
A59: (f
. x)
= the
carrier of W1 by
A12;
now
let u be
Element of V;
assume u
in W1;
then
A60: u
in the
carrier of W1 by
STRUCT_0:def 5;
the
carrier of W1
in (
rng f) by
A11,
A57,
A59,
FUNCT_1:def 3;
then u
in Z by
A60,
TARSKI:def 4;
hence u
in E by
A46,
STRUCT_0:def 5;
end;
then W1 is
Subspace of E by
VECTSP_4: 28;
hence
[x, y]
in R by
A2,
A58;
end;
end;
hence thesis;
end;
A61:
now
let x,y,z be
Element of X;
assume that
A62:
Z[x, y] and
A63:
Z[y, z];
consider W1,W2 be
strict
Subspace of V such that
A64: x
= W1 and
A65: y
= W2 & W1 is
Subspace of W2 by
A2,
A62;
consider W3,W4 be
strict
Subspace of V such that
A66: y
= W3 and
A67: z
= W4 and
A68: W3 is
Subspace of W4 by
A2,
A63;
W1 is
Subspace of W4 by
A65,
A66,
A68,
VECTSP_4: 26;
hence
Z[x, z] by
A2,
A64,
A67;
end;
A69:
now
let x be
Element of X;
consider W1 be
strict
Subspace of V such that
A70: x
= W1 and (W
/\ W1)
= (
(0). V) by
A1;
W1 is
Subspace of W1 by
VECTSP_4: 24;
hence
Z[x, x] by
A2,
A70;
end;
consider x be
Element of X such that
A71: for y be
Element of X st x
<> y holds not
Z[x, y] from
ORDERS_1:sch 1(
A69,
A3,
A61,
A4);
consider L be
strict
Subspace of V such that
A72: x
= L and
A73: (W
/\ L)
= (
(0). V) by
A1;
take L;
thus the ModuleStr of V
= (L
+ W)
proof
assume not thesis;
then
consider v be
Element of V such that
A74: for v1,v2 be
Element of V holds not v1
in L or not v2
in W or v
<> (v1
+ v2) by
Lm16;
v
= ((
0. V)
+ v) & (
0. V)
in W by
RLVECT_1: 4,
VECTSP_4: 17;
then
A75: not v
in L by
A74;
set A = the set of all (a
* v) where a be
Element of F;
A76: ((
1_ F)
* v)
in A;
now
let x be
object;
assume x
in A;
then ex a be
Element of F st x
= (a
* v);
hence x
in the
carrier of V;
end;
then
reconsider A as
Subset of V by
TARSKI:def 3;
A is
linearly-closed
proof
thus for v1,v2 be
Element of V st v1
in A & v2
in A holds (v1
+ v2)
in A
proof
let v1,v2 be
Element of V;
assume v1
in A;
then
consider a1 be
Element of F such that
A77: v1
= (a1
* v);
assume v2
in A;
then
consider a2 be
Element of F such that
A78: v2
= (a2
* v);
(v1
+ v2)
= ((a1
+ a2)
* v) by
A77,
A78,
VECTSP_1:def 15;
hence thesis;
end;
let a be
Element of F, v1 be
Element of V;
assume v1
in A;
then
consider a1 be
Element of F such that
A79: v1
= (a1
* v);
(a
* v1)
= ((a
* a1)
* v) by
A79,
VECTSP_1:def 16;
hence thesis;
end;
then
consider Z be
strict
Subspace of V such that
A80: the
carrier of Z
= A by
A76,
VECTSP_4: 34;
A81: not v
in (L
+ W) by
A74,
Th1;
now
let u be
Element of V;
thus u
in (Z
/\ (W
+ L)) implies u
in (
(0). V)
proof
assume
A82: u
in (Z
/\ (W
+ L));
then u
in Z by
Th3;
then u
in A by
A80,
STRUCT_0:def 5;
then
consider a be
Element of F such that
A83: u
= (a
* v);
now
u
in (W
+ L) by
A82,
Th3;
then ((a
" )
* (a
* v))
in (W
+ L) by
A83,
VECTSP_4: 21;
then
A84: (((a
" )
* a)
* v)
in (W
+ L) by
VECTSP_1:def 16;
assume a
<> (
0. F);
then ((
1_ F)
* v)
in (W
+ L) by
A84,
VECTSP_1:def 10;
then ((
1_ F)
* v)
in (L
+ W) by
Lm1;
hence contradiction by
A81,
VECTSP_1:def 17;
end;
then u
= (
0. V) by
A83,
VECTSP_1: 14;
hence thesis by
VECTSP_4: 17;
end;
assume u
in (
(0). V);
then u
in the
carrier of (
(0). V) by
STRUCT_0:def 5;
then u
in
{(
0. V)} by
VECTSP_4:def 3;
then u
= (
0. V) by
TARSKI:def 1;
hence u
in (Z
/\ (W
+ L)) by
VECTSP_4: 17;
end;
then
A85: (Z
/\ (W
+ L))
= (
(0). V) by
VECTSP_4: 30;
now
let u be
Element of V;
thus u
in ((Z
+ L)
/\ W) implies u
in (
(0). V)
proof
assume
A86: u
in ((Z
+ L)
/\ W);
then u
in (Z
+ L) by
Th3;
then
consider v1,v2 be
Element of V such that
A87: v1
in Z and
A88: v2
in L and
A89: u
= (v1
+ v2) by
Th1;
A90: u
in W by
A86,
Th3;
then
A91: u
in (W
+ L) by
Th2;
v1
= (u
- v2) & v2
in (W
+ L) by
A88,
A89,
Th2,
VECTSP_2: 2;
then v1
in (W
+ L) by
A91,
VECTSP_4: 23;
then v1
in (Z
/\ (W
+ L)) by
A87,
Th3;
then v1
in the
carrier of (
(0). V) by
A85,
STRUCT_0:def 5;
then v1
in
{(
0. V)} by
VECTSP_4:def 3;
then v1
= (
0. V) by
TARSKI:def 1;
then v2
= u by
A89,
RLVECT_1: 4;
hence thesis by
A73,
A88,
A90,
Th3;
end;
assume u
in (
(0). V);
then u
in the
carrier of (
(0). V) by
STRUCT_0:def 5;
then u
in
{(
0. V)} by
VECTSP_4:def 3;
then u
= (
0. V) by
TARSKI:def 1;
hence u
in ((Z
+ L)
/\ W) by
VECTSP_4: 17;
end;
then
A92: (W
/\ (Z
+ L))
= (
(0). V) by
VECTSP_4: 30;
(Z
+ L)
in (
Subspaces V) by
Def3;
then
reconsider x1 = (Z
+ L) as
Element of X by
A1,
A92;
L is
Subspace of (Z
+ L) by
Th7;
then
A93:
[x, x1]
in R by
A2,
A72;
v
in A by
A76,
VECTSP_1:def 17;
then v
in Z by
A80,
STRUCT_0:def 5;
then (Z
+ L)
<> L by
A75,
Th2;
hence contradiction by
A71,
A72,
A93;
end;
thus thesis by
A73;
end;
end
Lm17: for W1,W2 be
Subspace of M holds M
is_the_direct_sum_of (W1,W2) implies M
is_the_direct_sum_of (W2,W1) by
Lm1;
reserve W,W1,W2 for
Subspace of V;
theorem ::
VECTSP_5:37
V
is_the_direct_sum_of (W1,W2) implies W2 is
Linear_Compl of W1 by
Lm17,
Def5;
theorem ::
VECTSP_5:38
Th38: for L be
Linear_Compl of W holds V
is_the_direct_sum_of (L,W) & V
is_the_direct_sum_of (W,L) by
Def5,
Lm17;
theorem ::
VECTSP_5:39
Th39: for L be
Linear_Compl of W holds (W
+ L)
= the ModuleStr of V & (L
+ W)
= the ModuleStr of V
proof
let L be
Linear_Compl of W;
V
is_the_direct_sum_of (W,L) by
Th38;
hence (W
+ L)
= the ModuleStr of V;
hence thesis by
Lm1;
end;
theorem ::
VECTSP_5:40
Th40: for L be
Linear_Compl of W holds (W
/\ L)
= (
(0). V) & (L
/\ W)
= (
(0). V)
proof
let L be
Linear_Compl of W;
A1: V
is_the_direct_sum_of (W,L) by
Th38;
hence (W
/\ L)
= (
(0). V);
thus thesis by
A1;
end;
reserve W1,W2 for
Subspace of M;
theorem ::
VECTSP_5:41
M
is_the_direct_sum_of (W1,W2) implies M
is_the_direct_sum_of (W2,W1) by
Lm17;
theorem ::
VECTSP_5:42
Th42: M
is_the_direct_sum_of ((
(0). M),(
(Omega). M)) & M
is_the_direct_sum_of ((
(Omega). M),(
(0). M)) by
Th9,
Th20;
reserve W for
Subspace of V;
theorem ::
VECTSP_5:43
for L be
Linear_Compl of W holds W is
Linear_Compl of L
proof
let L be
Linear_Compl of W;
V
is_the_direct_sum_of (L,W) by
Def5;
then V
is_the_direct_sum_of (W,L) by
Lm17;
hence thesis by
Def5;
end;
theorem ::
VECTSP_5:44
(
(0). V) is
Linear_Compl of (
(Omega). V) & (
(Omega). V) is
Linear_Compl of (
(0). V) by
Th42,
Def5;
reserve W1,W2 for
Subspace of M;
reserve u,u1,u2,v for
Element of M;
reserve C1 for
Coset of W1;
reserve C2 for
Coset of W2;
theorem ::
VECTSP_5:45
Th45: C1
meets C2 implies (C1
/\ C2) is
Coset of (W1
/\ W2)
proof
set v = the
Element of (C1
/\ C2);
set C = (C1
/\ C2);
assume
A1: (C1
/\ C2)
<>
{} ;
then
reconsider v as
Element of M by
TARSKI:def 3;
v
in C2 by
A1,
XBOOLE_0:def 4;
then
A2: C2
= (v
+ W2) by
VECTSP_4: 77;
v
in C1 by
A1,
XBOOLE_0:def 4;
then
A3: C1
= (v
+ W1) by
VECTSP_4: 77;
C is
Coset of (W1
/\ W2)
proof
take v;
thus C
c= (v
+ (W1
/\ W2))
proof
let x be
object;
assume
A4: x
in C;
then x
in C1 by
XBOOLE_0:def 4;
then
consider u1 such that
A5: u1
in W1 and
A6: x
= (v
+ u1) by
A3,
VECTSP_4: 42;
x
in C2 by
A4,
XBOOLE_0:def 4;
then
consider u2 such that
A7: u2
in W2 and
A8: x
= (v
+ u2) by
A2,
VECTSP_4: 42;
u1
= u2 by
A6,
A8,
RLVECT_1: 8;
then u1
in (W1
/\ W2) by
A5,
A7,
Th3;
hence thesis by
A6;
end;
let x be
object;
assume x
in (v
+ (W1
/\ W2));
then
consider u such that
A9: u
in (W1
/\ W2) and
A10: x
= (v
+ u) by
VECTSP_4: 42;
u
in W2 by
A9,
Th3;
then
A11: x
in { (v
+ u2) : u2
in W2 } by
A10;
u
in W1 by
A9,
Th3;
then x
in { (v
+ u1) : u1
in W1 } by
A10;
hence thesis by
A3,
A2,
A11,
XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem ::
VECTSP_5:46
Th46: M
is_the_direct_sum_of (W1,W2) iff for C1 be
Coset of W1, C2 be
Coset of W2 holds ex v be
Element of M st (C1
/\ C2)
=
{v}
proof
set VW1 = the
carrier of W1;
set VW2 = the
carrier of W2;
A1: (W1
+ W2) is
Subspace of (
(Omega). M) by
Lm6;
thus M
is_the_direct_sum_of (W1,W2) implies for C1 be
Coset of W1, C2 be
Coset of W2 holds ex v be
Element of M st (C1
/\ C2)
=
{v}
proof
assume
A2: M
is_the_direct_sum_of (W1,W2);
then
A3: the ModuleStr of M
= (W1
+ W2);
let C1 be
Coset of W1, C2 be
Coset of W2;
consider v1 be
Element of M such that
A4: C1
= (v1
+ W1) by
VECTSP_4:def 6;
v1
in (
(Omega). M) by
RLVECT_1: 1;
then
consider v11,v12 be
Element of M such that
A5: v11
in W1 and
A6: v12
in W2 and
A7: v1
= (v11
+ v12) by
A3,
Th1;
consider v2 be
Element of M such that
A8: C2
= (v2
+ W2) by
VECTSP_4:def 6;
v2
in (
(Omega). M) by
RLVECT_1: 1;
then
consider v21,v22 be
Element of M such that
A9: v21
in W1 and
A10: v22
in W2 and
A11: v2
= (v21
+ v22) by
A3,
Th1;
take v = (v12
+ v21);
{v}
= (C1
/\ C2)
proof
thus
A12:
{v}
c= (C1
/\ C2)
proof
let x be
object;
assume x
in
{v};
then
A13: x
= v by
TARSKI:def 1;
v21
= (v2
- v22) by
A11,
VECTSP_2: 2;
then v21
in C2 by
A8,
A10,
VECTSP_4: 62;
then C2
= (v21
+ W2) by
VECTSP_4: 77;
then
A14: x
in C2 by
A6,
A13;
v12
= (v1
- v11) by
A7,
VECTSP_2: 2;
then v12
in C1 by
A4,
A5,
VECTSP_4: 62;
then C1
= (v12
+ W1) by
VECTSP_4: 77;
then x
in C1 by
A9,
A13;
hence thesis by
A14,
XBOOLE_0:def 4;
end;
let x be
object;
assume
A15: x
in (C1
/\ C2);
then C1
meets C2;
then
reconsider C = (C1
/\ C2) as
Coset of (W1
/\ W2) by
Th45;
A16: v
in
{v} by
TARSKI:def 1;
(W1
/\ W2)
= (
(0). M) by
A2;
then ex u be
Element of M st C
=
{u} by
VECTSP_4: 72;
hence thesis by
A12,
A15,
A16,
TARSKI:def 1;
end;
hence thesis;
end;
assume
A17: for C1 be
Coset of W1, C2 be
Coset of W2 holds ex v be
Element of M st (C1
/\ C2)
=
{v};
A18: VW2 is
Coset of W2 by
VECTSP_4: 73;
A19: the
carrier of M
c= the
carrier of (W1
+ W2)
proof
let x be
object;
assume x
in the
carrier of M;
then
reconsider u = x as
Element of M;
consider C1 be
Coset of W1 such that
A20: u
in C1 by
VECTSP_4: 68;
consider v be
Element of M such that
A21: (C1
/\ VW2)
=
{v} by
A18,
A17;
A22: v
in
{v} by
TARSKI:def 1;
then v
in C1 by
A21,
XBOOLE_0:def 4;
then
consider v1 be
Element of M such that
A23: v1
in W1 and
A24: (u
- v1)
= v by
A20,
VECTSP_4: 79;
v
in VW2 by
A21,
A22,
XBOOLE_0:def 4;
then
A25: v
in W2 by
STRUCT_0:def 5;
u
= (v1
+ v) by
A24,
VECTSP_2: 2;
then x
in (W1
+ W2) by
A25,
A23,
Th1;
hence thesis by
STRUCT_0:def 5;
end;
VW1 is
Coset of W1 by
VECTSP_4: 73;
then
consider v be
Element of M such that
A26: (VW1
/\ VW2)
=
{v} by
A18,
A17;
the
carrier of (W1
+ W2)
c= the
carrier of M by
VECTSP_4:def 2;
then the
carrier of M
= the
carrier of (W1
+ W2) by
A19;
hence the ModuleStr of M
= (W1
+ W2) by
A1,
VECTSP_4: 31;
(
0. M)
in W2 by
VECTSP_4: 17;
then
A27: (
0. M)
in VW2 by
STRUCT_0:def 5;
(
0. M)
in W1 by
VECTSP_4: 17;
then (
0. M)
in VW1 by
STRUCT_0:def 5;
then
A28: (
0. M)
in
{v} by
A26,
A27,
XBOOLE_0:def 4;
the
carrier of (
(0). M)
=
{(
0. M)} by
VECTSP_4:def 3
.= (VW1
/\ VW2) by
A26,
A28,
TARSKI:def 1
.= the
carrier of (W1
/\ W2) by
Def2;
hence thesis by
VECTSP_4: 29;
end;
theorem ::
VECTSP_5:47
for M be
strict
Abelian
add-associative
right_zeroed
right_complementable
vector-distributive
scalar-distributive
scalar-associative
scalar-unital non
empty
ModuleStr over GF, W1,W2 be
Subspace of M holds (W1
+ W2)
= M iff for v be
Element of M holds ex v1,v2 be
Element of M st v1
in W1 & v2
in W2 & v
= (v1
+ v2) by
Lm16;
theorem ::
VECTSP_5:48
Th48: for v,v1,v2,u1,u2 be
Element of M holds M
is_the_direct_sum_of (W1,W2) & v
= (v1
+ v2) & v
= (u1
+ u2) & v1
in W1 & u1
in W1 & v2
in W2 & u2
in W2 implies v1
= u1 & v2
= u2
proof
let v,v1,v2,u1,u2 be
Element of M;
reconsider C2 = (v1
+ W2) as
Coset of W2 by
VECTSP_4:def 6;
reconsider C1 = the
carrier of W1 as
Coset of W1 by
VECTSP_4: 73;
A1: v1
in C2 by
VECTSP_4: 44;
assume M
is_the_direct_sum_of (W1,W2);
then
consider u be
Element of M such that
A2: (C1
/\ C2)
=
{u} by
Th46;
assume that
A3: v
= (v1
+ v2) & v
= (u1
+ u2) and
A4: v1
in W1 and
A5: u1
in W1 and
A6: v2
in W2 & u2
in W2;
A7: (v2
- u2)
in W2 by
A6,
VECTSP_4: 23;
v1
in C1 by
A4,
STRUCT_0:def 5;
then v1
in (C1
/\ C2) by
A1,
XBOOLE_0:def 4;
then
A8: v1
= u by
A2,
TARSKI:def 1;
A9: u1
in C1 by
A5,
STRUCT_0:def 5;
u1
= ((v1
+ v2)
- u2) by
A3,
VECTSP_2: 2
.= (v1
+ (v2
- u2)) by
RLVECT_1:def 3;
then u1
in C2 by
A7;
then
A10: u1
in (C1
/\ C2) by
A9,
XBOOLE_0:def 4;
hence v1
= u1 by
A2,
A8,
TARSKI:def 1;
u1
= u by
A10,
A2,
TARSKI:def 1;
hence thesis by
A3,
A8,
RLVECT_1: 8;
end;
theorem ::
VECTSP_5:49
M
= (W1
+ W2) & (ex v st for v1,v2,u1,u2 be
Element of M st v
= (v1
+ v2) & v
= (u1
+ u2) & v1
in W1 & u1
in W1 & v2
in W2 & u2
in W2 holds v1
= u1 & v2
= u2) implies M
is_the_direct_sum_of (W1,W2)
proof
assume
A1: M
= (W1
+ W2);
the
carrier of (
(0). M)
=
{(
0. M)} & (
(0). M) is
Subspace of (W1
/\ W2) by
VECTSP_4: 39,
VECTSP_4:def 3;
then
A2:
{(
0. M)}
c= the
carrier of (W1
/\ W2) by
VECTSP_4:def 2;
given v such that
A3: for v1,v2,u1,u2 be
Element of M st v
= (v1
+ v2) & v
= (u1
+ u2) & v1
in W1 & u1
in W1 & v2
in W2 & u2
in W2 holds v1
= u1 & v2
= u2;
assume not thesis;
then (W1
/\ W2)
<> (
(0). M) by
A1;
then the
carrier of (W1
/\ W2)
<>
{(
0. M)} by
VECTSP_4:def 3;
then
{(
0. M)}
c< the
carrier of (W1
/\ W2) by
A2;
then
consider x be
object such that
A4: x
in the
carrier of (W1
/\ W2) and
A5: not x
in
{(
0. M)} by
XBOOLE_0: 6;
A6: x
in (W1
/\ W2) by
A4,
STRUCT_0:def 5;
then x
in M by
VECTSP_4: 9;
then
reconsider u = x as
Element of M by
STRUCT_0:def 5;
consider v1,v2 be
Element of M such that
A7: v1
in W1 and
A8: v2
in W2 and
A9: v
= (v1
+ v2) by
A1,
Lm16;
A10: v
= ((v1
+ v2)
+ (
0. M)) by
A9,
RLVECT_1: 4
.= ((v1
+ v2)
+ (u
- u)) by
VECTSP_1: 19
.= (((v1
+ v2)
+ u)
- u) by
RLVECT_1:def 3
.= (((v1
+ u)
+ v2)
- u) by
RLVECT_1:def 3
.= ((v1
+ u)
+ (v2
- u)) by
RLVECT_1:def 3;
x
in W2 by
A6,
Th3;
then
A11: (v2
- u)
in W2 by
A8,
VECTSP_4: 23;
x
in W1 by
A6,
Th3;
then (v1
+ u)
in W1 by
A7,
VECTSP_4: 20;
then (v2
- u)
= v2 by
A3,
A7,
A8,
A9,
A10,
A11;
then (v2
+ (
- u))
= (v2
+ (
0. M)) by
RLVECT_1: 4;
then (
- u)
= (
0. M) by
RLVECT_1: 8;
then
A12: u
= (
- (
0. M)) by
RLVECT_1: 17;
x
<> (
0. M) by
A5,
TARSKI:def 1;
hence thesis by
A12,
RLVECT_1: 12;
end;
reserve t1,t2 for
Element of
[:the
carrier of M, the
carrier of M:];
definition
let GF, M, v, W1, W2;
assume
A1: M
is_the_direct_sum_of (W1,W2);
::
VECTSP_5:def6
func v
|-- (W1,W2) ->
Element of
[:the
carrier of M, the
carrier of M:] means
:
Def6: v
= ((it
`1 )
+ (it
`2 )) & (it
`1 )
in W1 & (it
`2 )
in W2;
existence
proof
(W1
+ W2)
= the ModuleStr of M by
A1;
then
consider v1,v2 be
Element of M such that
A2: v1
in W1 & v2
in W2 & v
= (v1
+ v2) by
Lm16;
take
[v1, v2];
thus thesis by
A2;
end;
uniqueness
proof
let t1, t2;
assume v
= ((t1
`1 )
+ (t1
`2 )) & (t1
`1 )
in W1 & (t1
`2 )
in W2 & v
= ((t2
`1 )
+ (t2
`2 )) & (t2
`1 )
in W1 & (t2
`2 )
in W2;
then
A3: (t1
`1 )
= (t2
`1 ) & (t1
`2 )
= (t2
`2 ) by
A1,
Th48;
t1
=
[(t1
`1 ), (t1
`2 )] by
MCART_1: 21;
hence thesis by
A3,
MCART_1: 21;
end;
end
theorem ::
VECTSP_5:50
Th50: M
is_the_direct_sum_of (W1,W2) implies ((v
|-- (W1,W2))
`1 )
= ((v
|-- (W2,W1))
`2 )
proof
assume
A1: M
is_the_direct_sum_of (W1,W2);
then
A2: ((v
|-- (W1,W2))
`2 )
in W2 by
Def6;
A3: M
is_the_direct_sum_of (W2,W1) by
A1,
Lm17;
then
A4: v
= (((v
|-- (W2,W1))
`2 )
+ ((v
|-- (W2,W1))
`1 )) & ((v
|-- (W2,W1))
`1 )
in W2 by
Def6;
A5: ((v
|-- (W2,W1))
`2 )
in W1 by
A3,
Def6;
v
= (((v
|-- (W1,W2))
`1 )
+ ((v
|-- (W1,W2))
`2 )) & ((v
|-- (W1,W2))
`1 )
in W1 by
A1,
Def6;
hence thesis by
A1,
A2,
A4,
A5,
Th48;
end;
theorem ::
VECTSP_5:51
Th51: M
is_the_direct_sum_of (W1,W2) implies ((v
|-- (W1,W2))
`2 )
= ((v
|-- (W2,W1))
`1 )
proof
assume
A1: M
is_the_direct_sum_of (W1,W2);
then
A2: ((v
|-- (W1,W2))
`2 )
in W2 by
Def6;
A3: M
is_the_direct_sum_of (W2,W1) by
A1,
Lm17;
then
A4: v
= (((v
|-- (W2,W1))
`2 )
+ ((v
|-- (W2,W1))
`1 )) & ((v
|-- (W2,W1))
`1 )
in W2 by
Def6;
A5: ((v
|-- (W2,W1))
`2 )
in W1 by
A3,
Def6;
v
= (((v
|-- (W1,W2))
`1 )
+ ((v
|-- (W1,W2))
`2 )) & ((v
|-- (W1,W2))
`1 )
in W1 by
A1,
Def6;
hence thesis by
A1,
A2,
A4,
A5,
Th48;
end;
reserve W for
Subspace of V;
theorem ::
VECTSP_5:52
for L be
Linear_Compl of W, v be
Element of V, t be
Element of
[:the
carrier of V, the
carrier of V:] holds ((t
`1 )
+ (t
`2 ))
= v & (t
`1 )
in W & (t
`2 )
in L implies t
= (v
|-- (W,L))
proof
let L be
Linear_Compl of W;
let v be
Element of V;
let t be
Element of
[:the
carrier of V, the
carrier of V:];
V
is_the_direct_sum_of (W,L) by
Th38;
hence thesis by
Def6;
end;
theorem ::
VECTSP_5:53
for L be
Linear_Compl of W, v be
Element of V holds (((v
|-- (W,L))
`1 )
+ ((v
|-- (W,L))
`2 ))
= v
proof
let L be
Linear_Compl of W;
let v be
Element of V;
V
is_the_direct_sum_of (W,L) by
Th38;
hence thesis by
Def6;
end;
theorem ::
VECTSP_5:54
for L be
Linear_Compl of W, v be
Element of V holds ((v
|-- (W,L))
`1 )
in W & ((v
|-- (W,L))
`2 )
in L
proof
let L be
Linear_Compl of W;
let v be
Element of V;
V
is_the_direct_sum_of (W,L) by
Th38;
hence thesis by
Def6;
end;
theorem ::
VECTSP_5:55
for L be
Linear_Compl of W, v be
Element of V holds ((v
|-- (W,L))
`1 )
= ((v
|-- (L,W))
`2 ) by
Th38,
Th50;
theorem ::
VECTSP_5:56
for L be
Linear_Compl of W, v be
Element of V holds ((v
|-- (W,L))
`2 )
= ((v
|-- (L,W))
`1 ) by
Th38,
Th51;
reserve A1,A2,B for
Element of (
Subspaces M),
W1,W2 for
Subspace of M;
definition
let GF;
let M;
::
VECTSP_5:def7
func
SubJoin M ->
BinOp of (
Subspaces M) means
:
Def7: for A1, A2, W1, W2 st A1
= W1 & A2
= W2 holds (it
. (A1,A2))
= (W1
+ W2);
existence
proof
defpred
P[
set,
set,
set] means for W1, W2 st $1
= W1 & $2
= W2 holds $3
= (W1
+ W2);
A1: for A1, A2 holds ex B st
P[A1, A2, B]
proof
let A1, A2;
consider W1 be
strict
Subspace of M such that
A2: W1
= A1 by
Def3;
consider W2 be
strict
Subspace of M such that
A3: W2
= A2 by
Def3;
reconsider C = (W1
+ W2) as
Element of (
Subspaces M) by
Def3;
take C;
thus thesis by
A2,
A3;
end;
thus ex o be
BinOp of (
Subspaces M) st for A1, A2 holds
P[A1, A2, (o
. (A1,A2))] from
BINOP_1:sch 3(
A1);
end;
uniqueness
proof
let o1,o2 be
BinOp of (
Subspaces M);
assume
A4: for A1, A2, W1, W2 st A1
= W1 & A2
= W2 holds (o1
. (A1,A2))
= (W1
+ W2);
assume
A5: for A1, A2, W1, W2 st A1
= W1 & A2
= W2 holds (o2
. (A1,A2))
= (W1
+ W2);
now
let x,y be
set;
assume that
A6: x
in (
Subspaces M) and
A7: y
in (
Subspaces M);
reconsider A = x, B = y as
Element of (
Subspaces M) by
A6,
A7;
consider W1 be
strict
Subspace of M such that
A8: W1
= x by
A6,
Def3;
consider W2 be
strict
Subspace of M such that
A9: W2
= y by
A7,
Def3;
(o1
. (A,B))
= (W1
+ W2) by
A4,
A8,
A9;
hence (o1
. (x,y))
= (o2
. (x,y)) by
A5,
A8,
A9;
end;
hence thesis by
BINOP_1: 1;
end;
end
definition
let GF;
let M;
::
VECTSP_5:def8
func
SubMeet M ->
BinOp of (
Subspaces M) means
:
Def8: for A1, A2, W1, W2 st A1
= W1 & A2
= W2 holds (it
. (A1,A2))
= (W1
/\ W2);
existence
proof
defpred
P[
set,
set,
set] means for W1, W2 st $1
= W1 & $2
= W2 holds $3
= (W1
/\ W2);
A1: for A1, A2 holds ex B st
P[A1, A2, B]
proof
let A1, A2;
consider W1 be
strict
Subspace of M such that
A2: W1
= A1 by
Def3;
consider W2 be
strict
Subspace of M such that
A3: W2
= A2 by
Def3;
reconsider C = (W1
/\ W2) as
Element of (
Subspaces M) by
Def3;
take C;
thus thesis by
A2,
A3;
end;
thus ex o be
BinOp of (
Subspaces M) st for A1, A2 holds
P[A1, A2, (o
. (A1,A2))] from
BINOP_1:sch 3(
A1);
end;
uniqueness
proof
let o1,o2 be
BinOp of (
Subspaces M);
assume
A4: for A1, A2, W1, W2 st A1
= W1 & A2
= W2 holds (o1
. (A1,A2))
= (W1
/\ W2);
assume
A5: for A1, A2, W1, W2 st A1
= W1 & A2
= W2 holds (o2
. (A1,A2))
= (W1
/\ W2);
now
let x,y be
set;
assume that
A6: x
in (
Subspaces M) and
A7: y
in (
Subspaces M);
reconsider A = x, B = y as
Element of (
Subspaces M) by
A6,
A7;
consider W1 be
strict
Subspace of M such that
A8: W1
= x by
A6,
Def3;
consider W2 be
strict
Subspace of M such that
A9: W2
= y by
A7,
Def3;
(o1
. (A,B))
= (W1
/\ W2) by
A4,
A8,
A9;
hence (o1
. (x,y))
= (o2
. (x,y)) by
A5,
A8,
A9;
end;
hence thesis by
BINOP_1: 1;
end;
end
theorem ::
VECTSP_5:57
Th57:
LattStr (# (
Subspaces M), (
SubJoin M), (
SubMeet M) #) is
Lattice
proof
set S =
LattStr (# (
Subspaces M), (
SubJoin M), (
SubMeet M) #);
A1: for A,B be
Element of S holds (A
"/\" B)
= (B
"/\" A)
proof
let A,B be
Element of S;
consider W1 be
strict
Subspace of M such that
A2: W1
= A by
Def3;
consider W2 be
strict
Subspace of M such that
A3: W2
= B by
Def3;
thus (A
"/\" B)
= ((
SubMeet M)
. (A,B)) by
LATTICES:def 2
.= (W1
/\ W2) by
A2,
A3,
Def8
.= ((
SubMeet M)
. (B,A)) by
A2,
A3,
Def8
.= (B
"/\" A) by
LATTICES:def 2;
end;
A4: for A,B be
Element of S holds ((A
"/\" B)
"\/" B)
= B
proof
let A,B be
Element of S;
consider W1 be
strict
Subspace of M such that
A5: W1
= A by
Def3;
consider W2 be
strict
Subspace of M such that
A6: W2
= B by
Def3;
reconsider AB = (W1
/\ W2) as
Element of S by
Def3;
thus ((A
"/\" B)
"\/" B)
= ((
SubJoin M)
. ((A
"/\" B),B)) by
LATTICES:def 1
.= ((
SubJoin M)
. (((
SubMeet M)
. (A,B)),B)) by
LATTICES:def 2
.= ((
SubJoin M)
. (AB,B)) by
A5,
A6,
Def8
.= ((W1
/\ W2)
+ W2) by
A6,
Def7
.= B by
A6,
Lm10,
VECTSP_4: 29;
end;
A7: for A,B,C be
Element of S holds (A
"/\" (B
"/\" C))
= ((A
"/\" B)
"/\" C)
proof
let A,B,C be
Element of S;
consider W1 be
strict
Subspace of M such that
A8: W1
= A by
Def3;
consider W2 be
strict
Subspace of M such that
A9: W2
= B by
Def3;
consider W3 be
strict
Subspace of M such that
A10: W3
= C by
Def3;
reconsider AB = (W1
/\ W2), BC = (W2
/\ W3) as
Element of S by
Def3;
thus (A
"/\" (B
"/\" C))
= ((
SubMeet M)
. (A,(B
"/\" C))) by
LATTICES:def 2
.= ((
SubMeet M)
. (A,((
SubMeet M)
. (B,C)))) by
LATTICES:def 2
.= ((
SubMeet M)
. (A,BC)) by
A9,
A10,
Def8
.= (W1
/\ (W2
/\ W3)) by
A8,
Def8
.= ((W1
/\ W2)
/\ W3) by
Th14
.= ((
SubMeet M)
. (AB,C)) by
A10,
Def8
.= ((
SubMeet M)
. (((
SubMeet M)
. (A,B)),C)) by
A8,
A9,
Def8
.= ((
SubMeet M)
. ((A
"/\" B),C)) by
LATTICES:def 2
.= ((A
"/\" B)
"/\" C) by
LATTICES:def 2;
end;
A11: for A,B,C be
Element of S holds (A
"\/" (B
"\/" C))
= ((A
"\/" B)
"\/" C)
proof
let A,B,C be
Element of S;
consider W1 be
strict
Subspace of M such that
A12: W1
= A by
Def3;
consider W2 be
strict
Subspace of M such that
A13: W2
= B by
Def3;
consider W3 be
strict
Subspace of M such that
A14: W3
= C by
Def3;
reconsider AB = (W1
+ W2), BC = (W2
+ W3) as
Element of S by
Def3;
thus (A
"\/" (B
"\/" C))
= ((
SubJoin M)
. (A,(B
"\/" C))) by
LATTICES:def 1
.= ((
SubJoin M)
. (A,((
SubJoin M)
. (B,C)))) by
LATTICES:def 1
.= ((
SubJoin M)
. (A,BC)) by
A13,
A14,
Def7
.= (W1
+ (W2
+ W3)) by
A12,
Def7
.= ((W1
+ W2)
+ W3) by
Th6
.= ((
SubJoin M)
. (AB,C)) by
A14,
Def7
.= ((
SubJoin M)
. (((
SubJoin M)
. (A,B)),C)) by
A12,
A13,
Def7
.= ((
SubJoin M)
. ((A
"\/" B),C)) by
LATTICES:def 1
.= ((A
"\/" B)
"\/" C) by
LATTICES:def 1;
end;
A15: for A,B be
Element of S holds (A
"/\" (A
"\/" B))
= A
proof
let A,B be
Element of S;
consider W1 be
strict
Subspace of M such that
A16: W1
= A by
Def3;
consider W2 be
strict
Subspace of M such that
A17: W2
= B by
Def3;
reconsider AB = (W1
+ W2) as
Element of S by
Def3;
thus (A
"/\" (A
"\/" B))
= ((
SubMeet M)
. (A,(A
"\/" B))) by
LATTICES:def 2
.= ((
SubMeet M)
. (A,((
SubJoin M)
. (A,B)))) by
LATTICES:def 1
.= ((
SubMeet M)
. (A,AB)) by
A16,
A17,
Def7
.= (W1
/\ (W1
+ W2)) by
A16,
Def8
.= A by
A16,
Lm11,
VECTSP_4: 29;
end;
for A,B be
Element of S holds (A
"\/" B)
= (B
"\/" A)
proof
let A,B be
Element of S;
consider W1 be
strict
Subspace of M such that
A18: W1
= A by
Def3;
consider W2 be
strict
Subspace of M such that
A19: W2
= B by
Def3;
thus (A
"\/" B)
= ((
SubJoin M)
. (A,B)) by
LATTICES:def 1
.= (W1
+ W2) by
A18,
A19,
Def7
.= (W2
+ W1) by
Lm1
.= ((
SubJoin M)
. (B,A)) by
A18,
A19,
Def7
.= (B
"\/" A) by
LATTICES:def 1;
end;
then S is
join-commutative
join-associative
meet-absorbing
meet-commutative
meet-associative
join-absorbing by
A11,
A4,
A1,
A7,
A15,
LATTICES:def 4,
LATTICES:def 5,
LATTICES:def 6,
LATTICES:def 7,
LATTICES:def 8,
LATTICES:def 9;
hence thesis;
end;
theorem ::
VECTSP_5:58
Th58:
LattStr (# (
Subspaces M), (
SubJoin M), (
SubMeet M) #) is
0_Lattice
proof
set S =
LattStr (# (
Subspaces M), (
SubJoin M), (
SubMeet M) #);
ex C be
Element of S st for A be
Element of S holds (C
"/\" A)
= C & (A
"/\" C)
= C
proof
reconsider C = (
(0). M) as
Element of S by
Def3;
take C;
let A be
Element of S;
consider W be
strict
Subspace of M such that
A1: W
= A by
Def3;
thus (C
"/\" A)
= ((
SubMeet M)
. (C,A)) by
LATTICES:def 2
.= ((
(0). M)
/\ W) by
A1,
Def8
.= C by
Th20;
thus (A
"/\" C)
= ((
SubMeet M)
. (A,C)) by
LATTICES:def 2
.= (W
/\ (
(0). M)) by
A1,
Def8
.= C by
Th20;
end;
hence thesis by
Th57,
LATTICES:def 13;
end;
theorem ::
VECTSP_5:59
Th59:
LattStr (# (
Subspaces M), (
SubJoin M), (
SubMeet M) #) is
1_Lattice
proof
set S =
LattStr (# (
Subspaces M), (
SubJoin M), (
SubMeet M) #);
ex C be
Element of S st for A be
Element of S holds (C
"\/" A)
= C & (A
"\/" C)
= C
proof
consider W9 be
strict
Subspace of M such that
A1: the
carrier of W9
= the
carrier of (
(Omega). M);
reconsider C = W9 as
Element of S by
Def3;
take C;
let A be
Element of S;
consider W be
strict
Subspace of M such that
A2: W
= A by
Def3;
A3: C is
Subspace of (
(Omega). M) by
Lm6;
thus (C
"\/" A)
= ((
SubJoin M)
. (C,A)) by
LATTICES:def 1
.= (W9
+ W) by
A2,
Def7
.= ((
(Omega). M)
+ W) by
A1,
Lm5
.= the ModuleStr of M by
Th11
.= C by
A1,
A3,
VECTSP_4: 31;
thus (A
"\/" C)
= ((
SubJoin M)
. (A,C)) by
LATTICES:def 1
.= (W
+ W9) by
A2,
Def7
.= (W
+ (
(Omega). M)) by
A1,
Lm5
.= the ModuleStr of M by
Th11
.= C by
A1,
A3,
VECTSP_4: 31;
end;
hence thesis by
Th57,
LATTICES:def 14;
end;
theorem ::
VECTSP_5:60
Th60:
LattStr (# (
Subspaces M), (
SubJoin M), (
SubMeet M) #) is
01_Lattice
proof
LattStr (# (
Subspaces M), (
SubJoin M), (
SubMeet M) #) is
lower-bounded
upper-bounded
Lattice by
Th58,
Th59;
hence thesis;
end;
theorem ::
VECTSP_5:61
LattStr (# (
Subspaces M), (
SubJoin M), (
SubMeet M) #) is
M_Lattice
proof
set S =
LattStr (# (
Subspaces M), (
SubJoin M), (
SubMeet M) #);
for A,B,C be
Element of S st A
[= C holds (A
"\/" (B
"/\" C))
= ((A
"\/" B)
"/\" C)
proof
let A,B,C be
Element of S;
assume
A1: A
[= C;
consider W1 be
strict
Subspace of M such that
A2: W1
= A by
Def3;
consider W3 be
strict
Subspace of M such that
A3: W3
= C by
Def3;
(W1
+ W3)
= ((
SubJoin M)
. (A,C)) by
A2,
A3,
Def7
.= (A
"\/" C) by
LATTICES:def 1
.= W3 by
A1,
A3,
LATTICES:def 3;
then
A4: W1 is
Subspace of W3 by
Th8;
consider W2 be
strict
Subspace of M such that
A5: W2
= B by
Def3;
reconsider AB = (W1
+ W2) as
Element of S by
Def3;
reconsider BC = (W2
/\ W3) as
Element of S by
Def3;
thus (A
"\/" (B
"/\" C))
= ((
SubJoin M)
. (A,(B
"/\" C))) by
LATTICES:def 1
.= ((
SubJoin M)
. (A,((
SubMeet M)
. (B,C)))) by
LATTICES:def 2
.= ((
SubJoin M)
. (A,BC)) by
A5,
A3,
Def8
.= (W1
+ (W2
/\ W3)) by
A2,
Def7
.= ((W1
+ W2)
/\ W3) by
A4,
Th30
.= ((
SubMeet M)
. (AB,C)) by
A3,
Def8
.= ((
SubMeet M)
. (((
SubJoin M)
. (A,B)),C)) by
A2,
A5,
Def7
.= ((
SubMeet M)
. ((A
"\/" B),C)) by
LATTICES:def 1
.= ((A
"\/" B)
"/\" C) by
LATTICES:def 2;
end;
hence thesis by
Th57,
LATTICES:def 12;
end;
theorem ::
VECTSP_5:62
for F be
Field, V be
VectSp of F holds
LattStr (# (
Subspaces V), (
SubJoin V), (
SubMeet V) #) is
C_Lattice
proof
let F be
Field, V be
VectSp of F;
reconsider S =
LattStr (# (
Subspaces V), (
SubJoin V), (
SubMeet V) #) as
01_Lattice by
Th60;
reconsider S0 = S as
0_Lattice;
reconsider S1 = S as
1_Lattice;
consider W9 be
strict
Subspace of V such that
A1: the
carrier of W9
= the
carrier of (
(Omega). V);
reconsider I = W9 as
Element of S by
Def3;
reconsider I1 = I as
Element of S1;
reconsider Z = (
(0). V) as
Element of S by
Def3;
reconsider Z0 = Z as
Element of S0;
now
let A be
Element of S0;
consider W be
strict
Subspace of V such that
A2: W
= A by
Def3;
thus (A
"/\" Z0)
= ((
SubMeet V)
. (A,Z0)) by
LATTICES:def 2
.= (W
/\ (
(0). V)) by
A2,
Def8
.= Z0 by
Th20;
end;
then
A3: (
Bottom S)
= Z by
RLSUB_2: 64;
now
let A be
Element of S1;
consider W be
strict
Subspace of V such that
A4: W
= A by
Def3;
A5: W9 is
Subspace of (
(Omega). V) by
Lm6;
thus (A
"\/" I1)
= ((
SubJoin V)
. (A,I1)) by
LATTICES:def 1
.= (W
+ W9) by
A4,
Def7
.= (W
+ (
(Omega). V)) by
A1,
Lm5
.= the ModuleStr of V by
Th11
.= W9 by
A1,
A5,
VECTSP_4: 31;
end;
then
A6: (
Top S)
= I by
RLSUB_2: 65;
now
A7: I is
Subspace of (
(Omega). V) by
Lm6;
let A be
Element of S;
consider W be
strict
Subspace of V such that
A8: W
= A by
Def3;
set L = the
Linear_Compl of W;
consider W99 be
strict
Subspace of V such that
A9: the
carrier of W99
= the
carrier of L by
Lm4;
reconsider B9 = W99 as
Element of S by
Def3;
take B = B9;
A10: (B
"/\" A)
= ((
SubMeet V)
. (B,A)) by
LATTICES:def 2
.= (W99
/\ W) by
A8,
Def8
.= (L
/\ W) by
A9,
Lm8
.= (
Bottom S) by
A3,
Th40;
(B
"\/" A)
= ((
SubJoin V)
. (B,A)) by
LATTICES:def 1
.= (W99
+ W) by
A8,
Def7
.= (L
+ W) by
A9,
Lm5
.= the ModuleStr of V by
Th39
.= (
Top S) by
A1,
A6,
A7,
VECTSP_4: 31;
hence B
is_a_complement_of A by
A10,
LATTICES:def 18;
end;
hence thesis by
LATTICES:def 19;
end;