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 10 grpmndd ⊢ D ∈ V → G ∈ Mnd
12 2 1 4 symgtrf ⊢ T ⊆ Base G
13 4 8 gsumwspan ⊢ G ∈ Mnd ∧ T ⊆ Base G → mrCls ⁡ SubMnd ⁡ G ⁡ T = ran ⁡ w ∈ Word T ⟼ ∑ G w
14 11 12 13 sylancl ⊢ D ∈ V → mrCls ⁡ SubMnd ⁡ G ⁡ T = ran ⁡ w ∈ Word T ⟼ ∑ G w
15 9 14 eqtr3d ⊢ D ∈ V → p ∈ Base G | dom ⁡ p ∖ I ∈ Fin = ran ⁡ w ∈ Word T ⟼ ∑ G w
16 7 15 eqtrid ⊢ D ∈ V → dom ⁡ N = ran ⁡ w ∈ Word T ⟼ ∑ G w
17 16 eleq2d ⊢ D ∈ V → P ∈ dom ⁡ N ↔ P ∈ ran ⁡ w ∈ Word T ⟼ ∑ G w
18 eqid ⊢ w ∈ Word T ⟼ ∑ G w = w ∈ Word T ⟼ ∑ G w
19 ovex ⊢ ∑ G w ∈ V
20 18 19 elrnmpti ⊢ P ∈ ran ⁡ w ∈ Word T ⟼ ∑ G w ↔ ∃ w ∈ Word T P = ∑ G w
21 17 20 bitrdi ⊢ D ∈ V → P ∈ dom ⁡ N ↔ ∃ w ∈ Word T P = ∑ G w