rngqiprnglinlem2

	Ref	Expression
Hypotheses	rng2idlring.r	$⊢ φ \to R \in Rng$
	rng2idlring.i	$⊢ φ \to I \in 2Ideal (R)$
	rng2idlring.j	$⊢ J = R ↾_{𝑠} I$
	rng2idlring.u	$⊢ φ \to J \in Ring$
	rng2idlring.b	$⊢ B = {Base}_{R}$
	rng2idlring.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rng2idlring.1	$⊢ \underset{˙}{1} = 1_{J}$
	rngqiprngim.g	$⊢ \underset{˙}{\sim} = R ~_{QG} I$
	rngqiprngim.q	$⊢ Q = R /_{𝑠} \underset{˙}{\sim}$
Assertion	rngqiprnglinlem2	$⊢ (φ \land (A \in B \land C \in B)) \to [(A \underset{˙}{\cdot} C)] \underset{˙}{\sim} = [A] \underset{˙}{\sim} \cdot_{Q} [C] \underset{˙}{\sim}$

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	$⊢ φ \to R \in Rng$
2		rng2idlring.i	$⊢ φ \to I \in 2Ideal (R)$
3		rng2idlring.j	$⊢ J = R ↾_{𝑠} I$
4		rng2idlring.u	$⊢ φ \to J \in Ring$
5		rng2idlring.b	$⊢ B = {Base}_{R}$
6		rng2idlring.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
7		rng2idlring.1	$⊢ \underset{˙}{1} = 1_{J}$
8		rngqiprngim.g	$⊢ \underset{˙}{\sim} = R ~_{QG} I$
9		rngqiprngim.q	$⊢ Q = R /_{𝑠} \underset{˙}{\sim}$
10		ringrng	$⊢ J \in Ring \to J \in Rng$
11	4 10	syl	$⊢ φ \to J \in Rng$
12	3 11	eqeltrrid	$⊢ φ \to R ↾_{𝑠} I \in Rng$
13	1 2 12	rng2idlsubrng	Could not format ( ph -> I e. ( SubRng ` R ) ) : No typesetting found for \|- ( ph -> I e. ( SubRng ` R ) ) with typecode \|-
14		subrngsubg	Could not format ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) ) : No typesetting found for \|- ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) ) with typecode \|-
15	13 14	syl	$⊢ φ \to I \in SubGrp (R)$
16	1 2 15	3jca	$⊢ φ \to (R \in Rng \land I \in 2Ideal (R) \land I \in SubGrp (R))$
17		eqid	$⊢ R ~_{QG} I = R ~_{QG} I$
18	8	oveq2i	$⊢ R /_{𝑠} \underset{˙}{\sim} = R /_{𝑠} (R ~_{QG} I)$
19	9 18	eqtri	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
20		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
21	17 19 5 6 20	qusmulrng	$⊢ ((R \in Rng \land I \in 2Ideal (R) \land I \in SubGrp (R)) \land (A \in B \land C \in B)) \to [A] (R ~_{QG} I) \cdot_{Q} [C] (R ~_{QG} I) = [(A \underset{˙}{\cdot} C)] (R ~_{QG} I)$
22	16 21	sylan	$⊢ (φ \land (A \in B \land C \in B)) \to [A] (R ~_{QG} I) \cdot_{Q} [C] (R ~_{QG} I) = [(A \underset{˙}{\cdot} C)] (R ~_{QG} I)$
23	8	eceq2i	$⊢ [A] \underset{˙}{\sim} = [A] (R ~_{QG} I)$
24	8	eceq2i	$⊢ [C] \underset{˙}{\sim} = [C] (R ~_{QG} I)$
25	23 24	oveq12i	$⊢ [A] \underset{˙}{\sim} \cdot_{Q} [C] \underset{˙}{\sim} = [A] (R ~_{QG} I) \cdot_{Q} [C] (R ~_{QG} I)$
26	8	eceq2i	$⊢ [(A \underset{˙}{\cdot} C)] \underset{˙}{\sim} = [(A \underset{˙}{\cdot} C)] (R ~_{QG} I)$
27	22 25 26	3eqtr4g	$⊢ (φ \land (A \in B \land C \in B)) \to [A] \underset{˙}{\sim} \cdot_{Q} [C] \underset{˙}{\sim} = [(A \underset{˙}{\cdot} C)] \underset{˙}{\sim}$
28	27	eqcomd	$⊢ (φ \land (A \in B \land C \in B)) \to [(A \underset{˙}{\cdot} C)] \underset{˙}{\sim} = [A] \underset{˙}{\sim} \cdot_{Q} [C] \underset{˙}{\sim}$

Metamath Proof Explorer

Theorem rngqiprnglinlem2

Proof