Theorem symgextres

Description: The restriction of the extension of a permutation, fixing the additional element, to the original domain. (Contributed by AV, 6-Jan-2019)

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

Proof

Step	Hyp	Ref	Expression
1		symgext.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
2		symgext.e	⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
3	1 2	symgextfv	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐸 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) )
4	3	ralrimiv	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝐸 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) )
5	1 2	symgextf	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 ⟶ 𝑁 )
6	5	ffnd	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 Fn 𝑁 )
7		eqid	⊢ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
8	7 1	symgbasf	⊢ ( 𝑍 ∈ 𝑆 → 𝑍 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) )
9	8	ffnd	⊢ ( 𝑍 ∈ 𝑆 → 𝑍 Fn ( 𝑁 ∖ { 𝐾 } ) )
10	9	adantl	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝑍 Fn ( 𝑁 ∖ { 𝐾 } ) )
11		difssd	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 )
12		fvreseq1	⊢ ( ( ( 𝐸 Fn 𝑁 ∧ 𝑍 Fn ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ) → ( ( 𝐸 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = 𝑍 ↔ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝐸 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) )
13	6 10 11 12	syl21anc	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( ( 𝐸 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = 𝑍 ↔ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝐸 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) )
14	4 13	mpbird	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝐸 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = 𝑍 )