Theorem ressplusf

Description: The group operation function +f of a structure's restriction is the operation function's restriction to the new base. (Contributed by Thierry Arnoux, 26-Mar-2017)

	Ref	Expression
Hypotheses	ressplusf.1	|- B = ( Base ` G )
	ressplusf.2	|- H = ( G |`s A )
	ressplusf.3	|- .+^ = ( +g ` G )
	ressplusf.4	|- .+^ Fn ( B X. B )
	ressplusf.5	|- A C_ B
Assertion	ressplusf	|- ( +f ` H ) = ( .+^ |` ( A X. A ) )

Proof

Step	Hyp	Ref	Expression
1		ressplusf.1	|- B = ( Base ` G )
2		ressplusf.2	|- H = ( G |`s A )
3		ressplusf.3	|- .+^ = ( +g ` G )
4		ressplusf.4	|- .+^ Fn ( B X. B )
5		ressplusf.5	|- A C_ B
6		resmpo	|- ( ( A C_ B /\ A C_ B ) -> ( ( x e. B , y e. B |-> ( x .+^ y ) ) |` ( A X. A ) ) = ( x e. A , y e. A |-> ( x .+^ y ) ) )
7	5 5 6	mp2an	|- ( ( x e. B , y e. B |-> ( x .+^ y ) ) |` ( A X. A ) ) = ( x e. A , y e. A |-> ( x .+^ y ) )
8		fnov	|- ( .+^ Fn ( B X. B ) <-> .+^ = ( x e. B , y e. B |-> ( x .+^ y ) ) )
9	4 8	mpbi	|- .+^ = ( x e. B , y e. B |-> ( x .+^ y ) )
10	9	reseq1i	|- ( .+^ |` ( A X. A ) ) = ( ( x e. B , y e. B |-> ( x .+^ y ) ) |` ( A X. A ) )
11	2 1	ressbas2	|- ( A C_ B -> A = ( Base ` H ) )
12	5 11	ax-mp	|- A = ( Base ` H )
13	1	fvexi	|- B e. _V
14	13 5	ssexi	|- A e. _V
15		eqid	|- ( +g ` G ) = ( +g ` G )
16	2 15	ressplusg	|- ( A e. _V -> ( +g ` G ) = ( +g ` H ) )
17	14 16	ax-mp	|- ( +g ` G ) = ( +g ` H )
18	3 17	eqtri	|- .+^ = ( +g ` H )
19		eqid	|- ( +f ` H ) = ( +f ` H )
20	12 18 19	plusffval	|- ( +f ` H ) = ( x e. A , y e. A |-> ( x .+^ y ) )
21	7 10 20	3eqtr4ri	|- ( +f ` H ) = ( .+^ |` ( A X. A ) )