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={\mathrm{Base}}_G$$
	ressplusf.2	$$⊢H=G{\upharpoonright }_{𝑠}A$$
	ressplusf.3	$$⊢\underset{\dot{}}{⨣}={+}_G$$
	ressplusf.4	$$⊢\underset{\dot{}}{⨣}Fn\left(B\times B\right)$$
	ressplusf.5	$$⊢A\subseteq B$$
Assertion	ressplusf	$$⊢{+}_{𝑓}\left(H\right)={\underset{\dot{}}{⨣}\upharpoonright }_{\left(A\times A\right)}$$

Proof

Step	Hyp	Ref	Expression
1		ressplusf.1	$$⊢B={\mathrm{Base}}_G$$
2		ressplusf.2	$$⊢H=G{\upharpoonright }_{𝑠}A$$
3		ressplusf.3	$$⊢\underset{\dot{}}{⨣}={+}_G$$
4		ressplusf.4	$$⊢\underset{\dot{}}{⨣}Fn\left(B\times B\right)$$
5		ressplusf.5	$$⊢A\subseteq B$$
6		resmpo	$$⊢\left(A\subseteq B\wedge A\subseteq B\right)\to {\left(x\in B,y\in B⟼x\underset{\dot{}}{⨣}y\right)\upharpoonright }_{\left(A\times A\right)}=\left(x\in A,y\in A⟼x\underset{\dot{}}{⨣}y\right)$$
7	5 5 6	mp2an	$$⊢{\left(x\in B,y\in B⟼x\underset{\dot{}}{⨣}y\right)\upharpoonright }_{\left(A\times A\right)}=\left(x\in A,y\in A⟼x\underset{\dot{}}{⨣}y\right)$$
8		fnov	$$⊢\underset{\dot{}}{⨣}Fn\left(B\times B\right)\leftrightarrow \underset{\dot{}}{⨣}=\left(x\in B,y\in B⟼x\underset{\dot{}}{⨣}y\right)$$
9	4 8	mpbi	$$⊢\underset{\dot{}}{⨣}=\left(x\in B,y\in B⟼x\underset{\dot{}}{⨣}y\right)$$
10	9	reseq1i	$$⊢{\underset{\dot{}}{⨣}\upharpoonright }_{\left(A\times A\right)}={\left(x\in B,y\in B⟼x\underset{\dot{}}{⨣}y\right)\upharpoonright }_{\left(A\times A\right)}$$
11	2 1	ressbas2	$$⊢A\subseteq B\to A={\mathrm{Base}}_H$$
12	5 11	ax-mp	$$⊢A={\mathrm{Base}}_H$$
13	1	fvexi	$$⊢B\in \mathrm{V}$$
14	13 5	ssexi	$$⊢A\in \mathrm{V}$$
15		eqid	$$⊢{+}_G={+}_G$$
16	2 15	ressplusg	$$⊢A\in \mathrm{V}\to {+}_G={+}_H$$
17	14 16	ax-mp	$$⊢{+}_G={+}_H$$
18	3 17	eqtri	$$⊢\underset{\dot{}}{⨣}={+}_H$$
19		eqid	$$⊢{+}_{𝑓}\left(H\right)={+}_{𝑓}\left(H\right)$$
20	12 18 19	plusffval	$$⊢{+}_{𝑓}\left(H\right)=\left(x\in A,y\in A⟼x\underset{\dot{}}{⨣}y\right)$$
21	7 10 20	3eqtr4ri	$$⊢{+}_{𝑓}\left(H\right)={\underset{\dot{}}{⨣}\upharpoonright }_{\left(A\times A\right)}$$