symgfixf1

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a 1-1 function. (Contributed by AV, 4-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	symgfixf1	$⊢ K \in N \to H : Q \underset{1-1}{⟶} 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	4	fvtresfn	$⊢ g \in Q \to H (g) = {g ↾}_{(N ∖ \{K\})}$
7	4	fvtresfn	$⊢ p \in Q \to H (p) = {p ↾}_{(N ∖ \{K\})}$
8	6 7	eqeqan12d	$⊢ (g \in Q \land p \in Q) \to (H (g) = H (p) \leftrightarrow {g ↾}_{(N ∖ \{K\})} = {p ↾}_{(N ∖ \{K\})})$
9	8	adantl	$⊢ (K \in N \land (g \in Q \land p \in Q)) \to (H (g) = H (p) \leftrightarrow {g ↾}_{(N ∖ \{K\})} = {p ↾}_{(N ∖ \{K\})})$
10	1 2	symgfixelq	$⊢ g \in V \to (g \in Q \leftrightarrow (g : N \underset{1-1 onto}{⟶} N \land g (K) = K))$
11	10	elv	$⊢ g \in Q \leftrightarrow (g : N \underset{1-1 onto}{⟶} N \land g (K) = K)$
12	1 2	symgfixelq	$⊢ p \in V \to (p \in Q \leftrightarrow (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))$
13	12	elv	$⊢ p \in Q \leftrightarrow (p : N \underset{1-1 onto}{⟶} N \land p (K) = K)$
14	11 13	anbi12i	$⊢ (g \in Q \land p \in Q) \leftrightarrow ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))$
15		f1ofn	$⊢ g : N \underset{1-1 onto}{⟶} N \to g Fn N$
16	15	adantr	$⊢ (g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \to g Fn N$
17		f1ofn	$⊢ p : N \underset{1-1 onto}{⟶} N \to p Fn N$
18	17	adantr	$⊢ (p : N \underset{1-1 onto}{⟶} N \land p (K) = K) \to p Fn N$
19	16 18	anim12i	$⊢ ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K)) \to (g Fn N \land p Fn N)$
20		difss	$⊢ N ∖ \{K\} \subseteq N$
21	19 20	jctir	$⊢ ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K)) \to ((g Fn N \land p Fn N) \land N ∖ \{K\} \subseteq N)$
22	21	adantl	$⊢ (K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \to ((g Fn N \land p Fn N) \land N ∖ \{K\} \subseteq N)$
23		fvreseq	$⊢ ((g Fn N \land p Fn N) \land N ∖ \{K\} \subseteq N) \to ({g ↾}_{(N ∖ \{K\})} = {p ↾}_{(N ∖ \{K\})} \leftrightarrow \forall i \in (N ∖ \{K\}) g (i) = p (i))$
24	22 23	syl	$⊢ (K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \to ({g ↾}_{(N ∖ \{K\})} = {p ↾}_{(N ∖ \{K\})} \leftrightarrow \forall i \in (N ∖ \{K\}) g (i) = p (i))$
25		f1of	$⊢ g : N \underset{1-1 onto}{⟶} N \to g : N ⟶ N$
26	25	adantr	$⊢ (g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \to g : N ⟶ N$
27		f1of	$⊢ p : N \underset{1-1 onto}{⟶} N \to p : N ⟶ N$
28	27	adantr	$⊢ (p : N \underset{1-1 onto}{⟶} N \land p (K) = K) \to p : N ⟶ N$
29		fdm	$⊢ g : N ⟶ N \to dom g = N$
30		fdm	$⊢ p : N ⟶ N \to dom p = N$
31	29 30	anim12i	$⊢ (g : N ⟶ N \land p : N ⟶ N) \to (dom g = N \land dom p = N)$
32	26 28 31	syl2an	$⊢ ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K)) \to (dom g = N \land dom p = N)$
33		eqtr3	$⊢ (dom g = N \land dom p = N) \to dom g = dom p$
34	32 33	syl	$⊢ ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K)) \to dom g = dom p$
35	34	ad2antlr	$⊢ ((K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \land \forall i \in (N ∖ \{K\}) g (i) = p (i)) \to dom g = dom p$
36		simpr	$⊢ ((K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \land \forall i \in (N ∖ \{K\}) g (i) = p (i)) \to \forall i \in (N ∖ \{K\}) g (i) = p (i)$
37		eqtr3	$⊢ (g (K) = K \land p (K) = K) \to g (K) = p (K)$
38	37	ad2ant2l	$⊢ ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K)) \to g (K) = p (K)$
39	38	ad2antlr	$⊢ ((K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \land \forall i \in (N ∖ \{K\}) g (i) = p (i)) \to g (K) = p (K)$
40		fveq2	$⊢ i = K \to g (i) = g (K)$
41		fveq2	$⊢ i = K \to p (i) = p (K)$
42	40 41	eqeq12d	$⊢ i = K \to (g (i) = p (i) \leftrightarrow g (K) = p (K))$
43	42	ralunsn	$⊢ K \in N \to (\forall i \in ((N ∖ \{K\}) \cup \{K\}) g (i) = p (i) \leftrightarrow (\forall i \in (N ∖ \{K\}) g (i) = p (i) \land g (K) = p (K)))$
44	43	adantr	$⊢ (K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \to (\forall i \in ((N ∖ \{K\}) \cup \{K\}) g (i) = p (i) \leftrightarrow (\forall i \in (N ∖ \{K\}) g (i) = p (i) \land g (K) = p (K)))$
45	44	adantr	$⊢ ((K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \land \forall i \in (N ∖ \{K\}) g (i) = p (i)) \to (\forall i \in ((N ∖ \{K\}) \cup \{K\}) g (i) = p (i) \leftrightarrow (\forall i \in (N ∖ \{K\}) g (i) = p (i) \land g (K) = p (K)))$
46	36 39 45	mpbir2and	$⊢ ((K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \land \forall i \in (N ∖ \{K\}) g (i) = p (i)) \to \forall i \in ((N ∖ \{K\}) \cup \{K\}) g (i) = p (i)$
47		f1odm	$⊢ g : N \underset{1-1 onto}{⟶} N \to dom g = N$
48	47	adantr	$⊢ (g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \to dom g = N$
49	48	adantr	$⊢ ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K)) \to dom g = N$
50		difsnid	$⊢ K \in N \to (N ∖ \{K\}) \cup \{K\} = N$
51	50	eqcomd	$⊢ K \in N \to N = (N ∖ \{K\}) \cup \{K\}$
52	49 51	sylan9eqr	$⊢ (K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \to dom g = (N ∖ \{K\}) \cup \{K\}$
53	52	adantr	$⊢ ((K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \land \forall i \in (N ∖ \{K\}) g (i) = p (i)) \to dom g = (N ∖ \{K\}) \cup \{K\}$
54	53	raleqdv	$⊢ ((K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \land \forall i \in (N ∖ \{K\}) g (i) = p (i)) \to (\forall i \in dom g g (i) = p (i) \leftrightarrow \forall i \in ((N ∖ \{K\}) \cup \{K\}) g (i) = p (i))$
55	46 54	mpbird	$⊢ ((K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \land \forall i \in (N ∖ \{K\}) g (i) = p (i)) \to \forall i \in dom g g (i) = p (i)$
56		f1ofun	$⊢ g : N \underset{1-1 onto}{⟶} N \to Fun g$
57	56	adantr	$⊢ (g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \to Fun g$
58		f1ofun	$⊢ p : N \underset{1-1 onto}{⟶} N \to Fun p$
59	58	adantr	$⊢ (p : N \underset{1-1 onto}{⟶} N \land p (K) = K) \to Fun p$
60	57 59	anim12i	$⊢ ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K)) \to (Fun g \land Fun p)$
61	60	ad2antlr	$⊢ ((K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \land \forall i \in (N ∖ \{K\}) g (i) = p (i)) \to (Fun g \land Fun p)$
62		eqfunfv	$⊢ (Fun g \land Fun p) \to (g = p \leftrightarrow (dom g = dom p \land \forall i \in dom g g (i) = p (i)))$
63	61 62	syl	$⊢ ((K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \land \forall i \in (N ∖ \{K\}) g (i) = p (i)) \to (g = p \leftrightarrow (dom g = dom p \land \forall i \in dom g g (i) = p (i)))$
64	35 55 63	mpbir2and	$⊢ ((K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \land \forall i \in (N ∖ \{K\}) g (i) = p (i)) \to g = p$
65	64	ex	$⊢ (K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \to (\forall i \in (N ∖ \{K\}) g (i) = p (i) \to g = p)$
66	24 65	sylbid	$⊢ (K \in N \land ((g : N \underset{1-1 onto}{⟶} N \land g (K) = K) \land (p : N \underset{1-1 onto}{⟶} N \land p (K) = K))) \to ({g ↾}_{(N ∖ \{K\})} = {p ↾}_{(N ∖ \{K\})} \to g = p)$
67	14 66	sylan2b	$⊢ (K \in N \land (g \in Q \land p \in Q)) \to ({g ↾}_{(N ∖ \{K\})} = {p ↾}_{(N ∖ \{K\})} \to g = p)$
68	9 67	sylbid	$⊢ (K \in N \land (g \in Q \land p \in Q)) \to (H (g) = H (p) \to g = p)$
69	68	ralrimivva	$⊢ K \in N \to \forall g \in Q \forall p \in Q (H (g) = H (p) \to g = p)$
70		dff13	$⊢ H : Q \underset{1-1}{⟶} S \leftrightarrow (H : Q ⟶ S \land \forall g \in Q \forall p \in Q (H (g) = H (p) \to g = p))$
71	5 69 70	sylanbrc	$⊢ K \in N \to H : Q \underset{1-1}{⟶} S$

Metamath Proof Explorer

Theorem symgfixf1

Proof