Metamath Proof Explorer


Theorem hlcgreulem

Description: Lemma for hlcgreu . (Contributed by Thierry Arnoux, 9-Aug-2020)

Ref Expression
Hypotheses ishlg.p 𝑃 = ( Base ‘ 𝐺 )
ishlg.i 𝐼 = ( Itv ‘ 𝐺 )
ishlg.k 𝐾 = ( hlG ‘ 𝐺 )
ishlg.a ( 𝜑𝐴𝑃 )
ishlg.b ( 𝜑𝐵𝑃 )
ishlg.c ( 𝜑𝐶𝑃 )
hlln.1 ( 𝜑𝐺 ∈ TarskiG )
hltr.d ( 𝜑𝐷𝑃 )
hlcgrex.m = ( dist ‘ 𝐺 )
hlcgrex.1 ( 𝜑𝐷𝐴 )
hlcgrex.2 ( 𝜑𝐵𝐶 )
hlcgreulem.x ( 𝜑𝑋𝑃 )
hlcgreulem.y ( 𝜑𝑌𝑃 )
hlcgreulem.1 ( 𝜑𝑋 ( 𝐾𝐴 ) 𝐷 )
hlcgreulem.2 ( 𝜑𝑌 ( 𝐾𝐴 ) 𝐷 )
hlcgreulem.3 ( 𝜑 → ( 𝐴 𝑋 ) = ( 𝐵 𝐶 ) )
hlcgreulem.4 ( 𝜑 → ( 𝐴 𝑌 ) = ( 𝐵 𝐶 ) )
Assertion hlcgreulem ( 𝜑𝑋 = 𝑌 )

Proof

Step Hyp Ref Expression
1 ishlg.p 𝑃 = ( Base ‘ 𝐺 )
2 ishlg.i 𝐼 = ( Itv ‘ 𝐺 )
3 ishlg.k 𝐾 = ( hlG ‘ 𝐺 )
4 ishlg.a ( 𝜑𝐴𝑃 )
5 ishlg.b ( 𝜑𝐵𝑃 )
6 ishlg.c ( 𝜑𝐶𝑃 )
7 hlln.1 ( 𝜑𝐺 ∈ TarskiG )
8 hltr.d ( 𝜑𝐷𝑃 )
9 hlcgrex.m = ( dist ‘ 𝐺 )
10 hlcgrex.1 ( 𝜑𝐷𝐴 )
11 hlcgrex.2 ( 𝜑𝐵𝐶 )
12 hlcgreulem.x ( 𝜑𝑋𝑃 )
13 hlcgreulem.y ( 𝜑𝑌𝑃 )
14 hlcgreulem.1 ( 𝜑𝑋 ( 𝐾𝐴 ) 𝐷 )
15 hlcgreulem.2 ( 𝜑𝑌 ( 𝐾𝐴 ) 𝐷 )
16 hlcgreulem.3 ( 𝜑 → ( 𝐴 𝑋 ) = ( 𝐵 𝐶 ) )
17 hlcgreulem.4 ( 𝜑 → ( 𝐴 𝑌 ) = ( 𝐵 𝐶 ) )
18 7 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐺 ∈ TarskiG )
19 4 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐴𝑃 )
20 5 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐵𝑃 )
21 6 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐶𝑃 )
22 simplr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝑦𝑃 )
23 12 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝑋𝑃 )
24 13 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝑌𝑃 )
25 simprr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐴𝑦 )
26 25 necomd ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝑦𝐴 )
27 8 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐷𝑃 )
28 1 2 3 12 8 4 7 14 hlcomd ( 𝜑𝐷 ( 𝐾𝐴 ) 𝑋 )
29 28 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐷 ( 𝐾𝐴 ) 𝑋 )
30 simprl ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) )
31 1 2 3 27 23 22 18 19 29 30 btwnhl ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐴 ∈ ( 𝑋 𝐼 𝑦 ) )
32 1 9 2 18 23 19 22 31 tgbtwncom ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐴 ∈ ( 𝑦 𝐼 𝑋 ) )
33 1 2 3 13 8 4 7 15 hlcomd ( 𝜑𝐷 ( 𝐾𝐴 ) 𝑌 )
34 33 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐷 ( 𝐾𝐴 ) 𝑌 )
35 1 2 3 27 24 22 18 19 34 30 btwnhl ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐴 ∈ ( 𝑌 𝐼 𝑦 ) )
36 1 9 2 18 24 19 22 35 tgbtwncom ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝐴 ∈ ( 𝑦 𝐼 𝑌 ) )
37 16 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → ( 𝐴 𝑋 ) = ( 𝐵 𝐶 ) )
38 17 ad2antrr ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → ( 𝐴 𝑌 ) = ( 𝐵 𝐶 ) )
39 1 9 2 18 19 20 21 22 23 24 26 32 36 37 38 tgsegconeq ( ( ( 𝜑𝑦𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) ) → 𝑋 = 𝑌 )
40 1 fvexi 𝑃 ∈ V
41 40 a1i ( 𝜑𝑃 ∈ V )
42 41 5 6 11 nehash2 ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
43 1 9 2 7 8 4 42 tgbtwndiff ( 𝜑 → ∃ 𝑦𝑃 ( 𝐴 ∈ ( 𝐷 𝐼 𝑦 ) ∧ 𝐴𝑦 ) )
44 39 43 r19.29a ( 𝜑𝑋 = 𝑌 )