let F be non 2 -characteristic polynomial_disjoint non quadratic_complete Field; :: thesis: for a being non square Element of F
for a1, a2, b1, b2 being F -membered Element of (FAdj (F,{(sqrt a)})) st a1 + ((@ (sqrt a)) * b1) = a2 + ((@ (sqrt a)) * b2) holds
( a1 = a2 & b1 = b2 )
let a be non square Element of F; :: thesis: for a1, a2, b1, b2 being F -membered Element of (FAdj (F,{(sqrt a)})) st a1 + ((@ (sqrt a)) * b1) = a2 + ((@ (sqrt a)) * b2) holds
( a1 = a2 & b1 = b2 )
let a1, a2, b1, b2 be F -membered Element of (FAdj (F,{(sqrt a)})); :: thesis: ( a1 + ((@ (sqrt a)) * b1) = a2 + ((@ (sqrt a)) * b2) implies ( a1 = a2 & b1 = b2 ) )
set E = FAdj (F,{(sqrt a)});
set j = @ (sqrt a);
set V = VecSp ((FAdj (F,{(sqrt a)})),F);
assume a1 + ((@ (sqrt a)) * b1) = a2 + ((@ (sqrt a)) * b2) ; :: thesis: ( a1 = a2 & b1 = b2 )
then AS: 0. (FAdj (F,{(sqrt a)})) = (a1 + ((@ (sqrt a)) * b1)) - (a2 + ((@ (sqrt a)) * b2)) by RLVECT_1:15
.= (a1 + ((@ (sqrt a)) * b1)) + ((- a2) + (- ((@ (sqrt a)) * b2))) by RLVECT_1:31
.= (a1 + ((@ (sqrt a)) * b1)) + ((- a2) + ((@ (sqrt a)) * (- b2))) by VECTSP_1:8
.= ((@ (sqrt a)) * b1) + (a1 + ((- a2) + ((@ (sqrt a)) * (- b2)))) by RLVECT_1:def 3
.= ((@ (sqrt a)) * b1) + ((a1 + (- a2)) + ((@ (sqrt a)) * (- b2))) by RLVECT_1:def 3
.= (((@ (sqrt a)) * b1) + ((@ (sqrt a)) * (- b2))) + (a1 + (- a2)) by RLVECT_1:def 3
.= (a1 - a2) + ((@ (sqrt a)) * (b1 - b2)) by VECTSP_1:def 2 ;
reconsider 1V = 1. (FAdj (F,{(sqrt a)})), jV = @ (sqrt a) as Element of (VecSp ((FAdj (F,{(sqrt a)})),F)) by FIELD_4:def 6;
reconsider a1R = a1, a2R = a2, b1R = b1, b2R = b2 as Element of F by FIELD_7:def 5;
I0: F is Subring of FAdj (F,{(sqrt a)}) by FIELD_4:def 1;
then ( - a2 = - a2R & - b2 = - b2R ) by FIELD_6:17;
then I1: ( a1 - a2 = a1R - a2R & b1 - b2 = b1R - b2R ) by I0, FIELD_6:15;
defpred S1[ object , object ] means ( ( $1 = 1. (FAdj (F,{(sqrt a)})) & $2 = a1 - a2 ) or ( $1 = @ (sqrt a) & $2 = b1 - b2 ) or ( $1 <> 1. (FAdj (F,{(sqrt a)})) & $1 <> @ (sqrt a) & $2 = 0. F ) );
A: for x being object st x in the carrier of (VecSp ((FAdj (F,{(sqrt 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,{(sqrt 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,{(sqrt a)})),F)) ; :: thesis: ex y being object st
( y in the carrier of F & S1[x,y] )
per cases ( x = 1. (FAdj (F,{(sqrt a)})) or x = @ (sqrt a) or ( x <> 1. (FAdj (F,{(sqrt a)})) & x <> @ (sqrt a) ) ) ;
suppose x = 1. (FAdj (F,{(sqrt 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 = @ (sqrt 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,{(sqrt a)})) & x <> @ (sqrt 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,{(sqrt a)})),F)), the carrier of F such that
L: for x being object st x in the carrier of (VecSp ((FAdj (F,{(sqrt 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,{(sqrt a)})),F)), the carrier of F) by FUNCT_2:8;
for v being Element of (VecSp ((FAdj (F,{(sqrt a)})),F)) st not v in {1V,jV} holds
l . v = 0. F
proof
let v be Element of (VecSp ((FAdj (F,{(sqrt 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,{(sqrt a)})) & v <> @ (sqrt 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,{(sqrt 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,{(sqrt a)})),F)) such that
A1: ( o = v & l . v <> 0. F ) by VECTSP_6:1;
( ( v = 1. (FAdj (F,{(sqrt a)})) & l . v = a1 - a2 ) or ( v = @ (sqrt a) & l . v = b1 - b2 ) ) 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;
1. (FAdj (F,{(sqrt a)})) = 1. F by I0, C0SP1:def 3;
then I3: 1V <> jV by FIELD_7:def 5;
{(1. F),(sqrt a)} = {1V,jV} by I0, C0SP1:def 3;
then I2: {1V,jV} is linearly-independent by qbase4;
I8: [(a1 - a2),(1. (FAdj (F,{(sqrt a)})))] in [: the carrier of F, the carrier of (FAdj (F,{(sqrt a)})):] by I1, ZFMISC_1:def 2;
I6: (l . 1V) * 1V = ( the multF of (FAdj (F,{(sqrt a)})) | [: the carrier of F, the carrier of (FAdj (F,{(sqrt a)})):]) . ((l . 1V),(1. (FAdj (F,{(sqrt a)})))) by FIELD_4:def 6
.= ( the multF of (FAdj (F,{(sqrt a)})) | [: the carrier of F, the carrier of (FAdj (F,{(sqrt a)})):]) . ((a1 - a2),(1. (FAdj (F,{(sqrt a)})))) by I3, L
.= (a1 - a2) * (1. (FAdj (F,{(sqrt a)}))) by I8, FUNCT_1:49 ;
I8: [(b1 - b2),(@ (sqrt a))] in [: the carrier of F, the carrier of (FAdj (F,{(sqrt a)})):] by I1, ZFMISC_1:def 2;
I7: (l . jV) * jV = ( the multF of (FAdj (F,{(sqrt a)})) | [: the carrier of F, the carrier of (FAdj (F,{(sqrt a)})):]) . ((l . jV),(@ (sqrt a))) by FIELD_4:def 6
.= ( the multF of (FAdj (F,{(sqrt a)})) | [: the carrier of F, the carrier of (FAdj (F,{(sqrt a)})):]) . ((b1 - b2),(@ (sqrt a))) by I3, L
.= (b1 - b2) * (@ (sqrt a)) by I8, FUNCT_1:49
.= (@ (sqrt a)) * (b1 - b2) by GROUP_1:def 12 ;
((l . 1V) * 1V) + ((l . jV) * jV) = the addF of (FAdj (F,{(sqrt a)})) . ((a1 - a2),((@ (sqrt a)) * (b1 - b2))) by I6, I7, FIELD_4:def 6
.= 0. (VecSp ((FAdj (F,{(sqrt a)})),F)) by AS, FIELD_4:def 6 ;
then I5: ( l . 1V = 0. F & l . jV = 0. F ) by I2, I3, VECTSP_7:6;
l . 1V = a1 - a2 by I3, L;
then a1 - a2 = 0. (FAdj (F,{(sqrt a)})) by I5, I0, C0SP1:def 3;
hence a1 = a2 by RLVECT_1:21; :: thesis: b1 = b2
l . jV = b1 - b2 by I3, L;
then b1 - b2 = 0. (FAdj (F,{(sqrt a)})) by I5, I0, C0SP1:def 3;
hence b1 = b2 by RLVECT_1:21; :: thesis: verum