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