Metamath Proof Explorer

Theorem mulgsubdir

Description: Subtraction of a group element from itself. (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgsubdir.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgsubdir.t ⊢ · = ( .g ‘ 𝐺 )
mulgsubdir.d ⊢ − = ( -g ‘ 𝐺 )
Assertion mulgsubdir ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 − 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) − ( 𝑁 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mulgsubdir.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgsubdir.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgsubdir.d ⊢ − = ( -g ‘ 𝐺 )
4 znegcl ⊢ ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ )
5 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6 1 2 5 mulgdir ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ - 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + - 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) ( +g ‘ 𝐺 ) ( - 𝑁 · 𝑋 ) ) )
7 4 6 syl3anr2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + - 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) ( +g ‘ 𝐺 ) ( - 𝑁 · 𝑋 ) ) )
8 simpr1 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑀 ∈ ℤ )
9 8 zcnd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑀 ∈ ℂ )
10 simpr2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑁 ∈ ℤ )
11 10 zcnd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑁 ∈ ℂ )
12 9 11 negsubd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 + - 𝑁 ) = ( 𝑀 − 𝑁 ) )
13 12 oveq1d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + - 𝑁 ) · 𝑋 ) = ( ( 𝑀 − 𝑁 ) · 𝑋 ) )
14 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
15 1 2 14 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) )
16 15 3adant3r1 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( - 𝑁 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) )
17 16 oveq2d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 𝑋 ) ( +g ‘ 𝐺 ) ( - 𝑁 · 𝑋 ) ) = ( ( 𝑀 · 𝑋 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) ) )
18 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
19 18 3adant3r2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
20 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
21 20 3adant3r1 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
22 1 5 14 3 grpsubval ⊢ ( ( ( 𝑀 · 𝑋 ) ∈ 𝐵 ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( ( 𝑀 · 𝑋 ) − ( 𝑁 · 𝑋 ) ) = ( ( 𝑀 · 𝑋 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) ) )
23 19 21 22 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 𝑋 ) − ( 𝑁 · 𝑋 ) ) = ( ( 𝑀 · 𝑋 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) ) )
24 17 23 eqtr4d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 𝑋 ) ( +g ‘ 𝐺 ) ( - 𝑁 · 𝑋 ) ) = ( ( 𝑀 · 𝑋 ) − ( 𝑁 · 𝑋 ) ) )
25 7 13 24 3eqtr3d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 − 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) − ( 𝑁 · 𝑋 ) ) )