Theorem psgnprfval

Description: The permutation sign function for a pair. (Contributed by AV, 10-Dec-2018)

	Ref	Expression
Hypotheses	psgnprfval.0	⊢ 𝐷 = { 1 , 2 }
	psgnprfval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	psgnprfval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	psgnprfval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
	psgnprfval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion	psgnprfval	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑋 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		psgnprfval.0	⊢ 𝐷 = { 1 , 2 }
2		psgnprfval.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
3		psgnprfval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
4		psgnprfval.t	⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
5		psgnprfval.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
6		id	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝐵 )
7		elpri	⊢ ( 𝑋 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } → ( 𝑋 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∨ 𝑋 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) )
8		prfi	⊢ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ Fin
9		eleq1	⊢ ( 𝑋 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( 𝑋 ∈ Fin ↔ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ Fin ) )
10	8 9	mpbiri	⊢ ( 𝑋 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → 𝑋 ∈ Fin )
11		prfi	⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ Fin
12		eleq1	⊢ ( 𝑋 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑋 ∈ Fin ↔ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ Fin ) )
13	11 12	mpbiri	⊢ ( 𝑋 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → 𝑋 ∈ Fin )
14	10 13	jaoi	⊢ ( ( 𝑋 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∨ 𝑋 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → 𝑋 ∈ Fin )
15		diffi	⊢ ( 𝑋 ∈ Fin → ( 𝑋 ∖ I ) ∈ Fin )
16		dmfi	⊢ ( ( 𝑋 ∖ I ) ∈ Fin → dom ( 𝑋 ∖ I ) ∈ Fin )
17	7 14 15 16	4syl	⊢ ( 𝑋 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } → dom ( 𝑋 ∖ I ) ∈ Fin )
18		1ex	⊢ 1 ∈ V
19		2nn	⊢ 2 ∈ ℕ
20	2 3 1	symg2bas	⊢ ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → 𝐵 = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
21	18 19 20	mp2an	⊢ 𝐵 = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
22	17 21	eleq2s	⊢ ( 𝑋 ∈ 𝐵 → dom ( 𝑋 ∖ I ) ∈ Fin )
23	2 5 3	psgneldm	⊢ ( 𝑋 ∈ dom 𝑁 ↔ ( 𝑋 ∈ 𝐵 ∧ dom ( 𝑋 ∖ I ) ∈ Fin ) )
24	6 22 23	sylanbrc	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ dom 𝑁 )
25	2 4 5	psgnval	⊢ ( 𝑋 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑋 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
26	24 25	syl	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑋 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
27	6 26	syl	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ‘ 𝑋 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑋 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )