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 28056 |
. . 3
β’ (π β πΉ:πβ1-1-ontoβπ) |
6 | | f1ocnv 6844 |
. . 3
β’ (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβ1-1-ontoβπ) |
7 | 5, 6 | syl 17 |
. 2
β’ (π β β‘πΉ:πβ1-1-ontoβπ) |
8 | 3 | adantr 479 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β πΊ β π) |
9 | | f1of 6832 |
. . . . . . . 8
β’ (β‘πΉ:πβ1-1-ontoβπ β β‘πΉ:πβΆπ) |
10 | 7, 9 | syl 17 |
. . . . . . 7
β’ (π β β‘πΉ:πβΆπ) |
11 | 10 | adantr 479 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β β‘πΉ:πβΆπ) |
12 | | simprl 767 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β π β π) |
13 | 11, 12 | ffvelcdmd 7086 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (β‘πΉβπ) β π) |
14 | | simprr 769 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β π β π) |
15 | 11, 14 | ffvelcdmd 7086 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (β‘πΉβπ) β π) |
16 | 4 | adantr 479 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β πΉ β (πΊIsmtπΊ)) |
17 | 1, 2, 8, 13, 15, 16 | motcgr 28054 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β ((πΉβ(β‘πΉβπ)) β (πΉβ(β‘πΉβπ))) = ((β‘πΉβπ) β (β‘πΉβπ))) |
18 | | f1ocnvfv2 7277 |
. . . . . 6
β’ ((πΉ:πβ1-1-ontoβπ β§ π β π) β (πΉβ(β‘πΉβπ)) = π) |
19 | 5, 12, 18 | syl2an2r 681 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (πΉβ(β‘πΉβπ)) = π) |
20 | | f1ocnvfv2 7277 |
. . . . . 6
β’ ((πΉ:πβ1-1-ontoβπ β§ π β π) β (πΉβ(β‘πΉβπ)) = π) |
21 | 5, 14, 20 | syl2an2r 681 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (πΉβ(β‘πΉβπ)) = π) |
22 | 19, 21 | oveq12d 7429 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β ((πΉβ(β‘πΉβπ)) β (πΉβ(β‘πΉβπ))) = (π β π)) |
23 | 17, 22 | eqtr3d 2772 |
. . 3
β’ ((π β§ (π β π β§ π β π)) β ((β‘πΉβπ) β (β‘πΉβπ)) = (π β π)) |
24 | 23 | ralrimivva 3198 |
. 2
β’ (π β βπ β π βπ β π ((β‘πΉβπ) β (β‘πΉβπ)) = (π β π)) |
25 | 1, 2 | ismot 28053 |
. . 3
β’ (πΊ β π β (β‘πΉ β (πΊIsmtπΊ) β (β‘πΉ:πβ1-1-ontoβπ β§ βπ β π βπ β π ((β‘πΉβπ) β (β‘πΉβπ)) = (π β π)))) |
26 | 3, 25 | syl 17 |
. 2
β’ (π β (β‘πΉ β (πΊIsmtπΊ) β (β‘πΉ:πβ1-1-ontoβπ β§ βπ β π βπ β π ((β‘πΉβπ) β (β‘πΉβπ)) = (π β π)))) |
27 | 7, 24, 26 | mpbir2and 709 |
1
β’ (π β β‘πΉ β (πΊIsmtπΊ)) |