let I be non degenerated commutative domRing-like Ring; canHom I is embedding
A1:
0. I <> 1. I
;
for x1, x2 being object st x1 in dom (canHom I) & x2 in dom (canHom I) & (canHom I) . x1 = (canHom I) . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom (canHom I) & x2 in dom (canHom I) & (canHom I) . x1 = (canHom I) . x2 implies x1 = x2 )
assume that A2:
(
x1 in dom (canHom I) &
x2 in dom (canHom I) )
and A3:
(canHom I) . x1 = (canHom I) . x2
;
x1 = x2
reconsider x1 =
x1,
x2 =
x2 as
Element of
I by A2;
reconsider t1 =
quotient (
x1,
(1. I)),
t2 =
quotient (
x2,
(1. I)) as
Element of
Q. I ;
A4:
t1 in QClass. t1
by Th5;
QClass. t1 =
(canHom I) . x2
by A3, Def21
.=
QClass. t2
by Def21
;
then A5:
(t1 `1) * (t2 `2) = (t1 `2) * (t2 `1)
by A4, Def4;
A6:
t1 `2 =
[x1,(1. I)] `2
by A1, Def20
.=
1. I
;
A7:
t1 `1 =
[x1,(1. I)] `1
by A1, Def20
.=
x1
;
A8:
t2 `1 =
[x2,(1. I)] `1
by A1, Def20
.=
x2
;
t2 `2 =
[x2,(1. I)] `2
by A1, Def20
.=
1. I
;
then x1 =
(t1 `2) * (t2 `1)
by A5, A7
.=
x2
by A6, A8
;
hence
x1 = x2
;
verum
end;
then A9:
canHom I is one-to-one
by FUNCT_1:def 4;
canHom I is RingHomomorphism
by Th56;
hence
canHom I is embedding
by A9; verum