symgextf1

Description: The extension of a permutation, fixing the additional element, is a 1-1 function. (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	symgextf1	$⊢ (K \in N \land Z \in S) \to E : N \underset{1-1}{⟶} N$

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	symgextf	$⊢ (K \in N \land Z \in S) \to E : N ⟶ N$
4		difsnid	$⊢ K \in N \to (N ∖ \{K\}) \cup \{K\} = N$
5	4	eqcomd	$⊢ K \in N \to N = (N ∖ \{K\}) \cup \{K\}$
6	5	eleq2d	$⊢ K \in N \to (y \in N \leftrightarrow y \in ((N ∖ \{K\}) \cup \{K\}))$
7	5	eleq2d	$⊢ K \in N \to (z \in N \leftrightarrow z \in ((N ∖ \{K\}) \cup \{K\}))$
8	6 7	anbi12d	$⊢ K \in N \to ((y \in N \land z \in N) \leftrightarrow (y \in ((N ∖ \{K\}) \cup \{K\}) \land z \in ((N ∖ \{K\}) \cup \{K\})))$
9	8	adantr	$⊢ (K \in N \land Z \in S) \to ((y \in N \land z \in N) \leftrightarrow (y \in ((N ∖ \{K\}) \cup \{K\}) \land z \in ((N ∖ \{K\}) \cup \{K\})))$
10		elun	$⊢ y \in ((N ∖ \{K\}) \cup \{K\}) \leftrightarrow (y \in (N ∖ \{K\}) \lor y \in \{K\})$
11		elun	$⊢ z \in ((N ∖ \{K\}) \cup \{K\}) \leftrightarrow (z \in (N ∖ \{K\}) \lor z \in \{K\})$
12	1 2	symgextfv	$⊢ (K \in N \land Z \in S) \to (y \in (N ∖ \{K\}) \to E (y) = Z (y))$
13	12	com12	$⊢ y \in (N ∖ \{K\}) \to ((K \in N \land Z \in S) \to E (y) = Z (y))$
14	13	adantr	$⊢ (y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \to ((K \in N \land Z \in S) \to E (y) = Z (y))$
15	14	imp	$⊢ ((y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \land (K \in N \land Z \in S)) \to E (y) = Z (y)$
16	1 2	symgextfv	$⊢ (K \in N \land Z \in S) \to (z \in (N ∖ \{K\}) \to E (z) = Z (z))$
17	16	com12	$⊢ z \in (N ∖ \{K\}) \to ((K \in N \land Z \in S) \to E (z) = Z (z))$
18	17	adantl	$⊢ (y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \to ((K \in N \land Z \in S) \to E (z) = Z (z))$
19	18	imp	$⊢ ((y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \land (K \in N \land Z \in S)) \to E (z) = Z (z)$
20	15 19	eqeq12d	$⊢ ((y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \land (K \in N \land Z \in S)) \to (E (y) = E (z) \leftrightarrow Z (y) = Z (z))$
21		eqid	$⊢ SymGrp (N ∖ \{K\}) = SymGrp (N ∖ \{K\})$
22	21 1	symgbasf1o	$⊢ Z \in S \to Z : N ∖ \{K\} \underset{1-1 onto}{⟶} N ∖ \{K\}$
23		f1of1	$⊢ Z : N ∖ \{K\} \underset{1-1 onto}{⟶} N ∖ \{K\} \to Z : N ∖ \{K\} \underset{1-1}{⟶} N ∖ \{K\}$
24		dff13	$⊢ Z : N ∖ \{K\} \underset{1-1}{⟶} N ∖ \{K\} \leftrightarrow (Z : N ∖ \{K\} ⟶ N ∖ \{K\} \land \forall i \in (N ∖ \{K\}) \forall j \in (N ∖ \{K\}) (Z (i) = Z (j) \to i = j))$
25		fveqeq2	$⊢ i = y \to (Z (i) = Z (j) \leftrightarrow Z (y) = Z (j))$
26		equequ1	$⊢ i = y \to (i = j \leftrightarrow y = j)$
27	25 26	imbi12d	$⊢ i = y \to ((Z (i) = Z (j) \to i = j) \leftrightarrow (Z (y) = Z (j) \to y = j))$
28		fveq2	$⊢ j = z \to Z (j) = Z (z)$
29	28	eqeq2d	$⊢ j = z \to (Z (y) = Z (j) \leftrightarrow Z (y) = Z (z))$
30		equequ2	$⊢ j = z \to (y = j \leftrightarrow y = z)$
31	29 30	imbi12d	$⊢ j = z \to ((Z (y) = Z (j) \to y = j) \leftrightarrow (Z (y) = Z (z) \to y = z))$
32	27 31	rspc2va	$⊢ ((y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \land \forall i \in (N ∖ \{K\}) \forall j \in (N ∖ \{K\}) (Z (i) = Z (j) \to i = j)) \to (Z (y) = Z (z) \to y = z)$
33	32	expcom	$⊢ \forall i \in (N ∖ \{K\}) \forall j \in (N ∖ \{K\}) (Z (i) = Z (j) \to i = j) \to ((y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \to (Z (y) = Z (z) \to y = z))$
34	33	a1d	$⊢ \forall i \in (N ∖ \{K\}) \forall j \in (N ∖ \{K\}) (Z (i) = Z (j) \to i = j) \to (K \in N \to ((y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \to (Z (y) = Z (z) \to y = z)))$
35	24 34	simplbiim	$⊢ Z : N ∖ \{K\} \underset{1-1}{⟶} N ∖ \{K\} \to (K \in N \to ((y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \to (Z (y) = Z (z) \to y = z)))$
36	22 23 35	3syl	$⊢ Z \in S \to (K \in N \to ((y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \to (Z (y) = Z (z) \to y = z)))$
37	36	impcom	$⊢ (K \in N \land Z \in S) \to ((y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \to (Z (y) = Z (z) \to y = z))$
38	37	impcom	$⊢ ((y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \land (K \in N \land Z \in S)) \to (Z (y) = Z (z) \to y = z)$
39	20 38	sylbid	$⊢ ((y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \land (K \in N \land Z \in S)) \to (E (y) = E (z) \to y = z)$
40	39	ex	$⊢ (y \in (N ∖ \{K\}) \land z \in (N ∖ \{K\})) \to ((K \in N \land Z \in S) \to (E (y) = E (z) \to y = z))$
41	1 2	symgextf1lem	$⊢ (K \in N \land Z \in S) \to ((z \in (N ∖ \{K\}) \land y \in \{K\}) \to E (z) \neq E (y))$
42		eqneqall	$⊢ E (z) = E (y) \to (E (z) \neq E (y) \to y = z)$
43	42	eqcoms	$⊢ E (y) = E (z) \to (E (z) \neq E (y) \to y = z)$
44	43	com12	$⊢ E (z) \neq E (y) \to (E (y) = E (z) \to y = z)$
45	41 44	syl6com	$⊢ (z \in (N ∖ \{K\}) \land y \in \{K\}) \to ((K \in N \land Z \in S) \to (E (y) = E (z) \to y = z))$
46	45	ancoms	$⊢ (y \in \{K\} \land z \in (N ∖ \{K\})) \to ((K \in N \land Z \in S) \to (E (y) = E (z) \to y = z))$
47	1 2	symgextf1lem	$⊢ (K \in N \land Z \in S) \to ((y \in (N ∖ \{K\}) \land z \in \{K\}) \to E (y) \neq E (z))$
48		eqneqall	$⊢ E (y) = E (z) \to (E (y) \neq E (z) \to y = z)$
49	48	com12	$⊢ E (y) \neq E (z) \to (E (y) = E (z) \to y = z)$
50	47 49	syl6com	$⊢ (y \in (N ∖ \{K\}) \land z \in \{K\}) \to ((K \in N \land Z \in S) \to (E (y) = E (z) \to y = z))$
51		elsni	$⊢ y \in \{K\} \to y = K$
52		elsni	$⊢ z \in \{K\} \to z = K$
53		eqtr3	$⊢ (y = K \land z = K) \to y = z$
54	53	2a1d	$⊢ (y = K \land z = K) \to ((K \in N \land Z \in S) \to (E (y) = E (z) \to y = z))$
55	51 52 54	syl2an	$⊢ (y \in \{K\} \land z \in \{K\}) \to ((K \in N \land Z \in S) \to (E (y) = E (z) \to y = z))$
56	40 46 50 55	ccase	$⊢ ((y \in (N ∖ \{K\}) \lor y \in \{K\}) \land (z \in (N ∖ \{K\}) \lor z \in \{K\})) \to ((K \in N \land Z \in S) \to (E (y) = E (z) \to y = z))$
57	10 11 56	syl2anb	$⊢ (y \in ((N ∖ \{K\}) \cup \{K\}) \land z \in ((N ∖ \{K\}) \cup \{K\})) \to ((K \in N \land Z \in S) \to (E (y) = E (z) \to y = z))$
58	57	com12	$⊢ (K \in N \land Z \in S) \to ((y \in ((N ∖ \{K\}) \cup \{K\}) \land z \in ((N ∖ \{K\}) \cup \{K\})) \to (E (y) = E (z) \to y = z))$
59	9 58	sylbid	$⊢ (K \in N \land Z \in S) \to ((y \in N \land z \in N) \to (E (y) = E (z) \to y = z))$
60	59	ralrimivv	$⊢ (K \in N \land Z \in S) \to \forall y \in N \forall z \in N (E (y) = E (z) \to y = z)$
61		dff13	$⊢ E : N \underset{1-1}{⟶} N \leftrightarrow (E : N ⟶ N \land \forall y \in N \forall z \in N (E (y) = E (z) \to y = z))$
62	3 60 61	sylanbrc	$⊢ (K \in N \land Z \in S) \to E : N \underset{1-1}{⟶} N$

Metamath Proof Explorer

Theorem symgextf1

Proof