let F be finite Field; :: thesis: for V being VectSp of F
for n, q being Nat st V is finite-dimensional & n = dim V & q = card the carrier of F holds
card the carrier of V = q |^ n
let V be VectSp of F; :: thesis: for n, q being Nat st V is finite-dimensional & n = dim V & q = card the carrier of F holds
card the carrier of V = q |^ n
let n, q be Nat; :: thesis: ( V is finite-dimensional & n = dim V & q = card the carrier of F implies card the carrier of V = q |^ n )
assume that
A1:
V is finite-dimensional
and
A2:
n = dim V
and
A3:
q = card the carrier of F
; :: thesis: card the carrier of V = q |^ n
consider B being finite Subset of V such that
A4:
B is Basis of V
by A1, MATRLIN:def 3;
A5:
B is linearly-independent
by A4, VECTSP_7:def 3;
A6:
Lin B = VectSpStr(# the carrier of V,the addF of V,the ZeroF of V,the lmult of V #)
by A4, VECTSP_7:def 3;
A7:
card B = n
by A1, A2, A4, VECTSP_9:def 2;
q <> 0
by A3;
then A8:
q > 0
;
now per cases
( n = 0 or n <> 0 )
;
suppose
n <> 0
;
:: thesis: card the carrier of V = q |^ nthen A10:
B <> 0
by A7;
consider bf being
FinSequence such that A11:
rng bf = B
and A12:
bf is
one-to-one
by FINSEQ_4:73;
len bf = n
by A7, A11, A12, FINSEQ_4:77;
then A13:
Seg n = dom bf
by FINSEQ_1:def 3;
reconsider Vbf =
bf as
FinSequence of the
carrier of
V by A11, FINSEQ_1:def 4;
set cLinB = the
carrier of
(Lin B);
set ntocF =
n -tuples_on the
carrier of
F;
defpred S1[
Function,
set ]
means ex
lc being
Linear_Combination of
B st
( ( for
i being
set st
i in dom $1 holds
lc . (Vbf . i) = $1
. i ) & $2
= Sum (lc (#) Vbf) );
A14:
for
x being
Element of
n -tuples_on the
carrier of
F ex
y being
Element of the
carrier of
(Lin B) st
S1[
x,
y]
proof
let f be
Element of
n -tuples_on the
carrier of
F;
:: thesis: ex y being Element of the carrier of (Lin B) st S1[f,y]
ex
lc being
Linear_Combination of
B st
for
i being
set st
i in dom f holds
lc . (Vbf . i) = f . i
proof
deffunc H1(
set )
-> set =
f . (union (Vbf " {$1}));
A15:
for
x being
set st
x in B holds
H1(
x)
in the
carrier of
F
consider lc being
Function of
B,the
carrier of
F such that A19:
for
y being
set st
y in B holds
lc . y = H1(
y)
from FUNCT_2:sch 2(A15);
set ll =
lc +* ((the carrier of V \ B) --> (0. F));
A20:
dom ((the carrier of V \ B) --> (0. F)) = the
carrier of
V \ B
by FUNCOP_1:19;
then
dom (lc +* ((the carrier of V \ B) --> (0. F))) = (dom lc) \/ (the carrier of V \ B)
by FUNCT_4:def 1;
then
dom (lc +* ((the carrier of V \ B) --> (0. F))) = B \/ (the carrier of V \ B)
by FUNCT_2:def 1;
then
dom (lc +* ((the carrier of V \ B) --> (0. F))) = B \/ the
carrier of
V
by XBOOLE_1:39;
then A21:
dom (lc +* ((the carrier of V \ B) --> (0. F))) = the
carrier of
V
by XBOOLE_1:12;
A24:
rng (lc +* ((the carrier of V \ B) --> (0. F))) c= (rng lc) \/ (rng ((the carrier of V \ B) --> (0. F)))
by FUNCT_4:18;
lc +* ((the carrier of V \ B) --> (0. F)) is
Function of the
carrier of
V,the
carrier of
F
by A21, A24, FUNCT_2:4, XBOOLE_1:1;
then A25:
lc +* ((the carrier of V \ B) --> (0. F)) is
Element of
Funcs the
carrier of
V,the
carrier of
F
by FUNCT_2:11;
A26:
for
i being
set st
i in dom f holds
(lc +* ((the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i
proof
let i be
set ;
:: thesis: ( i in dom f implies (lc +* ((the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i )
assume A27:
i in dom f
;
:: thesis: (lc +* ((the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i
A28:
i in dom Vbf
by A13, A27, FINSEQ_2:144;
then
Vbf . i in B
by A11, FUNCT_1:12;
then consider y being
Element of
B such that A29:
y = Vbf . i
;
A30:
Vbf . i in {y}
by A29, TARSKI:def 1;
consider ee being
set such that A31:
Vbf " {y} c= {ee}
by A12, FUNCT_1:159;
A32:
i in Vbf " {y}
by A28, A30, FUNCT_1:def 13;
then
{i} c= {ee}
by A31, ZFMISC_1:37;
then
i = ee
by ZFMISC_1:24;
then A33:
Vbf " {y} = {i}
by A31, A32, ZFMISC_1:39;
not
y in the
carrier of
V \ B
by A10, XBOOLE_0:def 5;
then
(lc +* ((the carrier of V \ B) --> (0. F))) . y = lc . y
by A20, FUNCT_4:12;
then
(lc +* ((the carrier of V \ B) --> (0. F))) . y = f . (union (Vbf " {y}))
by A10, A19;
hence
(lc +* ((the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i
by A29, A33, ZFMISC_1:31;
:: thesis: verum
end;
A34:
for
v being
Element of
V st not
v in B holds
(lc +* ((the carrier of V \ B) --> (0. F))) . v = 0. F
then reconsider L =
lc +* ((the carrier of V \ B) --> (0. F)) as
Linear_Combination of
V by A25, VECTSP_6:def 4;
for
v being
Element of
V st
v in Carrier L holds
v in B
then
Carrier L c= B
by SUBSET_1:7;
then
L is
Linear_Combination of
B
by VECTSP_6:def 7;
hence
ex
lc being
Linear_Combination of
B st
for
i being
set st
i in dom f holds
lc . (Vbf . i) = f . i
by A26;
:: thesis: verum
end;
then consider lc being
Linear_Combination of
B such that A37:
for
i being
set st
i in dom f holds
lc . (Vbf . i) = f . i
;
ex
y being
Element of
V st
y = Sum (lc (#) Vbf)
;
hence
ex
y being
Element of the
carrier of
(Lin B) st
S1[
f,
y]
by A6, A37;
:: thesis: verum
end; consider G being
Function of
(n -tuples_on the carrier of F),the
carrier of
(Lin B) such that A38:
for
tup being
Element of
n -tuples_on the
carrier of
F holds
S1[
tup,
G . tup]
from FUNCT_2:sch 3(A14);
A39:
dom G = n -tuples_on the
carrier of
F
by FUNCT_2:def 1;
A40:
for
L being
Linear_Combination of
B ex
nt being
Element of
n -tuples_on the
carrier of
F st
for
i being
set st
i in dom nt holds
nt . i = L . (Vbf . i)
for
c being
set st
c in the
carrier of
(Lin B) holds
ex
x being
set st
(
x in n -tuples_on the
carrier of
F &
c = G . x )
then A61:
rng G = the
carrier of
(Lin B)
by FUNCT_2:16;
for
x1,
x2 being
set st
x1 in dom G &
x2 in dom G &
G . x1 = G . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
:: thesis: ( x1 in dom G & x2 in dom G & G . x1 = G . x2 implies x1 = x2 )
assume that A62:
x1 in dom G
and A63:
x2 in dom G
and A64:
G . x1 = G . x2
;
:: thesis: x1 = x2
reconsider t1 =
x1 as
Element of
n -tuples_on the
carrier of
F by A62;
reconsider t2 =
x2 as
Element of
n -tuples_on the
carrier of
F by A63;
consider L1 being
Linear_Combination of
B such that A65:
( ( for
i being
set st
i in dom t1 holds
L1 . (Vbf . i) = t1 . i ) &
G . t1 = Sum (L1 (#) Vbf) )
by A38;
consider L2 being
Linear_Combination of
B such that A66:
( ( for
i being
set st
i in dom t2 holds
L2 . (Vbf . i) = t2 . i ) &
G . t2 = Sum (L2 (#) Vbf) )
by A38;
Carrier L1 c= rng Vbf
by A11, VECTSP_6:def 7;
then A67:
Sum L1 = Sum (L1 (#) Vbf)
by A12, VECTSP_9:7;
Carrier L2 c= rng Vbf
by A11, VECTSP_6:def 7;
then
Sum L2 = Sum (L2 (#) Vbf)
by A12, VECTSP_9:7;
then
(Sum L1) - (Sum L2) = 0. V
by A64, A65, A66, A67, VECTSP_1:66;
then A68:
Sum (L1 - L2) = 0. V
by VECTSP_6:80;
L1 - L2 is
Linear_Combination of
B
by VECTSP_6:75;
then A69:
Carrier (L1 - L2) = {}
by A5, A68, VECTSP_7:def 1;
for
v being
Element of
V holds
L1 . v = L2 . v
then A70:
L1 = L2
by VECTSP_6:def 10;
A71:
(
dom t1 = Seg n &
dom t2 = Seg n )
by FINSEQ_2:144;
for
k being
Nat st
k in dom t1 holds
t1 . k = t2 . k
hence
x1 = x2
by A71, FINSEQ_1:17;
:: thesis: verum
end; then
G is
one-to-one
by FUNCT_1:def 8;
then
n -tuples_on the
carrier of
F,
G .: (n -tuples_on the carrier of F) are_equipotent
by A39, CARD_1:60;
then A73:
n -tuples_on the
carrier of
F,the
carrier of
(Lin B) are_equipotent
by A39, A61, RELAT_1:146;
A74:
(
card (Seg n) = card n &
card q = card the
carrier of
F )
by A3, FINSEQ_1:76;
card (n -tuples_on the carrier of F) =
card (Funcs (Seg n),the carrier of F)
by FINSEQ_2:111
.=
card (Funcs n,q)
by A74, FUNCT_5:68
.=
q |^ n
by A8, Th4
;
hence
card the
carrier of
V = q |^ n
by A6, A73, CARD_1:21;
:: thesis: verum end;
hence
card the carrier of V = q |^ n
; :: thesis: verum