let E, F be Field; :: thesis: for f being additive multiplicative Function of E,F holds
( ( f . (1. E) = 0. F & f = E --> (0. F) ) or ( f . (1. E) = 1. F & f is monomorphism ) )
let f be additive multiplicative Function of E,F; :: thesis: ( ( f . (1. E) = 0. F & f = E --> (0. F) ) or ( f . (1. E) = 1. F & f is monomorphism ) )
per cases ( f . (1. E) = 0. F or f . (1. E) = 1. F ) by hom2;
suppose A: f . (1. E) = 0. F ; :: thesis: ( ( f . (1. E) = 0. F & f = E --> (0. F) ) or ( f . (1. E) = 1. F & f is monomorphism ) )
B: dom f = the carrier of E by FUNCT_2:def 1;
now :: thesis: for z being object st z in dom f holds
f . z = 0. F
let z be object ; :: thesis: ( z in dom f implies f . z = 0. F )
assume z in dom f ; :: thesis: f . z = 0. F
then reconsider x = z as Element of E ;
f . x = f . (x * (1. E))
.= (f . x) * (f . (1. E)) by GROUP_6:def 6
.= 0. F by A ;
hence f . z = 0. F ; :: thesis: verum
end;
hence ( ( f . (1. E) = 0. F & f = E --> (0. F) ) or ( f . (1. E) = 1. F & f is monomorphism ) ) by B, FUNCOP_1:11; :: thesis: verum
end;
suppose A: f . (1. E) = 1. F ; :: thesis: ( ( f . (1. E) = 0. F & f = E --> (0. F) ) or ( f . (1. E) = 1. F & f is monomorphism ) )
then B: f is unity-preserving ;
H: now :: thesis: for x being Element of E st x <> 0. E holds
f . x <> 0. F
let x be Element of E; :: thesis: ( x <> 0. E implies f . x <> 0. F )
assume x <> 0. E ; :: thesis: f . x <> 0. F
then 1. F = f . (x * (x ")) by A, VECTSP_1:def 10
.= (f . x) * (f . (x ")) by GROUP_6:def 6 ;
hence f . x <> 0. F ; :: thesis: verum
end;
now :: thesis: for x, y being object st x in the carrier of E & y in the carrier of E & f . x = f . y holds
x = y
let x, y be object ; :: thesis: ( x in the carrier of E & y in the carrier of E & f . x = f . y implies x = y )
assume D: ( x in the carrier of E & y in the carrier of E & f . x = f . y ) ; :: thesis: x = y
then reconsider a = x, b = y as Element of E ;
G: a + (b - a) = (a + (- a)) + b by RLVECT_1:def 3
.= (0. E) + b by RLVECT_1:5
.= b ;
then E: f . b = (f . b) + (f . (b - a)) by D, VECTSP_1:def 20;
0. F = (f . b) + (- (f . b)) by RLVECT_1:5
.= (f . (b - a)) + ((f . b) + (- (f . b))) by E, RLVECT_1:def 3
.= (f . (b - a)) + (0. F) by RLVECT_1:5
.= f . (b - a) ;
then b = a + (0. E) by G, H
.= a ;
hence x = y ; :: thesis: verum
end;
then f is one-to-one by FUNCT_2:19;
hence ( ( f . (1. E) = 0. F & f = E --> (0. F) ) or ( f . (1. E) = 1. F & f is monomorphism ) ) by B; :: thesis: verum
end;
end;