Metamath Proof Explorer


Theorem tg5segofs

Description: Rephrase axtg5seg using the outer five segment predicate. Theorem 2.10 of Schwabhauser p. 28. (Contributed by Thierry Arnoux, 23-Mar-2019)

Ref Expression
Hypotheses tg5segofs.p
|- P = ( Base ` G )
tg5segofs.m
|- .- = ( dist ` G )
tg5segofs.s
|- I = ( Itv ` G )
tg5segofs.g
|- ( ph -> G e. TarskiG )
tg5segofs.a
|- ( ph -> A e. P )
tg5segofs.b
|- ( ph -> B e. P )
tg5segofs.c
|- ( ph -> C e. P )
tg5segofs.d
|- ( ph -> D e. P )
tg5segofs.e
|- ( ph -> E e. P )
tg5segofs.f
|- ( ph -> F e. P )
tg5segofs.o
|- O = ( AFS ` G )
tg5segofs.h
|- ( ph -> H e. P )
tg5segofs.i
|- ( ph -> I e. P )
tg5segofs.1
|- ( ph -> <. <. A , B >. , <. C , D >. >. O <. <. E , F >. , <. H , I >. >. )
tg5segofs.2
|- ( ph -> A =/= B )
Assertion tg5segofs
|- ( ph -> ( C .- D ) = ( H .- I ) )

Proof

Step Hyp Ref Expression
1 tg5segofs.p
 |-  P = ( Base ` G )
2 tg5segofs.m
 |-  .- = ( dist ` G )
3 tg5segofs.s
 |-  I = ( Itv ` G )
4 tg5segofs.g
 |-  ( ph -> G e. TarskiG )
5 tg5segofs.a
 |-  ( ph -> A e. P )
6 tg5segofs.b
 |-  ( ph -> B e. P )
7 tg5segofs.c
 |-  ( ph -> C e. P )
8 tg5segofs.d
 |-  ( ph -> D e. P )
9 tg5segofs.e
 |-  ( ph -> E e. P )
10 tg5segofs.f
 |-  ( ph -> F e. P )
11 tg5segofs.o
 |-  O = ( AFS ` G )
12 tg5segofs.h
 |-  ( ph -> H e. P )
13 tg5segofs.i
 |-  ( ph -> I e. P )
14 tg5segofs.1
 |-  ( ph -> <. <. A , B >. , <. C , D >. >. O <. <. E , F >. , <. H , I >. >. )
15 tg5segofs.2
 |-  ( ph -> A =/= B )
16 1 2 3 4 11 5 6 7 8 9 10 12 13 brafs
 |-  ( ph -> ( <. <. A , B >. , <. C , D >. >. O <. <. E , F >. , <. H , I >. >. <-> ( ( B e. ( A I C ) /\ F e. ( E I H ) ) /\ ( ( A .- B ) = ( E .- F ) /\ ( B .- C ) = ( F .- H ) ) /\ ( ( A .- D ) = ( E .- I ) /\ ( B .- D ) = ( F .- I ) ) ) ) )
17 14 16 mpbid
 |-  ( ph -> ( ( B e. ( A I C ) /\ F e. ( E I H ) ) /\ ( ( A .- B ) = ( E .- F ) /\ ( B .- C ) = ( F .- H ) ) /\ ( ( A .- D ) = ( E .- I ) /\ ( B .- D ) = ( F .- I ) ) ) )
18 17 simp1d
 |-  ( ph -> ( B e. ( A I C ) /\ F e. ( E I H ) ) )
19 18 simpld
 |-  ( ph -> B e. ( A I C ) )
20 18 simprd
 |-  ( ph -> F e. ( E I H ) )
21 17 simp2d
 |-  ( ph -> ( ( A .- B ) = ( E .- F ) /\ ( B .- C ) = ( F .- H ) ) )
22 21 simpld
 |-  ( ph -> ( A .- B ) = ( E .- F ) )
23 21 simprd
 |-  ( ph -> ( B .- C ) = ( F .- H ) )
24 17 simp3d
 |-  ( ph -> ( ( A .- D ) = ( E .- I ) /\ ( B .- D ) = ( F .- I ) ) )
25 24 simpld
 |-  ( ph -> ( A .- D ) = ( E .- I ) )
26 24 simprd
 |-  ( ph -> ( B .- D ) = ( F .- I ) )
27 1 2 3 4 5 6 7 9 10 12 8 13 15 19 20 22 23 25 26 axtg5seg
 |-  ( ph -> ( C .- D ) = ( H .- I ) )