let F be Field; for E1 being FieldExtension of F
for E2 being b1 -homomorphic FieldExtension of F
for h being Homomorphism of E1,E2 holds
( h is F -fixing iff h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F)) )
let E1 be FieldExtension of F; for E2 being E1 -homomorphic FieldExtension of F
for h being Homomorphism of E1,E2 holds
( h is F -fixing iff h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F)) )
let E2 be E1 -homomorphic FieldExtension of F; for h being Homomorphism of E1,E2 holds
( h is F -fixing iff h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F)) )
let h be Homomorphism of E1,E2; ( h is F -fixing iff h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F)) )
G:
now ( h is F -fixing implies h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F)) )assume AS:
h is
F -fixing
;
h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F))H:
dom h =
the
carrier of
E1
by FUNCT_2:def 1
.=
the
carrier of
(VecSp (E1,F))
by FIELD_4:def 6
;
rng h c= the
carrier of
E2
by RELAT_1:def 19;
then
rng h c= the
carrier of
(VecSp (E2,F))
by FIELD_4:def 6;
then reconsider f =
h as
Function of
(VecSp (E1,F)),
(VecSp (E2,F)) by H, FUNCT_2:2;
then A:
f is
additive
;
now for a being Scalar of F
for x being Vector of (VecSp (E1,F)) holds f . (a * x) = a * (f . x)let a be
Scalar of
F;
for x being Vector of (VecSp (E1,F)) holds f . (a * x) = a * (f . x)let x be
Vector of
(VecSp (E1,F));
f . (a * x) = a * (f . x)reconsider v =
x as
Element of
E1 by FIELD_4:def 6;
F is
Subring of
E1
by FIELD_4:def 1;
then
the
carrier of
F c= the
carrier of
E1
by C0SP1:def 3;
then reconsider u1 =
a as
Element of
E1 ;
F is
Subring of
E2
by FIELD_4:def 1;
then
the
carrier of
F c= the
carrier of
E2
by C0SP1:def 3;
then reconsider u2 =
a as
Element of
E2 ;
I:
[u1,v] in [: the carrier of F, the carrier of E1:]
by ZFMISC_1:def 2;
H:
a * x =
( the multF of E1 | [: the carrier of F, the carrier of E1:]) . (
u1,
v)
by FIELD_4:def 6
.=
u1 * v
by I, FUNCT_1:49
;
J:
[u2,(h . v)] in [: the carrier of F, the carrier of E2:]
by ZFMISC_1:def 2;
thus f . (a * x) =
(h . u1) * (h . v)
by H, GROUP_6:def 6
.=
u2 * (h . v)
by AS
.=
( the multF of E2 | [: the carrier of F, the carrier of E2:]) . (
u2,
(h . v))
by J, FUNCT_1:49
.=
a * (f . x)
by FIELD_4:def 6
;
verum end; hence
h is
linear-transformation of
(VecSp (E1,F)),
(VecSp (E2,F))
by A, MOD_2:def 2;
verum end;
set V1 = VecSp (E1,F);
set V2 = VecSp (E2,F);
now ( h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F)) implies h is F -fixing )assume
h is
linear-transformation of
(VecSp (E1,F)),
(VecSp (E2,F))
;
h is F -fixing then reconsider h1 =
h as
linear-transformation of
(VecSp (E1,F)),
(VecSp (E2,F)) ;
A:
the
carrier of
E1 = the
carrier of
(VecSp (E1,F))
by FIELD_4:def 6;
reconsider 1V =
1. E1 as
Element of
(VecSp (E1,F)) by FIELD_4:def 6;
now for a being Element of F holds h . a = alet a be
Element of
F;
h . a = a
F is
Subfield of
E1
by FIELD_4:7;
then B:
( the
carrier of
F c= the
carrier of
E1 & the
multF of
F = the
multF of
E1 || the
carrier of
F &
1. F = 1. E1 )
by EC_PF_1:def 1;
F is
Subfield of
E2
by FIELD_4:7;
then
the
carrier of
F c= the
carrier of
E2
by EC_PF_1:def 1;
then reconsider a2 =
a as
Element of
E2 ;
reconsider aV =
a as
Element of
(VecSp (E1,F)) by A, B;
D:
[a,(1. F)] in [: the carrier of F, the carrier of E1:]
by B, ZFMISC_1:def 2;
E:
[a,(1. F)] in [: the carrier of F, the carrier of F:]
by ZFMISC_1:def 2;
F: the
multF of
F . (
a,
(1. F)) =
the
multF of
E1 . (
a,
(1. F))
by B, E, FUNCT_1:49
.=
( the multF of E1 | [: the carrier of F, the carrier of E1:]) . (
a,
(1. F))
by D, FUNCT_1:49
.=
the
lmult of
(VecSp (E1,F)) . (
a,
1V)
by B, FIELD_4:def 6
;
I:
[a,(1. E2)] in [: the carrier of F, the carrier of E2:]
by ZFMISC_1:def 2;
G:
h1 . 1V =
h . (1_ E1)
.=
1_ E2
by GROUP_1:def 13
;
J: the
lmult of
(VecSp (E2,F)) . (
a,
(1. E2)) =
( the multF of E2 | [: the carrier of F, the carrier of E2:]) . (
a,
(1. E2))
by FIELD_4:def 6
.=
the
multF of
E2 . (
a2,
(1. E2))
by I, FUNCT_1:49
;
h . (a * (1. F)) =
h1 . (a * 1V)
by F
.=
a * (h1 . 1V)
by MOD_2:def 2
.=
a2 * (1. E2)
by J, G
;
hence
h . a = a
;
verum end; hence
h is
F -fixing
;
verum end;
hence
( h is F -fixing iff h is linear-transformation of (VecSp (E1,F)),(VecSp (E2,F)) )
by G; verum