Theorem rngqiprngfulem1

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

	Ref	Expression
Hypotheses	rngqiprngfu.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rngqiprngfu.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	rngqiprngfu.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
	rngqiprngfu.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
	rngqiprngfu.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rngqiprngfu.t	⊢ · = ( .r ‘ 𝑅 )
	rngqiprngfu.1	⊢ 1 = ( 1r ‘ 𝐽 )
	rngqiprngfu.g	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
	rngqiprngfu.q	⊢ 𝑄 = ( 𝑅 /s ∼ )
	rngqiprngfu.v	⊢ ( 𝜑 → 𝑄 ∈ Ring )
Assertion	rngqiprngfulem1	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ )

Proof

Step	Hyp	Ref	Expression
1		rngqiprngfu.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
2		rngqiprngfu.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3		rngqiprngfu.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4		rngqiprngfu.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
5		rngqiprngfu.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
6		rngqiprngfu.t	⊢ · = ( .r ‘ 𝑅 )
7		rngqiprngfu.1	⊢ 1 = ( 1r ‘ 𝐽 )
8		rngqiprngfu.g	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
9		rngqiprngfu.q	⊢ 𝑄 = ( 𝑅 /s ∼ )
10		rngqiprngfu.v	⊢ ( 𝜑 → 𝑄 ∈ Ring )
11		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
12		eqid	⊢ ( 1r ‘ 𝑄 ) = ( 1r ‘ 𝑄 )
13	11 12	ringidcl	⊢ ( 𝑄 ∈ Ring → ( 1r ‘ 𝑄 ) ∈ ( Base ‘ 𝑄 ) )
14	10 13	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑄 ) ∈ ( Base ‘ 𝑄 ) )
15	9	a1i	⊢ ( 𝜑 → 𝑄 = ( 𝑅 /s ∼ ) )
16	5	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
17	8	ovexi	⊢ ∼ ∈ V
18	17	a1i	⊢ ( 𝜑 → ∼ ∈ V )
19	15 16 18 1	qusbas	⊢ ( 𝜑 → ( 𝐵 / ∼ ) = ( Base ‘ 𝑄 ) )
20	14 19	eleqtrrd	⊢ ( 𝜑 → ( 1r ‘ 𝑄 ) ∈ ( 𝐵 / ∼ ) )
21		fvexd	⊢ ( 𝜑 → ( 1r ‘ 𝑄 ) ∈ V )
22		elqsg	⊢ ( ( 1r ‘ 𝑄 ) ∈ V → ( ( 1r ‘ 𝑄 ) ∈ ( 𝐵 / ∼ ) ↔ ∃ 𝑥 ∈ 𝐵 ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ ) )
23	21 22	syl	⊢ ( 𝜑 → ( ( 1r ‘ 𝑄 ) ∈ ( 𝐵 / ∼ ) ↔ ∃ 𝑥 ∈ 𝐵 ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ ) )
24	20 23	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ )