Metamath Proof Explorer


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𝑠A
ressmulgnn.2 ABaseG
ressmulgnn.3 ˙=G
ressmulgnn.4 I=invgG
Assertion ressmulgnn NXANHX=N˙X

Proof

Step Hyp Ref Expression
1 ressmulgnn.1 H=G𝑠A
2 ressmulgnn.2 ABaseG
3 ressmulgnn.3 ˙=G
4 ressmulgnn.4 I=invgG
5 eqid BaseG=BaseG
6 1 5 ressbas2 ABaseGA=BaseH
7 2 6 ax-mp A=BaseH
8 eqid +H=+H
9 eqid H=H
10 fvex BaseGV
11 10 2 ssexi AV
12 eqid +G=+G
13 1 12 ressplusg AV+G=+H
14 11 13 ax-mp +G=+H
15 seqeq2 +G=+Hseq1+G×X=seq1+H×X
16 14 15 ax-mp seq1+G×X=seq1+H×X
17 7 8 9 16 mulgnn NXANHX=seq1+G×XN
18 simpr NXAXA
19 2 18 sselid NXAXBaseG
20 eqid seq1+G×X=seq1+G×X
21 5 12 3 20 mulgnn NXBaseGN˙X=seq1+G×XN
22 19 21 syldan NXAN˙X=seq1+G×XN
23 17 22 eqtr4d NXANHX=N˙X