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