tgbtwndiff

Description: There is always a c distinct from B such that B lies between A and c . Theorem 3.14 of Schwabhauser p. 32. The condition "the space is of dimension 1 or more" is written here as 2 <_ ( #P ) for simplicity. (Contributed by Thierry Arnoux, 23-Mar-2019)

	Ref	Expression
Hypotheses	tgbtwndiff.p	$⊢ P = {Base}_{G}$
	tgbtwndiff.d	$⊢ \underset{˙}{-} = dist (G)$
	tgbtwndiff.i	$⊢ I = Itv (G)$
	tgbtwndiff.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgbtwndiff.a	$⊢ φ \to A \in P$
	tgbtwndiff.b	$⊢ φ \to B \in P$
	tgbtwndiff.l	$⊢ φ \to 2 \leq \|P\|$
Assertion	tgbtwndiff	$⊢ φ \to \exists c \in P (B \in (A I c) \land B \neq c)$

Proof

Step	Hyp	Ref	Expression
1		tgbtwndiff.p	$⊢ P = {Base}_{G}$
2		tgbtwndiff.d	$⊢ \underset{˙}{-} = dist (G)$
3		tgbtwndiff.i	$⊢ I = Itv (G)$
4		tgbtwndiff.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tgbtwndiff.a	$⊢ φ \to A \in P$
6		tgbtwndiff.b	$⊢ φ \to B \in P$
7		tgbtwndiff.l	$⊢ φ \to 2 \leq \|P\|$
8	4	ad3antrrr	$⊢ (((φ \land u \in P) \land v \in P) \land u \neq v) \to G \in 𝒢_{Tarski}$
9	5	ad3antrrr	$⊢ (((φ \land u \in P) \land v \in P) \land u \neq v) \to A \in P$
10	6	ad3antrrr	$⊢ (((φ \land u \in P) \land v \in P) \land u \neq v) \to B \in P$
11		simpllr	$⊢ (((φ \land u \in P) \land v \in P) \land u \neq v) \to u \in P$
12		simplr	$⊢ (((φ \land u \in P) \land v \in P) \land u \neq v) \to v \in P$
13	1 2 3 8 9 10 11 12	axtgsegcon	$⊢ (((φ \land u \in P) \land v \in P) \land u \neq v) \to \exists c \in P (B \in (A I c) \land B \underset{˙}{-} c = u \underset{˙}{-} v)$
14	8	ad3antrrr	$⊢ ((((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \land B = c) \to G \in 𝒢_{Tarski}$
15	11	ad3antrrr	$⊢ ((((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \land B = c) \to u \in P$
16	12	ad3antrrr	$⊢ ((((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \land B = c) \to v \in P$
17	10	ad3antrrr	$⊢ ((((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \land B = c) \to B \in P$
18		simpr	$⊢ ((((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \land B = c) \to B = c$
19	18	oveq2d	$⊢ ((((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \land B = c) \to B \underset{˙}{-} B = B \underset{˙}{-} c$
20		simplr	$⊢ ((((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \land B = c) \to B \underset{˙}{-} c = u \underset{˙}{-} v$
21	19 20	eqtr2d	$⊢ ((((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \land B = c) \to u \underset{˙}{-} v = B \underset{˙}{-} B$
22	1 2 3 14 15 16 17 21	axtgcgrid	$⊢ ((((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \land B = c) \to u = v$
23		simp-4r	$⊢ ((((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \land B = c) \to u \neq v$
24	23	neneqd	$⊢ ((((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \land B = c) \to \neg u = v$
25	22 24	pm2.65da	$⊢ (((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \to \neg B = c$
26	25	neqned	$⊢ (((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \to B \neq c$
27	26	ex	$⊢ ((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \to (B \underset{˙}{-} c = u \underset{˙}{-} v \to B \neq c)$
28	27	anim2d	$⊢ ((((φ \land u \in P) \land v \in P) \land u \neq v) \land c \in P) \to ((B \in (A I c) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \to (B \in (A I c) \land B \neq c))$
29	28	reximdva	$⊢ (((φ \land u \in P) \land v \in P) \land u \neq v) \to (\exists c \in P (B \in (A I c) \land B \underset{˙}{-} c = u \underset{˙}{-} v) \to \exists c \in P (B \in (A I c) \land B \neq c))$
30	13 29	mpd	$⊢ (((φ \land u \in P) \land v \in P) \land u \neq v) \to \exists c \in P (B \in (A I c) \land B \neq c)$
31	1 2 3 4 7	tglowdim1	$⊢ φ \to \exists u \in P \exists v \in P u \neq v$
32	30 31	r19.29vva	$⊢ φ \to \exists c \in P (B \in (A I c) \land B \neq c)$

Metamath Proof Explorer

Theorem tgbtwndiff

Proof