mulgsubdi

Description: Group multiple of a difference. (Contributed by Mario Carneiro, 13-Dec-2014)

	Ref	Expression
Hypotheses	mulgsubdi.b	$⊢ B = {Base}_{G}$
	mulgsubdi.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgsubdi.d	$⊢ \underset{˙}{-} = -_{G}$
Assertion	mulgsubdi	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} (X \underset{˙}{-} Y) = (M \underset{˙}{\cdot} X) \underset{˙}{-} (M \underset{˙}{\cdot} Y)$

Proof

Step	Hyp	Ref	Expression
1		mulgsubdi.b	$⊢ B = {Base}_{G}$
2		mulgsubdi.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgsubdi.d	$⊢ \underset{˙}{-} = -_{G}$
4		simpl	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to G \in Abel$
5		simpr1	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \in ℤ$
6		simpr2	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to X \in B$
7		ablgrp	$⊢ G \in Abel \to G \in Grp$
8	7	adantr	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to G \in Grp$
9		simpr3	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to Y \in B$
10		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
11	1 10	grpinvcl	$⊢ (G \in Grp \land Y \in B) \to {inv}_{g} (G) (Y) \in B$
12	8 9 11	syl2anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to {inv}_{g} (G) (Y) \in B$
13		eqid	$⊢ +_{G} = +_{G}$
14	1 2 13	mulgdi	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land {inv}_{g} (G) (Y) \in B)) \to M \underset{˙}{\cdot} (X +_{G} {inv}_{g} (G) (Y)) = (M \underset{˙}{\cdot} X) +_{G} (M \underset{˙}{\cdot} {inv}_{g} (G) (Y))$
15	4 5 6 12 14	syl13anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} (X +_{G} {inv}_{g} (G) (Y)) = (M \underset{˙}{\cdot} X) +_{G} (M \underset{˙}{\cdot} {inv}_{g} (G) (Y))$
16	1 2 10	mulginvcom	$⊢ (G \in Grp \land M \in ℤ \land Y \in B) \to M \underset{˙}{\cdot} {inv}_{g} (G) (Y) = {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
17	8 5 9 16	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} {inv}_{g} (G) (Y) = {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
18	17	oveq2d	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to (M \underset{˙}{\cdot} X) +_{G} (M \underset{˙}{\cdot} {inv}_{g} (G) (Y)) = (M \underset{˙}{\cdot} X) +_{G} {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
19	15 18	eqtrd	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} (X +_{G} {inv}_{g} (G) (Y)) = (M \underset{˙}{\cdot} X) +_{G} {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
20	1 13 10 3	grpsubval	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{-} Y = X +_{G} {inv}_{g} (G) (Y)$
21	6 9 20	syl2anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to X \underset{˙}{-} Y = X +_{G} {inv}_{g} (G) (Y)$
22	21	oveq2d	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} (X \underset{˙}{-} Y) = M \underset{˙}{\cdot} (X +_{G} {inv}_{g} (G) (Y))$
23	1 2	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land X \in B) \to M \underset{˙}{\cdot} X \in B$
24	8 5 6 23	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} X \in B$
25	1 2	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land Y \in B) \to M \underset{˙}{\cdot} Y \in B$
26	8 5 9 25	syl3anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} Y \in B$
27	1 13 10 3	grpsubval	$⊢ (M \underset{˙}{\cdot} X \in B \land M \underset{˙}{\cdot} Y \in B) \to (M \underset{˙}{\cdot} X) \underset{˙}{-} (M \underset{˙}{\cdot} Y) = (M \underset{˙}{\cdot} X) +_{G} {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
28	24 26 27	syl2anc	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to (M \underset{˙}{\cdot} X) \underset{˙}{-} (M \underset{˙}{\cdot} Y) = (M \underset{˙}{\cdot} X) +_{G} {inv}_{g} (G) (M \underset{˙}{\cdot} Y)$
29	19 22 28	3eqtr4d	$⊢ (G \in Abel \land (M \in ℤ \land X \in B \land Y \in B)) \to M \underset{˙}{\cdot} (X \underset{˙}{-} Y) = (M \underset{˙}{\cdot} X) \underset{˙}{-} (M \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem mulgsubdi

Proof