Step | Hyp | Ref
| Expression |
1 | | imasf1oxmet.u |
. . . 4
β’ (π β π = (πΉ βs π
)) |
2 | | imasf1oxmet.v |
. . . 4
β’ (π β π = (Baseβπ
)) |
3 | | imasf1oxmet.f |
. . . . 5
β’ (π β πΉ:πβ1-1-ontoβπ΅) |
4 | | f1ofo 6840 |
. . . . 5
β’ (πΉ:πβ1-1-ontoβπ΅ β πΉ:πβontoβπ΅) |
5 | 3, 4 | syl 17 |
. . . 4
β’ (π β πΉ:πβontoβπ΅) |
6 | | imasf1oxmet.r |
. . . 4
β’ (π β π
β π) |
7 | | eqid 2732 |
. . . 4
β’
(distβπ
) =
(distβπ
) |
8 | | imasf1oxmet.d |
. . . 4
β’ π· = (distβπ) |
9 | 1, 2, 5, 6, 7, 8 | imasdsfn 17462 |
. . 3
β’ (π β π· Fn (π΅ Γ π΅)) |
10 | 1 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β π = (πΉ βs π
)) |
11 | 2 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β π = (Baseβπ
)) |
12 | 3 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β πΉ:πβ1-1-ontoβπ΅) |
13 | 6 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β π
β π) |
14 | | imasf1oxmet.e |
. . . . . . . 8
β’ πΈ = ((distβπ
) βΎ (π Γ π)) |
15 | | imasf1oxmet.m |
. . . . . . . . 9
β’ (π β πΈ β (βMetβπ)) |
16 | 15 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β πΈ β (βMetβπ)) |
17 | | simprl 769 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β π β π) |
18 | | simprr 771 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β π β π) |
19 | 10, 11, 12, 13, 14, 8, 16, 17, 18 | imasdsf1o 23887 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β ((πΉβπ)π·(πΉβπ)) = (ππΈπ)) |
20 | | xmetcl 23844 |
. . . . . . . . 9
β’ ((πΈ β (βMetβπ) β§ π β π β§ π β π) β (ππΈπ) β
β*) |
21 | 20 | 3expb 1120 |
. . . . . . . 8
β’ ((πΈ β (βMetβπ) β§ (π β π β§ π β π)) β (ππΈπ) β
β*) |
22 | 15, 21 | sylan 580 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β (ππΈπ) β
β*) |
23 | 19, 22 | eqeltrd 2833 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β ((πΉβπ)π·(πΉβπ)) β
β*) |
24 | 23 | ralrimivva 3200 |
. . . . 5
β’ (π β βπ β π βπ β π ((πΉβπ)π·(πΉβπ)) β
β*) |
25 | | f1ofn 6834 |
. . . . . . . . 9
β’ (πΉ:πβ1-1-ontoβπ΅ β πΉ Fn π) |
26 | 3, 25 | syl 17 |
. . . . . . . 8
β’ (π β πΉ Fn π) |
27 | | oveq2 7419 |
. . . . . . . . . 10
β’ (π¦ = (πΉβπ) β ((πΉβπ)π·π¦) = ((πΉβπ)π·(πΉβπ))) |
28 | 27 | eleq1d 2818 |
. . . . . . . . 9
β’ (π¦ = (πΉβπ) β (((πΉβπ)π·π¦) β β* β ((πΉβπ)π·(πΉβπ)) β
β*)) |
29 | 28 | ralrn 7089 |
. . . . . . . 8
β’ (πΉ Fn π β (βπ¦ β ran πΉ((πΉβπ)π·π¦) β β* β
βπ β π ((πΉβπ)π·(πΉβπ)) β
β*)) |
30 | 26, 29 | syl 17 |
. . . . . . 7
β’ (π β (βπ¦ β ran πΉ((πΉβπ)π·π¦) β β* β
βπ β π ((πΉβπ)π·(πΉβπ)) β
β*)) |
31 | | forn 6808 |
. . . . . . . . 9
β’ (πΉ:πβontoβπ΅ β ran πΉ = π΅) |
32 | 5, 31 | syl 17 |
. . . . . . . 8
β’ (π β ran πΉ = π΅) |
33 | 32 | raleqdv 3325 |
. . . . . . 7
β’ (π β (βπ¦ β ran πΉ((πΉβπ)π·π¦) β β* β
βπ¦ β π΅ ((πΉβπ)π·π¦) β
β*)) |
34 | 30, 33 | bitr3d 280 |
. . . . . 6
β’ (π β (βπ β π ((πΉβπ)π·(πΉβπ)) β β* β
βπ¦ β π΅ ((πΉβπ)π·π¦) β
β*)) |
35 | 34 | ralbidv 3177 |
. . . . 5
β’ (π β (βπ β π βπ β π ((πΉβπ)π·(πΉβπ)) β β* β
βπ β π βπ¦ β π΅ ((πΉβπ)π·π¦) β
β*)) |
36 | 24, 35 | mpbid 231 |
. . . 4
β’ (π β βπ β π βπ¦ β π΅ ((πΉβπ)π·π¦) β
β*) |
37 | | oveq1 7418 |
. . . . . . . . 9
β’ (π₯ = (πΉβπ) β (π₯π·π¦) = ((πΉβπ)π·π¦)) |
38 | 37 | eleq1d 2818 |
. . . . . . . 8
β’ (π₯ = (πΉβπ) β ((π₯π·π¦) β β* β ((πΉβπ)π·π¦) β
β*)) |
39 | 38 | ralbidv 3177 |
. . . . . . 7
β’ (π₯ = (πΉβπ) β (βπ¦ β π΅ (π₯π·π¦) β β* β
βπ¦ β π΅ ((πΉβπ)π·π¦) β
β*)) |
40 | 39 | ralrn 7089 |
. . . . . 6
β’ (πΉ Fn π β (βπ₯ β ran πΉβπ¦ β π΅ (π₯π·π¦) β β* β
βπ β π βπ¦ β π΅ ((πΉβπ)π·π¦) β
β*)) |
41 | 26, 40 | syl 17 |
. . . . 5
β’ (π β (βπ₯ β ran πΉβπ¦ β π΅ (π₯π·π¦) β β* β
βπ β π βπ¦ β π΅ ((πΉβπ)π·π¦) β
β*)) |
42 | 32 | raleqdv 3325 |
. . . . 5
β’ (π β (βπ₯ β ran πΉβπ¦ β π΅ (π₯π·π¦) β β* β
βπ₯ β π΅ βπ¦ β π΅ (π₯π·π¦) β
β*)) |
43 | 41, 42 | bitr3d 280 |
. . . 4
β’ (π β (βπ β π βπ¦ β π΅ ((πΉβπ)π·π¦) β β* β
βπ₯ β π΅ βπ¦ β π΅ (π₯π·π¦) β
β*)) |
44 | 36, 43 | mpbid 231 |
. . 3
β’ (π β βπ₯ β π΅ βπ¦ β π΅ (π₯π·π¦) β
β*) |
45 | | ffnov 7537 |
. . 3
β’ (π·:(π΅ Γ π΅)βΆβ* β (π· Fn (π΅ Γ π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯π·π¦) β
β*)) |
46 | 9, 44, 45 | sylanbrc 583 |
. 2
β’ (π β π·:(π΅ Γ π΅)βΆβ*) |
47 | | xmeteq0 23851 |
. . . . . . . 8
β’ ((πΈ β (βMetβπ) β§ π β π β§ π β π) β ((ππΈπ) = 0 β π = π)) |
48 | 16, 17, 18, 47 | syl3anc 1371 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β ((ππΈπ) = 0 β π = π)) |
49 | 19 | eqeq1d 2734 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β (((πΉβπ)π·(πΉβπ)) = 0 β (ππΈπ) = 0)) |
50 | | f1of1 6832 |
. . . . . . . . 9
β’ (πΉ:πβ1-1-ontoβπ΅ β πΉ:πβ1-1βπ΅) |
51 | 3, 50 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:πβ1-1βπ΅) |
52 | | f1fveq 7263 |
. . . . . . . 8
β’ ((πΉ:πβ1-1βπ΅ β§ (π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β π = π)) |
53 | 51, 52 | sylan 580 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β π = π)) |
54 | 48, 49, 53 | 3bitr4d 310 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β (((πΉβπ)π·(πΉβπ)) = 0 β (πΉβπ) = (πΉβπ))) |
55 | 16 | adantr 481 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β πΈ β (βMetβπ)) |
56 | | simpr 485 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β π β π) |
57 | 17 | adantr 481 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β π β π) |
58 | 18 | adantr 481 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β π β π) |
59 | | xmettri2 23853 |
. . . . . . . . . 10
β’ ((πΈ β (βMetβπ) β§ (π β π β§ π β π β§ π β π)) β (ππΈπ) β€ ((ππΈπ) +π (ππΈπ))) |
60 | 55, 56, 57, 58, 59 | syl13anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β (ππΈπ) β€ ((ππΈπ) +π (ππΈπ))) |
61 | 19 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β ((πΉβπ)π·(πΉβπ)) = (ππΈπ)) |
62 | 10 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β π = (πΉ βs π
)) |
63 | 11 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β π = (Baseβπ
)) |
64 | 12 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β πΉ:πβ1-1-ontoβπ΅) |
65 | 13 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β π
β π) |
66 | 62, 63, 64, 65, 14, 8, 55, 56, 57 | imasdsf1o 23887 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β ((πΉβπ)π·(πΉβπ)) = (ππΈπ)) |
67 | 62, 63, 64, 65, 14, 8, 55, 56, 58 | imasdsf1o 23887 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β ((πΉβπ)π·(πΉβπ)) = (ππΈπ)) |
68 | 66, 67 | oveq12d 7429 |
. . . . . . . . 9
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) = ((ππΈπ) +π (ππΈπ))) |
69 | 60, 61, 68 | 3brtr4d 5180 |
. . . . . . . 8
β’ (((π β§ (π β π β§ π β π)) β§ π β π) β ((πΉβπ)π·(πΉβπ)) β€ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ)))) |
70 | 69 | ralrimiva 3146 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β βπ β π ((πΉβπ)π·(πΉβπ)) β€ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ)))) |
71 | | oveq1 7418 |
. . . . . . . . . . . . 13
β’ (π§ = (πΉβπ) β (π§π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
72 | | oveq1 7418 |
. . . . . . . . . . . . 13
β’ (π§ = (πΉβπ) β (π§π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
73 | 71, 72 | oveq12d 7429 |
. . . . . . . . . . . 12
β’ (π§ = (πΉβπ) β ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))) = (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ)))) |
74 | 73 | breq2d 5160 |
. . . . . . . . . . 11
β’ (π§ = (πΉβπ) β (((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))) β ((πΉβπ)π·(πΉβπ)) β€ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))))) |
75 | 74 | ralrn 7089 |
. . . . . . . . . 10
β’ (πΉ Fn π β (βπ§ β ran πΉ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))) β βπ β π ((πΉβπ)π·(πΉβπ)) β€ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))))) |
76 | 26, 75 | syl 17 |
. . . . . . . . 9
β’ (π β (βπ§ β ran πΉ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))) β βπ β π ((πΉβπ)π·(πΉβπ)) β€ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))))) |
77 | 32 | raleqdv 3325 |
. . . . . . . . 9
β’ (π β (βπ§ β ran πΉ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))) β βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))))) |
78 | 76, 77 | bitr3d 280 |
. . . . . . . 8
β’ (π β (βπ β π ((πΉβπ)π·(πΉβπ)) β€ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) β βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))))) |
79 | 78 | adantr 481 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π)) β (βπ β π ((πΉβπ)π·(πΉβπ)) β€ (((πΉβπ)π·(πΉβπ)) +π ((πΉβπ)π·(πΉβπ))) β βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))))) |
80 | 70, 79 | mpbid 231 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ)))) |
81 | 54, 80 | jca 512 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β ((((πΉβπ)π·(πΉβπ)) = 0 β (πΉβπ) = (πΉβπ)) β§ βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))))) |
82 | 81 | ralrimivva 3200 |
. . . 4
β’ (π β βπ β π βπ β π ((((πΉβπ)π·(πΉβπ)) = 0 β (πΉβπ) = (πΉβπ)) β§ βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))))) |
83 | 27 | eqeq1d 2734 |
. . . . . . . . . 10
β’ (π¦ = (πΉβπ) β (((πΉβπ)π·π¦) = 0 β ((πΉβπ)π·(πΉβπ)) = 0)) |
84 | | eqeq2 2744 |
. . . . . . . . . 10
β’ (π¦ = (πΉβπ) β ((πΉβπ) = π¦ β (πΉβπ) = (πΉβπ))) |
85 | 83, 84 | bibi12d 345 |
. . . . . . . . 9
β’ (π¦ = (πΉβπ) β ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β (((πΉβπ)π·(πΉβπ)) = 0 β (πΉβπ) = (πΉβπ)))) |
86 | | oveq2 7419 |
. . . . . . . . . . . 12
β’ (π¦ = (πΉβπ) β (π§π·π¦) = (π§π·(πΉβπ))) |
87 | 86 | oveq2d 7427 |
. . . . . . . . . . 11
β’ (π¦ = (πΉβπ) β ((π§π·(πΉβπ)) +π (π§π·π¦)) = ((π§π·(πΉβπ)) +π (π§π·(πΉβπ)))) |
88 | 27, 87 | breq12d 5161 |
. . . . . . . . . 10
β’ (π¦ = (πΉβπ) β (((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦)) β ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))))) |
89 | 88 | ralbidv 3177 |
. . . . . . . . 9
β’ (π¦ = (πΉβπ) β (βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦)) β βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ))))) |
90 | 85, 89 | anbi12d 631 |
. . . . . . . 8
β’ (π¦ = (πΉβπ) β (((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))) β ((((πΉβπ)π·(πΉβπ)) = 0 β (πΉβπ) = (πΉβπ)) β§ βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ)))))) |
91 | 90 | ralrn 7089 |
. . . . . . 7
β’ (πΉ Fn π β (βπ¦ β ran πΉ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))) β βπ β π ((((πΉβπ)π·(πΉβπ)) = 0 β (πΉβπ) = (πΉβπ)) β§ βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ)))))) |
92 | 26, 91 | syl 17 |
. . . . . 6
β’ (π β (βπ¦ β ran πΉ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))) β βπ β π ((((πΉβπ)π·(πΉβπ)) = 0 β (πΉβπ) = (πΉβπ)) β§ βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ)))))) |
93 | 32 | raleqdv 3325 |
. . . . . 6
β’ (π β (βπ¦ β ran πΉ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))) β βπ¦ β π΅ ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))))) |
94 | 92, 93 | bitr3d 280 |
. . . . 5
β’ (π β (βπ β π ((((πΉβπ)π·(πΉβπ)) = 0 β (πΉβπ) = (πΉβπ)) β§ βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ)))) β βπ¦ β π΅ ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))))) |
95 | 94 | ralbidv 3177 |
. . . 4
β’ (π β (βπ β π βπ β π ((((πΉβπ)π·(πΉβπ)) = 0 β (πΉβπ) = (πΉβπ)) β§ βπ§ β π΅ ((πΉβπ)π·(πΉβπ)) β€ ((π§π·(πΉβπ)) +π (π§π·(πΉβπ)))) β βπ β π βπ¦ β π΅ ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))))) |
96 | 82, 95 | mpbid 231 |
. . 3
β’ (π β βπ β π βπ¦ β π΅ ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦)))) |
97 | 37 | eqeq1d 2734 |
. . . . . . . . 9
β’ (π₯ = (πΉβπ) β ((π₯π·π¦) = 0 β ((πΉβπ)π·π¦) = 0)) |
98 | | eqeq1 2736 |
. . . . . . . . 9
β’ (π₯ = (πΉβπ) β (π₯ = π¦ β (πΉβπ) = π¦)) |
99 | 97, 98 | bibi12d 345 |
. . . . . . . 8
β’ (π₯ = (πΉβπ) β (((π₯π·π¦) = 0 β π₯ = π¦) β (((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦))) |
100 | | oveq2 7419 |
. . . . . . . . . . 11
β’ (π₯ = (πΉβπ) β (π§π·π₯) = (π§π·(πΉβπ))) |
101 | 100 | oveq1d 7426 |
. . . . . . . . . 10
β’ (π₯ = (πΉβπ) β ((π§π·π₯) +π (π§π·π¦)) = ((π§π·(πΉβπ)) +π (π§π·π¦))) |
102 | 37, 101 | breq12d 5161 |
. . . . . . . . 9
β’ (π₯ = (πΉβπ) β ((π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦)))) |
103 | 102 | ralbidv 3177 |
. . . . . . . 8
β’ (π₯ = (πΉβπ) β (βπ§ β π΅ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)) β βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦)))) |
104 | 99, 103 | anbi12d 631 |
. . . . . . 7
β’ (π₯ = (πΉβπ) β ((((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π΅ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))))) |
105 | 104 | ralbidv 3177 |
. . . . . 6
β’ (π₯ = (πΉβπ) β (βπ¦ β π΅ (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π΅ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β βπ¦ β π΅ ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))))) |
106 | 105 | ralrn 7089 |
. . . . 5
β’ (πΉ Fn π β (βπ₯ β ran πΉβπ¦ β π΅ (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π΅ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β βπ β π βπ¦ β π΅ ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))))) |
107 | 26, 106 | syl 17 |
. . . 4
β’ (π β (βπ₯ β ran πΉβπ¦ β π΅ (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π΅ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β βπ β π βπ¦ β π΅ ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))))) |
108 | 32 | raleqdv 3325 |
. . . 4
β’ (π β (βπ₯ β ran πΉβπ¦ β π΅ (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π΅ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β βπ₯ β π΅ βπ¦ β π΅ (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π΅ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))))) |
109 | 107, 108 | bitr3d 280 |
. . 3
β’ (π β (βπ β π βπ¦ β π΅ ((((πΉβπ)π·π¦) = 0 β (πΉβπ) = π¦) β§ βπ§ β π΅ ((πΉβπ)π·π¦) β€ ((π§π·(πΉβπ)) +π (π§π·π¦))) β βπ₯ β π΅ βπ¦ β π΅ (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π΅ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))))) |
110 | 96, 109 | mpbid 231 |
. 2
β’ (π β βπ₯ β π΅ βπ¦ β π΅ (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π΅ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))) |
111 | 15 | elfvexd 6930 |
. . . 4
β’ (π β π β V) |
112 | | focdmex 7944 |
. . . 4
β’ (π β V β (πΉ:πβontoβπ΅ β π΅ β V)) |
113 | 111, 5, 112 | sylc 65 |
. . 3
β’ (π β π΅ β V) |
114 | | isxmet 23837 |
. . 3
β’ (π΅ β V β (π· β (βMetβπ΅) β (π·:(π΅ Γ π΅)βΆβ* β§
βπ₯ β π΅ βπ¦ β π΅ (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π΅ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
115 | 113, 114 | syl 17 |
. 2
β’ (π β (π· β (βMetβπ΅) β (π·:(π΅ Γ π΅)βΆβ* β§
βπ₯ β π΅ βπ¦ β π΅ (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π΅ (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
116 | 46, 110, 115 | mpbir2and 711 |
1
β’ (π β π· β (βMetβπ΅)) |