let V be VectSp of F_Complex ; for M being Subspace of V holds RealVS M is Subspace of RealVS V
let M be Subspace of V; RealVS M is Subspace of RealVS V
A1:
the carrier of M c= the carrier of V
by VECTSP_4:def 2;
A2:
the lmult of M = the lmult of V | [: the carrier of F_Complex, the carrier of M:]
by VECTSP_4:def 2;
A3:
addLoopStr(# the carrier of M, the addF of M, the ZeroF of M #) = addLoopStr(# the carrier of (RealVS M), the addF of (RealVS M), the ZeroF of (RealVS M) #)
by Def17;
A4:
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #)
by Def17;
hence A5:
the carrier of (RealVS M) c= the carrier of (RealVS V)
by A3, VECTSP_4:def 2; RLSUB_1:def 2 ( 0. (RealVS M) = 0. (RealVS V) & the addF of (RealVS M) = the addF of (RealVS V) || the carrier of (RealVS M) & the Mult of (RealVS M) = K5( the Mult of (RealVS V),[:REAL, the carrier of (RealVS M):]) )
then
[:REAL, the carrier of (RealVS M):] c= [:REAL, the carrier of (RealVS V):]
by ZFMISC_1:95;
then
[:REAL, the carrier of (RealVS M):] c= dom the Mult of (RealVS V)
by FUNCT_2:def 1;
then A6:
dom ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]) = [:REAL, the carrier of (RealVS M):]
by RELAT_1:62;
rng ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]) c= the carrier of (RealVS M)
proof
let y be
object ;
TARSKI:def 3 ( not y in rng ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]) or y in the carrier of (RealVS M) )
assume
y in rng ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):])
;
y in the carrier of (RealVS M)
then consider x being
object such that A7:
x in dom ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):])
and A8:
y = ( the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]) . x
by FUNCT_1:def 3;
consider a,
b being
object such that A9:
x = [a,b]
by A7, RELAT_1:def 1;
reconsider a =
a as
Element of
REAL by A7, A9, ZFMISC_1:87;
reconsider b =
b as
Element of
(RealVS M) by A6, A7, A9, ZFMISC_1:87;
reconsider b1 =
b as
Element of
M by A3;
reconsider b2 =
b1 as
Element of
V by A1;
[[**a,0**],b2] in [: the carrier of F_Complex, the carrier of V:]
by ZFMISC_1:87;
then
(
[[**a,0**],b1] in [: the carrier of F_Complex, the carrier of M:] &
[[**a,0**],b2] in dom the
lmult of
V )
by FUNCT_2:def 1, ZFMISC_1:87;
then
[[**a,0**],b2] in (dom the lmult of V) /\ [: the carrier of F_Complex, the carrier of M:]
by XBOOLE_0:def 4;
then A10:
[[**a,0**],b2] in dom ( the lmult of V | [: the carrier of F_Complex, the carrier of M:])
by RELAT_1:61;
y =
the
Mult of
(RealVS V) . (
a,
b)
by A7, A8, A9, FUNCT_1:47
.=
[**a,0**] * b2
by Def17
.=
[**a,0**] * b1
by A2, A10, FUNCT_1:47
.=
the
Mult of
(RealVS M) . (
a,
b)
by Def17
;
hence
y in the
carrier of
(RealVS M)
;
verum
end;
then reconsider RM = the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):] as Function of [:REAL, the carrier of (RealVS M):], the carrier of (RealVS M) by A6, FUNCT_2:2;
thus 0. (RealVS M) =
0. M
by A3
.=
0. V
by VECTSP_4:def 2
.=
0. (RealVS V)
by A4
; ( the addF of (RealVS M) = the addF of (RealVS V) || the carrier of (RealVS M) & the Mult of (RealVS M) = K5( the Mult of (RealVS V),[:REAL, the carrier of (RealVS M):]) )
thus
the addF of (RealVS M) = the addF of (RealVS V) || the carrier of (RealVS M)
by A3, A4, VECTSP_4:def 2; the Mult of (RealVS M) = K5( the Mult of (RealVS V),[:REAL, the carrier of (RealVS M):])
now for a being Element of REAL
for b being Element of (RealVS M) holds the Mult of (RealVS M) . (a,b) = RM . (a,b)let a be
Element of
REAL ;
for b being Element of (RealVS M) holds the Mult of (RealVS M) . (a,b) = RM . (a,b)let b be
Element of
(RealVS M);
the Mult of (RealVS M) . (a,b) = RM . (a,b)reconsider b1 =
b as
Element of
M by A3;
reconsider b2 =
b1 as
Element of
V by A1;
[[**a,0**],b2] in [: the carrier of F_Complex, the carrier of V:]
by ZFMISC_1:87;
then
(
[[**a,0**],b1] in [: the carrier of F_Complex, the carrier of M:] &
[[**a,0**],b2] in dom the
lmult of
V )
by FUNCT_2:def 1, ZFMISC_1:87;
then
[[**a,0**],b2] in (dom the lmult of V) /\ [: the carrier of F_Complex, the carrier of M:]
by XBOOLE_0:def 4;
then A11:
[[**a,0**],b2] in dom ( the lmult of V | [: the carrier of F_Complex, the carrier of M:])
by RELAT_1:61;
(
a in REAL &
b in the
carrier of
(RealVS V) )
by A5;
then
[a,b] in [:REAL, the carrier of (RealVS V):]
by ZFMISC_1:87;
then
(
[a,b] in [:REAL, the carrier of (RealVS M):] &
[a,b] in dom the
Mult of
(RealVS V) )
by FUNCT_2:def 1, ZFMISC_1:87;
then
[a,b] in (dom the Mult of (RealVS V)) /\ [:REAL, the carrier of (RealVS M):]
by XBOOLE_0:def 4;
then A12:
[a,b] in dom RM
by RELAT_1:61;
thus the
Mult of
(RealVS M) . (
a,
b) =
[**a,0**] * b1
by Def17
.=
[**a,0**] * b2
by A2, A11, FUNCT_1:47
.=
the
Mult of
(RealVS V) . (
a,
b)
by Def17
.=
RM . (
a,
b)
by A12, FUNCT_1:47
;
verum end;
hence
the Mult of (RealVS M) = the Mult of (RealVS V) | [:REAL, the carrier of (RealVS M):]
by BINOP_1:2; verum