Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π€ = π β (β―βπ€) = (β―βπ)) |
2 | 1 | eqeq1d 2735 |
. . . . . . . . . . 11
β’ (π€ = π β ((β―βπ€) = (β―βπ) β (β―βπ) = (β―βπ))) |
3 | 1 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ (π€ = π β (0..^(β―βπ€)) = (0..^(β―βπ))) |
4 | | fveq1 6845 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π β (π€βπ) = (πβπ)) |
5 | 4 | fveq1d 6848 |
. . . . . . . . . . . . . . 15
β’ (π€ = π β ((π€βπ)βπ) = ((πβπ)βπ)) |
6 | 5 | eqeq1d 2735 |
. . . . . . . . . . . . . 14
β’ (π€ = π β (((π€βπ)βπ) = ((πβπ)βπ) β ((πβπ)βπ) = ((πβπ)βπ))) |
7 | 6 | ralbidv 3171 |
. . . . . . . . . . . . 13
β’ (π€ = π β (βπ β (π β {πΎ})((π€βπ)βπ) = ((πβπ)βπ) β βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))) |
8 | 7 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π€ = π β ((((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((π€βπ)βπ) = ((πβπ)βπ)) β (((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) |
9 | 3, 8 | raleqbidv 3318 |
. . . . . . . . . . 11
β’ (π€ = π β (βπ β (0..^(β―βπ€))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((π€βπ)βπ) = ((πβπ)βπ)) β βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) |
10 | 2, 9 | anbi12d 632 |
. . . . . . . . . 10
β’ (π€ = π β (((β―βπ€) = (β―βπ) β§ βπ β (0..^(β―βπ€))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((π€βπ)βπ) = ((πβπ)βπ))) β ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))))) |
11 | 10 | rexbidv 3172 |
. . . . . . . . 9
β’ (π€ = π β (βπ β Word π
((β―βπ€) = (β―βπ) β§ βπ β (0..^(β―βπ€))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((π€βπ)βπ) = ((πβπ)βπ))) β βπ β Word π
((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))))) |
12 | 11 | rspccv 3580 |
. . . . . . . 8
β’
(βπ€ β
Word πβπ β Word π
((β―βπ€) = (β―βπ) β§ βπ β (0..^(β―βπ€))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((π€βπ)βπ) = ((πβπ)βπ))) β (π β Word π β βπ β Word π
((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))))) |
13 | | psgnfix.t |
. . . . . . . . 9
β’ π = ran (pmTrspβ(π β {πΎ})) |
14 | | psgnfix.r |
. . . . . . . . 9
β’ π
= ran (pmTrspβπ) |
15 | 13, 14 | pmtrdifwrdel2 19276 |
. . . . . . . 8
β’ (πΎ β π β βπ€ β Word πβπ β Word π
((β―βπ€) = (β―βπ) β§ βπ β (0..^(β―βπ€))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((π€βπ)βπ) = ((πβπ)βπ)))) |
16 | 12, 15 | syl11 33 |
. . . . . . 7
β’ (π β Word π β (πΎ β π β βπ β Word π
((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))))) |
17 | 16 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
) β (πΎ β π β βπ β Word π
((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))))) |
18 | 17 | com12 32 |
. . . . 5
β’ (πΎ β π β ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
) β βπ β Word π
((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))))) |
19 | 18 | ad2antlr 726 |
. . . 4
β’ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
) β βπ β Word π
((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))))) |
20 | 19 | imp 408 |
. . 3
β’ ((((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
)) β βπ β Word π
((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) |
21 | | oveq2 7369 |
. . . . . . . . 9
β’
((β―βπ) =
(β―βπ) β
(-1β(β―βπ))
= (-1β(β―βπ))) |
22 | 21 | adantr 482 |
. . . . . . . 8
β’
(((β―βπ)
= (β―βπ) β§
βπ β
(0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))) β (-1β(β―βπ)) =
(-1β(β―βπ))) |
23 | 22 | ad3antlr 730 |
. . . . . . 7
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β
(-1β(β―βπ))
= (-1β(β―βπ))) |
24 | | psgnfix.z |
. . . . . . . 8
β’ π = (SymGrpβπ) |
25 | | simplll 774 |
. . . . . . . . 9
β’ ((((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
)) β π β Fin) |
26 | 25 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β π β Fin) |
27 | | simplll 774 |
. . . . . . . 8
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β π β Word π
) |
28 | | simprr3 1224 |
. . . . . . . . 9
β’ (((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β π β Word π
) |
29 | 28 | adantr 482 |
. . . . . . . 8
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β π β Word π
) |
30 | | simplrl 776 |
. . . . . . . . . 10
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β ((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ})) |
31 | | 3simpa 1149 |
. . . . . . . . . . . 12
β’ ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
) β (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π))) |
32 | 31 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
)) β (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π))) |
33 | 32 | ad2antlr 726 |
. . . . . . . . . 10
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π))) |
34 | | simplrl 776 |
. . . . . . . . . . 11
β’ (((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β (β―βπ) = (β―βπ)) |
35 | 34 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β (β―βπ) = (β―βπ)) |
36 | | simplrr 777 |
. . . . . . . . . . 11
β’ (((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))) |
37 | 36 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β βπ β
(0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))) |
38 | | psgnfix.p |
. . . . . . . . . . . . 13
β’ π =
(Baseβ(SymGrpβπ)) |
39 | | psgnfix.s |
. . . . . . . . . . . . 13
β’ π = (SymGrpβ(π β {πΎ})) |
40 | 38, 13, 39, 24, 14 | psgndiflemB 21027 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π)) β ((π β Word π
β§ (β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))) β π = (π Ξ£g π)))) |
41 | 40 | imp31 419 |
. . . . . . . . . . 11
β’
(((((π β Fin
β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π))) β§ (π β Word π
β§ (β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β π = (π Ξ£g π)) |
42 | 41 | eqcomd 2739 |
. . . . . . . . . 10
β’
(((((π β Fin
β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π))) β§ (π β Word π
β§ (β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β (π Ξ£g π) = π) |
43 | 30, 33, 27, 35, 37, 42 | syl23anc 1378 |
. . . . . . . . 9
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β (π Ξ£g π) = π) |
44 | | id 22 |
. . . . . . . . . . 11
β’ (π = ((SymGrpβπ) Ξ£g
π) β π = ((SymGrpβπ) Ξ£g π)) |
45 | 24 | eqcomi 2742 |
. . . . . . . . . . . 12
β’
(SymGrpβπ) =
π |
46 | 45 | oveq1i 7371 |
. . . . . . . . . . 11
β’
((SymGrpβπ)
Ξ£g π) = (π Ξ£g π) |
47 | 44, 46 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π = ((SymGrpβπ) Ξ£g
π) β π = (π Ξ£g π)) |
48 | 47 | adantl 483 |
. . . . . . . . 9
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β π = (π Ξ£g π)) |
49 | 43, 48 | eqtrd 2773 |
. . . . . . . 8
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β (π Ξ£g π) = (π Ξ£g π)) |
50 | 24, 14, 26, 27, 29, 49 | psgnuni 19289 |
. . . . . . 7
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β
(-1β(β―βπ))
= (-1β(β―βπ))) |
51 | 23, 50 | eqtrd 2773 |
. . . . . 6
β’ ((((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β§ π = ((SymGrpβπ) Ξ£g π)) β
(-1β(β―βπ))
= (-1β(β―βπ))) |
52 | 51 | ex 414 |
. . . . 5
β’ (((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β§ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
))) β (π = ((SymGrpβπ) Ξ£g π) β
(-1β(β―βπ))
= (-1β(β―βπ)))) |
53 | 52 | ex 414 |
. . . 4
β’ ((π β Word π
β§ ((β―βπ) = (β―βπ) β§ βπ β (0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)))) β ((((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
)) β (π = ((SymGrpβπ) Ξ£g π) β
(-1β(β―βπ))
= (-1β(β―βπ))))) |
54 | 53 | rexlimiva 3141 |
. . 3
β’
(βπ β
Word π
((β―βπ) = (β―βπ) β§ βπ β
(0..^(β―βπ))(((πβπ)βπΎ) = πΎ β§ βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ))) β ((((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
)) β (π = ((SymGrpβπ) Ξ£g π) β
(-1β(β―βπ))
= (-1β(β―βπ))))) |
55 | 20, 54 | mpcom 38 |
. 2
β’ ((((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β§ (π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
)) β (π = ((SymGrpβπ) Ξ£g π) β
(-1β(β―βπ))
= (-1β(β―βπ)))) |
56 | 55 | ex 414 |
1
β’ (((π β Fin β§ πΎ β π) β§ π β {π β π β£ (πβπΎ) = πΎ}) β ((π β Word π β§ (π βΎ (π β {πΎ})) = (π Ξ£g π) β§ π β Word π
) β (π = ((SymGrpβπ) Ξ£g π) β
(-1β(β―βπ))
= (-1β(β―βπ))))) |