Step |
Hyp |
Ref |
Expression |
1 |
|
mscl.x |
⊢ 𝑋 = ( Base ‘ 𝑀 ) |
2 |
|
mscl.d |
⊢ 𝐷 = ( dist ‘ 𝑀 ) |
3 |
1 2
|
msmet2 |
⊢ ( 𝑀 ∈ MetSp → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) ) |
4 |
|
mettri2 |
⊢ ( ( ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐵 ) ≤ ( ( 𝐶 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐴 ) + ( 𝐶 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐵 ) ) ) |
5 |
3 4
|
sylan |
⊢ ( ( 𝑀 ∈ MetSp ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐵 ) ≤ ( ( 𝐶 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐴 ) + ( 𝐶 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐵 ) ) ) |
6 |
|
simpr2 |
⊢ ( ( 𝑀 ∈ MetSp ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 ) |
7 |
|
simpr3 |
⊢ ( ( 𝑀 ∈ MetSp ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 ) |
8 |
6 7
|
ovresd |
⊢ ( ( 𝑀 ∈ MetSp ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐵 ) = ( 𝐴 𝐷 𝐵 ) ) |
9 |
|
simpr1 |
⊢ ( ( 𝑀 ∈ MetSp ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐶 ∈ 𝑋 ) |
10 |
9 6
|
ovresd |
⊢ ( ( 𝑀 ∈ MetSp ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐶 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐴 ) = ( 𝐶 𝐷 𝐴 ) ) |
11 |
9 7
|
ovresd |
⊢ ( ( 𝑀 ∈ MetSp ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐶 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐵 ) = ( 𝐶 𝐷 𝐵 ) ) |
12 |
10 11
|
oveq12d |
⊢ ( ( 𝑀 ∈ MetSp ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐶 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐴 ) + ( 𝐶 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝐵 ) ) = ( ( 𝐶 𝐷 𝐴 ) + ( 𝐶 𝐷 𝐵 ) ) ) |
13 |
5 8 12
|
3brtr3d |
⊢ ( ( 𝑀 ∈ MetSp ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( ( 𝐶 𝐷 𝐴 ) + ( 𝐶 𝐷 𝐵 ) ) ) |