rngringbdlem2

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, 14-Feb-2025)

	Ref	Expression
Hypotheses	rngringbd.r	$⊢ φ \to R \in Rng$
	rngringbd.i	$⊢ φ \to I \in 2Ideal (R)$
	rngringbd.j	$⊢ J = R ↾_{𝑠} I$
	rngringbd.u	$⊢ φ \to J \in Ring$
	rngringbd.q	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
Assertion	rngringbdlem2	$⊢ (φ \land Q \in Ring) \to R \in Ring$

Proof

Step	Hyp	Ref	Expression
1		rngringbd.r	$⊢ φ \to R \in Rng$
2		rngringbd.i	$⊢ φ \to I \in 2Ideal (R)$
3		rngringbd.j	$⊢ J = R ↾_{𝑠} I$
4		rngringbd.u	$⊢ φ \to J \in Ring$
5		rngringbd.q	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
6		eqid	$⊢ Q \times_{𝑠} J = Q \times_{𝑠} J$
7		simpr	$⊢ (φ \land Q \in Ring) \to Q \in Ring$
8	4	adantr	$⊢ (φ \land Q \in Ring) \to J \in Ring$
9	6 7 8	xpsringd	$⊢ (φ \land Q \in Ring) \to Q \times_{𝑠} J \in Ring$
10	1	adantr	$⊢ (φ \land Q \in Ring) \to R \in Rng$
11	2	adantr	$⊢ (φ \land Q \in Ring) \to I \in 2Ideal (R)$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13		eqid	$⊢ \cdot_{R} = \cdot_{R}$
14		eqid	$⊢ 1_{J} = 1_{J}$
15		eqid	$⊢ R ~_{QG} I = R ~_{QG} I$
16		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
17		eqid	$⊢ (x \in {Base}_{R} ⟼ ⟨[x] (R ~_{QG} I), 1_{J} \cdot_{R} x⟩) = (x \in {Base}_{R} ⟼ ⟨[x] (R ~_{QG} I), 1_{J} \cdot_{R} x⟩)$
18	10 11 3 8 12 13 14 15 5 16 6 17	rngqiprngim	$⊢ (φ \land Q \in Ring) \to (x \in {Base}_{R} ⟼ ⟨[x] (R ~_{QG} I), 1_{J} \cdot_{R} x⟩) \in (R RngIsom (Q \times_{𝑠} J))$
19		rngimcnv	$⊢ (x \in {Base}_{R} ⟼ ⟨[x] (R ~_{QG} I), 1_{J} \cdot_{R} x⟩) \in (R RngIsom (Q \times_{𝑠} J)) \to {(x \in {Base}_{R} ⟼ ⟨[x] (R ~_{QG} I), 1_{J} \cdot_{R} x⟩)}^{-1} \in ((Q \times_{𝑠} J) RngIsom R)$
20	18 19	syl	$⊢ (φ \land Q \in Ring) \to {(x \in {Base}_{R} ⟼ ⟨[x] (R ~_{QG} I), 1_{J} \cdot_{R} x⟩)}^{-1} \in ((Q \times_{𝑠} J) RngIsom R)$
21		rngisomring	$⊢ (Q \times_{𝑠} J \in Ring \land R \in Rng \land {(x \in {Base}_{R} ⟼ ⟨[x] (R ~_{QG} I), 1_{J} \cdot_{R} x⟩)}^{-1} \in ((Q \times_{𝑠} J) RngIsom R)) \to R \in Ring$
22	9 10 20 21	syl3anc	$⊢ (φ \land Q \in Ring) \to R \in Ring$

Metamath Proof Explorer

Theorem rngringbdlem2

Proof