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

Metamath Proof Explorer

Theorem mulg1

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

Ref Expression
Hypotheses mulg1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulg1.m ⊢ · = ( .g ‘ 𝐺 )
Assertion mulg1 ( 𝑋 ∈ 𝐵 → ( 1 · 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 mulg1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulg1.m ⊢ · = ( .g ‘ 𝐺 )
3 1nn ⊢ 1 ∈ ℕ
4 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5 eqid ⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) )
6 1 4 2 5 mulgnn ⊢ ( ( 1 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 1 · 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 1 ) )
7 3 6 mpan ⊢ ( 𝑋 ∈ 𝐵 → ( 1 · 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 1 ) )
8 1z ⊢ 1 ∈ ℤ
9 fvconst2g ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 1 ∈ ℕ ) → ( ( ℕ × { 𝑋 } ) ‘ 1 ) = 𝑋 )
10 3 9 mpan2 ⊢ ( 𝑋 ∈ 𝐵 → ( ( ℕ × { 𝑋 } ) ‘ 1 ) = 𝑋 )
11 8 10 seq1i ⊢ ( 𝑋 ∈ 𝐵 → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 1 ) = 𝑋 )
12 7 11 eqtrd ⊢ ( 𝑋 ∈ 𝐵 → ( 1 · 𝑋 ) = 𝑋 )