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