Metamath Proof Explorer


Theorem symgfixf

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a function. (Contributed by AV, 4-Jan-2019)

Ref Expression
Hypotheses symgfixf.p P = Base SymGrp N
symgfixf.q Q = q P | q K = K
symgfixf.s S = Base SymGrp N K
symgfixf.h H = q Q q N K
Assertion symgfixf K N H : Q S

Proof

Step Hyp Ref Expression
1 symgfixf.p P = Base SymGrp N
2 symgfixf.q Q = q P | q K = K
3 symgfixf.s S = Base SymGrp N K
4 symgfixf.h H = q Q q N K
5 eqid N K = N K
6 1 2 3 5 symgfixelsi K N q Q q N K S
7 6 4 fmptd K N H : Q S