Theorem mulgnn0gsum

Description: Group multiple (exponentiation) operation at a nonnegative integer expressed by a group sum. This corresponds to the definition in Lang p. 6, second formula. (Contributed by AV, 28-Dec-2023)

	Ref	Expression
Hypotheses	mulgnngsum.b	|- B = ( Base ` G )
	mulgnngsum.t	|- .x. = ( .g ` G )
	mulgnngsum.f	|- F = ( x e. ( 1 ... N ) |-> X )
Assertion	mulgnn0gsum	|- ( ( N e. NN0 /\ X e. B ) -> ( N .x. X ) = ( G gsum F ) )

Proof

Step	Hyp	Ref	Expression
1		mulgnngsum.b	|- B = ( Base ` G )
2		mulgnngsum.t	|- .x. = ( .g ` G )
3		mulgnngsum.f	|- F = ( x e. ( 1 ... N ) |-> X )
4		elnn0	|- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
5	1 2 3	mulgnngsum	|- ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( G gsum F ) )
6	5	ex	|- ( N e. NN -> ( X e. B -> ( N .x. X ) = ( G gsum F ) ) )
7		oveq1	|- ( N = 0 -> ( N .x. X ) = ( 0 .x. X ) )
8		eqid	|- ( 0g ` G ) = ( 0g ` G )
9	1 8 2	mulg0	|- ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
10	7 9	sylan9eq	|- ( ( N = 0 /\ X e. B ) -> ( N .x. X ) = ( 0g ` G ) )
11		oveq2	|- ( N = 0 -> ( 1 ... N ) = ( 1 ... 0 ) )
12		fz10	|- ( 1 ... 0 ) = (/)
13	11 12	eqtrdi	|- ( N = 0 -> ( 1 ... N ) = (/) )
14		eqidd	|- ( N = 0 -> X = X )
15	13 14	mpteq12dv	|- ( N = 0 -> ( x e. ( 1 ... N ) |-> X ) = ( x e. (/) |-> X ) )
16		mpt0	|- ( x e. (/) |-> X ) = (/)
17	15 16	eqtrdi	|- ( N = 0 -> ( x e. ( 1 ... N ) |-> X ) = (/) )
18	3 17	eqtrid	|- ( N = 0 -> F = (/) )
19	18	adantr	|- ( ( N = 0 /\ X e. B ) -> F = (/) )
20	19	oveq2d	|- ( ( N = 0 /\ X e. B ) -> ( G gsum F ) = ( G gsum (/) ) )
21	8	gsum0	|- ( G gsum (/) ) = ( 0g ` G )
22	20 21	eqtrdi	|- ( ( N = 0 /\ X e. B ) -> ( G gsum F ) = ( 0g ` G ) )
23	10 22	eqtr4d	|- ( ( N = 0 /\ X e. B ) -> ( N .x. X ) = ( G gsum F ) )
24	23	ex	|- ( N = 0 -> ( X e. B -> ( N .x. X ) = ( G gsum F ) ) )
25	6 24	jaoi	|- ( ( N e. NN \/ N = 0 ) -> ( X e. B -> ( N .x. X ) = ( G gsum F ) ) )
26	4 25	sylbi	|- ( N e. NN0 -> ( X e. B -> ( N .x. X ) = ( G gsum F ) ) )
27	26	imp	|- ( ( N e. NN0 /\ X e. B ) -> ( N .x. X ) = ( G gsum F ) )