Theorem rngqiprngfulem3

Description: Lemma 3 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$$
	rngqiprngfu.m	$$⊢\underset{\dot{}}{-}={-}_R$$
	rngqiprngfu.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	rngqiprngfu.n	$$⊢U=\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}$$
Assertion	rngqiprngfulem3	$$⊢\phi \to U\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		rngqiprngfu.m	$$⊢\underset{\dot{}}{-}={-}_R$$
13		rngqiprngfu.a	$$⊢\underset{\dot{}}{+}={+}_R$$
14		rngqiprngfu.n	$$⊢U=\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}$$
15		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
16	1 15	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
17	1 2 3 4 5 6 7 8 9 10 11	rngqiprngfulem2	$$⊢\phi \to E\in B$$
18	1 2 3 4 5 6 7	rngqiprng1elbas	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
19	5 6	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge \underset{\dot{}}{1}\in B\wedge E\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}E\in B$$
20	1 18 17 19	syl3anc	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}E\in B$$
21	5 12	grpsubcl	$$⊢\left(R\in \mathrm{Grp}\wedge E\in B\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}E\in B\right)\to E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\in B$$
22	16 17 20 21	syl3anc	$$⊢\phi \to E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\in B$$
23	5 13 16 22 18	grpcld	$$⊢\phi \to \left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}\in B$$
24	14 23	eqeltrid	$$⊢\phi \to U\in B$$