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	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	psgnval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
	psgnval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion	psgnvalii	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑁 ‘ ( 𝐺 Σg 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgnval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2		psgnval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3		psgnval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4	1 2 3	psgneldm2i	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐺 Σg 𝑊 ) ∈ dom 𝑁 )
5	1 2 3	psgnval	⊢ ( ( 𝐺 Σg 𝑊 ) ∈ dom 𝑁 → ( 𝑁 ‘ ( 𝐺 Σg 𝑊 ) ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
6	4 5	syl	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑁 ‘ ( 𝐺 Σg 𝑊 ) ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
7		simpr	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → 𝑊 ∈ Word 𝑇 )
8		eqidd	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑊 ) )
9		eqidd	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) )
10		oveq2	⊢ ( 𝑤 = 𝑊 → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg 𝑊 ) )
11	10	eqeq2d	⊢ ( 𝑤 = 𝑊 → ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ↔ ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑊 ) ) )
12		fveq2	⊢ ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
13	12	oveq2d	⊢ ( 𝑤 = 𝑊 → ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) )
14	13	eqeq2d	⊢ ( 𝑤 = 𝑊 → ( ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ) )
15	11 14	anbi12d	⊢ ( 𝑤 = 𝑊 → ( ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑊 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ) ) )
16	15	rspcev	⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑊 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
17	7 8 9 16	syl12anc	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
18		ovexd	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ∈ V )
19	1 2 3	psgneu	⊢ ( ( 𝐺 Σg 𝑊 ) ∈ dom 𝑁 → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
20	4 19	syl	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
21		eqeq1	⊢ ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) )
22	21	anbi2d	⊢ ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
23	22	rexbidv	⊢ ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) → ( ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
24	23	adantl	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ) → ( ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
25	18 20 24	iota2d	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) ) )
26	17 25	mpbid	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) )
27	6 26	eqtrd	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑁 ‘ ( 𝐺 Σg 𝑊 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑊 ) ) )