Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
2 | | frmdup3.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
3 | 1, 2 | mhmf 18608 |
. . . . 5
β’ (πΉ β (π MndHom πΊ) β πΉ:(Baseβπ)βΆπ΅) |
4 | 3 | ad2antrl 727 |
. . . 4
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β πΉ:(Baseβπ)βΆπ΅) |
5 | | frmdup3.m |
. . . . . . . 8
β’ π = (freeMndβπΌ) |
6 | 5, 1 | frmdbas 18663 |
. . . . . . 7
β’ (πΌ β π β (Baseβπ) = Word πΌ) |
7 | 6 | 3ad2ant2 1135 |
. . . . . 6
β’ ((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β (Baseβπ) = Word πΌ) |
8 | 7 | adantr 482 |
. . . . 5
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β (Baseβπ) = Word πΌ) |
9 | 8 | feq2d 6655 |
. . . 4
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β (πΉ:(Baseβπ)βΆπ΅ β πΉ:Word πΌβΆπ΅)) |
10 | 4, 9 | mpbid 231 |
. . 3
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β πΉ:Word πΌβΆπ΅) |
11 | 10 | feqmptd 6911 |
. 2
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β πΉ = (π₯ β Word πΌ β¦ (πΉβπ₯))) |
12 | | simplrl 776 |
. . . . 5
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β πΉ β (π MndHom πΊ)) |
13 | | simpr 486 |
. . . . . 6
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β π₯ β Word πΌ) |
14 | | frmdup3.u |
. . . . . . . . . 10
β’ π =
(varFMndβπΌ) |
15 | 14 | vrmdf 18669 |
. . . . . . . . 9
β’ (πΌ β π β π:πΌβΆWord πΌ) |
16 | 15 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β π:πΌβΆWord πΌ) |
17 | 7 | feq3d 6656 |
. . . . . . . 8
β’ ((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β (π:πΌβΆ(Baseβπ) β π:πΌβΆWord πΌ)) |
18 | 16, 17 | mpbird 257 |
. . . . . . 7
β’ ((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β π:πΌβΆ(Baseβπ)) |
19 | 18 | ad2antrr 725 |
. . . . . 6
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β π:πΌβΆ(Baseβπ)) |
20 | | wrdco 14721 |
. . . . . 6
β’ ((π₯ β Word πΌ β§ π:πΌβΆ(Baseβπ)) β (π β π₯) β Word (Baseβπ)) |
21 | 13, 19, 20 | syl2anc 585 |
. . . . 5
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (π β π₯) β Word (Baseβπ)) |
22 | 1 | gsumwmhm 18656 |
. . . . 5
β’ ((πΉ β (π MndHom πΊ) β§ (π β π₯) β Word (Baseβπ)) β (πΉβ(π Ξ£g (π β π₯))) = (πΊ Ξ£g (πΉ β (π β π₯)))) |
23 | 12, 21, 22 | syl2anc 585 |
. . . 4
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΉβ(π Ξ£g (π β π₯))) = (πΊ Ξ£g (πΉ β (π β π₯)))) |
24 | | simpll2 1214 |
. . . . . 6
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β πΌ β π) |
25 | 5, 14 | frmdgsum 18673 |
. . . . . 6
β’ ((πΌ β π β§ π₯ β Word πΌ) β (π Ξ£g (π β π₯)) = π₯) |
26 | 24, 13, 25 | syl2anc 585 |
. . . . 5
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (π Ξ£g (π β π₯)) = π₯) |
27 | 26 | fveq2d 6847 |
. . . 4
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΉβ(π Ξ£g (π β π₯))) = (πΉβπ₯)) |
28 | | coass 6218 |
. . . . . 6
β’ ((πΉ β π) β π₯) = (πΉ β (π β π₯)) |
29 | | simplrr 777 |
. . . . . . 7
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΉ β π) = π΄) |
30 | 29 | coeq1d 5818 |
. . . . . 6
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β ((πΉ β π) β π₯) = (π΄ β π₯)) |
31 | 28, 30 | eqtr3id 2791 |
. . . . 5
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΉ β (π β π₯)) = (π΄ β π₯)) |
32 | 31 | oveq2d 7374 |
. . . 4
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΊ Ξ£g (πΉ β (π β π₯))) = (πΊ Ξ£g (π΄ β π₯))) |
33 | 23, 27, 32 | 3eqtr3d 2785 |
. . 3
β’ ((((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β§ π₯ β Word πΌ) β (πΉβπ₯) = (πΊ Ξ£g (π΄ β π₯))) |
34 | 33 | mpteq2dva 5206 |
. 2
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β (π₯ β Word πΌ β¦ (πΉβπ₯)) = (π₯ β Word πΌ β¦ (πΊ Ξ£g (π΄ β π₯)))) |
35 | 11, 34 | eqtrd 2777 |
1
β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β πΉ = (π₯ β Word πΌ β¦ (πΊ Ξ£g (π΄ β π₯)))) |