Theorem tgbtwnconn1lem2

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	tgbtwnconn1lem2	$$⊢\phi \to E\underset{\dot{}}{-}F=C\underset{\dot{}}{-}D$$

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 12 13	axtgcgrrflx	$$⊢\phi \to E\underset{\dot{}}{-}F=F\underset{\dot{}}{-}E$$
25	24	adantr	$$⊢\left(\phi \wedge B=C\right)\to E\underset{\dot{}}{-}F=F\underset{\dot{}}{-}E$$
26	3	adantr	$$⊢\left(\phi \wedge B=C\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
27	12	adantr	$$⊢\left(\phi \wedge B=C\right)\to E\in P$$
28	14	adantr	$$⊢\left(\phi \wedge B=C\right)\to H\in P$$
29	6	adantr	$$⊢\left(\phi \wedge B=C\right)\to C\in P$$
30	22	adantr	$$⊢\left(\phi \wedge B=C\right)\to E\underset{\dot{}}{-}H=B\underset{\dot{}}{-}C$$
31		simpr	$$⊢\left(\phi \wedge B=C\right)\to B=C$$
32	31	oveq1d	$$⊢\left(\phi \wedge B=C\right)\to B\underset{\dot{}}{-}C=C\underset{\dot{}}{-}C$$
33	30 32	eqtrd	$$⊢\left(\phi \wedge B=C\right)\to E\underset{\dot{}}{-}H=C\underset{\dot{}}{-}C$$
34	1 11 2 26 27 28 29 33	axtgcgrid	$$⊢\left(\phi \wedge B=C\right)\to E=H$$
35	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	tgbtwnconn1lem1	$$⊢\phi \to H=J$$
36	35	adantr	$$⊢\left(\phi \wedge B=C\right)\to H=J$$
37	34 36	eqtrd	$$⊢\left(\phi \wedge B=C\right)\to E=J$$
38	37	oveq2d	$$⊢\left(\phi \wedge B=C\right)\to F\underset{\dot{}}{-}E=F\underset{\dot{}}{-}J$$
39	23	adantr	$$⊢\left(\phi \wedge B=C\right)\to F\underset{\dot{}}{-}J=B\underset{\dot{}}{-}D$$
40	31	oveq1d	$$⊢\left(\phi \wedge B=C\right)\to B\underset{\dot{}}{-}D=C\underset{\dot{}}{-}D$$
41	38 39 40	3eqtrd	$$⊢\left(\phi \wedge B=C\right)\to F\underset{\dot{}}{-}E=C\underset{\dot{}}{-}D$$
42	25 41	eqtrd	$$⊢\left(\phi \wedge B=C\right)\to E\underset{\dot{}}{-}F=C\underset{\dot{}}{-}D$$
43	3	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
44	13	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to F\in P$$
45	12	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to E\in P$$
46	7	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to D\in P$$
47	6	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to C\in P$$
48	5	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to B\in P$$
49	15	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to J\in P$$
50		simpr	$$⊢\left(\phi \wedge B\ne C\right)\to B\ne C$$
51	1 11 2 3 4 5 6 13 9 17	tgbtwnexch3	$$⊢\phi \to C\in \left(BIF\right)$$
52	51	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to C\in \left(BIF\right)$$
53	35	oveq2d	$$⊢\phi \to AIH=AIJ$$
54	18 53	eleqtrd	$$⊢\phi \to E\in \left(AIJ\right)$$
55	1 11 2 3 4 7 12 15 16 54	tgbtwnexch3	$$⊢\phi \to E\in \left(DIJ\right)$$
56	1 11 2 3 7 12 15 55	tgbtwncom	$$⊢\phi \to E\in \left(JID\right)$$
57	56	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to E\in \left(JID\right)$$
58	35	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to H=J$$
59	58	oveq2d	$$⊢\left(\phi \wedge B\ne C\right)\to E\underset{\dot{}}{-}H=E\underset{\dot{}}{-}J$$
60	22	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to E\underset{\dot{}}{-}H=B\underset{\dot{}}{-}C$$
61	1 11 2 43 45 49	axtgcgrrflx	$$⊢\left(\phi \wedge B\ne C\right)\to E\underset{\dot{}}{-}J=J\underset{\dot{}}{-}E$$
62	59 60 61	3eqtr3d	$$⊢\left(\phi \wedge B\ne C\right)\to B\underset{\dot{}}{-}C=J\underset{\dot{}}{-}E$$
63	21 20	eqtr4d	$$⊢\phi \to C\underset{\dot{}}{-}F=E\underset{\dot{}}{-}D$$
64	63	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to C\underset{\dot{}}{-}F=E\underset{\dot{}}{-}D$$
65	1 11 2 3 4 5 7 12 10 16	tgbtwnexch3	$$⊢\phi \to D\in \left(BIE\right)$$
66	65	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to D\in \left(BIE\right)$$
67	1 11 2 3 4 6 13 15 17 19	tgbtwnexch3	$$⊢\phi \to F\in \left(CIJ\right)$$
68	1 11 2 3 6 13 15 67	tgbtwncom	$$⊢\phi \to F\in \left(JIC\right)$$
69	68	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to F\in \left(JIC\right)$$
70	1 11 2 3 15 13	axtgcgrrflx	$$⊢\phi \to J\underset{\dot{}}{-}F=F\underset{\dot{}}{-}J$$
71	70 23	eqtr2d	$$⊢\phi \to B\underset{\dot{}}{-}D=J\underset{\dot{}}{-}F$$
72	71	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to B\underset{\dot{}}{-}D=J\underset{\dot{}}{-}F$$
73	1 11 2 3 6 13 12 7 63	tgcgrcomlr	$$⊢\phi \to F\underset{\dot{}}{-}C=D\underset{\dot{}}{-}E$$
74	73	adantr	$$⊢\left(\phi \wedge B\ne C\right)\to F\underset{\dot{}}{-}C=D\underset{\dot{}}{-}E$$
75	74	eqcomd	$$⊢\left(\phi \wedge B\ne C\right)\to D\underset{\dot{}}{-}E=F\underset{\dot{}}{-}C$$
76	1 11 2 43 48 46 45 49 44 47 66 69 72 75	tgcgrextend	$$⊢\left(\phi \wedge B\ne C\right)\to B\underset{\dot{}}{-}E=J\underset{\dot{}}{-}C$$
77	1 11 2 43 47 45	axtgcgrrflx	$$⊢\left(\phi \wedge B\ne C\right)\to C\underset{\dot{}}{-}E=E\underset{\dot{}}{-}C$$
78	1 11 2 43 48 47 44 49 45 46 45 47 50 52 57 62 64 76 77	axtg5seg	$$⊢\left(\phi \wedge B\ne C\right)\to F\underset{\dot{}}{-}E=D\underset{\dot{}}{-}C$$
79	1 11 2 43 44 45 46 47 78	tgcgrcomlr	$$⊢\left(\phi \wedge B\ne C\right)\to E\underset{\dot{}}{-}F=C\underset{\dot{}}{-}D$$
80	42 79	pm2.61dane	$$⊢\phi \to E\underset{\dot{}}{-}F=C\underset{\dot{}}{-}D$$