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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ressplusf.2	⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
	ressplusf.3	⊢ ⨣ = ( +g ‘ 𝐺 )
	ressplusf.4	⊢ ⨣ Fn ( 𝐵 × 𝐵 )
	ressplusf.5	⊢ 𝐴 ⊆ 𝐵
Assertion	ressplusf	⊢ ( +𝑓 ‘ 𝐻 ) = ( ⨣ ↾ ( 𝐴 × 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ressplusf.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ressplusf.2	⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
3		ressplusf.3	⊢ ⨣ = ( +g ‘ 𝐺 )
4		ressplusf.4	⊢ ⨣ Fn ( 𝐵 × 𝐵 )
5		ressplusf.5	⊢ 𝐴 ⊆ 𝐵
6		resmpo	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ⨣ 𝑦 ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑥 ⨣ 𝑦 ) ) )
7	5 5 6	mp2an	⊢ ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ⨣ 𝑦 ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑥 ⨣ 𝑦 ) )
8		fnov	⊢ ( ⨣ Fn ( 𝐵 × 𝐵 ) ↔ ⨣ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ⨣ 𝑦 ) ) )
9	4 8	mpbi	⊢ ⨣ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ⨣ 𝑦 ) )
10	9	reseq1i	⊢ ( ⨣ ↾ ( 𝐴 × 𝐴 ) ) = ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ⨣ 𝑦 ) ) ↾ ( 𝐴 × 𝐴 ) )
11	2 1	ressbas2	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ 𝐻 ) )
12	5 11	ax-mp	⊢ 𝐴 = ( Base ‘ 𝐻 )
13	1	fvexi	⊢ 𝐵 ∈ V
14	13 5	ssexi	⊢ 𝐴 ∈ V
15		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
16	2 15	ressplusg	⊢ ( 𝐴 ∈ V → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
17	14 16	ax-mp	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 )
18	3 17	eqtri	⊢ ⨣ = ( +g ‘ 𝐻 )
19		eqid	⊢ ( +𝑓 ‘ 𝐻 ) = ( +𝑓 ‘ 𝐻 )
20	12 18 19	plusffval	⊢ ( +𝑓 ‘ 𝐻 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑥 ⨣ 𝑦 ) )
21	7 10 20	3eqtr4ri	⊢ ( +𝑓 ‘ 𝐻 ) = ( ⨣ ↾ ( 𝐴 × 𝐴 ) )