Theorem mulg0

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

	Ref	Expression
Hypotheses	mulg0.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mulg0.o	⊢ 0 = ( 0g ‘ 𝐺 )
	mulg0.t	⊢ · = ( .g ‘ 𝐺 )
Assertion	mulg0	⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		mulg0.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mulg0.o	⊢ 0 = ( 0g ‘ 𝐺 )
3		mulg0.t	⊢ · = ( .g ‘ 𝐺 )
4		0z	⊢ 0 ∈ ℤ
5		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
7		eqid	⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) )
8	1 5 2 6 3 7	mulgval	⊢ ( ( 0 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = if ( 0 = 0 , 0 , if ( 0 < 0 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 0 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 0 ) ) ) ) )
9		eqid	⊢ 0 = 0
10	9	iftruei	⊢ if ( 0 = 0 , 0 , if ( 0 < 0 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 0 ) , ( ( invg ‘ 𝐺 ) ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 0 ) ) ) ) = 0
11	8 10	eqtrdi	⊢ ( ( 0 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = 0 )
12	4 11	mpan	⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = 0 )