let F be finite Field; 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; 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; ( 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
; 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 1;
A5:
B is linearly-independent
by A4, VECTSP_7:def 3;
A6:
Lin B = ModuleStr(# 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 1;
now card the carrier of V = q |^ nper cases
( n = 0 or n <> 0 )
;
suppose
n <> 0
;
card the carrier of V = q |^ nthen A9:
B <> 0
by A7;
consider bf being
FinSequence such that A10:
rng bf = B
and A11:
bf is
one-to-one
by FINSEQ_4:58;
len bf = n
by A7, A10, A11, FINSEQ_4:62;
then A12:
Seg n = dom bf
by FINSEQ_1:def 3;
reconsider Vbf =
bf as
FinSequence of the
carrier of
V by A10, 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) );
A13:
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;
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(
object )
-> set =
f . (union (Vbf " {$1}));
A14:
for
x being
object st
x in B holds
H1(
x)
in the
carrier of
F
consider lc being
Function of
B, the
carrier of
F such that A17:
for
y being
object st
y in B holds
lc . y = H1(
y)
from FUNCT_2:sch 2(A14);
set ll =
lc +* (( the carrier of V \ B) --> (0. F));
A18:
dom (( the carrier of V \ B) --> (0. F)) = the
carrier of
V \ B
;
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 A19:
dom (lc +* (( the carrier of V \ B) --> (0. F))) = the
carrier of
V
by XBOOLE_1:12;
rng (lc +* (( the carrier of V \ B) --> (0. F))) c= (rng lc) \/ (rng (( the carrier of V \ B) --> (0. F)))
by FUNCT_4:17;
then
lc +* (( the carrier of V \ B) --> (0. F)) is
Function of the
carrier of
V, the
carrier of
F
by A19, FUNCT_2:2, XBOOLE_1:1;
then A20:
lc +* (( the carrier of V \ B) --> (0. F)) is
Element of
Funcs ( the
carrier of
V, the
carrier of
F)
by FUNCT_2:8;
A21:
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 ;
( i in dom f implies (lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i )
assume
i in dom f
;
(lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i
then A22:
i in dom Vbf
by A12, FINSEQ_2:124;
then
Vbf . i in B
by A10, FUNCT_1:3;
then consider y being
Element of
B such that A23:
y = Vbf . i
;
A24:
Vbf . i in {y}
by A23, TARSKI:def 1;
consider ee being
object such that A25:
Vbf " {y} c= {ee}
by A11, FUNCT_1:89;
A26:
i in Vbf " {y}
by A22, A24, FUNCT_1:def 7;
then
{i} c= {ee}
by A25, ZFMISC_1:31;
then
i = ee
by ZFMISC_1:18;
then A27:
Vbf " {y} = {i}
by A25, A26, ZFMISC_1:33;
not
y in the
carrier of
V \ B
by A9, XBOOLE_0:def 5;
then
(lc +* (( the carrier of V \ B) --> (0. F))) . y = lc . y
by A18, FUNCT_4:11;
then
(lc +* (( the carrier of V \ B) --> (0. F))) . y = f . (union (Vbf " {y}))
by A9, A17;
hence
(lc +* (( the carrier of V \ B) --> (0. F))) . (Vbf . i) = f . i
by A23, A27, ZFMISC_1:25;
verum
end;
A28:
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 A20, VECTSP_6:def 1;
for
v being
Element of
V st
v in Carrier L holds
v in B
then
Carrier L c= B
;
then
L is
Linear_Combination of
B
by VECTSP_6:def 4;
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 A21;
verum
end;
then consider lc being
Linear_Combination of
B such that A31:
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, A31;
verum
end; consider G being
Function of
(n -tuples_on the carrier of F), the
carrier of
(Lin B) such that A32:
for
tup being
Element of
n -tuples_on the
carrier of
F holds
S1[
tup,
G . tup]
from FUNCT_2:sch 3(A13);
A33:
dom G = n -tuples_on the
carrier of
F
by FUNCT_2:def 1;
A34:
for
L being
Linear_Combination of
B ex
nt being
Element of
n -tuples_on the
carrier of
F st
for
i being
object st
i in dom nt holds
nt . i = L . (Vbf . i)
for
c being
object st
c in the
carrier of
(Lin B) holds
ex
x being
object st
(
x in n -tuples_on the
carrier of
F &
c = G . x )
then A54:
rng G = the
carrier of
(Lin B)
by FUNCT_2:10;
for
x1,
x2 being
object st
x1 in dom G &
x2 in dom G &
G . x1 = G . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom G & x2 in dom G & G . x1 = G . x2 implies x1 = x2 )
assume that A55:
x1 in dom G
and A56:
x2 in dom G
and A57:
G . x1 = G . x2
;
x1 = x2
reconsider t1 =
x1 as
Element of
n -tuples_on the
carrier of
F by A55;
reconsider t2 =
x2 as
Element of
n -tuples_on the
carrier of
F by A56;
consider L1 being
Linear_Combination of
B such that A58:
for
i being
set st
i in dom t1 holds
L1 . (Vbf . i) = t1 . i
and A59:
G . t1 = Sum (L1 (#) Vbf)
by A32;
consider L2 being
Linear_Combination of
B such that A60:
for
i being
set st
i in dom t2 holds
L2 . (Vbf . i) = t2 . i
and A61:
G . t2 = Sum (L2 (#) Vbf)
by A32;
Carrier L1 c= rng Vbf
by A10, VECTSP_6:def 4;
then A62:
Sum L1 = Sum (L1 (#) Vbf)
by A11, VECTSP_9:3;
Carrier L2 c= rng Vbf
by A10, VECTSP_6:def 4;
then
Sum L2 = Sum (L2 (#) Vbf)
by A11, VECTSP_9:3;
then
(Sum L1) - (Sum L2) = 0. V
by A57, A59, A61, A62, VECTSP_1:19;
then A63:
Sum (L1 - L2) = 0. V
by VECTSP_6:47;
L1 - L2 is
Linear_Combination of
B
by VECTSP_6:42;
then A64:
Carrier (L1 - L2) = {}
by A5, A63, VECTSP_7:def 1;
for
v being
Element of
V holds
L1 . v = L2 . v
then A65:
L1 = L2
by VECTSP_6:def 7;
A66:
dom t1 = Seg n
by FINSEQ_2:124;
A67:
dom t2 = Seg n
by FINSEQ_2:124;
for
k being
Nat st
k in dom t1 holds
t1 . k = t2 . k
hence
x1 = x2
by A67, FINSEQ_1:13, FINSEQ_2:124;
verum
end; then
G is
one-to-one
;
then
n -tuples_on the
carrier of
F,
G .: (n -tuples_on the carrier of F) are_equipotent
by A33, CARD_1:33;
then A69:
n -tuples_on the
carrier of
F, the
carrier of
(Lin B) are_equipotent
by A33, A54, RELAT_1:113;
A70:
card (Seg n) = card n
by FINSEQ_1:55;
A71:
card q = card the
carrier of
F
by A3;
card (n -tuples_on the carrier of F) =
card (Funcs ((Seg n), the carrier of F))
by FINSEQ_2:93
.=
card (Funcs (n,q))
by A70, A71, FUNCT_5:61
.=
q |^ n
by A3, Th4
;
hence
card the
carrier of
V = q |^ n
by A6, A69, CARD_1:5;
verum end;
hence
card the carrier of V = q |^ n
; verum