psgnfitr

Description: A permutation of a finite set is generated by transpositions. (Contributed by AV, 13-Jan-2019)

	Ref	Expression
Hypotheses	psgnfitr.g	$⊢ G = SymGrp (N)$
	psgnfitr.p	$⊢ B = {Base}_{G}$
	psgnfitr.t	$⊢ T = ran pmTrsp (N)$
Assertion	psgnfitr	$⊢ N \in Fin \to (Q \in B \leftrightarrow \exists w \in Word T Q = \sum_{G} w)$

Step	Hyp	Ref	Expression
1		psgnfitr.g	$⊢ G = SymGrp (N)$
2		psgnfitr.p	$⊢ B = {Base}_{G}$
3		psgnfitr.t	$⊢ T = ran pmTrsp (N)$
4		eqid	$⊢ mrCls (SubMnd (G)) = mrCls (SubMnd (G))$
5	3 1 2 4	symggen2	$⊢ N \in Fin \to mrCls (SubMnd (G)) (T) = B$
6	1	symggrp	$⊢ N \in Fin \to G \in Grp$
7	6	grpmndd	$⊢ N \in Fin \to G \in Mnd$
8		eqid	$⊢ {Base}_{G} = {Base}_{G}$
9	3 1 8	symgtrf	$⊢ T \subseteq {Base}_{G}$
10	8 4	gsumwspan	$⊢ (G \in Mnd \land T \subseteq {Base}_{G}) \to mrCls (SubMnd (G)) (T) = ran (w \in Word T ⟼ \sum_{G} w)$
11	7 9 10	sylancl	$⊢ N \in Fin \to mrCls (SubMnd (G)) (T) = ran (w \in Word T ⟼ \sum_{G} w)$
12	5 11	eqtr3d	$⊢ N \in Fin \to B = ran (w \in Word T ⟼ \sum_{G} w)$
13	12	eleq2d	$⊢ N \in Fin \to (Q \in B \leftrightarrow Q \in ran (w \in Word T ⟼ \sum_{G} w))$
14		eqid	$⊢ (w \in Word T ⟼ \sum_{G} w) = (w \in Word T ⟼ \sum_{G} w)$
15		ovex	$⊢ \sum_{G} w \in V$
16	14 15	elrnmpti	$⊢ Q \in ran (w \in Word T ⟼ \sum_{G} w) \leftrightarrow \exists w \in Word T Q = \sum_{G} w$
17	13 16	bitrdi	$⊢ N \in Fin \to (Q \in B \leftrightarrow \exists w \in Word T Q = \sum_{G} w)$

Metamath Proof Explorer