Theorem mulgsubdir

Description: Distribution of group multiples over subtraction for group elements, subdir analog. (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 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 − 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) − ( 𝑁 · 𝑋 ) ) )