let R, R1 be commutative Ring; :: thesis: for f being Function of R,R1
for u being Unit of R
for v being Element of R st f is RingHomomorphism holds
( f . u is Unit of R1 & (f . u) ["] = f . (u ["]) )
let f be Function of R,R1; :: thesis: for u being Unit of R
for v being Element of R st f is RingHomomorphism holds
( f . u is Unit of R1 & (f . u) ["] = f . (u ["]) )
let u be Unit of R; :: thesis: for v being Element of R st f is RingHomomorphism holds
( f . u is Unit of R1 & (f . u) ["] = f . (u ["]) )
let v be Element of R; :: thesis: ( f is RingHomomorphism implies ( f . u is Unit of R1 & (f . u) ["] = f . (u ["]) ) )
assume A1: f is RingHomomorphism ; :: thesis: ( f . u is Unit of R1 & (f . u) ["] = f . (u ["]) )
then A3: f is multiplicative ;
A2: u in Unit_Set R ;
f is unity-preserving by A1;
then A5: 1. R1 = f . (u * (u ["])) by A2, Def2
.= (f . u) * (f . (u ["])) by A3 ;
then f . u divides 1. R1 ;
then A7: f . u is unital ;
then A8: f . u in Unit_Set R1 ;
(f . u) ["] = ((f . u) ["]) * ((f . u) * (f . (u ["]))) by A5
.= (((f . u) ["]) * (f . u)) * (f . (u ["])) by GROUP_1:def 3
.= (1. R1) * (f . (u ["])) by Def2, A8
.= f . (u ["]) ;
hence ( f . u is Unit of R1 & (f . u) ["] = f . (u ["]) ) by A7; :: thesis: verum