Theorem rngqiprngfulem2

Description: Lemma 2 for rngqiprngfu (and lemma for rngqiprngu ). (Contributed by AV, 16-Mar-2025)

	Ref	Expression
Hypotheses	rngqiprngfu.r	$$⊢\phi \to R\in \mathrm{Rng}$$
	rngqiprngfu.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rngqiprngfu.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	rngqiprngfu.u	$$⊢\phi \to J\in \mathrm{Ring}$$
	rngqiprngfu.b	$$⊢B={\mathrm{Base}}_R$$
	rngqiprngfu.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rngqiprngfu.1	$$⊢\underset{\dot{}}{1}=1_J$$
	rngqiprngfu.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
	rngqiprngfu.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	rngqiprngfu.v	$$⊢\phi \to Q\in \mathrm{Ring}$$
	rngqiprngfu.e	$$⊢\phi \to E\in 1_Q$$
Assertion	rngqiprngfulem2	$$⊢\phi \to E\in B$$

Proof

Step	Hyp	Ref	Expression
1		rngqiprngfu.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rngqiprngfu.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rngqiprngfu.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
4		rngqiprngfu.u	$$⊢\phi \to J\in \mathrm{Ring}$$
5		rngqiprngfu.b	$$⊢B={\mathrm{Base}}_R$$
6		rngqiprngfu.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
7		rngqiprngfu.1	$$⊢\underset{\dot{}}{1}=1_J$$
8		rngqiprngfu.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
9		rngqiprngfu.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
10		rngqiprngfu.v	$$⊢\phi \to Q\in \mathrm{Ring}$$
11		rngqiprngfu.e	$$⊢\phi \to E\in 1_Q$$
12	1 2 3 4 5 6 7 8 9 10	rngqiprngfulem1	$$⊢\phi \to \exists x\in B{1}_Q=\left[x\right]\underset{\dot{}}{\sim }$$
13	11	adantr	$$⊢\left(\phi \wedge x\in B\right)\to E\in 1_Q$$
14		eleq2	$$⊢1_Q=\left[x\right]\underset{\dot{}}{\sim }\to \left(E\in 1_Q\leftrightarrow E\in \left[x\right]\underset{\dot{}}{\sim }\right)$$
15	14	adantl	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge 1_Q=\left[x\right]\underset{\dot{}}{\sim }\right)\to \left(E\in 1_Q\leftrightarrow E\in \left[x\right]\underset{\dot{}}{\sim }\right)$$
16		elecg	$$⊢\left(E\in 1_Q\wedge x\in B\right)\to \left(E\in \left[x\right]\underset{\dot{}}{\sim }\leftrightarrow x\underset{\dot{}}{\sim }E\right)$$
17	11 16	sylan	$$⊢\left(\phi \wedge x\in B\right)\to \left(E\in \left[x\right]\underset{\dot{}}{\sim }\leftrightarrow x\underset{\dot{}}{\sim }E\right)$$
18		rngabl	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Abel}$$
19	1 18	syl	$$⊢\phi \to R\in \mathrm{Abel}$$
20		eqid	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
21	5 20	2idlss	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to I\subseteq B$$
22	2 21	syl	$$⊢\phi \to I\subseteq B$$
23	19 22	jca	$$⊢\phi \to \left(R\in \mathrm{Abel}\wedge I\subseteq B\right)$$
24	23	adantr	$$⊢\left(\phi \wedge x\in B\right)\to \left(R\in \mathrm{Abel}\wedge I\subseteq B\right)$$
25		eqid	$$⊢{-}_R={-}_R$$
26	5 25 8	eqgabl	$$⊢\left(R\in \mathrm{Abel}\wedge I\subseteq B\right)\to \left(x\underset{\dot{}}{\sim }E\leftrightarrow \left(x\in B\wedge E\in B\wedge E{-}_{R}x\in I\right)\right)$$
27	24 26	syl	$$⊢\left(\phi \wedge x\in B\right)\to \left(x\underset{\dot{}}{\sim }E\leftrightarrow \left(x\in B\wedge E\in B\wedge E{-}_{R}x\in I\right)\right)$$
28		simp2	$$⊢\left(x\in B\wedge E\in B\wedge E{-}_{R}x\in I\right)\to E\in B$$
29	27 28	biimtrdi	$$⊢\left(\phi \wedge x\in B\right)\to \left(x\underset{\dot{}}{\sim }E\to E\in B\right)$$
30	17 29	sylbid	$$⊢\left(\phi \wedge x\in B\right)\to \left(E\in \left[x\right]\underset{\dot{}}{\sim }\to E\in B\right)$$
31	30	adantr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge 1_Q=\left[x\right]\underset{\dot{}}{\sim }\right)\to \left(E\in \left[x\right]\underset{\dot{}}{\sim }\to E\in B\right)$$
32	15 31	sylbid	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge 1_Q=\left[x\right]\underset{\dot{}}{\sim }\right)\to \left(E\in 1_Q\to E\in B\right)$$
33	32	ex	$$⊢\left(\phi \wedge x\in B\right)\to \left(1_Q=\left[x\right]\underset{\dot{}}{\sim }\to \left(E\in 1_Q\to E\in B\right)\right)$$
34	13 33	mpid	$$⊢\left(\phi \wedge x\in B\right)\to \left(1_Q=\left[x\right]\underset{\dot{}}{\sim }\to E\in B\right)$$
35	34	rexlimdva	$$⊢\phi \to \left(\exists x\in B{1}_Q=\left[x\right]\underset{\dot{}}{\sim }\to E\in B\right)$$
36	12 35	mpd	$$⊢\phi \to E\in B$$