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

Metamath Proof Explorer

Theorem lidlunitel

Description: If an ideal I contains a unit J , then it is the whole ring. (Contributed by Thierry Arnoux, 19-Mar-2025)

Ref Expression
Hypotheses lidlunitel.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
lidlunitel.2 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
lidlunitel.3 ⊢ ( 𝜑 → 𝐽 ∈ 𝑈 )
lidlunitel.4 ⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
lidlunitel.5 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
lidlunitel.6 ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
Assertion lidlunitel ( 𝜑 → 𝐼 = 𝐵 )

Proof

Step Hyp Ref Expression
1 lidlunitel.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 lidlunitel.2 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 lidlunitel.3 ⊢ ( 𝜑 → 𝐽 ∈ 𝑈 )
4 lidlunitel.4 ⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
5 lidlunitel.5 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 lidlunitel.6 ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
7 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
8 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10 2 7 8 9 unitlinv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐽 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝐽 ) ( .r ‘ 𝑅 ) 𝐽 ) = ( 1r ‘ 𝑅 ) )
11 5 3 10 syl2anc ⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝐽 ) ( .r ‘ 𝑅 ) 𝐽 ) = ( 1r ‘ 𝑅 ) )
12 1 2 unitss ⊢ 𝑈 ⊆ 𝐵
13 2 7 unitinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐽 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝐽 ) ∈ 𝑈 )
14 5 3 13 syl2anc ⊢ ( 𝜑 → ( ( invr ‘ 𝑅 ) ‘ 𝐽 ) ∈ 𝑈 )
15 12 14 sselid ⊢ ( 𝜑 → ( ( invr ‘ 𝑅 ) ‘ 𝐽 ) ∈ 𝐵 )
16 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
17 16 1 8 lidlmcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( ( invr ‘ 𝑅 ) ‘ 𝐽 ) ∈ 𝐵 ∧ 𝐽 ∈ 𝐼 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝐽 ) ( .r ‘ 𝑅 ) 𝐽 ) ∈ 𝐼 )
18 5 6 15 4 17 syl22anc ⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝐽 ) ( .r ‘ 𝑅 ) 𝐽 ) ∈ 𝐼 )
19 11 18 eqeltrrd ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐼 )
20 16 1 9 lidl1el ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ∈ 𝐼 ↔ 𝐼 = 𝐵 ) )
21 20 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐼 ) → 𝐼 = 𝐵 )
22 5 6 19 21 syl21anc ⊢ ( 𝜑 → 𝐼 = 𝐵 )