rngqiprngfulem2

Description: Lemma 2 for rngqiprngfu (and lemma for rngqiprngu ). (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}$
Assertion	rngqiprngfulem2	$⊢ φ \to E \in B$

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	1 2 3 4 5 6 7 8 9 10	rngqiprngfulem1	$⊢ φ \to \exists x \in B 1_{Q} = [x] \underset{˙}{\sim}$
13	11	adantr	$⊢ (φ \land x \in B) \to E \in 1_{Q}$
14		eleq2	$⊢ 1_{Q} = [x] \underset{˙}{\sim} \to (E \in 1_{Q} \leftrightarrow E \in [x] \underset{˙}{\sim})$
15	14	adantl	$⊢ ((φ \land x \in B) \land 1_{Q} = [x] \underset{˙}{\sim}) \to (E \in 1_{Q} \leftrightarrow E \in [x] \underset{˙}{\sim})$
16		elecg	$⊢ (E \in 1_{Q} \land x \in B) \to (E \in [x] \underset{˙}{\sim} \leftrightarrow x \underset{˙}{\sim} E)$
17	11 16	sylan	$⊢ (φ \land x \in B) \to (E \in [x] \underset{˙}{\sim} \leftrightarrow x \underset{˙}{\sim} E)$
18		rngabl	$⊢ R \in Rng \to R \in Abel$
19	1 18	syl	$⊢ φ \to R \in Abel$
20		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
21	5 20	2idlss	$⊢ I \in 2Ideal (R) \to I \subseteq B$
22	2 21	syl	$⊢ φ \to I \subseteq B$
23	19 22	jca	$⊢ φ \to (R \in Abel \land I \subseteq B)$
24	23	adantr	$⊢ (φ \land x \in B) \to (R \in Abel \land I \subseteq B)$
25		eqid	$⊢ -_{R} = -_{R}$
26	5 25 8	eqgabl	$⊢ (R \in Abel \land I \subseteq B) \to (x \underset{˙}{\sim} E \leftrightarrow (x \in B \land E \in B \land E -_{R} x \in I))$
27	24 26	syl	$⊢ (φ \land x \in B) \to (x \underset{˙}{\sim} E \leftrightarrow (x \in B \land E \in B \land E -_{R} x \in I))$
28		simp2	$⊢ (x \in B \land E \in B \land E -_{R} x \in I) \to E \in B$
29	27 28	syl6bi	$⊢ (φ \land x \in B) \to (x \underset{˙}{\sim} E \to E \in B)$
30	17 29	sylbid	$⊢ (φ \land x \in B) \to (E \in [x] \underset{˙}{\sim} \to E \in B)$
31	30	adantr	$⊢ ((φ \land x \in B) \land 1_{Q} = [x] \underset{˙}{\sim}) \to (E \in [x] \underset{˙}{\sim} \to E \in B)$
32	15 31	sylbid	$⊢ ((φ \land x \in B) \land 1_{Q} = [x] \underset{˙}{\sim}) \to (E \in 1_{Q} \to E \in B)$
33	32	ex	$⊢ (φ \land x \in B) \to (1_{Q} = [x] \underset{˙}{\sim} \to (E \in 1_{Q} \to E \in B))$
34	13 33	mpid	$⊢ (φ \land x \in B) \to (1_{Q} = [x] \underset{˙}{\sim} \to E \in B)$
35	34	rexlimdva	$⊢ φ \to (\exists x \in B 1_{Q} = [x] \underset{˙}{\sim} \to E \in B)$
36	12 35	mpd	$⊢ φ \to E \in B$

Metamath Proof Explorer

Theorem rngqiprngfulem2

Proof