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