let p be Prime; for F being Z/ p -homomorphic p -characteristic Field
for f being Homomorphism of (Z/ p),F holds f = canHom_Z/ (p,F)
let F be Z/ p -homomorphic p -characteristic Field; for f being Homomorphism of (Z/ p),F holds f = canHom_Z/ (p,F)
let f be Homomorphism of (Z/ p),F; f = canHom_Z/ (p,F)
set g = canHom_Z/ (p,F);
A1:
f is unity-preserving
;
A2:
( canHom_Z/ (p,F) is unity-preserving & canHom_Z/ (p,F) is additive & canHom_Z/ (p,F) is multiplicative )
;
A3: dom f =
the carrier of (Z/ p)
by FUNCT_2:def 1
.=
dom (canHom_Z/ (p,F))
by FUNCT_2:def 1
;
A4:
1. (Z/ p) = 1
by INT_3:14, INT_2:def 4;
reconsider p1 = p - 1 as Element of NAT by INT_1:3;
A5:
p1 + 1 = p
;
defpred S1[ Nat] means for j being Element of (Z/ p) st j = $1 holds
f . j = (canHom_Z/ (p,F)) . j;
f . 0 =
f . (0. (Z/ p))
by NAT_1:44, SUBSET_1:def 8
.=
0. F
by RING_2:6
.=
(canHom_Z/ (p,F)) . (0. (Z/ p))
by RING_2:6
.=
(canHom_Z/ (p,F)) . 0
by NAT_1:44, SUBSET_1:def 8
;
then A6:
S1[ 0 ]
;
A7:
for k being Element of NAT st 0 <= k & k < p1 & S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( 0 <= k & k < p1 & S1[k] implies S1[k + 1] )
assume A8:
(
0 <= k &
k < p1 )
;
( not S1[k] or S1[k + 1] )
assume A9:
S1[
k]
;
S1[k + 1]
reconsider e = 1 as
Element of
Segm p by A4;
k < p
by A5, A8, NAT_1:13;
then reconsider z =
k as
Element of
(Z/ p) by NAT_1:44;
reconsider z0 =
z as
Element of
Segm p ;
A10:
k + 1
< p1 + 1
by A8, XREAL_1:6;
then reconsider z1 =
k + 1 as
Element of
Segm p by NAT_1:44;
reconsider z1 =
z1 as
Element of
(Z/ p) ;
A11:
z + (1. (Z/ p)) =
(addint p) . (
k,1)
by INT_3:14, INT_2:def 4
.=
z0 + e
by A10, INT_3:7
.=
k + 1
;
f . z1 =
(f . z) + (f . (1. (Z/ p)))
by A11, VECTSP_1:def 20
.=
((canHom_Z/ (p,F)) . z) + ((canHom_Z/ (p,F)) . (1. (Z/ p)))
by A9, A1, A2
.=
(canHom_Z/ (p,F)) . z1
by A11, A2
;
hence
S1[
k + 1]
;
verum
end;
A12:
for k being Element of NAT st 0 <= k & k <= p1 holds
S1[k]
from INT_1:sch 7(A6, A7);
hence
f = canHom_Z/ (p,F)
by A3; verum