let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A holds
( I ||^ 1 = I & I *' ([#] A) = I )
let I be Ideal of A; :: thesis: ( I ||^ 1 = I & I *' ([#] A) = I )
set f = <*I*>;
A1: ( len <*I*> = 1 & <*I*> . 1 = I ) by FINSEQ_1:40;
A2: for i being Nat st i in dom <*I*> & i + 1 in dom <*I*> holds
<*I*> . (i + 1) = I *' (<*I*> /. i)
proof
let i be Nat; :: thesis: ( i in dom <*I*> & i + 1 in dom <*I*> implies <*I*> . (i + 1) = I *' (<*I*> /. i) )
assume A3: ( i in dom <*I*> & i + 1 in dom <*I*> ) ; :: thesis: <*I*> . (i + 1) = I *' (<*I*> /. i)
dom <*I*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then ( i = 1 & i + 1 = 1 ) by A3, TARSKI:def 1;
hence <*I*> . (i + 1) = I *' (<*I*> /. i) ; :: thesis: verum
end;
I + ([#] A) = [#] A by IDEAL_1:74;
then I, [#] A are_co-prime ;
then I *' ([#] A) = I /\ ([#] A) by IDEAL_1:84
.= I by XBOOLE_1:28 ;
hence ( I ||^ 1 = I & I *' ([#] A) = I ) by A1, A2, Def2; :: thesis: verum