pgrpgt2nabl

Description: Every symmetric group on a set with more than 2 elements is not abelian, see also the remark in Rotman p. 28. (Contributed by AV, 21-Mar-2019)

		Ref	Expression
	Hypothesis	pgrple2abl.g	$⊢ G = SymGrp (A)$
	Assertion	pgrpgt2nabl	$⊢ (A \in V \land 2 < \|A\|) \to G \notin Abel$

Proof

Step	Hyp	Ref	Expression
1		pgrple2abl.g	$⊢ G = SymGrp (A)$
2		eqid	$⊢ ran pmTrsp (A) = ran pmTrsp (A)$
3		eqid	$⊢ {Base}_{G} = {Base}_{G}$
4	2 1 3	symgtrf	$⊢ ran pmTrsp (A) \subseteq {Base}_{G}$
5		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
6		2nn0	$⊢ 2 \in ℕ_{0}$
7		nn0ltp1le	$⊢ (2 \in ℕ_{0} \land \|A\| \in ℕ_{0}) \to (2 < \|A\| \leftrightarrow 2 + 1 \leq \|A\|)$
8	6 7	mpan	$⊢ \|A\| \in ℕ_{0} \to (2 < \|A\| \leftrightarrow 2 + 1 \leq \|A\|)$
9		2p1e3	$⊢ 2 + 1 = 3$
10	9	a1i	$⊢ \|A\| \in ℕ_{0} \to 2 + 1 = 3$
11	10	breq1d	$⊢ \|A\| \in ℕ_{0} \to (2 + 1 \leq \|A\| \leftrightarrow 3 \leq \|A\|)$
12	8 11	bitrd	$⊢ \|A\| \in ℕ_{0} \to (2 < \|A\| \leftrightarrow 3 \leq \|A\|)$
13	12	biimpd	$⊢ \|A\| \in ℕ_{0} \to (2 < \|A\| \to 3 \leq \|A\|)$
14	13	adantld	$⊢ \|A\| \in ℕ_{0} \to ((A \in V \land 2 < \|A\|) \to 3 \leq \|A\|)$
15	5 14	syl	$⊢ A \in Fin \to ((A \in V \land 2 < \|A\|) \to 3 \leq \|A\|)$
16		3re	$⊢ 3 \in ℝ$
17	16	rexri	$⊢ 3 \in ℝ^{*}$
18		pnfge	$⊢ 3 \in ℝ^{*} \to 3 \leq +∞$
19	17 18	ax-mp	$⊢ 3 \leq +∞$
20		hashinf	$⊢ (A \in V \land \neg A \in Fin) \to \|A\| = +∞$
21	19 20	breqtrrid	$⊢ (A \in V \land \neg A \in Fin) \to 3 \leq \|A\|$
22	21	ex	$⊢ A \in V \to (\neg A \in Fin \to 3 \leq \|A\|)$
23	22	adantr	$⊢ (A \in V \land 2 < \|A\|) \to (\neg A \in Fin \to 3 \leq \|A\|)$
24	23	com12	$⊢ \neg A \in Fin \to ((A \in V \land 2 < \|A\|) \to 3 \leq \|A\|)$
25	15 24	pm2.61i	$⊢ (A \in V \land 2 < \|A\|) \to 3 \leq \|A\|$
26		eqid	$⊢ pmTrsp (A) = pmTrsp (A)$
27	26	pmtr3ncom	$⊢ (A \in V \land 3 \leq \|A\|) \to \exists y \in ran pmTrsp (A) \exists x \in ran pmTrsp (A) x \circ y \neq y \circ x$
28		rexcom	$⊢ \exists x \in ran pmTrsp (A) \exists y \in ran pmTrsp (A) x \circ y \neq y \circ x \leftrightarrow \exists y \in ran pmTrsp (A) \exists x \in ran pmTrsp (A) x \circ y \neq y \circ x$
29	27 28	sylibr	$⊢ (A \in V \land 3 \leq \|A\|) \to \exists x \in ran pmTrsp (A) \exists y \in ran pmTrsp (A) x \circ y \neq y \circ x$
30	25 29	syldan	$⊢ (A \in V \land 2 < \|A\|) \to \exists x \in ran pmTrsp (A) \exists y \in ran pmTrsp (A) x \circ y \neq y \circ x$
31		ssrexv	$⊢ ran pmTrsp (A) \subseteq {Base}_{G} \to (\exists y \in ran pmTrsp (A) x \circ y \neq y \circ x \to \exists y \in {Base}_{G} x \circ y \neq y \circ x)$
32	31	reximdv	$⊢ ran pmTrsp (A) \subseteq {Base}_{G} \to (\exists x \in ran pmTrsp (A) \exists y \in ran pmTrsp (A) x \circ y \neq y \circ x \to \exists x \in ran pmTrsp (A) \exists y \in {Base}_{G} x \circ y \neq y \circ x)$
33	4 30 32	mpsyl	$⊢ (A \in V \land 2 < \|A\|) \to \exists x \in ran pmTrsp (A) \exists y \in {Base}_{G} x \circ y \neq y \circ x$
34		ssrexv	$⊢ ran pmTrsp (A) \subseteq {Base}_{G} \to (\exists x \in ran pmTrsp (A) \exists y \in {Base}_{G} x \circ y \neq y \circ x \to \exists x \in {Base}_{G} \exists y \in {Base}_{G} x \circ y \neq y \circ x)$
35	4 33 34	mpsyl	$⊢ (A \in V \land 2 < \|A\|) \to \exists x \in {Base}_{G} \exists y \in {Base}_{G} x \circ y \neq y \circ x$
36		eqid	$⊢ +_{G} = +_{G}$
37	1 3 36	symgov	$⊢ (x \in {Base}_{G} \land y \in {Base}_{G}) \to x +_{G} y = x \circ y$
38	37	adantl	$⊢ ((A \in V \land 2 < \|A\|) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to x +_{G} y = x \circ y$
39		pm3.22	$⊢ (x \in {Base}_{G} \land y \in {Base}_{G}) \to (y \in {Base}_{G} \land x \in {Base}_{G})$
40	39	adantl	$⊢ ((A \in V \land 2 < \|A\|) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to (y \in {Base}_{G} \land x \in {Base}_{G})$
41	1 3 36	symgov	$⊢ (y \in {Base}_{G} \land x \in {Base}_{G}) \to y +_{G} x = y \circ x$
42	40 41	syl	$⊢ ((A \in V \land 2 < \|A\|) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to y +_{G} x = y \circ x$
43	38 42	neeq12d	$⊢ ((A \in V \land 2 < \|A\|) \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to (x +_{G} y \neq y +_{G} x \leftrightarrow x \circ y \neq y \circ x)$
44	43	2rexbidva	$⊢ (A \in V \land 2 < \|A\|) \to (\exists x \in {Base}_{G} \exists y \in {Base}_{G} x +_{G} y \neq y +_{G} x \leftrightarrow \exists x \in {Base}_{G} \exists y \in {Base}_{G} x \circ y \neq y \circ x)$
45	35 44	mpbird	$⊢ (A \in V \land 2 < \|A\|) \to \exists x \in {Base}_{G} \exists y \in {Base}_{G} x +_{G} y \neq y +_{G} x$
46		rexnal	$⊢ \exists x \in {Base}_{G} \neg \forall y \in {Base}_{G} x +_{G} y = y +_{G} x \leftrightarrow \neg \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y = y +_{G} x$
47		rexnal	$⊢ \exists y \in {Base}_{G} \neg x +_{G} y = y +_{G} x \leftrightarrow \neg \forall y \in {Base}_{G} x +_{G} y = y +_{G} x$
48		df-ne	$⊢ x +_{G} y \neq y +_{G} x \leftrightarrow \neg x +_{G} y = y +_{G} x$
49	48	bicomi	$⊢ \neg x +_{G} y = y +_{G} x \leftrightarrow x +_{G} y \neq y +_{G} x$
50	49	rexbii	$⊢ \exists y \in {Base}_{G} \neg x +_{G} y = y +_{G} x \leftrightarrow \exists y \in {Base}_{G} x +_{G} y \neq y +_{G} x$
51	47 50	bitr3i	$⊢ \neg \forall y \in {Base}_{G} x +_{G} y = y +_{G} x \leftrightarrow \exists y \in {Base}_{G} x +_{G} y \neq y +_{G} x$
52	51	rexbii	$⊢ \exists x \in {Base}_{G} \neg \forall y \in {Base}_{G} x +_{G} y = y +_{G} x \leftrightarrow \exists x \in {Base}_{G} \exists y \in {Base}_{G} x +_{G} y \neq y +_{G} x$
53	46 52	bitr3i	$⊢ \neg \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y = y +_{G} x \leftrightarrow \exists x \in {Base}_{G} \exists y \in {Base}_{G} x +_{G} y \neq y +_{G} x$
54	45 53	sylibr	$⊢ (A \in V \land 2 < \|A\|) \to \neg \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y = y +_{G} x$
55	54	intnand	$⊢ (A \in V \land 2 < \|A\|) \to \neg (G \in Mnd \land \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y = y +_{G} x)$
56	55	intnand	$⊢ (A \in V \land 2 < \|A\|) \to \neg (G \in Grp \land (G \in Mnd \land \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y = y +_{G} x))$
57		df-nel	$⊢ G \notin Abel \leftrightarrow \neg G \in Abel$
58		isabl	$⊢ G \in Abel \leftrightarrow (G \in Grp \land G \in CMnd)$
59	3 36	iscmn	$⊢ G \in CMnd \leftrightarrow (G \in Mnd \land \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y = y +_{G} x)$
60	59	anbi2i	$⊢ (G \in Grp \land G \in CMnd) \leftrightarrow (G \in Grp \land (G \in Mnd \land \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y = y +_{G} x))$
61	58 60	bitri	$⊢ G \in Abel \leftrightarrow (G \in Grp \land (G \in Mnd \land \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y = y +_{G} x))$
62	57 61	xchbinx	$⊢ G \notin Abel \leftrightarrow \neg (G \in Grp \land (G \in Mnd \land \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y = y +_{G} x))$
63	56 62	sylibr	$⊢ (A \in V \land 2 < \|A\|) \to G \notin Abel$

Metamath Proof Explorer

Theorem pgrpgt2nabl

Proof