let F1 be Field; for p being non constant Element of the carrier of (Polynom-Ring F1)
for F2 being F1 -isomorphic Field
for h being Isomorphism of F1,F2 st p splits_in F1 holds
(PolyHom h) . p splits_in F2
let p be non constant Element of the carrier of (Polynom-Ring F1); for F2 being F1 -isomorphic Field
for h being Isomorphism of F1,F2 st p splits_in F1 holds
(PolyHom h) . p splits_in F2
let F2 be F1 -isomorphic Field; for h being Isomorphism of F1,F2 st p splits_in F1 holds
(PolyHom h) . p splits_in F2
let h be Isomorphism of F1,F2; ( p splits_in F1 implies (PolyHom h) . p splits_in F2 )
assume AS:
p splits_in F1
; (PolyHom h) . p splits_in F2
defpred S1[ Nat] means for p being Element of the carrier of (Polynom-Ring F1) st deg p = $1 & p splits_in F1 holds
(PolyHom h) . p splits_in F2;
IA:
S1[1]
IS:
now for k being Nat st 1 <= k & S1[k] holds
S1[k + 1]let k be
Nat;
( 1 <= k & S1[k] implies S1[k + 1] )assume
1
<= k
;
( S1[k] implies S1[k + 1] )assume IV:
S1[
k]
;
S1[k + 1]now for p being Element of the carrier of (Polynom-Ring F1) st deg p = k + 1 & p splits_in F1 holds
(PolyHom h) . p splits_in F2let p be
Element of the
carrier of
(Polynom-Ring F1);
( deg p = k + 1 & p splits_in F1 implies (PolyHom h) . b1 splits_in F2 )assume AS3:
(
deg p = k + 1 &
p splits_in F1 )
;
(PolyHom h) . b1 splits_in F2then consider a being non
zero Element of
F1,
q being
Ppoly of
F1 such that A1:
p = a * q
by FIELD_4:def 5;
reconsider qq =
q as
Element of the
carrier of
(Polynom-Ring F1) by POLYNOM3:def 10;
consider G being non
empty FinSequence of
(Polynom-Ring F1) such that A2:
(
q = Product G & ( for
i being
Nat st
i in dom G holds
ex
a being
Element of
F1 st
G . i = rpoly (1,
a) ) )
by RING_5:def 4;
deg q = k + 1
by AS3, A1, RING_5:4;
then A3:
len G = k + 1
by A2, lemppoly;
consider H being
FinSequence,
y being
object such that B2:
G = H ^ <*y*>
by FINSEQ_1:46;
B2a:
rng H c= rng G
by B2, FINSEQ_1:29;
B2b:
rng G c= the
carrier of
(Polynom-Ring F1)
by FINSEQ_1:def 4;
then reconsider H =
H as
FinSequence of
(Polynom-Ring F1) by B2a, XBOOLE_1:1, FINSEQ_1:def 4;
B3:
len G =
(len H) + (len <*y*>)
by B2, FINSEQ_1:22
.=
(len H) + 1
by FINSEQ_1:39
;
rng <*y*> = {y}
by FINSEQ_1:39;
then G5:
y in rng <*y*>
by TARSKI:def 1;
rng <*y*> c= rng G
by B2, FINSEQ_1:30;
then reconsider y =
y as
Element of the
carrier of
(Polynom-Ring F1) by G5, B2b;
dom <*y*> = {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
then
1
in dom <*y*>
by TARSKI:def 1;
then B6:
G . (k + 1) =
<*y*> . 1
by B2, B3, A3, FINSEQ_1:def 7
.=
y
by FINSEQ_1:def 8
;
dom G = Seg (k + 1)
by A3, FINSEQ_1:def 3;
then consider b being
Element of
F1 such that B9:
y = rpoly (1,
b)
by A2, B6, FINSEQ_1:4;
deg y = 1
by B9, HURWITZ:27;
then
deg ((PolyHom h) . y) = 1
by FIELD_1:31;
then Y:
(PolyHom h) . y splits_in F2
by FIELD_4:29;
per cases
( H is empty or not H is empty )
;
suppose
not
H is
empty
;
(PolyHom h) . b1 splits_in F2then reconsider H =
H as non
empty FinSequence of
(Polynom-Ring F1) ;
reconsider q1 =
Product H as
Element of the
carrier of
(Polynom-Ring F1) ;
C:
dom H c= dom G
by B2, FINSEQ_1:26;
then reconsider q1p =
q1 as
Ppoly of
F1 by RING_5:def 4;
E:
q1p splits_in F1
by lemppolspl;
deg q1 = k
by A3, B3, D, lemppoly;
then F:
(PolyHom h) . q1 splits_in F2
by E, IV;
then reconsider ha =
h . a as non
zero Element of
F2 by STRUCT_0:def 12;
reconsider q1h =
(PolyHom h) . q1,
yh =
(PolyHom h) . y as
Polynomial of
F2 ;
I:
q1h *' yh =
((PolyHom h) . q1) * ((PolyHom h) . y)
by POLYNOM3:def 10
.=
(PolyHom h) . (q1 * y)
by FIELD_1:25
.=
(PolyHom h) . q
by A2, B2, GROUP_4:6
;
q1h *' yh splits_in F2
by Y, F, lemppolspl1;
then
ha * ((PolyHom h) . qq) splits_in F2
by I, lemppolspl2;
hence
(PolyHom h) . p splits_in F2
by A1, FIELD_1:26;
verum end; end; end; hence
S1[
k + 1]
;
verum end;
I:
for k being Nat st 1 <= k holds
S1[k]
from NAT_1:sch 8(IA, IS);
consider n being Nat such that
H:
n = deg p
;
n > 0
by H, RING_4:def 4;
then
n >= 1
by NAT_1:14;
hence
(PolyHom h) . p splits_in F2
by AS, H, I; verum