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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tg5segofs.m	⊢ − = ( dist ‘ 𝐺 )
	tg5segofs.s	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tg5segofs.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tg5segofs.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tg5segofs.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tg5segofs.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tg5segofs.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	tg5segofs.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	tg5segofs.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	tg5segofs.o	⊢ 𝑂 = ( AFS ‘ 𝐺 )
	tg5segofs.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
	tg5segofs.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑃 )
	tg5segofs.1	⊢ ( 𝜑 → ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ 𝑂 ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐻 , 𝐼 ⟩ ⟩ )
	tg5segofs.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion	tg5segofs	⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) = ( 𝐻 − 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		tg5segofs.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tg5segofs.m	⊢ − = ( dist ‘ 𝐺 )
3		tg5segofs.s	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tg5segofs.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tg5segofs.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		tg5segofs.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		tg5segofs.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		tg5segofs.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		tg5segofs.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10		tg5segofs.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11		tg5segofs.o	⊢ 𝑂 = ( AFS ‘ 𝐺 )
12		tg5segofs.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
13		tg5segofs.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑃 )
14		tg5segofs.1	⊢ ( 𝜑 → ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ 𝑂 ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐻 , 𝐼 ⟩ ⟩ )
15		tg5segofs.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
16	1 2 3 4 11 5 6 7 8 9 10 12 13	brafs	⊢ ( 𝜑 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ ⟩ 𝑂 ⟨ ⟨ 𝐸 , 𝐹 ⟩ , ⟨ 𝐻 , 𝐼 ⟩ ⟩ ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝐹 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝐹 − 𝐻 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝐸 − 𝐼 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐼 ) ) ) ) )
17	14 16	mpbid	⊢ ( 𝜑 → ( ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) ∧ ( ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝐹 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝐹 − 𝐻 ) ) ∧ ( ( 𝐴 − 𝐷 ) = ( 𝐸 − 𝐼 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐼 ) ) ) )
18	17	simp1d	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) )
19	18	simpld	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
20	18	simprd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) )
21	17	simp2d	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝐹 ) ∧ ( 𝐵 − 𝐶 ) = ( 𝐹 − 𝐻 ) ) )
22	21	simpld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐸 − 𝐹 ) )
23	21	simprd	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐹 − 𝐻 ) )
24	17	simp3d	⊢ ( 𝜑 → ( ( 𝐴 − 𝐷 ) = ( 𝐸 − 𝐼 ) ∧ ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐼 ) ) )
25	24	simpld	⊢ ( 𝜑 → ( 𝐴 − 𝐷 ) = ( 𝐸 − 𝐼 ) )
26	24	simprd	⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) = ( 𝐹 − 𝐼 ) )
27	1 2 3 4 5 6 7 9 10 12 8 13 15 19 20 22 23 25 26	axtg5seg	⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) = ( 𝐻 − 𝐼 ) )