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

Metamath Proof Explorer

Theorem 2idlcpblrng

Description: The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015) Generalization for non-unital rings and two-sided ideals which are subgroups of the additive group of the non-unital ring. (Revised by AV, 23-Feb-2025)

Ref Expression
Hypotheses 2idlcpblrng.x ⊢ 𝑋 = ( Base ‘ 𝑅 )
2idlcpblrng.r ⊢ 𝐸 = ( 𝑅 ~QG 𝑆 )
2idlcpblrng.i ⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
2idlcpblrng.t ⊢ · = ( .r ‘ 𝑅 )
Assertion 2idlcpblrng ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 2idlcpblrng.x ⊢ 𝑋 = ( Base ‘ 𝑅 )
2 2idlcpblrng.r ⊢ 𝐸 = ( 𝑅 ~QG 𝑆 )
3 2idlcpblrng.i ⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
4 2idlcpblrng.t ⊢ · = ( .r ‘ 𝑅 )
5 simpl1 ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑅 ∈ Rng )
6 simpl3 ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
7 1 2 eqger ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → 𝐸 Er 𝑋 )
8 6 7 syl ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐸 Er 𝑋 )
9 simprl ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐴 𝐸 𝐶 )
10 8 9 ersym ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐶 𝐸 𝐴 )
11 rngabl ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
12 11 3ad2ant1 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑅 ∈ Abel )
13 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
14 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
15 eqid ⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
16 13 14 15 3 2idlelb ⊢ ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
17 16 simplbi ⊢ ( 𝑆 ∈ 𝐼 → 𝑆 ∈ ( LIdeal ‘ 𝑅 ) )
18 17 3ad2ant2 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑆 ∈ ( LIdeal ‘ 𝑅 ) )
19 18 adantr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ∈ ( LIdeal ‘ 𝑅 ) )
20 1 13 lidlss ⊢ ( 𝑆 ∈ ( LIdeal ‘ 𝑅 ) → 𝑆 ⊆ 𝑋 )
21 19 20 syl ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ⊆ 𝑋 )
22 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
23 1 22 2 eqgabl ⊢ ( ( 𝑅 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐶 𝐸 𝐴 ↔ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) ) )
24 12 21 23 syl2an2r ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 𝐸 𝐴 ↔ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) ) )
25 10 24 mpbid ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) )
26 25 simp2d ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐴 ∈ 𝑋 )
27 simprr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐵 𝐸 𝐷 )
28 1 22 2 eqgabl ⊢ ( ( 𝑅 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐵 𝐸 𝐷 ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) ) )
29 12 21 28 syl2an2r ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 𝐸 𝐷 ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) ) )
30 27 29 mpbid ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) )
31 30 simp1d ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐵 ∈ 𝑋 )
32 1 4 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 · 𝐵 ) ∈ 𝑋 )
33 5 26 31 32 syl3anc ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑋 )
34 25 simp1d ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐶 ∈ 𝑋 )
35 30 simp2d ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝐷 ∈ 𝑋 )
36 1 4 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) → ( 𝐶 · 𝐷 ) ∈ 𝑋 )
37 5 34 35 36 syl3anc ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · 𝐷 ) ∈ 𝑋 )
38 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
39 38 3ad2ant1 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑅 ∈ Grp )
40 39 adantr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑅 ∈ Grp )
41 1 4 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐶 · 𝐵 ) ∈ 𝑋 )
42 5 34 31 41 syl3anc ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · 𝐵 ) ∈ 𝑋 )
43 1 22 grpnnncan2 ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝐶 · 𝐷 ) ∈ 𝑋 ∧ ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 · 𝐵 ) ∈ 𝑋 ) ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) = ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) )
44 40 37 33 42 43 syl13anc ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) = ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) )
45 1 4 22 5 34 35 31 rngsubdi ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ) = ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) )
46 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
47 46 subg0cl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝑆 )
48 47 3ad2ant3 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ 𝑆 )
49 48 adantr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 0g ‘ 𝑅 ) ∈ 𝑆 )
50 30 simp3d ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 )
51 46 1 4 13 rnglidlmcl ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 0g ‘ 𝑅 ) ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑋 ∧ ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ∈ 𝑆 ) ) → ( 𝐶 · ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ) ∈ 𝑆 )
52 5 19 49 34 50 51 syl32anc ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐶 · ( 𝐷 ( -g ‘ 𝑅 ) 𝐵 ) ) ∈ 𝑆 )
53 45 52 eqeltrrd ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 )
54 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
55 1 4 14 54 opprmul ⊢ ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) = ( ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) · 𝐵 )
56 1 4 22 5 26 34 31 rngsubdir ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) · 𝐵 ) = ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) )
57 55 56 eqtrid ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) )
58 14 opprrng ⊢ ( 𝑅 ∈ Rng → ( oppr ‘ 𝑅 ) ∈ Rng )
59 58 3ad2ant1 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( oppr ‘ 𝑅 ) ∈ Rng )
60 59 adantr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( oppr ‘ 𝑅 ) ∈ Rng )
61 16 simprbi ⊢ ( 𝑆 ∈ 𝐼 → 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
62 61 3ad2ant2 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
63 62 adantr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
64 25 simp3d ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 )
65 14 46 oppr0 ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( oppr ‘ 𝑅 ) )
66 14 1 opprbas ⊢ 𝑋 = ( Base ‘ ( oppr ‘ 𝑅 ) )
67 65 66 54 15 rnglidlmcl ⊢ ( ( ( ( oppr ‘ 𝑅 ) ∈ Rng ∧ 𝑆 ∈ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ∧ ( 0g ‘ 𝑅 ) ∈ 𝑆 ) ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ∈ 𝑆 ) ) → ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) ∈ 𝑆 )
68 60 63 49 31 64 67 syl32anc ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐵 ( .r ‘ ( oppr ‘ 𝑅 ) ) ( 𝐴 ( -g ‘ 𝑅 ) 𝐶 ) ) ∈ 𝑆 )
69 57 68 eqeltrrd ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 )
70 22 subgsubcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 ∧ ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ∈ 𝑆 ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) ∈ 𝑆 )
71 6 53 69 70 syl3anc ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝐵 ) ( -g ‘ 𝑅 ) ( 𝐶 · 𝐵 ) ) ) ∈ 𝑆 )
72 44 71 eqeltrrd ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) ∈ 𝑆 )
73 1 22 2 eqgabl ⊢ ( ( 𝑅 ∈ Abel ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ↔ ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 · 𝐷 ) ∈ 𝑋 ∧ ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) ∈ 𝑆 ) ) )
74 12 21 73 syl2an2r ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ↔ ( ( 𝐴 · 𝐵 ) ∈ 𝑋 ∧ ( 𝐶 · 𝐷 ) ∈ 𝑋 ∧ ( ( 𝐶 · 𝐷 ) ( -g ‘ 𝑅 ) ( 𝐴 · 𝐵 ) ) ∈ 𝑆 ) ) )
75 33 37 72 74 mpbir3and ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) )
76 75 ex ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ 𝐼 ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( 𝐴 𝐸 𝐶 ∧ 𝐵 𝐸 𝐷 ) → ( 𝐴 · 𝐵 ) 𝐸 ( 𝐶 · 𝐷 ) ) )