let K be Field; for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for A being Subset of V1
for B being Subset of V2 st f .: A = B holds
f .: the carrier of (Lin A) = the carrier of (Lin B)
let V1, V2 be VectSp of K; for f being linear-transformation of V1,V2
for A being Subset of V1
for B being Subset of V2 st f .: A = B holds
f .: the carrier of (Lin A) = the carrier of (Lin B)
let f be linear-transformation of V1,V2; for A being Subset of V1
for B being Subset of V2 st f .: A = B holds
f .: the carrier of (Lin A) = the carrier of (Lin B)
A1:
dom f = [#] V1
by FUNCT_2:def 1;
let A be Subset of V1; for B being Subset of V2 st f .: A = B holds
f .: the carrier of (Lin A) = the carrier of (Lin B)
let B be Subset of V2; ( f .: A = B implies f .: the carrier of (Lin A) = the carrier of (Lin B) )
assume A2:
f .: A = B
; f .: the carrier of (Lin A) = the carrier of (Lin B)
thus
f .: the carrier of (Lin A) c= the carrier of (Lin B)
XBOOLE_0:def 10 the carrier of (Lin B) c= f .: the carrier of (Lin A)proof
let y be
object ;
TARSKI:def 3 ( not y in f .: the carrier of (Lin A) or y in the carrier of (Lin B) )
assume
y in f .: the
carrier of
(Lin A)
;
y in the carrier of (Lin B)
then consider x being
object such that
x in dom f
and A3:
x in the
carrier of
(Lin A)
and A4:
f . x = y
by FUNCT_1:def 6;
x in Lin A
by A3;
then consider L being
Linear_Combination of
A such that A5:
x = Sum L
by VECTSP_7:7;
consider F being
FinSequence of
V1 such that
F is
one-to-one
and A6:
rng F = Carrier L
and A7:
x = Sum (L (#) F)
by A5, VECTSP_6:def 6;
set LF =
L (#) F;
consider g being
sequence of the
carrier of
V1 such that A8:
x = g . (len (L (#) F))
and A9:
g . 0 = 0. V1
and A10:
for
j being
Nat for
v being
Vector of
V1 st
j < len (L (#) F) &
v = (L (#) F) . (j + 1) holds
g . (j + 1) = (g . j) + v
by A7, RLVECT_1:def 12;
defpred S1[
Nat]
means ( $1
<= len F implies
f . (g . $1) in Lin B );
A11:
len (L (#) F) = len F
by VECTSP_6:def 5;
then A12:
dom (L (#) F) = dom F
by FINSEQ_3:29;
A13:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A14:
S1[
n]
;
S1[n + 1]
reconsider N =
n as
Element of
NAT by ORDINAL1:def 12;
reconsider gn =
g . N as
Vector of
V1 ;
set N1 =
N + 1;
assume A15:
n + 1
<= len F
;
f . (g . (n + 1)) in Lin B
then A16:
N < len F
by NAT_1:13;
A17:
(
Carrier L c= A &
dom f = [#] V1 )
by FUNCT_2:def 1, VECTSP_6:def 4;
1
<= n + 1
by NAT_1:14;
then A18:
n + 1
in dom F
by A15, FINSEQ_3:25;
then
(
F /. (N + 1) = F . (N + 1) &
F . (N + 1) in Carrier L )
by A6, FUNCT_1:def 3, PARTFUN1:def 6;
then
f . (F /. (N + 1)) in B
by A2, A17, FUNCT_1:def 6;
then A19:
(L . (F /. (N + 1))) * (f . (F /. (N + 1))) in Lin B
by VECTSP_4:21, VECTSP_7:8;
(L (#) F) . (N + 1) = (L . (F /. (N + 1))) * (F /. (N + 1))
by A12, A18, VECTSP_6:def 5;
then
g . (N + 1) = gn + ((L . (F /. (N + 1))) * (F /. (N + 1)))
by A11, A10, A16;
then f . (g . (n + 1)) =
(f . gn) + (f . ((L . (F /. (N + 1))) * (F /. (N + 1))))
by VECTSP_1:def 20
.=
(f . gn) + ((L . (F /. (N + 1))) * (f . (F /. (N + 1))))
by MOD_2:def 2
;
hence
f . (g . (n + 1)) in Lin B
by A14, A15, A19, NAT_1:13, VECTSP_4:20;
verum
end;
f . (0. V1) = 0. V2
by RANKNULL:9;
then A20:
S1[
0 ]
by A9, VECTSP_4:17;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A20, A13);
then
S1[
len F]
;
hence
y in the
carrier of
(Lin B)
by A4, A11, A8, STRUCT_0:def 5;
verum
end;
let x be object ; TARSKI:def 3 ( not x in the carrier of (Lin B) or x in f .: the carrier of (Lin A) )
assume
x in the carrier of (Lin B)
; x in f .: the carrier of (Lin A)
then
x in Lin B
;
then consider L being Linear_Combination of B such that
A21:
x = Sum L
by VECTSP_7:7;
Carrier L c= B
by VECTSP_6:def 4;
then consider M being Linear_Combination of A such that
A22:
f . (Sum M) = Sum L
by A2, Th41;
Sum M in Lin A
by VECTSP_7:7;
then
Sum M in the carrier of (Lin A)
;
hence
x in f .: the carrier of (Lin A)
by A21, A22, A1, FUNCT_1:def 6; verum