Metamath Proof Explorer


Theorem ismet2

Description: An extended metric is a metric exactly when it takes real values for all values of the arguments. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion ismet2 D Met X D ∞Met X D : X × X

Proof

Step Hyp Ref Expression
1 elfvex D Met X X V
2 elfvex D ∞Met X X V
3 2 adantr D ∞Met X D : X × X X V
4 simpllr X V D : X × X x X y X z X D : X × X
5 simpr X V D : X × X x X y X z X z X
6 simplrl X V D : X × X x X y X z X x X
7 4 5 6 fovrnd X V D : X × X x X y X z X z D x
8 simplrr X V D : X × X x X y X z X y X
9 4 5 8 fovrnd X V D : X × X x X y X z X z D y
10 7 9 rexaddd X V D : X × X x X y X z X z D x + 𝑒 z D y = z D x + z D y
11 10 breq2d X V D : X × X x X y X z X x D y z D x + 𝑒 z D y x D y z D x + z D y
12 11 ralbidva X V D : X × X x X y X z X x D y z D x + 𝑒 z D y z X x D y z D x + z D y
13 12 anbi2d X V D : X × X x X y X x D y = 0 x = y z X x D y z D x + 𝑒 z D y x D y = 0 x = y z X x D y z D x + z D y
14 13 2ralbidva X V D : X × X x X y X x D y = 0 x = y z X x D y z D x + 𝑒 z D y x X y X x D y = 0 x = y z X x D y z D x + z D y
15 simpr X V D : X × X D : X × X
16 ressxr *
17 fss D : X × X * D : X × X *
18 15 16 17 sylancl X V D : X × X D : X × X *
19 18 biantrurd X V D : X × X x X y X x D y = 0 x = y z X x D y z D x + 𝑒 z D y D : X × X * x X y X x D y = 0 x = y z X x D y z D x + 𝑒 z D y
20 14 19 bitr3d X V D : X × X x X y X x D y = 0 x = y z X x D y z D x + z D y D : X × X * x X y X x D y = 0 x = y z X x D y z D x + 𝑒 z D y
21 20 pm5.32da X V D : X × X x X y X x D y = 0 x = y z X x D y z D x + z D y D : X × X D : X × X * x X y X x D y = 0 x = y z X x D y z D x + 𝑒 z D y
22 21 biancomd X V D : X × X x X y X x D y = 0 x = y z X x D y z D x + z D y D : X × X * x X y X x D y = 0 x = y z X x D y z D x + 𝑒 z D y D : X × X
23 ismet X V D Met X D : X × X x X y X x D y = 0 x = y z X x D y z D x + z D y
24 isxmet X V D ∞Met X D : X × X * x X y X x D y = 0 x = y z X x D y z D x + 𝑒 z D y
25 24 anbi1d X V D ∞Met X D : X × X D : X × X * x X y X x D y = 0 x = y z X x D y z D x + 𝑒 z D y D : X × X
26 22 23 25 3bitr4d X V D Met X D ∞Met X D : X × X
27 1 3 26 pm5.21nii D Met X D ∞Met X D : X × X