:: Isomorphism Theorem on Vector Spaces over a Ring
:: by Yuichi Futa and Yasunari Shidama
::
:: Received August 30, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies VECTSP_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
FUNCSDOM, FINSET_1, CARD_1, CARD_3, ARYTM_3, ARYTM_1, MOD_3, FINSEQ_1,
VALUED_1, SUPINF_2, MSSUBFAM, STRUCT_0, RLSUB_1, RLSUB_2, RLVECT_2,
SETWISEO, ORDINAL4, RLVECT_3, UNIALG_1, RANKNULL, UPROOTS, VECTSP10,
ZMODUL05, QC_LANG1, RLVECT_5, ALGSTR_0, VECTSP12, GROUP_2, PRVECT_1,
PRVECT_2, BINOP_1, NUMBERS, RLVECT_1, ZFMISC_1, NAT_1, FUNCT_6, FINSEQOP,
MESFUNC1, PRVECT_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
FUNCT_2, BINOP_1, FINSET_1, CARD_1, ORDINAL1, CARD_3, XCMPLX_0, NUMBERS,
FINSEQ_1, FINSEQOP, STRUCT_0, SETWISEO, ALGSTR_0, RLVECT_1, VECTSP_1,
MOD_2, RLVECT_2, VECTSP_4, VECTSP_5, VECTSP_6, MATRLIN, VECTSP_7,
VECTSP_9, VECTSP10, PRVECT_1, PRVECT_2, PRVECT_3, RANKNULL, ZMODUL05,
ZMODUL07;
constructors RELSET_1, REALSET1, FINSEQOP, RLVECT_2, VECTSP_9, WELLORD2,
SETWISEO, PRVECT_2, ZMODUL05, ZMODUL07, PRVECT_3;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, FINSET_1,
RLVECT_1, CARD_3, FINSEQ_1, PRVECT_1, PRVECT_2, XREAL_0, STRUCT_0,
MATRLIN, RANKNULL, VECTSP_9, VECTSP_1, FUNCT_2, ALGSTR_0, PRVECT_3;
requirements BOOLE, SUBSET, NUMERALS;
definitions TARSKI, RLVECT_1, ALGSTR_0, VECTSP_1;
equalities FINSEQ_1, STRUCT_0, ALGSTR_0, VECTSP_4, VECTSP_6, RELAT_1,
VECTSP10, ZMODUL05, BINOP_1, VECTSP_1, PRVECT_3;
expansions TARSKI, XBOOLE_0, STRUCT_0, VECTSP_1, MOD_2, VECTSP_7, FUNCT_2,
MATRLIN, RLVECT_1, BINOP_1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2,
CARD_1, FINSEQ_1, VECTSP_1, VECTSP10, RLVECT_1, RLVECT_2, RANKNULL,
VECTSP_5, MATRLIN, VECTSP_7, VECTSP_9, VECTSP_4, FVSUM_1, FINSEQOP,
VECTSP_6, MOD_2, BINOP_1, FINSEQ_3, SETWISEO, ZMODUL04, ZMODUL05,
ZMODUL06, PRVECT_1, PRVECT_2, CARD_3, ALGSTR_0, PRVECT_3, SUBSET_1,
XTUPLE_0, NDIFF_5;
schemes FUNCT_2, PRVECT_1, BINOP_1;
begin :: 1. Bijective linear transformation
reserve K,F for Ring;
reserve V,W for VectSp of K;
reserve l for Linear_Combination of V;
reserve T for linear-transformation of V,W;
theorem
for K being Field,
V,W being finite-dimensional VectSp of K,
A being Subset of V,
B being Basis of V,
T being linear-transformation of V, W,
l being Linear_Combination of B \ A
st A is Basis of ker T & A c= B holds T.(Sum l) = Sum(T@*l)
proof
let K be Field,
V,W be finite-dimensional VectSp of K,
A be Subset of V, B be Basis of V,
T be linear-transformation of V,W,
l be Linear_Combination of B \ A;
assume A is Basis of ker T & A c= B; then
A1: T | (B \ A) is one-to-one by RANKNULL:22;
A2: (T | (B \ A)) | (Carrier l) = T | (Carrier l)
by RELAT_1:74,VECTSP_6:def 4; then
A3: T | (Carrier l) is one-to-one by A1,FUNCT_1:52;
consider G be FinSequence of V such that
A4: G is one-to-one and
A5: rng G = Carrier l and
A6: Sum l = Sum (l (#) G) by VECTSP_6:def 6;
set H = T*G;
A7: rng H = T .: (Carrier l) by A5,RELAT_1:127
.= Carrier(T@*l) by A3,ZMODUL05:56;
dom T = [#]V by RANKNULL:7;
then H is one-to-one by A1,A2,A4,A5,FUNCT_1:52,RANKNULL:1; then
A8: Sum (T@*l) = Sum ((T@*l) (#) H) by A7,VECTSP_6:def 6;
T*(l (#) G) = (T@*l) (#) H by A3,A5,ZMODUL05:55;
hence thesis by A6,A8,MATRLIN:16;
end;
HM11:
for F being Field, X, Y being VectSp of F,
T being linear-transformation of X, Y,
A being Subset of X st T is bijective holds
A is Basis of X implies T.: A is Basis of Y
proof
let F be Field, X, Y be VectSp of F,
T be linear-transformation of X, Y,
A be Subset of X;
assume AS1: T is bijective;
assume A is Basis of X; then
P1: A is linearly-independent &
Lin (A) = the ModuleStr of X by VECTSP_7:def 3;
D1: dom T = the carrier of X by FUNCT_2:def 1;
R1: rng T = the carrier of Y by FUNCT_2:def 3,AS1;
P2: T.:A is linearly-independent by ZMODUL06:45,AS1,P1;
P6: Lin(T.: A) is strict Subspace of (Omega).Y by ZMODUL06:47;
the carrier of Lin(T.: A) = T.: (the carrier of (the ModuleStr of X))
by P1,AS1,ZMODUL06:46
.= the carrier of (Omega).Y by D1,R1,RELAT_1:113;
hence thesis by P2,VECTSP_7:def 3,P6,VECTSP_4:31;
end;
theorem HM12:
for F being Field, X, Y being VectSp of F,
T being linear-transformation of X, Y,
A being Subset of X st T is bijective holds
A is Basis of X iff T.: A is Basis of Y
proof
let F be Field, X, Y be VectSp of F,
L be linear-transformation of X, Y,
A be Subset of X;
assume AS1: L is bijective;
D1: dom L = the carrier of X by FUNCT_2:def 1;
consider K be linear-transformation of Y, X such that
AS3: K= L" & K is bijective by ZMODUL06:42,AS1;
thus A is Basis of X implies L.:A is Basis of Y by AS1,HM11;
assume L.:A is Basis of Y;
then K.: (L.:A) is Basis of X by AS3,HM11;
hence thesis by D1,AS1,AS3,FUNCT_1:107;
end;
HM13:
for F being Field, X, Y being VectSp of F,
T being linear-transformation of X, Y
st T is bijective holds
X is finite-dimensional implies Y is finite-dimensional
proof
let F be Field, X, Y be VectSp of F,
L be linear-transformation of X, Y;
assume AS1: L is bijective;
assume X is finite-dimensional;
then consider A be finite Subset of X such that
P1: A is Basis of X;
L.: A is Basis of Y by P1,HM12,AS1;
hence thesis;
end;
theorem HM151:
for F being Field, X, Y being VectSp of F,
T being linear-transformation of X, Y
st T is bijective holds
X is finite-dimensional iff Y is finite-dimensional
proof
let F be Field, X, Y be VectSp of F,
T be linear-transformation of X, Y;
assume AS1: T is bijective;
consider K be linear-transformation of Y, X such that
AS3: K= T" & K is bijective by ZMODUL06:42,AS1;
thus thesis by HM13,AS1,AS3;
end;
theorem HM15:
for F being Field, X being finite-dimensional VectSp of F,
Y being VectSp of F,
T being linear-transformation of X, Y
st T is bijective holds
Y is finite-dimensional & dim(X) = dim(Y)
proof
let F be Field, X be finite-dimensional VectSp of F,
Y be VectSp of F, T be linear-transformation of X, Y;
assume AS1: T is bijective;
hence
X1: Y is finite-dimensional by HM151;
for I being Basis of X holds dim(Y) = card I
proof
let I be Basis of X;
dom T = the carrier of X by FUNCT_2:def 1; then
X12: card I = card (T.:I) by CARD_1:5,AS1,CARD_1:33;
T.: I is Basis of Y by AS1,HM12;
hence dim(Y) = card I by X1,X12,VECTSP_9:def 1;
end;
hence thesis by VECTSP_9:def 1;
end;
theorem
for F being Field, X, Y being VectSp of F,
l being Linear_Combination of X,
T being linear-transformation of X, Y
st T is one-to-one holds
T @ l = T @* l
proof
let F be Field, X, Y be VectSp of F,
l be Linear_Combination of X,
T be linear-transformation of X, Y;
assume AS: T is one-to-one;
A1:Carrier (T @ l) c= T.:(Carrier l) by RANKNULL:30;
for y being Element of Y holds (T @ l).y = Sum(lCFST(l,T,y))
proof
let y be Element of Y;
rng lCFST(l,T,y) c= the carrier of F;
then reconsider Z = lCFST(l,T,y) as FinSequence of F by FINSEQ_1:def 4;
C0: (T @ l).y = Sum (l .: (T"{y})) by RANKNULL:def 5;
per cases;
suppose C1: T"{y} = {};
then lCFST(l,T,y) = <*> the carrier of F; then
C2: Sum(lCFST(l,T,y)) = 0.F by RLVECT_1:43;
l .: (T"{y}) = {}F by C1;
hence (T @ l).y = Sum(lCFST(l,T,y)) by C0,C2,RLVECT_2:8;
end;
suppose T"{y} <> {};
then consider x be object such that
X1: x in T"{y} by XBOOLE_0:def 1;
X2: x in dom T & T.x in {y} by X1,FUNCT_1:def 7;
reconsider x as Element of X by X1;
C2: T.x = y by X2,TARSKI:def 1;
y in rng T by X2,C2,FUNCT_1:def 3;
then C3: ex x0 being object st T " {y} = {x0} by AS,FUNCT_1:74;
then C31: T " {y} = {x} by X1,TARSKI:def 1;
C81: dom l = the carrier of X by FUNCT_2:def 1;
C9: l .: (T"{y}) = Im(l,x) by C3,X1,TARSKI:def 1
.= {l.x} by C81,FUNCT_1:59;
per cases;
suppose C61: x in Carrier l; then
C6: (T"{y}) /\ (Carrier l) ={x} by C31,XBOOLE_1:28,ZFMISC_1:31;
dom l = the carrier of X by FUNCT_2:def 1;
then rng canFS((T"{y}) /\ (Carrier l)) c= dom l by XBOOLE_1:1; then
C81: dom Z = dom canFS((T"{y}) /\ (Carrier l)) by RELAT_1:27
.= dom canFS({x}) by C31,C61,XBOOLE_1:28,ZFMISC_1:31
.= dom <*x*> by FINSEQ_1:94
.= Seg 1 by FINSEQ_1:38; then
C82: len Z = 1 by FINSEQ_1:def 3;
1 in dom Z by C81;
then Z.1 = l.( (canFS({x})).1) by C6,FUNCT_1:12
.= l.((<*x*>).1) by FINSEQ_1:94
.= l.x; then
C83: Z = <* l.x *> by FINSEQ_1:40,C82;
then C8: Z = canFS{l.x} by FINSEQ_1:94;
rng Z = l.:(T"{y}) by C9,C83,FINSEQ_1:38;
hence (T @ l).y = Sum(lCFST(l,T,y)) by C0,C8,RLVECT_2:def 2;
end;
suppose C5: not x in Carrier l;
(T"{y}) /\ (Carrier l) = {}
proof
assume (T"{y}) /\ (Carrier l) <> {};
then consider x0 be object such that
C60: x0 in (T"{y}) /\ (Carrier l) by XBOOLE_0:def 1;
x0 in (T"{y}) & x0 in Carrier l by C60,XBOOLE_0:def 4;
hence contradiction by C5,C31,TARSKI:def 1;
end;
then Z = <*> the carrier of F; then
C8: Sum(lCFST(l,T,y)) = 0.F by RLVECT_1:43;
l .: (T"{y}) = { 0.F } by C5,C9;
hence (T @ l).y = Sum(lCFST(l,T,y)) by C0,C8,RLVECT_2:9;
end;
end;
end;
hence thesis by A1,ZMODUL05:def 8;
end;
begin :: 2. Properties of linear combinations on modules over a ring
theorem FRds1:
for K being Field,V being VectSp of K, W1, W2 being Subspace of V,
I1 being Basis of W1, I2 being Basis of W2 st V is_the_direct_sum_of W1,W2
holds I1 /\ I2 = {}
proof
let K be Field;
let V be VectSp of K, W1, W2 be Subspace of V,
I1 be Basis of W1, I2 be Basis of W2 such that
A1: V is_the_direct_sum_of W1,W2;
assume I1 /\ I2 <> {};
then consider v be object such that
A2: v in I1 /\ I2 by XBOOLE_0:7;
A3: v in I1 by A2,XBOOLE_0:def 4;
not 0.W1 in I1 by VECTSP_7:2,VECTSP_7:def 3; then
A4: v <> 0.V by A3,VECTSP_4:11;
A5: v in W1 by A3;
v in W2 by A2; then v in W1 /\ W2 by A5,VECTSP_5:3;
then v in (0).V by A1,VECTSP_5:def 4;
hence contradiction by A4,VECTSP_4:35;
end;
theorem FRds2:
for K being Field,V being VectSp of K, W1, W2 being Subspace of V,
I1 being Basis of W1, I2 being Basis of W2, I being Subset of V
st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2
holds Lin(I) = the ModuleStr of V
proof
let K be Field,V being VectSp of K, W1, W2 be Subspace of V,
I1 be Basis of W1, I2 being Basis of W2, I be Subset of V such that
A1: V is_the_direct_sum_of W1,W2 and
A2: I = I1 \/ I2;
the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
then reconsider II1 = I1 as Subset of V by XBOOLE_1:1;
the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then reconsider II2 = I2 as Subset of V by XBOOLE_1:1;
A5: the ModuleStr of W1 = Lin(I1) by VECTSP_7:def 3
.= Lin(II1) by VECTSP_9:17;
A6: the ModuleStr of W2 = Lin(I2) by VECTSP_7:def 3
.= Lin(II2) by VECTSP_9:17;
for x being Vector of V holds x in W1+W2 iff x in Lin(II1) + Lin(II2)
proof
let x be Vector of V;
hereby
assume x in W1+W2;
then consider x1, x2 be Vector of V such that
B1: x1 in W1 & x2 in W2 & x = x1 + x2 by VECTSP_5:1;
B2: x1 in Lin(II1) by A5,B1;
x2 in Lin(II2) by A6,B1;
hence x in Lin(II1) + Lin(II2) by B1,B2,VECTSP_5:1;
end;
assume x in Lin(II1) + Lin(II2);
then consider x1, x2 be Vector of V such that
B1: x1 in Lin(II1) & x2 in Lin(II2) & x = x1 + x2 by VECTSP_5:1;
B2: x1 in W1 by A5,B1;
x2 in W2 by A6,B1;
hence x in W1 + W2 by B1,B2,VECTSP_5:1;
end; then
A7: W1 + W2 = Lin(II1) + Lin(II2) by VECTSP_4:30;
thus the ModuleStr of V = W1 + W2 by A1,VECTSP_5:def 4
.= Lin(I) by A2,A7,VECTSP_7:15;
end;
theorem FRds3:
for K being Field,V being VectSp of K, W1, W2 being Subspace of V,
I1 being Basis of W1, I2 being Basis of W2, I being Subset of V
st V is_the_direct_sum_of W1,W2 & I = I1 \/ I2
holds I is linearly-independent
proof
let K be Field, V be VectSp of K, W1, W2 be Subspace of V,
I1 be Basis of W1, I2 be Basis of W2, I be Subset of V such that
A1: V is_the_direct_sum_of W1,W2 and
A2: I = I1 \/ I2;
assume I is linearly-dependent;
then consider l be Linear_Combination of I such that
A3: Sum(l) = 0.V and
A4: Carrier(l) <> {};
A5A: I1 /\ I2 = {} by A1,FRds1;
A5B: I1 misses I2 by A1,FRds1;
the carrier of W1 c= the carrier of V
& the carrier of W2 c= the carrier of V by VECTSP_4:def 2;
then reconsider II1 = I1, II2 = I2 as Subset of V by XBOOLE_1:1;
consider l1 be Linear_Combination of II1,
l2 be Linear_Combination of II2 such that
A6: l = l1 + l2 by A2,A5A,ZMODUL04:26;
reconsider ll1 = l1 as Linear_Combination of I
by A2,XBOOLE_1:7,VECTSP_6:4;
reconsider ll2 = l2 as Linear_Combination of I
by A2,XBOOLE_1:7,VECTSP_6:4;
A7: Sum(l) = Sum(ll1) + Sum(ll2) by A6,VECTSP_6:44;
set v1 = Sum(ll1);
set v2 = Sum(ll2);
Carrier(ll1) c= I1 & Carrier(ll2) c= I2 by VECTSP_6:def 4;
then A8: Carrier(ll1) /\ Carrier(ll2) = {}
by A5B,XBOOLE_0:def 7,XBOOLE_1:64;
A10: v1 <> 0.V
proof
assume B1: v1 = 0.V;
II1 is linearly-independent by VECTSP_7:def 3,VECTSP_9:11;
then B3: Carrier(l1) = {} by B1;
II2 is linearly-independent by VECTSP_7:def 3,VECTSP_9:11;
then Carrier(ll1) \/ Carrier(ll2) = {} by A3,A7,B1,B3;
hence contradiction by A4,A6,A8,ZMODUL04:25;
end;
A13: v1 = -v2 by A3,A7,RLVECT_1:6;
v1 in Lin(II1) by VECTSP_7:7;
then v1 in Lin(I1) by VECTSP_9:17;
then v1 in the ModuleStr of W1 by VECTSP_7:def 3;
then A14: v1 in W1;
v2 in Lin(II2) by VECTSP_7:7;
then v2 in Lin(I2) by VECTSP_9:17;
then v2 in the ModuleStr of W2 by VECTSP_7:def 3;
then v2 in W2;
then A15: v1 in W2 by A13,VECTSP_4:22;
W1 /\ W2 = (0).V by A1,VECTSP_5:def 4;
hence contradiction by A10,A14,A15,VECTSP_5:3,VECTSP_4:35;
end;
theorem
for K being Field,V being VectSp of K,
W1, W2 being Subspace of V,
I1 being Basis of W1,I2 being Basis of W2
st W1 /\ W2 = (0).V holds
I1 \/ I2 is Basis of W1+W2
proof
let K be Field, V be VectSp of K,
W1, W2 be Subspace of V,
I1 be Basis of W1,I2 be Basis of W2 such that
P1: W1 /\ W2 = (0).V;
set I = I1 \/ I2;
reconsider W = W1 + W2 as strict Subspace of V;
reconsider WW1 = W1, WW2 = W2 as Subspace of W by VECTSP_5:7;
the carrier of WW1 c= the carrier of W &
the carrier of WW2 c= the carrier of W by VECTSP_4:def 2;
then I1 c= the carrier of W & I2 c= the carrier of W;
then reconsider I0 = I as Subset of W by XBOOLE_1:8;
reconsider I10 = I1 as Basis of WW1;
reconsider I20 = I2 as Basis of WW2;
A2: WW1 /\ WW2 is Subspace of V by VECTSP_4:26;
A3: WW1 + WW2 is Subspace of V by VECTSP_4:26;
for x being object holds x in WW1 /\ WW2 iff x in (0).V
proof
let x be object;
hereby
assume x in WW1 /\ WW2;
then x in WW1 & x in WW2 by VECTSP_5:3;
hence x in (0).V by P1,VECTSP_5:3;
end;
assume x in (0).V;
then x in W1 & x in W2 by P1,VECTSP_5:3;
hence x in WW1 /\ WW2 by VECTSP_5:3;
end;
then for x being Vector of V holds x in WW1 /\ WW2 iff x in (0).V;
then A4: WW1 /\ WW2 = (0).V by A2,VECTSP_4:30
.= (0).W by VECTSP_4:36;
for x being object holds x in W iff x in WW1 + WW2
proof
let x be object;
hereby
assume x in W;
then consider x1, x2 be Vector of V such that
B2: x1 in W1 & x2 in W2 & x = x1 + x2 by VECTSP_5:1;
x1 in W1 + W2 by B2,VECTSP_5:2;
then reconsider xx1 = x1 as Vector of W;
x2 in W1 + W2 by B2,VECTSP_5:2;
then reconsider xx2 = x2 as Vector of W;
x = xx1 + xx2 by B2,VECTSP_4:13;
hence x in WW1 + WW2 by B2,VECTSP_5:1;
end;
assume x in WW1 + WW2;
then consider x1, x2 be Vector of W such that
B2: x1 in WW1 & x2 in WW2 & x = x1 + x2 by VECTSP_5:1;
thus x in W by B2;
end;
then for x being Vector of V holds x in W iff x in WW1 + WW2;
then W = WW1 + WW2 by A3,VECTSP_4:30;
then I0 is base by A4,FRds2,FRds3,VECTSP_5:def 4;
hence thesis;
end;
begin :: 3. 1st isomorphism theorem
theorem Th38A:
for K being Field
for V being finite-dimensional VectSp of K,
W being Subspace of V holds
ex S being Linear_Compl of W,
T being linear-transformation of S, VectQuot(V,W)
st T is bijective &
for v being Vector of V st v in S holds T.v = v+ W
proof
let K be Field;
let V be finite-dimensional VectSp of K,
W be Subspace of V;
set S = the Linear_Compl of W;
set aC = addCoset(V,W);
set C = CosetSet(V,W);
set Vq = VectQuot(V,W);
defpred P[Vector of V,Vector of Vq] means $2 = $1 + W;
A2:
now
let v be Vector of V;
reconsider y=v+W as Vector of Vq by VECTSP10:23;
take y;
thus P[v, y];
end;
consider ff be Function of the carrier of V, the carrier of Vq such that
A7: for v being Vector of V holds P[v, ff.v] from FUNCT_2:sch 3(A2);
set T = ff| the carrier of S;
S1: the carrier of S c= the carrier of V by VECTSP_4:def 2;
then reconsider T as Function of the carrier of S,the carrier of Vq
by FUNCT_2:32;
P1: for v being Vector of V st v in S holds T.v = v+ W
proof
let v be Vector of V;
assume v in S;
hence T.v = ff.v by FUNCT_1:49
.= v+W by A7;
end;
now
let a, b be Vector of S;
reconsider a1 = a, b1 = b as Vector of V by S1;
A91: a1 in S & b1 in S;
a1+b1 = a+b by VECTSP_4:13; then
A94: a1+b1 in S;
A95: T.a = a1+W by P1,A91;
A96: T.b = b1+W by P1,A91;
thus T.(a+b) = T.(a1+b1) by VECTSP_4:13
.= (a1+b1) + W by A94,P1
.= T.a + T.b by A95,A96,VECTSP10:26;
end; then
AD: T is additive;
now
let a be Vector of S;
let r be Element of K;
reconsider a1 = a as Vector of V by S1;
A91: a1 in S;
r*a = r*a1 by VECTSP_4:14; then
A94: r*a1 in S;
A95: T.a = a1+W by P1,A91;
thus T.(r*a) = T.(r*a1) by VECTSP_4:14
.= (r*a1) + W by A94,P1
.= r*T.a by A95,VECTSP10:25;
end;
then T is homogeneous;
then reconsider T as linear-transformation of S,Vq by AD;
A100: V is_the_direct_sum_of S,W by VECTSP_5:def 5;
the carrier of Vq c= rng T
proof
let y be object;
assume y in the carrier of Vq;
then consider a be Vector of V such that
A10: y = a+W by VECTSP10:22;
the ModuleStr of V = S+W by A100,VECTSP_5:def 4;
then a in S+W;
then consider s, w be Element of V such that
A12: s in S & w in W & a = s + w by VECTSP_5:1;
reconsider s0 = s as Vector of S by A12;
reconsider B = s+W as Vector of Vq by VECTSP10:23;
reconsider A = a+W, Z = w+W as Vector of Vq by VECTSP10:23;
Z = zeroCoset (V,W) by A12,VECTSP_4:49
.= 0.Vq by VECTSP10:def 6; then
A13: B = B+Z
.= A by A12,VECTSP10:26;
T.s0 = y by A10,A12,A13,P1;
hence y in rng T by FUNCT_2:4;
end;
then rng T = the carrier of Vq; then
A14: T is onto;
X1: for x1,x2 being object st x1 in the carrier of S
& x2 in the carrier of S & T.x1 = T.x2 holds x1 = x2
proof
let x1,x2 be object;
assume A15: x1 in the carrier of S
& x2 in the carrier of S & T.x1 = T.x2;
then reconsider a1=x1,a2=x2 as Vector of V by S1;
A16: a1 in S & a2 in S by A15;
A17: T.x1 = a1+W by P1,A16;
T.x2 = a2+W by P1,A16;
then consider w be Element of V such that
A19: w in W & a2 = a1 + w by A15,A17,VECTSP_4:42,VECTSP_4:55;
A20: a2-a1 = w +(a1 -a1) by A19,RLVECT_1:28
.= w + 0.V by VECTSP_1:19
.= w;
a2-a1 in S by A16,VECTSP_4:23;
then a2-a1 in S /\ W by A19,A20,VECTSP_5:3;
then a2-a1 in (0).V by A100,VECTSP_5:def 4;
then a2-a1 = 0.V by VECTSP_4:35;
hence x1 = x2 by RLVECT_1:21;
end;
take S, T;
thus thesis by A14,P1,X1,FUNCT_2:19;
end;
theorem
for K being Field
for V being finite-dimensional VectSp of K, W being Subspace of V holds
VectQuot(V,W) is finite-dimensional &
dim VectQuot(V,W) + dim W = dim V
proof
let K be Field;
let V be finite-dimensional VectSp of K,
W be Subspace of V;
set Vq = VectQuot(V,W);
consider S be Linear_Compl of W,
T be linear-transformation of S, Vq such that
X1: T is bijective and
for v being Vector of V st v in S holds T.v = v+ W by Th38A;
Vq is finite-dimensional & dim(S) = dim(Vq) by HM15,X1;
hence thesis by VECTSP_5:def 5,VECTSP_9:34;
end;
definition
let K be Ring;
let V,U be VectSp of K;
let W be Subspace of V;
let f be linear-transformation of V,U;
assume
A1: the carrier of W c= the carrier of ker f;
func QFunctional(f,W) -> linear-transformation of VectQuot(V,W),U means
:Def12:
for A being Vector of VectQuot(V,W), a being Vector of V st A = a+W
holds it.A = f.a;
existence
proof
defpred P[set,set] means for a being Vector of V st $1 = a+W
holds $2 = f.a;
set aC = addCoset(V,W);
set C = CosetSet(V,W);
set vq = VectQuot(V,W);
A2:
now
let A be Vector of vq;
consider a be Vector of V such that
A3: A = a+W by VECTSP10:22;
take y = f.a;
thus P[A, y]
proof
let a1 be Vector of V;
assume A = a1+W;
then consider w be Vector of V such that
A4: w in W and
A5: a = a1 + w by A3,VECTSP_4:42,VECTSP_4:44;
w in ker f by A1,A4; then
A6: f.w = 0.U by RANKNULL:10;
thus y = f.a1+f.w by A5,VECTSP_1:def 20
.= f.a1 by A6;
end;
end;
consider ff be Function of the carrier of vq, the carrier of U such that
A7: for A being Vector of vq holds P[A, ff.A] from FUNCT_2:sch 3(A2);
reconsider ff as Function of vq, U;
A8: C = the carrier of vq by VECTSP10:def 6;
now
A9: the addF of vq = addCoset(V,W) by VECTSP10:def 6;
let A, B be Vector of vq;
consider a be Vector of V such that
A10: A = a+W by VECTSP10:22;
consider b be Vector of V such that
A11: B = b+W by VECTSP10:22;
aC.(A,B) =a+b+W by A8,A10,A11,VECTSP10:def 3;
hence ff.(A+B) = f.(a+b) by A7,A9
.= f.a + f.b by VECTSP_1:def 20
.= ff.A + f.b by A7,A10
.= ff.A + ff.B by A7,A11;
end; then
AD: ff is additive;
now
let A be Vector of vq;
let r be Element of K;
A2: C = the carrier of vq by VECTSP10:def 6;
then A in C;
then consider aa be Coset of W such that
A3: A = aa;
consider a be Vector of V such that
A4: aa = a+W by VECTSP_4:def 6;
r*A = (lmultCoset(V,W)).(r,A) by VECTSP10:def 6
.= r*a+ W by A2,A3,A4,VECTSP10:def 5;
hence ff.(r*A) = f.(r*a) by A7
.= r*f.a by MOD_2:def 2
.= r*(ff.A) by A3,A4,A7;
end;
then ff is homogeneous;
then reconsider ff as linear-transformation of vq, U by AD;
take ff;
thus thesis by A7;
end;
uniqueness
proof
set vq = VectQuot(V,W);
let f1,f2 be linear-transformation of vq,U such that
A12: for A being Vector of VectQuot(V,W), a being Vector of V st A = a+W
holds f1.A = f.a and
A13: for A being Vector of VectQuot(V,W), a being Vector of V st A = a+W
holds f2.A = f.a;
now
let A be Vector of vq;
consider a be Vector of V such that
A14: A = a+W by VECTSP10:22;
thus f1.A = f.a by A12,A14
.= f2.A by A13,A14;
end;
hence thesis;
end;
end;
definition
let K be Ring;
let V,U be VectSp of K;
let f be linear-transformation of V,U;
func CQFunctional(f) -> linear-transformation of VectQuot(V,ker f),U
equals
QFunctional(f,ker f);
coherence;
end;
registration let K be Ring;
let V,U be VectSp of K, f be linear-transformation of V,U;
cluster CQFunctional(f) -> one-to-one;
coherence
proof
set T = CQFunctional(f);
set Vq = VectQuot(V,ker f);
for x1,x2 being object st x1 in the carrier of Vq &
x2 in the carrier of Vq & T.x1 = T.x2 holds x1 = x2
proof
let xx1, xx2 be object;
assume AS:xx1 in the carrier of Vq & xx2 in the carrier of Vq &
T.xx1 = T.xx2;
then reconsider x1 = xx1, x2 = xx2 as Vector of Vq;
consider a1 be Vector of V such that
A14: x1 = a1+(ker f) by VECTSP10:22;
consider a2 be Vector of V such that
A15: x2 = a2+(ker f) by VECTSP10:22;
f.a1= T.x1 by A14,Def12
.= f.a2 by AS,A15,Def12; then
A16: a1-a2 in ker f by RANKNULL:17;
a1 = a1 - 0.V
.= a1-(a2-a2) by VECTSP_1:19
.= a2+ (a1-a2) by RLVECT_1:29;
then a1 in x1 & a1 in x2 by A14,A15,A16,VECTSP_4:44;
hence xx1 = xx2 by VECTSP_4:56,A14,A15;
end;
hence thesis by FUNCT_2:19;
end;
end;
:: 1st isomorphism theorem
theorem
for K being Ring,
V, U being VectSp of K, f being linear-transformation of V,U holds
ex T being linear-transformation of VectQuot(V,ker f), im f
st T = CQFunctional(f) & T is bijective
proof
let K be Ring,
V, U be VectSp of K, f be linear-transformation of V,U;
set T = CQFunctional(f);
set Vq = VectQuot(V,ker f);
Q0: the carrier of im f = [#] im f
.= f.: [#]V by RANKNULL:def 2
.= f.: (dom f) by FUNCT_2:def 1
.= rng f by RELAT_1:113;
Q1: for x being object holds x in rng T iff x in rng f
proof
let x be object;
hereby
assume x in rng T;
then consider z be object such that
Q12: z in dom T & x = T.z by FUNCT_1:def 3;
reconsider z as Vector of Vq by Q12;
consider a be Vector of V such that
A14: z = a+(ker f) by VECTSP10:22;
T.z = f.a by A14,Def12;
hence x in rng f by Q12,FUNCT_2:4;
end;
assume x in rng f;
then consider a be object such that
Q12: a in dom f & x = f.a by FUNCT_1:def 3;
reconsider a as Vector of V by Q12;
reconsider z = a+ ker f as Vector of Vq by VECTSP10:23;
T.z = f.a by Def12;
hence x in rng T by Q12,FUNCT_2:4;
end; then
P1: rng T = the carrier of im f by Q0,TARSKI:2;
the carrier of (VectQuot(V,ker f)) = dom T by FUNCT_2:def 1;
then reconsider T as Function of
the carrier of (VectQuot(V,ker f)),the carrier of im f by FUNCT_2:2,P1;
A1: T is onto by Q0,Q1,TARSKI:2;
set Tq = CQFunctional(f);
now
let A, B be Vector of Vq;
thus T.(A+B) = (Tq.A) +(Tq.B) by VECTSP_1:def 20
.=T.A + T.B by VECTSP_4:13;
end; then
AD: T is additive;
now
let A be Vector of Vq;
let r be Element of K;
thus T.(r*A) = r*Tq.A by MOD_2:def 2
.= r*(T.A) by VECTSP_4:14;
end;
then T is homogeneous;
then reconsider T as linear-transformation of Vq, im f by AD;
take T;
thus thesis by A1;
end;
definition
let K be Ring, V, U, W be VectSp of K,
f be linear-transformation of V, U,
g be linear-transformation of U, W;
redefine func g*f -> linear-transformation of V, W; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
correctness
proof
g*f is linear-transformation of V, W;
hence thesis;
end;
end;
begin :: 4. The product space of vector spaces
definition
let K be Ring;
mode VectorSpace-Sequence of K -> non empty FinSequence means :Def3:
for S be set st S in rng it holds S is VectSp of K;
existence
proof
set S = the VectSp of K;
take <*S*>;
let x be set;
assume that
A1: x in rng <*S*> and
A2: not x is VectSp of K;
x in {S} by A1,FINSEQ_1:38;
hence contradiction by A2,TARSKI:def 1;
end;
end;
registration let K be Ring;
cluster -> AbGroup-yielding for VectorSpace-Sequence of K;
coherence
proof
let F be VectorSpace-Sequence of K;
for x being set st x in rng F holds x is AbGroup by Def3;
hence thesis by PRVECT_1:def 10;
end;
end;
definition
let K be Ring;
let G be VectorSpace-Sequence of K;
let j be Element of dom G;
redefine func G.j -> VectSp of K; :: redefines . (FUNCT_1, definition)
coherence
proof
G.j in rng G by FUNCT_1:def 3;
hence thesis by Def3;
end;
end;
definition
let K be Ring,
G be VectorSpace-Sequence of K,
j be Element of dom carr G;
redefine func G.j -> VectSp of K; :: redefines . (FUNCT_1, definition)
coherence
proof
dom G = Seg len G & Seg len(carr G) = dom carr G by FINSEQ_1:def 3;
then reconsider j9 = j as Element of dom G by PRVECT_1:def 11;
G.j9 is VectSp of K;
hence thesis;
end;
end;
definition
let K be Ring,
G be VectorSpace-Sequence of K;
func multop G -> MultOps of the carrier of K,carr G means :Def8:
len it = len carr G &
for j being Element of dom carr G holds it.j = the lmult of G.j;
existence
proof
deffunc F(Element of dom carr G) = the lmult of G.$1;
consider p be non empty FinSequence such that
A20: len p = len carr G
& for j being Element of dom carr G holds p.j = F(j) from PRVECT_1:sch 1;
now
let ai be set;
assume ai in dom carr G;
then reconsider i=ai as Element of dom carr G;
len G = len(carr G) by PRVECT_1:def 11;
then reconsider j = i as Element of dom G by FINSEQ_3:29;
p.i = the lmult of G.i & the carrier of G.j = (carr G).j
by A20,PRVECT_1:def 11;
hence p.ai is Function of
[:the carrier of K,(carr G).ai:],(carr G).ai;
end;
then reconsider p9 = p as MultOps of the carrier of K,
carr G by A20,PRVECT_2:4;
take p9;
thus thesis by A20;
end;
uniqueness
proof
let f,h be MultOps of the carrier of K, carr G;
assume that
A21: len f = len carr G and
A22: for j being Element of dom carr G holds f.j = the lmult of G.j and
A23: len h = len carr G and
A24: for j being Element of dom carr G holds h.j = the lmult of G.j;
reconsider f9 = f,h9 = h as FinSequence;
A25:
now
let i be Nat;
assume i in dom f9;
then reconsider i9 = i as Element of dom carr G by A21,FINSEQ_3:29;
f9.i = the lmult of G.i9 by A22;
hence f9.i = h9.i by A24;
end;
dom f9 = Seg len f9 & dom h9 = Seg len h9 by FINSEQ_1:def 3;
hence thesis by A21,A23,A25,FINSEQ_1:13;
end;
end;
definition
let K be Ring,
G be VectorSpace-Sequence of K;
func product G -> strict non empty ModuleStr over K equals
ModuleStr (# product carr G, [: addop G :], zeros G, [: multop G :] #);
coherence;
end;
Lm3: for K being Ring, G being VectorSpace-Sequence of K
holds for v1,w1 being Element of product
carr G, i be Element of dom carr G holds ([:addop G:].(v1,w1)).i =
(the addF of G.i).(v1.i,w1.i) &
for vi, wi being Vector of G.i st vi = v1.i & wi=w1.i holds
([:addop G:].(v1,w1)).i = vi+wi
proof
let K be Ring,
G be VectorSpace-Sequence of K;
let v1,w1 be Element of product carr G;
let i be Element of dom carr G;
([:addop G:].(v1,w1)).i = ((addop G).i).(v1.i,w1.i) by PRVECT_1:def 8;
hence thesis by PRVECT_1:def 12;
end;
Lm4: for K being Ring, G being VectorSpace-Sequence of K, r being Element of K,
v being Element of product carr G, i being Element of dom carr G holds
([:multop G:].(r,v)).i = (the lmult of G.i).(r,v.i) &
for vi being Vector of G.i st vi = v.i holds ([:multop G:].(r,v)).i = r*vi
proof
let K be Ring,
G be VectorSpace-Sequence of K;
let r be Element of K,v be Element of product carr G;
let i be Element of dom carr G;
([:multop G:].(r,v)).i = ((multop G).i).(r,v.i) by PRVECT_2: def 2;
hence thesis by Def8;
end;
Lm5: for K being Ring, G being VectorSpace-Sequence of K
holds product G is vector-distributive
scalar-distributive scalar-associative scalar-unital
proof
let K be Ring,
G be VectorSpace-Sequence of K;
deffunc ad(addLoopStr) = the addF of $1;
reconsider GS = ModuleStr(# product carr G,[:addop G:],zeros G,[:multop G:]
#) as non empty ModuleStr over K;
dom G = Seg len G by FINSEQ_1:def 3;
then dom G = Seg len carr G by PRVECT_1:def 11;
then
A1: dom G = dom carr G by FINSEQ_1:def 3;
now
let a,b be Element of K;
let v,w be Vector of GS;
reconsider v1=v, w1=w as Element of product carr G;
A2:
now
let x be object;
assume x in dom carr G;
then reconsider i = x as Element of dom carr G;
reconsider vi=v1.i as Vector of G.i by A1,PRVECT_1:def 11;
( [:multop G:].(1.K,v1)).x = 1.K *vi by Lm4;
hence ([:multop G:].(1.K,v1)).x = v1.x;
end;
A3:
now
let x be object;
assume x in dom carr G;
then reconsider i = x as Element of dom carr G;
reconsider vi=v1.i as Vector of G.i by A1,PRVECT_1:def 11;
([:multop G:].(a+b,v1)).i = (a+b)*vi by Lm4
.= a*vi+b*vi by VECTSP_1:def 15
.= ad(G.i).(([:multop G:].(a,v1)).i,b*vi) by Lm4
.= ad(G.i).(([:multop G:].(a,v1)).i,([:multop G:].(b,v1)).i) by Lm4;
hence ([:multop G:].((a+b),v1)).x =([:addop G:].([:multop G:].(a,v1),[:
multop G:].(b,v1))).x by Lm3;
end;
A4:
now
let x be object;
assume x in dom carr G;
then reconsider i = x as Element of dom carr G;
reconsider vi=v1.i, wi=w1.i as Vector of G.i by A1,PRVECT_1:def 11;
([:multop G:].(a,[:addop G:].(v1,w1))).i
= (the lmult of G.i).(a,([:addop G:].(v1,w1)).i) by Lm4
.= a*(vi+wi) by Lm3
.= a*vi+a*wi by VECTSP_1:def 14
.= ad(G.i).(([:multop G:].(a,v1)).i,a*wi) by Lm4
.= ad(G.i).(([:multop G:].(a,v1)).i,([:multop G:].(a,w1)).i) by Lm4;
hence ([:multop G:].(a,[:addop G:].(v1,w1))).x =
([:addop G:].([:multop G:].(a,v1),[:multop G:].(a,w1))).x by Lm3;
end;
dom([:multop G:].(a,[:addop G:].(v1,w1))) = dom carr G &
dom([:addop G:].([: multop G:].(a,v1),[:multop G:].(a,w1))) = dom carr G
by CARD_3:9;
hence a * (v + w) = a * v + a * w by A4,FUNCT_1:2;
A5:
now
let x be object;
assume x in dom carr G;
then reconsider i = x as Element of dom carr G;
reconsider vi=v1.i as Vector of G.i by A1,PRVECT_1:def 11;
([:multop G:].(a*b,v1)).i = (a*b)*vi by Lm4
.= a*(b*vi) by VECTSP_1:def 16
.= (the lmult of G.i).(a,([:multop G:].(b,v1)).i) by Lm4;
hence
([:multop G:].((a*b),v1)).x = ([:multop G:].(a,[:multop G:].(b,v1))).x
by Lm4;
end;
dom([:multop G:].(a+b,v1)) = dom carr G &
dom([:addop G:].([:multop G:].(a, v1),[:multop G:].(b,v1))) = dom carr G
by CARD_3:9;
hence (a + b) * v = a * v + b * v by A3,FUNCT_1:2;
dom([:multop G:].(a*b,v1)) = dom carr G &
dom([:multop G:].(a,[:multop G:].( b,v1))) = dom carr G by CARD_3:9;
hence a * b * v = a * (b * v) by A5,FUNCT_1:2;
dom([:multop G:].(1.K,v1)) = dom carr G
& dom v1 = dom carr G by CARD_3:9;
hence 1.K * v = v by A2,FUNCT_1:2;
end;
hence thesis;
end;
registration
let K be Ring,
G be VectorSpace-Sequence of K;
cluster product G -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence
proof
deffunc zr(addLoopStr) = the ZeroF of $1;
reconsider GS =
ModuleStr(# product carr G,[:addop G:],zeros G,[:multop G:] #)
as non empty ModuleStr over K;
deffunc car(1-sorted) = the carrier of $1;
deffunc ad(addLoopStr) = the addF of $1;
A1:
now
let i be Element of dom carr G;
dom G = Seg len G by FINSEQ_1:def 3
.= Seg len carr G by PRVECT_1:def 11
.= dom carr G by FINSEQ_1:def 3;
hence (carr G).i = car(G.i) by PRVECT_1:def 11;
end;
now
let i be Element of dom carr G;
(addop G).i = ad(G.i) & (carr G).i = car(G.i) by A1,PRVECT_1:def 12;
hence (addop G).i is associative by FVSUM_1:2;
end;
then
A2: [:addop G:] is associative by PRVECT_1:18;
now
let i be Element of dom carr G;
A3: (zeros G).i = 0.(G.i) by PRVECT_1:def 14;
(addop G).i = ad(G.i) & (carr G).i = car(G.i) by A1,PRVECT_1:def 12;
hence (zeros G).i is_a_unity_wrt (addop G).i by A3,PRVECT_1:1;
end;
then
A4: zeros G is_a_unity_wrt [:addop G:] by PRVECT_1:19;
A5: GS is right_complementable
proof
let x be Element of GS;
reconsider y = (Frege complop G).x as Element of GS by FUNCT_2:5;
take y;
now
let i be Element of dom carr G;
A6: 0.(G.i) = zr(G.i);
A7: (complop G).i = comp G.i by PRVECT_1:def 13;
(carr G).i = car(G.i) & (addop G).i = ad(G.i) by A1,PRVECT_1:def 12;
hence (complop G).i is_an_inverseOp_wrt (addop G).i & (addop G).i is
having_a_unity by A6,A7,PRVECT_1:1,PRVECT_1:2,SETWISEO:def 2;
end;
then Frege complop G is_an_inverseOp_wrt [:addop G:] by PRVECT_1:20;
then [:addop G:].(x,y) = the_unity_wrt [:addop G:]
by FINSEQOP:def 1;
hence thesis by A4,BINOP_1:def 8;
end;
now
let i be Element of dom carr G;
(addop G).i = ad(G.i) & (carr G).i = car(G.i) by A1,PRVECT_1:def 12;
hence (addop G).i is commutative by FVSUM_1:1;
end;
then [:addop G:] is commutative by PRVECT_1:17;
hence thesis by A2,A4,A5,Lm5,BINOP_1:3;
end;
end;
begin :: 5. Cartesian product of vector spaces
reserve K for Ring;
definition
let K be Ring,
G,F be non empty ModuleStr over K;
func prod_MLT(G,F) -> Function of
[:the carrier of K ,
[:the carrier of G,the carrier of F:] :],
[:the carrier of G,the carrier of F:] means :YDef2:
for r being Element of K, g be Vector of G, f being Vector of F
holds it.(r,[g,f]) = [r*g,r*f];
existence
proof
defpred MLT[object,object,object] means
ex r being Element of the carrier of K, g be Vector of G, f be Vector of F
st r = $1 & $2=[g,f] & $3= [r*g,r*f];
set CarrG = the carrier of G;
set CarrF = the carrier of F;
A1:for x, y being object st x in the carrier of K & y in [:CarrG,CarrF:]
ex z being object st z in [:CarrG,CarrF:] & MLT[x,y,z]
proof
let x, y be object;
assume A2: x in the carrier of K & y in [:CarrG,CarrF:]; then
reconsider r=x as Element of the carrier of K;
consider y1 be Vector of G, y2 be Vector of F such that
A3: y = [y1,y2] by A2,SUBSET_1:43;
set z = [r*y1,r*y2];
z in [:CarrG,CarrF:] & MLT[x,y,z] by A3;
hence thesis;
end;
consider MLTGF be Function of [:the carrier of K,
[:CarrG,CarrF:] :],[:CarrG,CarrF:] such that
A4: for x, y being object st x in the carrier of K & y in [:CarrG,CarrF:]
holds MLT[x,y,MLTGF.(x,y)] from BINOP_1:sch 1(A1);
now
let r be Element of K, g be Vector of G, f be Vector of F;
MLT[r,[g,f],MLTGF.(r,[g,f])] by A4; then
consider rr be Element of the carrier of K, gg be Vector of G,
ff be Vector of F such that
A5: rr = r & [g,f]=[gg,ff] & MLTGF.(r,[g,f]) = [rr*gg,r*ff];
g = gg & f = ff by A5,XTUPLE_0:1;
hence MLTGF.(r,[g,f]) = [r*g,r*f] by A5;
end;
hence thesis;
end;
uniqueness
proof
let H1,H2 be Function of
[:the carrier of K, [:the carrier of G,the carrier of F:] :],
[:the carrier of G,the carrier of F:];
assume
A6: for r being Element of K, g being Vector of G, f be Vector of F
holds H1.(r,[g,f]) = [r*g,r*f];
assume
A7: for r being Element of K, g being Vector of G, f be Vector of F
holds H2.(r,[g,f]) = [r*g,r*f];
now
let r be Element of the carrier of K, x be Element of
[:the carrier of G,the carrier of F:];
[:the carrier of G,the carrier of F:] <> {} by ZFMISC_1:90;
then consider x1 be Element of G, x2 be Element of F such that
A8: x = [x1,x2] by SUBSET_1:43;
thus H1.(r,x) = [r*x1,r*x2] by A6,A8
.= H2.(r,x) by A7,A8;
end;
hence H1 = H2;
end;
end;
definition
let K be Ring;
let G,F be non empty ModuleStr over K;
func [:G,F:] -> strict non empty ModuleStr over K equals
ModuleStr (# [:the carrier of G,the carrier of F:],
prod_ADD(G,F), prod_ZERO(G,F), prod_MLT(G,F) #);
correctness
proof
[:the carrier of G,the carrier of F:] <> {} by ZFMISC_1:90;
hence thesis;
end;
end;
registration
let K be Ring;
let G,F be Abelian non empty ModuleStr over K;
cluster [:G,F:] -> Abelian;
correctness
proof
let x, y be Element of [:G,F:];
consider x1 be Vector of G, x2 be Vector of F such that
A1: x = [x1,x2] by SUBSET_1:43;
consider y1 be Vector of G, y2 be Vector of F such that
A2: y = [y1,y2] by SUBSET_1:43;
x+y = [x1+y1,x2+y2] by A1,A2,PRVECT_3:def 1;
hence x+y = y+x by A1,A2,PRVECT_3:def 1;
end;
end;
registration
let K be Ring;
let G,F be add-associative non empty ModuleStr over K;
cluster [:G,F:] -> add-associative;
correctness
proof
let x, y, z be Element of [:G,F:];
consider x1 be Vector of G, x2 be Vector of F such that
A1: x = [x1,x2] by SUBSET_1:43;
consider y1 be Vector of G, y2 be Vector of F such that
A2: y = [y1,y2] by SUBSET_1:43;
consider z1 be Vector of G, z2 be Vector of F such that
A3: z = [z1,z2] by SUBSET_1:43;
A4:(x1+y1)+z1 = x1+(y1+z1) & (x2+y2)+z2 = x2+(y2+z2) by RLVECT_1:def 3;
thus (x+y)+z = prod_ADD(G,F).([x1+y1,x2+y2],[z1,z2])
by A1,A2,A3,PRVECT_3:def 1
.= [x1+(y1+z1),x2+(y2+z2)] by A4,PRVECT_3:def 1
.= prod_ADD(G,F).([x1,x2],[(y1+z1),(y2+z2)] ) by PRVECT_3:def 1
.= x+(y+z) by A1,A2,A3,PRVECT_3:def 1;
end;
end;
registration
let K be Ring;
let G, F be right_zeroed non empty ModuleStr over K;
cluster [:G,F:] -> right_zeroed;
correctness
proof
let x be Element of [:G,F:];
consider x1 be Vector of G, x2 be Vector of F such that
A1: x = [x1,x2] by SUBSET_1:43;
x1+0.G = x1 & x2+0.F = x2 by RLVECT_1:def 4;
hence x+0.[:G,F:] = x by A1,PRVECT_3:def 1;
end;
end;
registration
let K be Ring;
let G,F be right_complementable non empty ModuleStr over K;
cluster [:G,F:] -> right_complementable;
correctness
proof
let x be Element of [:G,F:];
consider x1 be Vector of G, x2 be Vector of F such that
A1: x = [x1,x2] by SUBSET_1:43;
consider y1 be Vector of G such that
A2: x1+y1 = 0.G by ALGSTR_0:def 11;
consider y2 be Vector of F such that
A3: x2+y2 = 0.F by ALGSTR_0:def 11;
reconsider y=[y1,y2] as Element of [:G,F:];
take y;
thus thesis by A1,A2,A3,PRVECT_3:def 1;
end;
end;
theorem
for G, F being non empty ModuleStr over K holds
( for x being set holds (x is Vector of [:G,F:]
iff ex x1 being Vector of G, x2 being Vector of F st x=[x1,x2]) )
& ( for x, y being Vector of [:G,F:],
x1, y1 being Vector of G, x2, y2 being Vector of F
st x = [x1,x2] & y = [y1,y2] holds x+y = [x1+y1,x2+y2] )
& 0.[:G,F:] = [0.G,0.F]
& ( for x being Vector of [:G,F:], x1 being Vector of G, x2 be Vector of F,
a being Element of K
st x = [x1,x2] holds a*x = [a*x1,a*x2] )
by YDef2,PRVECT_3:def 1,SUBSET_1:43;
theorem
for G,F being add-associative right_zeroed
right_complementable non empty ModuleStr over K,
x being Vector of [:G,F:], x1 being Vector of G, x2 be Vector of F
st x = [x1,x2] holds -x = [-x1,-x2]
proof
let G,F be add-associative right_zeroed right_complementable
non empty ModuleStr over K;
let x be Vector of [:G,F:], x1 be Vector of G, x2 be Vector of F;
assume A1: x=[x1,x2];
reconsider y = [-x1,-x2 ] as Vector of [:G,F:];
x+y = [x1+-x1,x2+-x2] by A1,PRVECT_3:def 1
.= [0.G,x2+-x2] by RLVECT_1:def 10
.= 0.[:G,F:] by RLVECT_1:def 10;
hence thesis by RLVECT_1:def 10;
end;
registration
let K be Ring;
let G, F be vector-distributive non empty ModuleStr over K;
cluster [:G,F:] -> vector-distributive;
correctness
proof
let a be Element of K, x,y be Vector of [:G,F:];
consider x1 be Vector of G, x2 be Vector of F such that
A1: x = [x1,x2] by SUBSET_1:43;
consider y1 be Vector of G, y2 be Vector of F such that
A2: y = [y1,y2] by SUBSET_1:43;
A3: a*(x1+y1) = a*x1 + a*y1 & a*(x2+y2) = a*x2 + a*y2
by VECTSP_1:def 14;
thus a*(x+y) = prod_MLT(G,F).(a,[x1+y1,x2+y2]) by A1,A2,PRVECT_3:def 1
.= [a*(x1+y1),a*(x2+y2)] by YDef2
.= prod_ADD(G,F).([a*x1,a*x2],[a*y1,a*y2]) by A3,PRVECT_3:def 1
.= prod_ADD(G,F).(prod_MLT(G,F).(a,[x1,x2]),[a*y1,a*y2]) by YDef2
.= a*x + a*y by A1,A2,YDef2;
end;
end;
registration
let K be Ring;
let G, F be scalar-distributive non empty ModuleStr over K;
cluster [:G,F:] -> scalar-distributive;
correctness
proof
let a, b be Element of K, x be Vector of [:G,F:];
consider x1 be Vector of G, x2 be Vector of F such that
A1: x = [x1,x2] by SUBSET_1:43;
A2: (a+b)*x1 = a*x1 + b*x1 & (a+b)*x2 = a*x2 + b*x2
by VECTSP_1:def 15;
thus (a+b)*x = [(a+b)*x1,(a+b)*x2] by A1,YDef2
.= prod_ADD(G,F).([a*x1,a*x2],[b*x1,b*x2]) by A2,PRVECT_3:def 1
.= prod_ADD(G,F).(prod_MLT(G,F).(a,[x1,x2]),[b*x1,b*x2]) by YDef2
.= a*x + b*x by A1,YDef2;
end;
end;
registration
let K be Ring;
let G,F be scalar-associative non empty ModuleStr over K;
cluster [:G,F:] -> scalar-associative;
correctness
proof
let a,b be Element of K, x be Vector of [:G,F:];
consider x1 be Vector of G, x2 be Vector of F such that
A1: x = [x1,x2] by SUBSET_1:43;
A2: (a*b)*x1 = a * (b*x1) & (a*b)*x2 = a * (b*x2) by VECTSP_1:def 16;
thus (a*b)*x = [(a*b)*x1,(a*b)*x2] by A1,YDef2
.= prod_MLT(G,F).(a,[b*x1,b*x2]) by A2,YDef2
.= a*(b*x) by A1,YDef2;
end;
end;
registration
let K be Ring;
let G, F be scalar-unital non empty ModuleStr over K;
cluster [:G,F:] -> scalar-unital;
correctness
proof
let x be Vector of [:G,F:];
consider x1 be Vector of G, x2 be Vector of F such that
A1: x = [x1,x2] by SUBSET_1:43;
1.K * x1 = x1 & 1.K * x2 = x2 by VECTSP_1:def 17;
hence 1.K * x = x by A1,YDef2;
end;
end;
definition
let K be Ring;
let G be VectSp of K;
redefine func <* G *> -> VectorSpace-Sequence of K; :: redefines <* (FINSEQ_1, definition)
correctness
proof
let S be set;
assume S in rng <*G*>; then
consider i be object such that
A1: i in dom <*G*> & <*G*>.i = S by FUNCT_1:def 3;
reconsider i as Element of NAT by A1;
dom <*G*> = {1} by FINSEQ_1:2,def 8; then
i = 1 by A1,TARSKI:def 1;
hence S is VectSp of K by A1;
end;
end;
definition
let K be Ring;
let G, F be VectSp of K;
redefine func <* G,F *> -> VectorSpace-Sequence of K; :: redefines <* (FINSEQ_1, definition)
correctness
proof
let S be set;
assume S in rng <*G,F*>; then
consider i be object such that
A1: i in dom <*G,F*> & <*G,F*>.i = S by FUNCT_1:def 3;
dom <*G,F*> = {1,2} by FINSEQ_1:2,89; then
i = 1 or i = 2 by A1,TARSKI:def 2;
hence S is VectSp of K by A1;
end;
end;
theorem
for X being VectSp of K holds
ex I being Function of X, product <*X*>
st I is one-to-one onto
& ( for x being Vector of X holds I.x = <*x*> )
& ( for v, w being Vector of X holds I.(v+w) = I.v + I.w )
& ( for v being Vector of X, r being Element of the carrier of K
holds I.(r*v) = r*(I.v) )
& I.(0.X) = 0.product <*X*>
proof
let X be VectSp of K;
set CarrX = the carrier of X;
consider I be Function of CarrX,product <*CarrX*> such that
A1: I is one-to-one onto
& for x being object st x in CarrX holds I.x = <*x*> by PRVECT_3:4;
len carr <*X*> = len <*X*> by PRVECT_1:def 11; then
A2:len carr <*X*> = 1 by FINSEQ_1:40;
A3:dom <*X*> = {1} by FINSEQ_1:2,def 8;
A4:<*X*>.1 = X;
1 in {1} by TARSKI:def 1; then
(carr <*X*>).1= the carrier of X by A3,A4,PRVECT_1:def 11; then
A5:carr <*X*> = <* CarrX *> by A2,FINSEQ_1:40; then
reconsider I as Function of X,product <*X*>;
A6: for x being Vector of X holds I.x = <*x*> by A1;
A7: for v, w being Vector of X holds I.(v+w) = I.v + I.w
proof
let v, w be Vector of X;
A8: I.v = <*v*> & I.w = <*w*> & I.(v+w) = <*v+w*> by A1;
reconsider Iv = I.v, Iw = I.w as Element of product carr <*X*>;
1 in {1} by TARSKI:def 1; then
reconsider j1=1 as Element of dom carr <*X*> by A2,FINSEQ_1:2,def 3;
A10: (addop <*X*>).j1 = the addF of (<*X*>.j1) by PRVECT_1:def 12;
A11: ([:addop <*X*>:].(Iv,Iw)).j1
= ((addop <*X*>).j1).(Iv.j1,Iw.j1) by PRVECT_1:def 8
.= v+w by A10,A8;
consider Ivw be Function such that
A12: I.v + I.w = Ivw & dom Ivw = dom carr <*X*>
& for i being object st i in dom carr <*X*> holds Ivw.i in carr (<*X*>).i
by CARD_3:def 5;
A13: dom Ivw = Seg 1 by A2,A12,FINSEQ_1:def 3; then
reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 1 by A13,FINSEQ_1:def 3;
hence thesis by A8,A12,A11,FINSEQ_1:40;
end;
A14: for v being Vector of X,
r being Element of the carrier of K holds I.(r*v)=r*(I.v)
proof
let v be Vector of X, r be Element of the carrier of K;
A15: I.v = <*v*> & I.(r*v) = <* r*v *> by A1;
1 in {1} by TARSKI:def 1; then
reconsider j1=1 as Element of dom carr <*X*> by A2,FINSEQ_1:2,def 3;
A17: (multop <*X*>).j1 = the lmult of (<*X*>.j1) by Def8;
reconsider Iv = I.v as Element of product carr <*X*>;
A18: ([:multop <*X*>:].(r,Iv)).j1
= ((multop <*X*>).j1).(r,Iv.j1) by PRVECT_2:def 2
.= r*v by A17,A15;
consider Ivw be Function such that
A19: r*(I.v) = Ivw & dom Ivw = dom carr <*X*>
& for i being object st i in dom carr <*X*> holds Ivw.i in carr (<*X*>).i
by CARD_3:def 5;
A20: dom Ivw = Seg 1 by A2,A19,FINSEQ_1:def 3; then
reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 1 by A20,FINSEQ_1:def 3;
hence thesis by A15,A19,A18,FINSEQ_1:40;
end;
I.(0.X) = I.(0.X + 0.X)
.= I.(0.X) + I.(0.X) by A7; then
I.(0.X) - I.(0.X) = I.(0.X) + (I.(0.X) - I.(0.X)) by RLVECT_1:28
.= I.(0.X) + 0.product <*X*> by RLVECT_1:15
.= I.(0.X);
hence thesis by A1,A6,A5,A7,A14,RLVECT_1:15;
end;
definition
let K be Ring;
let G, F be VectorSpace-Sequence of K;
redefine func G^F -> VectorSpace-Sequence of K; :: redefines ^ (FINSEQ_1, definition)
correctness
proof
let S be set;
assume S in rng (G^F); then
consider i be object such that
A1: i in dom (G^F) & (G^F).i = S by FUNCT_1:def 3;
reconsider i as Element of NAT by A1;
per cases by A1,FINSEQ_1:25;
suppose A2: i in dom G; then
A3: (G^F).i = G.i by FINSEQ_1:def 7;
G.i in rng G by A2,FUNCT_1:3;
hence S is VectSp of K by A3,A1,Def3;
end;
suppose ex n be Nat st n in dom F & i=len G + n; then
consider n be Nat such that
A4: n in dom F & i=len G + n;
A5: (G^F).i = F.n by A4,FINSEQ_1:def 7;
F.n in rng F by A4,FUNCT_1:3;
hence S is VectSp of K by A5,A1,Def3;
end;
end;
end;
theorem Th12:
for X, Y being VectSp of K holds
ex I being Function of [:X,Y:],product <*X,Y*>
st I is one-to-one onto
& ( for x being Vector of X, y be Vector of Y holds I.(x,y) = <*x,y*> )
& ( for v, w being Vector of [:X,Y:] holds I.(v+w)=(I.v) + (I.w) )
& ( for v being Vector of [:X,Y:], r being Element of K
holds I.(r*v) = r*(I.v) )
& I.(0.[:X,Y:]) = 0.product <*X,Y*>
proof
let X, Y be VectSp of K;
set CarrX = the carrier of X;
set CarrY = the carrier of Y;
consider I be Function of [:CarrX,CarrY:],product <*CarrX,CarrY*> such that
A1: I is one-to-one onto
& for x, y being object st x in CarrX & y in CarrY
holds I.(x,y) = <*x,y*> by PRVECT_3:5;
len carr <*X,Y*> = len <*X,Y*> by PRVECT_1:def 11; then
A2:len carr <*X,Y*> = 2 by FINSEQ_1:44; then
A3:dom carr <*X,Y*> = {1,2} by FINSEQ_1:2,def 3;
len <*X,Y*> = 2 by FINSEQ_1:44; then
A4:dom <*X,Y*> = {1,2} by FINSEQ_1:2,def 3;
A5:<*X,Y*>.1 = X & <*X,Y*>.2 = Y;
1 in {1,2} & 2 in {1,2} by TARSKI:def 2; then
(carr <*X,Y*>).1 = CarrX & (carr <*X,Y*>).2 = CarrY
by A4,A5,PRVECT_1:def 11; then
A6:carr <*X,Y*> = <* CarrX,CarrY *> by A2,FINSEQ_1:44; then
reconsider I as Function of [:X,Y:],product <*X,Y*>;
A7: for x being Vector of X,y be Vector of Y holds I.(x,y) = <*x,y*> by A1;
A8: for v, w being Vector of [:X,Y:] holds I.(v+w) = I.v + I.w
proof
let v, w be Vector of [:X,Y:];
consider x1 be Vector of X, y1 be Vector of Y such that
A9: v = [x1,y1] by SUBSET_1:43;
consider x2 be Vector of X, y2 be Vector of Y such that
A10: w = [x2,y2] by SUBSET_1:43;
I.v = I.(x1,y1) & I.w = I.(x2,y2) by A9,A10; then
A11:I.v = <*x1,y1*> & I.w = <*x2,y2*> by A1;
A12:I.(v+w) =I.(x1+x2,y1+y2) by A9,A10,PRVECT_3:def 1
.= <* x1+x2,y1+y2 *> by A1;
reconsider Iv = I.v, Iw = I.w as Element of product carr <*X,Y*>;
reconsider j1=1, j2=2 as Element of dom (carr <*X,Y*>)
by A3,TARSKI:def 2;
A14: (addop <*X,Y*>).j1 = the addF of (<*X,Y*>.j1) by PRVECT_1:def 12;
A15: ([:addop <*X,Y*>:].(Iv,Iw)).j1
= ((addop <*X,Y*>).j1).(Iv.j1,Iw.j1) by PRVECT_1:def 8
.= x1+x2 by A14,A11;
A16: (addop <*X,Y*>).j2 = the addF of (<*X,Y*>.j2) by PRVECT_1:def 12;
A17: ([:addop <*X,Y*>:].(Iv,Iw)).j2
= ((addop <*X,Y*>).j2).(Iv.j2,Iw.j2) by PRVECT_1:def 8
.= y1+y2 by A16,A11;
consider Ivw be Function such that
A18: I.v + I.w = Ivw & dom Ivw = dom carr <*X,Y*>
& for i being object st i in dom carr <*X,Y*>
holds Ivw.i in carr (<*X,Y*>).i by CARD_3:def 5;
A19: dom Ivw = Seg 2 by A2,A18,FINSEQ_1:def 3; then
reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 2 by A19,FINSEQ_1:def 3;
hence thesis by A12,A18,A15,A17,FINSEQ_1:44;
end;
A20: for v being Vector of [:X,Y:], r being Element of K holds
I.(r*v)=r*(I.v)
proof
let v be Vector of [:X,Y:], r be Element of K;
consider x1 be Vector of X, y1 be Vector of Y such that
A21: v = [x1,y1] by SUBSET_1:43;
A22:I.v =I.(x1,y1) by A21 .= <*x1,y1*> by A1;
A23:I.(r*v) =I.(r*x1,r*y1) by A21,YDef2 .= <* r*x1,r*y1 *> by A1;
reconsider j1=1, j2=2 as Element of dom carr <*X,Y*> by A3,TARSKI:def 2;
A25: (multop <*X,Y*>).j1 = the lmult of (<*X,Y*>.j1)
& (multop <*X,Y*>).j2 = the lmult of (<*X,Y*>.j2) by Def8;
reconsider Iv = I.v as Element of product carr <*X,Y*>;
reconsider rr=r as Element of the carrier of K;
([:multop <*X,Y*>:].(rr,Iv)).j1 = ((multop <*X,Y*>).j1).(r,Iv.j1)
& ([:multop <*X,Y*>:].(rr,Iv)).j2 = ((multop <*X,Y*>).j2).(r,Iv.j2)
by PRVECT_2:def 2; then
A26: ([:multop <*X,Y*>:].(rr,Iv)).j1 = r*x1
& ([:multop <*X,Y*>:].(rr,Iv)).j2 = r*y1 by A25,A22;
consider Ivw be Function such that
A27: r*(I.v) = Ivw & dom Ivw = dom carr <*X,Y*>
& for i being object st i in dom carr <*X,Y*>
holds Ivw.i in carr (<*X,Y*>).i
by CARD_3:def 5;
A28: dom Ivw = Seg 2 by A2,A27,FINSEQ_1:def 3; then
reconsider Ivw as FinSequence by FINSEQ_1:def 2;
len Ivw = 2 by A28,FINSEQ_1:def 3;
hence thesis by A23,A27,A26,FINSEQ_1:44;
end;
I.(0.[:X,Y:]) = I.(0.[:X,Y:] + 0.[:X,Y:])
.= I.(0.[:X,Y:]) + I.(0.[:X,Y:]) by A8; then
I.(0.[:X,Y:]) - I.(0.[:X,Y:])
= I.(0.[:X,Y:]) + (I.(0.[:X,Y:]) - I.(0.[:X,Y:])) by RLVECT_1:28
.= I.(0.[:X,Y:]) + 0.product <*X,Y*> by RLVECT_1:15
.= I.(0.[:X,Y:]);
hence thesis by A7,A8,A20,A1,A6,RLVECT_1:15;
end;
theorem
for X, Y being VectorSpace-Sequence of K
holds ex I being Function of [:product X,product Y:],product (X^Y)
st I is one-to-one onto
& ( for x being Vector of product X, y being Vector of product Y
holds ex x1, y1 being FinSequence st x = x1 & y = y1 & I.(x,y) = x1^y1 )
& ( for v, w being Vector of [:product X,product Y:]
holds I.(v+w) = I.v + I.w )
& ( for v being Vector of [:product X,product Y:],
r be Element of the carrier of K
holds I.(r*v) = r*(I.v) )
& I.(0.[:product X,product Y:]) = 0.product (X^Y)
proof
let X,Y be VectorSpace-Sequence of K;
reconsider CX = carr X, CY = carr Y as non-empty non empty FinSequence;
A1:len CX = len X & len CY = len Y
& len carr (X^Y) = len (X^Y) by PRVECT_1:def 11;
consider I be Function of [:product CX,product CY:],product (CX^CY)
such that
A2: I is one-to-one onto
& for x, y being FinSequence st x in product CX & y in product CY
holds I.(x,y) = x^y by PRVECT_3:6;
set PX = product X;
set PY = product Y;
len carr (X^Y) = len X + len Y & len (CX^CY) =len X + len Y
by A1,FINSEQ_1:22; then
A3:dom carr (X^Y) = dom (CX^CY) by FINSEQ_3:29;
A4:for k being Nat st k in dom carr (X^Y) holds carr (X^Y).k = (CX^CY).k
proof
let k be Nat;
assume A5: k in dom carr (X^Y); then
reconsider k1=k as Element of dom (X^Y) by A1,FINSEQ_3:29;
A6: carr (X^Y).k = the carrier of ((X^Y).k1) by PRVECT_1:def 11;
A7: k in dom (X^Y) by A1,A5,FINSEQ_3:29;
per cases by A7,FINSEQ_1:25;
suppose A8: k in dom X; then
A9: k in dom CX by A1,FINSEQ_3:29;
reconsider k2=k1 as Element of dom X by A8;
thus carr (X^Y).k = the carrier of (X.k2) by A6,FINSEQ_1:def 7
.= CX.k by PRVECT_1:def 11
.= (CX^CY).k by A9,FINSEQ_1:def 7;
end;
suppose ex n being Nat st n in dom Y & k=len X + n; then
consider n be Nat such that
A10: n in dom Y & k=len X + n;
A11: n in dom CY by A1,A10,FINSEQ_3:29;
reconsider n1=n as Element of dom Y by A10;
thus carr (X^Y).k = the carrier of (Y.n1) by A6,A10,FINSEQ_1:def 7
.= CY.n by PRVECT_1:def 11
.= (CX^CY).k by A11,A10,A1,FINSEQ_1:def 7;
end;
end; then
A12: carr (X^Y) = CX^CY by A3,FINSEQ_1:13;
reconsider I as Function of [:PX,PY:] ,product (X^Y) by A3,A4,FINSEQ_1:13;
A13: for x being Vector of product X, y be Vector of product Y
holds ex x1, y1 being FinSequence st x = x1 & y = y1 & I.(x,y) = x1^y1
proof
let x be Vector of PX, y be Vector of PY;
reconsider x1=x, y1=y as FinSequence by NDIFF_5:9;
I.(x,y) = x1^y1 by A2;
hence thesis;
end;
A14: for v, w being Vector of [:PX,PY:] holds I.(v+w) = I.v + I.w
proof
let v, w be Vector of [:PX,PY:];
consider x1 be Vector of PX, y1 be Vector of PY such that
A15: v = [x1,y1] by SUBSET_1:43;
consider x2 be Vector of PX, y2 be Vector of PY such that
A16: w = [x2,y2] by SUBSET_1:43;
reconsider xx1 = x1, xx2 = x2 as FinSequence by NDIFF_5:9;
reconsider yy1 = y1, yy2 = y2 as FinSequence by NDIFF_5:9;
reconsider xx12 = x1+x2, yy12 = y1+y2 as FinSequence by NDIFF_5:9;
A17: dom xx1 = dom CX & dom xx2 = dom CX & dom xx12 = dom CX
& dom yy1 = dom CY & dom yy2 = dom CY & dom yy12 = dom CY by CARD_3:9;
I.v = I.(x1,y1) & I.w = I.(x2,y2) by A15,A16; then
A18:I.v = xx1^yy1 & I.w = xx2^yy2 by A2;
I.(v+w) = I.(x1+x2,y1+y2) by A15,A16,PRVECT_3:def 1; then
A19:I.(v+w) = xx12^yy12 by A2; then
A20: dom (xx12^yy12) = dom carr (X^Y) by CARD_3:9;
reconsider Iv = I.v, Iw = I.w as Element of product carr (X^Y);
reconsider Ivw = I.v + I.w as FinSequence by NDIFF_5:9;
for j0 being Nat st j0 in dom Ivw holds Ivw.j0 = (xx12^yy12).j0
proof
let j0 be Nat;
assume j0 in dom Ivw; then
reconsider j=j0 as Element of dom carr (X^Y) by CARD_3:9;
A22: Ivw.j0 = ((addop (X^Y)).j).(Iv.j,Iw.j) by PRVECT_1:def 8
.= (the addF of (X^Y).j).(Iv.j,Iw.j) by PRVECT_1:def 12;
per cases by A22,A3,FINSEQ_1:25;
suppose A23: j0 in dom CX; then
j0 in dom X by A1,FINSEQ_3:29; then
A24: (X^Y).j = X.j0 by FINSEQ_1:def 7;
A25: Iv.j = xx1.j & Iw.j = xx2.j by A23,A17,A18,FINSEQ_1:def 7;
A26: (xx12^yy12).j0 = xx12.j0 by A23,A17,FINSEQ_1:def 7;
reconsider j1=j0 as Element of dom carr X by A23;
(the addF of (X^Y).j).(Iv.j,Iw.j)
=((addop X ).j1).(xx1.j1,xx2.j1) by A24,A25,PRVECT_1:def 12
.= (xx12^yy12).j0 by A26,PRVECT_1:def 8;
hence Ivw.j0 = (xx12^yy12).j0 by A22;
end;
suppose ex n being Nat st n in dom CY & j0=len CX + n; then
consider n be Nat such that
A27: n in dom CY & j0=len CX + n;
A28: len CX = len xx1 & len CX = len xx2 & len CX = len xx12
by A17,FINSEQ_3:29;
n in dom Y by A1,A27,FINSEQ_3:29; then
A29: (X^Y).j = Y.n by A27,A1,FINSEQ_1:def 7;
A30: Iv.j = yy1.n & Iw.j = yy2.n by A17,A18,A27,A28,FINSEQ_1:def 7;
A31: (xx12^yy12).j0 = yy12.n by A27,A28,A17,FINSEQ_1:def 7;
reconsider j1=n as Element of dom carr Y by A27;
(the addF of (X^Y).j).(Iv.j,Iw.j)
= ((addop Y).j1).(yy1.j1,yy2.j1) by A29,A30,PRVECT_1:def 12
.= (xx12^yy12).j0 by A31,PRVECT_1:def 8;
hence Ivw.j0 = (xx12^yy12).j0 by A22;
end;
end;
hence thesis by A19,A20,CARD_3:9,FINSEQ_1:13;
end;
A32: for v being Vector of [:PX,PY:],
r being Element of the carrier of K holds I.(r*v)=r*(I.v)
proof
let v be Vector of [:PX,PY:],r be Element of the carrier of K;
consider x1 be Vector of PX, y1 be Vector of PY such that
A33: v = [x1,y1] by SUBSET_1:43;
reconsider xx1 = x1, yy1 = y1 as FinSequence by NDIFF_5:9;
reconsider rxx1 = r*x1, ryy1 = r*y1 as FinSequence by NDIFF_5:9;
A34: dom xx1 = dom CX & dom yy1 = dom CY
& dom rxx1 = dom CX & dom ryy1 = dom CY by CARD_3:9;
A35:I.v = I.(x1,y1) by A33 .= xx1^yy1 by A2;
A36:I.(r*v) = I.(r*x1,r*y1) by A33,YDef2 .= rxx1^ryy1 by A2;
reconsider Iv = I.v as Element of product carr (X^Y);
reconsider rIv=r*I.v as FinSequence by NDIFF_5:9;
A37:dom rIv = dom carr (X^Y) by CARD_3:9;
A38: dom (rxx1^ryy1) = dom carr (X^Y) by A36,CARD_3:9;
for j0 being Nat st j0 in dom rIv holds rIv.j0 = (rxx1^ryy1).j0
proof
let j0 be Nat;
assume A39: j0 in dom rIv; then
reconsider j = j0 as Element of dom carr (X^Y) by CARD_3:9;
A40: rIv.j0 = ((multop (X^Y)).j).(r,Iv.j) by PRVECT_2:def 2
.= (the lmult of (X^Y).j).(r,Iv.j) by Def8;
per cases by A3,A39,A37,FINSEQ_1:25;
suppose A41: j0 in dom CX; then
j0 in dom X by A1,FINSEQ_3:29; then
A42: (X^Y).j = X.j0 by FINSEQ_1:def 7;
A43: Iv.j = xx1.j by A41,A34,A35,FINSEQ_1:def 7;
A44: (rxx1^ryy1).j0 = rxx1.j0 by A41,A34,FINSEQ_1:def 7;
reconsider j1 = j0 as Element of dom carr X by A41;
(the lmult of (X^Y).j).(r,Iv.j)
= ((multop X ).j1).(r,xx1.j1) by A42,A43,Def8
.= (rxx1^ryy1).j0 by A44,PRVECT_2:def 2;
hence rIv.j0 = (rxx1^ryy1).j0 by A40;
end;
suppose ex n being Nat st n in dom CY & j0=len CX + n; then
consider n be Nat such that
A45: n in dom CY & j0=len CX + n;
A46: len CX= len xx1 & len CX= len rxx1 by A34,FINSEQ_3:29;
n in dom Y by A45,A1,FINSEQ_3:29; then
A47: (X^Y).j = Y.n by A45,A1,FINSEQ_1:def 7;
A48: Iv.j = yy1.n by A35,A45,A34,A46,FINSEQ_1:def 7;
A49: (rxx1^ryy1).j0 = ryy1.n by A45,A46,A34,FINSEQ_1:def 7;
reconsider j1 = n as Element of dom carr Y by A45;
(the lmult of (X^Y).j).(r,Iv.j)
= ((multop Y ).j1).(r,yy1.j1) by A47,A48,Def8
.= (rxx1^ryy1).j0 by A49,PRVECT_2:def 2;
hence rIv.j0 = (rxx1^ryy1).j0 by A40;
end;
end;
hence thesis by A36,A38,CARD_3:9,FINSEQ_1:13;
end;
I.(0.[:PX,PY:]) = I.(0.[:PX,PY:] + 0.[:PX,PY:])
.= I.(0.[:PX,PY:]) + I.(0.[:PX,PY:]) by A14; then
I.(0.[:PX,PY:]) - I.(0.[:PX,PY:])
= I.(0.[:PX,PY:]) + (I.(0.[:PX,PY:]) - I.(0.[:PX,PY:])) by RLVECT_1:28
.= I.(0.[:PX,PY:]) + 0. product (X^Y) by RLVECT_1:15
.= I.(0.[:PX,PY:]);
hence thesis by A13,A14,A32,A2,A12,RLVECT_1:15;
end;
theorem
for G, F being VectSp of K holds
( for x being set holds
( x is Vector of product <*G,F*>
iff ex x1 being Vector of G, x2 being Vector of F st x=<* x1,x2 *> ) )
& ( for x, y being Vector of product <*G,F*>,
x1, y1 being Vector of G, x2, y2 being Vector of F
st x = <*x1,x2*> & y = <*y1,y2*>
holds x+y = <*x1+y1,x2+y2*> )
& 0.(product <*G,F*>) = <* 0.G,0.F *>
& ( for x being Vector of product <*G,F*>,
x1 being Vector of G, x2 being Vector of F
st x = <* x1,x2 *> holds -x = <* -x1,-x2 *> )
& ( for x being Vector of product <*G,F*>,
x1 being Vector of G, x2 being Vector of F,
a being Element of K
st x = <*x1,x2*> holds a*x = <* a*x1,a*x2 *> )
proof
let G, F be VectSp of K;
consider I be Function of [:G,F:], product <* G,F *> such that
A1: I is one-to-one onto
& ( for x being Vector of G, y being Vector of F
holds I.(x,y) = <* x,y *> )
& ( for v, w being Vector of [:G,F:] holds I.(v+w) = I.v + I.w )
& ( for v being Vector of [:G,F:], r being Element of K holds
I.(r*v)=r*(I.v) ) & 0. product <*G,F*> = I.(0.[:G,F:]) by Th12;
thus
A2: for x being set holds
( x is Vector of product <*G,F*>
iff ex x1 being Vector of G, x2 being Vector of F st x = <* x1,x2 *> )
proof
let y be set;
hereby assume y is Vector of product <*G,F*>;
then consider x be Element of the carrier of [:G,F:] such that
A3: y = I.x by A1,FUNCT_2:113;
consider x1 be Vector of G, x2 be Vector of F such that
A4: x = [x1,x2] by SUBSET_1:43;
take x1, x2;
I.(x1,x2) = <*x1,x2*> by A1;
hence y = <*x1,x2*> by A3,A4;
end;
now assume ex x1 being Vector of G, x2 being Vector of F
st y = <*x1,x2*>;
then
consider x1 be Vector of G, x2 be Vector of F such that
A5: y = <*x1,x2*>;
A6: I.[x1,x2] in rng I by FUNCT_2:112;
I.(x1,x2) = <*x1,x2*> by A1;
hence y is Vector of product <*G,F*> by A5,A6;
end;
hence thesis;
end;
thus
A7: for x, y being Vector of product <*G,F*>,
x1, y1 being Vector of G, x2,y2 be Vector of F
st x = <*x1,x2*> & y = <*y1,y2*>
holds x+y = <*x1+y1,x2+y2*>
proof
let x,y be Vector of product <*G,F*>;
let x1,y1 be Vector of G, x2,y2 be Vector of F;
assume A8: x = <*x1,x2*> & y = <*y1,y2*>;
reconsider z=[x1,x2], w=[y1,y2] as Vector of [:G,F:];
A9: z+w = [x1+y1,x2+y2] by PRVECT_3:def 1;
I.(x1+y1,x2+y2) = <* x1+y1,x2+y2 *>
& I.(x1,x2) = <* x1,x2 *> & I.(y1,y2) = <* y1,y2 *> by A1;
hence <* x1+y1,x2+y2 *> =x+y by A1,A9,A8;
end;
thus
A10: 0. product <*G,F*> = <* 0.G,0.F *>
proof
I.(0.G,0.F) = <* 0.G,0.F *> by A1;
hence thesis by A1;
end;
thus for x being Vector of product <*G,F*>,
x1 being Vector of G, x2 being Vector of F
st x = <*x1,x2*> holds -x = <* -x1,-x2 *>
proof
let x be Vector of product <*G,F*>;
let x1 be Vector of G, x2 be Vector of F;
assume A11: x=<* x1,x2 *>;
reconsider y = <* -x1,-x2 *> as Vector of product <*G,F*> by A2;
x+y = <* x1+-x1,x2+-x2 *> by A7,A11
.= <* 0.G,x2+-x2 *> by RLVECT_1:def 10
.= 0.(product <*G,F*>) by A10,RLVECT_1:def 10;
hence thesis by RLVECT_1:def 10;
end;
thus for x being Vector of product <*G,F*>,
x1 being Vector of G, x2 being Vector of F, a being Element of K
st x = <* x1,x2 *> holds a*x = <* a*x1,a*x2 *>
proof
let x be Vector of product <*G,F*>;
let x1 be Vector of G, x2 be Vector of F, a be Element of K;
assume A12: x = <* x1,x2 *>;
reconsider y = [x1,x2] as Vector of [:G,F:];
A13: <* x1,x2 *> = I.(x1,x2) by A1;
I.(a*y) = I.(a*x1,a*x2) by YDef2
.= <* a*x1,a*x2 *> by A1;
hence thesis by A1,A12,A13;
end;
end;