Metamath Proof Explorer


Theorem hlcgreulem

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

Ref Expression
Hypotheses ishlg.p
|- P = ( Base ` G )
ishlg.i
|- I = ( Itv ` G )
ishlg.k
|- K = ( hlG ` G )
ishlg.a
|- ( ph -> A e. P )
ishlg.b
|- ( ph -> B e. P )
ishlg.c
|- ( ph -> C e. P )
hlln.1
|- ( ph -> G e. TarskiG )
hltr.d
|- ( ph -> D e. P )
hlcgrex.m
|- .- = ( dist ` G )
hlcgrex.1
|- ( ph -> D =/= A )
hlcgrex.2
|- ( ph -> B =/= C )
hlcgreulem.x
|- ( ph -> X e. P )
hlcgreulem.y
|- ( ph -> Y e. P )
hlcgreulem.1
|- ( ph -> X ( K ` A ) D )
hlcgreulem.2
|- ( ph -> Y ( K ` A ) D )
hlcgreulem.3
|- ( ph -> ( A .- X ) = ( B .- C ) )
hlcgreulem.4
|- ( ph -> ( A .- Y ) = ( B .- C ) )
Assertion hlcgreulem
|- ( ph -> X = Y )

Proof

Step Hyp Ref Expression
1 ishlg.p
 |-  P = ( Base ` G )
2 ishlg.i
 |-  I = ( Itv ` G )
3 ishlg.k
 |-  K = ( hlG ` G )
4 ishlg.a
 |-  ( ph -> A e. P )
5 ishlg.b
 |-  ( ph -> B e. P )
6 ishlg.c
 |-  ( ph -> C e. P )
7 hlln.1
 |-  ( ph -> G e. TarskiG )
8 hltr.d
 |-  ( ph -> D e. P )
9 hlcgrex.m
 |-  .- = ( dist ` G )
10 hlcgrex.1
 |-  ( ph -> D =/= A )
11 hlcgrex.2
 |-  ( ph -> B =/= C )
12 hlcgreulem.x
 |-  ( ph -> X e. P )
13 hlcgreulem.y
 |-  ( ph -> Y e. P )
14 hlcgreulem.1
 |-  ( ph -> X ( K ` A ) D )
15 hlcgreulem.2
 |-  ( ph -> Y ( K ` A ) D )
16 hlcgreulem.3
 |-  ( ph -> ( A .- X ) = ( B .- C ) )
17 hlcgreulem.4
 |-  ( ph -> ( A .- Y ) = ( B .- C ) )
18 7 ad2antrr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> G e. TarskiG )
19 4 ad2antrr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> A e. P )
20 5 ad2antrr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> B e. P )
21 6 ad2antrr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> C e. P )
22 simplr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> y e. P )
23 12 ad2antrr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> X e. P )
24 13 ad2antrr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> Y e. P )
25 simprr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> A =/= y )
26 25 necomd
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> y =/= A )
27 8 ad2antrr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> D e. P )
28 1 2 3 12 8 4 7 14 hlcomd
 |-  ( ph -> D ( K ` A ) X )
29 28 ad2antrr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> D ( K ` A ) X )
30 simprl
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> A e. ( D I y ) )
31 1 2 3 27 23 22 18 19 29 30 btwnhl
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> A e. ( X I y ) )
32 1 9 2 18 23 19 22 31 tgbtwncom
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> A e. ( y I X ) )
33 1 2 3 13 8 4 7 15 hlcomd
 |-  ( ph -> D ( K ` A ) Y )
34 33 ad2antrr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> D ( K ` A ) Y )
35 1 2 3 27 24 22 18 19 34 30 btwnhl
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> A e. ( Y I y ) )
36 1 9 2 18 24 19 22 35 tgbtwncom
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> A e. ( y I Y ) )
37 16 ad2antrr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> ( A .- X ) = ( B .- C ) )
38 17 ad2antrr
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> ( A .- Y ) = ( B .- C ) )
39 1 9 2 18 19 20 21 22 23 24 26 32 36 37 38 tgsegconeq
 |-  ( ( ( ph /\ y e. P ) /\ ( A e. ( D I y ) /\ A =/= y ) ) -> X = Y )
40 1 fvexi
 |-  P e. _V
41 40 a1i
 |-  ( ph -> P e. _V )
42 41 5 6 11 nehash2
 |-  ( ph -> 2 <_ ( # ` P ) )
43 1 9 2 7 8 4 42 tgbtwndiff
 |-  ( ph -> E. y e. P ( A e. ( D I y ) /\ A =/= y ) )
44 39 43 r19.29a
 |-  ( ph -> X = Y )