Theorem rngqiprngfulem2

Description: Lemma 2 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 )
	rngqiprngfu.e	⊢ ( 𝜑 → 𝐸 ∈ ( 1r ‘ 𝑄 ) )
Assertion	rngqiprngfulem2	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )

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		rngqiprngfu.e	⊢ ( 𝜑 → 𝐸 ∈ ( 1r ‘ 𝑄 ) )
12	1 2 3 4 5 6 7 8 9 10	rngqiprngfulem1	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ )
13	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐸 ∈ ( 1r ‘ 𝑄 ) )
14		eleq2	⊢ ( ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ → ( 𝐸 ∈ ( 1r ‘ 𝑄 ) ↔ 𝐸 ∈ [ 𝑥 ] ∼ ) )
15	14	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ ) → ( 𝐸 ∈ ( 1r ‘ 𝑄 ) ↔ 𝐸 ∈ [ 𝑥 ] ∼ ) )
16		elecg	⊢ ( ( 𝐸 ∈ ( 1r ‘ 𝑄 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐸 ∈ [ 𝑥 ] ∼ ↔ 𝑥 ∼ 𝐸 ) )
17	11 16	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐸 ∈ [ 𝑥 ] ∼ ↔ 𝑥 ∼ 𝐸 ) )
18		rngabl	⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
19	1 18	syl	⊢ ( 𝜑 → 𝑅 ∈ Abel )
20		eqid	⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
21	5 20	2idlss	⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) → 𝐼 ⊆ 𝐵 )
22	2 21	syl	⊢ ( 𝜑 → 𝐼 ⊆ 𝐵 )
23	19 22	jca	⊢ ( 𝜑 → ( 𝑅 ∈ Abel ∧ 𝐼 ⊆ 𝐵 ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑅 ∈ Abel ∧ 𝐼 ⊆ 𝐵 ) )
25		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
26	5 25 8	eqgabl	⊢ ( ( 𝑅 ∈ Abel ∧ 𝐼 ⊆ 𝐵 ) → ( 𝑥 ∼ 𝐸 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵 ∧ ( 𝐸 ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) ) )
27	24 26	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∼ 𝐸 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵 ∧ ( 𝐸 ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) ) )
28		simp2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵 ∧ ( 𝐸 ( -g ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) → 𝐸 ∈ 𝐵 )
29	27 28	biimtrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∼ 𝐸 → 𝐸 ∈ 𝐵 ) )
30	17 29	sylbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐸 ∈ [ 𝑥 ] ∼ → 𝐸 ∈ 𝐵 ) )
31	30	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ ) → ( 𝐸 ∈ [ 𝑥 ] ∼ → 𝐸 ∈ 𝐵 ) )
32	15 31	sylbid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ ) → ( 𝐸 ∈ ( 1r ‘ 𝑄 ) → 𝐸 ∈ 𝐵 ) )
33	32	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ → ( 𝐸 ∈ ( 1r ‘ 𝑄 ) → 𝐸 ∈ 𝐵 ) ) )
34	13 33	mpid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ → 𝐸 ∈ 𝐵 ) )
35	34	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 ( 1r ‘ 𝑄 ) = [ 𝑥 ] ∼ → 𝐸 ∈ 𝐵 ) )
36	12 35	mpd	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )