mideulem

Description: Lemma for mideu . We can assume mideulem.9 "without loss of generality". (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$
	mideulem.1	$⊢ φ \to A \neq B$
	mideulem.2	$⊢ φ \to Q \in P$
	mideulem.3	$⊢ φ \to O \in P$
	mideulem.4	$⊢ φ \to T \in P$
	mideulem.5	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (Q L B)$
	mideulem.6	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (A L O)$
	mideulem.7	$⊢ φ \to T \in (A L B)$
	mideulem.8	$⊢ φ \to T \in (Q I O)$
	mideulem.9	$⊢ φ \to (A \underset{˙}{-} O) \leq_{𝒢} (G) (B \underset{˙}{-} Q)$
Assertion	mideulem	$⊢ φ \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		mideulem.1	$⊢ φ \to A \neq B$
10		mideulem.2	$⊢ φ \to Q \in P$
11		mideulem.3	$⊢ φ \to O \in P$
12		mideulem.4	$⊢ φ \to T \in P$
13		mideulem.5	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (Q L B)$
14		mideulem.6	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (A L O)$
15		mideulem.7	$⊢ φ \to T \in (A L B)$
16		mideulem.8	$⊢ φ \to T \in (Q I O)$
17		mideulem.9	$⊢ φ \to (A \underset{˙}{-} O) \leq_{𝒢} (G) (B \underset{˙}{-} Q)$
18		simprrl	$⊢ (((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \land (x \in P \land (B = S (x) (A) \land O = S (x) (r)))) \to B = S (x) (A)$
19	5	ad2antrr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to G \in 𝒢_{Tarski}$
20	7	ad2antrr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to A \in P$
21	8	ad2antrr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to B \in P$
22	9	ad2antrr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to A \neq B$
23	10	ad2antrr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to Q \in P$
24	11	ad2antrr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to O \in P$
25	12	ad2antrr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to T \in P$
26	13	ad2antrr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to (A L B) ⟂_{𝒢} (G) (Q L B)$
27	14	ad2antrr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to (A L B) ⟂_{𝒢} (G) (A L O)$
28	15	ad2antrr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to T \in (A L B)$
29	16	ad2antrr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to T \in (Q I O)$
30		simplr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to r \in P$
31		simprl	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to r \in (B I Q)$
32		simprr	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to A \underset{˙}{-} O = B \underset{˙}{-} r$
33	1 2 3 4 19 6 20 21 22 23 24 25 26 27 28 29 30 31 32	opphllem	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to \exists x \in P (B = S (x) (A) \land O = S (x) (r))$
34	18 33	reximddv	$⊢ ((φ \land r \in P) \land (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)) \to \exists x \in P B = S (x) (A)$
35		eqid	$⊢ \leq_{𝒢} (G) = \leq_{𝒢} (G)$
36	1 2 3 35 5 7 11 8 10	legov	$⊢ φ \to ((A \underset{˙}{-} O) \leq_{𝒢} (G) (B \underset{˙}{-} Q) \leftrightarrow \exists r \in P (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r))$
37	17 36	mpbid	$⊢ φ \to \exists r \in P (r \in (B I Q) \land A \underset{˙}{-} O = B \underset{˙}{-} r)$
38	34 37	r19.29a	$⊢ φ \to \exists x \in P B = S (x) (A)$

Metamath Proof Explorer

Theorem mideulem

Proof