Theorem symgextsymg

Description: The extension of a permutation is an element of the extended symmetric group. (Contributed by AV, 9-Mar-2019)

	Ref	Expression
Hypotheses	symgext.s	$$⊢S={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
	symgext.e	$$⊢E=\left(x\in N⟼if\left(x=K,K,Z\left(x\right)\right)\right)$$
Assertion	symgextsymg	$$⊢\left(N\in V\wedge K\in N\wedge Z\in S\right)\to E\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$

Proof

Step	Hyp	Ref	Expression
1		symgext.s	$$⊢S={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
2		symgext.e	$$⊢E=\left(x\in N⟼if\left(x=K,K,Z\left(x\right)\right)\right)$$
3	1 2	symgextf1o	$$⊢\left(K\in N\wedge Z\in S\right)\to E:N\underset{1-1\; onto}{⟶}N$$
4	3	3adant1	$$⊢\left(N\in V\wedge K\in N\wedge Z\in S\right)\to E:N\underset{1-1\; onto}{⟶}N$$
5		eqid	$$⊢\mathrm{SymGrp}\left(N\right)=\mathrm{SymGrp}\left(N\right)$$
6		eqid	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
7	5 6	elsymgbas	$$⊢N\in V\to \left(E\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}\leftrightarrow E:N\underset{1-1\; onto}{⟶}N\right)$$
8	7	3ad2ant1	$$⊢\left(N\in V\wedge K\in N\wedge Z\in S\right)\to \left(E\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}\leftrightarrow E:N\underset{1-1\; onto}{⟶}N\right)$$
9	4 8	mpbird	$$⊢\left(N\in V\wedge K\in N\wedge Z\in S\right)\to E\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$