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

Metamath Proof Explorer

Theorem mulg0

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

Ref Expression
Hypotheses mulg0.b 
|- B = ( Base ` G )
mulg0.o 
|- .0. = ( 0g ` G )
mulg0.t 
|- .x. = ( .g ` G )
Assertion mulg0 
|- ( X e. B -> ( 0 .x. X ) = .0. )

Proof

Step Hyp Ref Expression
1 mulg0.b 
 |-  B = ( Base ` G )
2 mulg0.o 
 |-  .0. = ( 0g ` G )
3 mulg0.t 
 |-  .x. = ( .g ` G )
4 0z 
 |-  0 e. ZZ
5 eqid 
 |-  ( +g ` G ) = ( +g ` G )
6 eqid 
 |-  ( invg ` G ) = ( invg ` G )
7 eqid 
 |-  seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { X } ) )
8 1 5 2 6 3 7 mulgval 
 |-  ( ( 0 e. ZZ /\ X e. B ) -> ( 0 .x. X ) = if ( 0 = 0 , .0. , if ( 0 < 0 , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` 0 ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u 0 ) ) ) ) )
9 eqid 
 |-  0 = 0
10 9 iftruei 
 |-  if ( 0 = 0 , .0. , if ( 0 < 0 , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` 0 ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u 0 ) ) ) ) = .0.
11 8 10 eqtrdi 
 |-  ( ( 0 e. ZZ /\ X e. B ) -> ( 0 .x. X ) = .0. )
12 4 11 mpan 
 |-  ( X e. B -> ( 0 .x. X ) = .0. )