let A, B be Ring; for i being Function of A,B st i is RingHomomorphism & i = id A holds
A is Subring of B
let i be Function of A,B; ( i is RingHomomorphism & i = id A implies A is Subring of B )
assume A1:
( i is RingHomomorphism & i = id A )
; A is Subring of B
then A2:
i is unity-preserving
;
A3:
for o being object st o in the carrier of A holds
o in the carrier of B
then A6:
the carrier of A c= the carrier of B
;
A7:
the addF of A = the addF of B || the carrier of A
proof
set aA = the
addF of
A;
set aB = the
addF of
B || the
carrier of
A;
A8:
dom ( the addF of B || the carrier of A) =
(dom the addF of B) /\ [: the carrier of A, the carrier of A:]
by RELAT_1:61
.=
[: the carrier of B, the carrier of B:] /\ [: the carrier of A, the carrier of A:]
by FUNCT_2:def 1
.=
[: the carrier of A, the carrier of A:]
by A6, ZFMISC_1:96, XBOOLE_1:28
;
for
x being
object st
x in dom the
addF of
A holds
the
addF of
A . x = ( the addF of B || the carrier of A) . x
proof
let x be
object ;
( x in dom the addF of A implies the addF of A . x = ( the addF of B || the carrier of A) . x )
assume A9:
x in dom the
addF of
A
;
the addF of A . x = ( the addF of B || the carrier of A) . x
then consider a,
b being
object such that A10:
(
a in the
carrier of
A &
b in the
carrier of
A &
x = [a,b] )
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Element of
A by A10;
reconsider a1 =
a,
b1 =
b as
Element of
B by A3;
A11:
i . a = a
by A1;
A12:
i . b = b
by A1;
the
addF of
A . x =
i . (a + b)
by A1, A10
.=
a1 + b1
by A11, A12, A1, VECTSP_1:def 20
.=
( the addF of B || the carrier of A) . x
by A9, A10, FUNCT_1:49
;
hence
the
addF of
A . x = ( the addF of B || the carrier of A) . x
;
verum
end;
hence
the
addF of
A = the
addF of
B || the
carrier of
A
by A8, FUNCT_2:def 1;
verum
end;
A13:
the multF of A = the multF of B || the carrier of A
0. B =
i . (0. A)
by A1, RING_2:6
.=
0. A
by A1
;
hence
A is Subring of B
by A1, A2, A6, A7, A13, C0SP1:def 3; verum