let X, X9 be BCI-algebra; for I being Ideal of X
for f being BCI-homomorphism of X,X9 st f is onto holds
f .: I is Ideal of X9
let I be Ideal of X; for f being BCI-homomorphism of X,X9 st f is onto holds
f .: I is Ideal of X9
let f be BCI-homomorphism of X,X9; ( f is onto implies f .: I is Ideal of X9 )
0. X in the carrier of X
;
then A1:
0. X in dom f
by FUNCT_2:def 1;
( 0. X in I & f . (0. X) = 0. X9 )
by Th35, BCIALG_1:def 18;
then reconsider imaf = f .: I as non empty Subset of X9 by A1, FUNCT_1:def 6;
0. X in the carrier of X
;
then A2:
0. X in dom f
by FUNCT_2:def 1;
assume A3:
f is onto
; f .: I is Ideal of X9
A4:
for x, y being Element of X9 st x \ y in imaf & y in imaf holds
x in imaf
proof
let x,
y be
Element of
X9;
( x \ y in imaf & y in imaf implies x in imaf )
assume that A5:
x \ y in imaf
and A6:
y in imaf
;
x in imaf
consider y9 being
object such that A7:
y9 in dom f
and A8:
y9 in I
and A9:
y = f . y9
by A6, FUNCT_1:def 6;
consider yy being
Element of
X such that A10:
f . yy = x
by A3, Th42;
consider z being
object such that A11:
z in dom f
and A12:
z in I
and A13:
x \ y = f . z
by A5, FUNCT_1:def 6;
reconsider y9 =
y9,
z =
z as
Element of
X by A7, A11;
set u =
yy \ ((yy \ y9) \ z);
((yy \ y9) \ ((yy \ y9) \ z)) \ z = 0. X
by BCIALG_1:1;
then
((yy \ ((yy \ y9) \ z)) \ y9) \ z = 0. X
by BCIALG_1:7;
then
((yy \ ((yy \ y9) \ z)) \ y9) \ z in I
by BCIALG_1:def 18;
then
(yy \ ((yy \ y9) \ z)) \ y9 in I
by A12, BCIALG_1:def 18;
then A14:
yy \ ((yy \ y9) \ z) in I
by A8, BCIALG_1:def 18;
yy \ ((yy \ y9) \ z) in the
carrier of
X
;
then
yy \ ((yy \ y9) \ z) in dom f
by FUNCT_2:def 1;
then
[(yy \ ((yy \ y9) \ z)),(f . (yy \ ((yy \ y9) \ z)))] in f
by FUNCT_1:1;
then
f . (yy \ ((yy \ y9) \ z)) in f .: I
by A14, RELAT_1:def 13;
then
(f . yy) \ (f . ((yy \ y9) \ z)) in f .: I
by Def6;
then
(f . yy) \ ((f . (yy \ y9)) \ (f . z)) in f .: I
by Def6;
then
(f . yy) \ ((x \ y) \ (x \ y)) in f .: I
by A9, A13, A10, Def6;
then
(f . yy) \ (0. X9) in f .: I
by BCIALG_1:def 5;
hence
x in imaf
by A10, BCIALG_1:2;
verum
end;
( 0. X in I & f . (0. X) = 0. X9 )
by Th35, BCIALG_1:def 18;
then
0. X9 in imaf
by A2, FUNCT_1:def 6;
hence
f .: I is Ideal of X9
by A4, BCIALG_1:def 18; verum