mulgnnass

Description: Product of group multiples, for positive multiples in a semigroup. (Contributed by Mario Carneiro, 13-Dec-2014) (Revised by AV, 29-Aug-2021)

	Ref	Expression
Hypotheses	mulgass.b	$⊢ B = {Base}_{G}$
	mulgass.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	mulgnnass	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		mulgass.b	$⊢ B = {Base}_{G}$
2		mulgass.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		oveq1	$⊢ n = 1 \to n \cdot N = 1 \cdot N$
4	3	oveq1d	$⊢ n = 1 \to n \cdot N \underset{˙}{\cdot} X = 1 \cdot N \underset{˙}{\cdot} X$
5		oveq1	$⊢ n = 1 \to n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = 1 \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
6	4 5	eqeq12d	$⊢ n = 1 \to (n \cdot N \underset{˙}{\cdot} X = n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \leftrightarrow 1 \cdot N \underset{˙}{\cdot} X = 1 \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
7	6	imbi2d	$⊢ n = 1 \to (((N \in ℕ \land X \in B \land G \in Smgrp) \to n \cdot N \underset{˙}{\cdot} X = n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) \leftrightarrow ((N \in ℕ \land X \in B \land G \in Smgrp) \to 1 \cdot N \underset{˙}{\cdot} X = 1 \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)))$
8		oveq1	$⊢ n = m \to n \cdot N = m \cdot N$
9	8	oveq1d	$⊢ n = m \to n \cdot N \underset{˙}{\cdot} X = m \cdot N \underset{˙}{\cdot} X$
10		oveq1	$⊢ n = m \to n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = m \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
11	9 10	eqeq12d	$⊢ n = m \to (n \cdot N \underset{˙}{\cdot} X = n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \leftrightarrow m \cdot N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
12	11	imbi2d	$⊢ n = m \to (((N \in ℕ \land X \in B \land G \in Smgrp) \to n \cdot N \underset{˙}{\cdot} X = n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) \leftrightarrow ((N \in ℕ \land X \in B \land G \in Smgrp) \to m \cdot N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)))$
13		oveq1	$⊢ n = m + 1 \to n \cdot N = (m + 1) \cdot N$
14	13	oveq1d	$⊢ n = m + 1 \to n \cdot N \underset{˙}{\cdot} X = (m + 1) \cdot N \underset{˙}{\cdot} X$
15		oveq1	$⊢ n = m + 1 \to n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = (m + 1) \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
16	14 15	eqeq12d	$⊢ n = m + 1 \to (n \cdot N \underset{˙}{\cdot} X = n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \leftrightarrow (m + 1) \cdot N \underset{˙}{\cdot} X = (m + 1) \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
17	16	imbi2d	$⊢ n = m + 1 \to (((N \in ℕ \land X \in B \land G \in Smgrp) \to n \cdot N \underset{˙}{\cdot} X = n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) \leftrightarrow ((N \in ℕ \land X \in B \land G \in Smgrp) \to (m + 1) \cdot N \underset{˙}{\cdot} X = (m + 1) \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)))$
18		oveq1	$⊢ n = M \to n \cdot N = M \cdot N$
19	18	oveq1d	$⊢ n = M \to n \cdot N \underset{˙}{\cdot} X = M \cdot N \underset{˙}{\cdot} X$
20		oveq1	$⊢ n = M \to n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
21	19 20	eqeq12d	$⊢ n = M \to (n \cdot N \underset{˙}{\cdot} X = n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \leftrightarrow M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
22	21	imbi2d	$⊢ n = M \to (((N \in ℕ \land X \in B \land G \in Smgrp) \to n \cdot N \underset{˙}{\cdot} X = n \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) \leftrightarrow ((N \in ℕ \land X \in B \land G \in Smgrp) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)))$
23		nncn	$⊢ N \in ℕ \to N \in ℂ$
24	23	mullidd	$⊢ N \in ℕ \to 1 \cdot N = N$
25	24	3ad2ant1	$⊢ (N \in ℕ \land X \in B \land G \in Smgrp) \to 1 \cdot N = N$
26	25	oveq1d	$⊢ (N \in ℕ \land X \in B \land G \in Smgrp) \to 1 \cdot N \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$
27		sgrpmgm	$⊢ G \in Smgrp \to G \in Mgm$
28	1 2	mulgnncl	$⊢ (G \in Mgm \land N \in ℕ \land X \in B) \to N \underset{˙}{\cdot} X \in B$
29	27 28	syl3an1	$⊢ (G \in Smgrp \land N \in ℕ \land X \in B) \to N \underset{˙}{\cdot} X \in B$
30	29	3coml	$⊢ (N \in ℕ \land X \in B \land G \in Smgrp) \to N \underset{˙}{\cdot} X \in B$
31	1 2	mulg1	$⊢ N \underset{˙}{\cdot} X \in B \to 1 \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} X$
32	30 31	syl	$⊢ (N \in ℕ \land X \in B \land G \in Smgrp) \to 1 \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} X$
33	26 32	eqtr4d	$⊢ (N \in ℕ \land X \in B \land G \in Smgrp) \to 1 \cdot N \underset{˙}{\cdot} X = 1 \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
34		oveq1	$⊢ m \cdot N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \to (m \cdot N \underset{˙}{\cdot} X) +_{G} (N \underset{˙}{\cdot} X) = (m \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) +_{G} (N \underset{˙}{\cdot} X)$
35		nncn	$⊢ m \in ℕ \to m \in ℂ$
36	35	adantr	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to m \in ℂ$
37		simpr1	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to N \in ℕ$
38	37	nncnd	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to N \in ℂ$
39	36 38	adddirp1d	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to (m + 1) \cdot N = m \cdot N + N$
40	39	oveq1d	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to (m + 1) \cdot N \underset{˙}{\cdot} X = (m \cdot N + N) \underset{˙}{\cdot} X$
41		simpr3	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to G \in Smgrp$
42		nnmulcl	$⊢ (m \in ℕ \land N \in ℕ) \to m \cdot N \in ℕ$
43	42	3ad2antr1	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to m \cdot N \in ℕ$
44		simpr2	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to X \in B$
45		eqid	$⊢ +_{G} = +_{G}$
46	1 2 45	mulgnndir	$⊢ (G \in Smgrp \land (m \cdot N \in ℕ \land N \in ℕ \land X \in B)) \to (m \cdot N + N) \underset{˙}{\cdot} X = (m \cdot N \underset{˙}{\cdot} X) +_{G} (N \underset{˙}{\cdot} X)$
47	41 43 37 44 46	syl13anc	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to (m \cdot N + N) \underset{˙}{\cdot} X = (m \cdot N \underset{˙}{\cdot} X) +_{G} (N \underset{˙}{\cdot} X)$
48	40 47	eqtrd	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to (m + 1) \cdot N \underset{˙}{\cdot} X = (m \cdot N \underset{˙}{\cdot} X) +_{G} (N \underset{˙}{\cdot} X)$
49	1 2 45	mulgnnp1	$⊢ (m \in ℕ \land N \underset{˙}{\cdot} X \in B) \to (m + 1) \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = (m \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) +_{G} (N \underset{˙}{\cdot} X)$
50	30 49	sylan2	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to (m + 1) \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = (m \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) +_{G} (N \underset{˙}{\cdot} X)$
51	48 50	eqeq12d	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to ((m + 1) \cdot N \underset{˙}{\cdot} X = (m + 1) \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \leftrightarrow (m \cdot N \underset{˙}{\cdot} X) +_{G} (N \underset{˙}{\cdot} X) = (m \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) +_{G} (N \underset{˙}{\cdot} X))$
52	34 51	imbitrrid	$⊢ (m \in ℕ \land (N \in ℕ \land X \in B \land G \in Smgrp)) \to (m \cdot N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \to (m + 1) \cdot N \underset{˙}{\cdot} X = (m + 1) \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
53	52	ex	$⊢ m \in ℕ \to ((N \in ℕ \land X \in B \land G \in Smgrp) \to (m \cdot N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \to (m + 1) \cdot N \underset{˙}{\cdot} X = (m + 1) \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)))$
54	53	a2d	$⊢ m \in ℕ \to (((N \in ℕ \land X \in B \land G \in Smgrp) \to m \cdot N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)) \to ((N \in ℕ \land X \in B \land G \in Smgrp) \to (m + 1) \cdot N \underset{˙}{\cdot} X = (m + 1) \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)))$
55	7 12 17 22 33 54	nnind	$⊢ M \in ℕ \to ((N \in ℕ \land X \in B \land G \in Smgrp) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
56	55	3expd	$⊢ M \in ℕ \to (N \in ℕ \to (X \in B \to (G \in Smgrp \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))))$
57	56	com4r	$⊢ G \in Smgrp \to (M \in ℕ \to (N \in ℕ \to (X \in B \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))))$
58	57	3imp2	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem mulgnnass

Proof