let F be Field; for E being FieldExtension of F
for p, q being Element of the carrier of (Polynom-Ring F)
for p1, q1 being Element of the carrier of (Polynom-Ring E) st p1 = p & q1 = q holds
p1 gcd q1 = p gcd q
let E be FieldExtension of F; for p, q being Element of the carrier of (Polynom-Ring F)
for p1, q1 being Element of the carrier of (Polynom-Ring E) st p1 = p & q1 = q holds
p1 gcd q1 = p gcd q
let p, q be Element of the carrier of (Polynom-Ring F); for p1, q1 being Element of the carrier of (Polynom-Ring E) st p1 = p & q1 = q holds
p1 gcd q1 = p gcd q
let p1, q1 be Element of the carrier of (Polynom-Ring E); ( p1 = p & q1 = q implies p1 gcd q1 = p gcd q )
assume AS:
( p1 = p & q1 = q )
; p1 gcd q1 = p gcd q
( the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) & p gcd q is Element of the carrier of (Polynom-Ring F) )
by POLYNOM3:def 10, FIELD_4:10;
then reconsider d = p gcd q as Element of the carrier of (Polynom-Ring E) ;
set g = p1 gcd q1;
consider u, v being Element of (Polynom-Ring E) such that
H1:
( u = p1 & v = q1 & p1 gcd q1 = u gcd v )
by RING_4:def 12;
consider x, y being Element of (Polynom-Ring F) such that
H2:
( x = p & y = q & p gcd q = x gcd y )
by RING_4:def 12;
per cases
( ( p = 0_. F & q = 0_. F ) or p <> 0_. F or q <> 0_. F )
;
suppose A:
(
p <> 0_. F or
q <> 0_. F )
;
p1 gcd q1 = p gcd qthen
(
p1 <> 0_. E or
q1 <> 0_. E )
by AS, FIELD_4:12;
then H:
p1 gcd q1 is
monic Element of the
carrier of
(Polynom-Ring E)
by H1, RING_4:def 11;
I:
d is
monic Element of the
carrier of
(Polynom-Ring E)
reconsider d =
d,
g =
p1 gcd q1 as
Element of
(Polynom-Ring E) by POLYNOM3:def 10;
B:
g divides d
proof
consider aF,
bF being
Element of
(Polynom-Ring F) such that B1:
x gcd y = (aF * x) + (bF * y)
by lemgcdh;
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring E)
by FIELD_4:10;
then reconsider aE =
aF,
bE =
bF as
Element of
(Polynom-Ring E) ;
B2:
Polynom-Ring F is
Subring of
Polynom-Ring E
by FIELD_4:def 1;
then
(
aE * u = aF * x &
bE * v = bF * y )
by AS, H1, H2, FIELD_6:16;
then B3:
d = (aE * u) + (bE * v)
by H2, B1, B2, FIELD_6:15;
consider c being
Element of
(Polynom-Ring E) such that B5:
(u gcd v) * c = u
by RING_4:51, GCD_1:def 1;
consider e being
Element of
(Polynom-Ring E) such that B6:
(u gcd v) * e = v
by RING_4:51, GCD_1:def 1;
((aE * c) + (bE * e)) * (u gcd v) =
((aE * c) * (u gcd v)) + ((bE * e) * (u gcd v))
by VECTSP_1:def 3
.=
(aE * u) + ((bE * e) * (u gcd v))
by B5, GROUP_1:def 3
.=
(aE * u) + (bE * v)
by B6, GROUP_1:def 3
;
hence
g divides d
by B3, H1, GCD_1:def 1;
verum
end; C:
d divides g
proof
reconsider d1 =
d as
Polynomial of
E ;
reconsider w =
p gcd q as
Polynomial of
F ;
consider r being
Polynomial of
F such that C2:
w *' r = p
by RING_4:52, RING_4:1;
reconsider rE =
r as
Polynomial of
E by FIELD_4:8;
rE is
Element of the
carrier of
(Polynom-Ring E)
by POLYNOM3:def 10;
then reconsider rX =
r as
Element of
(Polynom-Ring E) ;
d * rX =
d1 *' rE
by POLYNOM3:def 10
.=
u
by AS, C2, H1, FIELD_4:17
;
then C3:
d divides u
by GCD_1:def 1;
consider r being
Polynomial of
F such that C4:
w *' r = q
by RING_4:52, RING_4:1;
reconsider rE =
r as
Polynomial of
E by FIELD_4:8;
rE is
Element of the
carrier of
(Polynom-Ring E)
by POLYNOM3:def 10;
then reconsider rX =
r as
Element of
(Polynom-Ring E) ;
d * rX =
d1 *' rE
by POLYNOM3:def 10
.=
v
by AS, C4, H1, FIELD_4:17
;
then
d divides v
by GCD_1:def 1;
hence
d divides g
by H1, C3, RING_4:51;
verum
end; thus
p1 gcd q1 = p gcd q
by I, H, C, B, GCD_1:def 3, RING_4:30;
verum end;