This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qusmulcrng

Description: Value of the ring operation in a quotient ring of a commutative ring. (Contributed by Thierry Arnoux, 1-Sep-2024) (Proof shortened by metakunt, 3-Jun-2025)

		Ref	Expression
	Hypotheses	qusmulcrng.h	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
		qusmulcrng.v	$⊢ B = {Base}_{R}$
		qusmulcrng.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		qusmulcrng.a	$⊢ \underset{˙}{\times} = \cdot_{Q}$
		qusmulcrng.r	$⊢ φ \to R \in CRing$
		qusmulcrng.i	$⊢ φ \to I \in LIdeal (R)$
		qusmulcrng.x	$⊢ φ \to X \in B$
		qusmulcrng.y	$⊢ φ \to Y \in B$
	Assertion	qusmulcrng	$⊢ φ \to [X] (R ~_{QG} I) \underset{˙}{\times} [Y] (R ~_{QG} I) = [(X \underset{˙}{\cdot} Y)] (R ~_{QG} I)$

Proof

Step	Hyp	Ref	Expression
1		qusmulcrng.h	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
2		qusmulcrng.v	$⊢ B = {Base}_{R}$
3		qusmulcrng.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		qusmulcrng.a	$⊢ \underset{˙}{\times} = \cdot_{Q}$
5		qusmulcrng.r	$⊢ φ \to R \in CRing$
6		qusmulcrng.i	$⊢ φ \to I \in LIdeal (R)$
7		qusmulcrng.x	$⊢ φ \to X \in B$
8		qusmulcrng.y	$⊢ φ \to Y \in B$
9	5	crngringd	$⊢ φ \to R \in Ring$
10		eqid	$⊢ LIdeal (R) = LIdeal (R)$
11	10	crng2idl	$⊢ R \in CRing \to LIdeal (R) = 2Ideal (R)$
12	5 11	syl	$⊢ φ \to LIdeal (R) = 2Ideal (R)$
13	6 12	eleqtrd	$⊢ φ \to I \in 2Ideal (R)$
14	1 2 3 4 9 13 7 8	qusmul2idl	$⊢ φ \to [X] (R ~_{QG} I) \underset{˙}{\times} [Y] (R ~_{QG} I) = [(X \underset{˙}{\cdot} Y)] (R ~_{QG} I)$