Step | Hyp | Ref
| Expression |
1 | | coeq2 5815 |
. . . . . . 7
β’ (π₯ = β
β (π β π₯) = (π β β
)) |
2 | | co02 6213 |
. . . . . . 7
β’ (π β β
) =
β
|
3 | 1, 2 | eqtrdi 2793 |
. . . . . 6
β’ (π₯ = β
β (π β π₯) = β
) |
4 | 3 | oveq2d 7374 |
. . . . 5
β’ (π₯ = β
β (π Ξ£g
(π β π₯)) = (π Ξ£g
β
)) |
5 | | id 22 |
. . . . 5
β’ (π₯ = β
β π₯ = β
) |
6 | 4, 5 | eqeq12d 2753 |
. . . 4
β’ (π₯ = β
β ((π Ξ£g
(π β π₯)) = π₯ β (π Ξ£g β
) =
β
)) |
7 | 6 | imbi2d 341 |
. . 3
β’ (π₯ = β
β ((πΌ β π β (π Ξ£g (π β π₯)) = π₯) β (πΌ β π β (π Ξ£g β
) =
β
))) |
8 | | coeq2 5815 |
. . . . . 6
β’ (π₯ = π¦ β (π β π₯) = (π β π¦)) |
9 | 8 | oveq2d 7374 |
. . . . 5
β’ (π₯ = π¦ β (π Ξ£g (π β π₯)) = (π Ξ£g (π β π¦))) |
10 | | id 22 |
. . . . 5
β’ (π₯ = π¦ β π₯ = π¦) |
11 | 9, 10 | eqeq12d 2753 |
. . . 4
β’ (π₯ = π¦ β ((π Ξ£g (π β π₯)) = π₯ β (π Ξ£g (π β π¦)) = π¦)) |
12 | 11 | imbi2d 341 |
. . 3
β’ (π₯ = π¦ β ((πΌ β π β (π Ξ£g (π β π₯)) = π₯) β (πΌ β π β (π Ξ£g (π β π¦)) = π¦))) |
13 | | coeq2 5815 |
. . . . . 6
β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β (π β π₯) = (π β (π¦ ++ β¨βπ§ββ©))) |
14 | 13 | oveq2d 7374 |
. . . . 5
β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β (π Ξ£g (π β π₯)) = (π Ξ£g (π β (π¦ ++ β¨βπ§ββ©)))) |
15 | | id 22 |
. . . . 5
β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β π₯ = (π¦ ++ β¨βπ§ββ©)) |
16 | 14, 15 | eqeq12d 2753 |
. . . 4
β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β ((π Ξ£g (π β π₯)) = π₯ β (π Ξ£g (π β (π¦ ++ β¨βπ§ββ©))) = (π¦ ++ β¨βπ§ββ©))) |
17 | 16 | imbi2d 341 |
. . 3
β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β ((πΌ β π β (π Ξ£g (π β π₯)) = π₯) β (πΌ β π β (π Ξ£g (π β (π¦ ++ β¨βπ§ββ©))) = (π¦ ++ β¨βπ§ββ©)))) |
18 | | coeq2 5815 |
. . . . . 6
β’ (π₯ = π β (π β π₯) = (π β π)) |
19 | 18 | oveq2d 7374 |
. . . . 5
β’ (π₯ = π β (π Ξ£g (π β π₯)) = (π Ξ£g (π β π))) |
20 | | id 22 |
. . . . 5
β’ (π₯ = π β π₯ = π) |
21 | 19, 20 | eqeq12d 2753 |
. . . 4
β’ (π₯ = π β ((π Ξ£g (π β π₯)) = π₯ β (π Ξ£g (π β π)) = π)) |
22 | 21 | imbi2d 341 |
. . 3
β’ (π₯ = π β ((πΌ β π β (π Ξ£g (π β π₯)) = π₯) β (πΌ β π β (π Ξ£g (π β π)) = π))) |
23 | | frmdmnd.m |
. . . . . 6
β’ π = (freeMndβπΌ) |
24 | 23 | frmd0 18671 |
. . . . 5
β’ β
=
(0gβπ) |
25 | 24 | gsum0 18540 |
. . . 4
β’ (π Ξ£g
β
) = β
|
26 | 25 | a1i 11 |
. . 3
β’ (πΌ β π β (π Ξ£g β
) =
β
) |
27 | | oveq1 7365 |
. . . . . 6
β’ ((π Ξ£g
(π β π¦)) = π¦ β ((π Ξ£g (π β π¦)) ++ β¨βπ§ββ©) = (π¦ ++ β¨βπ§ββ©)) |
28 | | simprl 770 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β π¦ β Word πΌ) |
29 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β π§ β πΌ) |
30 | 29 | s1cld 14492 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β β¨βπ§ββ© β Word πΌ) |
31 | | frmdgsum.u |
. . . . . . . . . . . . 13
β’ π =
(varFMndβπΌ) |
32 | 31 | vrmdf 18669 |
. . . . . . . . . . . 12
β’ (πΌ β π β π:πΌβΆWord πΌ) |
33 | 32 | adantr 482 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β π:πΌβΆWord πΌ) |
34 | | ccatco 14725 |
. . . . . . . . . . 11
β’ ((π¦ β Word πΌ β§ β¨βπ§ββ© β Word πΌ β§ π:πΌβΆWord πΌ) β (π β (π¦ ++ β¨βπ§ββ©)) = ((π β π¦) ++ (π β β¨βπ§ββ©))) |
35 | 28, 30, 33, 34 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π β (π¦ ++ β¨βπ§ββ©)) = ((π β π¦) ++ (π β β¨βπ§ββ©))) |
36 | | s1co 14723 |
. . . . . . . . . . . . 13
β’ ((π§ β πΌ β§ π:πΌβΆWord πΌ) β (π β β¨βπ§ββ©) = β¨β(πβπ§)ββ©) |
37 | 29, 33, 36 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π β β¨βπ§ββ©) = β¨β(πβπ§)ββ©) |
38 | 31 | vrmdval 18668 |
. . . . . . . . . . . . . 14
β’ ((πΌ β π β§ π§ β πΌ) β (πβπ§) = β¨βπ§ββ©) |
39 | 38 | adantrl 715 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (πβπ§) = β¨βπ§ββ©) |
40 | 39 | s1eqd 14490 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β β¨β(πβπ§)ββ© =
β¨ββ¨βπ§ββ©ββ©) |
41 | 37, 40 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π β β¨βπ§ββ©) =
β¨ββ¨βπ§ββ©ββ©) |
42 | 41 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β ((π β π¦) ++ (π β β¨βπ§ββ©)) = ((π β π¦) ++ β¨ββ¨βπ§ββ©ββ©)) |
43 | 35, 42 | eqtrd 2777 |
. . . . . . . . 9
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π β (π¦ ++ β¨βπ§ββ©)) = ((π β π¦) ++ β¨ββ¨βπ§ββ©ββ©)) |
44 | 43 | oveq2d 7374 |
. . . . . . . 8
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π Ξ£g (π β (π¦ ++ β¨βπ§ββ©))) = (π Ξ£g ((π β π¦) ++ β¨ββ¨βπ§ββ©ββ©))) |
45 | 23 | frmdmnd 18670 |
. . . . . . . . . . 11
β’ (πΌ β π β π β Mnd) |
46 | 45 | adantr 482 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β π β Mnd) |
47 | | wrdco 14721 |
. . . . . . . . . . . 12
β’ ((π¦ β Word πΌ β§ π:πΌβΆWord πΌ) β (π β π¦) β Word Word πΌ) |
48 | 28, 33, 47 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π β π¦) β Word Word πΌ) |
49 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(Baseβπ) =
(Baseβπ) |
50 | 23, 49 | frmdbas 18663 |
. . . . . . . . . . . . 13
β’ (πΌ β π β (Baseβπ) = Word πΌ) |
51 | 50 | adantr 482 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (Baseβπ) = Word πΌ) |
52 | | wrdeq 14425 |
. . . . . . . . . . . 12
β’
((Baseβπ) =
Word πΌ β Word
(Baseβπ) = Word Word
πΌ) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β Word (Baseβπ) = Word Word πΌ) |
54 | 48, 53 | eleqtrrd 2841 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π β π¦) β Word (Baseβπ)) |
55 | 30, 51 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β β¨βπ§ββ© β (Baseβπ)) |
56 | 55 | s1cld 14492 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β β¨ββ¨βπ§ββ©ββ©
β Word (Baseβπ)) |
57 | | eqid 2737 |
. . . . . . . . . . 11
β’
(+gβπ) = (+gβπ) |
58 | 49, 57 | gsumccat 18652 |
. . . . . . . . . 10
β’ ((π β Mnd β§ (π β π¦) β Word (Baseβπ) β§ β¨ββ¨βπ§ββ©ββ©
β Word (Baseβπ))
β (π
Ξ£g ((π β π¦) ++ β¨ββ¨βπ§ββ©ββ©)) =
((π
Ξ£g (π β π¦))(+gβπ)(π Ξ£g
β¨ββ¨βπ§ββ©ββ©))) |
59 | 46, 54, 56, 58 | syl3anc 1372 |
. . . . . . . . 9
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π Ξ£g ((π β π¦) ++ β¨ββ¨βπ§ββ©ββ©)) =
((π
Ξ£g (π β π¦))(+gβπ)(π Ξ£g
β¨ββ¨βπ§ββ©ββ©))) |
60 | 49 | gsumws1 18649 |
. . . . . . . . . . . 12
β’
(β¨βπ§ββ© β (Baseβπ) β (π Ξ£g
β¨ββ¨βπ§ββ©ββ©) =
β¨βπ§ββ©) |
61 | 55, 60 | syl 17 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π Ξ£g
β¨ββ¨βπ§ββ©ββ©) =
β¨βπ§ββ©) |
62 | 61 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β ((π Ξ£g (π β π¦))(+gβπ)(π Ξ£g
β¨ββ¨βπ§ββ©ββ©)) = ((π Ξ£g
(π β π¦))(+gβπ)β¨βπ§ββ©)) |
63 | 49 | gsumwcl 18650 |
. . . . . . . . . . . 12
β’ ((π β Mnd β§ (π β π¦) β Word (Baseβπ)) β (π Ξ£g (π β π¦)) β (Baseβπ)) |
64 | 46, 54, 63 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π Ξ£g (π β π¦)) β (Baseβπ)) |
65 | 23, 49, 57 | frmdadd 18666 |
. . . . . . . . . . 11
β’ (((π Ξ£g
(π β π¦)) β (Baseβπ) β§ β¨βπ§ββ© β
(Baseβπ)) β
((π
Ξ£g (π β π¦))(+gβπ)β¨βπ§ββ©) = ((π Ξ£g (π β π¦)) ++ β¨βπ§ββ©)) |
66 | 64, 55, 65 | syl2anc 585 |
. . . . . . . . . 10
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β ((π Ξ£g (π β π¦))(+gβπ)β¨βπ§ββ©) = ((π Ξ£g (π β π¦)) ++ β¨βπ§ββ©)) |
67 | 62, 66 | eqtrd 2777 |
. . . . . . . . 9
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β ((π Ξ£g (π β π¦))(+gβπ)(π Ξ£g
β¨ββ¨βπ§ββ©ββ©)) = ((π Ξ£g
(π β π¦)) ++ β¨βπ§ββ©)) |
68 | 59, 67 | eqtrd 2777 |
. . . . . . . 8
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π Ξ£g ((π β π¦) ++ β¨ββ¨βπ§ββ©ββ©)) =
((π
Ξ£g (π β π¦)) ++ β¨βπ§ββ©)) |
69 | 44, 68 | eqtrd 2777 |
. . . . . . 7
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β (π Ξ£g (π β (π¦ ++ β¨βπ§ββ©))) = ((π Ξ£g (π β π¦)) ++ β¨βπ§ββ©)) |
70 | 69 | eqeq1d 2739 |
. . . . . 6
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β ((π Ξ£g (π β (π¦ ++ β¨βπ§ββ©))) = (π¦ ++ β¨βπ§ββ©) β ((π Ξ£g (π β π¦)) ++ β¨βπ§ββ©) = (π¦ ++ β¨βπ§ββ©))) |
71 | 27, 70 | syl5ibr 246 |
. . . . 5
β’ ((πΌ β π β§ (π¦ β Word πΌ β§ π§ β πΌ)) β ((π Ξ£g (π β π¦)) = π¦ β (π Ξ£g (π β (π¦ ++ β¨βπ§ββ©))) = (π¦ ++ β¨βπ§ββ©))) |
72 | 71 | expcom 415 |
. . . 4
β’ ((π¦ β Word πΌ β§ π§ β πΌ) β (πΌ β π β ((π Ξ£g (π β π¦)) = π¦ β (π Ξ£g (π β (π¦ ++ β¨βπ§ββ©))) = (π¦ ++ β¨βπ§ββ©)))) |
73 | 72 | a2d 29 |
. . 3
β’ ((π¦ β Word πΌ β§ π§ β πΌ) β ((πΌ β π β (π Ξ£g (π β π¦)) = π¦) β (πΌ β π β (π Ξ£g (π β (π¦ ++ β¨βπ§ββ©))) = (π¦ ++ β¨βπ§ββ©)))) |
74 | 7, 12, 17, 22, 26, 73 | wrdind 14611 |
. 2
β’ (π β Word πΌ β (πΌ β π β (π Ξ£g (π β π)) = π)) |
75 | 74 | impcom 409 |
1
β’ ((πΌ β π β§ π β Word πΌ) β (π Ξ£g (π β π)) = π) |