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 = {Base}_{G}$
	mulgnngsum.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgnngsum.f	$⊢ F = (x \in (1 \dots N) ⟼ X)$
Assertion	mulgnn0gsum	$⊢ (N \in ℕ_{0} \land X \in B) \to N \underset{˙}{\cdot} X = \sum_{G} F$

Proof

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

Metamath Proof Explorer

Theorem mulgnn0gsum

Proof