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	⊢ ( 𝜑 → 𝐼 = 𝐵 )