let n be Nat; for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
ex A being linearly-independent Subset of (TOP-REAL n) st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )
let p be Point of (TOP-REAL n); ( p <> 0. (TOP-REAL n) implies ex A being linearly-independent Subset of (TOP-REAL n) st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) ) )
assume A1:
p <> 0. (TOP-REAL n)
; ex A being linearly-independent Subset of (TOP-REAL n) st
( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
A2: 0. (TOP-REAL n) =
- (0. (TOP-REAL n1))
by JGRAPH_5:10
.=
- (0. (TOP-REAL n))
;
set V1 = Plane (p,(0. (TOP-REAL n)));
|(p,(0. (TOP-REAL n)))| = 0
by EUCLID_2:32;
then
|(p,((0. (TOP-REAL n)) - (0. (TOP-REAL n))))| = 0
by RLVECT_1:5;
then A3:
0. (TOP-REAL n) in Plane (p,(0. (TOP-REAL n)))
;
A4:
for v, u being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) & u in Plane (p,(0. (TOP-REAL n))) holds
v + u in Plane (p,(0. (TOP-REAL n)))
proof
let v,
u be
VECTOR of
(TOP-REAL n);
( v in Plane (p,(0. (TOP-REAL n))) & u in Plane (p,(0. (TOP-REAL n))) implies v + u in Plane (p,(0. (TOP-REAL n))) )
assume
v in Plane (
p,
(0. (TOP-REAL n)))
;
( not u in Plane (p,(0. (TOP-REAL n))) or v + u in Plane (p,(0. (TOP-REAL n))) )
then consider v1 being
Point of
(TOP-REAL n) such that A5:
(
v = v1 &
|(p,(v1 - (0. (TOP-REAL n))))| = 0 )
;
assume
u in Plane (
p,
(0. (TOP-REAL n)))
;
v + u in Plane (p,(0. (TOP-REAL n)))
then consider u1 being
Point of
(TOP-REAL n) such that A6:
(
u = u1 &
|(p,(u1 - (0. (TOP-REAL n))))| = 0 )
;
|(p,((v1 + u1) - (0. (TOP-REAL n))))| =
|(p,(v1 + (u1 - (0. (TOP-REAL n)))))|
by RLVECT_1:def 3
.=
|(p,v1)| + |(p,(u1 - (0. (TOP-REAL n))))|
by EUCLID_2:26
.=
0
by A5, A2, A6, RLVECT_1:4
;
hence
v + u in Plane (
p,
(0. (TOP-REAL n)))
by A5, A6;
verum
end;
for a being Real
for v being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) holds
a * v in Plane (p,(0. (TOP-REAL n)))
proof
let a be
Real;
for v being VECTOR of (TOP-REAL n) st v in Plane (p,(0. (TOP-REAL n))) holds
a * v in Plane (p,(0. (TOP-REAL n)))let v be
VECTOR of
(TOP-REAL n);
( v in Plane (p,(0. (TOP-REAL n))) implies a * v in Plane (p,(0. (TOP-REAL n))) )
assume
v in Plane (
p,
(0. (TOP-REAL n)))
;
a * v in Plane (p,(0. (TOP-REAL n)))
then consider v1 being
Point of
(TOP-REAL n) such that A7:
(
v = v1 &
|(p,(v1 - (0. (TOP-REAL n))))| = 0 )
;
|(p,(a * (v1 - (0. (TOP-REAL n)))))| = a * 0
by A7, EUCLID_2:20;
then
|(p,((a * v1) - (a * (0. (TOP-REAL n)))))| = 0
by RLVECT_1:34;
then
|(p,((a * v1) - (0. (TOP-REAL n))))| = 0
by RLVECT_1:10;
hence
a * v in Plane (
p,
(0. (TOP-REAL n)))
by A7;
verum
end;
then consider W being strict Subspace of TOP-REAL n such that
A8:
Plane (p,(0. (TOP-REAL n))) = the carrier of W
by A3, RLSUB_1:35, A4, RLSUB_1:def 1;
set A1 = the Basis of W;
A10:
[#] (Lin the Basis of W) = Plane (p,(0. (TOP-REAL n)))
by A8, RLVECT_3:def 3;
reconsider A = the Basis of W as linearly-independent Subset of (TOP-REAL n) by RLVECT_3:def 3, RLVECT_5:14;
take
A
; ( card A = n - 1 & [#] (Lin A) = Plane (p,(0. (TOP-REAL n))) )
reconsider A2 = {p} as linearly-independent Subset of (TOP-REAL n) by A1, RLVECT_3:8;
A11: dim (Lin A2) =
card A2
by RLVECT_5:29
.=
1
by CARD_1:30
;
for v being VECTOR of (TOP-REAL n) ex v1, v2 being VECTOR of (TOP-REAL n) st
( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )
proof
let v be
VECTOR of
(TOP-REAL n);
ex v1, v2 being VECTOR of (TOP-REAL n) st
( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )
set a =
|(p,v)| / |(p,p)|;
set v2 =
(|(p,v)| / |(p,p)|) * p;
set v1 =
v - ((|(p,v)| / |(p,p)|) * p);
reconsider v1 =
v - ((|(p,v)| / |(p,p)|) * p),
v2 =
(|(p,v)| / |(p,p)|) * p as
VECTOR of
(TOP-REAL n) ;
take
v1
;
ex v2 being VECTOR of (TOP-REAL n) st
( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )
take
v2
;
( v1 in Lin A & v2 in Lin A2 & v = v1 + v2 )
A12:
|(p,p)| > 0
by A1, EUCLID_2:43;
|(p,v1)| =
|(p,v)| - |(p,v2)|
by EUCLID_2:27
.=
|(p,v)| - ((|(p,v)| / |(p,p)|) * |(p,p)|)
by EUCLID_2:20
.=
|(p,v)| - |(p,v)|
by A12, XCMPLX_1:87
.=
0
;
then
|(p,(v1 - (0. (TOP-REAL n))))| = 0
by A2, RLVECT_1:4;
then
v1 in Lin the
Basis of
W
by A10;
hence
v1 in Lin A
by RLVECT_5:20;
( v2 in Lin A2 & v = v1 + v2 )
thus
v2 in Lin A2
by RLVECT_4:8;
v = v1 + v2
thus
v = v1 + v2
by RLVECT_4:1;
verum
end;
then A13:
RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the U5 of (TOP-REAL n), the Mult of (TOP-REAL n) #) = (Lin A) + (Lin A2)
by RLSUB_2:44;
(Lin A) /\ (Lin A2) = (0). (TOP-REAL n)
proof
for
v being
VECTOR of
(TOP-REAL n) holds
(
v in (Lin A) /\ (Lin A2) iff
v in (0). (TOP-REAL n) )
proof
let v be
VECTOR of
(TOP-REAL n);
( v in (Lin A) /\ (Lin A2) iff v in (0). (TOP-REAL n) )
hereby ( v in (0). (TOP-REAL n) implies v in (Lin A) /\ (Lin A2) )
assume
v in (Lin A) /\ (Lin A2)
;
v in (0). (TOP-REAL n)then A14:
(
v in Lin A &
v in Lin A2 )
by RLSUB_2:3;
then consider a being
Real such that A15:
v = a * p
by RLVECT_4:8;
v in Plane (
p,
(0. (TOP-REAL n)))
by A10, A14, RLVECT_5:20;
then consider y being
Point of
(TOP-REAL n) such that A16:
(
y = v &
|(p,(y - (0. (TOP-REAL n))))| = 0 )
;
|(p,v)| = 0
by A2, A16, RLVECT_1:4;
then A17:
a * |(p,p)| = 0
by A15, EUCLID_2:20;
|(p,p)| > 0
by A1, EUCLID_2:43;
then
a = 0
by A17;
then
v = 0. (TOP-REAL n)
by A15, RLVECT_1:10;
hence
v in (0). (TOP-REAL n)
by RLVECT_3:29;
verum
end;
assume
v in (0). (TOP-REAL n)
;
v in (Lin A) /\ (Lin A2)
then
v = 0. (TOP-REAL n)
by RLVECT_3:29;
hence
v in (Lin A) /\ (Lin A2)
by RLSUB_1:17;
verum
end;
hence
(Lin A) /\ (Lin A2) = (0). (TOP-REAL n)
by RLSUB_1:31;
verum
end;
then
dim (TOP-REAL n) = (dim (Lin A)) + (dim (Lin A2))
by RLVECT_5:37, A13, RLSUB_2:def 4;
then
n = (dim (Lin A)) + 1
by A11, RLAFFIN3:4;
hence
card A = n - 1
by RLVECT_5:29; [#] (Lin A) = Plane (p,(0. (TOP-REAL n)))
thus
[#] (Lin A) = Plane (p,(0. (TOP-REAL n)))
by A10, RLVECT_5:20; verum