Metamath Proof Explorer

Theorem ring2idlqusb

Description: A non-unital ring is unital if and only if there is a (two-sided) ideal of the ring which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (Contributed by AV, 20-Feb-2025)

		Ref	Expression
	Assertion	ring2idlqusb	$⊢ R \in Rng \to (R \in Ring \leftrightarrow \exists i \in 2Ideal (R) (R ↾_{𝑠} i \in Ring \land R /_{𝑠} (R ~_{QG} i) \in Ring))$

Proof

Step	Hyp	Ref	Expression
1		ring2idlqus	$⊢ R \in Ring \to \exists i \in 2Ideal (R) (R ↾_{𝑠} i \in Ring \land R /_{𝑠} (R ~_{QG} i) \in Ring)$
2		simpll	$⊢ ((R \in Rng \land i \in 2Ideal (R)) \land R ↾_{𝑠} i \in Ring) \to R \in Rng$
3		simplr	$⊢ ((R \in Rng \land i \in 2Ideal (R)) \land R ↾_{𝑠} i \in Ring) \to i \in 2Ideal (R)$
4		eqid	$⊢ R ↾_{𝑠} i = R ↾_{𝑠} i$
5		simpr	$⊢ ((R \in Rng \land i \in 2Ideal (R)) \land R ↾_{𝑠} i \in Ring) \to R ↾_{𝑠} i \in Ring$
6		eqid	$⊢ R /_{𝑠} (R ~_{QG} i) = R /_{𝑠} (R ~_{QG} i)$
7	2 3 4 5 6	rngringbdlem2	$⊢ (((R \in Rng \land i \in 2Ideal (R)) \land R ↾_{𝑠} i \in Ring) \land R /_{𝑠} (R ~_{QG} i) \in Ring) \to R \in Ring$
8	7	expl	$⊢ (R \in Rng \land i \in 2Ideal (R)) \to ((R ↾_{𝑠} i \in Ring \land R /_{𝑠} (R ~_{QG} i) \in Ring) \to R \in Ring)$
9	8	rexlimdva	$⊢ R \in Rng \to (\exists i \in 2Ideal (R) (R ↾_{𝑠} i \in Ring \land R /_{𝑠} (R ~_{QG} i) \in Ring) \to R \in Ring)$
10	1 9	impbid2	$⊢ R \in Rng \to (R \in Ring \leftrightarrow \exists i \in 2Ideal (R) (R ↾_{𝑠} i \in Ring \land R /_{𝑠} (R ~_{QG} i) \in Ring))$