Step | Hyp | Ref
| Expression |
1 | | frgpup.w |
. . . . . . 7
β’ π = ( I βWord (πΌ Γ
2o)) |
2 | | frgpup.r |
. . . . . . 7
β’ βΌ = (
~FG βπΌ) |
3 | 1, 2 | efgval 19506 |
. . . . . 6
β’ βΌ =
β© {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))} |
4 | | coeq2 5819 |
. . . . . . . . . . . . 13
β’ (π’ = π£ β (π β π’) = (π β π£)) |
5 | 4 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π’ = π£ β (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))) |
6 | | eqid 2737 |
. . . . . . . . . . . 12
β’
{β¨π’, π£β© β£ (π» Ξ£g
(π β π’)) = (π» Ξ£g (π β π£))} = {β¨π’, π£β© β£ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))} |
7 | 5, 6 | eqer 8690 |
. . . . . . . . . . 11
β’
{β¨π’, π£β© β£ (π» Ξ£g
(π β π’)) = (π» Ξ£g (π β π£))} Er V |
8 | 7 | a1i 11 |
. . . . . . . . . 10
β’ (π β {β¨π’, π£β© β£ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))} Er V) |
9 | | ssv 3973 |
. . . . . . . . . . 11
β’ π β V |
10 | 9 | a1i 11 |
. . . . . . . . . 10
β’ (π β π β V) |
11 | 8, 10 | erinxp 8737 |
. . . . . . . . 9
β’ (π β ({β¨π’, π£β© β£ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))} β© (π Γ π)) Er π) |
12 | | df-xp 5644 |
. . . . . . . . . . . . 13
β’ (π Γ π) = {β¨π’, π£β© β£ (π’ β π β§ π£ β π)} |
13 | 12 | ineq1i 4173 |
. . . . . . . . . . . 12
β’ ((π Γ π) β© {β¨π’, π£β© β£ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))}) = ({β¨π’, π£β© β£ (π’ β π β§ π£ β π)} β© {β¨π’, π£β© β£ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))}) |
14 | | incom 4166 |
. . . . . . . . . . . 12
β’ ((π Γ π) β© {β¨π’, π£β© β£ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))}) = ({β¨π’, π£β© β£ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))} β© (π Γ π)) |
15 | | inopab 5790 |
. . . . . . . . . . . 12
β’
({β¨π’, π£β© β£ (π’ β π β§ π£ β π)} β© {β¨π’, π£β© β£ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))}) = {β¨π’, π£β© β£ ((π’ β π β§ π£ β π) β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} |
16 | 13, 14, 15 | 3eqtr3i 2773 |
. . . . . . . . . . 11
β’
({β¨π’, π£β© β£ (π» Ξ£g
(π β π’)) = (π» Ξ£g (π β π£))} β© (π Γ π)) = {β¨π’, π£β© β£ ((π’ β π β§ π£ β π) β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} |
17 | | vex 3452 |
. . . . . . . . . . . . . 14
β’ π’ β V |
18 | | vex 3452 |
. . . . . . . . . . . . . 14
β’ π£ β V |
19 | 17, 18 | prss 4785 |
. . . . . . . . . . . . 13
β’ ((π’ β π β§ π£ β π) β {π’, π£} β π) |
20 | 19 | anbi1i 625 |
. . . . . . . . . . . 12
β’ (((π’ β π β§ π£ β π) β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))) β ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))) |
21 | 20 | opabbii 5177 |
. . . . . . . . . . 11
β’
{β¨π’, π£β© β£ ((π’ β π β§ π£ β π) β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} = {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} |
22 | 16, 21 | eqtri 2765 |
. . . . . . . . . 10
β’
({β¨π’, π£β© β£ (π» Ξ£g
(π β π’)) = (π» Ξ£g (π β π£))} β© (π Γ π)) = {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} |
23 | | ereq1 8662 |
. . . . . . . . . 10
β’
(({β¨π’, π£β© β£ (π» Ξ£g
(π β π’)) = (π» Ξ£g (π β π£))} β© (π Γ π)) = {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β (({β¨π’, π£β© β£ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))} β© (π Γ π)) Er π β {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} Er π)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . 9
β’
(({β¨π’, π£β© β£ (π» Ξ£g
(π β π’)) = (π» Ξ£g (π β π£))} β© (π Γ π)) Er π β {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} Er π) |
25 | 11, 24 | sylib 217 |
. . . . . . . 8
β’ (π β {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} Er π) |
26 | | simplrl 776 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β π₯ β π) |
27 | | fviss 6923 |
. . . . . . . . . . . . . . 15
β’ ( I
βWord (πΌ Γ
2o)) β Word (πΌ Γ 2o) |
28 | 1, 27 | eqsstri 3983 |
. . . . . . . . . . . . . 14
β’ π β Word (πΌ Γ 2o) |
29 | 28, 26 | sselid 3947 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β π₯ β Word (πΌ Γ 2o)) |
30 | | opelxpi 5675 |
. . . . . . . . . . . . . . 15
β’ ((π β πΌ β§ π β 2o) β β¨π, πβ© β (πΌ Γ 2o)) |
31 | 30 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β β¨π, πβ© β (πΌ Γ 2o)) |
32 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β π β πΌ) |
33 | | 2oconcl 8454 |
. . . . . . . . . . . . . . . 16
β’ (π β 2o β
(1o β π)
β 2o) |
34 | 33 | ad2antll 728 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (1o
β π) β
2o) |
35 | 32, 34 | opelxpd 5676 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β β¨π, (1o β π)β© β (πΌ Γ
2o)) |
36 | 31, 35 | s2cld 14767 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ© β Word (πΌ Γ
2o)) |
37 | | splcl 14647 |
. . . . . . . . . . . . 13
β’ ((π₯ β Word (πΌ Γ 2o) β§
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ© β Word (πΌ Γ 2o)) β
(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β Word
(πΌ Γ
2o)) |
38 | 29, 36, 37 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β Word
(πΌ Γ
2o)) |
39 | 1 | efgrcl 19504 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β (πΌ β V β§ π = Word (πΌ Γ 2o))) |
40 | 26, 39 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (πΌ β V β§ π = Word (πΌ Γ 2o))) |
41 | 40 | simprd 497 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β π = Word (πΌ Γ 2o)) |
42 | 38, 41 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β π) |
43 | | pfxcl 14572 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β Word (πΌ Γ 2o) β (π₯ prefix π) β Word (πΌ Γ 2o)) |
44 | 29, 43 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π₯ prefix π) β Word (πΌ Γ 2o)) |
45 | | frgpup.b |
. . . . . . . . . . . . . . . . . . 19
β’ π΅ = (Baseβπ») |
46 | | frgpup.n |
. . . . . . . . . . . . . . . . . . 19
β’ π = (invgβπ») |
47 | | frgpup.t |
. . . . . . . . . . . . . . . . . . 19
β’ π = (π¦ β πΌ, π§ β 2o β¦ if(π§ = β
, (πΉβπ¦), (πβ(πΉβπ¦)))) |
48 | | frgpup.h |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π» β Grp) |
49 | | frgpup.i |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΌ β π) |
50 | | frgpup.a |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ:πΌβΆπ΅) |
51 | 45, 46, 47, 48, 49, 50 | frgpuptf 19559 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π:(πΌ Γ 2o)βΆπ΅) |
52 | 51 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β π:(πΌ Γ 2o)βΆπ΅) |
53 | | ccatco 14731 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ prefix π) β Word (πΌ Γ 2o) β§
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ© β Word (πΌ Γ 2o) β§
π:(πΌ Γ 2o)βΆπ΅) β (π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) = ((π β (π₯ prefix π)) ++ (π β β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©))) |
54 | 44, 36, 52, 53 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) = ((π β (π₯ prefix π)) ++ (π β β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©))) |
55 | 54 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
(π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©))) = (π» Ξ£g ((π β (π₯ prefix π)) ++ (π β β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)))) |
56 | 48 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β π» β Grp) |
57 | 56 | grpmndd 18767 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β π» β Mnd) |
58 | | wrdco 14727 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ prefix π) β Word (πΌ Γ 2o) β§ π:(πΌ Γ 2o)βΆπ΅) β (π β (π₯ prefix π)) β Word π΅) |
59 | 44, 52, 58 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β (π₯ prefix π)) β Word π΅) |
60 | | wrdco 14727 |
. . . . . . . . . . . . . . . . 17
β’
((β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ© β Word (πΌ Γ 2o) β§
π:(πΌ Γ 2o)βΆπ΅) β (π β β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) β Word π΅) |
61 | 36, 52, 60 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) β Word π΅) |
62 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(+gβπ») = (+gβπ») |
63 | 45, 62 | gsumccat 18658 |
. . . . . . . . . . . . . . . 16
β’ ((π» β Mnd β§ (π β (π₯ prefix π)) β Word π΅ β§ (π β β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) β Word π΅) β (π» Ξ£g ((π β (π₯ prefix π)) ++ (π β β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©))) = ((π» Ξ£g (π β (π₯ prefix π)))(+gβπ»)(π» Ξ£g (π β
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)))) |
64 | 57, 59, 61, 63 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
((π β (π₯ prefix π)) ++ (π β β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©))) = ((π» Ξ£g (π β (π₯ prefix π)))(+gβπ»)(π» Ξ£g (π β
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)))) |
65 | 52, 31, 35 | s2co 14816 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) = β¨β(πββ¨π, πβ©)(πββ¨π, (1o β π)β©)ββ©) |
66 | | df-ov 7365 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πππ) = (πββ¨π, πβ©) |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (πππ) = (πββ¨π, πβ©)) |
68 | 66 | fveq2i 6850 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πβ(πππ)) = (πβ(πββ¨π, πβ©)) |
69 | | df-ov 7365 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π(π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©)π) = ((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©)ββ¨π, πβ©) |
70 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
71 | 70 | efgmval 19501 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β πΌ β§ π β 2o) β (π(π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©)π) = β¨π, (1o β π)β©) |
72 | 69, 71 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β πΌ β§ π β 2o) β ((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©)ββ¨π, πβ©) = β¨π, (1o β π)β©) |
73 | 72 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β ((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©)ββ¨π, πβ©) = β¨π, (1o β π)β©) |
74 | 73 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (πβ((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©)ββ¨π, πβ©)) = (πββ¨π, (1o β π)β©)) |
75 | 45, 46, 47, 48, 49, 50, 70 | frgpuptinv 19560 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ β¨π, πβ© β (πΌ Γ 2o)) β (πβ((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©)ββ¨π, πβ©)) = (πβ(πββ¨π, πβ©))) |
76 | 30, 75 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π β πΌ β§ π β 2o)) β (πβ((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©)ββ¨π, πβ©)) = (πβ(πββ¨π, πβ©))) |
77 | 76 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (πβ((π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©)ββ¨π, πβ©)) = (πβ(πββ¨π, πβ©))) |
78 | 74, 77 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (πββ¨π, (1o β π)β©) = (πβ(πββ¨π, πβ©))) |
79 | 68, 78 | eqtr4id 2796 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (πβ(πππ)) = (πββ¨π, (1o β π)β©)) |
80 | 67, 79 | s2eqd 14759 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β
β¨β(πππ)(πβ(πππ))ββ© = β¨β(πββ¨π, πβ©)(πββ¨π, (1o β π)β©)ββ©) |
81 | 65, 80 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) = β¨β(πππ)(πβ(πππ))ββ©) |
82 | 81 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
(π β
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) = (π» Ξ£g
β¨β(πππ)(πβ(πππ))ββ©)) |
83 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β π β
2o) |
84 | 52, 32, 83 | fovcdmd 7531 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (πππ) β π΅) |
85 | 45, 46 | grpinvcl 18805 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π» β Grp β§ (πππ) β π΅) β (πβ(πππ)) β π΅) |
86 | 56, 84, 85 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (πβ(πππ)) β π΅) |
87 | 45, 62 | gsumws2 18659 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π» β Mnd β§ (πππ) β π΅ β§ (πβ(πππ)) β π΅) β (π» Ξ£g
β¨β(πππ)(πβ(πππ))ββ©) = ((πππ)(+gβπ»)(πβ(πππ)))) |
88 | 57, 84, 86, 87 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
β¨β(πππ)(πβ(πππ))ββ©) = ((πππ)(+gβπ»)(πβ(πππ)))) |
89 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’
(0gβπ») = (0gβπ») |
90 | 45, 62, 89, 46 | grprinv 18808 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π» β Grp β§ (πππ) β π΅) β ((πππ)(+gβπ»)(πβ(πππ))) = (0gβπ»)) |
91 | 56, 84, 90 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β ((πππ)(+gβπ»)(πβ(πππ))) = (0gβπ»)) |
92 | 82, 88, 91 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
(π β
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) =
(0gβπ»)) |
93 | 92 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β ((π» Ξ£g
(π β (π₯ prefix π)))(+gβπ»)(π» Ξ£g (π β
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©))) = ((π» Ξ£g (π β (π₯ prefix π)))(+gβπ»)(0gβπ»))) |
94 | 45 | gsumwcl 18656 |
. . . . . . . . . . . . . . . . . 18
β’ ((π» β Mnd β§ (π β (π₯ prefix π)) β Word π΅) β (π» Ξ£g (π β (π₯ prefix π))) β π΅) |
95 | 57, 59, 94 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
(π β (π₯ prefix π))) β π΅) |
96 | 45, 62, 89 | grprid 18788 |
. . . . . . . . . . . . . . . . 17
β’ ((π» β Grp β§ (π» Ξ£g
(π β (π₯ prefix π))) β π΅) β ((π» Ξ£g (π β (π₯ prefix π)))(+gβπ»)(0gβπ»)) = (π» Ξ£g (π β (π₯ prefix π)))) |
97 | 56, 95, 96 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β ((π» Ξ£g
(π β (π₯ prefix π)))(+gβπ»)(0gβπ»)) = (π» Ξ£g (π β (π₯ prefix π)))) |
98 | 93, 97 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β ((π» Ξ£g
(π β (π₯ prefix π)))(+gβπ»)(π» Ξ£g (π β
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©))) = (π» Ξ£g (π β (π₯ prefix π)))) |
99 | 55, 64, 98 | 3eqtrrd 2782 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
(π β (π₯ prefix π))) = (π» Ξ£g (π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)))) |
100 | 99 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β ((π» Ξ£g
(π β (π₯ prefix π)))(+gβπ»)(π» Ξ£g (π β (π₯ substr β¨π, (β―βπ₯)β©)))) = ((π» Ξ£g (π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)))(+gβπ»)(π» Ξ£g (π β (π₯ substr β¨π, (β―βπ₯)β©))))) |
101 | | swrdcl 14540 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β Word (πΌ Γ 2o) β (π₯ substr β¨π, (β―βπ₯)β©) β Word (πΌ Γ 2o)) |
102 | 29, 101 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π₯ substr β¨π, (β―βπ₯)β©) β Word (πΌ Γ 2o)) |
103 | | wrdco 14727 |
. . . . . . . . . . . . . . 15
β’ (((π₯ substr β¨π, (β―βπ₯)β©) β Word (πΌ Γ 2o) β§ π:(πΌ Γ 2o)βΆπ΅) β (π β (π₯ substr β¨π, (β―βπ₯)β©)) β Word π΅) |
104 | 102, 52, 103 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β (π₯ substr β¨π, (β―βπ₯)β©)) β Word π΅) |
105 | 45, 62 | gsumccat 18658 |
. . . . . . . . . . . . . 14
β’ ((π» β Mnd β§ (π β (π₯ prefix π)) β Word π΅ β§ (π β (π₯ substr β¨π, (β―βπ₯)β©)) β Word π΅) β (π» Ξ£g ((π β (π₯ prefix π)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©)))) = ((π» Ξ£g (π β (π₯ prefix π)))(+gβπ»)(π» Ξ£g (π β (π₯ substr β¨π, (β―βπ₯)β©))))) |
106 | 57, 59, 104, 105 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
((π β (π₯ prefix π)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©)))) = ((π» Ξ£g (π β (π₯ prefix π)))(+gβπ»)(π» Ξ£g (π β (π₯ substr β¨π, (β―βπ₯)β©))))) |
107 | | ccatcl 14469 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ prefix π) β Word (πΌ Γ 2o) β§
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ© β Word (πΌ Γ 2o)) β
((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) β Word (πΌ Γ
2o)) |
108 | 44, 36, 107 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) β Word (πΌ Γ
2o)) |
109 | | wrdco 14727 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) β Word (πΌ Γ 2o) β§
π:(πΌ Γ 2o)βΆπ΅) β (π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) β Word π΅) |
110 | 108, 52, 109 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) β Word π΅) |
111 | 45, 62 | gsumccat 18658 |
. . . . . . . . . . . . . 14
β’ ((π» β Mnd β§ (π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) β Word π΅ β§ (π β (π₯ substr β¨π, (β―βπ₯)β©)) β Word π΅) β (π» Ξ£g ((π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©)))) = ((π» Ξ£g (π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)))(+gβπ»)(π» Ξ£g (π β (π₯ substr β¨π, (β―βπ₯)β©))))) |
112 | 57, 110, 104, 111 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
((π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©)))) = ((π» Ξ£g (π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)))(+gβπ»)(π» Ξ£g (π β (π₯ substr β¨π, (β―βπ₯)β©))))) |
113 | 100, 106,
112 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
((π β (π₯ prefix π)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©)))) = (π» Ξ£g ((π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©))))) |
114 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β π β
(0...(β―βπ₯))) |
115 | | lencl 14428 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β Word (πΌ Γ 2o) β
(β―βπ₯) β
β0) |
116 | 29, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β
(β―βπ₯) β
β0) |
117 | | nn0uz 12812 |
. . . . . . . . . . . . . . . . . . 19
β’
β0 = (β€β₯β0) |
118 | 116, 117 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β
(β―βπ₯) β
(β€β₯β0)) |
119 | | eluzfz2 13456 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ₯)
β (β€β₯β0) β (β―βπ₯) β
(0...(β―βπ₯))) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β
(β―βπ₯) β
(0...(β―βπ₯))) |
121 | | ccatpfx 14596 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β Word (πΌ Γ 2o) β§ π β
(0...(β―βπ₯))
β§ (β―βπ₯)
β (0...(β―βπ₯))) β ((π₯ prefix π) ++ (π₯ substr β¨π, (β―βπ₯)β©)) = (π₯ prefix (β―βπ₯))) |
122 | 29, 114, 120, 121 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β ((π₯ prefix π) ++ (π₯ substr β¨π, (β―βπ₯)β©)) = (π₯ prefix (β―βπ₯))) |
123 | | pfxid 14579 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β Word (πΌ Γ 2o) β (π₯ prefix (β―βπ₯)) = π₯) |
124 | 29, 123 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π₯ prefix (β―βπ₯)) = π₯) |
125 | 122, 124 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β ((π₯ prefix π) ++ (π₯ substr β¨π, (β―βπ₯)β©)) = π₯) |
126 | 125 | coeq2d 5823 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β ((π₯ prefix π) ++ (π₯ substr β¨π, (β―βπ₯)β©))) = (π β π₯)) |
127 | | ccatco 14731 |
. . . . . . . . . . . . . . 15
β’ (((π₯ prefix π) β Word (πΌ Γ 2o) β§ (π₯ substr β¨π, (β―βπ₯)β©) β Word (πΌ Γ 2o) β§ π:(πΌ Γ 2o)βΆπ΅) β (π β ((π₯ prefix π) ++ (π₯ substr β¨π, (β―βπ₯)β©))) = ((π β (π₯ prefix π)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©)))) |
128 | 44, 102, 52, 127 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β ((π₯ prefix π) ++ (π₯ substr β¨π, (β―βπ₯)β©))) = ((π β (π₯ prefix π)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©)))) |
129 | 126, 128 | eqtr3d 2779 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β π₯) = ((π β (π₯ prefix π)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©)))) |
130 | 129 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
(π β π₯)) = (π» Ξ£g ((π β (π₯ prefix π)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©))))) |
131 | | splval 14646 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π β§ (π β (0...(β―βπ₯)) β§ π β (0...(β―βπ₯)) β§
β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ© β Word (πΌ Γ 2o))) β
(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) = (((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) ++ (π₯ substr β¨π, (β―βπ₯)β©))) |
132 | 26, 114, 114, 36, 131 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) = (((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) ++ (π₯ substr β¨π, (β―βπ₯)β©))) |
133 | 132 | coeq2d 5823 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) = (π β (((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) ++ (π₯ substr β¨π, (β―βπ₯)β©)))) |
134 | | ccatco 14731 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) β Word (πΌ Γ 2o) β§
(π₯ substr β¨π, (β―βπ₯)β©) β Word (πΌ Γ 2o) β§
π:(πΌ Γ 2o)βΆπ΅) β (π β (((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) ++ (π₯ substr β¨π, (β―βπ₯)β©))) = ((π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©)))) |
135 | 108, 102,
52, 134 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β (((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©) ++ (π₯ substr β¨π, (β―βπ₯)β©))) = ((π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©)))) |
136 | 133, 135 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) = ((π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©)))) |
137 | 136 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
(π β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))) = (π» Ξ£g
((π β ((π₯ prefix π) ++ β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©)) ++ (π β (π₯ substr β¨π, (β―βπ₯)β©))))) |
138 | 113, 130,
137 | 3eqtr4d 2787 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β (π» Ξ£g
(π β π₯)) = (π» Ξ£g (π β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)))) |
139 | | vex 3452 |
. . . . . . . . . . . 12
β’ π₯ β V |
140 | | ovex 7395 |
. . . . . . . . . . . 12
β’ (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β
V |
141 | | eleq1 2826 |
. . . . . . . . . . . . . . 15
β’ (π’ = π₯ β (π’ β π β π₯ β π)) |
142 | | eleq1 2826 |
. . . . . . . . . . . . . . 15
β’ (π£ = (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β (π£ β π β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β π)) |
143 | 141, 142 | bi2anan9 638 |
. . . . . . . . . . . . . 14
β’ ((π’ = π₯ β§ π£ = (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) β ((π’ β π β§ π£ β π) β (π₯ β π β§ (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β π))) |
144 | 19, 143 | bitr3id 285 |
. . . . . . . . . . . . 13
β’ ((π’ = π₯ β§ π£ = (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) β ({π’, π£} β π β (π₯ β π β§ (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β π))) |
145 | | coeq2 5819 |
. . . . . . . . . . . . . . 15
β’ (π’ = π₯ β (π β π’) = (π β π₯)) |
146 | 145 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π’ = π₯ β (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π₯))) |
147 | | coeq2 5819 |
. . . . . . . . . . . . . . 15
β’ (π£ = (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β (π β π£) = (π β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))) |
148 | 147 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π£ = (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β (π» Ξ£g
(π β π£)) = (π» Ξ£g (π β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)))) |
149 | 146, 148 | eqeqan12d 2751 |
. . . . . . . . . . . . 13
β’ ((π’ = π₯ β§ π£ = (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) β ((π» Ξ£g
(π β π’)) = (π» Ξ£g (π β π£)) β (π» Ξ£g (π β π₯)) = (π» Ξ£g (π β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))))) |
150 | 144, 149 | anbi12d 632 |
. . . . . . . . . . . 12
β’ ((π’ = π₯ β§ π£ = (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) β (({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))) β ((π₯ β π β§ (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β π) β§ (π» Ξ£g (π β π₯)) = (π» Ξ£g (π β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)))))) |
151 | | eqid 2737 |
. . . . . . . . . . . 12
β’
{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} = {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} |
152 | 139, 140,
150, 151 | braba 5499 |
. . . . . . . . . . 11
β’ (π₯{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β ((π₯ β π β§ (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β π) β§ (π» Ξ£g (π β π₯)) = (π» Ξ£g (π β (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))))) |
153 | 26, 42, 138, 152 | syl21anbrc 1345 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β§ (π β πΌ β§ π β 2o)) β π₯{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) |
154 | 153 | ralrimivva 3198 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π β§ π β (0...(β―βπ₯)))) β βπ β πΌ βπ β 2o π₯{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) |
155 | 154 | ralrimivva 3198 |
. . . . . . . 8
β’ (π β βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) |
156 | 1 | fvexi 6861 |
. . . . . . . . . 10
β’ π β V |
157 | | erex 8679 |
. . . . . . . . . 10
β’
({β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} Er π β (π β V β {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β V)) |
158 | 25, 156, 157 | mpisyl 21 |
. . . . . . . . 9
β’ (π β {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β V) |
159 | | ereq1 8662 |
. . . . . . . . . . 11
β’ (π = {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β (π Er π β {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} Er π)) |
160 | | breq 5112 |
. . . . . . . . . . . . 13
β’ (π = {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β (π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β π₯{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))) |
161 | 160 | 2ralbidv 3213 |
. . . . . . . . . . . 12
β’ (π = {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β (βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β
βπ β πΌ βπ β 2o π₯{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))) |
162 | 161 | 2ralbidv 3213 |
. . . . . . . . . . 11
β’ (π = {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β (βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©) β
βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))) |
163 | 159, 162 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β ((π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)) β
({β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)))) |
164 | 163 | elabg 3633 |
. . . . . . . . 9
β’
({β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β V β ({β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))} β
({β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)))) |
165 | 158, 164 | syl 17 |
. . . . . . . 8
β’ (π β ({β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))} β
({β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} (π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©)))) |
166 | 25, 155, 165 | mpbir2and 712 |
. . . . . . 7
β’ (π β {β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))}) |
167 | | intss1 4929 |
. . . . . . 7
β’
({β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))} β {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))} β β© {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))} β
{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))}) |
168 | 166, 167 | syl 17 |
. . . . . 6
β’ (π β β© {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ β πΌ βπ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π, πβ©β¨π, (1o β π)β©ββ©β©))} β
{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))}) |
169 | 3, 168 | eqsstrid 3997 |
. . . . 5
β’ (π β βΌ β
{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))}) |
170 | 169 | ssbrd 5153 |
. . . 4
β’ (π β (π΄ βΌ πΆ β π΄{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))}πΆ)) |
171 | 170 | imp 408 |
. . 3
β’ ((π β§ π΄ βΌ πΆ) β π΄{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))}πΆ) |
172 | 1, 2 | efger 19507 |
. . . . . 6
β’ βΌ Er
π |
173 | | errel 8664 |
. . . . . 6
β’ ( βΌ Er
π β Rel βΌ
) |
174 | 172, 173 | mp1i 13 |
. . . . 5
β’ (π β Rel βΌ ) |
175 | | brrelex12 5689 |
. . . . 5
β’ ((Rel
βΌ
β§ π΄ βΌ πΆ) β (π΄ β V β§ πΆ β V)) |
176 | 174, 175 | sylan 581 |
. . . 4
β’ ((π β§ π΄ βΌ πΆ) β (π΄ β V β§ πΆ β V)) |
177 | | preq12 4701 |
. . . . . . 7
β’ ((π’ = π΄ β§ π£ = πΆ) β {π’, π£} = {π΄, πΆ}) |
178 | 177 | sseq1d 3980 |
. . . . . 6
β’ ((π’ = π΄ β§ π£ = πΆ) β ({π’, π£} β π β {π΄, πΆ} β π)) |
179 | | coeq2 5819 |
. . . . . . . 8
β’ (π’ = π΄ β (π β π’) = (π β π΄)) |
180 | 179 | oveq2d 7378 |
. . . . . . 7
β’ (π’ = π΄ β (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π΄))) |
181 | | coeq2 5819 |
. . . . . . . 8
β’ (π£ = πΆ β (π β π£) = (π β πΆ)) |
182 | 181 | oveq2d 7378 |
. . . . . . 7
β’ (π£ = πΆ β (π» Ξ£g (π β π£)) = (π» Ξ£g (π β πΆ))) |
183 | 180, 182 | eqeqan12d 2751 |
. . . . . 6
β’ ((π’ = π΄ β§ π£ = πΆ) β ((π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)) β (π» Ξ£g (π β π΄)) = (π» Ξ£g (π β πΆ)))) |
184 | 178, 183 | anbi12d 632 |
. . . . 5
β’ ((π’ = π΄ β§ π£ = πΆ) β (({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£))) β ({π΄, πΆ} β π β§ (π» Ξ£g (π β π΄)) = (π» Ξ£g (π β πΆ))))) |
185 | 184, 151 | brabga 5496 |
. . . 4
β’ ((π΄ β V β§ πΆ β V) β (π΄{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))}πΆ β ({π΄, πΆ} β π β§ (π» Ξ£g (π β π΄)) = (π» Ξ£g (π β πΆ))))) |
186 | 176, 185 | syl 17 |
. . 3
β’ ((π β§ π΄ βΌ πΆ) β (π΄{β¨π’, π£β© β£ ({π’, π£} β π β§ (π» Ξ£g (π β π’)) = (π» Ξ£g (π β π£)))}πΆ β ({π΄, πΆ} β π β§ (π» Ξ£g (π β π΄)) = (π» Ξ£g (π β πΆ))))) |
187 | 171, 186 | mpbid 231 |
. 2
β’ ((π β§ π΄ βΌ πΆ) β ({π΄, πΆ} β π β§ (π» Ξ£g (π β π΄)) = (π» Ξ£g (π β πΆ)))) |
188 | 187 | simprd 497 |
1
β’ ((π β§ π΄ βΌ πΆ) β (π» Ξ£g (π β π΄)) = (π» Ξ£g (π β πΆ))) |