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 ⊢ B = Base G
mulgsubdir.t ⊢ · ˙ = ⋅ G
mulgsubdir.d ⊢ - ˙ = - G
Assertion mulgsubdir ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → M − N · ˙ X = M · ˙ X - ˙ N · ˙ X

Proof

Step Hyp Ref Expression
1 mulgsubdir.b ⊢ B = Base G
2 mulgsubdir.t ⊢ · ˙ = ⋅ G
3 mulgsubdir.d ⊢ - ˙ = - G
4 znegcl ⊢ N ∈ ℤ → − N ∈ ℤ
5 eqid ⊢ + G = + G
6 1 2 5 mulgdir ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ − N ∈ ℤ ∧ X ∈ B → M + -N · ˙ X = M · ˙ X + G -N · ˙ X
7 4 6 syl3anr2 ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → M + -N · ˙ X = M · ˙ X + G -N · ˙ X
8 simpr1 ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → M ∈ ℤ
9 8 zcnd ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → M ∈ ℂ
10 simpr2 ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → N ∈ ℤ
11 10 zcnd ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → N ∈ ℂ
12 9 11 negsubd ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → M + -N = M − N
13 12 oveq1d ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → M + -N · ˙ X = M − N · ˙ X
14 eqid ⊢ inv g ⁡ G = inv g ⁡ G
15 1 2 14 mulgneg ⊢ G ∈ Grp ∧ N ∈ ℤ ∧ X ∈ B → -N · ˙ X = inv g ⁡ G ⁡ N · ˙ X
16 15 3adant3r1 ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → -N · ˙ X = inv g ⁡ G ⁡ N · ˙ X
17 16 oveq2d ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → M · ˙ X + G -N · ˙ X = M · ˙ X + G inv g ⁡ G ⁡ N · ˙ X
18 1 2 mulgcl ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ X ∈ B → M · ˙ X ∈ B
19 18 3adant3r2 ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → M · ˙ X ∈ B
20 1 2 mulgcl ⊢ G ∈ Grp ∧ N ∈ ℤ ∧ X ∈ B → N · ˙ X ∈ B
21 20 3adant3r1 ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → N · ˙ X ∈ B
22 1 5 14 3 grpsubval ⊢ M · ˙ X ∈ B ∧ N · ˙ X ∈ B → M · ˙ X - ˙ N · ˙ X = M · ˙ X + G inv g ⁡ G ⁡ N · ˙ X
23 19 21 22 syl2anc ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → M · ˙ X - ˙ N · ˙ X = M · ˙ X + G inv g ⁡ G ⁡ N · ˙ X
24 17 23 eqtr4d ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → M · ˙ X + G -N · ˙ X = M · ˙ X - ˙ N · ˙ X
25 7 13 24 3eqtr3d ⊢ G ∈ Grp ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ X ∈ B → M − N · ˙ X = M · ˙ X - ˙ N · ˙ X