mulgaddcomlem

Description: Lemma for mulgaddcom . (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 31-Aug-2021)

	Ref	Expression
Hypotheses	mulgaddcom.b	$⊢ B = {Base}_{G}$
	mulgaddcom.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgaddcom.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	mulgaddcomlem	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		mulgaddcom.b	$⊢ B = {Base}_{G}$
2		mulgaddcom.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgaddcom.p	$⊢ \underset{˙}{+} = +_{G}$
4		simp1	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to G \in Grp$
5	4	adantr	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to G \in Grp$
6		simp3	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to X \in B$
7	6	adantr	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to X \in B$
8		znegcl	$⊢ y \in ℤ \to - y \in ℤ$
9	1 2	mulgcl	$⊢ (G \in Grp \land - y \in ℤ \land X \in B) \to (- y) \underset{˙}{\cdot} X \in B$
10	8 9	syl3an2	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to (- y) \underset{˙}{\cdot} X \in B$
11	10	adantr	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to (- y) \underset{˙}{\cdot} X \in B$
12		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
13	1 12	grpinvcl	$⊢ (G \in Grp \land X \in B) \to {inv}_{g} (G) (X) \in B$
14	13	3adant2	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to {inv}_{g} (G) (X) \in B$
15	14	adantr	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to {inv}_{g} (G) (X) \in B$
16	1 3	grpass	$⊢ (G \in Grp \land (X \in B \land (- y) \underset{˙}{\cdot} X \in B \land {inv}_{g} (G) (X) \in B)) \to (X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)) \underset{˙}{+} {inv}_{g} (G) (X) = X \underset{˙}{+} (((- y) \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (X))$
17	5 7 11 15 16	syl13anc	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to (X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)) \underset{˙}{+} {inv}_{g} (G) (X) = X \underset{˙}{+} (((- y) \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (X))$
18	1 2 12	mulgneg	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to (- y) \underset{˙}{\cdot} X = {inv}_{g} (G) (y \underset{˙}{\cdot} X)$
19	18	adantr	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to (- y) \underset{˙}{\cdot} X = {inv}_{g} (G) (y \underset{˙}{\cdot} X)$
20	19	oveq1d	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (X) = {inv}_{g} (G) (y \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (X)$
21	1 2	mulgcl	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to y \underset{˙}{\cdot} X \in B$
22	21	adantr	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to y \underset{˙}{\cdot} X \in B$
23	1 3 12	grpinvadd	$⊢ (G \in Grp \land X \in B \land y \underset{˙}{\cdot} X \in B) \to {inv}_{g} (G) (X \underset{˙}{+} (y \underset{˙}{\cdot} X)) = {inv}_{g} (G) (y \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (X)$
24	5 7 22 23	syl3anc	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to {inv}_{g} (G) (X \underset{˙}{+} (y \underset{˙}{\cdot} X)) = {inv}_{g} (G) (y \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (X)$
25	19	oveq2d	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to {inv}_{g} (G) (X) \underset{˙}{+} ((- y) \underset{˙}{\cdot} X) = {inv}_{g} (G) (X) \underset{˙}{+} {inv}_{g} (G) (y \underset{˙}{\cdot} X)$
26	1 3 12	grpinvadd	$⊢ (G \in Grp \land y \underset{˙}{\cdot} X \in B \land X \in B) \to {inv}_{g} (G) ((y \underset{˙}{\cdot} X) \underset{˙}{+} X) = {inv}_{g} (G) (X) \underset{˙}{+} {inv}_{g} (G) (y \underset{˙}{\cdot} X)$
27	5 22 7 26	syl3anc	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to {inv}_{g} (G) ((y \underset{˙}{\cdot} X) \underset{˙}{+} X) = {inv}_{g} (G) (X) \underset{˙}{+} {inv}_{g} (G) (y \underset{˙}{\cdot} X)$
28		fveq2	$⊢ (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X) \to {inv}_{g} (G) ((y \underset{˙}{\cdot} X) \underset{˙}{+} X) = {inv}_{g} (G) (X \underset{˙}{+} (y \underset{˙}{\cdot} X))$
29	28	adantl	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to {inv}_{g} (G) ((y \underset{˙}{\cdot} X) \underset{˙}{+} X) = {inv}_{g} (G) (X \underset{˙}{+} (y \underset{˙}{\cdot} X))$
30	25 27 29	3eqtr2rd	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to {inv}_{g} (G) (X \underset{˙}{+} (y \underset{˙}{\cdot} X)) = {inv}_{g} (G) (X) \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)$
31	20 24 30	3eqtr2d	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (X) = {inv}_{g} (G) (X) \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)$
32	31	oveq2d	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to X \underset{˙}{+} (((- y) \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (G) (X)) = X \underset{˙}{+} ({inv}_{g} (G) (X) \underset{˙}{+} ((- y) \underset{˙}{\cdot} X))$
33	1 3 12	grpasscan1	$⊢ (G \in Grp \land X \in B \land (- y) \underset{˙}{\cdot} X \in B) \to X \underset{˙}{+} ({inv}_{g} (G) (X) \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)) = (- y) \underset{˙}{\cdot} X$
34	5 7 11 33	syl3anc	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to X \underset{˙}{+} ({inv}_{g} (G) (X) \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)) = (- y) \underset{˙}{\cdot} X$
35	17 32 34	3eqtrd	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to (X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)) \underset{˙}{+} {inv}_{g} (G) (X) = (- y) \underset{˙}{\cdot} X$
36	35	oveq1d	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to ((X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)) \underset{˙}{+} {inv}_{g} (G) (X)) \underset{˙}{+} X = ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} X$
37	1 3	grpcl	$⊢ (G \in Grp \land X \in B \land (- y) \underset{˙}{\cdot} X \in B) \to X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X) \in B$
38	4 6 10 37	syl3anc	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X) \in B$
39	38	adantr	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X) \in B$
40	1 3 12	grpasscan2	$⊢ (G \in Grp \land X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X) \in B \land X \in B) \to ((X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)) \underset{˙}{+} {inv}_{g} (G) (X)) \underset{˙}{+} X = X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)$
41	5 39 7 40	syl3anc	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to ((X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)) \underset{˙}{+} {inv}_{g} (G) (X)) \underset{˙}{+} X = X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)$
42	36 41	eqtr3d	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem mulgaddcomlem

Proof