Theorem ressmulgnn

Description: Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 12-Jun-2017)

	Ref	Expression
Hypotheses	ressmulgnn.1	|- H = ( G |`s A )
	ressmulgnn.2	|- A C_ ( Base ` G )
	ressmulgnn.3	|- .* = ( .g ` G )
	ressmulgnn.4	|- I = ( invg ` G )
Assertion	ressmulgnn	|- ( ( N e. NN /\ X e. A ) -> ( N ( .g ` H ) X ) = ( N .* X ) )

Proof

Step	Hyp	Ref	Expression
1		ressmulgnn.1	|- H = ( G |`s A )
2		ressmulgnn.2	|- A C_ ( Base ` G )
3		ressmulgnn.3	|- .* = ( .g ` G )
4		ressmulgnn.4	|- I = ( invg ` G )
5		eqid	|- ( Base ` G ) = ( Base ` G )
6	1 5	ressbas2	|- ( A C_ ( Base ` G ) -> A = ( Base ` H ) )
7	2 6	ax-mp	|- A = ( Base ` H )
8		eqid	|- ( +g ` H ) = ( +g ` H )
9		eqid	|- ( .g ` H ) = ( .g ` H )
10		fvex	|- ( Base ` G ) e. _V
11	10 2	ssexi	|- A e. _V
12		eqid	|- ( +g ` G ) = ( +g ` G )
13	1 12	ressplusg	|- ( A e. _V -> ( +g ` G ) = ( +g ` H ) )
14	11 13	ax-mp	|- ( +g ` G ) = ( +g ` H )
15		seqeq2	|- ( ( +g ` G ) = ( +g ` H ) -> seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) )
16	14 15	ax-mp	|- seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) )
17	7 8 9 16	mulgnn	|- ( ( N e. NN /\ X e. A ) -> ( N ( .g ` H ) X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
18		simpr	|- ( ( N e. NN /\ X e. A ) -> X e. A )
19	2 18	sselid	|- ( ( N e. NN /\ X e. A ) -> X e. ( Base ` G ) )
20		eqid	|- seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { X } ) )
21	5 12 3 20	mulgnn	|- ( ( N e. NN /\ X e. ( Base ` G ) ) -> ( N .* X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
22	19 21	syldan	|- ( ( N e. NN /\ X e. A ) -> ( N .* X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
23	17 22	eqtr4d	|- ( ( N e. NN /\ X e. A ) -> ( N ( .g ` H ) X ) = ( N .* X ) )