Metamath Proof Explorer

Theorem 2idlcpbl

Description: The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015) (Proof shortened by AV, 31-Mar-2025)

		Ref	Expression
	Hypotheses	2idlcpblrng.x	$⊢ X = {Base}_{R}$
		2idlcpblrng.r	$⊢ E = R ~_{QG} S$
		2idlcpblrng.i	$⊢ I = 2Ideal (R)$
		2idlcpblrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	Assertion	2idlcpbl	$⊢ (R \in Ring \land S \in I) \to ((A E C \land B E D) \to (A \underset{˙}{\cdot} B) E (C \underset{˙}{\cdot} D))$

Proof

Step	Hyp	Ref	Expression
1		2idlcpblrng.x	$⊢ X = {Base}_{R}$
2		2idlcpblrng.r	$⊢ E = R ~_{QG} S$
3		2idlcpblrng.i	$⊢ I = 2Ideal (R)$
4		2idlcpblrng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		ringrng	$⊢ R \in Ring \to R \in Rng$
6	5	adantr	$⊢ (R \in Ring \land S \in I) \to R \in Rng$
7		simpr	$⊢ (R \in Ring \land S \in I) \to S \in I$
8		eqid	$⊢ LIdeal (R) = LIdeal (R)$
9		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
10		eqid	$⊢ LIdeal ({opp}_{r} (R)) = LIdeal ({opp}_{r} (R))$
11	8 9 10 3	2idlelb	$⊢ S \in I \leftrightarrow (S \in LIdeal (R) \land S \in LIdeal ({opp}_{r} (R)))$
12	11	simplbi	$⊢ S \in I \to S \in LIdeal (R)$
13	8	lidlsubg	$⊢ (R \in Ring \land S \in LIdeal (R)) \to S \in SubGrp (R)$
14	12 13	sylan2	$⊢ (R \in Ring \land S \in I) \to S \in SubGrp (R)$
15	1 2 3 4	2idlcpblrng	$⊢ (R \in Rng \land S \in I \land S \in SubGrp (R)) \to ((A E C \land B E D) \to (A \underset{˙}{\cdot} B) E (C \underset{˙}{\cdot} D))$
16	6 7 14 15	syl3anc	$⊢ (R \in Ring \land S \in I) \to ((A E C \land B E D) \to (A \underset{˙}{\cdot} B) E (C \underset{˙}{\cdot} D))$