Metamath Proof Explorer

Theorem psgneldm2

Description: The finitary permutations are the span of the transpositions. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgnval.g ⊢ G = SymGrp ⁡ D
psgnval.t ⊢ T = ran ⁡ pmTrsp ⁡ D
psgnval.n ⊢ N = pmSgn ⁡ D
Assertion psgneldm2 ⊢ D ∈ V → P ∈ dom ⁡ N ↔ ∃ w ∈ Word T P = ∑ G w

Proof

Step Hyp Ref Expression
1 psgnval.g ⊢ G = SymGrp ⁡ D
2 psgnval.t ⊢ T = ran ⁡ pmTrsp ⁡ D
3 psgnval.n ⊢ N = pmSgn ⁡ D
4 eqid ⊢ Base G = Base G
5 eqid ⊢ p ∈ Base G | dom ⁡ p ∖ I ∈ Fin = p ∈ Base G | dom ⁡ p ∖ I ∈ Fin
6 1 4 5 3 psgnfn ⊢ N Fn p ∈ Base G | dom ⁡ p ∖ I ∈ Fin
7 6 fndmi ⊢ dom ⁡ N = p ∈ Base G | dom ⁡ p ∖ I ∈ Fin
8 eqid ⊢ mrCls ⁡ SubMnd ⁡ G = mrCls ⁡ SubMnd ⁡ G
9 2 1 4 8 symggen ⊢ D ∈ V → mrCls ⁡ SubMnd ⁡ G ⁡ T = p ∈ Base G | dom ⁡ p ∖ I ∈ Fin
10 1 symggrp ⊢ D ∈ V → G ∈ Grp
11 grpmnd ⊢ G ∈ Grp → G ∈ Mnd
12 10 11 syl ⊢ D ∈ V → G ∈ Mnd
13 2 1 4 symgtrf ⊢ T ⊆ Base G
14 4 8 gsumwspan ⊢ G ∈ Mnd ∧ T ⊆ Base G → mrCls ⁡ SubMnd ⁡ G ⁡ T = ran ⁡ w ∈ Word T ⟼ ∑ G w
15 12 13 14 sylancl ⊢ D ∈ V → mrCls ⁡ SubMnd ⁡ G ⁡ T = ran ⁡ w ∈ Word T ⟼ ∑ G w
16 9 15 eqtr3d ⊢ D ∈ V → p ∈ Base G | dom ⁡ p ∖ I ∈ Fin = ran ⁡ w ∈ Word T ⟼ ∑ G w
17 7 16 syl5eq ⊢ D ∈ V → dom ⁡ N = ran ⁡ w ∈ Word T ⟼ ∑ G w
18 17 eleq2d ⊢ D ∈ V → P ∈ dom ⁡ N ↔ P ∈ ran ⁡ w ∈ Word T ⟼ ∑ G w
19 eqid ⊢ w ∈ Word T ⟼ ∑ G w = w ∈ Word T ⟼ ∑ G w
20 ovex ⊢ ∑ G w ∈ V
21 19 20 elrnmpti ⊢ P ∈ ran ⁡ w ∈ Word T ⟼ ∑ G w ↔ ∃ w ∈ Word T P = ∑ G w
22 18 21 bitrdi ⊢ D ∈ V → P ∈ dom ⁡ N ↔ ∃ w ∈ Word T P = ∑ G w