Theorem rngqiprngfulem5

Description: Lemma 5 for rngqiprngfu . (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	rngqiprngfulem5	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}U=\underset{\dot{}}{1}$$

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	14	oveq2i	$$⊢\underset{\dot{}}{1}\underset{\dot{}}{·}U=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}\right)$$
16	15	a1i	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}U=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}\right)$$
17	1 2 3 4 5 6 7	rngqiprng1elbas	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
18		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
19	1 18	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
20	1 2 3 4 5 6 7 8 9 10 11	rngqiprngfulem2	$$⊢\phi \to E\in B$$
21	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$$
22	1 17 20 21	syl3anc	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}E\in B$$
23	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$$
24	19 20 22 23	syl3anc	$$⊢\phi \to E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\in B$$
25	5 13 6	rngdi	$$⊢\left(R\in \mathrm{Rng}\wedge \left(\underset{\dot{}}{1}\in B\wedge E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\in B\wedge \underset{\dot{}}{1}\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
26	1 17 24 17 25	syl13anc	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
27	5 6 12 1 17 20 22	rngsubdi	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)$$
28	5 6	rngass	$$⊢\left(R\in \mathrm{Rng}\wedge \left(\underset{\dot{}}{1}\in B\wedge \underset{\dot{}}{1}\in B\wedge E\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}E=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)$$
29	1 17 17 20 28	syl13anc	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}E=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)$$
30	3 6	ressmulr	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to \underset{\dot{}}{·}={\cdot }_J$$
31	2 30	syl	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_J$$
32	31	oveqd	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}{\cdot }_J\underset{\dot{}}{1}$$
33		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
34	33 7	ringidcl	$$⊢J\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
35		eqid	$$⊢{\cdot }_J={\cdot }_J$$
36	33 35 7	ringlidm	$$⊢\left(J\in \mathrm{Ring}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_J\right)\to \underset{\dot{}}{1}{\cdot }_J\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
37	4 34 36	syl2anc2	$$⊢\phi \to \underset{\dot{}}{1}{\cdot }_J\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
38	32 37	eqtrd	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
39	38	oveq1d	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}E=\underset{\dot{}}{1}\underset{\dot{}}{·}E$$
40	29 39	eqtr3d	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)=\underset{\dot{}}{1}\underset{\dot{}}{·}E$$
41	40	oveq2d	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)$$
42		eqid	$$⊢0_R=0_R$$
43	5 42 12	grpsubid	$$⊢\left(R\in \mathrm{Grp}\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}E\in B\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)=0_R$$
44	19 22 43	syl2anc	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)=0_R$$
45	27 41 44	3eqtrd	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)=0_R$$
46	45 38	oveq12d	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\right)\underset{\dot{}}{+}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}\right)=0_R\underset{\dot{}}{+}\underset{\dot{}}{1}$$
47	26 46	eqtrd	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}\right)=0_R\underset{\dot{}}{+}\underset{\dot{}}{1}$$
48	5 13 42 19 17	grplidd	$$⊢\phi \to 0_R\underset{\dot{}}{+}\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
49	16 47 48	3eqtrd	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}U=\underset{\dot{}}{1}$$