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 ) )