Theorem metidv

Description: A and B identify by the metric D if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018)

	Ref	Expression
Assertion	metidv	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ( ~Met ‘ 𝐷 ) 𝐵 ↔ ( 𝐴 𝐷 𝐵 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 ∈ 𝑋 ↔ 𝐴 ∈ 𝑋 ) )
2		eleq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋 ) )
3	1 2	bi2anan9	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) )
4		oveq12	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 𝐷 𝑏 ) = ( 𝐴 𝐷 𝐵 ) )
5	4	eqeq1d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 𝐷 𝑏 ) = 0 ↔ ( 𝐴 𝐷 𝐵 ) = 0 ) )
6	3 5	anbi12d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑎 𝐷 𝑏 ) = 0 ) ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝐷 𝐵 ) = 0 ) ) )
7		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑎 𝐷 𝑏 ) = 0 ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑎 𝐷 𝑏 ) = 0 ) }
8	6 7	brabga	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑎 𝐷 𝑏 ) = 0 ) } 𝐵 ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝐷 𝐵 ) = 0 ) ) )
9	8	adantl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑎 𝐷 𝑏 ) = 0 ) } 𝐵 ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝐷 𝐵 ) = 0 ) ) )
10		metidval	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ~Met ‘ 𝐷 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑎 𝐷 𝑏 ) = 0 ) } )
11	10	adantr	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ~Met ‘ 𝐷 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑎 𝐷 𝑏 ) = 0 ) } )
12	11	breqd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ( ~Met ‘ 𝐷 ) 𝐵 ↔ 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝑎 𝐷 𝑏 ) = 0 ) } 𝐵 ) )
13		ibar	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) = 0 ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝐷 𝐵 ) = 0 ) ) )
14	13	adantl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) = 0 ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐴 𝐷 𝐵 ) = 0 ) ) )
15	9 12 14	3bitr4d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ( ~Met ‘ 𝐷 ) 𝐵 ↔ ( 𝐴 𝐷 𝐵 ) = 0 ) )