Metamath Proof Explorer

Theorem qusmulrng

Description: Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng . Similar to qusmul2idl . (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 28-Feb-2025)

		Ref	Expression
	Hypotheses	qusmulrng.e	$⊢ \underset{˙}{\sim} = R ~_{QG} S$
		qusmulrng.h	$⊢ H = R /_{𝑠} \underset{˙}{\sim}$
		qusmulrng.b	$⊢ B = {Base}_{R}$
		qusmulrng.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		qusmulrng.a	$⊢ \underset{˙}{∙} = \cdot_{H}$
	Assertion	qusmulrng	$⊢ ((R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \land (X \in B \land Y \in B)) \to [X] \underset{˙}{\sim} \underset{˙}{∙} [Y] \underset{˙}{\sim} = [(X \underset{˙}{\cdot} Y)] \underset{˙}{\sim}$

Proof

Step	Hyp	Ref	Expression
1		qusmulrng.e	$⊢ \underset{˙}{\sim} = R ~_{QG} S$
2		qusmulrng.h	$⊢ H = R /_{𝑠} \underset{˙}{\sim}$
3		qusmulrng.b	$⊢ B = {Base}_{R}$
4		qusmulrng.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		qusmulrng.a	$⊢ \underset{˙}{∙} = \cdot_{H}$
6	2	a1i	$⊢ (R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \to H = R /_{𝑠} \underset{˙}{\sim}$
7	3	a1i	$⊢ (R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \to B = {Base}_{R}$
8	3 1	eqger	$⊢ S \in SubGrp (R) \to \underset{˙}{\sim} Er B$
9	8	3ad2ant3	$⊢ (R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \to \underset{˙}{\sim} Er B$
10		simp1	$⊢ (R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \to R \in Rng$
11		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
12	3 1 11 4	2idlcpblrng	$⊢ (R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \to ((a \underset{˙}{\sim} b \land c \underset{˙}{\sim} d) \to (a \underset{˙}{\cdot} c) \underset{˙}{\sim} (b \underset{˙}{\cdot} d))$
13	10	anim1i	$⊢ ((R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \land (b \in B \land d \in B)) \to (R \in Rng \land (b \in B \land d \in B))$
14		3anass	$⊢ (R \in Rng \land b \in B \land d \in B) \leftrightarrow (R \in Rng \land (b \in B \land d \in B))$
15	13 14	sylibr	$⊢ ((R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \land (b \in B \land d \in B)) \to (R \in Rng \land b \in B \land d \in B)$
16	3 4	rngcl	$⊢ (R \in Rng \land b \in B \land d \in B) \to b \underset{˙}{\cdot} d \in B$
17	15 16	syl	$⊢ ((R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \land (b \in B \land d \in B)) \to b \underset{˙}{\cdot} d \in B$
18	6 7 9 10 12 17 4 5	qusmulval	$⊢ ((R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \land X \in B \land Y \in B) \to [X] \underset{˙}{\sim} \underset{˙}{∙} [Y] \underset{˙}{\sim} = [(X \underset{˙}{\cdot} Y)] \underset{˙}{\sim}$
19	18	3expb	$⊢ ((R \in Rng \land S \in 2Ideal (R) \land S \in SubGrp (R)) \land (X \in B \land Y \in B)) \to [X] \underset{˙}{\sim} \underset{˙}{∙} [Y] \underset{˙}{\sim} = [(X \underset{˙}{\cdot} Y)] \underset{˙}{\sim}$