let A be non degenerated commutative Ring; :: thesis: for I, q being Ideal of A st q c= I & I is maximal holds
(canHom q) .: I is maximal
let I, q be Ideal of A; :: thesis: ( q c= I & I is maximal implies (canHom q) .: I is maximal )
set M = (canHom q) .: I;
reconsider M = (canHom q) .: I as Ideal of (A / q) by Th19;
assume A1: ( q c= I & I is maximal ) ; :: thesis: (canHom q) .: I is maximal
(canHom q) .: I is maximal
proof
assume not (canHom q) .: I is maximal ; :: thesis: contradiction
per cases then ( not M is proper or not M is quasi-maximal ) ;
suppose not M is proper ; :: thesis: contradiction
then M = [#] (A / q) ;
then [#] A = (canHom q) " M by Th28
.= I by A1, Th25 ;
hence contradiction by A1; :: thesis: verum
end;
suppose not M is quasi-maximal ; :: thesis: contradiction
then consider J being Ideal of (A / q) such that
A6: ( M c= J & J <> M & J is proper ) ;
A7: (canHom q) " M <> (canHom q) " J by Lm2, A6;
A8: (canHom q) " J is proper by A6, Th29;
reconsider I2 = (canHom q) " J as Ideal of A by Th22;
(canHom q) " M = I by Th25, A1;
then consider I0 being Ideal of A such that
I0 = I2 and
A9: ( I c= I0 & I <> I0 & I0 is proper ) by A6, Th27, A7, A8;
not I is quasi-maximal by A9;
hence contradiction by A1; :: thesis: verum
end;
end;
end;
hence (canHom q) .: I is maximal ; :: thesis: verum