Theorem 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={\mathrm{Base}}_G$$
	mulgass.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	mulgnnass	Could not format assertion : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mulgass.b	$$⊢B={\mathrm{Base}}_G$$
2		mulgass.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		oveq1	$$⊢n=1\to n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
4	3	oveq1d	$$⊢n=1\to n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X$$
5		oveq1	$$⊢n=1\to n\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)=1\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)$$
6	4 5	eqeq12d	$$⊢n=1\to \left(n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=n\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)\leftrightarrow 1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=1\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)\right)$$
7	6	imbi2d	Could not format ( n = 1 -> ( ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( n x. N ) .x. X ) = ( n .x. ( N .x. X ) ) ) <-> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( 1 x. N ) .x. X ) = ( 1 .x. ( N .x. X ) ) ) ) ) : No typesetting found for |- ( n = 1 -> ( ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( n x. N ) .x. X ) = ( n .x. ( N .x. X ) ) ) <-> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( 1 x. N ) .x. X ) = ( 1 .x. ( N .x. X ) ) ) ) ) with typecode |-
8		oveq1	$$⊢n=m\to n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=m\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
9	8	oveq1d	$$⊢n=m\to n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=m\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X$$
10		oveq1	$$⊢n=m\to n\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)=m\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)$$
11	9 10	eqeq12d	$$⊢n=m\to \left(n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=n\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)\leftrightarrow m\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=m\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)\right)$$
12	11	imbi2d	Could not format ( n = m -> ( ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( n x. N ) .x. X ) = ( n .x. ( N .x. X ) ) ) <-> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( m x. N ) .x. X ) = ( m .x. ( N .x. X ) ) ) ) ) : No typesetting found for |- ( n = m -> ( ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( n x. N ) .x. X ) = ( n .x. ( N .x. X ) ) ) <-> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( m x. N ) .x. X ) = ( m .x. ( N .x. X ) ) ) ) ) with typecode |-
13		oveq1	$$⊢n=m+1\to n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\left(m+1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
14	13	oveq1d	$$⊢n=m+1\to n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=\left(m+1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X$$
15		oveq1	$$⊢n=m+1\to n\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)=\left(m+1\right)\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)$$
16	14 15	eqeq12d	$$⊢n=m+1\to \left(n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=n\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)\leftrightarrow \left(m+1\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=\left(m+1\right)\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)\right)$$
17	16	imbi2d	Could not format ( n = ( m + 1 ) -> ( ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( n x. N ) .x. X ) = ( n .x. ( N .x. X ) ) ) <-> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( m + 1 ) .x. ( N .x. X ) ) ) ) ) : No typesetting found for |- ( n = ( m + 1 ) -> ( ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( n x. N ) .x. X ) = ( n .x. ( N .x. X ) ) ) <-> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( m + 1 ) .x. ( N .x. X ) ) ) ) ) with typecode |-
18		oveq1	$$⊢n=M\to n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
19	18	oveq1d	$$⊢n=M\to n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X$$
20		oveq1	$$⊢n=M\to n\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)=M\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)$$
21	19 20	eqeq12d	$$⊢n=M\to \left(n\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=n\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)\leftrightarrow \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=M\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)\right)$$
22	21	imbi2d	Could not format ( n = M -> ( ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( n x. N ) .x. X ) = ( n .x. ( N .x. X ) ) ) <-> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) ) ) : No typesetting found for |- ( n = M -> ( ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( n x. N ) .x. X ) = ( n .x. ( N .x. X ) ) ) <-> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) ) ) with typecode |-
23		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
24	23	mullidd	$$⊢N\in \mathbb{N}\to 1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N$$
25	24	3ad2ant1	Could not format ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( 1 x. N ) = N ) : No typesetting found for |- ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( 1 x. N ) = N ) with typecode |-
26	25	oveq1d	Could not format ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( 1 x. N ) .x. X ) = ( N .x. X ) ) : No typesetting found for |- ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( 1 x. N ) .x. X ) = ( N .x. X ) ) with typecode |-
27		sgrpmgm	Could not format ( G e. Smgrp -> G e. Mgm ) : No typesetting found for |- ( G e. Smgrp -> G e. Mgm ) with typecode |-
28	1 2	mulgnncl	$$⊢\left(G\in \mathrm{Mgm}\wedge N\in \mathbb{N}\wedge X\in B\right)\to N\underset{\dot{}}{·}X\in B$$
29	27 28	syl3an1	Could not format ( ( G e. Smgrp /\ N e. NN /\ X e. B ) -> ( N .x. X ) e. B ) : No typesetting found for |- ( ( G e. Smgrp /\ N e. NN /\ X e. B ) -> ( N .x. X ) e. B ) with typecode |-
30	29	3coml	Could not format ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( N .x. X ) e. B ) : No typesetting found for |- ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( N .x. X ) e. B ) with typecode |-
31	1 2	mulg1	$$⊢N\underset{\dot{}}{·}X\in B\to 1\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)=N\underset{\dot{}}{·}X$$
32	30 31	syl	Could not format ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( 1 .x. ( N .x. X ) ) = ( N .x. X ) ) : No typesetting found for |- ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( 1 .x. ( N .x. X ) ) = ( N .x. X ) ) with typecode |-
33	26 32	eqtr4d	Could not format ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( 1 x. N ) .x. X ) = ( 1 .x. ( N .x. X ) ) ) : No typesetting found for |- ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( 1 x. N ) .x. X ) = ( 1 .x. ( N .x. X ) ) ) with typecode |-
34		oveq1	$$⊢m\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X=m\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)\to \left(m\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\underset{\dot{}}{·}X\right){+}_G\left(N\underset{\dot{}}{·}X\right)=\left(m\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)\right){+}_G\left(N\underset{\dot{}}{·}X\right)$$
35		nncn	$$⊢m\in \mathbb{N}\to m\in ℂ$$
36	35	adantr	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> m e. CC ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> m e. CC ) with typecode |-
37		simpr1	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> N e. NN ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> N e. NN ) with typecode |-
38	37	nncnd	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> N e. CC ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> N e. CC ) with typecode |-
39	36 38	adddirp1d	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( m + 1 ) x. N ) = ( ( m x. N ) + N ) ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( m + 1 ) x. N ) = ( ( m x. N ) + N ) ) with typecode |-
40	39	oveq1d	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( ( m x. N ) + N ) .x. X ) ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( ( m x. N ) + N ) .x. X ) ) with typecode |-
41		simpr3	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> G e. Smgrp ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> G e. Smgrp ) with typecode |-
42		nnmulcl	$$⊢\left(m\in \mathbb{N}\wedge N\in \mathbb{N}\right)\to m\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}$$
43	42	3ad2antr1	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( m x. N ) e. NN ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( m x. N ) e. NN ) with typecode |-
44		simpr2	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> X e. B ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> X e. B ) with typecode |-
45		eqid	$$⊢{+}_G={+}_G$$
46	1 2 45	mulgnndir	Could not format ( ( G e. Smgrp /\ ( ( m x. N ) e. NN /\ N e. NN /\ X e. B ) ) -> ( ( ( m x. N ) + N ) .x. X ) = ( ( ( m x. N ) .x. X ) ( +g ` G ) ( N .x. X ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( ( m x. N ) e. NN /\ N e. NN /\ X e. B ) ) -> ( ( ( m x. N ) + N ) .x. X ) = ( ( ( m x. N ) .x. X ) ( +g ` G ) ( N .x. X ) ) ) with typecode |-
47	41 43 37 44 46	syl13anc	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( ( m x. N ) + N ) .x. X ) = ( ( ( m x. N ) .x. X ) ( +g ` G ) ( N .x. X ) ) ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( ( m x. N ) + N ) .x. X ) = ( ( ( m x. N ) .x. X ) ( +g ` G ) ( N .x. X ) ) ) with typecode |-
48	40 47	eqtrd	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( ( m x. N ) .x. X ) ( +g ` G ) ( N .x. X ) ) ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( ( m x. N ) .x. X ) ( +g ` G ) ( N .x. X ) ) ) with typecode |-
49	1 2 45	mulgnnp1	$$⊢\left(m\in \mathbb{N}\wedge N\underset{\dot{}}{·}X\in B\right)\to \left(m+1\right)\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)=\left(m\underset{\dot{}}{·}\left(N\underset{\dot{}}{·}X\right)\right){+}_G\left(N\underset{\dot{}}{·}X\right)$$
50	30 49	sylan2	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( m + 1 ) .x. ( N .x. X ) ) = ( ( m .x. ( N .x. X ) ) ( +g ` G ) ( N .x. X ) ) ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( m + 1 ) .x. ( N .x. X ) ) = ( ( m .x. ( N .x. X ) ) ( +g ` G ) ( N .x. X ) ) ) with typecode |-
51	48 50	eqeq12d	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( ( ( m + 1 ) x. N ) .x. X ) = ( ( m + 1 ) .x. ( N .x. X ) ) <-> ( ( ( m x. N ) .x. X ) ( +g ` G ) ( N .x. X ) ) = ( ( m .x. ( N .x. X ) ) ( +g ` G ) ( N .x. X ) ) ) ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( ( ( m + 1 ) x. N ) .x. X ) = ( ( m + 1 ) .x. ( N .x. X ) ) <-> ( ( ( m x. N ) .x. X ) ( +g ` G ) ( N .x. X ) ) = ( ( m .x. ( N .x. X ) ) ( +g ` G ) ( N .x. X ) ) ) ) with typecode |-
52	34 51	imbitrrid	Could not format ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( ( m x. N ) .x. X ) = ( m .x. ( N .x. X ) ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( m + 1 ) .x. ( N .x. X ) ) ) ) : No typesetting found for |- ( ( m e. NN /\ ( N e. NN /\ X e. B /\ G e. Smgrp ) ) -> ( ( ( m x. N ) .x. X ) = ( m .x. ( N .x. X ) ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( m + 1 ) .x. ( N .x. X ) ) ) ) with typecode |-
53	52	ex	Could not format ( m e. NN -> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( ( m x. N ) .x. X ) = ( m .x. ( N .x. X ) ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( m + 1 ) .x. ( N .x. X ) ) ) ) ) : No typesetting found for |- ( m e. NN -> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( ( m x. N ) .x. X ) = ( m .x. ( N .x. X ) ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( m + 1 ) .x. ( N .x. X ) ) ) ) ) with typecode |-
54	53	a2d	Could not format ( m e. NN -> ( ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( m x. N ) .x. X ) = ( m .x. ( N .x. X ) ) ) -> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( m + 1 ) .x. ( N .x. X ) ) ) ) ) : No typesetting found for |- ( m e. NN -> ( ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( m x. N ) .x. X ) = ( m .x. ( N .x. X ) ) ) -> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( ( m + 1 ) x. N ) .x. X ) = ( ( m + 1 ) .x. ( N .x. X ) ) ) ) ) with typecode |-
55	7 12 17 22 33 54	nnind	Could not format ( M e. NN -> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) ) : No typesetting found for |- ( M e. NN -> ( ( N e. NN /\ X e. B /\ G e. Smgrp ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) ) with typecode |-
56	55	3expd	Could not format ( M e. NN -> ( N e. NN -> ( X e. B -> ( G e. Smgrp -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) ) ) ) : No typesetting found for |- ( M e. NN -> ( N e. NN -> ( X e. B -> ( G e. Smgrp -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) ) ) ) with typecode |-
57	56	com4r	Could not format ( G e. Smgrp -> ( M e. NN -> ( N e. NN -> ( X e. B -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) ) ) ) : No typesetting found for |- ( G e. Smgrp -> ( M e. NN -> ( N e. NN -> ( X e. B -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) ) ) ) with typecode |-
58	57	3imp2	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) with typecode |-