Metamath Proof Explorer

Theorem psgnvalii

Description: Any representation of a permutation is length matching the permutation sign. (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 psgnvalii ⊢ D ∈ V ∧ W ∈ Word T → N ⁡ ∑ G W = − 1 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 1 2 3 psgneldm2i ⊢ D ∈ V ∧ W ∈ Word T → ∑ G W ∈ dom ⁡ N
5 1 2 3 psgnval ⊢ ∑ G W ∈ dom ⁡ N → N ⁡ ∑ G W = ι s | ∃ w ∈ Word T ∑ G W = ∑ G w ∧ s = − 1 w
6 4 5 syl ⊢ D ∈ V ∧ W ∈ Word T → N ⁡ ∑ G W = ι s | ∃ w ∈ Word T ∑ G W = ∑ G w ∧ s = − 1 w
7 simpr ⊢ D ∈ V ∧ W ∈ Word T → W ∈ Word T
8 eqidd ⊢ D ∈ V ∧ W ∈ Word T → ∑ G W = ∑ G W
9 eqidd ⊢ D ∈ V ∧ W ∈ Word T → − 1 W = − 1 W
10 oveq2 ⊢ w = W → ∑ G w = ∑ G W
11 10 eqeq2d ⊢ w = W → ∑ G W = ∑ G w ↔ ∑ G W = ∑ G W
12 fveq2 ⊢ w = W → w = W
13 12 oveq2d ⊢ w = W → − 1 w = − 1 W
14 13 eqeq2d ⊢ w = W → − 1 W = − 1 w ↔ − 1 W = − 1 W
15 11 14 anbi12d ⊢ w = W → ∑ G W = ∑ G w ∧ − 1 W = − 1 w ↔ ∑ G W = ∑ G W ∧ − 1 W = − 1 W
16 15 rspcev ⊢ W ∈ Word T ∧ ∑ G W = ∑ G W ∧ − 1 W = − 1 W → ∃ w ∈ Word T ∑ G W = ∑ G w ∧ − 1 W = − 1 w
17 7 8 9 16 syl12anc ⊢ D ∈ V ∧ W ∈ Word T → ∃ w ∈ Word T ∑ G W = ∑ G w ∧ − 1 W = − 1 w
18 ovexd ⊢ D ∈ V ∧ W ∈ Word T → − 1 W ∈ V
19 1 2 3 psgneu ⊢ ∑ G W ∈ dom ⁡ N → ∃! s ∃ w ∈ Word T ∑ G W = ∑ G w ∧ s = − 1 w
20 4 19 syl ⊢ D ∈ V ∧ W ∈ Word T → ∃! s ∃ w ∈ Word T ∑ G W = ∑ G w ∧ s = − 1 w
21 eqeq1 ⊢ s = − 1 W → s = − 1 w ↔ − 1 W = − 1 w
22 21 anbi2d ⊢ s = − 1 W → ∑ G W = ∑ G w ∧ s = − 1 w ↔ ∑ G W = ∑ G w ∧ − 1 W = − 1 w
23 22 rexbidv ⊢ s = − 1 W → ∃ w ∈ Word T ∑ G W = ∑ G w ∧ s = − 1 w ↔ ∃ w ∈ Word T ∑ G W = ∑ G w ∧ − 1 W = − 1 w
24 23 adantl ⊢ D ∈ V ∧ W ∈ Word T ∧ s = − 1 W → ∃ w ∈ Word T ∑ G W = ∑ G w ∧ s = − 1 w ↔ ∃ w ∈ Word T ∑ G W = ∑ G w ∧ − 1 W = − 1 w
25 18 20 24 iota2d ⊢ D ∈ V ∧ W ∈ Word T → ∃ w ∈ Word T ∑ G W = ∑ G w ∧ − 1 W = − 1 w ↔ ι s | ∃ w ∈ Word T ∑ G W = ∑ G w ∧ s = − 1 w = − 1 W
26 17 25 mpbid ⊢ D ∈ V ∧ W ∈ Word T → ι s | ∃ w ∈ Word T ∑ G W = ∑ G w ∧ s = − 1 w = − 1 W
27 6 26 eqtrd ⊢ D ∈ V ∧ W ∈ Word T → N ⁡ ∑ G W = − 1 W