Metamath Proof Explorer

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=BaseR
lidl1el.o ⊢1˙=1R
Assertion lidl1el ⊢R∈Ring∧I∈U→1˙∈I↔I=B

Proof

Step Hyp Ref Expression
1 lidlcl.u ⊢U=LIdeal⁡R
2 lidlcl.b ⊢B=BaseR
3 lidl1el.o ⊢1˙=1R
4 2 1 lidlss ⊢I∈U→I⊆B
5 4 ad2antlr ⊢R∈Ring∧I∈U∧1˙∈I→I⊆B
6 eqid ⊢⋅R=⋅R
7 2 6 3 ringridm ⊢R∈Ring∧a∈B→a⋅R1˙=a
8 7 ad2ant2rl ⊢R∈Ring∧I∈U∧1˙∈I∧a∈B→a⋅R1˙=a
9 1 2 6 lidlmcl ⊢R∈Ring∧I∈U∧a∈B∧1˙∈I→a⋅R1˙∈I
10 9 ancom2s ⊢R∈Ring∧I∈U∧1˙∈I∧a∈B→a⋅R1˙∈I
11 8 10 eqeltrrd ⊢R∈Ring∧I∈U∧1˙∈I∧a∈B→a∈I
12 11 expr ⊢R∈Ring∧I∈U∧1˙∈I→a∈B→a∈I
13 12 ssrdv ⊢R∈Ring∧I∈U∧1˙∈I→B⊆I
14 5 13 eqssd ⊢R∈Ring∧I∈U∧1˙∈I→I=B
15 14 ex ⊢R∈Ring∧I∈U→1˙∈I→I=B
16 2 3 ringidcl ⊢R∈Ring→1˙∈B
17 16 adantr ⊢R∈Ring∧I∈U→1˙∈B
18 eleq2 ⊢I=B→1˙∈I↔1˙∈B
19 17 18 syl5ibrcom ⊢R∈Ring∧I∈U→I=B→1˙∈I
20 15 19 impbid ⊢R∈Ring∧I∈U→1˙∈I↔I=B