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	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐸 ‘ 𝑋 ) = ( 𝑍 ‘ 𝑋 ) ) )