Step | Hyp | Ref
| Expression |
1 | | elex 3462 |
. . . 4
β’ (πΊ β π β πΊ β V) |
2 | | elex 3462 |
. . . 4
β’ (π» β π β π» β V) |
3 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΊ β (Baseβπ) = (BaseβπΊ)) |
4 | | isismt.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΊ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = πΊ β (Baseβπ) = π΅) |
6 | 5 | f1oeq2d 6781 |
. . . . . . 7
β’ (π = πΊ β (π:(Baseβπ)β1-1-ontoβ(Baseββ) β π:π΅β1-1-ontoβ(Baseββ))) |
7 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = πΊ β (distβπ) = (distβπΊ)) |
8 | | isismt.d |
. . . . . . . . . . . 12
β’ π· = (distβπΊ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π = πΊ β (distβπ) = π·) |
10 | 9 | oveqd 7375 |
. . . . . . . . . 10
β’ (π = πΊ β (π(distβπ)π) = (ππ·π)) |
11 | 10 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = πΊ β (((πβπ)(distββ)(πβπ)) = (π(distβπ)π) β ((πβπ)(distββ)(πβπ)) = (ππ·π))) |
12 | 5, 11 | raleqbidv 3318 |
. . . . . . . 8
β’ (π = πΊ β (βπ β (Baseβπ)((πβπ)(distββ)(πβπ)) = (π(distβπ)π) β βπ β π΅ ((πβπ)(distββ)(πβπ)) = (ππ·π))) |
13 | 5, 12 | raleqbidv 3318 |
. . . . . . 7
β’ (π = πΊ β (βπ β (Baseβπ)βπ β (Baseβπ)((πβπ)(distββ)(πβπ)) = (π(distβπ)π) β βπ β π΅ βπ β π΅ ((πβπ)(distββ)(πβπ)) = (ππ·π))) |
14 | 6, 13 | anbi12d 632 |
. . . . . 6
β’ (π = πΊ β ((π:(Baseβπ)β1-1-ontoβ(Baseββ) β§ βπ β (Baseβπ)βπ β (Baseβπ)((πβπ)(distββ)(πβπ)) = (π(distβπ)π)) β (π:π΅β1-1-ontoβ(Baseββ) β§ βπ β π΅ βπ β π΅ ((πβπ)(distββ)(πβπ)) = (ππ·π)))) |
15 | 14 | abbidv 2802 |
. . . . 5
β’ (π = πΊ β {π β£ (π:(Baseβπ)β1-1-ontoβ(Baseββ) β§ βπ β (Baseβπ)βπ β (Baseβπ)((πβπ)(distββ)(πβπ)) = (π(distβπ)π))} = {π β£ (π:π΅β1-1-ontoβ(Baseββ) β§ βπ β π΅ βπ β π΅ ((πβπ)(distββ)(πβπ)) = (ππ·π))}) |
16 | | fveq2 6843 |
. . . . . . . . 9
β’ (β = π» β (Baseββ) = (Baseβπ»)) |
17 | | isismt.p |
. . . . . . . . 9
β’ π = (Baseβπ») |
18 | 16, 17 | eqtr4di 2791 |
. . . . . . . 8
β’ (β = π» β (Baseββ) = π) |
19 | 18 | f1oeq3d 6782 |
. . . . . . 7
β’ (β = π» β (π:π΅β1-1-ontoβ(Baseββ) β π:π΅β1-1-ontoβπ)) |
20 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (β = π» β (distββ) = (distβπ»)) |
21 | | isismt.m |
. . . . . . . . . . 11
β’ β =
(distβπ») |
22 | 20, 21 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (β = π» β (distββ) = β ) |
23 | 22 | oveqd 7375 |
. . . . . . . . 9
β’ (β = π» β ((πβπ)(distββ)(πβπ)) = ((πβπ) β (πβπ))) |
24 | 23 | eqeq1d 2735 |
. . . . . . . 8
β’ (β = π» β (((πβπ)(distββ)(πβπ)) = (ππ·π) β ((πβπ) β (πβπ)) = (ππ·π))) |
25 | 24 | 2ralbidv 3209 |
. . . . . . 7
β’ (β = π» β (βπ β π΅ βπ β π΅ ((πβπ)(distββ)(πβπ)) = (ππ·π) β βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π))) |
26 | 19, 25 | anbi12d 632 |
. . . . . 6
β’ (β = π» β ((π:π΅β1-1-ontoβ(Baseββ) β§ βπ β π΅ βπ β π΅ ((πβπ)(distββ)(πβπ)) = (ππ·π)) β (π:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π)))) |
27 | 26 | abbidv 2802 |
. . . . 5
β’ (β = π» β {π β£ (π:π΅β1-1-ontoβ(Baseββ) β§ βπ β π΅ βπ β π΅ ((πβπ)(distββ)(πβπ)) = (ππ·π))} = {π β£ (π:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π))}) |
28 | | df-ismt 27517 |
. . . . 5
β’ Ismt =
(π β V, β β V β¦ {π β£ (π:(Baseβπ)β1-1-ontoβ(Baseββ) β§ βπ β (Baseβπ)βπ β (Baseβπ)((πβπ)(distββ)(πβπ)) = (π(distβπ)π))}) |
29 | | ovex 7391 |
. . . . . 6
β’ (π βm π΅) β V |
30 | | f1of 6785 |
. . . . . . . . 9
β’ (π:π΅β1-1-ontoβπ β π:π΅βΆπ) |
31 | 17 | fvexi 6857 |
. . . . . . . . . 10
β’ π β V |
32 | 4 | fvexi 6857 |
. . . . . . . . . 10
β’ π΅ β V |
33 | 31, 32 | elmap 8812 |
. . . . . . . . 9
β’ (π β (π βm π΅) β π:π΅βΆπ) |
34 | 30, 33 | sylibr 233 |
. . . . . . . 8
β’ (π:π΅β1-1-ontoβπ β π β (π βm π΅)) |
35 | 34 | adantr 482 |
. . . . . . 7
β’ ((π:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π)) β π β (π βm π΅)) |
36 | 35 | abssi 4028 |
. . . . . 6
β’ {π β£ (π:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π))} β (π βm π΅) |
37 | 29, 36 | ssexi 5280 |
. . . . 5
β’ {π β£ (π:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π))} β V |
38 | 15, 27, 28, 37 | ovmpo 7516 |
. . . 4
β’ ((πΊ β V β§ π» β V) β (πΊIsmtπ») = {π β£ (π:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π))}) |
39 | 1, 2, 38 | syl2an 597 |
. . 3
β’ ((πΊ β π β§ π» β π) β (πΊIsmtπ») = {π β£ (π:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π))}) |
40 | 39 | eleq2d 2820 |
. 2
β’ ((πΊ β π β§ π» β π) β (πΉ β (πΊIsmtπ») β πΉ β {π β£ (π:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π))})) |
41 | | f1of 6785 |
. . . . 5
β’ (πΉ:π΅β1-1-ontoβπ β πΉ:π΅βΆπ) |
42 | | fex 7177 |
. . . . 5
β’ ((πΉ:π΅βΆπ β§ π΅ β V) β πΉ β V) |
43 | 41, 32, 42 | sylancl 587 |
. . . 4
β’ (πΉ:π΅β1-1-ontoβπ β πΉ β V) |
44 | 43 | adantr 482 |
. . 3
β’ ((πΉ:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πΉβπ) β (πΉβπ)) = (ππ·π)) β πΉ β V) |
45 | | f1oeq1 6773 |
. . . 4
β’ (π = πΉ β (π:π΅β1-1-ontoβπ β πΉ:π΅β1-1-ontoβπ)) |
46 | | fveq1 6842 |
. . . . . . 7
β’ (π = πΉ β (πβπ) = (πΉβπ)) |
47 | | fveq1 6842 |
. . . . . . 7
β’ (π = πΉ β (πβπ) = (πΉβπ)) |
48 | 46, 47 | oveq12d 7376 |
. . . . . 6
β’ (π = πΉ β ((πβπ) β (πβπ)) = ((πΉβπ) β (πΉβπ))) |
49 | 48 | eqeq1d 2735 |
. . . . 5
β’ (π = πΉ β (((πβπ) β (πβπ)) = (ππ·π) β ((πΉβπ) β (πΉβπ)) = (ππ·π))) |
50 | 49 | 2ralbidv 3209 |
. . . 4
β’ (π = πΉ β (βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π) β βπ β π΅ βπ β π΅ ((πΉβπ) β (πΉβπ)) = (ππ·π))) |
51 | 45, 50 | anbi12d 632 |
. . 3
β’ (π = πΉ β ((π:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π)) β (πΉ:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πΉβπ) β (πΉβπ)) = (ππ·π)))) |
52 | 44, 51 | elab3 3639 |
. 2
β’ (πΉ β {π β£ (π:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πβπ) β (πβπ)) = (ππ·π))} β (πΉ:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πΉβπ) β (πΉβπ)) = (ππ·π))) |
53 | 40, 52 | bitrdi 287 |
1
β’ ((πΊ β π β§ π» β π) β (πΉ β (πΊIsmtπ») β (πΉ:π΅β1-1-ontoβπ β§ βπ β π΅ βπ β π΅ ((πΉβπ) β (πΉβπ)) = (ππ·π)))) |