Description: Closure of the 3-cycles in the permutations. (Contributed by Thierry Arnoux, 19-Sep-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cycpm3.c | |- C = ( toCyc ` D ) |
|
| cycpm3.s | |- S = ( SymGrp ` D ) |
||
| cycpm3.d | |- ( ph -> D e. V ) |
||
| cycpm3.i | |- ( ph -> I e. D ) |
||
| cycpm3.j | |- ( ph -> J e. D ) |
||
| cycpm3.k | |- ( ph -> K e. D ) |
||
| cycpm3.1 | |- ( ph -> I =/= J ) |
||
| cycpm3.2 | |- ( ph -> J =/= K ) |
||
| cycpm3.3 | |- ( ph -> K =/= I ) |
||
| Assertion | cycpm3cl | |- ( ph -> ( C ` <" I J K "> ) e. ( Base ` S ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cycpm3.c | |- C = ( toCyc ` D ) |
|
| 2 | cycpm3.s | |- S = ( SymGrp ` D ) |
|
| 3 | cycpm3.d | |- ( ph -> D e. V ) |
|
| 4 | cycpm3.i | |- ( ph -> I e. D ) |
|
| 5 | cycpm3.j | |- ( ph -> J e. D ) |
|
| 6 | cycpm3.k | |- ( ph -> K e. D ) |
|
| 7 | cycpm3.1 | |- ( ph -> I =/= J ) |
|
| 8 | cycpm3.2 | |- ( ph -> J =/= K ) |
|
| 9 | cycpm3.3 | |- ( ph -> K =/= I ) |
|
| 10 | 4 5 6 | s3cld | |- ( ph -> <" I J K "> e. Word D ) |
| 11 | 4 5 6 7 8 9 | s3f1 | |- ( ph -> <" I J K "> : dom <" I J K "> -1-1-> D ) |
| 12 | 1 3 10 11 2 | cycpmcl | |- ( ph -> ( C ` <" I J K "> ) e. ( Base ` S ) ) |