Metamath Proof Explorer


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 𝑠 A
ressplusf.3 ˙ = + G
ressplusf.4 ˙ Fn B × B
ressplusf.5 A B
Assertion ressplusf + 𝑓 H = ˙ A × A

Proof

Step Hyp Ref Expression
1 ressplusf.1 B = Base G
2 ressplusf.2 H = G 𝑠 A
3 ressplusf.3 ˙ = + G
4 ressplusf.4 ˙ Fn B × B
5 ressplusf.5 A B
6 resmpo A B A B x B , y B x ˙ y A × A = x A , y A x ˙ y
7 5 5 6 mp2an x B , y B x ˙ y A × A = x A , y A x ˙ y
8 fnov ˙ Fn B × B ˙ = x B , y B x ˙ y
9 4 8 mpbi ˙ = x B , y B x ˙ y
10 9 reseq1i ˙ A × A = x B , y B x ˙ y A × A
11 2 1 ressbas2 A B A = Base H
12 5 11 ax-mp A = Base H
13 1 fvexi B V
14 13 5 ssexi A V
15 eqid + G = + G
16 2 15 ressplusg A V + G = + H
17 14 16 ax-mp + G = + H
18 3 17 eqtri ˙ = + H
19 eqid + 𝑓 H = + 𝑓 H
20 12 18 19 plusffval + 𝑓 H = x A , y A x ˙ y
21 7 10 20 3eqtr4ri + 𝑓 H = ˙ A × A