rngqipring1

Description: The ring unity of the product of the quotient with a two-sided ideal and the two-sided ideal, which both are rings. (Contributed by AV, 16-Mar-2025)

	Ref	Expression
Hypotheses	rngqiprngfu.r	$⊢ φ \to R \in Rng$
	rngqiprngfu.i	$⊢ φ \to I \in 2Ideal (R)$
	rngqiprngfu.j	$⊢ J = R ↾_{𝑠} I$
	rngqiprngfu.u	$⊢ φ \to J \in Ring$
	rngqiprngfu.b	$⊢ B = {Base}_{R}$
	rngqiprngfu.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rngqiprngfu.1	$⊢ \underset{˙}{1} = 1_{J}$
	rngqiprngfu.g	$⊢ \underset{˙}{\sim} = R ~_{QG} I$
	rngqiprngfu.q	$⊢ Q = R /_{𝑠} \underset{˙}{\sim}$
	rngqiprngfu.v	$⊢ φ \to Q \in Ring$
	rngqiprngfu.e	$⊢ φ \to E \in 1_{Q}$
	rngqiprngfu.m	$⊢ \underset{˙}{-} = -_{R}$
	rngqiprngfu.a	$⊢ \underset{˙}{+} = +_{R}$
	rngqiprngfu.n	$⊢ U = (E \underset{˙}{-} (\underset{˙}{1} \underset{˙}{\cdot} E)) \underset{˙}{+} \underset{˙}{1}$
	rngqipring1.p	$⊢ P = Q \times_{𝑠} J$
Assertion	rngqipring1	$⊢ φ \to 1_{P} = ⟨[E] \underset{˙}{\sim}, \underset{˙}{1}⟩$

Proof

Step	Hyp	Ref	Expression
1		rngqiprngfu.r	$⊢ φ \to R \in Rng$
2		rngqiprngfu.i	$⊢ φ \to I \in 2Ideal (R)$
3		rngqiprngfu.j	$⊢ J = R ↾_{𝑠} I$
4		rngqiprngfu.u	$⊢ φ \to J \in Ring$
5		rngqiprngfu.b	$⊢ B = {Base}_{R}$
6		rngqiprngfu.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
7		rngqiprngfu.1	$⊢ \underset{˙}{1} = 1_{J}$
8		rngqiprngfu.g	$⊢ \underset{˙}{\sim} = R ~_{QG} I$
9		rngqiprngfu.q	$⊢ Q = R /_{𝑠} \underset{˙}{\sim}$
10		rngqiprngfu.v	$⊢ φ \to Q \in Ring$
11		rngqiprngfu.e	$⊢ φ \to E \in 1_{Q}$
12		rngqiprngfu.m	$⊢ \underset{˙}{-} = -_{R}$
13		rngqiprngfu.a	$⊢ \underset{˙}{+} = +_{R}$
14		rngqiprngfu.n	$⊢ U = (E \underset{˙}{-} (\underset{˙}{1} \underset{˙}{\cdot} E)) \underset{˙}{+} \underset{˙}{1}$
15		rngqipring1.p	$⊢ P = Q \times_{𝑠} J$
16	15 10 4	xpsring1d	$⊢ φ \to 1_{P} = ⟨1_{Q}, 1_{J}⟩$
17	11	adantr	$⊢ (φ \land x \in B) \to E \in 1_{Q}$
18		eleq2	$⊢ 1_{Q} = [x] \underset{˙}{\sim} \to (E \in 1_{Q} \leftrightarrow E \in [x] \underset{˙}{\sim})$
19	18	adantl	$⊢ ((φ \land x \in B) \land 1_{Q} = [x] \underset{˙}{\sim}) \to (E \in 1_{Q} \leftrightarrow E \in [x] \underset{˙}{\sim})$
20		elecg	$⊢ (E \in 1_{Q} \land x \in B) \to (E \in [x] \underset{˙}{\sim} \leftrightarrow x \underset{˙}{\sim} E)$
21	11 20	sylan	$⊢ (φ \land x \in B) \to (E \in [x] \underset{˙}{\sim} \leftrightarrow x \underset{˙}{\sim} E)$
22		ringrng	$⊢ J \in Ring \to J \in Rng$
23	4 22	syl	$⊢ φ \to J \in Rng$
24	3 23	eqeltrrid	$⊢ φ \to R ↾_{𝑠} I \in Rng$
25	1 2 24	rng2idlnsg	$⊢ φ \to I \in NrmSGrp (R)$
26		nsgsubg	$⊢ I \in NrmSGrp (R) \to I \in SubGrp (R)$
27	25 26	syl	$⊢ φ \to I \in SubGrp (R)$
28	27	adantr	$⊢ (φ \land x \in B) \to I \in SubGrp (R)$
29	5 8	eqger	$⊢ I \in SubGrp (R) \to \underset{˙}{\sim} Er B$
30	28 29	syl	$⊢ (φ \land x \in B) \to \underset{˙}{\sim} Er B$
31		simpr	$⊢ (φ \land x \in B) \to x \in B$
32	30 31	erth	$⊢ (φ \land x \in B) \to (x \underset{˙}{\sim} E \leftrightarrow [x] \underset{˙}{\sim} = [E] \underset{˙}{\sim})$
33	32	biimpa	$⊢ ((φ \land x \in B) \land x \underset{˙}{\sim} E) \to [x] \underset{˙}{\sim} = [E] \underset{˙}{\sim}$
34	33	eqcomd	$⊢ ((φ \land x \in B) \land x \underset{˙}{\sim} E) \to [E] \underset{˙}{\sim} = [x] \underset{˙}{\sim}$
35	34	ex	$⊢ (φ \land x \in B) \to (x \underset{˙}{\sim} E \to [E] \underset{˙}{\sim} = [x] \underset{˙}{\sim})$
36	21 35	sylbid	$⊢ (φ \land x \in B) \to (E \in [x] \underset{˙}{\sim} \to [E] \underset{˙}{\sim} = [x] \underset{˙}{\sim})$
37	36	adantr	$⊢ ((φ \land x \in B) \land 1_{Q} = [x] \underset{˙}{\sim}) \to (E \in [x] \underset{˙}{\sim} \to [E] \underset{˙}{\sim} = [x] \underset{˙}{\sim})$
38	19 37	sylbid	$⊢ ((φ \land x \in B) \land 1_{Q} = [x] \underset{˙}{\sim}) \to (E \in 1_{Q} \to [E] \underset{˙}{\sim} = [x] \underset{˙}{\sim})$
39	38	ex	$⊢ (φ \land x \in B) \to (1_{Q} = [x] \underset{˙}{\sim} \to (E \in 1_{Q} \to [E] \underset{˙}{\sim} = [x] \underset{˙}{\sim}))$
40	17 39	mpid	$⊢ (φ \land x \in B) \to (1_{Q} = [x] \underset{˙}{\sim} \to [E] \underset{˙}{\sim} = [x] \underset{˙}{\sim})$
41	40	imp	$⊢ ((φ \land x \in B) \land 1_{Q} = [x] \underset{˙}{\sim}) \to [E] \underset{˙}{\sim} = [x] \underset{˙}{\sim}$
42		simpr	$⊢ ((φ \land x \in B) \land 1_{Q} = [x] \underset{˙}{\sim}) \to 1_{Q} = [x] \underset{˙}{\sim}$
43	41 42	eqtr4d	$⊢ ((φ \land x \in B) \land 1_{Q} = [x] \underset{˙}{\sim}) \to [E] \underset{˙}{\sim} = 1_{Q}$
44	1 2 3 4 5 6 7 8 9 10	rngqiprngfulem1	$⊢ φ \to \exists x \in B 1_{Q} = [x] \underset{˙}{\sim}$
45	43 44	r19.29a	$⊢ φ \to [E] \underset{˙}{\sim} = 1_{Q}$
46	45	eqcomd	$⊢ φ \to 1_{Q} = [E] \underset{˙}{\sim}$
47	7	eqcomi	$⊢ 1_{J} = \underset{˙}{1}$
48	47	a1i	$⊢ φ \to 1_{J} = \underset{˙}{1}$
49	46 48	opeq12d	$⊢ φ \to ⟨1_{Q}, 1_{J}⟩ = ⟨[E] \underset{˙}{\sim}, \underset{˙}{1}⟩$
50	16 49	eqtrd	$⊢ φ \to 1_{P} = ⟨[E] \underset{˙}{\sim}, \underset{˙}{1}⟩$

Metamath Proof Explorer

Theorem rngqipring1

Proof