let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for x, y being Element of (FAdj (F,{a}))
for p, q being Polynomial of F st x = Ext_eval (p,a) & y = Ext_eval (q,a) holds
( x + y = Ext_eval ((p + q),a) & x * y = Ext_eval ((p *' q),a) )
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for x, y being Element of (FAdj (F,{a}))
for p, q being Polynomial of F st x = Ext_eval (p,a) & y = Ext_eval (q,a) holds
( x + y = Ext_eval ((p + q),a) & x * y = Ext_eval ((p *' q),a) )
let a be F -algebraic Element of E; :: thesis: for x, y being Element of (FAdj (F,{a}))
for p, q being Polynomial of F st x = Ext_eval (p,a) & y = Ext_eval (q,a) holds
( x + y = Ext_eval ((p + q),a) & x * y = Ext_eval ((p *' q),a) )
let x, y be Element of (FAdj (F,{a})); :: thesis: for p, q being Polynomial of F st x = Ext_eval (p,a) & y = Ext_eval (q,a) holds
( x + y = Ext_eval ((p + q),a) & x * y = Ext_eval ((p *' q),a) )
let p, q be Polynomial of F; :: thesis: ( x = Ext_eval (p,a) & y = Ext_eval (q,a) implies ( x + y = Ext_eval ((p + q),a) & x * y = Ext_eval ((p *' q),a) ) )
assume AS: ( x = Ext_eval (p,a) & y = Ext_eval (q,a) ) ; :: thesis: ( x + y = Ext_eval ((p + q),a) & x * y = Ext_eval ((p *' q),a) )
H0: F is Subring of E by FIELD_4:def 1;
x in the carrier of (FAdj (F,{a})) ;
then H1: x in carrierFA {a} by FIELD_6:def 6;
y in the carrier of (FAdj (F,{a})) ;
then y in carrierFA {a} by FIELD_6:def 6;
then H2: [x,y] in [:(carrierFA {a}),(carrierFA {a}):] by H1, ZFMISC_1:def 2;
thus x + y = ( the addF of E || (carrierFA {a})) . (x,y) by FIELD_6:def 6
.= (Ext_eval (p,a)) + (Ext_eval (q,a)) by AS, H2, FUNCT_1:49
.= Ext_eval ((p + q),a) by H0, ALGNUM_1:15 ; :: thesis: x * y = Ext_eval ((p *' q),a)
thus x * y = ( the multF of E || (carrierFA {a})) . (x,y) by FIELD_6:def 6
.= (Ext_eval (p,a)) * (Ext_eval (q,a)) by AS, H2, FUNCT_1:49
.= Ext_eval ((p *' q),a) by H0, ALGNUM_1:20 ; :: thesis: verum