Theorem rngqiprngghmlem2

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

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		ringrng	$$⊢J\in \mathrm{Ring}\to J\in \mathrm{Rng}$$
9	4 8	syl	$$⊢\phi \to J\in \mathrm{Rng}$$
10	9	adantr	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to J\in \mathrm{Rng}$$
11	1 2 3 4 5 6 7	rngqiprngghmlem1	$$⊢\left(\phi \wedge A\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}A\in {\mathrm{Base}}_J$$
12	11	adantrr	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}A\in {\mathrm{Base}}_J$$
13	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$$
14	13	adantrl	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}C\in {\mathrm{Base}}_J$$
15		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
16		eqid	$$⊢{+}_J={+}_J$$
17	15 16	rngacl	$$⊢\left(J\in \mathrm{Rng}\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}A\in {\mathrm{Base}}_J\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}C\in {\mathrm{Base}}_J\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){+}_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\in {\mathrm{Base}}_J$$
18	10 12 14 17	syl3anc	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){+}_J\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)\in {\mathrm{Base}}_J$$