Metamath Proof Explorer


Theorem symgextfv

Description: The function value of the extension of a permutation, fixing the additional element, for elements in the original domain. (Contributed by AV, 6-Jan-2019)

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

Proof

Step Hyp Ref Expression
1 symgext.s 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
2 symgext.e 𝐸 = ( 𝑥𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍𝑥 ) ) )
3 eldifi ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) → 𝑋𝑁 )
4 fvexd ( ( 𝐾𝑁𝑍𝑆 ) → ( 𝑍𝑋 ) ∈ V )
5 ifexg ( ( 𝐾𝑁 ∧ ( 𝑍𝑋 ) ∈ V ) → if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍𝑋 ) ) ∈ V )
6 4 5 syldan ( ( 𝐾𝑁𝑍𝑆 ) → if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍𝑋 ) ) ∈ V )
7 eqeq1 ( 𝑥 = 𝑋 → ( 𝑥 = 𝐾𝑋 = 𝐾 ) )
8 fveq2 ( 𝑥 = 𝑋 → ( 𝑍𝑥 ) = ( 𝑍𝑋 ) )
9 7 8 ifbieq2d ( 𝑥 = 𝑋 → if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍𝑥 ) ) = if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍𝑋 ) ) )
10 9 2 fvmptg ( ( 𝑋𝑁 ∧ if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍𝑋 ) ) ∈ V ) → ( 𝐸𝑋 ) = if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍𝑋 ) ) )
11 3 6 10 syl2anr ( ( ( 𝐾𝑁𝑍𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝐸𝑋 ) = if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍𝑋 ) ) )
12 eldifsnneq ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) → ¬ 𝑋 = 𝐾 )
13 12 adantl ( ( ( 𝐾𝑁𝑍𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ¬ 𝑋 = 𝐾 )
14 13 iffalsed ( ( ( 𝐾𝑁𝑍𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍𝑋 ) ) = ( 𝑍𝑋 ) )
15 11 14 eqtrd ( ( ( 𝐾𝑁𝑍𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝐸𝑋 ) = ( 𝑍𝑋 ) )
16 15 ex ( ( 𝐾𝑁𝑍𝑆 ) → ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐸𝑋 ) = ( 𝑍𝑋 ) ) )