Description: If a (left) ideal (which is not the zero ideal) of a domain has a multiplicative identity element, the identity element is the identity of the domain. (Contributed by AV, 17-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lidldomn1.l | |
|
lidldomn1.t | |
||
lidldomn1.1 | |
||
lidldomn1.0 | |
||
Assertion | lidldomn1 | |