Theorem rngqiprngfulem3

Description: Lemma 3 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 ‘ 𝑄 ) )
	rngqiprngfu.m	⊢ − = ( -g ‘ 𝑅 )
	rngqiprngfu.a	⊢ + = ( +g ‘ 𝑅 )
	rngqiprngfu.n	⊢ 𝑈 = ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 )
Assertion	rngqiprngfulem3	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )

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		rngqiprngfu.m	⊢ − = ( -g ‘ 𝑅 )
13		rngqiprngfu.a	⊢ + = ( +g ‘ 𝑅 )
14		rngqiprngfu.n	⊢ 𝑈 = ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 )
15		rnggrp	⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
16	1 15	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
17	1 2 3 4 5 6 7 8 9 10 11	rngqiprngfulem2	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
18	1 2 3 4 5 6 7	rngqiprng1elbas	⊢ ( 𝜑 → 1 ∈ 𝐵 )
19	5 6	rngcl	⊢ ( ( 𝑅 ∈ Rng ∧ 1 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵 ) → ( 1 · 𝐸 ) ∈ 𝐵 )
20	1 18 17 19	syl3anc	⊢ ( 𝜑 → ( 1 · 𝐸 ) ∈ 𝐵 )
21	5 12	grpsubcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐸 ∈ 𝐵 ∧ ( 1 · 𝐸 ) ∈ 𝐵 ) → ( 𝐸 − ( 1 · 𝐸 ) ) ∈ 𝐵 )
22	16 17 20 21	syl3anc	⊢ ( 𝜑 → ( 𝐸 − ( 1 · 𝐸 ) ) ∈ 𝐵 )
23	5 13 16 22 18	grpcld	⊢ ( 𝜑 → ( ( 𝐸 − ( 1 · 𝐸 ) ) + 1 ) ∈ 𝐵 )
24	14 23	eqeltrid	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )