Theorem tgbtwnconn1lem1

Description: Lemma for tgbtwnconn1 . (Contributed by Thierry Arnoux, 30-Apr-2019)

	Ref	Expression
Hypotheses	tgbtwnconn1.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgbtwnconn1.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgbtwnconn1.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgbtwnconn1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgbtwnconn1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgbtwnconn1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgbtwnconn1.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	tgbtwnconn1.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	tgbtwnconn1.2	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
	tgbtwnconn1.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
	tgbtwnconn1.m	⊢ − = ( dist ‘ 𝐺 )
	tgbtwnconn1.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	tgbtwnconn1.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	tgbtwnconn1.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
	tgbtwnconn1.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
	tgbtwnconn1.4	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐼 𝐸 ) )
	tgbtwnconn1.5	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐹 ) )
	tgbtwnconn1.6	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐴 𝐼 𝐻 ) )
	tgbtwnconn1.7	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 𝐼 𝐽 ) )
	tgbtwnconn1.8	⊢ ( 𝜑 → ( 𝐸 − 𝐷 ) = ( 𝐶 − 𝐷 ) )
	tgbtwnconn1.9	⊢ ( 𝜑 → ( 𝐶 − 𝐹 ) = ( 𝐶 − 𝐷 ) )
	tgbtwnconn1.10	⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) )
	tgbtwnconn1.11	⊢ ( 𝜑 → ( 𝐹 − 𝐽 ) = ( 𝐵 − 𝐷 ) )
Assertion	tgbtwnconn1lem1	⊢ ( 𝜑 → 𝐻 = 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		tgbtwnconn1.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgbtwnconn1.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tgbtwnconn1.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
4		tgbtwnconn1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5		tgbtwnconn1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6		tgbtwnconn1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7		tgbtwnconn1.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
8		tgbtwnconn1.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
9		tgbtwnconn1.2	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
10		tgbtwnconn1.3	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
11		tgbtwnconn1.m	⊢ − = ( dist ‘ 𝐺 )
12		tgbtwnconn1.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
13		tgbtwnconn1.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
14		tgbtwnconn1.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
15		tgbtwnconn1.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
16		tgbtwnconn1.4	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐼 𝐸 ) )
17		tgbtwnconn1.5	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐹 ) )
18		tgbtwnconn1.6	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐴 𝐼 𝐻 ) )
19		tgbtwnconn1.7	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 𝐼 𝐽 ) )
20		tgbtwnconn1.8	⊢ ( 𝜑 → ( 𝐸 − 𝐷 ) = ( 𝐶 − 𝐷 ) )
21		tgbtwnconn1.9	⊢ ( 𝜑 → ( 𝐶 − 𝐹 ) = ( 𝐶 − 𝐷 ) )
22		tgbtwnconn1.10	⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) )
23		tgbtwnconn1.11	⊢ ( 𝜑 → ( 𝐹 − 𝐽 ) = ( 𝐵 − 𝐷 ) )
24	1 11 2 3 4 5 7 12 10 16	tgbtwnexch	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐸 ) )
25	1 11 2 3 4 5 12 14 24 18	tgbtwnexch	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐻 ) )
26	1 11 2 3 4 5 6 13 9 17	tgbtwnexch	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐹 ) )
27	1 11 2 3 4 5 13 15 26 19	tgbtwnexch	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐽 ) )
28	1 11 2 3 4 5 12 14 24 18	tgbtwnexch3	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐵 𝐼 𝐻 ) )
29	1 11 2 3 4 6 13 15 17 19	tgbtwnexch	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐽 ) )
30	1 11 2 3 4 5 6 15 9 29	tgbtwnexch3	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐽 ) )
31	1 11 2 3 5 6 15 30	tgbtwncom	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐽 𝐼 𝐵 ) )
32	1 11 2 3 4 5 7 12 10 16	tgbtwnexch3	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐵 𝐼 𝐸 ) )
33	1 11 2 3 4 6 13 15 17 19	tgbtwnexch3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 𝐼 𝐽 ) )
34	1 11 2 3 6 13 15 33	tgbtwncom	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 𝐼 𝐶 ) )
35	1 11 2 3 15 13	axtgcgrrflx	⊢ ( 𝜑 → ( 𝐽 − 𝐹 ) = ( 𝐹 − 𝐽 ) )
36	35 23	eqtr2d	⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) = ( 𝐽 − 𝐹 ) )
37	20 21	eqtr4d	⊢ ( 𝜑 → ( 𝐸 − 𝐷 ) = ( 𝐶 − 𝐹 ) )
38	1 11 2 3 12 7 6 13 37	tgcgrcomlr	⊢ ( 𝜑 → ( 𝐷 − 𝐸 ) = ( 𝐹 − 𝐶 ) )
39	1 11 2 3 5 7 12 15 13 6 32 34 36 38	tgcgrextend	⊢ ( 𝜑 → ( 𝐵 − 𝐸 ) = ( 𝐽 − 𝐶 ) )
40	1 11 2 3 12 14 5 6 22	tgcgrcomr	⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐶 − 𝐵 ) )
41	1 11 2 3 5 12 14 15 6 5 28 31 39 40	tgcgrextend	⊢ ( 𝜑 → ( 𝐵 − 𝐻 ) = ( 𝐽 − 𝐵 ) )
42	1 11 2 3 5 15	axtgcgrrflx	⊢ ( 𝜑 → ( 𝐵 − 𝐽 ) = ( 𝐽 − 𝐵 ) )
43	1 11 2 3 5 15 5 4 14 15 8 25 27 41 42	tgsegconeq	⊢ ( 𝜑 → 𝐻 = 𝐽 )