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	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
	symgext.e	⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
Assertion	symgextsymg	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		symgext.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
2		symgext.e	⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
3	1 2	symgextf1o	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 –1-1-onto→ 𝑁 )
4	3	3adant1	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 –1-1-onto→ 𝑁 )
5		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
6		eqid	⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
7	5 6	elsymgbas	⊢ ( 𝑁 ∈ 𝑉 → ( 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↔ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ) )
8	7	3ad2ant1	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↔ 𝐸 : 𝑁 –1-1-onto→ 𝑁 ) )
9	4 8	mpbird	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) )