Metamath Proof Explorer


Theorem mulgsubdi

Description: Group multiple of a difference. (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgsubdi.b 𝐵 = ( Base ‘ 𝐺 )
mulgsubdi.t · = ( .g𝐺 )
mulgsubdi.d = ( -g𝐺 )
Assertion mulgsubdi ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( 𝑀 · ( 𝑋 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) ( 𝑀 · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mulgsubdi.b 𝐵 = ( Base ‘ 𝐺 )
2 mulgsubdi.t · = ( .g𝐺 )
3 mulgsubdi.d = ( -g𝐺 )
4 simpl ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → 𝐺 ∈ Abel )
5 simpr1 ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → 𝑀 ∈ ℤ )
6 simpr2 ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → 𝑋𝐵 )
7 ablgrp ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
8 7 adantr ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → 𝐺 ∈ Grp )
9 simpr3 ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → 𝑌𝐵 )
10 eqid ( invg𝐺 ) = ( invg𝐺 )
11 1 10 grpinvcl ( ( 𝐺 ∈ Grp ∧ 𝑌𝐵 ) → ( ( invg𝐺 ) ‘ 𝑌 ) ∈ 𝐵 )
12 8 9 11 syl2anc ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( ( invg𝐺 ) ‘ 𝑌 ) ∈ 𝐵 )
13 eqid ( +g𝐺 ) = ( +g𝐺 )
14 1 2 13 mulgdi ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵 ∧ ( ( invg𝐺 ) ‘ 𝑌 ) ∈ 𝐵 ) ) → ( 𝑀 · ( 𝑋 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑌 ) ) ) = ( ( 𝑀 · 𝑋 ) ( +g𝐺 ) ( 𝑀 · ( ( invg𝐺 ) ‘ 𝑌 ) ) ) )
15 4 5 6 12 14 syl13anc ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( 𝑀 · ( 𝑋 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑌 ) ) ) = ( ( 𝑀 · 𝑋 ) ( +g𝐺 ) ( 𝑀 · ( ( invg𝐺 ) ‘ 𝑌 ) ) ) )
16 1 2 10 mulginvcom ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑌𝐵 ) → ( 𝑀 · ( ( invg𝐺 ) ‘ 𝑌 ) ) = ( ( invg𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) )
17 8 5 9 16 syl3anc ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( 𝑀 · ( ( invg𝐺 ) ‘ 𝑌 ) ) = ( ( invg𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) )
18 17 oveq2d ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( ( 𝑀 · 𝑋 ) ( +g𝐺 ) ( 𝑀 · ( ( invg𝐺 ) ‘ 𝑌 ) ) ) = ( ( 𝑀 · 𝑋 ) ( +g𝐺 ) ( ( invg𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) ) )
19 15 18 eqtrd ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( 𝑀 · ( 𝑋 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑌 ) ) ) = ( ( 𝑀 · 𝑋 ) ( +g𝐺 ) ( ( invg𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) ) )
20 1 13 10 3 grpsubval ( ( 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) = ( 𝑋 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑌 ) ) )
21 6 9 20 syl2anc ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝑌 ) = ( 𝑋 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑌 ) ) )
22 21 oveq2d ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( 𝑀 · ( 𝑋 𝑌 ) ) = ( 𝑀 · ( 𝑋 ( +g𝐺 ) ( ( invg𝐺 ) ‘ 𝑌 ) ) ) )
23 1 2 mulgcl ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋𝐵 ) → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
24 8 5 6 23 syl3anc ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
25 1 2 mulgcl ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑌𝐵 ) → ( 𝑀 · 𝑌 ) ∈ 𝐵 )
26 8 5 9 25 syl3anc ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( 𝑀 · 𝑌 ) ∈ 𝐵 )
27 1 13 10 3 grpsubval ( ( ( 𝑀 · 𝑋 ) ∈ 𝐵 ∧ ( 𝑀 · 𝑌 ) ∈ 𝐵 ) → ( ( 𝑀 · 𝑋 ) ( 𝑀 · 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) ( +g𝐺 ) ( ( invg𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) ) )
28 24 26 27 syl2anc ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( ( 𝑀 · 𝑋 ) ( 𝑀 · 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) ( +g𝐺 ) ( ( invg𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) ) )
29 19 22 28 3eqtr4d ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋𝐵𝑌𝐵 ) ) → ( 𝑀 · ( 𝑋 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) ( 𝑀 · 𝑌 ) ) )