let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E st not a in F & a ^2 in F holds
for c1, c2, d1, d2 being Element of (FAdj (F,{a})) st c1 in F & c2 in F & d1 in F & d2 in F & c1 + ((@ ((FAdj (F,{a})),a)) * c2) = d1 + ((@ ((FAdj (F,{a})),a)) * d2) holds
( c1 = d1 & c2 = d2 )
let E be FieldExtension of F; :: thesis: for a being Element of E st not a in F & a ^2 in F holds
for c1, c2, d1, d2 being Element of (FAdj (F,{a})) st c1 in F & c2 in F & d1 in F & d2 in F & c1 + ((@ ((FAdj (F,{a})),a)) * c2) = d1 + ((@ ((FAdj (F,{a})),a)) * d2) holds
( c1 = d1 & c2 = d2 )
let a be Element of E; :: thesis: ( not a in F & a ^2 in F implies for c1, c2, d1, d2 being Element of (FAdj (F,{a})) st c1 in F & c2 in F & d1 in F & d2 in F & c1 + ((@ ((FAdj (F,{a})),a)) * c2) = d1 + ((@ ((FAdj (F,{a})),a)) * d2) holds
( c1 = d1 & c2 = d2 ) )
assume AS1: ( not a in F & a ^2 in F ) ; :: thesis: for c1, c2, d1, d2 being Element of (FAdj (F,{a})) st c1 in F & c2 in F & d1 in F & d2 in F & c1 + ((@ ((FAdj (F,{a})),a)) * c2) = d1 + ((@ ((FAdj (F,{a})),a)) * d2) holds
( c1 = d1 & c2 = d2 )
let c1, c2, d1, d2 be Element of (FAdj (F,{a})); :: thesis: ( c1 in F & c2 in F & d1 in F & d2 in F & c1 + ((@ ((FAdj (F,{a})),a)) * c2) = d1 + ((@ ((FAdj (F,{a})),a)) * d2) implies ( c1 = d1 & c2 = d2 ) )
assume AS2: ( c1 in F & c2 in F & d1 in F & d2 in F & c1 + ((@ ((FAdj (F,{a})),a)) * c2) = d1 + ((@ ((FAdj (F,{a})),a)) * d2) ) ; :: thesis: ( c1 = d1 & c2 = d2 )
set K = FAdj (F,{a});
set V = VecSp ((FAdj (F,{a})),F);
set j = @ ((FAdj (F,{a})),a);
A1: 0. (FAdj (F,{a})) = (c1 + ((@ ((FAdj (F,{a})),a)) * c2)) - (d1 + ((@ ((FAdj (F,{a})),a)) * d2)) by AS2, RLVECT_1:15
.= (c1 + ((@ ((FAdj (F,{a})),a)) * c2)) + ((- d1) + (- ((@ ((FAdj (F,{a})),a)) * d2))) by RLVECT_1:31
.= (c1 + ((@ ((FAdj (F,{a})),a)) * c2)) + ((- d1) + ((@ ((FAdj (F,{a})),a)) * (- d2))) by VECTSP_1:8
.= ((@ ((FAdj (F,{a})),a)) * c2) + (c1 + ((- d1) + ((@ ((FAdj (F,{a})),a)) * (- d2)))) by RLVECT_1:def 3
.= ((@ ((FAdj (F,{a})),a)) * c2) + ((c1 + (- d1)) + ((@ ((FAdj (F,{a})),a)) * (- d2))) by RLVECT_1:def 3
.= (((@ ((FAdj (F,{a})),a)) * c2) + ((@ ((FAdj (F,{a})),a)) * (- d2))) + (c1 + (- d1)) by RLVECT_1:def 3
.= (c1 - d1) + ((@ ((FAdj (F,{a})),a)) * (c2 - d2)) by VECTSP_1:def 2 ;
reconsider 1V = 1. (FAdj (F,{a})), jV = @ ((FAdj (F,{a})),a) as Element of (VecSp ((FAdj (F,{a})),F)) by FIELD_4:def 6;
reconsider c1F = c1, c2F = c2, d1F = d1, d2F = d2 as Element of F by AS2;
I0: ( F is Subring of FAdj (F,{a}) & F is Subring of E ) by FIELD_4:def 1;
then ( - d1 = - d1F & - d2 = - d2F ) by FIELD_6:17;
then I1: ( c1 - d1 = c1F - d1F & c2 - d2 = c2F - d2F ) by I0, FIELD_6:15;
defpred S1[ object , object ] means ( ( $1 = 1. (FAdj (F,{a})) & $2 = c1 - d1 ) or ( $1 = @ ((FAdj (F,{a})),a) & $2 = c2 - d2 ) or ( $1 <> 1. (FAdj (F,{a})) & $1 <> @ ((FAdj (F,{a})),a) & $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 = 1. (FAdj (F,{a})) or x = @ ((FAdj (F,{a})),a) or ( x <> 1. (FAdj (F,{a})) & x <> @ ((FAdj (F,{a})),a) ) ) ;
suppose x = 1. (FAdj (F,{a})) ; :: 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] ) by I1; :: thesis: verum
end;
suppose x = @ ((FAdj (F,{a})),a) ; :: 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] ) by I1; :: thesis: verum
end;
suppose ( x <> 1. (FAdj (F,{a})) & x <> @ ((FAdj (F,{a})),a) ) ; :: 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 {1V,jV} holds
l . v = 0. F
proof
let v be Element of (VecSp ((FAdj (F,{a})),F)); :: thesis: ( not v in {1V,jV} implies l . v = 0. F )
assume not v in {1V,jV} ; :: thesis: l . v = 0. F
then ( v <> 1. (FAdj (F,{a})) & v <> @ ((FAdj (F,{a})),a) ) by TARSKI:def 2;
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 {1V,jV}
let o be object ; :: thesis: ( o in Carrier l implies o in {1V,jV} )
assume o in Carrier l ; :: thesis: o in {1V,jV}
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 = 1. (FAdj (F,{a})) & l . v = c1 - d1 ) or ( v = @ ((FAdj (F,{a})),a) & l . v = c2 - d2 ) ) by L, A1;
hence o in {1V,jV} by A1, TARSKI:def 2; :: thesis: verum
end;
then Carrier l c= {1V,jV} ;
then reconsider l = l as Linear_Combination of {1V,jV} by VECTSP_6:def 4;
( a in {a} & {a} is Subset of (FAdj (F,{a})) ) by TARSKI:def 1, FIELD_6:35;
then I8: a is FAdj (F,{a}) -membered ;
I9: 1. (FAdj (F,{a})) = 1. F by I0, C0SP1:def 3
.= 1. E by I0, C0SP1:def 3 ;
1. (FAdj (F,{a})) = 1. F by I0, C0SP1:def 3;
then I3: 1. (FAdj (F,{a})) <> @ ((FAdj (F,{a})),a) by I8, AS1;
I2: {1V,jV} is linearly-independent by I8, I9, AS1, ThBas;
I8: [(c1 - d1),(1. (FAdj (F,{a})))] in [: the carrier of F, the carrier of (FAdj (F,{a})):] by I1, ZFMISC_1:def 2;
I6: (l . 1V) * 1V = ( the multF of (FAdj (F,{a})) | [: the carrier of F, the carrier of (FAdj (F,{a})):]) . ((l . 1V),(1. (FAdj (F,{a})))) by FIELD_4:def 6
.= ( the multF of (FAdj (F,{a})) | [: the carrier of F, the carrier of (FAdj (F,{a})):]) . ((c1 - d1),(1. (FAdj (F,{a})))) by I3, L
.= (c1 - d1) * (1. (FAdj (F,{a}))) by I8, FUNCT_1:49 ;
I8: [(c2 - d2),(@ ((FAdj (F,{a})),a))] in [: the carrier of F, the carrier of (FAdj (F,{a})):] by I1, ZFMISC_1:def 2;
I7: (l . jV) * jV = ( the multF of (FAdj (F,{a})) | [: the carrier of F, the carrier of (FAdj (F,{a})):]) . ((l . jV),(@ ((FAdj (F,{a})),a))) by FIELD_4:def 6
.= ( the multF of (FAdj (F,{a})) | [: the carrier of F, the carrier of (FAdj (F,{a})):]) . ((c2 - d2),(@ ((FAdj (F,{a})),a))) by I3, L
.= (c2 - d2) * (@ ((FAdj (F,{a})),a)) by I8, FUNCT_1:49
.= (@ ((FAdj (F,{a})),a)) * (c2 - d2) ;
((l . 1V) * 1V) + ((l . jV) * jV) = the addF of (FAdj (F,{a})) . (((l . 1V) * 1V),((l . jV) * jV)) by FIELD_4:def 6
.= 0. (VecSp ((FAdj (F,{a})),F)) by A1, I6, I7, FIELD_4:def 6 ;
then I5: ( l . 1V = 0. F & l . jV = 0. F ) by I2, I3, VECTSP_7:6;
l . 1V = c1 - d1 by I3, L;
then c1 - d1 = 0. (FAdj (F,{a})) by I5, I0, C0SP1:def 3;
hence c1 = d1 by RLVECT_1:21; :: thesis: c2 = d2
l . jV = c2 - d2 by I3, L;
then c2 - d2 = 0. (FAdj (F,{a})) by I5, I0, C0SP1:def 3;
hence c2 = d2 by RLVECT_1:21; :: thesis: verum