mulg0

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

	Ref	Expression
Hypotheses	mulg0.b	$⊢ B = {Base}_{G}$
	mulg0.o	$⊢ \underset{˙}{0} = 0_{G}$
	mulg0.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		mulg0.b	$⊢ B = {Base}_{G}$
2		mulg0.o	$⊢ \underset{˙}{0} = 0_{G}$
3		mulg0.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		0z	$⊢ 0 \in ℤ$
5		eqid	$⊢ +_{G} = +_{G}$
6		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
7		eqid	$⊢ seq 1 (+_{G}, (ℕ \times \{X\})) = seq 1 (+_{G}, (ℕ \times \{X\}))$
8	1 5 2 6 3 7	mulgval	$⊢ (0 \in ℤ \land X \in B) \to 0 \underset{˙}{\cdot} X = if (0 = 0, \underset{˙}{0}, if (0 < 0, seq 1 (+_{G}, (ℕ \times \{X\})) (0), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- 0))))$
9		eqid	$⊢ 0 = 0$
10	9	iftruei	$⊢ if (0 = 0, \underset{˙}{0}, if (0 < 0, seq 1 (+_{G}, (ℕ \times \{X\})) (0), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- 0)))) = \underset{˙}{0}$
11	8 10	eqtrdi	$⊢ (0 \in ℤ \land X \in B) \to 0 \underset{˙}{\cdot} X = \underset{˙}{0}$
12	4 11	mpan	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = \underset{˙}{0}$

Metamath Proof Explorer