Theorem rngqiprngghmlem3

Description: Lemma 3 for rngqiprngghm . (Contributed by AV, 25-Feb-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	rngqiprngghmlem3	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(A{+}_{R}C\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){+}_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)$$

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 2 3 4 5 6 7	rngqiprng1elbas	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
9	8	anim1i	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\underset{\dot{}}{1}\in B\wedge \left(A\in B\wedge C\in B\right)\right)$$
10		3anass	$$⊢\left(\underset{\dot{}}{1}\in B\wedge A\in B\wedge C\in B\right)\leftrightarrow \left(\underset{\dot{}}{1}\in B\wedge \left(A\in B\wedge C\in B\right)\right)$$
11	9 10	sylibr	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\underset{\dot{}}{1}\in B\wedge A\in B\wedge C\in B\right)$$
12		eqid	$$⊢{+}_R={+}_R$$
13	5 12 6	rngdi	$$⊢\left(R\in \mathrm{Rng}\wedge \left(\underset{\dot{}}{1}\in B\wedge A\in B\wedge C\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(A{+}_{R}C\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){+}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)$$
14	1 11 13	syl2an2r	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(A{+}_{R}C\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){+}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)$$
15	3 12	ressplusg	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to {+}_R={+}_J$$
16	2 15	syl	$$⊢\phi \to {+}_R={+}_J$$
17	16	oveqd	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){+}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){+}_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)$$
18	17	adantr	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){+}_R\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){+}_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)$$
19	14 18	eqtrd	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\left(A{+}_{R}C\right)=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){+}_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)$$