Metamath Proof Explorer


Theorem symgextres

Description: The restriction of the extension of a permutation, fixing the additional element, to the original domain. (Contributed by AV, 6-Jan-2019)

Ref Expression
Hypotheses symgext.s S = Base SymGrp N K
symgext.e E = x N if x = K K Z x
Assertion symgextres K N Z S E N K = Z

Proof

Step Hyp Ref Expression
1 symgext.s S = Base SymGrp N K
2 symgext.e E = x N if x = K K Z x
3 1 2 symgextfv K N Z S i N K E i = Z i
4 3 ralrimiv K N Z S i N K E i = Z i
5 1 2 symgextf K N Z S E : N N
6 5 ffnd K N Z S E Fn N
7 eqid SymGrp N K = SymGrp N K
8 7 1 symgbasf Z S Z : N K N K
9 8 ffnd Z S Z Fn N K
10 9 adantl K N Z S Z Fn N K
11 difssd K N Z S N K N
12 fvreseq1 E Fn N Z Fn N K N K N E N K = Z i N K E i = Z i
13 6 10 11 12 syl21anc K N Z S E N K = Z i N K E i = Z i
14 4 13 mpbird K N Z S E N K = Z