This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem symgextf

Description: The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019)

Ref Expression
Hypotheses symgext.s ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
symgext.e ⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
Assertion symgextf ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 ⟶ 𝑁 )

Proof

Step Hyp Ref Expression
1 symgext.s ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
2 symgext.e ⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
3 simplll ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ 𝑥 = 𝐾 ) → 𝐾 ∈ 𝑁 )
4 simpllr ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ¬ 𝑥 = 𝐾 ) → 𝑍 ∈ 𝑆 )
5 simpr ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
6 neqne ⊢ ( ¬ 𝑥 = 𝐾 → 𝑥 ≠ 𝐾 )
7 5 6 anim12i ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ¬ 𝑥 = 𝐾 ) → ( 𝑥 ∈ 𝑁 ∧ 𝑥 ≠ 𝐾 ) )
8 eldifsn ⊢ ( 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ↔ ( 𝑥 ∈ 𝑁 ∧ 𝑥 ≠ 𝐾 ) )
9 7 8 sylibr ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ¬ 𝑥 = 𝐾 ) → 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) )
10 eqid ⊢ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
11 10 1 symgfv ⊢ ( ( 𝑍 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑍 ‘ 𝑥 ) ∈ ( 𝑁 ∖ { 𝐾 } ) )
12 4 9 11 syl2anc ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ¬ 𝑥 = 𝐾 ) → ( 𝑍 ‘ 𝑥 ) ∈ ( 𝑁 ∖ { 𝐾 } ) )
13 12 eldifad ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ¬ 𝑥 = 𝐾 ) → ( 𝑍 ‘ 𝑥 ) ∈ 𝑁 )
14 3 13 ifclda ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) → if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) ∈ 𝑁 )
15 14 2 fmptd ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 ⟶ 𝑁 )