Metamath Proof Explorer


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 14 15 syl ( ( 𝑋 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∨ 𝑋 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → ( 𝑋 ∖ I ) ∈ Fin )
17 dmfi ( ( 𝑋 ∖ I ) ∈ Fin → dom ( 𝑋 ∖ I ) ∈ Fin )
18 7 16 17 3syl ( 𝑋 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } → dom ( 𝑋 ∖ I ) ∈ Fin )
19 1ex 1 ∈ V
20 2nn 2 ∈ ℕ
21 2 3 1 symg2bas ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → 𝐵 = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
22 19 20 21 mp2an 𝐵 = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
23 18 22 eleq2s ( 𝑋𝐵 → dom ( 𝑋 ∖ I ) ∈ Fin )
24 2 5 3 psgneldm ( 𝑋 ∈ dom 𝑁 ↔ ( 𝑋𝐵 ∧ dom ( 𝑋 ∖ I ) ∈ Fin ) )
25 6 23 24 sylanbrc ( 𝑋𝐵𝑋 ∈ dom 𝑁 )
26 2 4 5 psgnval ( 𝑋 ∈ dom 𝑁 → ( 𝑁𝑋 ) = ( ℩ 𝑠𝑤 ∈ Word 𝑇 ( 𝑋 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
27 25 26 syl ( 𝑋𝐵 → ( 𝑁𝑋 ) = ( ℩ 𝑠𝑤 ∈ Word 𝑇 ( 𝑋 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
28 6 27 syl ( 𝑋𝐵 → ( 𝑁𝑋 ) = ( ℩ 𝑠𝑤 ∈ Word 𝑇 ( 𝑋 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )