Metamath Proof Explorer


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 ‘ 𝑁 ) ) )