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	syl5eq	|- ( 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 ) )