Theorem tgbtwnconn1lem1

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

	Ref	Expression
Hypotheses	tgbtwnconn1.p	$$⊢P={\mathrm{Base}}_G$$
	tgbtwnconn1.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tgbtwnconn1.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tgbtwnconn1.a	$$⊢\phi \to A\in P$$
	tgbtwnconn1.b	$$⊢\phi \to B\in P$$
	tgbtwnconn1.c	$$⊢\phi \to C\in P$$
	tgbtwnconn1.d	$$⊢\phi \to D\in P$$
	tgbtwnconn1.1	$$⊢\phi \to A\ne B$$
	tgbtwnconn1.2	$$⊢\phi \to B\in \left(AIC\right)$$
	tgbtwnconn1.3	$$⊢\phi \to B\in \left(AID\right)$$
	tgbtwnconn1.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tgbtwnconn1.e	$$⊢\phi \to E\in P$$
	tgbtwnconn1.f	$$⊢\phi \to F\in P$$
	tgbtwnconn1.h	$$⊢\phi \to H\in P$$
	tgbtwnconn1.j	$$⊢\phi \to J\in P$$
	tgbtwnconn1.4	$$⊢\phi \to D\in \left(AIE\right)$$
	tgbtwnconn1.5	$$⊢\phi \to C\in \left(AIF\right)$$
	tgbtwnconn1.6	$$⊢\phi \to E\in \left(AIH\right)$$
	tgbtwnconn1.7	$$⊢\phi \to F\in \left(AIJ\right)$$
	tgbtwnconn1.8	$$⊢\phi \to E\underset{\dot{}}{-}D=C\underset{\dot{}}{-}D$$
	tgbtwnconn1.9	$$⊢\phi \to C\underset{\dot{}}{-}F=C\underset{\dot{}}{-}D$$
	tgbtwnconn1.10	$$⊢\phi \to E\underset{\dot{}}{-}H=B\underset{\dot{}}{-}C$$
	tgbtwnconn1.11	$$⊢\phi \to F\underset{\dot{}}{-}J=B\underset{\dot{}}{-}D$$
Assertion	tgbtwnconn1lem1	$$⊢\phi \to H=J$$

Proof

Step	Hyp	Ref	Expression
1		tgbtwnconn1.p	$$⊢P={\mathrm{Base}}_G$$
2		tgbtwnconn1.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		tgbtwnconn1.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
4		tgbtwnconn1.a	$$⊢\phi \to A\in P$$
5		tgbtwnconn1.b	$$⊢\phi \to B\in P$$
6		tgbtwnconn1.c	$$⊢\phi \to C\in P$$
7		tgbtwnconn1.d	$$⊢\phi \to D\in P$$
8		tgbtwnconn1.1	$$⊢\phi \to A\ne B$$
9		tgbtwnconn1.2	$$⊢\phi \to B\in \left(AIC\right)$$
10		tgbtwnconn1.3	$$⊢\phi \to B\in \left(AID\right)$$
11		tgbtwnconn1.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
12		tgbtwnconn1.e	$$⊢\phi \to E\in P$$
13		tgbtwnconn1.f	$$⊢\phi \to F\in P$$
14		tgbtwnconn1.h	$$⊢\phi \to H\in P$$
15		tgbtwnconn1.j	$$⊢\phi \to J\in P$$
16		tgbtwnconn1.4	$$⊢\phi \to D\in \left(AIE\right)$$
17		tgbtwnconn1.5	$$⊢\phi \to C\in \left(AIF\right)$$
18		tgbtwnconn1.6	$$⊢\phi \to E\in \left(AIH\right)$$
19		tgbtwnconn1.7	$$⊢\phi \to F\in \left(AIJ\right)$$
20		tgbtwnconn1.8	$$⊢\phi \to E\underset{\dot{}}{-}D=C\underset{\dot{}}{-}D$$
21		tgbtwnconn1.9	$$⊢\phi \to C\underset{\dot{}}{-}F=C\underset{\dot{}}{-}D$$
22		tgbtwnconn1.10	$$⊢\phi \to E\underset{\dot{}}{-}H=B\underset{\dot{}}{-}C$$
23		tgbtwnconn1.11	$$⊢\phi \to F\underset{\dot{}}{-}J=B\underset{\dot{}}{-}D$$
24	1 11 2 3 4 5 7 12 10 16	tgbtwnexch	$$⊢\phi \to B\in \left(AIE\right)$$
25	1 11 2 3 4 5 12 14 24 18	tgbtwnexch	$$⊢\phi \to B\in \left(AIH\right)$$
26	1 11 2 3 4 5 6 13 9 17	tgbtwnexch	$$⊢\phi \to B\in \left(AIF\right)$$
27	1 11 2 3 4 5 13 15 26 19	tgbtwnexch	$$⊢\phi \to B\in \left(AIJ\right)$$
28	1 11 2 3 4 5 12 14 24 18	tgbtwnexch3	$$⊢\phi \to E\in \left(BIH\right)$$
29	1 11 2 3 4 6 13 15 17 19	tgbtwnexch	$$⊢\phi \to C\in \left(AIJ\right)$$
30	1 11 2 3 4 5 6 15 9 29	tgbtwnexch3	$$⊢\phi \to C\in \left(BIJ\right)$$
31	1 11 2 3 5 6 15 30	tgbtwncom	$$⊢\phi \to C\in \left(JIB\right)$$
32	1 11 2 3 4 5 7 12 10 16	tgbtwnexch3	$$⊢\phi \to D\in \left(BIE\right)$$
33	1 11 2 3 4 6 13 15 17 19	tgbtwnexch3	$$⊢\phi \to F\in \left(CIJ\right)$$
34	1 11 2 3 6 13 15 33	tgbtwncom	$$⊢\phi \to F\in \left(JIC\right)$$
35	1 11 2 3 15 13	axtgcgrrflx	$$⊢\phi \to J\underset{\dot{}}{-}F=F\underset{\dot{}}{-}J$$
36	35 23	eqtr2d	$$⊢\phi \to B\underset{\dot{}}{-}D=J\underset{\dot{}}{-}F$$
37	20 21	eqtr4d	$$⊢\phi \to E\underset{\dot{}}{-}D=C\underset{\dot{}}{-}F$$
38	1 11 2 3 12 7 6 13 37	tgcgrcomlr	$$⊢\phi \to D\underset{\dot{}}{-}E=F\underset{\dot{}}{-}C$$
39	1 11 2 3 5 7 12 15 13 6 32 34 36 38	tgcgrextend	$$⊢\phi \to B\underset{\dot{}}{-}E=J\underset{\dot{}}{-}C$$
40	1 11 2 3 12 14 5 6 22	tgcgrcomr	$$⊢\phi \to E\underset{\dot{}}{-}H=C\underset{\dot{}}{-}B$$
41	1 11 2 3 5 12 14 15 6 5 28 31 39 40	tgcgrextend	$$⊢\phi \to B\underset{\dot{}}{-}H=J\underset{\dot{}}{-}B$$
42	1 11 2 3 5 15	axtgcgrrflx	$$⊢\phi \to B\underset{\dot{}}{-}J=J\underset{\dot{}}{-}B$$
43	1 11 2 3 5 15 5 4 14 15 8 25 27 41 42	tgsegconeq	$$⊢\phi \to H=J$$