Metamath Proof Explorer

Theorem tgbtwnxfr

Description: A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of Schwabhauser p. 36. (Contributed by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Hypotheses tgcgrxfr.p 
|- P = ( Base ` G )
tgcgrxfr.m 
|- .- = ( dist ` G )
tgcgrxfr.i 
|- I = ( Itv ` G )
tgcgrxfr.r 
|- .~ = ( cgrG ` G )
tgcgrxfr.g 
|- ( ph -> G e. TarskiG )
tgbtwnxfr.a 
|- ( ph -> A e. P )
tgbtwnxfr.b 
|- ( ph -> B e. P )
tgbtwnxfr.c 
|- ( ph -> C e. P )
tgbtwnxfr.d 
|- ( ph -> D e. P )
tgbtwnxfr.e 
|- ( ph -> E e. P )
tgbtwnxfr.f 
|- ( ph -> F e. P )
tgbtwnxfr.2 
|- ( ph -> <" A B C "> .~ <" D E F "> )
tgbtwnxfr.1 
|- ( ph -> B e. ( A I C ) )
Assertion tgbtwnxfr 
|- ( ph -> E e. ( D I F ) )

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p 
 |-  P = ( Base ` G )
2 tgcgrxfr.m 
 |-  .- = ( dist ` G )
3 tgcgrxfr.i 
 |-  I = ( Itv ` G )
4 tgcgrxfr.r 
 |-  .~ = ( cgrG ` G )
5 tgcgrxfr.g 
 |-  ( ph -> G e. TarskiG )
6 tgbtwnxfr.a 
 |-  ( ph -> A e. P )
7 tgbtwnxfr.b 
 |-  ( ph -> B e. P )
8 tgbtwnxfr.c 
 |-  ( ph -> C e. P )
9 tgbtwnxfr.d 
 |-  ( ph -> D e. P )
10 tgbtwnxfr.e 
 |-  ( ph -> E e. P )
11 tgbtwnxfr.f 
 |-  ( ph -> F e. P )
12 tgbtwnxfr.2 
 |-  ( ph -> <" A B C "> .~ <" D E F "> )
13 tgbtwnxfr.1 
 |-  ( ph -> B e. ( A I C ) )
14 5 ad2antrr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> G e. TarskiG )
15 simplr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> e e. P )
16 10 ad2antrr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> E e. P )
17 9 ad2antrr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> D e. P )
18 11 ad2antrr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> F e. P )
19 simprl 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> e e. ( D I F ) )
20 eqidd 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> ( D .- F ) = ( D .- F ) )
21 eqidd 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> ( e .- F ) = ( e .- F ) )
22 6 ad2antrr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> A e. P )
23 7 ad2antrr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> B e. P )
24 8 ad2antrr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> C e. P )
25 simprr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> <" A B C "> .~ <" D e F "> )
26 1 2 3 4 14 22 23 24 17 15 18 25 trgcgrcom 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> <" D e F "> .~ <" A B C "> )
27 12 ad2antrr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> <" A B C "> .~ <" D E F "> )
28 1 2 3 4 14 17 15 18 22 23 24 26 17 16 18 27 cgr3tr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> <" D e F "> .~ <" D E F "> )
29 1 2 3 4 14 17 15 18 17 16 18 28 trgcgrcom 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> <" D E F "> .~ <" D e F "> )
30 1 2 3 4 14 17 16 18 17 15 18 29 cgr3simp1 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> ( D .- E ) = ( D .- e ) )
31 1 2 3 4 14 17 16 18 17 15 18 29 cgr3simp2 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> ( E .- F ) = ( e .- F ) )
32 1 2 3 14 16 18 15 18 31 tgcgrcomlr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> ( F .- E ) = ( F .- e ) )
33 1 2 3 14 17 15 18 16 17 15 18 15 19 19 20 21 30 32 tgifscgr 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> ( e .- E ) = ( e .- e ) )
34 1 2 3 14 15 16 15 33 axtgcgrid 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> e = E )
35 34 19 eqeltrrd 
 |-  ( ( ( ph /\ e e. P ) /\ ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) -> E e. ( D I F ) )
36 1 2 3 4 5 6 7 8 9 10 11 12 cgr3simp3 
 |-  ( ph -> ( C .- A ) = ( F .- D ) )
37 1 2 3 5 8 6 11 9 36 tgcgrcomlr 
 |-  ( ph -> ( A .- C ) = ( D .- F ) )
38 1 2 3 4 5 6 7 8 9 11 13 37 tgcgrxfr 
 |-  ( ph -> E. e e. P ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) )
39 35 38 r19.29a 
 |-  ( ph -> E e. ( D I F ) )