Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
2 | | frmdup3.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
3 | 1, 2 | mhmf 18719 |
. . . . 5
β’ (πΉ β (π MndHom πΊ) β πΉ:(Baseβπ)βΆπ΅) |
4 | 3 | ad2antrl 725 |
. . . 4
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β πΉ:(Baseβπ)βΆπ΅) |
5 | | frmdup3.m |
. . . . . . . 8
β’ π = (freeMndβπΌ) |
6 | 5, 1 | frmdbas 18777 |
. . . . . . 7
β’ (πΌ β π β (Baseβπ) = Word πΌ) |
7 | 6 | 3ad2ant2 1131 |
. . . . . 6
β’ ((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β (Baseβπ) = Word πΌ) |
8 | 7 | adantr 480 |
. . . . 5
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β (Baseβπ) = Word πΌ) |
9 | 8 | feq2d 6697 |
. . . 4
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β (πΉ:(Baseβπ)βΆπ΅ β πΉ:Word πΌβΆπ΅)) |
10 | 4, 9 | mpbid 231 |
. . 3
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β πΉ:Word πΌβΆπ΅) |
11 | 10 | feqmptd 6954 |
. 2
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β πΉ = (π₯ β Word πΌ β¦ (πΉβπ₯))) |
12 | | simplrl 774 |
. . . . 5
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β πΉ β (π MndHom πΊ)) |
13 | | simpr 484 |
. . . . . 6
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β π₯ β Word πΌ) |
14 | | frmdup3.u |
. . . . . . . . . 10
β’ π =
(varFMndβπΌ) |
15 | 14 | vrmdf 18783 |
. . . . . . . . 9
β’ (πΌ β π β π:πΌβΆWord πΌ) |
16 | 15 | 3ad2ant2 1131 |
. . . . . . . 8
β’ ((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β π:πΌβΆWord πΌ) |
17 | 7 | feq3d 6698 |
. . . . . . . 8
β’ ((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β (π:πΌβΆ(Baseβπ) β π:πΌβΆWord πΌ)) |
18 | 16, 17 | mpbird 257 |
. . . . . . 7
β’ ((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β π:πΌβΆ(Baseβπ)) |
19 | 18 | ad2antrr 723 |
. . . . . 6
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β π:πΌβΆ(Baseβπ)) |
20 | | wrdco 14788 |
. . . . . 6
β’ ((π₯ β Word πΌ β§ π:πΌβΆ(Baseβπ)) β (π β π₯) β Word (Baseβπ)) |
21 | 13, 19, 20 | syl2anc 583 |
. . . . 5
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (π β π₯) β Word (Baseβπ)) |
22 | 1 | gsumwmhm 18770 |
. . . . 5
β’ ((πΉ β (π MndHom πΊ) β§ (π β π₯) β Word (Baseβπ)) β (πΉβ(π Ξ£g (π β π₯))) = (πΊ Ξ£g (πΉ β (π β π₯)))) |
23 | 12, 21, 22 | syl2anc 583 |
. . . 4
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΉβ(π Ξ£g (π β π₯))) = (πΊ Ξ£g (πΉ β (π β π₯)))) |
24 | | simpll2 1210 |
. . . . . 6
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β πΌ β π) |
25 | 5, 14 | frmdgsum 18787 |
. . . . . 6
β’ ((πΌ β π β§ π₯ β Word πΌ) β (π Ξ£g (π β π₯)) = π₯) |
26 | 24, 13, 25 | syl2anc 583 |
. . . . 5
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (π Ξ£g (π β π₯)) = π₯) |
27 | 26 | fveq2d 6889 |
. . . 4
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΉβ(π Ξ£g (π β π₯))) = (πΉβπ₯)) |
28 | | coass 6258 |
. . . . . 6
β’ ((πΉ β π) β π₯) = (πΉ β (π β π₯)) |
29 | | simplrr 775 |
. . . . . . 7
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΉ β π) = π΄) |
30 | 29 | coeq1d 5855 |
. . . . . 6
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β ((πΉ β π) β π₯) = (π΄ β π₯)) |
31 | 28, 30 | eqtr3id 2780 |
. . . . 5
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΉ β (π β π₯)) = (π΄ β π₯)) |
32 | 31 | oveq2d 7421 |
. . . 4
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΊ Ξ£g (πΉ β (π β π₯))) = (πΊ Ξ£g (π΄ β π₯))) |
33 | 23, 27, 32 | 3eqtr3d 2774 |
. . 3
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΉβπ₯) = (πΊ Ξ£g (π΄ β π₯))) |
34 | 33 | mpteq2dva 5241 |
. 2
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β (π₯ β Word πΌ β¦ (πΉβπ₯)) = (π₯ β Word πΌ β¦ (πΊ Ξ£g (π΄ β π₯)))) |
35 | 11, 34 | eqtrd 2766 |
1
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β πΉ = (π₯ β Word πΌ β¦ (πΊ Ξ£g (π΄ β π₯)))) |