qusmul2idl

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

	Ref	Expression
Hypotheses	qusmul2idl.h	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
	qusmul2idl.v	$⊢ B = {Base}_{R}$
	qusmul2idl.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	qusmul2idl.a	$⊢ \underset{˙}{\times} = \cdot_{Q}$
	qusmul2idl.1	$⊢ φ \to R \in Ring$
	qusmul2idl.2	$⊢ φ \to I \in 2Ideal (R)$
	qusmul2idl.3	$⊢ φ \to X \in B$
	qusmul2idl.4	$⊢ φ \to Y \in B$
Assertion	qusmul2idl	$⊢ φ \to [X] (R ~_{QG} I) \underset{˙}{\times} [Y] (R ~_{QG} I) = [(X \underset{˙}{\cdot} Y)] (R ~_{QG} I)$

Proof

Step	Hyp	Ref	Expression
1		qusmul2idl.h	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
2		qusmul2idl.v	$⊢ B = {Base}_{R}$
3		qusmul2idl.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		qusmul2idl.a	$⊢ \underset{˙}{\times} = \cdot_{Q}$
5		qusmul2idl.1	$⊢ φ \to R \in Ring$
6		qusmul2idl.2	$⊢ φ \to I \in 2Ideal (R)$
7		qusmul2idl.3	$⊢ φ \to X \in B$
8		qusmul2idl.4	$⊢ φ \to Y \in B$
9	1	a1i	$⊢ φ \to Q = R /_{𝑠} (R ~_{QG} I)$
10	2	a1i	$⊢ φ \to B = {Base}_{R}$
11	6	2idllidld	$⊢ φ \to I \in LIdeal (R)$
12		eqid	$⊢ LIdeal (R) = LIdeal (R)$
13	12	lidlsubg	$⊢ (R \in Ring \land I \in LIdeal (R)) \to I \in SubGrp (R)$
14	5 11 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		eqid	$⊢ 2Ideal (R) = 2Ideal (R)$
19	2 15 18 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))$
20	5 6 19	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))$
21	2 3	ringcl	$⊢ (R \in Ring \land p \in B \land q \in B) \to p \underset{˙}{\cdot} q \in B$
22	21	3expb	$⊢ (R \in Ring \land (p \in B \land q \in B)) \to p \underset{˙}{\cdot} q \in B$
23	5 22	sylan	$⊢ (φ \land (p \in B \land q \in B)) \to p \underset{˙}{\cdot} q \in B$
24	23	caovclg	$⊢ (φ \land (y \in B \land t \in B)) \to y \underset{˙}{\cdot} t \in B$
25	9 10 17 5 20 24 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)$
26	7 8 25	mpd3an23	$⊢ φ \to [X] (R ~_{QG} I) \underset{˙}{\times} [Y] (R ~_{QG} I) = [(X \underset{˙}{\cdot} Y)] (R ~_{QG} I)$

Metamath Proof Explorer

Theorem qusmul2idl

Proof