midex

Description: Existence of the midpoint, part Theorem 8.22 of Schwabhauser p. 64. Note that this proof requires a construction in 2 dimensions or more, i.e. it does not prove the existence of a midpoint in dimension 1, for a geometry restricted to a line. (Contributed by Thierry Arnoux, 25-Nov-2019)

	Ref	Expression
Hypotheses	colperpex.p	$⊢ P = {Base}_{G}$
	colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
	colperpex.i	$⊢ I = Itv (G)$
	colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
	colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mideu.s	$⊢ S = {pInv}_{𝒢} (G)$
	mideu.1	$⊢ φ \to A \in P$
	mideu.2	$⊢ φ \to B \in P$
	mideu.3	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
Assertion	midex	$⊢ φ \to \exists x \in P B = S (x) (A)$

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	$⊢ P = {Base}_{G}$
2		colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
3		colperpex.i	$⊢ I = Itv (G)$
4		colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
5		colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		mideu.s	$⊢ S = {pInv}_{𝒢} (G)$
7		mideu.1	$⊢ φ \to A \in P$
8		mideu.2	$⊢ φ \to B \in P$
9		mideu.3	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
10	5	adantr	$⊢ (φ \land A = B) \to G \in 𝒢_{Tarski}$
11	7	adantr	$⊢ (φ \land A = B) \to A \in P$
12		eqid	$⊢ S (A) = S (A)$
13	1 2 3 4 6 10 11 12	mircinv	$⊢ (φ \land A = B) \to S (A) (A) = A$
14		simpr	$⊢ (φ \land A = B) \to A = B$
15	13 14	eqtr2d	$⊢ (φ \land A = B) \to B = S (A) (A)$
16		fveq2	$⊢ x = A \to S (x) = S (A)$
17	16	fveq1d	$⊢ x = A \to S (x) (A) = S (A) (A)$
18	17	rspceeqv	$⊢ (A \in P \land B = S (A) (A)) \to \exists x \in P B = S (x) (A)$
19	7 15 18	syl2an2r	$⊢ (φ \land A = B) \to \exists x \in P B = S (x) (A)$
20	5	ad3antrrr	$⊢ (((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \to G \in 𝒢_{Tarski}$
21	20	ad4antr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to G \in 𝒢_{Tarski}$
22	7	ad3antrrr	$⊢ (((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \to A \in P$
23	22	ad4antr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to A \in P$
24	8	ad3antrrr	$⊢ (((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \to B \in P$
25	24	ad4antr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to B \in P$
26		simpllr	$⊢ (((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \to A \neq B$
27	26	ad4antr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to A \neq B$
28		simplr	$⊢ (((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \to q \in P$
29	28	ad4antr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to q \in P$
30		simp-4r	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to p \in P$
31		simpllr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to t \in P$
32		simp-5r	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to (B L q) ⟂_{𝒢} (G) (A L B)$
33	4 21 32	perpln1	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to B L q \in ran L$
34	1 3 4 21 23 25 27	tgelrnln	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to A L B \in ran L$
35	1 2 3 4 21 33 34 32	perpcom	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to (A L B) ⟂_{𝒢} (G) (B L q)$
36	1 3 4 21 25 29 33	tglnne	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to B \neq q$
37	1 3 4 21 25 29 36	tglinecom	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to B L q = q L B$
38	35 37	breqtrd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to (A L B) ⟂_{𝒢} (G) (q L B)$
39		simplr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))$
40	39	simpld	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to (A L p) ⟂_{𝒢} (G) (A L B)$
41	4 21 40	perpln1	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to A L p \in ran L$
42	1 2 3 4 21 41 34 40	perpcom	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to (A L B) ⟂_{𝒢} (G) (A L p)$
43	27	neneqd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to \neg A = B$
44	39	simprd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to ((t \in (A L B) \lor A = B) \land t \in (q I p))$
45	44	simpld	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to (t \in (A L B) \lor A = B)$
46	45	orcomd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to (A = B \lor t \in (A L B))$
47	46	ord	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to (\neg A = B \to t \in (A L B))$
48	43 47	mpd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to t \in (A L B)$
49	44	simprd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to t \in (q I p)$
50		simpr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)$
51	1 2 3 4 21 6 23 25 27 29 30 31 38 42 48 49 50	mideulem	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q)) \to \exists x \in P B = S (x) (A)$
52	20	ad4antr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to G \in 𝒢_{Tarski}$
53	52	adantr	$⊢ ((((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \land (x \in P \land A = S (x) (B))) \to G \in 𝒢_{Tarski}$
54		simprl	$⊢ ((((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \land (x \in P \land A = S (x) (B))) \to x \in P$
55		eqid	$⊢ S (x) = S (x)$
56	24	ad4antr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to B \in P$
57	56	adantr	$⊢ ((((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \land (x \in P \land A = S (x) (B))) \to B \in P$
58		simprr	$⊢ ((((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \land (x \in P \land A = S (x) (B))) \to A = S (x) (B)$
59	58	eqcomd	$⊢ ((((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \land (x \in P \land A = S (x) (B))) \to S (x) (B) = A$
60	1 2 3 4 6 53 54 55 57 59	mircom	$⊢ ((((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \land (x \in P \land A = S (x) (B))) \to S (x) (A) = B$
61	60	eqcomd	$⊢ ((((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \land (x \in P \land A = S (x) (B))) \to B = S (x) (A)$
62	22	ad4antr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to A \in P$
63	26	ad4antr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to A \neq B$
64	63	necomd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to B \neq A$
65		simp-4r	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to p \in P$
66	28	ad4antr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to q \in P$
67		simpllr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to t \in P$
68		simplr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))$
69	68	simpld	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to (A L p) ⟂_{𝒢} (G) (A L B)$
70	4 52 69	perpln1	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to A L p \in ran L$
71	1 3 4 52 62 65 70	tglnne	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to A \neq p$
72	1 3 4 52 62 65 71	tglinecom	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to A L p = p L A$
73	72 70	eqeltrrd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to p L A \in ran L$
74	1 3 4 52 56 62 64	tgelrnln	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to B L A \in ran L$
75	1 3 4 52 62 56 63	tglinecom	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to A L B = B L A$
76	69 72 75	3brtr3d	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to (p L A) ⟂_{𝒢} (G) (B L A)$
77	1 2 3 4 52 73 74 76	perpcom	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to (B L A) ⟂_{𝒢} (G) (p L A)$
78		simp-5r	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to (B L q) ⟂_{𝒢} (G) (A L B)$
79	4 52 78	perpln1	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to B L q \in ran L$
80	78 75	breqtrd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to (B L q) ⟂_{𝒢} (G) (B L A)$
81	1 2 3 4 52 79 74 80	perpcom	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to (B L A) ⟂_{𝒢} (G) (B L q)$
82	63	neneqd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to \neg A = B$
83	68	simprd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to ((t \in (A L B) \lor A = B) \land t \in (q I p))$
84	83	simpld	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to (t \in (A L B) \lor A = B)$
85	84	orcomd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to (A = B \lor t \in (A L B))$
86	85	ord	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to (\neg A = B \to t \in (A L B))$
87	82 86	mpd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to t \in (A L B)$
88	87 75	eleqtrd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to t \in (B L A)$
89	83	simprd	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to t \in (q I p)$
90	1 2 3 52 66 67 65 89	tgbtwncom	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to t \in (p I q)$
91		simpr	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)$
92	1 2 3 4 52 6 56 62 64 65 66 67 77 81 88 90 91	mideulem	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to \exists x \in P A = S (x) (B)$
93	61 92	reximddv	$⊢ (((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \land (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p)) \to \exists x \in P B = S (x) (A)$
94		eqid	$⊢ \leq_{𝒢} (G) = \leq_{𝒢} (G)$
95	20	ad3antrrr	$⊢ ((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \to G \in 𝒢_{Tarski}$
96	22	ad3antrrr	$⊢ ((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \to A \in P$
97		simpllr	$⊢ ((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \to p \in P$
98	24	ad3antrrr	$⊢ ((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \to B \in P$
99		simp-5r	$⊢ ((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \to q \in P$
100	1 2 3 94 95 96 97 98 99	legtrid	$⊢ ((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \to ((A \underset{˙}{-} p) \leq_{𝒢} (G) (B \underset{˙}{-} q) \lor (B \underset{˙}{-} q) \leq_{𝒢} (G) (A \underset{˙}{-} p))$
101	51 93 100	mpjaodan	$⊢ ((((((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \land p \in P) \land t \in P) \land ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))) \to \exists x \in P B = S (x) (A)$
102	9	ad3antrrr	$⊢ (((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \to G {Dim}_{𝒢} \geq 2$
103	1 2 3 4 20 22 24 28 26 102	colperpex	$⊢ (((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \to \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (q I p)))$
104		r19.42v	$⊢ \exists t \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p))) \leftrightarrow ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (q I p)))$
105	104	rexbii	$⊢ \exists p \in P \exists t \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p))) \leftrightarrow \exists p \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land \exists t \in P ((t \in (A L B) \lor A = B) \land t \in (q I p)))$
106	103 105	sylibr	$⊢ (((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \to \exists p \in P \exists t \in P ((A L p) ⟂_{𝒢} (G) (A L B) \land ((t \in (A L B) \lor A = B) \land t \in (q I p)))$
107	101 106	r19.29vva	$⊢ (((φ \land A \neq B) \land q \in P) \land (B L q) ⟂_{𝒢} (G) (A L B)) \to \exists x \in P B = S (x) (A)$
108	5	adantr	$⊢ (φ \land A \neq B) \to G \in 𝒢_{Tarski}$
109	8	adantr	$⊢ (φ \land A \neq B) \to B \in P$
110	7	adantr	$⊢ (φ \land A \neq B) \to A \in P$
111		simpr	$⊢ (φ \land A \neq B) \to A \neq B$
112	111	necomd	$⊢ (φ \land A \neq B) \to B \neq A$
113	9	adantr	$⊢ (φ \land A \neq B) \to G {Dim}_{𝒢} \geq 2$
114	1 2 3 4 108 109 110 110 112 113	colperpex	$⊢ (φ \land A \neq B) \to \exists q \in P ((B L q) ⟂_{𝒢} (G) (B L A) \land \exists s \in P ((s \in (B L A) \lor B = A) \land s \in (A I q)))$
115		simprl	$⊢ ((φ \land A \neq B) \land ((B L q) ⟂_{𝒢} (G) (B L A) \land \exists s \in P ((s \in (B L A) \lor B = A) \land s \in (A I q)))) \to (B L q) ⟂_{𝒢} (G) (B L A)$
116	1 3 4 108 110 109 111	tglinecom	$⊢ (φ \land A \neq B) \to A L B = B L A$
117	116	adantr	$⊢ ((φ \land A \neq B) \land ((B L q) ⟂_{𝒢} (G) (B L A) \land \exists s \in P ((s \in (B L A) \lor B = A) \land s \in (A I q)))) \to A L B = B L A$
118	115 117	breqtrrd	$⊢ ((φ \land A \neq B) \land ((B L q) ⟂_{𝒢} (G) (B L A) \land \exists s \in P ((s \in (B L A) \lor B = A) \land s \in (A I q)))) \to (B L q) ⟂_{𝒢} (G) (A L B)$
119	118	ex	$⊢ (φ \land A \neq B) \to (((B L q) ⟂_{𝒢} (G) (B L A) \land \exists s \in P ((s \in (B L A) \lor B = A) \land s \in (A I q))) \to (B L q) ⟂_{𝒢} (G) (A L B))$
120	119	reximdv	$⊢ (φ \land A \neq B) \to (\exists q \in P ((B L q) ⟂_{𝒢} (G) (B L A) \land \exists s \in P ((s \in (B L A) \lor B = A) \land s \in (A I q))) \to \exists q \in P (B L q) ⟂_{𝒢} (G) (A L B))$
121	114 120	mpd	$⊢ (φ \land A \neq B) \to \exists q \in P (B L q) ⟂_{𝒢} (G) (A L B)$
122	107 121	r19.29a	$⊢ (φ \land A \neq B) \to \exists x \in P B = S (x) (A)$
123	19 122	pm2.61dane	$⊢ φ \to \exists x \in P B = S (x) (A)$

Metamath Proof Explorer

Theorem midex

Proof