Step | Hyp | Ref
| Expression |
1 | | frmdup.i |
. . 3
β’ (π β πΌ β π) |
2 | | frmdup.m |
. . . 4
β’ π = (freeMndβπΌ) |
3 | 2 | frmdmnd 18670 |
. . 3
β’ (πΌ β π β π β Mnd) |
4 | 1, 3 | syl 17 |
. 2
β’ (π β π β Mnd) |
5 | | frmdup.g |
. 2
β’ (π β πΊ β Mnd) |
6 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β Word πΌ) β πΊ β Mnd) |
7 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π₯ β Word πΌ) β π₯ β Word πΌ) |
8 | | frmdup.a |
. . . . . . . 8
β’ (π β π΄:πΌβΆπ΅) |
9 | 8 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β Word πΌ) β π΄:πΌβΆπ΅) |
10 | | wrdco 14721 |
. . . . . . 7
β’ ((π₯ β Word πΌ β§ π΄:πΌβΆπ΅) β (π΄ β π₯) β Word π΅) |
11 | 7, 9, 10 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π₯ β Word πΌ) β (π΄ β π₯) β Word π΅) |
12 | | frmdup.b |
. . . . . . 7
β’ π΅ = (BaseβπΊ) |
13 | 12 | gsumwcl 18650 |
. . . . . 6
β’ ((πΊ β Mnd β§ (π΄ β π₯) β Word π΅) β (πΊ Ξ£g (π΄ β π₯)) β π΅) |
14 | 6, 11, 13 | syl2anc 585 |
. . . . 5
β’ ((π β§ π₯ β Word πΌ) β (πΊ Ξ£g (π΄ β π₯)) β π΅) |
15 | | frmdup.e |
. . . . 5
β’ πΈ = (π₯ β Word πΌ β¦ (πΊ Ξ£g (π΄ β π₯))) |
16 | 14, 15 | fmptd 7063 |
. . . 4
β’ (π β πΈ:Word πΌβΆπ΅) |
17 | | eqid 2737 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
18 | 2, 17 | frmdbas 18663 |
. . . . . 6
β’ (πΌ β π β (Baseβπ) = Word πΌ) |
19 | 1, 18 | syl 17 |
. . . . 5
β’ (π β (Baseβπ) = Word πΌ) |
20 | 19 | feq2d 6655 |
. . . 4
β’ (π β (πΈ:(Baseβπ)βΆπ΅ β πΈ:Word πΌβΆπ΅)) |
21 | 16, 20 | mpbird 257 |
. . 3
β’ (π β πΈ:(Baseβπ)βΆπ΅) |
22 | 2, 17 | frmdelbas 18664 |
. . . . . . . . 9
β’ (π¦ β (Baseβπ) β π¦ β Word πΌ) |
23 | 22 | ad2antrl 727 |
. . . . . . . 8
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π¦ β Word πΌ) |
24 | 2, 17 | frmdelbas 18664 |
. . . . . . . . 9
β’ (π§ β (Baseβπ) β π§ β Word πΌ) |
25 | 24 | ad2antll 728 |
. . . . . . . 8
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π§ β Word πΌ) |
26 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β π΄:πΌβΆπ΅) |
27 | | ccatco 14725 |
. . . . . . . 8
β’ ((π¦ β Word πΌ β§ π§ β Word πΌ β§ π΄:πΌβΆπ΅) β (π΄ β (π¦ ++ π§)) = ((π΄ β π¦) ++ (π΄ β π§))) |
28 | 23, 25, 26, 27 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π΄ β (π¦ ++ π§)) = ((π΄ β π¦) ++ (π΄ β π§))) |
29 | 28 | oveq2d 7374 |
. . . . . 6
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (πΊ Ξ£g (π΄ β (π¦ ++ π§))) = (πΊ Ξ£g ((π΄ β π¦) ++ (π΄ β π§)))) |
30 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β πΊ β Mnd) |
31 | | wrdco 14721 |
. . . . . . . 8
β’ ((π¦ β Word πΌ β§ π΄:πΌβΆπ΅) β (π΄ β π¦) β Word π΅) |
32 | 23, 26, 31 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π΄ β π¦) β Word π΅) |
33 | | wrdco 14721 |
. . . . . . . 8
β’ ((π§ β Word πΌ β§ π΄:πΌβΆπ΅) β (π΄ β π§) β Word π΅) |
34 | 25, 26, 33 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π΄ β π§) β Word π΅) |
35 | | eqid 2737 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
36 | 12, 35 | gsumccat 18652 |
. . . . . . 7
β’ ((πΊ β Mnd β§ (π΄ β π¦) β Word π΅ β§ (π΄ β π§) β Word π΅) β (πΊ Ξ£g ((π΄ β π¦) ++ (π΄ β π§))) = ((πΊ Ξ£g (π΄ β π¦))(+gβπΊ)(πΊ Ξ£g (π΄ β π§)))) |
37 | 30, 32, 34, 36 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (πΊ Ξ£g ((π΄ β π¦) ++ (π΄ β π§))) = ((πΊ Ξ£g (π΄ β π¦))(+gβπΊ)(πΊ Ξ£g (π΄ β π§)))) |
38 | 29, 37 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (πΊ Ξ£g (π΄ β (π¦ ++ π§))) = ((πΊ Ξ£g (π΄ β π¦))(+gβπΊ)(πΊ Ξ£g (π΄ β π§)))) |
39 | | eqid 2737 |
. . . . . . . . 9
β’
(+gβπ) = (+gβπ) |
40 | 2, 17, 39 | frmdadd 18666 |
. . . . . . . 8
β’ ((π¦ β (Baseβπ) β§ π§ β (Baseβπ)) β (π¦(+gβπ)π§) = (π¦ ++ π§)) |
41 | 40 | adantl 483 |
. . . . . . 7
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π¦(+gβπ)π§) = (π¦ ++ π§)) |
42 | 41 | fveq2d 6847 |
. . . . . 6
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (πΈβ(π¦(+gβπ)π§)) = (πΈβ(π¦ ++ π§))) |
43 | | ccatcl 14463 |
. . . . . . . 8
β’ ((π¦ β Word πΌ β§ π§ β Word πΌ) β (π¦ ++ π§) β Word πΌ) |
44 | 23, 25, 43 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (π¦ ++ π§) β Word πΌ) |
45 | | coeq2 5815 |
. . . . . . . . 9
β’ (π₯ = (π¦ ++ π§) β (π΄ β π₯) = (π΄ β (π¦ ++ π§))) |
46 | 45 | oveq2d 7374 |
. . . . . . . 8
β’ (π₯ = (π¦ ++ π§) β (πΊ Ξ£g (π΄ β π₯)) = (πΊ Ξ£g (π΄ β (π¦ ++ π§)))) |
47 | | ovex 7391 |
. . . . . . . 8
β’ (πΊ Ξ£g
(π΄ β π₯)) β V |
48 | 46, 15, 47 | fvmpt3i 6954 |
. . . . . . 7
β’ ((π¦ ++ π§) β Word πΌ β (πΈβ(π¦ ++ π§)) = (πΊ Ξ£g (π΄ β (π¦ ++ π§)))) |
49 | 44, 48 | syl 17 |
. . . . . 6
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (πΈβ(π¦ ++ π§)) = (πΊ Ξ£g (π΄ β (π¦ ++ π§)))) |
50 | 42, 49 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (πΈβ(π¦(+gβπ)π§)) = (πΊ Ξ£g (π΄ β (π¦ ++ π§)))) |
51 | | coeq2 5815 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π΄ β π₯) = (π΄ β π¦)) |
52 | 51 | oveq2d 7374 |
. . . . . . . 8
β’ (π₯ = π¦ β (πΊ Ξ£g (π΄ β π₯)) = (πΊ Ξ£g (π΄ β π¦))) |
53 | 52, 15, 47 | fvmpt3i 6954 |
. . . . . . 7
β’ (π¦ β Word πΌ β (πΈβπ¦) = (πΊ Ξ£g (π΄ β π¦))) |
54 | | coeq2 5815 |
. . . . . . . . 9
β’ (π₯ = π§ β (π΄ β π₯) = (π΄ β π§)) |
55 | 54 | oveq2d 7374 |
. . . . . . . 8
β’ (π₯ = π§ β (πΊ Ξ£g (π΄ β π₯)) = (πΊ Ξ£g (π΄ β π§))) |
56 | 55, 15, 47 | fvmpt3i 6954 |
. . . . . . 7
β’ (π§ β Word πΌ β (πΈβπ§) = (πΊ Ξ£g (π΄ β π§))) |
57 | 53, 56 | oveqan12d 7377 |
. . . . . 6
β’ ((π¦ β Word πΌ β§ π§ β Word πΌ) β ((πΈβπ¦)(+gβπΊ)(πΈβπ§)) = ((πΊ Ξ£g (π΄ β π¦))(+gβπΊ)(πΊ Ξ£g (π΄ β π§)))) |
58 | 23, 25, 57 | syl2anc 585 |
. . . . 5
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β ((πΈβπ¦)(+gβπΊ)(πΈβπ§)) = ((πΊ Ξ£g (π΄ β π¦))(+gβπΊ)(πΊ Ξ£g (π΄ β π§)))) |
59 | 38, 50, 58 | 3eqtr4d 2787 |
. . . 4
β’ ((π β§ (π¦ β (Baseβπ) β§ π§ β (Baseβπ))) β (πΈβ(π¦(+gβπ)π§)) = ((πΈβπ¦)(+gβπΊ)(πΈβπ§))) |
60 | 59 | ralrimivva 3198 |
. . 3
β’ (π β βπ¦ β (Baseβπ)βπ§ β (Baseβπ)(πΈβ(π¦(+gβπ)π§)) = ((πΈβπ¦)(+gβπΊ)(πΈβπ§))) |
61 | | wrd0 14428 |
. . . 4
β’ β
β Word πΌ |
62 | | coeq2 5815 |
. . . . . . . 8
β’ (π₯ = β
β (π΄ β π₯) = (π΄ β β
)) |
63 | | co02 6213 |
. . . . . . . 8
β’ (π΄ β β
) =
β
|
64 | 62, 63 | eqtrdi 2793 |
. . . . . . 7
β’ (π₯ = β
β (π΄ β π₯) = β
) |
65 | 64 | oveq2d 7374 |
. . . . . 6
β’ (π₯ = β
β (πΊ Ξ£g
(π΄ β π₯)) = (πΊ Ξ£g
β
)) |
66 | | eqid 2737 |
. . . . . . 7
β’
(0gβπΊ) = (0gβπΊ) |
67 | 66 | gsum0 18540 |
. . . . . 6
β’ (πΊ Ξ£g
β
) = (0gβπΊ) |
68 | 65, 67 | eqtrdi 2793 |
. . . . 5
β’ (π₯ = β
β (πΊ Ξ£g
(π΄ β π₯)) = (0gβπΊ)) |
69 | 68, 15, 47 | fvmpt3i 6954 |
. . . 4
β’ (β
β Word πΌ β (πΈββ
) =
(0gβπΊ)) |
70 | 61, 69 | mp1i 13 |
. . 3
β’ (π β (πΈββ
) = (0gβπΊ)) |
71 | 21, 60, 70 | 3jca 1129 |
. 2
β’ (π β (πΈ:(Baseβπ)βΆπ΅ β§ βπ¦ β (Baseβπ)βπ§ β (Baseβπ)(πΈβ(π¦(+gβπ)π§)) = ((πΈβπ¦)(+gβπΊ)(πΈβπ§)) β§ (πΈββ
) = (0gβπΊ))) |
72 | 2 | frmd0 18671 |
. . 3
β’ β
=
(0gβπ) |
73 | 17, 12, 39, 35, 72, 66 | ismhm 18604 |
. 2
β’ (πΈ β (π MndHom πΊ) β ((π β Mnd β§ πΊ β Mnd) β§ (πΈ:(Baseβπ)βΆπ΅ β§ βπ¦ β (Baseβπ)βπ§ β (Baseβπ)(πΈβ(π¦(+gβπ)π§)) = ((πΈβπ¦)(+gβπΊ)(πΈβπ§)) β§ (πΈββ
) = (0gβπΊ)))) |
74 | 4, 5, 71, 73 | syl21anbrc 1345 |
1
β’ (π β πΈ β (π MndHom πΊ)) |