Theorem rngqiprngfulem1

Description: Lemma 1 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}$$
Assertion	rngqiprngfulem1	$$⊢\phi \to \exists x\in B{1}_Q=\left[x\right]\underset{\dot{}}{\sim }$$

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		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
12		eqid	$$⊢1_Q=1_Q$$
13	11 12	ringidcl	$$⊢Q\in \mathrm{Ring}\to 1_Q\in {\mathrm{Base}}_Q$$
14	10 13	syl	$$⊢\phi \to 1_Q\in {\mathrm{Base}}_Q$$
15	9	a1i	$$⊢\phi \to Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
16	5	a1i	$$⊢\phi \to B={\mathrm{Base}}_R$$
17	8	ovexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
18	17	a1i	$$⊢\phi \to \underset{\dot{}}{\sim }\in \mathrm{V}$$
19	15 16 18 1	qusbas	$$⊢\phi \to B/\underset{\dot{}}{\sim }={\mathrm{Base}}_Q$$
20	14 19	eleqtrrd	$$⊢\phi \to 1_Q\in \left(B/\underset{\dot{}}{\sim }\right)$$
21		fvexd	$$⊢\phi \to 1_Q\in \mathrm{V}$$
22		elqsg	$$⊢1_Q\in \mathrm{V}\to \left(1_Q\in \left(B/\underset{\dot{}}{\sim }\right)\leftrightarrow \exists x\in B{1}_Q=\left[x\right]\underset{\dot{}}{\sim }\right)$$
23	21 22	syl	$$⊢\phi \to \left(1_Q\in \left(B/\underset{\dot{}}{\sim }\right)\leftrightarrow \exists x\in B{1}_Q=\left[x\right]\underset{\dot{}}{\sim }\right)$$
24	20 23	mpbid	$$⊢\phi \to \exists x\in B{1}_Q=\left[x\right]\underset{\dot{}}{\sim }$$