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