ring2idlqus1

Description: If a non-unital ring has a (two-sided) ideal which is unital, and the quotient of the ring and the ideal is also unital, then the ring is also unital with a ring unity which can be constructed from the ring unity of the ideal and a representative of the ring unity of the quotient. (Contributed by AV, 17-Mar-2025)

	Ref	Expression
Hypotheses	ring2idlqus1.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ring2idlqus1.1	$⊢ \underset{˙}{1} = 1_{(R ↾_{𝑠} I)}$
	ring2idlqus1.m	$⊢ \underset{˙}{-} = -_{R}$
	ring2idlqus1.a	$⊢ \underset{˙}{+} = +_{R}$
Assertion	ring2idlqus1	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \land U \in 1_{(R /_{𝑠} (R ~_{QG} I))}) \to (R \in Ring \land 1_{R} = (U \underset{˙}{-} (\underset{˙}{1} \underset{˙}{\cdot} U)) \underset{˙}{+} \underset{˙}{1})$

Proof

Step	Hyp	Ref	Expression
1		ring2idlqus1.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
2		ring2idlqus1.1	$⊢ \underset{˙}{1} = 1_{(R ↾_{𝑠} I)}$
3		ring2idlqus1.m	$⊢ \underset{˙}{-} = -_{R}$
4		ring2idlqus1.a	$⊢ \underset{˙}{+} = +_{R}$
5		simpr	$⊢ (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \to R /_{𝑠} (R ~_{QG} I) \in Ring$
6	5	adantl	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring)) \to R /_{𝑠} (R ~_{QG} I) \in Ring$
7	6	ancli	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring)) \to (((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring)) \land R /_{𝑠} (R ~_{QG} I) \in Ring)$
8	7	3adant3	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \land U \in 1_{(R /_{𝑠} (R ~_{QG} I))}) \to (((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring)) \land R /_{𝑠} (R ~_{QG} I) \in Ring)$
9		simpl	$⊢ (R \in Rng \land I \in 2Ideal (R)) \to R \in Rng$
10	9	adantr	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring)) \to R \in Rng$
11		simpr	$⊢ (R \in Rng \land I \in 2Ideal (R)) \to I \in 2Ideal (R)$
12	11	adantr	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring)) \to I \in 2Ideal (R)$
13		eqid	$⊢ R ↾_{𝑠} I = R ↾_{𝑠} I$
14		simpl	$⊢ (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \to R ↾_{𝑠} I \in Ring$
15	14	adantl	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring)) \to R ↾_{𝑠} I \in Ring$
16		eqid	$⊢ R /_{𝑠} (R ~_{QG} I) = R /_{𝑠} (R ~_{QG} I)$
17	10 12 13 15 16	rngringbdlem2	$⊢ (((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring)) \land R /_{𝑠} (R ~_{QG} I) \in Ring) \to R \in Ring$
18	8 17	syl	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \land U \in 1_{(R /_{𝑠} (R ~_{QG} I))}) \to R \in Ring$
19	9	3ad2ant1	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \land U \in 1_{(R /_{𝑠} (R ~_{QG} I))}) \to R \in Rng$
20	11	3ad2ant1	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \land U \in 1_{(R /_{𝑠} (R ~_{QG} I))}) \to I \in 2Ideal (R)$
21		simp2l	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \land U \in 1_{(R /_{𝑠} (R ~_{QG} I))}) \to R ↾_{𝑠} I \in Ring$
22		eqid	$⊢ {Base}_{R} = {Base}_{R}$
23		eqid	$⊢ R ~_{QG} I = R ~_{QG} I$
24	6	3adant3	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \land U \in 1_{(R /_{𝑠} (R ~_{QG} I))}) \to R /_{𝑠} (R ~_{QG} I) \in Ring$
25		simp3	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \land U \in 1_{(R /_{𝑠} (R ~_{QG} I))}) \to U \in 1_{(R /_{𝑠} (R ~_{QG} I))}$
26		eqid	$⊢ (U \underset{˙}{-} (\underset{˙}{1} \underset{˙}{\cdot} U)) \underset{˙}{+} \underset{˙}{1} = (U \underset{˙}{-} (\underset{˙}{1} \underset{˙}{\cdot} U)) \underset{˙}{+} \underset{˙}{1}$
27	19 20 13 21 22 1 2 23 16 24 25 3 4 26	rngqiprngu	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \land U \in 1_{(R /_{𝑠} (R ~_{QG} I))}) \to 1_{R} = (U \underset{˙}{-} (\underset{˙}{1} \underset{˙}{\cdot} U)) \underset{˙}{+} \underset{˙}{1}$
28	18 27	jca	$⊢ ((R \in Rng \land I \in 2Ideal (R)) \land (R ↾_{𝑠} I \in Ring \land R /_{𝑠} (R ~_{QG} I) \in Ring) \land U \in 1_{(R /_{𝑠} (R ~_{QG} I))}) \to (R \in Ring \land 1_{R} = (U \underset{˙}{-} (\underset{˙}{1} \underset{˙}{\cdot} U)) \underset{˙}{+} \underset{˙}{1})$

Metamath Proof Explorer

Theorem ring2idlqus1

Proof