Metamath Proof Explorer

Theorem xmetsym

Description: The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmetsym 
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )

Proof

Step Hyp Ref Expression
1 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
2 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ B e. X /\ A e. X ) -> ( B D A ) e. RR* )
3 2 3com23 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( B D A ) e. RR* )
4 simp1 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> D e. ( *Met ` X ) )
5 simp3 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> B e. X )
6 simp2 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> A e. X )
7 xmettri2 
 |-  ( ( D e. ( *Met ` X ) /\ ( B e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( B D A ) +e ( B D B ) ) )
8 4 5 6 5 7 syl13anc 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) <_ ( ( B D A ) +e ( B D B ) ) )
9 xmet0 
 |-  ( ( D e. ( *Met ` X ) /\ B e. X ) -> ( B D B ) = 0 )
10 9 3adant2 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( B D B ) = 0 )
11 10 oveq2d 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( ( B D A ) +e ( B D B ) ) = ( ( B D A ) +e 0 ) )
12 2 xaddid1d 
 |-  ( ( D e. ( *Met ` X ) /\ B e. X /\ A e. X ) -> ( ( B D A ) +e 0 ) = ( B D A ) )
13 12 3com23 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( ( B D A ) +e 0 ) = ( B D A ) )
14 11 13 eqtrd 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( ( B D A ) +e ( B D B ) ) = ( B D A ) )
15 8 14 breqtrd 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) <_ ( B D A ) )
16 xmettri2 
 |-  ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ A e. X ) ) -> ( B D A ) <_ ( ( A D B ) +e ( A D A ) ) )
17 4 6 5 6 16 syl13anc 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( B D A ) <_ ( ( A D B ) +e ( A D A ) ) )
18 xmet0 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X ) -> ( A D A ) = 0 )
19 18 3adant3 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D A ) = 0 )
20 19 oveq2d 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( ( A D B ) +e ( A D A ) ) = ( ( A D B ) +e 0 ) )
21 1 xaddid1d 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( ( A D B ) +e 0 ) = ( A D B ) )
22 20 21 eqtrd 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( ( A D B ) +e ( A D A ) ) = ( A D B ) )
23 17 22 breqtrd 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( B D A ) <_ ( A D B ) )
24 1 3 15 23 xrletrid 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )