This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
lidlcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
lidl1el.o ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion lidl1el ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 1 ∈ 𝐼 ↔ 𝐼 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 lidlcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 lidlcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 lidl1el.o ⊢ 1 = ( 1r ‘ 𝑅 )
4 2 1 lidlss ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ 𝐵 )
5 4 ad2antlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ 1 ∈ 𝐼 ) → 𝐼 ⊆ 𝐵 )
6 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7 2 6 3 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 ( .r ‘ 𝑅 ) 1 ) = 𝑎 )
8 7 ad2ant2rl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 1 ∈ 𝐼 ∧ 𝑎 ∈ 𝐵 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 1 ) = 𝑎 )
9 1 2 6 lidlmcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 1 ∈ 𝐼 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 1 ) ∈ 𝐼 )
10 9 ancom2s ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 1 ∈ 𝐼 ∧ 𝑎 ∈ 𝐵 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 1 ) ∈ 𝐼 )
11 8 10 eqeltrrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 1 ∈ 𝐼 ∧ 𝑎 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐼 )
12 11 expr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ 1 ∈ 𝐼 ) → ( 𝑎 ∈ 𝐵 → 𝑎 ∈ 𝐼 ) )
13 12 ssrdv ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ 1 ∈ 𝐼 ) → 𝐵 ⊆ 𝐼 )
14 5 13 eqssd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ 1 ∈ 𝐼 ) → 𝐼 = 𝐵 )
15 14 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 1 ∈ 𝐼 → 𝐼 = 𝐵 ) )
16 2 3 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
17 16 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 1 ∈ 𝐵 )
18 eleq2 ⊢ ( 𝐼 = 𝐵 → ( 1 ∈ 𝐼 ↔ 1 ∈ 𝐵 ) )
19 17 18 syl5ibrcom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 𝐼 = 𝐵 → 1 ∈ 𝐼 ) )
20 15 19 impbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 1 ∈ 𝐼 ↔ 𝐼 = 𝐵 ) )