Description: The function value of the extension of a permutation, fixing the additional element, for the additional element. (Contributed by AV, 6-Jan-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | symgext.s | ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) | |
symgext.e | ⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) ) | ||
Assertion | symgextfve | ⊢ ( 𝐾 ∈ 𝑁 → ( 𝑋 = 𝐾 → ( 𝐸 ‘ 𝑋 ) = 𝐾 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | symgext.s | ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) | |
2 | symgext.e | ⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) ) | |
3 | fveq2 | ⊢ ( 𝑋 = 𝐾 → ( 𝐸 ‘ 𝑋 ) = ( 𝐸 ‘ 𝐾 ) ) | |
4 | iftrue | ⊢ ( 𝑥 = 𝐾 → if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) = 𝐾 ) | |
5 | 4 2 | fvmptg | ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐸 ‘ 𝐾 ) = 𝐾 ) |
6 | 5 | anidms | ⊢ ( 𝐾 ∈ 𝑁 → ( 𝐸 ‘ 𝐾 ) = 𝐾 ) |
7 | 3 6 | sylan9eqr | ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑋 = 𝐾 ) → ( 𝐸 ‘ 𝑋 ) = 𝐾 ) |
8 | 7 | ex | ⊢ ( 𝐾 ∈ 𝑁 → ( 𝑋 = 𝐾 → ( 𝐸 ‘ 𝑋 ) = 𝐾 ) ) |