Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . 5
β’
(((((π· β π β§ π β (0...π)) β§ π β πΆ) β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (πβπ’) = π) |
2 | | cycpmconjs.m |
. . . . . . . 8
β’ π = (toCycβπ·) |
3 | | simplll 774 |
. . . . . . . 8
β’ ((((π· β π β§ π β (0...π)) β§ π β πΆ) β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β π· β π) |
4 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π· β π β§ π β (0...π)) β§ π β πΆ) β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) |
5 | 4 | elin1d 4159 |
. . . . . . . . 9
β’ ((((π· β π β§ π β (0...π)) β§ π β πΆ) β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
6 | | elrabi 3640 |
. . . . . . . . 9
β’ (π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β π’ β Word π·) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
β’ ((((π· β π β§ π β (0...π)) β§ π β πΆ) β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β π’ β Word π·) |
8 | | id 22 |
. . . . . . . . . . . 12
β’ (π€ = π’ β π€ = π’) |
9 | | dmeq 5860 |
. . . . . . . . . . . 12
β’ (π€ = π’ β dom π€ = dom π’) |
10 | | eqidd 2734 |
. . . . . . . . . . . 12
β’ (π€ = π’ β π· = π·) |
11 | 8, 9, 10 | f1eq123d 6777 |
. . . . . . . . . . 11
β’ (π€ = π’ β (π€:dom π€β1-1βπ· β π’:dom π’β1-1βπ·)) |
12 | 11 | elrab 3646 |
. . . . . . . . . 10
β’ (π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β (π’ β Word π· β§ π’:dom π’β1-1βπ·)) |
13 | 12 | simprbi 498 |
. . . . . . . . 9
β’ (π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β π’:dom π’β1-1βπ·) |
14 | 5, 13 | syl 17 |
. . . . . . . 8
β’ ((((π· β π β§ π β (0...π)) β§ π β πΆ) β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β π’:dom π’β1-1βπ·) |
15 | | cycpmconjs.s |
. . . . . . . 8
β’ π = (SymGrpβπ·) |
16 | 2, 3, 7, 14, 15 | cycpmcl 32014 |
. . . . . . 7
β’ ((((π· β π β§ π β (0...π)) β§ π β πΆ) β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β (πβπ’) β (Baseβπ)) |
17 | 16 | adantr 482 |
. . . . . 6
β’
(((((π· β π β§ π β (0...π)) β§ π β πΆ) β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (πβπ’) β (Baseβπ)) |
18 | | cycpmgcl.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
19 | 17, 18 | eleqtrrdi 2845 |
. . . . 5
β’
(((((π· β π β§ π β (0...π)) β§ π β πΆ) β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (πβπ’) β π΅) |
20 | 1, 19 | eqeltrrd 2835 |
. . . 4
β’
(((((π· β π β§ π β (0...π)) β§ π β πΆ) β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π β π΅) |
21 | | nfcv 2904 |
. . . . 5
β’
β²π’π |
22 | | simpl 484 |
. . . . . . 7
β’ ((π· β π β§ π β (0...π)) β π· β π) |
23 | 2, 15, 18 | tocycf 32015 |
. . . . . . 7
β’ (π· β π β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆπ΅) |
24 | | ffn 6669 |
. . . . . . 7
β’ (π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆπ΅ β π Fn {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
25 | 22, 23, 24 | 3syl 18 |
. . . . . 6
β’ ((π· β π β§ π β (0...π)) β π Fn {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
26 | 25 | adantr 482 |
. . . . 5
β’ (((π· β π β§ π β (0...π)) β§ π β πΆ) β π Fn {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
27 | | cycpmconjs.c |
. . . . . . . 8
β’ πΆ = (π β (β‘β― β {π})) |
28 | 27 | eleq2i 2826 |
. . . . . . 7
β’ (π β πΆ β π β (π β (β‘β― β {π}))) |
29 | 28 | a1i 11 |
. . . . . 6
β’ ((π· β π β§ π β (0...π)) β (π β πΆ β π β (π β (β‘β― β {π})))) |
30 | 29 | biimpa 478 |
. . . . 5
β’ (((π· β π β§ π β (0...π)) β§ π β πΆ) β π β (π β (β‘β― β {π}))) |
31 | 21, 26, 30 | fvelimad 6910 |
. . . 4
β’ (((π· β π β§ π β (0...π)) β§ π β πΆ) β βπ’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))(πβπ’) = π) |
32 | 20, 31 | r19.29a 3156 |
. . 3
β’ (((π· β π β§ π β (0...π)) β§ π β πΆ) β π β π΅) |
33 | 32 | ex 414 |
. 2
β’ ((π· β π β§ π β (0...π)) β (π β πΆ β π β π΅)) |
34 | 33 | ssrdv 3951 |
1
β’ ((π· β π β§ π β (0...π)) β πΆ β π΅) |