let R be non empty right_unital left_unital doubleLoopStr ; :: thesis: for I being non empty right-ideal Subset of R holds
( I is proper iff for u being Element of R st u is unital holds
not u in I )
let I be non empty right-ideal Subset of R; :: thesis: ( I is proper iff for u being Element of R st u is unital holds
not u in I )
A1: now :: thesis: ( I is proper implies for u being Element of R st u is unital holds
not u in I )
assume A2: I is proper ; :: thesis: for u being Element of R st u is unital holds
not u in I
A3: not 1. R in I
proof
assume A4: 1. R in I ; :: thesis: contradiction
A5: now :: thesis: for u being object st u in the carrier of R holds
u in I
let u be object ; :: thesis: ( u in the carrier of R implies u in I )
assume u in the carrier of R ; :: thesis: u in I
then reconsider u9 = u as Element of R ;
(1. R) * u9 = u9 ;
hence u in I by A4, Def3; :: thesis: verum
end;
for u being object st u in I holds
u in the carrier of R ;
then I = the carrier of R by A5, TARSKI:2;
hence contradiction by A2, SUBSET_1:def 6; :: thesis: verum
end;
thus for u being Element of R st u is unital holds
not u in I :: thesis: verum
proof
let u be Element of R; :: thesis: ( u is unital implies not u in I )
assume u is unital ; :: thesis: not u in I
then u divides 1. R by GCD_1:def 2;
then ex b being Element of R st 1. R = u * b by GCD_1:def 1;
hence not u in I by A3, Def3; :: thesis: verum
end;
end;
now :: thesis: ( ( for u being Element of R st u is unital holds
not u in I ) implies I is proper )
1. R divides 1. R ;
then A6: 1. R is unital by GCD_1:def 2;
assume for u being Element of R st u is unital holds
not u in I ; :: thesis: I is proper
then I <> the carrier of R by A6;
hence I is proper by SUBSET_1:def 6; :: thesis: verum
end;
hence ( I is proper iff for u being Element of R st u is unital holds
not u in I ) by A1; :: thesis: verum