pmtr3ncom

Description: Transpositions over sets with at least 3 elements are not commutative, see also the remark in Rotman p. 28. (Contributed by AV, 21-Mar-2019)

		Ref	Expression
	Hypothesis	pmtr3ncom.t	$⊢ T = pmTrsp (D)$
	Assertion	pmtr3ncom	$⊢ (D \in V \land 3 \leq \|D\|) \to \exists f \in ran T \exists g \in ran T g \circ f \neq f \circ g$

Proof

Step	Hyp	Ref	Expression
1		pmtr3ncom.t	$⊢ T = pmTrsp (D)$
2		hashge3el3dif	$⊢ (D \in V \land 3 \leq \|D\|) \to \exists x \in D \exists y \in D \exists z \in D (x \neq y \land x \neq z \land y \neq z)$
3		simprl	$⊢ ((((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \land (D \in V \land 3 \leq \|D\|)) \to D \in V$
4		prssi	$⊢ (x \in D \land y \in D) \to \{x, y\} \subseteq D$
5	4	adantr	$⊢ ((x \in D \land y \in D) \land z \in D) \to \{x, y\} \subseteq D$
6	5	ad2antrr	$⊢ ((((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \land (D \in V \land 3 \leq \|D\|)) \to \{x, y\} \subseteq D$
7		simplll	$⊢ (((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \to x \in D$
8		simplr	$⊢ ((x \in D \land y \in D) \land z \in D) \to y \in D$
9	8	adantr	$⊢ (((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \to y \in D$
10		simpr1	$⊢ (((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \to x \neq y$
11		pr2nelem	$⊢ (x \in D \land y \in D \land x \neq y) \to \{x, y\} \approx 2_{𝑜}$
12	7 9 10 11	syl3anc	$⊢ (((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \to \{x, y\} \approx 2_{𝑜}$
13	12	adantr	$⊢ ((((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \land (D \in V \land 3 \leq \|D\|)) \to \{x, y\} \approx 2_{𝑜}$
14		eqid	$⊢ ran T = ran T$
15	1 14	pmtrrn	$⊢ (D \in V \land \{x, y\} \subseteq D \land \{x, y\} \approx 2_{𝑜}) \to T (\{x, y\}) \in ran T$
16	3 6 13 15	syl3anc	$⊢ ((((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \land (D \in V \land 3 \leq \|D\|)) \to T (\{x, y\}) \in ran T$
17		prssi	$⊢ (y \in D \land z \in D) \to \{y, z\} \subseteq D$
18	17	ad5ant23	$⊢ ((((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \land (D \in V \land 3 \leq \|D\|)) \to \{y, z\} \subseteq D$
19		simplr	$⊢ (((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \to z \in D$
20		simpr3	$⊢ (((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \to y \neq z$
21		pr2nelem	$⊢ (y \in D \land z \in D \land y \neq z) \to \{y, z\} \approx 2_{𝑜}$
22	9 19 20 21	syl3anc	$⊢ (((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \to \{y, z\} \approx 2_{𝑜}$
23	22	adantr	$⊢ ((((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \land (D \in V \land 3 \leq \|D\|)) \to \{y, z\} \approx 2_{𝑜}$
24	1 14	pmtrrn	$⊢ (D \in V \land \{y, z\} \subseteq D \land \{y, z\} \approx 2_{𝑜}) \to T (\{y, z\}) \in ran T$
25	3 18 23 24	syl3anc	$⊢ ((((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \land (D \in V \land 3 \leq \|D\|)) \to T (\{y, z\}) \in ran T$
26		df-3an	$⊢ (x \in D \land y \in D \land z \in D) \leftrightarrow ((x \in D \land y \in D) \land z \in D)$
27	26	biimpri	$⊢ ((x \in D \land y \in D) \land z \in D) \to (x \in D \land y \in D \land z \in D)$
28	27	ad2antrr	$⊢ ((((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \land (D \in V \land 3 \leq \|D\|)) \to (x \in D \land y \in D \land z \in D)$
29		simplr	$⊢ ((((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \land (D \in V \land 3 \leq \|D\|)) \to (x \neq y \land x \neq z \land y \neq z)$
30		eqid	$⊢ T (\{x, y\}) = T (\{x, y\})$
31		eqid	$⊢ T (\{y, z\}) = T (\{y, z\})$
32	1 30 31	pmtr3ncomlem2	$⊢ (D \in V \land (x \in D \land y \in D \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \to T (\{y, z\}) \circ T (\{x, y\}) \neq T (\{x, y\}) \circ T (\{y, z\})$
33	3 28 29 32	syl3anc	$⊢ ((((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \land (D \in V \land 3 \leq \|D\|)) \to T (\{y, z\}) \circ T (\{x, y\}) \neq T (\{x, y\}) \circ T (\{y, z\})$
34		coeq2	$⊢ f = T (\{x, y\}) \to g \circ f = g \circ T (\{x, y\})$
35		coeq1	$⊢ f = T (\{x, y\}) \to f \circ g = T (\{x, y\}) \circ g$
36	34 35	neeq12d	$⊢ f = T (\{x, y\}) \to (g \circ f \neq f \circ g \leftrightarrow g \circ T (\{x, y\}) \neq T (\{x, y\}) \circ g)$
37		coeq1	$⊢ g = T (\{y, z\}) \to g \circ T (\{x, y\}) = T (\{y, z\}) \circ T (\{x, y\})$
38		coeq2	$⊢ g = T (\{y, z\}) \to T (\{x, y\}) \circ g = T (\{x, y\}) \circ T (\{y, z\})$
39	37 38	neeq12d	$⊢ g = T (\{y, z\}) \to (g \circ T (\{x, y\}) \neq T (\{x, y\}) \circ g \leftrightarrow T (\{y, z\}) \circ T (\{x, y\}) \neq T (\{x, y\}) \circ T (\{y, z\}))$
40	36 39	rspc2ev	$⊢ (T (\{x, y\}) \in ran T \land T (\{y, z\}) \in ran T \land T (\{y, z\}) \circ T (\{x, y\}) \neq T (\{x, y\}) \circ T (\{y, z\})) \to \exists f \in ran T \exists g \in ran T g \circ f \neq f \circ g$
41	16 25 33 40	syl3anc	$⊢ ((((x \in D \land y \in D) \land z \in D) \land (x \neq y \land x \neq z \land y \neq z)) \land (D \in V \land 3 \leq \|D\|)) \to \exists f \in ran T \exists g \in ran T g \circ f \neq f \circ g$
42	41	exp31	$⊢ ((x \in D \land y \in D) \land z \in D) \to ((x \neq y \land x \neq z \land y \neq z) \to ((D \in V \land 3 \leq \|D\|) \to \exists f \in ran T \exists g \in ran T g \circ f \neq f \circ g))$
43	42	rexlimdva	$⊢ (x \in D \land y \in D) \to (\exists z \in D (x \neq y \land x \neq z \land y \neq z) \to ((D \in V \land 3 \leq \|D\|) \to \exists f \in ran T \exists g \in ran T g \circ f \neq f \circ g))$
44	43	rexlimivv	$⊢ \exists x \in D \exists y \in D \exists z \in D (x \neq y \land x \neq z \land y \neq z) \to ((D \in V \land 3 \leq \|D\|) \to \exists f \in ran T \exists g \in ran T g \circ f \neq f \circ g)$
45	2 44	mpcom	$⊢ (D \in V \land 3 \leq \|D\|) \to \exists f \in ran T \exists g \in ran T g \circ f \neq f \circ g$

Metamath Proof Explorer

Theorem pmtr3ncom

Proof