let F be Field; :: thesis: for E being FieldExtension of F
for a being non zero Element of F
for b being non zero Element of E
for p being Ppoly of F
for q being Ppoly of E st a * p = b * q holds
( a = b & p = q )
let E be FieldExtension of F; :: thesis: for a being non zero Element of F
for b being non zero Element of E
for p being Ppoly of F
for q being Ppoly of E st a * p = b * q holds
( a = b & p = q )
let a be non zero Element of F; :: thesis: for b being non zero Element of E
for p being Ppoly of F
for q being Ppoly of E st a * p = b * q holds
( a = b & p = q )
let b be non zero Element of E; :: thesis: for p being Ppoly of F
for q being Ppoly of E st a * p = b * q holds
( a = b & p = q )
let p be Ppoly of F; :: thesis: for q being Ppoly of E st a * p = b * q holds
( a = b & p = q )
let q be Ppoly of E; :: thesis: ( a * p = b * q implies ( a = b & p = q ) )
assume AS: a * p = b * q ; :: thesis: ( a = b & p = q )
thus T: b = b * (1. E)
.= b * (LC q) by RING_5:50
.= LC (b * q) by RATFUNC1:18
.= LC (a * p) by AS, lemma2e
.= a * (LC p) by RATFUNC1:18
.= a * (1. F) by RING_5:50
.= a ; :: thesis: p = q
F is Subfield of E by FIELD_4:7;
then the carrier of F c= the carrier of E by EC_PF_1:def 1;
then reconsider a1 = a as Element of E ;
reconsider q1 = p as Ppoly of E by lemmapp;
a1 | E = a | F by FIELD_6:23;
then (a1 | E) *' q1 = (a | F) *' p by FIELD_4:17
.= a * p by poly1 ;
then (a1 | E) *' q1 = (b | E) *' q by AS, poly1;
hence p = q by T, RATFUNC1:7; :: thesis: verum