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 ⊢ ( 𝜑 → 𝑋 = 𝑌 )