Theorem rngqiprngfulem4

Description: Lemma 4 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	rngqiprngfulem4	$$⊢\phi \to \left[U\right]\underset{\dot{}}{\sim }=\left[E\right]\underset{\dot{}}{\sim }$$

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	$$⊢E\underset{\dot{}}{-}U=E\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 E\underset{\dot{}}{-}U=E\underset{\dot{}}{-}\left(\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}\right)$$
17		rngabl	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Abel}$$
18	1 17	syl	$$⊢\phi \to R\in \mathrm{Abel}$$
19	1 2 3 4 5 6 7 8 9 10 11	rngqiprngfulem2	$$⊢\phi \to E\in B$$
20		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
21	1 20	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
22	1 2 3 4 5 6 7	rngqiprng1elbas	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
23	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$$
24	1 22 19 23	syl3anc	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}E\in B$$
25	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$$
26	21 19 24 25	syl3anc	$$⊢\phi \to E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\in B$$
27	5 13 12 18 19 26 22	ablsubsub4	$$⊢\phi \to \left(E\underset{\dot{}}{-}\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\right)\underset{\dot{}}{-}\underset{\dot{}}{1}=E\underset{\dot{}}{-}\left(\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\underset{\dot{}}{+}\underset{\dot{}}{1}\right)$$
28	5 12 18 19 24	ablnncan	$$⊢\phi \to E\underset{\dot{}}{-}\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)=\underset{\dot{}}{1}\underset{\dot{}}{·}E$$
29	28	oveq1d	$$⊢\phi \to \left(E\underset{\dot{}}{-}\left(E\underset{\dot{}}{-}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\right)\right)\underset{\dot{}}{-}\underset{\dot{}}{1}=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}\underset{\dot{}}{1}$$
30	16 27 29	3eqtr2d	$$⊢\phi \to E\underset{\dot{}}{-}U=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}\underset{\dot{}}{1}$$
31		ringrng	$$⊢J\in \mathrm{Ring}\to J\in \mathrm{Rng}$$
32	4 31	syl	$$⊢\phi \to J\in \mathrm{Rng}$$
33	3 32	eqeltrrid	$$⊢\phi \to R{\upharpoonright }_{𝑠}I\in \mathrm{Rng}$$
34	1 2 33	rng2idlnsg	$$⊢\phi \to I\in \mathrm{NrmSGrp}\left(R\right)$$
35		nsgsubg	$$⊢I\in \mathrm{NrmSGrp}\left(R\right)\to I\in \mathrm{SubGrp}\left(R\right)$$
36	34 35	syl	$$⊢\phi \to I\in \mathrm{SubGrp}\left(R\right)$$
37	1 2 3 4 5 6 7	rngqiprngghmlem1	$$⊢\left(\phi \wedge E\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}E\in {\mathrm{Base}}_J$$
38	19 37	mpdan	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}E\in {\mathrm{Base}}_J$$
39		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
40	2 3 39	2idlbas	$$⊢\phi \to {\mathrm{Base}}_J=I$$
41	38 40	eleqtrd	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}E\in I$$
42	39 7	ringidcl	$$⊢J\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
43	4 42	syl	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
44	43 40	eleqtrd	$$⊢\phi \to \underset{\dot{}}{1}\in I$$
45		eqid	$$⊢{-}_J={-}_J$$
46	12 3 45	subgsub	$$⊢\left(I\in \mathrm{SubGrp}\left(R\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}E\in I\wedge \underset{\dot{}}{1}\in I\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}\underset{\dot{}}{1}=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right){-}_J\underset{\dot{}}{1}$$
47	36 41 44 46	syl3anc	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}\underset{\dot{}}{1}=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right){-}_J\underset{\dot{}}{1}$$
48	4	ringgrpd	$$⊢\phi \to J\in \mathrm{Grp}$$
49	39 45	grpsubcl	$$⊢\left(J\in \mathrm{Grp}\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}E\in {\mathrm{Base}}_J\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_J\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right){-}_J\underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
50	48 38 43 49	syl3anc	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right){-}_J\underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
51	47 50	eqeltrd	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}\underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
52	51 40	eleqtrd	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}E\right)\underset{\dot{}}{-}\underset{\dot{}}{1}\in I$$
53	30 52	eqeltrd	$$⊢\phi \to E\underset{\dot{}}{-}U\in I$$
54	1 2 3 4 5 6 7 8 9 10 11 12 13 14	rngqiprngfulem3	$$⊢\phi \to U\in B$$
55	5 12 8	qusecsub	$$⊢\left(\left(R\in \mathrm{Abel}\wedge I\in \mathrm{SubGrp}\left(R\right)\right)\wedge \left(U\in B\wedge E\in B\right)\right)\to \left(\left[U\right]\underset{\dot{}}{\sim }=\left[E\right]\underset{\dot{}}{\sim }\leftrightarrow E\underset{\dot{}}{-}U\in I\right)$$
56	18 36 54 19 55	syl22anc	$$⊢\phi \to \left(\left[U\right]\underset{\dot{}}{\sim }=\left[E\right]\underset{\dot{}}{\sim }\leftrightarrow E\underset{\dot{}}{-}U\in I\right)$$
57	53 56	mpbird	$$⊢\phi \to \left[U\right]\underset{\dot{}}{\sim }=\left[E\right]\underset{\dot{}}{\sim }$$