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	|- .x. = ( .r ` R )
Assertion	2idlcpbl	|- ( ( R e. Ring /\ S e. I ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. 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	|- .x. = ( .r ` R )
5		ringrng	|- ( R e. Ring -> R e. Rng )
6	5	adantr	|- ( ( R e. Ring /\ S e. I ) -> R e. Rng )
7		simpr	|- ( ( R e. Ring /\ S e. I ) -> S e. I )
8		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
9		eqid	|- ( oppR ` R ) = ( oppR ` R )
10		eqid	|- ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
11	8 9 10 3	2idlelb	|- ( S e. I <-> ( S e. ( LIdeal ` R ) /\ S e. ( LIdeal ` ( oppR ` R ) ) ) )
12	11	simplbi	|- ( S e. I -> S e. ( LIdeal ` R ) )
13	8	lidlsubg	|- ( ( R e. Ring /\ S e. ( LIdeal ` R ) ) -> S e. ( SubGrp ` R ) )
14	12 13	sylan2	|- ( ( R e. Ring /\ S e. I ) -> S e. ( SubGrp ` R ) )
15	1 2 3 4	2idlcpblrng	|- ( ( R e. Rng /\ S e. I /\ S e. ( SubGrp ` R ) ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )
16	6 7 14 15	syl3anc	|- ( ( R e. Ring /\ S e. I ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )