Metamath Proof Explorer

Theorem mirreu3

Description: Existential uniqueness of the mirror point. Theorem 7.8 of Schwabhauser p. 49. (Contributed by Thierry Arnoux, 30-May-2019)

Ref Expression
Hypotheses mirreu.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirreu.d ⊢ − = ( dist ‘ 𝐺 )
mirreu.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
mirreu.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
mirreu.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
mirreu.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )
Assertion mirreu3 ( 𝜑 → ∃! 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 mirreu.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 mirreu.d ⊢ − = ( dist ‘ 𝐺 )
3 mirreu.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 mirreu.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 mirreu.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 mirreu.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )
7 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑀 ) → 𝐴 ∈ 𝑃 )
8 eqidd ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑀 ) → ( 𝑀 − 𝐴 ) = ( 𝑀 − 𝐴 ) )
9 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑀 ) → 𝐴 = 𝑀 )
10 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑀 ) → 𝐺 ∈ TarskiG )
11 1 2 3 10 7 7 tgbtwntriv2 ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑀 ) → 𝐴 ∈ ( 𝐴 𝐼 𝐴 ) )
12 9 11 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑀 ) → 𝑀 ∈ ( 𝐴 𝐼 𝐴 ) )
13 oveq2 ⊢ ( 𝑏 = 𝐴 → ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) )
14 13 eqeq1d ⊢ ( 𝑏 = 𝐴 → ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ↔ ( 𝑀 − 𝐴 ) = ( 𝑀 − 𝐴 ) ) )
15 oveq1 ⊢ ( 𝑏 = 𝐴 → ( 𝑏 𝐼 𝐴 ) = ( 𝐴 𝐼 𝐴 ) )
16 15 eleq2d ⊢ ( 𝑏 = 𝐴 → ( 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ↔ 𝑀 ∈ ( 𝐴 𝐼 𝐴 ) ) )
17 14 16 anbi12d ⊢ ( 𝑏 = 𝐴 → ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ↔ ( ( 𝑀 − 𝐴 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝐴 𝐼 𝐴 ) ) ) )
18 17 rspcev ⊢ ( ( 𝐴 ∈ 𝑃 ∧ ( ( 𝑀 − 𝐴 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝐴 𝐼 𝐴 ) ) ) → ∃ 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) )
19 7 8 12 18 syl12anc ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑀 ) → ∃ 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) )
20 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝐺 ∈ TarskiG )
21 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑀 ∈ 𝑃 )
22 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑏 ∈ 𝑃 )
23 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) )
24 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝐴 = 𝑀 )
25 24 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → ( 𝑀 − 𝐴 ) = ( 𝑀 − 𝑀 ) )
26 23 25 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝑀 ) )
27 1 2 3 20 21 22 21 26 axtgcgrid ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑀 = 𝑏 )
28 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑐 ∈ 𝑃 )
29 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) )
30 29 25 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝑀 ) )
31 1 2 3 20 21 28 21 30 axtgcgrid ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑀 = 𝑐 )
32 27 31 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑏 = 𝑐 )
33 32 ex ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) → ( ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) → 𝑏 = 𝑐 ) )
34 33 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑀 ) → ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ( ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) → 𝑏 = 𝑐 ) )
35 19 34 jca ⊢ ( ( 𝜑 ∧ 𝐴 = 𝑀 ) → ( ∃ 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ( ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) → 𝑏 = 𝑐 ) ) )
36 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) → 𝐺 ∈ TarskiG )
37 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) → 𝐴 ∈ 𝑃 )
38 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) → 𝑀 ∈ 𝑃 )
39 1 2 3 36 37 38 38 37 axtgsegcon ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) → ∃ 𝑏 ∈ 𝑃 ( 𝑀 ∈ ( 𝐴 𝐼 𝑏 ) ∧ ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ) )
40 ancom ⊢ ( ( 𝑀 ∈ ( 𝐴 𝐼 𝑏 ) ∧ ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ) ↔ ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝐴 𝐼 𝑏 ) ) )
41 4 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) → 𝐺 ∈ TarskiG )
42 5 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) → 𝐴 ∈ 𝑃 )
43 6 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) → 𝑀 ∈ 𝑃 )
44 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) → 𝑏 ∈ 𝑃 )
45 1 2 3 41 42 43 44 tgbtwncomb ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) → ( 𝑀 ∈ ( 𝐴 𝐼 𝑏 ) ↔ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) )
46 45 anbi2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) → ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝐴 𝐼 𝑏 ) ) ↔ ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ) )
47 40 46 bitrid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑃 ) → ( ( 𝑀 ∈ ( 𝐴 𝐼 𝑏 ) ∧ ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ) ↔ ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ) )
48 47 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ 𝑃 ( 𝑀 ∈ ( 𝐴 𝐼 𝑏 ) ∧ ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ) ↔ ∃ 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) → ( ∃ 𝑏 ∈ 𝑃 ( 𝑀 ∈ ( 𝐴 𝐼 𝑏 ) ∧ ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ) ↔ ∃ 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ) )
50 39 49 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) → ∃ 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) )
51 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝐺 ∈ TarskiG )
52 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑀 ∈ 𝑃 )
53 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝐴 ∈ 𝑃 )
54 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑏 ∈ 𝑃 )
55 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑐 ∈ 𝑃 )
56 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝐴 ≠ 𝑀 )
57 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) )
58 1 2 3 51 54 52 53 57 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑀 ∈ ( 𝐴 𝐼 𝑏 ) )
59 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) )
60 1 2 3 51 55 52 53 59 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑀 ∈ ( 𝐴 𝐼 𝑐 ) )
61 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) )
62 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) )
63 1 2 3 51 52 52 53 53 54 55 56 58 60 61 62 tgsegconeq ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) ∧ ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) ) → 𝑏 = 𝑐 )
64 63 ex ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) ∧ ( 𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ) ) → ( ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) → 𝑏 = 𝑐 ) )
65 64 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) → ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ( ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) → 𝑏 = 𝑐 ) )
66 50 65 jca ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑀 ) → ( ∃ 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ( ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) → 𝑏 = 𝑐 ) ) )
67 35 66 pm2.61dane ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ( ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) → 𝑏 = 𝑐 ) ) )
68 oveq2 ⊢ ( 𝑏 = 𝑐 → ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝑐 ) )
69 68 eqeq1d ⊢ ( 𝑏 = 𝑐 → ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ↔ ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ) )
70 oveq1 ⊢ ( 𝑏 = 𝑐 → ( 𝑏 𝐼 𝐴 ) = ( 𝑐 𝐼 𝐴 ) )
71 70 eleq2d ⊢ ( 𝑏 = 𝑐 → ( 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ↔ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) )
72 69 71 anbi12d ⊢ ( 𝑏 = 𝑐 → ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ↔ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) )
73 72 reu4 ⊢ ( ∃! 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ↔ ( ∃ 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ∀ 𝑏 ∈ 𝑃 ∀ 𝑐 ∈ 𝑃 ( ( ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) ∧ ( ( 𝑀 − 𝑐 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑐 𝐼 𝐴 ) ) ) → 𝑏 = 𝑐 ) ) )
74 67 73 sylibr ⊢ ( 𝜑 → ∃! 𝑏 ∈ 𝑃 ( ( 𝑀 − 𝑏 ) = ( 𝑀 − 𝐴 ) ∧ 𝑀 ∈ ( 𝑏 𝐼 𝐴 ) ) )