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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	colperpex.d	⊢ − = ( dist ‘ 𝐺 )
	colperpex.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	colperpex.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	colperpex.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	mideu.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
	mideu.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	mideu.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	mideulem.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	mideulem.2	⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
	mideulem.3	⊢ ( 𝜑 → 𝑂 ∈ 𝑃 )
	mideulem.4	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
	mideulem.5	⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝑄 𝐿 𝐵 ) )
	mideulem.6	⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑂 ) )
	mideulem.7	⊢ ( 𝜑 → 𝑇 ∈ ( 𝐴 𝐿 𝐵 ) )
	mideulem.8	⊢ ( 𝜑 → 𝑇 ∈ ( 𝑄 𝐼 𝑂 ) )
	mideulem.9	⊢ ( 𝜑 → ( 𝐴 − 𝑂 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑄 ) )
Assertion	mideulem	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		colperpex.d	⊢ − = ( dist ‘ 𝐺 )
3		colperpex.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		colperpex.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		colperpex.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		mideu.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
7		mideu.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8		mideu.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9		mideulem.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
10		mideulem.2	⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
11		mideulem.3	⊢ ( 𝜑 → 𝑂 ∈ 𝑃 )
12		mideulem.4	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
13		mideulem.5	⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝑄 𝐿 𝐵 ) )
14		mideulem.6	⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑂 ) )
15		mideulem.7	⊢ ( 𝜑 → 𝑇 ∈ ( 𝐴 𝐿 𝐵 ) )
16		mideulem.8	⊢ ( 𝜑 → 𝑇 ∈ ( 𝑄 𝐼 𝑂 ) )
17		mideulem.9	⊢ ( 𝜑 → ( 𝐴 − 𝑂 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑄 ) )
18		simprrl	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝑂 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑟 ) ) ) ) → 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
19	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → 𝐺 ∈ TarskiG )
20	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → 𝐴 ∈ 𝑃 )
21	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → 𝐵 ∈ 𝑃 )
22	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → 𝐴 ≠ 𝐵 )
23	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → 𝑄 ∈ 𝑃 )
24	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → 𝑂 ∈ 𝑃 )
25	12	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → 𝑇 ∈ 𝑃 )
26	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝑄 𝐿 𝐵 ) )
27	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑂 ) )
28	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → 𝑇 ∈ ( 𝐴 𝐿 𝐵 ) )
29	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → 𝑇 ∈ ( 𝑄 𝐼 𝑂 ) )
30		simplr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → 𝑟 ∈ 𝑃 )
31		simprl	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) )
32		simprr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) )
33	1 2 3 4 19 6 20 21 22 23 24 25 26 27 28 29 30 31 32	opphllem	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝑂 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑟 ) ) )
34	18 33	reximddv	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
35		eqid	⊢ ( ≤G ‘ 𝐺 ) = ( ≤G ‘ 𝐺 )
36	1 2 3 35 5 7 11 8 10	legov	⊢ ( 𝜑 → ( ( 𝐴 − 𝑂 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑄 ) ↔ ∃ 𝑟 ∈ 𝑃 ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) ) )
37	17 36	mpbid	⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑃 ( 𝑟 ∈ ( 𝐵 𝐼 𝑄 ) ∧ ( 𝐴 − 𝑂 ) = ( 𝐵 − 𝑟 ) ) )
38	34 37	r19.29a	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )

Metamath Proof Explorer

Theorem mideulem

Proof