blin

Description: The intersection of two balls with the same center is the smaller of them. (Contributed by NM, 1-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

		Ref	Expression
	Assertion	blin	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) = ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ^* )
2	1	ad4ant124	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ^* )
3		simplrl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ℝ^* )
4		simplrr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ∈ ℝ^* )
5		xrltmin	⊢ ( ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) → ( ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ↔ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
6	2 3 4 5	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ↔ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
7	6	pm5.32da	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) ) )
8		ifcl	⊢ ( ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) → if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ∈ ℝ^* )
9		elbl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ) )
10	9	3expa	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ) )
11	8 10	sylan2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ) )
12		elbl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
13	12	3expa	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
14	13	adantrr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
15		elbl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
16	15	3expa	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑆 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
17	16	adantrl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
18	14 17	anbi12d	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) ) )
19		elin	⊢ ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) )
20		anandi	⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) )
21	18 19 20	3bitr4g	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) → ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑆 ) ) ) )
22	7 11 21	3bitr4rd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) → ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) ) )
23	22	eqrdv	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) ) = ( 𝑃 ( ball ‘ 𝐷 ) if ( 𝑅 ≤ 𝑆 , 𝑅 , 𝑆 ) ) )

Metamath Proof Explorer

Theorem blin

Proof