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 
|- B = ( Base ` G )
mulg1.m 
|- .x. = ( .g ` G )
mulgnnp1.p 
|- .+ = ( +g ` G )
Assertion mulg2 
|- ( X e. B -> ( 2 .x. X ) = ( X .+ X ) )

Proof

Step Hyp Ref Expression
1 mulg1.b 
 |-  B = ( Base ` G )
2 mulg1.m 
 |-  .x. = ( .g ` G )
3 mulgnnp1.p 
 |-  .+ = ( +g ` G )
4 df-2 
 |-  2 = ( 1 + 1 )
5 4 oveq1i 
 |-  ( 2 .x. X ) = ( ( 1 + 1 ) .x. X )
6 1nn 
 |-  1 e. NN
7 1 2 3 mulgnnp1 
 |-  ( ( 1 e. NN /\ X e. B ) -> ( ( 1 + 1 ) .x. X ) = ( ( 1 .x. X ) .+ X ) )
8 6 7 mpan 
 |-  ( X e. B -> ( ( 1 + 1 ) .x. X ) = ( ( 1 .x. X ) .+ X ) )
9 5 8 eqtrid 
 |-  ( X e. B -> ( 2 .x. X ) = ( ( 1 .x. X ) .+ X ) )
10 1 2 mulg1 
 |-  ( X e. B -> ( 1 .x. X ) = X )
11 10 oveq1d 
 |-  ( X e. B -> ( ( 1 .x. X ) .+ X ) = ( X .+ X ) )
12 9 11 eqtrd 
 |-  ( X e. B -> ( 2 .x. X ) = ( X .+ X ) )