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={\mathrm{Base}}_G$$
	tg5segofs.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tg5segofs.s	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tg5segofs.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tg5segofs.a	$$⊢\phi \to A\in P$$
	tg5segofs.b	$$⊢\phi \to B\in P$$
	tg5segofs.c	$$⊢\phi \to C\in P$$
	tg5segofs.d	$$⊢\phi \to D\in P$$
	tg5segofs.e	$$⊢\phi \to E\in P$$
	tg5segofs.f	$$⊢\phi \to F\in P$$
	tg5segofs.o	$$⊢O=AFS\left(G\right)$$
	tg5segofs.h	$$⊢\phi \to H\in P$$
	tg5segofs.i	$$⊢\phi \to I\in P$$
	tg5segofs.1	$$⊢\phi \to ⟨⟨A,B⟩,⟨C,D⟩⟩O⟨⟨E,F⟩,⟨H,I⟩⟩$$
	tg5segofs.2	$$⊢\phi \to A\ne B$$
Assertion	tg5segofs	$$⊢\phi \to C\underset{\dot{}}{-}D=H\underset{\dot{}}{-}I$$

Proof

Step	Hyp	Ref	Expression
1		tg5segofs.p	$$⊢P={\mathrm{Base}}_G$$
2		tg5segofs.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		tg5segofs.s	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tg5segofs.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tg5segofs.a	$$⊢\phi \to A\in P$$
6		tg5segofs.b	$$⊢\phi \to B\in P$$
7		tg5segofs.c	$$⊢\phi \to C\in P$$
8		tg5segofs.d	$$⊢\phi \to D\in P$$
9		tg5segofs.e	$$⊢\phi \to E\in P$$
10		tg5segofs.f	$$⊢\phi \to F\in P$$
11		tg5segofs.o	$$⊢O=AFS\left(G\right)$$
12		tg5segofs.h	$$⊢\phi \to H\in P$$
13		tg5segofs.i	$$⊢\phi \to I\in P$$
14		tg5segofs.1	$$⊢\phi \to ⟨⟨A,B⟩,⟨C,D⟩⟩O⟨⟨E,F⟩,⟨H,I⟩⟩$$
15		tg5segofs.2	$$⊢\phi \to A\ne B$$
16	1 2 3 4 11 5 6 7 8 9 10 12 13	brafs	$$⊢\phi \to \left(⟨⟨A,B⟩,⟨C,D⟩⟩O⟨⟨E,F⟩,⟨H,I⟩⟩\leftrightarrow \left(\left(B\in \left(AIC\right)\wedge F\in \left(EIH\right)\right)\wedge \left(A\underset{\dot{}}{-}B=E\underset{\dot{}}{-}F\wedge B\underset{\dot{}}{-}C=F\underset{\dot{}}{-}H\right)\wedge \left(A\underset{\dot{}}{-}D=E\underset{\dot{}}{-}I\wedge B\underset{\dot{}}{-}D=F\underset{\dot{}}{-}I\right)\right)\right)$$
17	14 16	mpbid	$$⊢\phi \to \left(\left(B\in \left(AIC\right)\wedge F\in \left(EIH\right)\right)\wedge \left(A\underset{\dot{}}{-}B=E\underset{\dot{}}{-}F\wedge B\underset{\dot{}}{-}C=F\underset{\dot{}}{-}H\right)\wedge \left(A\underset{\dot{}}{-}D=E\underset{\dot{}}{-}I\wedge B\underset{\dot{}}{-}D=F\underset{\dot{}}{-}I\right)\right)$$
18	17	simp1d	$$⊢\phi \to \left(B\in \left(AIC\right)\wedge F\in \left(EIH\right)\right)$$
19	18	simpld	$$⊢\phi \to B\in \left(AIC\right)$$
20	18	simprd	$$⊢\phi \to F\in \left(EIH\right)$$
21	17	simp2d	$$⊢\phi \to \left(A\underset{\dot{}}{-}B=E\underset{\dot{}}{-}F\wedge B\underset{\dot{}}{-}C=F\underset{\dot{}}{-}H\right)$$
22	21	simpld	$$⊢\phi \to A\underset{\dot{}}{-}B=E\underset{\dot{}}{-}F$$
23	21	simprd	$$⊢\phi \to B\underset{\dot{}}{-}C=F\underset{\dot{}}{-}H$$
24	17	simp3d	$$⊢\phi \to \left(A\underset{\dot{}}{-}D=E\underset{\dot{}}{-}I\wedge B\underset{\dot{}}{-}D=F\underset{\dot{}}{-}I\right)$$
25	24	simpld	$$⊢\phi \to A\underset{\dot{}}{-}D=E\underset{\dot{}}{-}I$$
26	24	simprd	$$⊢\phi \to B\underset{\dot{}}{-}D=F\underset{\dot{}}{-}I$$
27	1 2 3 4 5 6 7 9 10 12 8 13 15 19 20 22 23 25 26	axtg5seg	$$⊢\phi \to C\underset{\dot{}}{-}D=H\underset{\dot{}}{-}I$$