Step | Hyp | Ref
| Expression |
1 | | ismot.p |
. . . 4
β’ π = (BaseβπΊ) |
2 | | ismot.m |
. . . 4
β’ β =
(distβπΊ) |
3 | | motgrp.1 |
. . . 4
β’ (π β πΊ β π) |
4 | | motco.2 |
. . . 4
β’ (π β πΉ β (πΊIsmtπΊ)) |
5 | 1, 2, 3, 4 | motf1o 28044 |
. . 3
β’ (π β πΉ:πβ1-1-ontoβπ) |
6 | | motco.3 |
. . . 4
β’ (π β π» β (πΊIsmtπΊ)) |
7 | 1, 2, 3, 6 | motf1o 28044 |
. . 3
β’ (π β π»:πβ1-1-ontoβπ) |
8 | | f1oco 6856 |
. . 3
β’ ((πΉ:πβ1-1-ontoβπ β§ π»:πβ1-1-ontoβπ) β (πΉ β π»):πβ1-1-ontoβπ) |
9 | 5, 7, 8 | syl2anc 584 |
. 2
β’ (π β (πΉ β π»):πβ1-1-ontoβπ) |
10 | | f1of 6833 |
. . . . . . . 8
β’ (π»:πβ1-1-ontoβπ β π»:πβΆπ) |
11 | 7, 10 | syl 17 |
. . . . . . 7
β’ (π β π»:πβΆπ) |
12 | 11 | adantr 481 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β π»:πβΆπ) |
13 | | simprl 769 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β π β π) |
14 | | fvco3 6990 |
. . . . . 6
β’ ((π»:πβΆπ β§ π β π) β ((πΉ β π»)βπ) = (πΉβ(π»βπ))) |
15 | 12, 13, 14 | syl2anc 584 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β ((πΉ β π»)βπ) = (πΉβ(π»βπ))) |
16 | | simprr 771 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β π β π) |
17 | | fvco3 6990 |
. . . . . 6
β’ ((π»:πβΆπ β§ π β π) β ((πΉ β π»)βπ) = (πΉβ(π»βπ))) |
18 | 12, 16, 17 | syl2anc 584 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β ((πΉ β π»)βπ) = (πΉβ(π»βπ))) |
19 | 15, 18 | oveq12d 7429 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β (((πΉ β π»)βπ) β ((πΉ β π»)βπ)) = ((πΉβ(π»βπ)) β (πΉβ(π»βπ)))) |
20 | 3 | adantr 481 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β πΊ β π) |
21 | 12, 13 | ffvelcdmd 7087 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (π»βπ) β π) |
22 | 12, 16 | ffvelcdmd 7087 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (π»βπ) β π) |
23 | 4 | adantr 481 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β πΉ β (πΊIsmtπΊ)) |
24 | 1, 2, 20, 21, 22, 23 | motcgr 28042 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β ((πΉβ(π»βπ)) β (πΉβ(π»βπ))) = ((π»βπ) β (π»βπ))) |
25 | 6 | adantr 481 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β π» β (πΊIsmtπΊ)) |
26 | 1, 2, 20, 13, 16, 25 | motcgr 28042 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β ((π»βπ) β (π»βπ)) = (π β π)) |
27 | 19, 24, 26 | 3eqtrd 2776 |
. . 3
β’ ((π β§ (π β π β§ π β π)) β (((πΉ β π»)βπ) β ((πΉ β π»)βπ)) = (π β π)) |
28 | 27 | ralrimivva 3200 |
. 2
β’ (π β βπ β π βπ β π (((πΉ β π»)βπ) β ((πΉ β π»)βπ)) = (π β π)) |
29 | 1, 2 | ismot 28041 |
. . 3
β’ (πΊ β π β ((πΉ β π») β (πΊIsmtπΊ) β ((πΉ β π»):πβ1-1-ontoβπ β§ βπ β π βπ β π (((πΉ β π»)βπ) β ((πΉ β π»)βπ)) = (π β π)))) |
30 | 3, 29 | syl 17 |
. 2
β’ (π β ((πΉ β π») β (πΊIsmtπΊ) β ((πΉ β π»):πβ1-1-ontoβπ β§ βπ β π βπ β π (((πΉ β π»)βπ) β ((πΉ β π»)βπ)) = (π β π)))) |
31 | 9, 28, 30 | mpbir2and 711 |
1
β’ (π β (πΉ β π») β (πΊIsmtπΊ)) |