This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )