Theorem rngqiprnglinlem3

Description: Lemma 3 for rngqiprnglin . (Contributed by AV, 28-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$$
	rngqiprngim.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
	rngqiprngim.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
Assertion	rngqiprnglinlem3	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left[A\right]\underset{\dot{}}{\sim }{\cdot }_Q\left[C\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$

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		rngqiprngim.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
9		rngqiprngim.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
10	1 2 3 4 5 6 7 8 9	rngqiprnglinlem2	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left[\left(A\underset{\dot{}}{·}C\right)\right]\underset{\dot{}}{\sim }=\left[A\right]\underset{\dot{}}{\sim }{\cdot }_Q\left[C\right]\underset{\dot{}}{\sim }$$
11	1	anim1i	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(R\in \mathrm{Rng}\wedge \left(A\in B\wedge C\in B\right)\right)$$
12		3anass	$$⊢\left(R\in \mathrm{Rng}\wedge A\in B\wedge C\in B\right)\leftrightarrow \left(R\in \mathrm{Rng}\wedge \left(A\in B\wedge C\in B\right)\right)$$
13	11 12	sylibr	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(R\in \mathrm{Rng}\wedge A\in B\wedge C\in B\right)$$
14	5 6	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge A\in B\wedge C\in B\right)\to A\underset{\dot{}}{·}C\in B$$
15	13 14	syl	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to A\underset{\dot{}}{·}C\in B$$
16		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
17	8 9 5 16	quseccl0	$$⊢\left(R\in \mathrm{Rng}\wedge A\underset{\dot{}}{·}C\in B\right)\to \left[\left(A\underset{\dot{}}{·}C\right)\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$
18	1 15 17	syl2an2r	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left[\left(A\underset{\dot{}}{·}C\right)\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$
19	10 18	eqeltrrd	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left[A\right]\underset{\dot{}}{\sim }{\cdot }_Q\left[C\right]\underset{\dot{}}{\sim }\in {\mathrm{Base}}_Q$$