let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for p being Polynomial of F st deg p < deg (MinPoly (a,F)) holds
Ext_eval ((Leading-Monomial p),a) in Lin (Base a)
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for p being Polynomial of F st deg p < deg (MinPoly (a,F)) holds
Ext_eval ((Leading-Monomial p),a) in Lin (Base a)
let a be F -algebraic Element of E; :: thesis: for p being Polynomial of F st deg p < deg (MinPoly (a,F)) holds
Ext_eval ((Leading-Monomial p),a) in Lin (Base a)
let p be Polynomial of F; :: thesis: ( deg p < deg (MinPoly (a,F)) implies Ext_eval ((Leading-Monomial p),a) in Lin (Base a) )
assume AS: deg p < deg (MinPoly (a,F)) ; :: thesis: Ext_eval ((Leading-Monomial p),a) in Lin (Base a)
set LMp = Leading-Monomial p;
set V = VecSp ((FAdj (F,{a})),F);
set ma = MinPoly (a,F);
set K = FAdj (F,{a});
H0a: F is Subring of FAdj (F,{a}) by FIELD_4:def 1;
per cases ( p = 0_. F or p <> 0_. F ) ;
suppose J: p = 0_. F ; :: thesis: Ext_eval ((Leading-Monomial p),a) in Lin (Base a)
then I: Leading-Monomial p = p by POLYNOM4:13;
H: Ext_eval (p,a) = 0. E by J, ALGNUM_1:13
.= 0. (FAdj (F,{a})) by dFA
.= 0. (VecSp ((FAdj (F,{a})),F)) by FIELD_4:def 6
.= Sum (ZeroLC (VecSp ((FAdj (F,{a})),F))) by VECTSP_6:15 ;
ZeroLC (VecSp ((FAdj (F,{a})),F)) is Linear_Combination of Base a by VECTSP_6:5;
hence Ext_eval ((Leading-Monomial p),a) in Lin (Base a) by I, H, VECTSP_7:7; :: thesis: verum
end;
suppose J: p <> 0_. F ; :: thesis: Ext_eval ((Leading-Monomial p),a) in Lin (Base a)
then reconsider n = deg p as Element of NAT by FIELD_1:1;
J1: not p is zero by J, UPROOTS:def 5;
defpred S1[ object , object ] means ( ( $1 = a |^ n & $2 = LC p ) or ( $1 <> a |^ n & $2 = 0. F ) );
A: for x being object st x in the carrier of (VecSp ((FAdj (F,{a})),F)) holds
ex y being object st
( y in the carrier of F & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of (VecSp ((FAdj (F,{a})),F)) implies ex y being object st
( y in the carrier of F & S1[x,y] ) )
assume x in the carrier of (VecSp ((FAdj (F,{a})),F)) ; :: thesis: ex y being object st
( y in the carrier of F & S1[x,y] )
per cases ( x = a |^ n or x <> a |^ n ) ;
suppose x = a |^ n ; :: thesis: ex y being object st
( y in the carrier of F & S1[x,y] )
hence ex y being object st
( y in the carrier of F & S1[x,y] ) ; :: thesis: verum
end;
suppose x <> a |^ n ; :: thesis: ex y being object st
( y in the carrier of F & S1[x,y] )
hence ex y being object st
( y in the carrier of F & S1[x,y] ) ; :: thesis: verum
end;
end;
end;
consider l being Function of the carrier of (VecSp ((FAdj (F,{a})),F)), the carrier of F such that
L: for x being object st x in the carrier of (VecSp ((FAdj (F,{a})),F)) holds
S1[x,l . x] from FUNCT_2:sch 1(A);
reconsider l = l as Element of Funcs ( the carrier of (VecSp ((FAdj (F,{a})),F)), the carrier of F) by FUNCT_2:8;
for v being Element of (VecSp ((FAdj (F,{a})),F)) st not v in Base a holds
l . v = 0. F
proof
let v be Element of (VecSp ((FAdj (F,{a})),F)); :: thesis: ( not v in Base a implies l . v = 0. F )
assume not v in Base a ; :: thesis: l . v = 0. F
then v <> a |^ n by AS;
hence l . v = 0. F by L; :: thesis: verum
end;
then reconsider l = l as Linear_Combination of VecSp ((FAdj (F,{a})),F) by VECTSP_6:def 1;
now :: thesis: for o being object st o in Carrier l holds
o in Base a
let o be object ; :: thesis: ( o in Carrier l implies o in Base a )
assume o in Carrier l ; :: thesis: o in Base a
then consider v being Element of (VecSp ((FAdj (F,{a})),F)) such that
A1: ( o = v & l . v <> 0. F ) by VECTSP_6:1;
( v = a |^ n & l . v = LC p ) by L, A1;
hence o in Base a by A1, AS; :: thesis: verum
end;
then Carrier l c= Base a ;
then reconsider l = l as Linear_Combination of Base a by VECTSP_6:def 4;
J5: {a} is Subset of (FAdj (F,{a})) by FAt;
a in {a} by TARSKI:def 1;
then reconsider ak = a as Element of (FAdj (F,{a})) by J5;
J4: FAdj (F,{a}) is Subring of E by FIELD_5:12;
ak |^ n is Element of (FAdj (F,{a})) ;
then A8: a |^ n is Element of (FAdj (F,{a})) by J4, pr5;
then reconsider v = a |^ n as Element of (VecSp ((FAdj (F,{a})),F)) by FIELD_4:def 6;
( the carrier of F c= the carrier of (FAdj (F,{a})) & the carrier of (FAdj (F,{a})) c= the carrier of E ) by H0a, C0SP1:def 3, EC_PF_1:def 1;
then reconsider p0 = LC p as Element of E ;
reconsider a0 = a |^ n as Element of E ;
A3: [(l . v),v] in [: the carrier of F, the carrier of (FAdj (F,{a})):] by A8, ZFMISC_1:def 2;
the carrier of F c= the carrier of (FAdj (F,{a})) by H0a, C0SP1:def 3;
then LC p in the carrier of (FAdj (F,{a})) ;
then A4: [p0,a0] in [: the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{a})):] by A8, ZFMISC_1:def 2;
A9: Carrier l = {v}
proof
Y: now :: thesis: for o being object st o in Carrier l holds
o in {v}
let o be object ; :: thesis: ( o in Carrier l implies o in {v} )
assume o in Carrier l ; :: thesis: o in {v}
then consider w being Element of (VecSp ((FAdj (F,{a})),F)) such that
A9b: ( o = w & l . w <> 0. F ) by VECTSP_6:1;
o = v by A9b, L;
hence o in {v} by TARSKI:def 1; :: thesis: verum
end;
now :: thesis: for o being object st o in {v} holds
o in Carrier l
let o be object ; :: thesis: ( o in {v} implies o in Carrier l )
assume o in {v} ; :: thesis: o in Carrier l
then A9c: o = v by TARSKI:def 1;
not p is zero by J, UPROOTS:def 5;
then l . v <> 0. F by L;
hence o in Carrier l by A9c, VECTSP_6:1; :: thesis: verum
end;
hence Carrier l = {v} by TARSKI:2, Y; :: thesis: verum
end;
A5: the multF of (FAdj (F,{a})) = the multF of E || the carrier of (FAdj (F,{a})) by EC_PF_1:def 1;
Sum l = (l . v) * v by A9, VECTSP_6:20
.= ( the multF of (FAdj (F,{a})) | [: the carrier of F, the carrier of (FAdj (F,{a})):]) . ((l . v),v) by FIELD_4:def 6
.= the multF of (FAdj (F,{a})) . ((l . v),v) by A3, FUNCT_1:49
.= the multF of (FAdj (F,{a})) . (p0,a0) by L
.= p0 * (a |^ n) by A4, A5, FUNCT_1:49
.= Ext_eval ((Leading-Monomial p),a) by J1, exevalLM ;
hence Ext_eval ((Leading-Monomial p),a) in Lin (Base a) by VECTSP_7:7; :: thesis: verum
end;
end;