Theorem mulgnn0gsum

Description: Group multiple (exponentiation) operation at a nonnegative integer expressed by a group sum. This corresponds to the definition in Lang p. 6, second formula. (Contributed by AV, 28-Dec-2023)

	Ref	Expression
Hypotheses	mulgnngsum.b	$$⊢B={\mathrm{Base}}_G$$
	mulgnngsum.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mulgnngsum.f	$$⊢F=\left(x\in \left(1\dots N\right)⟼X\right)$$
Assertion	mulgnn0gsum	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in B\right)\to N\underset{\dot{}}{·}X={\sum }_{G}F$$

Proof

Step	Hyp	Ref	Expression
1		mulgnngsum.b	$$⊢B={\mathrm{Base}}_G$$
2		mulgnngsum.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		mulgnngsum.f	$$⊢F=\left(x\in \left(1\dots N\right)⟼X\right)$$
4		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
5	1 2 3	mulgnngsum	$$⊢\left(N\in \mathbb{N}\wedge X\in B\right)\to N\underset{\dot{}}{·}X={\sum }_{G}F$$
6	5	ex	$$⊢N\in \mathbb{N}\to \left(X\in B\to N\underset{\dot{}}{·}X={\sum }_{G}F\right)$$
7		oveq1	$$⊢N=0\to N\underset{\dot{}}{·}X=0\underset{\dot{}}{·}X$$
8		eqid	$$⊢0_G=0_G$$
9	1 8 2	mulg0	$$⊢X\in B\to 0\underset{\dot{}}{·}X=0_G$$
10	7 9	sylan9eq	$$⊢\left(N=0\wedge X\in B\right)\to N\underset{\dot{}}{·}X=0_G$$
11		oveq2	$$⊢N=0\to \left(1\dots N\right)=\left(1\dots 0\right)$$
12		fz10	$$⊢\left(1\dots 0\right)=\varnothing$$
13	11 12	eqtrdi	$$⊢N=0\to \left(1\dots N\right)=\varnothing$$
14		eqidd	$$⊢N=0\to X=X$$
15	13 14	mpteq12dv	$$⊢N=0\to \left(x\in \left(1\dots N\right)⟼X\right)=\left(x\in \varnothing ⟼X\right)$$
16		mpt0	$$⊢\left(x\in \varnothing ⟼X\right)=\varnothing$$
17	15 16	eqtrdi	$$⊢N=0\to \left(x\in \left(1\dots N\right)⟼X\right)=\varnothing$$
18	3 17	eqtrid	$$⊢N=0\to F=\varnothing$$
19	18	adantr	$$⊢\left(N=0\wedge X\in B\right)\to F=\varnothing$$
20	19	oveq2d	$$⊢\left(N=0\wedge X\in B\right)\to {\sum }_{G}F={\sum }_G\varnothing$$
21	8	gsum0	$$⊢{\sum }_G\varnothing =0_G$$
22	20 21	eqtrdi	$$⊢\left(N=0\wedge X\in B\right)\to {\sum }_{G}F=0_G$$
23	10 22	eqtr4d	$$⊢\left(N=0\wedge X\in B\right)\to N\underset{\dot{}}{·}X={\sum }_{G}F$$
24	23	ex	$$⊢N=0\to \left(X\in B\to N\underset{\dot{}}{·}X={\sum }_{G}F\right)$$
25	6 24	jaoi	$$⊢\left(N\in \mathbb{N}\vee N=0\right)\to \left(X\in B\to N\underset{\dot{}}{·}X={\sum }_{G}F\right)$$
26	4 25	sylbi	$$⊢N\in {\mathbb{N}}_0\to \left(X\in B\to N\underset{\dot{}}{·}X={\sum }_{G}F\right)$$
27	26	imp	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in B\right)\to N\underset{\dot{}}{·}X={\sum }_{G}F$$