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 ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑀 · ( 𝑋 − 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) − ( 𝑀 · 𝑌 ) ) )