mulg1

Description: Group multiple (exponentiation) operation at one. (Contributed by Mario Carneiro, 11-Dec-2014)

Step	Hyp	Ref	Expression
1		mulg1.b	$⊢ B = {Base}_{G}$
2		mulg1.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		1nn	$⊢ 1 \in ℕ$
4		eqid	$⊢ +_{G} = +_{G}$
5		eqid	$⊢ seq 1 (+_{G}, (ℕ \times \{X\})) = seq 1 (+_{G}, (ℕ \times \{X\}))$
6	1 4 2 5	mulgnn	$⊢ (1 \in ℕ \land X \in B) \to 1 \underset{˙}{\cdot} X = seq 1 (+_{G}, (ℕ \times \{X\})) (1)$
7	3 6	mpan	$⊢ X \in B \to 1 \underset{˙}{\cdot} X = seq 1 (+_{G}, (ℕ \times \{X\})) (1)$
8		1z	$⊢ 1 \in ℤ$
9		fvconst2g	$⊢ (X \in B \land 1 \in ℕ) \to (ℕ \times \{X\}) (1) = X$
10	3 9	mpan2	$⊢ X \in B \to (ℕ \times \{X\}) (1) = X$
11	8 10	seq1i	$⊢ X \in B \to seq 1 (+_{G}, (ℕ \times \{X\})) (1) = X$
12	7 11	eqtrd	$⊢ X \in B \to 1 \underset{˙}{\cdot} X = X$

Metamath Proof Explorer