Theorem rngqiprnglinlem1

Description: Lemma 1 for rngqiprnglin . (Contributed by AV, 28-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	rngqiprnglinlem1	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(A\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	2	adantr	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to I\in \mathrm{2Ideal}\left(R\right)$$
9	3 6	ressmulr	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to \underset{\dot{}}{·}={\cdot }_J$$
10	8 9	syl	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \underset{\dot{}}{·}={\cdot }_J$$
11	10	oveqd	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}\underset{\dot{}}{1}=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){\cdot }_J\underset{\dot{}}{1}$$
12		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
13		eqid	$$⊢{\cdot }_J={\cdot }_J$$
14	4	adantr	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to J\in \mathrm{Ring}$$
15	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$$
16	15	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$$
17	12 13 7 14 16	ringridmd	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right){\cdot }_J\underset{\dot{}}{1}=\underset{\dot{}}{1}\underset{\dot{}}{·}A$$
18	11 17	eqtrd	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}\underset{\dot{}}{·}A$$
19	18	oveq1d	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}C=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}C$$
20	1	adantr	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to R\in \mathrm{Rng}$$
21	1 2 3 4 5 6 7	rngqiprng1elbas	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
22	21	adantr	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \underset{\dot{}}{1}\in B$$
23		simprl	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to A\in B$$
24	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$$
25	20 22 23 24	syl3anc	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}A\in B$$
26		simprr	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to C\in B$$
27	5 6	rngass	$$⊢\left(R\in \mathrm{Rng}\wedge \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\in B\wedge \underset{\dot{}}{1}\in B\wedge C\in B\right)\right)\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}C=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)$$
28	20 25 22 26 27	syl13anc	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\underset{\dot{}}{·}C=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)$$
29	5 6	rngass	$$⊢\left(R\in \mathrm{Rng}\wedge \left(\underset{\dot{}}{1}\in B\wedge A\in B\wedge C\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}C=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}C\right)$$
30	20 22 23 26 29	syl13anc	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}C=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}C\right)$$
31	19 28 30	3eqtr3d	$$⊢\left(\phi \wedge \left(A\in B\wedge C\in B\right)\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}A\right)\underset{\dot{}}{·}\left(\underset{\dot{}}{1}\underset{\dot{}}{·}C\right)=\underset{\dot{}}{1}\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}C\right)$$