Metamath Proof Explorer

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	$⊢ S = {Base}_{SymGrp (N ∖ \{K\})}$
		symgext.e	$⊢ E = (x \in N ⟼ if (x = K, K, Z (x)))$
	Assertion	symgextres	$⊢ (K \in N \land Z \in S) \to {E ↾}_{(N ∖ \{K\})} = Z$

Proof

Step	Hyp	Ref	Expression
1		symgext.s	$⊢ S = {Base}_{SymGrp (N ∖ \{K\})}$
2		symgext.e	$⊢ E = (x \in N ⟼ if (x = K, K, Z (x)))$
3	1 2	symgextfv	$⊢ (K \in N \land Z \in S) \to (i \in (N ∖ \{K\}) \to E (i) = Z (i))$
4	3	ralrimiv	$⊢ (K \in N \land Z \in S) \to \forall i \in (N ∖ \{K\}) E (i) = Z (i)$
5	1 2	symgextf	$⊢ (K \in N \land Z \in S) \to E : N ⟶ N$
6	5	ffnd	$⊢ (K \in N \land Z \in S) \to E Fn N$
7		eqid	$⊢ SymGrp (N ∖ \{K\}) = SymGrp (N ∖ \{K\})$
8	7 1	symgbasf	$⊢ Z \in S \to Z : N ∖ \{K\} ⟶ N ∖ \{K\}$
9	8	ffnd	$⊢ Z \in S \to Z Fn (N ∖ \{K\})$
10	9	adantl	$⊢ (K \in N \land Z \in S) \to Z Fn (N ∖ \{K\})$
11		difssd	$⊢ (K \in N \land Z \in S) \to N ∖ \{K\} \subseteq N$
12		fvreseq1	$⊢ ((E Fn N \land Z Fn (N ∖ \{K\})) \land N ∖ \{K\} \subseteq N) \to ({E ↾}_{(N ∖ \{K\})} = Z \leftrightarrow \forall i \in (N ∖ \{K\}) E (i) = Z (i))$
13	6 10 11 12	syl21anc	$⊢ (K \in N \land Z \in S) \to ({E ↾}_{(N ∖ \{K\})} = Z \leftrightarrow \forall i \in (N ∖ \{K\}) E (i) = Z (i))$
14	4 13	mpbird	$⊢ (K \in N \land Z \in S) \to {E ↾}_{(N ∖ \{K\})} = Z$