Theorem rngqiprngimfolem

Description: Lemma for rngqiprngimfo . (Contributed by AV, 5-Mar-2025) (Proof shortened by AV, 24-Mar-2025)

	Ref	Expression
Hypotheses	rng2idlring.r	$$⊢\phi \to R\in \mathrm{Rng}$$
	rng2idlring.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rng2idlring.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	rng2idlring.u	$$⊢\phi \to J\in \mathrm{Ring}$$
	rng2idlring.b	$$⊢B={\mathrm{Base}}_R$$
	rng2idlring.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rng2idlring.1	$$⊢\underset{\dot{}}{1}=1_J$$
Assertion	rngqiprngimfolem	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(\left(C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\right){+}_{R}A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rng2idlring.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rng2idlring.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
4		rng2idlring.u	$$⊢\phi \to J\in \mathrm{Ring}$$
5		rng2idlring.b	$$⊢B={\mathrm{Base}}_R$$
6		rng2idlring.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
7		rng2idlring.1	$$⊢\underset{\dot{}}{1}=1_J$$
8	1	3ad2ant1	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to R\in \mathrm{Rng}$$
9	1 2 3 4 5 6 7	rngqiprng1elbas	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
10	9	3ad2ant1	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\in B$$
11		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
12	1 11	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
13	12	3ad2ant1	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to R\in \mathrm{Grp}$$
14		simp3	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to C\in B$$
15	5 6	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge \underset{\dot{}}{1}\in B\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}C\in B$$
16	8 10 14 15	syl3anc	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}C\in B$$
17		eqid	$$⊢{-}_R={-}_R$$
18	5 17	grpsubcl	$$⊢\left(R\in \mathrm{Grp}\wedge C\in B\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}C\in B\right)\to C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\in B$$
19	13 14 16 18	syl3anc	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\in B$$
20		eqid	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
21	5 20	2idlss	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to I\subseteq B$$
22	2 21	syl	$$⊢\phi \to I\subseteq B$$
23	22	sselda	$$⊢\left(\phi \wedge A\in I\right)\to A\in B$$
24	23	3adant3	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to A\in B$$
25		eqid	$$⊢{+}_R={+}_R$$
26	5 25 6	rngdi	$$⊢\left(R\in \mathrm{Rng}\wedge \left(\underset{\dot{}}{1}\in B\wedge C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\in B\wedge A\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(\left(C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\right){+}_{R}A\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\right)\right){+}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)$$
27	8 10 19 24 26	syl13anc	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(\left(C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\right){+}_{R}A\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\right)\right){+}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)$$
28	5 6 17 8 10 14 16	rngsubdi	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right){-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\right)$$
29	3 6	ressmulr	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to \underset{\dot{}}{·}={\cdot }_J$$
30	2 29	syl	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_J$$
31	30	oveqd	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)=\underset{\dot{}}{1}{\cdot }_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)$$
32	31	3ad2ant1	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)=\underset{\dot{}}{1}{\cdot }_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)$$
33		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
34		eqid	$$⊢{\cdot }_J={\cdot }_J$$
35	4	3ad2ant1	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to J\in \mathrm{Ring}$$
36	1 2 3 4 5 6 7	rngqiprngghmlem1	$$⊢\left(\phi \wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}C\in {\mathrm{Base}}_J$$
37	36	3adant2	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}C\in {\mathrm{Base}}_J$$
38	33 34 7 35 37	ringlidmd	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}{\cdot }_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)=\underset{\dot{}}{1}\underset{\dot{}}{·}C$$
39	32 38	eqtrd	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)=\underset{\dot{}}{1}\underset{\dot{}}{·}C$$
40	39	oveq2d	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right){-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right){-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)$$
41		eqid	$$⊢0_R=0_R$$
42	5 41 17	grpsubid	$$⊢\left(R\in \mathrm{Grp}\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}C\in B\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right){-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)=0_R$$
43	13 16 42	syl2anc	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right){-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)=0_R$$
44	28 40 43	3eqtrd	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\right)=0_R$$
45	44	oveq1d	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}\left(C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\right)\right){+}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)=0_R{+}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)$$
46	5 6	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge \underset{\dot{}}{1}\in B\wedge A\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}A\in B$$
47	8 10 24 46	syl3anc	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}A\in B$$
48	5 25 41 13 47	grplidd	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to 0_R{+}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)=\underset{\dot{}}{1}\underset{\dot{}}{·}A$$
49	30	oveqd	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}A=\underset{\dot{}}{1}{\cdot }_{J}A$$
50	49	3ad2ant1	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}A=\underset{\dot{}}{1}{\cdot }_{J}A$$
51	4	adantr	$$⊢\left(\phi \wedge A\in I\right)\to J\in \mathrm{Ring}$$
52	2 3 33	2idlbas	$$⊢\phi \to {\mathrm{Base}}_J=I$$
53	52	eqcomd	$$⊢\phi \to I={\mathrm{Base}}_J$$
54	53	eleq2d	$$⊢\phi \to \left(A\in I\leftrightarrow A\in {\mathrm{Base}}_J\right)$$
55	54	biimpa	$$⊢\left(\phi \wedge A\in I\right)\to A\in {\mathrm{Base}}_J$$
56	33 34 7 51 55	ringlidmd	$$⊢\left(\phi \wedge A\in I\right)\to \underset{\dot{}}{1}{\cdot }_{J}A=A$$
57	56	3adant3	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}{\cdot }_{J}A=A$$
58	48 50 57	3eqtrd	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to 0_R{+}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)=A$$
59	27 45 58	3eqtrd	$$⊢\left(\phi \wedge A\in I\wedge C\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(\left(C{-}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\right){+}_{R}A\right)=A$$