Theorem mulgnn0z

Description: A group multiple of the identity, for nonnegative multiple. (Contributed by Mario Carneiro, 13-Dec-2014)

	Ref	Expression
Hypotheses	mulgnn0z.b	$$⊢B={\mathrm{Base}}_G$$
	mulgnn0z.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mulgnn0z.o	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	mulgnn0z	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\right)\to N\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		mulgnn0z.b	$$⊢B={\mathrm{Base}}_G$$
2		mulgnn0z.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		mulgnn0z.o	$$⊢\underset{\dot{}}{0}=0_G$$
4		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
5		id	$$⊢N\in \mathbb{N}\to N\in \mathbb{N}$$
6	1 3	mndidcl	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
7		eqid	$$⊢{+}_G={+}_G$$
8		eqid	$$⊢seq1\left({+}_G,\left(\mathbb{N}\times \left\{\underset{\dot{}}{0}\right\}\right)\right)=seq1\left({+}_G,\left(\mathbb{N}\times \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
9	1 7 2 8	mulgnn	$$⊢\left(N\in \mathbb{N}\wedge \underset{\dot{}}{0}\in B\right)\to N\underset{\dot{}}{·}\underset{\dot{}}{0}=seq1\left({+}_G,\left(\mathbb{N}\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(N\right)$$
10	5 6 9	syl2anr	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in \mathbb{N}\right)\to N\underset{\dot{}}{·}\underset{\dot{}}{0}=seq1\left({+}_G,\left(\mathbb{N}\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(N\right)$$
11	1 7 3	mndlid	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{0}\in B\right)\to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
12	6 11	mpdan	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
13	12	adantr	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in \mathbb{N}\right)\to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
14		simpr	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in \mathbb{N}\right)\to N\in \mathbb{N}$$
15		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
16	14 15	eleqtrdi	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in \mathbb{N}\right)\to N\in {\mathbb{Z}}_{\ge 1}$$
17	6	adantr	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in \mathbb{N}\right)\to \underset{\dot{}}{0}\in B$$
18		elfznn	$$⊢x\in \left(1\dots N\right)\to x\in \mathbb{N}$$
19		fvconst2g	$$⊢\left(\underset{\dot{}}{0}\in B\wedge x\in \mathbb{N}\right)\to \left(\mathbb{N}\times \left\{\underset{\dot{}}{0}\right\}\right)\left(x\right)=\underset{\dot{}}{0}$$
20	17 18 19	syl2an	$$⊢\left(\left(G\in \mathrm{Mnd}\wedge N\in \mathbb{N}\right)\wedge x\in \left(1\dots N\right)\right)\to \left(\mathbb{N}\times \left\{\underset{\dot{}}{0}\right\}\right)\left(x\right)=\underset{\dot{}}{0}$$
21	13 16 20	seqid3	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in \mathbb{N}\right)\to seq1\left({+}_G,\left(\mathbb{N}\times \left\{\underset{\dot{}}{0}\right\}\right)\right)\left(N\right)=\underset{\dot{}}{0}$$
22	10 21	eqtrd	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in \mathbb{N}\right)\to N\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
23		oveq1	$$⊢N=0\to N\underset{\dot{}}{·}\underset{\dot{}}{0}=0\underset{\dot{}}{·}\underset{\dot{}}{0}$$
24	1 3 2	mulg0	$$⊢\underset{\dot{}}{0}\in B\to 0\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
25	6 24	syl	$$⊢G\in \mathrm{Mnd}\to 0\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
26	23 25	sylan9eqr	$$⊢\left(G\in \mathrm{Mnd}\wedge N=0\right)\to N\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
27	22 26	jaodan	$$⊢\left(G\in \mathrm{Mnd}\wedge \left(N\in \mathbb{N}\vee N=0\right)\right)\to N\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
28	4 27	sylan2b	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\right)\to N\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$