Metamath Proof Explorer

Theorem mideu

Description: Existence and uniqueness of the midpoint, Theorem 8.22 of Schwabhauser p. 64. (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 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
mideu.3 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
Assertion mideu ( 𝜑 → ∃! 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )

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 mideu.3 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
10 1 2 3 4 5 6 7 8 9 midex ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
11 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) ∧ ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → 𝐺 ∈ TarskiG )
12 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) ∧ ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → 𝑥 ∈ 𝑃 )
13 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) ∧ ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → 𝑦 ∈ 𝑃 )
14 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) ∧ ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → 𝐴 ∈ 𝑃 )
15 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) ∧ ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → 𝐵 ∈ 𝑃 )
16 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) ∧ ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
17 16 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) ∧ ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) = 𝐵 )
18 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) ∧ ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) )
19 18 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) ∧ ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) = 𝐵 )
20 1 2 3 4 6 11 12 13 14 15 17 19 miduniq ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) ∧ ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → 𝑥 = 𝑦 )
21 20 ex ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) → 𝑥 = 𝑦 ) )
22 21 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) → 𝑥 = 𝑦 ) )
23 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑦 ) )
24 23 fveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) )
25 24 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ↔ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) )
26 25 rmo4 ⊢ ( ∃* 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( ( 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝑦 ) ‘ 𝐴 ) ) → 𝑥 = 𝑦 ) )
27 22 26 sylibr ⊢ ( 𝜑 → ∃* 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
28 reu5 ⊢ ( ∃! 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ↔ ( ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ∧ ∃* 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) ) )
29 10 27 28 sylanbrc ⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )