Theorem pgrple2abl

Description: Every symmetric group on a set with at most 2 elements is abelian. (Contributed by AV, 16-Mar-2019)

	Ref	Expression
Hypothesis	pgrple2abl.g	|- G = ( SymGrp ` A )
Assertion	pgrple2abl	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> G e. Abel )

Proof

Step	Hyp	Ref	Expression
1		pgrple2abl.g	|- G = ( SymGrp ` A )
2	1	symggrp	|- ( A e. V -> G e. Grp )
3	2	adantr	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> G e. Grp )
4		2nn0	|- 2 e. NN0
5		hashbnd	|- ( ( A e. V /\ 2 e. NN0 /\ ( # ` A ) <_ 2 ) -> A e. Fin )
6	4 5	mp3an2	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> A e. Fin )
7		eqid	|- ( Base ` G ) = ( Base ` G )
8	1 7	symghash	|- ( A e. Fin -> ( # ` ( Base ` G ) ) = ( ! ` ( # ` A ) ) )
9	6 8	syl	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> ( # ` ( Base ` G ) ) = ( ! ` ( # ` A ) ) )
10		hashcl	|- ( A e. Fin -> ( # ` A ) e. NN0 )
11	6 10	syl	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> ( # ` A ) e. NN0 )
12		faccl	|- ( ( # ` A ) e. NN0 -> ( ! ` ( # ` A ) ) e. NN )
13	11 12	syl	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> ( ! ` ( # ` A ) ) e. NN )
14	13	nnred	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> ( ! ` ( # ` A ) ) e. RR )
15	11 11	nn0expcld	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> ( ( # ` A ) ^ ( # ` A ) ) e. NN0 )
16	15	nn0red	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> ( ( # ` A ) ^ ( # ` A ) ) e. RR )
17		6re	|- 6 e. RR
18	17	a1i	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> 6 e. RR )
19		facubnd	|- ( ( # ` A ) e. NN0 -> ( ! ` ( # ` A ) ) <_ ( ( # ` A ) ^ ( # ` A ) ) )
20	11 19	syl	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> ( ! ` ( # ` A ) ) <_ ( ( # ` A ) ^ ( # ` A ) ) )
21		exple2lt6	|- ( ( ( # ` A ) e. NN0 /\ ( # ` A ) <_ 2 ) -> ( ( # ` A ) ^ ( # ` A ) ) < 6 )
22	11 21	sylancom	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> ( ( # ` A ) ^ ( # ` A ) ) < 6 )
23	14 16 18 20 22	lelttrd	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> ( ! ` ( # ` A ) ) < 6 )
24	9 23	eqbrtrd	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> ( # ` ( Base ` G ) ) < 6 )
25	7	lt6abl	|- ( ( G e. Grp /\ ( # ` ( Base ` G ) ) < 6 ) -> G e. Abel )
26	3 24 25	syl2anc	|- ( ( A e. V /\ ( # ` A ) <_ 2 ) -> G e. Abel )