qusmul

Description: Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		qusmul.h	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
2		qusmul.v	$⊢ B = {Base}_{R}$
3		qusmul.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		qusmul.a	$⊢ \underset{˙}{\times} = \cdot_{Q}$
5		qusmul.r	$⊢ φ \to R \in CRing$
6		qusmul.i	$⊢ φ \to I \in LIdeal (R)$
7		qusmul.x	$⊢ φ \to X \in B$
8		qusmul.y	$⊢ φ \to Y \in B$
9	1	a1i	$⊢ φ \to Q = R /_{𝑠} (R ~_{QG} I)$
10	2	a1i	$⊢ φ \to B = {Base}_{R}$
11	5	crngringd	$⊢ φ \to R \in Ring$
12		eqid	$⊢ LIdeal (R) = LIdeal (R)$
13	12	lidlsubg	$⊢ (R \in Ring \land I \in LIdeal (R)) \to I \in SubGrp (R)$
14	11 6 13	syl2anc	$⊢ φ \to I \in SubGrp (R)$
15		eqid	$⊢ R ~_{QG} I = R ~_{QG} I$
16	2 15	eqger	$⊢ I \in SubGrp (R) \to (R ~_{QG} I) Er B$
17	14 16	syl	$⊢ φ \to (R ~_{QG} I) Er B$
18	12	crng2idl	$⊢ R \in CRing \to LIdeal (R) = 2Ideal (R)$
19	5 18	syl	$⊢ φ \to LIdeal (R) = 2Ideal (R)$
20	6 19	eleqtrd	$⊢ φ \to I \in 2Ideal (R)$
21		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
22	2 15 21 3	2idlcpbl	$⊢ (R \in Ring \land I \in 2Ideal (R)) \to ((x (R ~_{QG} I) y \land z (R ~_{QG} I) t) \to (x \underset{˙}{\cdot} z) (R ~_{QG} I) (y \underset{˙}{\cdot} t))$
23	11 20 22	syl2anc	$⊢ φ \to ((x (R ~_{QG} I) y \land z (R ~_{QG} I) t) \to (x \underset{˙}{\cdot} z) (R ~_{QG} I) (y \underset{˙}{\cdot} t))$
24	2 3	ringcl	$⊢ (R \in Ring \land p \in B \land q \in B) \to p \underset{˙}{\cdot} q \in B$
25	24	3expb	$⊢ (R \in Ring \land (p \in B \land q \in B)) \to p \underset{˙}{\cdot} q \in B$
26	11 25	sylan	$⊢ (φ \land (p \in B \land q \in B)) \to p \underset{˙}{\cdot} q \in B$
27	26	caovclg	$⊢ (φ \land (y \in B \land t \in B)) \to y \underset{˙}{\cdot} t \in B$
28	9 10 17 5 23 27 3 4	qusmulval	$⊢ (φ \land X \in B \land Y \in B) \to [X] (R ~_{QG} I) \underset{˙}{\times} [Y] (R ~_{QG} I) = [(X \underset{˙}{\cdot} Y)] (R ~_{QG} I)$
29	7 8 28	mpd3an23	$⊢ φ \to [X] (R ~_{QG} I) \underset{˙}{\times} [Y] (R ~_{QG} I) = [(X \underset{˙}{\cdot} Y)] (R ~_{QG} I)$

Metamath Proof Explorer

Theorem qusmul

Proof