Theorem lidl1el

Description: An ideal contains 1 iff it is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Wolf Lammen, 6-Sep-2020)

	Ref	Expression
Hypotheses	lidlcl.u	|- U = ( LIdeal ` R )
	lidlcl.b	|- B = ( Base ` R )
	lidl1el.o	|- .1. = ( 1r ` R )
Assertion	lidl1el	|- ( ( R e. Ring /\ I e. U ) -> ( .1. e. I <-> I = B ) )

Proof

Step	Hyp	Ref	Expression
1		lidlcl.u	|- U = ( LIdeal ` R )
2		lidlcl.b	|- B = ( Base ` R )
3		lidl1el.o	|- .1. = ( 1r ` R )
4	2 1	lidlss	|- ( I e. U -> I C_ B )
5	4	ad2antlr	|- ( ( ( R e. Ring /\ I e. U ) /\ .1. e. I ) -> I C_ B )
6		eqid	|- ( .r ` R ) = ( .r ` R )
7	2 6 3	ringridm	|- ( ( R e. Ring /\ a e. B ) -> ( a ( .r ` R ) .1. ) = a )
8	7	ad2ant2rl	|- ( ( ( R e. Ring /\ I e. U ) /\ ( .1. e. I /\ a e. B ) ) -> ( a ( .r ` R ) .1. ) = a )
9	1 2 6	lidlmcl	|- ( ( ( R e. Ring /\ I e. U ) /\ ( a e. B /\ .1. e. I ) ) -> ( a ( .r ` R ) .1. ) e. I )
10	9	ancom2s	|- ( ( ( R e. Ring /\ I e. U ) /\ ( .1. e. I /\ a e. B ) ) -> ( a ( .r ` R ) .1. ) e. I )
11	8 10	eqeltrrd	|- ( ( ( R e. Ring /\ I e. U ) /\ ( .1. e. I /\ a e. B ) ) -> a e. I )
12	11	expr	|- ( ( ( R e. Ring /\ I e. U ) /\ .1. e. I ) -> ( a e. B -> a e. I ) )
13	12	ssrdv	|- ( ( ( R e. Ring /\ I e. U ) /\ .1. e. I ) -> B C_ I )
14	5 13	eqssd	|- ( ( ( R e. Ring /\ I e. U ) /\ .1. e. I ) -> I = B )
15	14	ex	|- ( ( R e. Ring /\ I e. U ) -> ( .1. e. I -> I = B ) )
16	2 3	ringidcl	|- ( R e. Ring -> .1. e. B )
17	16	adantr	|- ( ( R e. Ring /\ I e. U ) -> .1. e. B )
18		eleq2	|- ( I = B -> ( .1. e. I <-> .1. e. B ) )
19	17 18	syl5ibrcom	|- ( ( R e. Ring /\ I e. U ) -> ( I = B -> .1. e. I ) )
20	15 19	impbid	|- ( ( R e. Ring /\ I e. U ) -> ( .1. e. I <-> I = B ) )