symgfixfo

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is an onto function. (Contributed by AV, 7-Jan-2019)

	Ref	Expression
Hypotheses	symgfixf.p	$⊢ P = {Base}_{SymGrp (N)}$
	symgfixf.q	$⊢ Q = \{q \in P \| q (K) = K\}$
	symgfixf.s	$⊢ S = {Base}_{SymGrp (N ∖ \{K\})}$
	symgfixf.h	$⊢ H = (q \in Q ⟼ {q ↾}_{(N ∖ \{K\})})$
Assertion	symgfixfo	$⊢ (N \in V \land K \in N) \to H : Q \underset{onto}{⟶} S$

Proof

Step	Hyp	Ref	Expression
1		symgfixf.p	$⊢ P = {Base}_{SymGrp (N)}$
2		symgfixf.q	$⊢ Q = \{q \in P \| q (K) = K\}$
3		symgfixf.s	$⊢ S = {Base}_{SymGrp (N ∖ \{K\})}$
4		symgfixf.h	$⊢ H = (q \in Q ⟼ {q ↾}_{(N ∖ \{K\})})$
5	1 2 3 4	symgfixf	$⊢ K \in N \to H : Q ⟶ S$
6	5	adantl	$⊢ (N \in V \land K \in N) \to H : Q ⟶ S$
7		eqeq1	$⊢ i = j \to (i = K \leftrightarrow j = K)$
8		fveq2	$⊢ i = j \to s (i) = s (j)$
9	7 8	ifbieq2d	$⊢ i = j \to if (i = K, K, s (i)) = if (j = K, K, s (j))$
10	9	cbvmptv	$⊢ (i \in N ⟼ if (i = K, K, s (i))) = (j \in N ⟼ if (j = K, K, s (j)))$
11	1 2 3 4 10	symgfixfolem1	$⊢ (N \in V \land K \in N \land s \in S) \to (i \in N ⟼ if (i = K, K, s (i))) \in Q$
12	11	3expa	$⊢ ((N \in V \land K \in N) \land s \in S) \to (i \in N ⟼ if (i = K, K, s (i))) \in Q$
13		simpr	$⊢ (N \in V \land K \in N) \to K \in N$
14	13	anim1i	$⊢ ((N \in V \land K \in N) \land s \in S) \to (K \in N \land s \in S)$
15	14	adantl	$⊢ (p = (i \in N ⟼ if (i = K, K, s (i))) \land ((N \in V \land K \in N) \land s \in S)) \to (K \in N \land s \in S)$
16		eqid	$⊢ (i \in N ⟼ if (i = K, K, s (i))) = (i \in N ⟼ if (i = K, K, s (i)))$
17	3 16	symgextres	$⊢ (K \in N \land s \in S) \to {(i \in N ⟼ if (i = K, K, s (i))) ↾}_{(N ∖ \{K\})} = s$
18	15 17	syl	$⊢ (p = (i \in N ⟼ if (i = K, K, s (i))) \land ((N \in V \land K \in N) \land s \in S)) \to {(i \in N ⟼ if (i = K, K, s (i))) ↾}_{(N ∖ \{K\})} = s$
19	18	eqcomd	$⊢ (p = (i \in N ⟼ if (i = K, K, s (i))) \land ((N \in V \land K \in N) \land s \in S)) \to s = {(i \in N ⟼ if (i = K, K, s (i))) ↾}_{(N ∖ \{K\})}$
20		reseq1	$⊢ p = (i \in N ⟼ if (i = K, K, s (i))) \to {p ↾}_{(N ∖ \{K\})} = {(i \in N ⟼ if (i = K, K, s (i))) ↾}_{(N ∖ \{K\})}$
21	20	eqeq2d	$⊢ p = (i \in N ⟼ if (i = K, K, s (i))) \to (s = {p ↾}_{(N ∖ \{K\})} \leftrightarrow s = {(i \in N ⟼ if (i = K, K, s (i))) ↾}_{(N ∖ \{K\})})$
22	21	adantr	$⊢ (p = (i \in N ⟼ if (i = K, K, s (i))) \land ((N \in V \land K \in N) \land s \in S)) \to (s = {p ↾}_{(N ∖ \{K\})} \leftrightarrow s = {(i \in N ⟼ if (i = K, K, s (i))) ↾}_{(N ∖ \{K\})})$
23	19 22	mpbird	$⊢ (p = (i \in N ⟼ if (i = K, K, s (i))) \land ((N \in V \land K \in N) \land s \in S)) \to s = {p ↾}_{(N ∖ \{K\})}$
24	23	ex	$⊢ p = (i \in N ⟼ if (i = K, K, s (i))) \to (((N \in V \land K \in N) \land s \in S) \to s = {p ↾}_{(N ∖ \{K\})})$
25	24	adantl	$⊢ (((N \in V \land K \in N) \land s \in S) \land p = (i \in N ⟼ if (i = K, K, s (i)))) \to (((N \in V \land K \in N) \land s \in S) \to s = {p ↾}_{(N ∖ \{K\})})$
26	12 25	rspcimedv	$⊢ ((N \in V \land K \in N) \land s \in S) \to (((N \in V \land K \in N) \land s \in S) \to \exists p \in Q s = {p ↾}_{(N ∖ \{K\})})$
27	26	pm2.43i	$⊢ ((N \in V \land K \in N) \land s \in S) \to \exists p \in Q s = {p ↾}_{(N ∖ \{K\})}$
28	4	fvtresfn	$⊢ p \in Q \to H (p) = {p ↾}_{(N ∖ \{K\})}$
29	28	eqeq2d	$⊢ p \in Q \to (s = H (p) \leftrightarrow s = {p ↾}_{(N ∖ \{K\})})$
30	29	adantl	$⊢ (((N \in V \land K \in N) \land s \in S) \land p \in Q) \to (s = H (p) \leftrightarrow s = {p ↾}_{(N ∖ \{K\})})$
31	30	rexbidva	$⊢ ((N \in V \land K \in N) \land s \in S) \to (\exists p \in Q s = H (p) \leftrightarrow \exists p \in Q s = {p ↾}_{(N ∖ \{K\})})$
32	27 31	mpbird	$⊢ ((N \in V \land K \in N) \land s \in S) \to \exists p \in Q s = H (p)$
33	32	ralrimiva	$⊢ (N \in V \land K \in N) \to \forall s \in S \exists p \in Q s = H (p)$
34		dffo3	$⊢ H : Q \underset{onto}{⟶} S \leftrightarrow (H : Q ⟶ S \land \forall s \in S \exists p \in Q s = H (p))$
35	6 33 34	sylanbrc	$⊢ (N \in V \land K \in N) \to H : Q \underset{onto}{⟶} S$

Metamath Proof Explorer

Theorem symgfixfo

Proof