lidlunitel

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

Step	Hyp	Ref	Expression
1		lidlunitel.1	$⊢ B = {Base}_{R}$
2		lidlunitel.2	$⊢ U = Unit (R)$
3		lidlunitel.3	$⊢ φ \to J \in U$
4		lidlunitel.4	$⊢ φ \to J \in I$
5		lidlunitel.5	$⊢ φ \to R \in Ring$
6		lidlunitel.6	$⊢ φ \to I \in LIdeal (R)$
7		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
8		eqid	$⊢ \cdot_{R} = \cdot_{R}$
9		eqid	$⊢ 1_{R} = 1_{R}$
10	2 7 8 9	unitlinv	$⊢ (R \in Ring \land J \in U) \to {inv}_{r} (R) (J) \cdot_{R} J = 1_{R}$
11	5 3 10	syl2anc	$⊢ φ \to {inv}_{r} (R) (J) \cdot_{R} J = 1_{R}$
12	1 2	unitss	$⊢ U \subseteq B$
13	2 7	unitinvcl	$⊢ (R \in Ring \land J \in U) \to {inv}_{r} (R) (J) \in U$
14	5 3 13	syl2anc	$⊢ φ \to {inv}_{r} (R) (J) \in U$
15	12 14	sselid	$⊢ φ \to {inv}_{r} (R) (J) \in B$
16		eqid	$⊢ LIdeal (R) = LIdeal (R)$
17	16 1 8	lidlmcl	$⊢ ((R \in Ring \land I \in LIdeal (R)) \land ({inv}_{r} (R) (J) \in B \land J \in I)) \to {inv}_{r} (R) (J) \cdot_{R} J \in I$
18	5 6 15 4 17	syl22anc	$⊢ φ \to {inv}_{r} (R) (J) \cdot_{R} J \in I$
19	11 18	eqeltrrd	$⊢ φ \to 1_{R} \in I$
20	16 1 9	lidl1el	$⊢ (R \in Ring \land I \in LIdeal (R)) \to (1_{R} \in I \leftrightarrow I = B)$
21	20	biimpa	$⊢ ((R \in Ring \land I \in LIdeal (R)) \land 1_{R} \in I) \to I = B$
22	5 6 19 21	syl21anc	$⊢ φ \to I = B$

Metamath Proof Explorer