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

Metamath Proof Explorer

Theorem mulg2

Description: Group multiple (exponentiation) operation at two. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses mulg1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulg1.m ⊢ · = ( .g ‘ 𝐺 )
mulgnnp1.p ⊢ + = ( +g ‘ 𝐺 )
Assertion mulg2 ( 𝑋 ∈ 𝐵 → ( 2 · 𝑋 ) = ( 𝑋 + 𝑋 ) )

Proof

Step Hyp Ref Expression
1 mulg1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulg1.m ⊢ · = ( .g ‘ 𝐺 )
3 mulgnnp1.p ⊢ + = ( +g ‘ 𝐺 )
4 df-2 ⊢ 2 = ( 1 + 1 )
5 4 oveq1i ⊢ ( 2 · 𝑋 ) = ( ( 1 + 1 ) · 𝑋 )
6 1nn ⊢ 1 ∈ ℕ
7 1 2 3 mulgnnp1 ⊢ ( ( 1 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( ( 1 + 1 ) · 𝑋 ) = ( ( 1 · 𝑋 ) + 𝑋 ) )
8 6 7 mpan ⊢ ( 𝑋 ∈ 𝐵 → ( ( 1 + 1 ) · 𝑋 ) = ( ( 1 · 𝑋 ) + 𝑋 ) )
9 5 8 eqtrid ⊢ ( 𝑋 ∈ 𝐵 → ( 2 · 𝑋 ) = ( ( 1 · 𝑋 ) + 𝑋 ) )
10 1 2 mulg1 ⊢ ( 𝑋 ∈ 𝐵 → ( 1 · 𝑋 ) = 𝑋 )
11 10 oveq1d ⊢ ( 𝑋 ∈ 𝐵 → ( ( 1 · 𝑋 ) + 𝑋 ) = ( 𝑋 + 𝑋 ) )
12 9 11 eqtrd ⊢ ( 𝑋 ∈ 𝐵 → ( 2 · 𝑋 ) = ( 𝑋 + 𝑋 ) )