Theorem mulgnndir

Description: Sum of group multiples, for positive multiples. (Contributed by Mario Carneiro, 11-Dec-2014) (Revised by AV, 29-Aug-2021)

	Ref	Expression
Hypotheses	mulgnndir.b	$$⊢B={\mathrm{Base}}_G$$
	mulgnndir.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mulgnndir.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	mulgnndir	Could not format assertion : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mulgnndir.b	$$⊢B={\mathrm{Base}}_G$$
2		mulgnndir.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		mulgnndir.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		sgrpmgm	Could not format ( G e. Smgrp -> G e. Mgm ) : No typesetting found for |- ( G e. Smgrp -> G e. Mgm ) with typecode |-
5	1 3	mgmcl	$$⊢\left(G\in \mathrm{Mgm}\wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
6	4 5	syl3an1	Could not format ( ( G e. Smgrp /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B ) : No typesetting found for |- ( ( G e. Smgrp /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B ) with typecode |-
7	6	3expb	Could not format ( ( G e. Smgrp /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B ) with typecode |-
8	7	adantlr	Could not format ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B ) with typecode |-
9	1 3	sgrpass	Could not format ( ( G e. Smgrp /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) with typecode |-
10	9	adantlr	Could not format ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) with typecode |-
11		simpr2	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> N e. NN ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> N e. NN ) with typecode |-
12		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
13	11 12	eleqtrdi	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> N e. ( ZZ>= ` 1 ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> N e. ( ZZ>= ` 1 ) ) with typecode |-
14		simpr1	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. NN ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. NN ) with typecode |-
15	14	nnzd	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. ZZ ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. ZZ ) with typecode |-
16		eluzadd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 1}\wedge M\in \mathbb{Z}\right)\to N+M\in {\mathbb{Z}}_{\ge \left(1+M\right)}$$
17	13 15 16	syl2anc	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( N + M ) e. ( ZZ>= ` ( 1 + M ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( N + M ) e. ( ZZ>= ` ( 1 + M ) ) ) with typecode |-
18	14	nncnd	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. CC ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. CC ) with typecode |-
19	11	nncnd	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> N e. CC ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> N e. CC ) with typecode |-
20	18 19	addcomd	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + N ) = ( N + M ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + N ) = ( N + M ) ) with typecode |-
21		ax-1cn	$$⊢1\in ℂ$$
22		addcom	$$⊢\left(M\in ℂ\wedge 1\in ℂ\right)\to M+1=1+M$$
23	18 21 22	sylancl	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + 1 ) = ( 1 + M ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + 1 ) = ( 1 + M ) ) with typecode |-
24	23	fveq2d	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ZZ>= ` ( M + 1 ) ) = ( ZZ>= ` ( 1 + M ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ZZ>= ` ( M + 1 ) ) = ( ZZ>= ` ( 1 + M ) ) ) with typecode |-
25	17 20 24	3eltr4d	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + N ) e. ( ZZ>= ` ( M + 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + N ) e. ( ZZ>= ` ( M + 1 ) ) ) with typecode |-
26	14 12	eleqtrdi	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. ( ZZ>= ` 1 ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. ( ZZ>= ` 1 ) ) with typecode |-
27		simpr3	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> X e. B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> X e. B ) with typecode |-
28		elfznn	$$⊢x\in \left(1\dots M+N\right)\to x\in \mathbb{N}$$
29		fvconst2g	$$⊢\left(X\in B\wedge x\in \mathbb{N}\right)\to \left(\mathbb{N}\times \left\{X\right\}\right)\left(x\right)=X$$
30	27 28 29	syl2an	Could not format ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... ( M + N ) ) ) -> ( ( NN X. { X } ) ` x ) = X ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... ( M + N ) ) ) -> ( ( NN X. { X } ) ` x ) = X ) with typecode |-
31	27	adantr	Could not format ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... ( M + N ) ) ) -> X e. B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... ( M + N ) ) ) -> X e. B ) with typecode |-
32	30 31	eqeltrd	Could not format ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... ( M + N ) ) ) -> ( ( NN X. { X } ) ` x ) e. B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... ( M + N ) ) ) -> ( ( NN X. { X } ) ` x ) e. B ) with typecode |-
33	8 10 25 26 32	seqsplit	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) .+ ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) .+ ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) ) ) with typecode |-
34		nnaddcl	$$⊢\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)\to M+N\in \mathbb{N}$$
35	14 11 34	syl2anc	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + N ) e. NN ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + N ) e. NN ) with typecode |-
36		eqid	$$⊢seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)$$
37	1 3 2 36	mulgnn	$$⊢\left(M+N\in \mathbb{N}\wedge X\in B\right)\to \left(M+N\right)\underset{\dot{}}{·}X=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(M+N\right)$$
38	35 27 37	syl2anc	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) ) with typecode |-
39	1 3 2 36	mulgnn	$$⊢\left(M\in \mathbb{N}\wedge X\in B\right)\to M\underset{\dot{}}{·}X=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(M\right)$$
40	14 27 39	syl2anc	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) ) with typecode |-
41		elfznn	$$⊢x\in \left(1\dots N\right)\to x\in \mathbb{N}$$
42	27 41 29	syl2an	Could not format ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` x ) = X ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` x ) = X ) with typecode |-
43	27	adantr	Could not format ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> X e. B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> X e. B ) with typecode |-
44		nnaddcl	$$⊢\left(x\in \mathbb{N}\wedge M\in \mathbb{N}\right)\to x+M\in \mathbb{N}$$
45	41 14 44	syl2anr	Could not format ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( x + M ) e. NN ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( x + M ) e. NN ) with typecode |-
46		fvconst2g	$$⊢\left(X\in B\wedge x+M\in \mathbb{N}\right)\to \left(\mathbb{N}\times \left\{X\right\}\right)\left(x+M\right)=X$$
47	43 45 46	syl2anc	Could not format ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` ( x + M ) ) = X ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` ( x + M ) ) = X ) with typecode |-
48	42 47	eqtr4d	Could not format ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` x ) = ( ( NN X. { X } ) ` ( x + M ) ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` x ) = ( ( NN X. { X } ) ` ( x + M ) ) ) with typecode |-
49	13 15 48	seqshft2	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) = ( seq ( 1 + M ) ( .+ , ( NN X. { X } ) ) ` ( N + M ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) = ( seq ( 1 + M ) ( .+ , ( NN X. { X } ) ) ` ( N + M ) ) ) with typecode |-
50	1 3 2 36	mulgnn	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to N\underset{\dot{}}{·}X=seq1\left(\underset{\dot{}}{+},\left(\mathbb{N}\times \left\{X\right\}\right)\right)\left(N\right)$$
51	11 27 50	syl2anc	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( N .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( N .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) ) with typecode |-
52	23	seqeq1d	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) = seq ( 1 + M ) ( .+ , ( NN X. { X } ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) = seq ( 1 + M ) ( .+ , ( NN X. { X } ) ) ) with typecode |-
53	52 20	fveq12d	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) = ( seq ( 1 + M ) ( .+ , ( NN X. { X } ) ) ` ( N + M ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) = ( seq ( 1 + M ) ( .+ , ( NN X. { X } ) ) ` ( N + M ) ) ) with typecode |-
54	49 51 53	3eqtr4d	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( N .x. X ) = ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( N .x. X ) = ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) ) with typecode |-
55	40 54	oveq12d	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M .x. X ) .+ ( N .x. X ) ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) .+ ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M .x. X ) .+ ( N .x. X ) ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) .+ ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) ) ) with typecode |-
56	33 38 55	3eqtr4d	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) ) with typecode |-