Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )