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 )