Step | Hyp | Ref
| Expression |
1 | | psgnfval.n |
. 2
⊢ 𝑁 = (pmSgn‘𝐷) |
2 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → (SymGrp‘𝑑) = (SymGrp‘𝐷)) |
3 | | psgnfval.g |
. . . . . . . . . 10
⊢ 𝐺 = (SymGrp‘𝐷) |
4 | 2, 3 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → (SymGrp‘𝑑) = 𝐺) |
5 | 4 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (Base‘(SymGrp‘𝑑)) = (Base‘𝐺)) |
6 | | psgnfval.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
7 | 5, 6 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → (Base‘(SymGrp‘𝑑)) = 𝐵) |
8 | | rabeq 3166 |
. . . . . . 7
⊢
((Base‘(SymGrp‘𝑑)) = 𝐵 → {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} =
{𝑝 ∈ 𝐵 ∣ dom (𝑝 ∖ I ) ∈ Fin}) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (𝑑 = 𝐷 → {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} =
{𝑝 ∈ 𝐵 ∣ dom (𝑝 ∖ I ) ∈ Fin}) |
10 | | psgnfval.f |
. . . . . 6
⊢ 𝐹 = {𝑝 ∈ 𝐵 ∣ dom (𝑝 ∖ I ) ∈ Fin} |
11 | 9, 10 | syl6eqr 2662 |
. . . . 5
⊢ (𝑑 = 𝐷 → {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} = 𝐹) |
12 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → (pmTrsp‘𝑑) = (pmTrsp‘𝐷)) |
13 | 12 | rneqd 5274 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → ran (pmTrsp‘𝑑) = ran (pmTrsp‘𝐷)) |
14 | | psgnfval.t |
. . . . . . . . 9
⊢ 𝑇 = ran (pmTrsp‘𝐷) |
15 | 13, 14 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → ran (pmTrsp‘𝑑) = 𝑇) |
16 | | wrdeq 13182 |
. . . . . . . 8
⊢ (ran
(pmTrsp‘𝑑) = 𝑇 → Word ran
(pmTrsp‘𝑑) = Word
𝑇) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → Word ran (pmTrsp‘𝑑) = Word 𝑇) |
18 | 4 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → ((SymGrp‘𝑑) Σg 𝑤) = (𝐺 Σg 𝑤)) |
19 | 18 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ↔ 𝑥 = (𝐺 Σg 𝑤))) |
20 | 19 | anbi1d 737 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → ((𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))) ↔ (𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))) |
21 | 17, 20 | rexeqbidv 3130 |
. . . . . 6
⊢ (𝑑 = 𝐷 → (∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))) ↔ ∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))) |
22 | 21 | iotabidv 5789 |
. . . . 5
⊢ (𝑑 = 𝐷 → (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))) = (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))) |
23 | 11, 22 | mpteq12dv 4663 |
. . . 4
⊢ (𝑑 = 𝐷 → (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦
(℩𝑠∃𝑤 ∈ Word ran
(pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg
𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))) = (𝑥 ∈ 𝐹 ↦ (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))))) |
24 | | df-psgn 17734 |
. . . 4
⊢ pmSgn =
(𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦
(℩𝑠∃𝑤 ∈ Word ran
(pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg
𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))))) |
25 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐺)
∈ V |
26 | 6, 25 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
27 | 10, 26 | rabex2 4742 |
. . . . 5
⊢ 𝐹 ∈ V |
28 | 27 | mptex 6390 |
. . . 4
⊢ (𝑥 ∈ 𝐹 ↦ (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))) ∈ V |
29 | 23, 24, 28 | fvmpt 6191 |
. . 3
⊢ (𝐷 ∈ V →
(pmSgn‘𝐷) = (𝑥 ∈ 𝐹 ↦ (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))))) |
30 | | fvprc 6097 |
. . . 4
⊢ (¬
𝐷 ∈ V →
(pmSgn‘𝐷) =
∅) |
31 | | fvprc 6097 |
. . . . . . . . . . . . 13
⊢ (¬
𝐷 ∈ V →
(SymGrp‘𝐷) =
∅) |
32 | 3, 31 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ (¬
𝐷 ∈ V → 𝐺 = ∅) |
33 | 32 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (¬
𝐷 ∈ V →
(Base‘𝐺) =
(Base‘∅)) |
34 | | base0 15740 |
. . . . . . . . . . 11
⊢ ∅ =
(Base‘∅) |
35 | 33, 34 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (¬
𝐷 ∈ V →
(Base‘𝐺) =
∅) |
36 | 6, 35 | syl5eq 2656 |
. . . . . . . . 9
⊢ (¬
𝐷 ∈ V → 𝐵 = ∅) |
37 | | rabeq 3166 |
. . . . . . . . 9
⊢ (𝐵 = ∅ → {𝑝 ∈ 𝐵 ∣ dom (𝑝 ∖ I ) ∈ Fin} = {𝑝 ∈ ∅ ∣ dom
(𝑝 ∖ I ) ∈
Fin}) |
38 | 36, 37 | syl 17 |
. . . . . . . 8
⊢ (¬
𝐷 ∈ V → {𝑝 ∈ 𝐵 ∣ dom (𝑝 ∖ I ) ∈ Fin} = {𝑝 ∈ ∅ ∣ dom
(𝑝 ∖ I ) ∈
Fin}) |
39 | | rab0 3909 |
. . . . . . . 8
⊢ {𝑝 ∈ ∅ ∣ dom
(𝑝 ∖ I ) ∈ Fin}
= ∅ |
40 | 38, 39 | syl6eq 2660 |
. . . . . . 7
⊢ (¬
𝐷 ∈ V → {𝑝 ∈ 𝐵 ∣ dom (𝑝 ∖ I ) ∈ Fin} =
∅) |
41 | 10, 40 | syl5eq 2656 |
. . . . . 6
⊢ (¬
𝐷 ∈ V → 𝐹 = ∅) |
42 | 41 | mpteq1d 4666 |
. . . . 5
⊢ (¬
𝐷 ∈ V → (𝑥 ∈ 𝐹 ↦ (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))) = (𝑥 ∈ ∅ ↦ (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))))) |
43 | | mpt0 5934 |
. . . . 5
⊢ (𝑥 ∈ ∅ ↦
(℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))) = ∅ |
44 | 42, 43 | syl6eq 2660 |
. . . 4
⊢ (¬
𝐷 ∈ V → (𝑥 ∈ 𝐹 ↦ (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))) = ∅) |
45 | 30, 44 | eqtr4d 2647 |
. . 3
⊢ (¬
𝐷 ∈ V →
(pmSgn‘𝐷) = (𝑥 ∈ 𝐹 ↦ (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤)))))) |
46 | 29, 45 | pm2.61i 175 |
. 2
⊢
(pmSgn‘𝐷) =
(𝑥 ∈ 𝐹 ↦ (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))) |
47 | 1, 46 | eqtri 2632 |
1
⊢ 𝑁 = (𝑥 ∈ 𝐹 ↦ (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(#‘𝑤))))) |