Step | Hyp | Ref
| Expression |
1 | | partfun 6649 |
. . . 4
β’ (π₯ β π· β¦ if(π₯ β {πΌ, π½}, βͺ ({πΌ, π½} β {π₯}), π₯)) = ((π₯ β (π· β© {πΌ, π½}) β¦ βͺ
({πΌ, π½} β {π₯})) βͺ (π₯ β (π· β {πΌ, π½}) β¦ π₯)) |
2 | 1 | a1i 11 |
. . 3
β’ (π β (π₯ β π· β¦ if(π₯ β {πΌ, π½}, βͺ ({πΌ, π½} β {π₯}), π₯)) = ((π₯ β (π· β© {πΌ, π½}) β¦ βͺ
({πΌ, π½} β {π₯})) βͺ (π₯ β (π· β {πΌ, π½}) β¦ π₯))) |
3 | | cycpm2.i |
. . . . . . 7
β’ (π β πΌ β π·) |
4 | | cycpm2.j |
. . . . . . 7
β’ (π β π½ β π·) |
5 | | cshw1s2 31863 |
. . . . . . 7
β’ ((πΌ β π· β§ π½ β π·) β (β¨βπΌπ½ββ© cyclShift 1) =
β¨βπ½πΌββ©) |
6 | 3, 4, 5 | syl2anc 585 |
. . . . . 6
β’ (π β (β¨βπΌπ½ββ© cyclShift 1) =
β¨βπ½πΌββ©) |
7 | 6 | coeq1d 5818 |
. . . . 5
β’ (π β ((β¨βπΌπ½ββ© cyclShift 1) β β‘β¨βπΌπ½ββ©) = (β¨βπ½πΌββ© β β‘β¨βπΌπ½ββ©)) |
8 | | 0nn0 12433 |
. . . . . . . 8
β’ 0 β
β0 |
9 | 8 | a1i 11 |
. . . . . . 7
β’ (π β 0 β
β0) |
10 | | 1nn0 12434 |
. . . . . . . 8
β’ 1 β
β0 |
11 | 10 | a1i 11 |
. . . . . . 7
β’ (π β 1 β
β0) |
12 | | 0ne1 12229 |
. . . . . . . 8
β’ 0 β
1 |
13 | 12 | a1i 11 |
. . . . . . 7
β’ (π β 0 β 1) |
14 | | cycpm2.1 |
. . . . . . 7
β’ (π β πΌ β π½) |
15 | 9, 4, 11, 3, 13, 3, 4, 14 | coprprop 31660 |
. . . . . 6
β’ (π β ({β¨0, π½β©, β¨1, πΌβ©} β {β¨πΌ, 0β©, β¨π½, 1β©}) = {β¨πΌ, π½β©, β¨π½, πΌβ©}) |
16 | | s2prop 14802 |
. . . . . . . 8
β’ ((π½ β π· β§ πΌ β π·) β β¨βπ½πΌββ© = {β¨0, π½β©, β¨1, πΌβ©}) |
17 | 4, 3, 16 | syl2anc 585 |
. . . . . . 7
β’ (π β β¨βπ½πΌββ© = {β¨0, π½β©, β¨1, πΌβ©}) |
18 | | s2prop 14802 |
. . . . . . . . . 10
β’ ((πΌ β π· β§ π½ β π·) β β¨βπΌπ½ββ© = {β¨0, πΌβ©, β¨1, π½β©}) |
19 | 3, 4, 18 | syl2anc 585 |
. . . . . . . . 9
β’ (π β β¨βπΌπ½ββ© = {β¨0, πΌβ©, β¨1, π½β©}) |
20 | 19 | cnveqd 5832 |
. . . . . . . 8
β’ (π β β‘β¨βπΌπ½ββ© = β‘{β¨0, πΌβ©, β¨1, π½β©}) |
21 | | cnvprop 31657 |
. . . . . . . . 9
β’ (((0
β β0 β§ πΌ β π·) β§ (1 β β0 β§
π½ β π·)) β β‘{β¨0, πΌβ©, β¨1, π½β©} = {β¨πΌ, 0β©, β¨π½, 1β©}) |
22 | 9, 3, 11, 4, 21 | syl22anc 838 |
. . . . . . . 8
β’ (π β β‘{β¨0, πΌβ©, β¨1, π½β©} = {β¨πΌ, 0β©, β¨π½, 1β©}) |
23 | 20, 22 | eqtrd 2773 |
. . . . . . 7
β’ (π β β‘β¨βπΌπ½ββ© = {β¨πΌ, 0β©, β¨π½, 1β©}) |
24 | 17, 23 | coeq12d 5821 |
. . . . . 6
β’ (π β (β¨βπ½πΌββ© β β‘β¨βπΌπ½ββ©) = ({β¨0, π½β©, β¨1, πΌβ©} β {β¨πΌ, 0β©, β¨π½, 1β©})) |
25 | 3, 4, 4, 3, 14 | mptprop 31659 |
. . . . . . 7
β’ (π β {β¨πΌ, π½β©, β¨π½, πΌβ©} = (π₯ β {πΌ, π½} β¦ if(π₯ = πΌ, π½, πΌ))) |
26 | 3, 4 | prssd 4783 |
. . . . . . . . . 10
β’ (π β {πΌ, π½} β π·) |
27 | | df-ss 3928 |
. . . . . . . . . 10
β’ ({πΌ, π½} β π· β ({πΌ, π½} β© π·) = {πΌ, π½}) |
28 | 26, 27 | sylib 217 |
. . . . . . . . 9
β’ (π β ({πΌ, π½} β© π·) = {πΌ, π½}) |
29 | | incom 4162 |
. . . . . . . . 9
β’ ({πΌ, π½} β© π·) = (π· β© {πΌ, π½}) |
30 | 28, 29 | eqtr3di 2788 |
. . . . . . . 8
β’ (π β {πΌ, π½} = (π· β© {πΌ, π½})) |
31 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β {πΌ, π½}) β§ π₯ = πΌ) β π₯ = πΌ) |
32 | 31 | sneqd 4599 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β {πΌ, π½}) β§ π₯ = πΌ) β {π₯} = {πΌ}) |
33 | 32 | difeq2d 4083 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β {πΌ, π½}) β§ π₯ = πΌ) β ({πΌ, π½} β {π₯}) = ({πΌ, π½} β {πΌ})) |
34 | 33 | unieqd 4880 |
. . . . . . . . . 10
β’ (((π β§ π₯ β {πΌ, π½}) β§ π₯ = πΌ) β βͺ
({πΌ, π½} β {π₯}) = βͺ ({πΌ, π½} β {πΌ})) |
35 | | difprsn1 4761 |
. . . . . . . . . . . . . 14
β’ (πΌ β π½ β ({πΌ, π½} β {πΌ}) = {π½}) |
36 | 35 | unieqd 4880 |
. . . . . . . . . . . . 13
β’ (πΌ β π½ β βͺ ({πΌ, π½} β {πΌ}) = βͺ {π½}) |
37 | 14, 36 | syl 17 |
. . . . . . . . . . . 12
β’ (π β βͺ ({πΌ,
π½} β {πΌ}) = βͺ {π½}) |
38 | | unisng 4887 |
. . . . . . . . . . . . 13
β’ (π½ β π· β βͺ {π½} = π½) |
39 | 4, 38 | syl 17 |
. . . . . . . . . . . 12
β’ (π β βͺ {π½}
= π½) |
40 | 37, 39 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β βͺ ({πΌ,
π½} β {πΌ}) = π½) |
41 | 40 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β {πΌ, π½}) β§ π₯ = πΌ) β βͺ
({πΌ, π½} β {πΌ}) = π½) |
42 | 34, 41 | eqtr2d 2774 |
. . . . . . . . 9
β’ (((π β§ π₯ β {πΌ, π½}) β§ π₯ = πΌ) β π½ = βͺ ({πΌ, π½} β {π₯})) |
43 | | vex 3448 |
. . . . . . . . . . . . . . . . 17
β’ π₯ β V |
44 | 43 | elpr 4610 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β {πΌ, π½} β (π₯ = πΌ β¨ π₯ = π½)) |
45 | | df-or 847 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = πΌ β¨ π₯ = π½) β (Β¬ π₯ = πΌ β π₯ = π½)) |
46 | 44, 45 | sylbb 218 |
. . . . . . . . . . . . . . 15
β’ (π₯ β {πΌ, π½} β (Β¬ π₯ = πΌ β π₯ = π½)) |
47 | 46 | imp 408 |
. . . . . . . . . . . . . 14
β’ ((π₯ β {πΌ, π½} β§ Β¬ π₯ = πΌ) β π₯ = π½) |
48 | 47 | adantll 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β {πΌ, π½}) β§ Β¬ π₯ = πΌ) β π₯ = π½) |
49 | 48 | sneqd 4599 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β {πΌ, π½}) β§ Β¬ π₯ = πΌ) β {π₯} = {π½}) |
50 | 49 | difeq2d 4083 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β {πΌ, π½}) β§ Β¬ π₯ = πΌ) β ({πΌ, π½} β {π₯}) = ({πΌ, π½} β {π½})) |
51 | 50 | unieqd 4880 |
. . . . . . . . . 10
β’ (((π β§ π₯ β {πΌ, π½}) β§ Β¬ π₯ = πΌ) β βͺ
({πΌ, π½} β {π₯}) = βͺ ({πΌ, π½} β {π½})) |
52 | | difprsn2 4762 |
. . . . . . . . . . . . . 14
β’ (πΌ β π½ β ({πΌ, π½} β {π½}) = {πΌ}) |
53 | 52 | unieqd 4880 |
. . . . . . . . . . . . 13
β’ (πΌ β π½ β βͺ ({πΌ, π½} β {π½}) = βͺ {πΌ}) |
54 | 14, 53 | syl 17 |
. . . . . . . . . . . 12
β’ (π β βͺ ({πΌ,
π½} β {π½}) = βͺ {πΌ}) |
55 | | unisng 4887 |
. . . . . . . . . . . . 13
β’ (πΌ β π· β βͺ {πΌ} = πΌ) |
56 | 3, 55 | syl 17 |
. . . . . . . . . . . 12
β’ (π β βͺ {πΌ}
= πΌ) |
57 | 54, 56 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β βͺ ({πΌ,
π½} β {π½}) = πΌ) |
58 | 57 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β {πΌ, π½}) β§ Β¬ π₯ = πΌ) β βͺ
({πΌ, π½} β {π½}) = πΌ) |
59 | 51, 58 | eqtr2d 2774 |
. . . . . . . . 9
β’ (((π β§ π₯ β {πΌ, π½}) β§ Β¬ π₯ = πΌ) β πΌ = βͺ ({πΌ, π½} β {π₯})) |
60 | 42, 59 | ifeqda 4523 |
. . . . . . . 8
β’ ((π β§ π₯ β {πΌ, π½}) β if(π₯ = πΌ, π½, πΌ) = βͺ ({πΌ, π½} β {π₯})) |
61 | 30, 60 | mpteq12dva 5195 |
. . . . . . 7
β’ (π β (π₯ β {πΌ, π½} β¦ if(π₯ = πΌ, π½, πΌ)) = (π₯ β (π· β© {πΌ, π½}) β¦ βͺ
({πΌ, π½} β {π₯}))) |
62 | 25, 61 | eqtr2d 2774 |
. . . . . 6
β’ (π β (π₯ β (π· β© {πΌ, π½}) β¦ βͺ
({πΌ, π½} β {π₯})) = {β¨πΌ, π½β©, β¨π½, πΌβ©}) |
63 | 15, 24, 62 | 3eqtr4d 2783 |
. . . . 5
β’ (π β (β¨βπ½πΌββ© β β‘β¨βπΌπ½ββ©) = (π₯ β (π· β© {πΌ, π½}) β¦ βͺ
({πΌ, π½} β {π₯}))) |
64 | 7, 63 | eqtrd 2773 |
. . . 4
β’ (π β ((β¨βπΌπ½ββ© cyclShift 1) β β‘β¨βπΌπ½ββ©) = (π₯ β (π· β© {πΌ, π½}) β¦ βͺ
({πΌ, π½} β {π₯}))) |
65 | 3, 4 | s2rn 31849 |
. . . . . . 7
β’ (π β ran β¨βπΌπ½ββ© = {πΌ, π½}) |
66 | 65 | difeq2d 4083 |
. . . . . 6
β’ (π β (π· β ran β¨βπΌπ½ββ©) = (π· β {πΌ, π½})) |
67 | 66 | reseq2d 5938 |
. . . . 5
β’ (π β ( I βΎ (π· β ran β¨βπΌπ½ββ©)) = ( I βΎ (π· β {πΌ, π½}))) |
68 | | mptresid 6005 |
. . . . 5
β’ ( I
βΎ (π· β {πΌ, π½})) = (π₯ β (π· β {πΌ, π½}) β¦ π₯) |
69 | 67, 68 | eqtrdi 2789 |
. . . 4
β’ (π β ( I βΎ (π· β ran β¨βπΌπ½ββ©)) = (π₯ β (π· β {πΌ, π½}) β¦ π₯)) |
70 | 64, 69 | uneq12d 4125 |
. . 3
β’ (π β (((β¨βπΌπ½ββ© cyclShift 1) β β‘β¨βπΌπ½ββ©) βͺ ( I βΎ (π· β ran β¨βπΌπ½ββ©))) = ((π₯ β (π· β© {πΌ, π½}) β¦ βͺ
({πΌ, π½} β {π₯})) βͺ (π₯ β (π· β {πΌ, π½}) β¦ π₯))) |
71 | | uncom 4114 |
. . . 4
β’
(((β¨βπΌπ½ββ© cyclShift 1) β β‘β¨βπΌπ½ββ©) βͺ ( I βΎ (π· β ran β¨βπΌπ½ββ©))) = (( I βΎ (π· β ran β¨βπΌπ½ββ©)) βͺ ((β¨βπΌπ½ββ© cyclShift 1) β β‘β¨βπΌπ½ββ©)) |
72 | 71 | a1i 11 |
. . 3
β’ (π β (((β¨βπΌπ½ββ© cyclShift 1) β β‘β¨βπΌπ½ββ©) βͺ ( I βΎ (π· β ran β¨βπΌπ½ββ©))) = (( I βΎ (π· β ran β¨βπΌπ½ββ©)) βͺ ((β¨βπΌπ½ββ© cyclShift 1) β β‘β¨βπΌπ½ββ©))) |
73 | 2, 70, 72 | 3eqtr2rd 2780 |
. 2
β’ (π β (( I βΎ (π· β ran β¨βπΌπ½ββ©)) βͺ ((β¨βπΌπ½ββ© cyclShift 1) β β‘β¨βπΌπ½ββ©)) = (π₯ β π· β¦ if(π₯ β {πΌ, π½}, βͺ ({πΌ, π½} β {π₯}), π₯))) |
74 | | cycpm2.c |
. . 3
β’ πΆ = (toCycβπ·) |
75 | | cycpm2.d |
. . 3
β’ (π β π· β π) |
76 | 3, 4 | s2cld 14766 |
. . 3
β’ (π β β¨βπΌπ½ββ© β Word π·) |
77 | 3, 4, 14 | s2f1 31850 |
. . 3
β’ (π β β¨βπΌπ½ββ©:dom β¨βπΌπ½ββ©β1-1βπ·) |
78 | 74, 75, 76, 77 | tocycfv 32007 |
. 2
β’ (π β (πΆββ¨βπΌπ½ββ©) = (( I βΎ (π· β ran β¨βπΌπ½ββ©)) βͺ ((β¨βπΌπ½ββ© cyclShift 1) β β‘β¨βπΌπ½ββ©))) |
79 | | enpr2 9943 |
. . . 4
β’ ((πΌ β π· β§ π½ β π· β§ πΌ β π½) β {πΌ, π½} β 2o) |
80 | 3, 4, 14, 79 | syl3anc 1372 |
. . 3
β’ (π β {πΌ, π½} β 2o) |
81 | | cycpm2tr.t |
. . . 4
β’ π = (pmTrspβπ·) |
82 | 81 | pmtrval 19238 |
. . 3
β’ ((π· β π β§ {πΌ, π½} β π· β§ {πΌ, π½} β 2o) β (πβ{πΌ, π½}) = (π₯ β π· β¦ if(π₯ β {πΌ, π½}, βͺ ({πΌ, π½} β {π₯}), π₯))) |
83 | 75, 26, 80, 82 | syl3anc 1372 |
. 2
β’ (π β (πβ{πΌ, π½}) = (π₯ β π· β¦ if(π₯ β {πΌ, π½}, βͺ ({πΌ, π½} β {π₯}), π₯))) |
84 | 73, 78, 83 | 3eqtr4d 2783 |
1
β’ (π β (πΆββ¨βπΌπ½ββ©) = (πβ{πΌ, π½})) |