Metamath Proof Explorer

Theorem symquadlem

Description: Lemma of the symmetrical quadrilateral. The diagonals of quadrilaterals with congruent opposing sides intersect at their middle point. In Euclidean geometry, such quadrilaterals are called parallelograms, as opposing sides are parallel. However, this is not necessarily true in the case of absolute geometry. Lemma 7.21 of Schwabhauser p. 52. (Contributed by Thierry Arnoux, 6-Aug-2019)

Ref Expression
Hypotheses mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirval.d ⊢ − = ( dist ‘ 𝐺 )
mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
symquadlem.m ⊢ 𝑀 = ( 𝑆 ‘ 𝑋 )
symquadlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
symquadlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
symquadlem.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
symquadlem.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
symquadlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
symquadlem.1 ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
symquadlem.2 ⊢ ( 𝜑 → 𝐵 ≠ 𝐷 )
symquadlem.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )
symquadlem.4 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐷 − 𝐴 ) )
symquadlem.5 ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
symquadlem.6 ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐵 𝐿 𝐷 ) ∨ 𝐵 = 𝐷 ) )
Assertion symquadlem ( 𝜑 → 𝐴 = ( 𝑀 ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 mirval.d ⊢ − = ( dist ‘ 𝐺 )
3 mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6 mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 symquadlem.m ⊢ 𝑀 = ( 𝑆 ‘ 𝑋 )
8 symquadlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
9 symquadlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
10 symquadlem.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
11 symquadlem.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
12 symquadlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
13 symquadlem.1 ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
14 symquadlem.2 ⊢ ( 𝜑 → 𝐵 ≠ 𝐷 )
15 symquadlem.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )
16 symquadlem.4 ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐷 − 𝐴 ) )
17 symquadlem.5 ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
18 symquadlem.6 ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐵 𝐿 𝐷 ) ∨ 𝐵 = 𝐷 ) )
19 1 2 3 6 9 8 tgbtwntriv2 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 𝐼 𝐴 ) )
20 1 4 3 6 9 8 8 19 btwncolg1 ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐴 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
22 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐶 )
23 22 oveq2d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐵 𝐿 𝐴 ) = ( 𝐵 𝐿 𝐶 ) )
24 23 eleq2d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐴 ∈ ( 𝐵 𝐿 𝐴 ) ↔ 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ) )
25 22 eqeq2d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐵 = 𝐴 ↔ 𝐵 = 𝐶 ) )
26 24 25 orbi12d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( ( 𝐴 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ↔ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) ) )
27 21 26 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
28 13 27 mtand ⊢ ( 𝜑 → ¬ 𝐴 = 𝐶 )
29 28 neqned ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
30 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝐴 ≠ 𝐶 )
31 30 necomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝐶 ≠ 𝐴 )
32 31 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ¬ 𝐶 = 𝐴 )
33 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝐺 ∈ TarskiG )
34 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝐶 ∈ 𝑃 )
35 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝐴 ∈ 𝑃 )
36 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝑋 ∈ 𝑃 )
37 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
38 1 4 3 33 35 34 36 37 colcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝑋 ∈ ( 𝐶 𝐿 𝐴 ) ∨ 𝐶 = 𝐴 ) )
39 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝐵 ∈ 𝑃 )
40 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝐷 ∈ 𝑃 )
41 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
42 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝑥 ∈ 𝑃 )
43 1 4 3 6 9 11 12 18 colrot2 ⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝑋 𝐿 𝐵 ) ∨ 𝑋 = 𝐵 ) )
44 1 4 3 6 12 9 11 43 colcom ⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐵 𝐿 𝑋 ) ∨ 𝐵 = 𝑋 ) )
45 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝐷 ∈ ( 𝐵 𝐿 𝑋 ) ∨ 𝐵 = 𝑋 ) )
46 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ )
47 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝐵 − 𝐶 ) = ( 𝐷 − 𝐴 ) )
48 1 2 3 6 8 9 10 11 15 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝐷 − 𝐶 ) )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝐵 − 𝐴 ) = ( 𝐷 − 𝐶 ) )
50 49 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝐷 − 𝐶 ) = ( 𝐵 − 𝐴 ) )
51 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝐵 ≠ 𝐷 )
52 1 4 3 33 39 40 36 41 40 39 2 34 42 35 45 46 47 50 51 tgfscgr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝑋 − 𝐶 ) = ( 𝑥 − 𝐴 ) )
53 1 4 3 6 9 10 8 13 ncolcom ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) )
54 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) )
55 17 orcomd ⊢ ( 𝜑 → ( 𝐴 = 𝐶 ∨ 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) )
56 55 ord ⊢ ( 𝜑 → ( ¬ 𝐴 = 𝐶 → 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ) )
57 28 56 mpd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) )
58 57 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) )
59 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ¬ 𝐴 = 𝐶 )
60 47 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝐷 − 𝐴 ) = ( 𝐵 − 𝐶 ) )
61 1 4 3 33 39 40 36 41 40 39 2 35 42 34 45 46 49 60 51 tgfscgr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝑋 − 𝐴 ) = ( 𝑥 − 𝐶 ) )
62 1 2 3 33 36 35 42 34 61 tgcgrcomlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝐴 − 𝑋 ) = ( 𝐶 − 𝑥 ) )
63 1 2 3 33 34 35 axtgcgrrflx ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝐶 − 𝐴 ) = ( 𝐴 − 𝐶 ) )
64 1 2 41 33 35 36 34 34 42 35 62 52 63 trgcgr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ⟨“ 𝐴 𝑋 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝑥 𝐴 ”⟩ )
65 1 4 3 33 35 36 34 41 34 42 35 37 64 lnxfr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝑥 ∈ ( 𝐶 𝐿 𝐴 ) ∨ 𝐶 = 𝐴 ) )
66 1 4 3 33 34 35 42 65 colcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝑥 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
67 66 orcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝐴 = 𝐶 ∨ 𝑥 ∈ ( 𝐴 𝐿 𝐶 ) ) )
68 67 ord ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( ¬ 𝐴 = 𝐶 → 𝑥 ∈ ( 𝐴 𝐿 𝐶 ) ) )
69 59 68 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝑥 ∈ ( 𝐴 𝐿 𝐶 ) )
70 14 neneqd ⊢ ( 𝜑 → ¬ 𝐵 = 𝐷 )
71 18 orcomd ⊢ ( 𝜑 → ( 𝐵 = 𝐷 ∨ 𝑋 ∈ ( 𝐵 𝐿 𝐷 ) ) )
72 71 ord ⊢ ( 𝜑 → ( ¬ 𝐵 = 𝐷 → 𝑋 ∈ ( 𝐵 𝐿 𝐷 ) ) )
73 70 72 mpd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 𝐿 𝐷 ) )
74 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝑋 ∈ ( 𝐵 𝐿 𝐷 ) )
75 70 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ¬ 𝐵 = 𝐷 )
76 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝑋 ∈ ( 𝐵 𝐿 𝐷 ) ∨ 𝐵 = 𝐷 ) )
77 1 2 3 41 33 39 40 36 40 39 42 46 cgr3swap23 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ⟨“ 𝐵 𝑋 𝐷 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝑥 𝐵 ”⟩ )
78 1 4 3 33 39 36 40 41 40 42 39 76 77 lnxfr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝑥 ∈ ( 𝐷 𝐿 𝐵 ) ∨ 𝐷 = 𝐵 ) )
79 1 4 3 33 40 39 42 78 colcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝑥 ∈ ( 𝐵 𝐿 𝐷 ) ∨ 𝐵 = 𝐷 ) )
80 79 orcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝐵 = 𝐷 ∨ 𝑥 ∈ ( 𝐵 𝐿 𝐷 ) ) )
81 80 ord ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( ¬ 𝐵 = 𝐷 → 𝑥 ∈ ( 𝐵 𝐿 𝐷 ) ) )
82 75 81 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝑥 ∈ ( 𝐵 𝐿 𝐷 ) )
83 1 3 4 33 35 34 39 40 54 58 69 74 82 tglineinteq ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝑋 = 𝑥 )
84 83 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝑋 − 𝐴 ) = ( 𝑥 − 𝐴 ) )
85 52 84 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝑋 − 𝐶 ) = ( 𝑋 − 𝐴 ) )
86 1 2 3 4 5 33 7 34 35 36 38 85 colmid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝐴 = ( 𝑀 ‘ 𝐶 ) ∨ 𝐶 = 𝐴 ) )
87 86 orcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( 𝐶 = 𝐴 ∨ 𝐴 = ( 𝑀 ‘ 𝐶 ) ) )
88 87 ord ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → ( ¬ 𝐶 = 𝐴 → 𝐴 = ( 𝑀 ‘ 𝐶 ) ) )
89 32 88 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ ) → 𝐴 = ( 𝑀 ‘ 𝐶 ) )
90 1 2 3 6 9 11 axtgcgrrflx ⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) = ( 𝐷 − 𝐵 ) )
91 1 4 3 6 9 11 12 41 11 9 2 44 90 lnext ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ⟨“ 𝐵 𝐷 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝑥 ”⟩ )
92 89 91 r19.29a ⊢ ( 𝜑 → 𝐴 = ( 𝑀 ‘ 𝐶 ) )