Theorem tgbtwnconn1lem2

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	tgbtwnconn1lem2	⊢ ( 𝜑 → ( 𝐸 − 𝐹 ) = ( 𝐶 − 𝐷 ) )

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 12 13	axtgcgrrflx	⊢ ( 𝜑 → ( 𝐸 − 𝐹 ) = ( 𝐹 − 𝐸 ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐸 − 𝐹 ) = ( 𝐹 − 𝐸 ) )
26	3	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐺 ∈ TarskiG )
27	12	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐸 ∈ 𝑃 )
28	14	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐻 ∈ 𝑃 )
29	6	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐶 ∈ 𝑃 )
30	22	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) )
31		simpr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐵 = 𝐶 )
32	31	oveq1d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐵 − 𝐶 ) = ( 𝐶 − 𝐶 ) )
33	30 32	eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐸 − 𝐻 ) = ( 𝐶 − 𝐶 ) )
34	1 11 2 26 27 28 29 33	axtgcgrid	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐸 = 𝐻 )
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	⊢ ( 𝜑 → 𝐻 = 𝐽 )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐻 = 𝐽 )
37	34 36	eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐸 = 𝐽 )
38	37	oveq2d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐹 − 𝐸 ) = ( 𝐹 − 𝐽 ) )
39	23	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐹 − 𝐽 ) = ( 𝐵 − 𝐷 ) )
40	31	oveq1d	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐵 − 𝐷 ) = ( 𝐶 − 𝐷 ) )
41	38 39 40	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐹 − 𝐸 ) = ( 𝐶 − 𝐷 ) )
42	25 41	eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐸 − 𝐹 ) = ( 𝐶 − 𝐷 ) )
43	3	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
44	13	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐹 ∈ 𝑃 )
45	12	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐸 ∈ 𝑃 )
46	7	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐷 ∈ 𝑃 )
47	6	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
48	5	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ∈ 𝑃 )
49	15	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐽 ∈ 𝑃 )
50		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ≠ 𝐶 )
51	1 11 2 3 4 5 6 13 9 17	tgbtwnexch3	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐹 ) )
52	51	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ∈ ( 𝐵 𝐼 𝐹 ) )
53	35	oveq2d	⊢ ( 𝜑 → ( 𝐴 𝐼 𝐻 ) = ( 𝐴 𝐼 𝐽 ) )
54	18 53	eleqtrd	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐴 𝐼 𝐽 ) )
55	1 11 2 3 4 7 12 15 16 54	tgbtwnexch3	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐽 ) )
56	1 11 2 3 7 12 15 55	tgbtwncom	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐽 𝐼 𝐷 ) )
57	56	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐸 ∈ ( 𝐽 𝐼 𝐷 ) )
58	35	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐻 = 𝐽 )
59	58	oveq2d	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐸 − 𝐻 ) = ( 𝐸 − 𝐽 ) )
60	22	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) )
61	1 11 2 43 45 49	axtgcgrrflx	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐸 − 𝐽 ) = ( 𝐽 − 𝐸 ) )
62	59 60 61	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 − 𝐶 ) = ( 𝐽 − 𝐸 ) )
63	21 20	eqtr4d	⊢ ( 𝜑 → ( 𝐶 − 𝐹 ) = ( 𝐸 − 𝐷 ) )
64	63	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐶 − 𝐹 ) = ( 𝐸 − 𝐷 ) )
65	1 11 2 3 4 5 7 12 10 16	tgbtwnexch3	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐵 𝐼 𝐸 ) )
66	65	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐷 ∈ ( 𝐵 𝐼 𝐸 ) )
67	1 11 2 3 4 6 13 15 17 19	tgbtwnexch3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 𝐼 𝐽 ) )
68	1 11 2 3 6 13 15 67	tgbtwncom	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 𝐼 𝐶 ) )
69	68	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → 𝐹 ∈ ( 𝐽 𝐼 𝐶 ) )
70	1 11 2 3 15 13	axtgcgrrflx	⊢ ( 𝜑 → ( 𝐽 − 𝐹 ) = ( 𝐹 − 𝐽 ) )
71	70 23	eqtr2d	⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) = ( 𝐽 − 𝐹 ) )
72	71	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 − 𝐷 ) = ( 𝐽 − 𝐹 ) )
73	1 11 2 3 6 13 12 7 63	tgcgrcomlr	⊢ ( 𝜑 → ( 𝐹 − 𝐶 ) = ( 𝐷 − 𝐸 ) )
74	73	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐹 − 𝐶 ) = ( 𝐷 − 𝐸 ) )
75	74	eqcomd	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐷 − 𝐸 ) = ( 𝐹 − 𝐶 ) )
76	1 11 2 43 48 46 45 49 44 47 66 69 72 75	tgcgrextend	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 − 𝐸 ) = ( 𝐽 − 𝐶 ) )
77	1 11 2 43 47 45	axtgcgrrflx	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐶 − 𝐸 ) = ( 𝐸 − 𝐶 ) )
78	1 11 2 43 48 47 44 49 45 46 45 47 50 52 57 62 64 76 77	axtg5seg	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐹 − 𝐸 ) = ( 𝐷 − 𝐶 ) )
79	1 11 2 43 44 45 46 47 78	tgcgrcomlr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ 𝐶 ) → ( 𝐸 − 𝐹 ) = ( 𝐶 − 𝐷 ) )
80	42 79	pm2.61dane	⊢ ( 𝜑 → ( 𝐸 − 𝐹 ) = ( 𝐶 − 𝐷 ) )