Theorem mulg1

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

	Ref	Expression
Hypotheses	mulg1.b	|- B = ( Base ` G )
	mulg1.m	|- .x. = ( .g ` G )
Assertion	mulg1	|- ( X e. B -> ( 1 .x. X ) = X )

Proof

Step	Hyp	Ref	Expression
1		mulg1.b	|- B = ( Base ` G )
2		mulg1.m	|- .x. = ( .g ` G )
3		1nn	|- 1 e. NN
4		eqid	|- ( +g ` G ) = ( +g ` G )
5		eqid	|- seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { X } ) )
6	1 4 2 5	mulgnn	|- ( ( 1 e. NN /\ X e. B ) -> ( 1 .x. X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` 1 ) )
7	3 6	mpan	|- ( X e. B -> ( 1 .x. X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` 1 ) )
8		1z	|- 1 e. ZZ
9		fvconst2g	|- ( ( X e. B /\ 1 e. NN ) -> ( ( NN X. { X } ) ` 1 ) = X )
10	3 9	mpan2	|- ( X e. B -> ( ( NN X. { X } ) ` 1 ) = X )
11	8 10	seq1i	|- ( X e. B -> ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` 1 ) = X )
12	7 11	eqtrd	|- ( X e. B -> ( 1 .x. X ) = X )