Theorem tgcgrextend

Description: Link congruence over a pair of line segments. Theorem 2.11 of Schwabhauser p. 29. (Contributed by Thierry Arnoux, 23-Mar-2019) (Shortened by David A. Wheeler and Thierry Arnoux, 22-Apr-2020.)

	Ref	Expression
Hypotheses	tkgeom.p	$$⊢P={\mathrm{Base}}_G$$
	tkgeom.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tkgeom.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tkgeom.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tgcgrextend.a	$$⊢\phi \to A\in P$$
	tgcgrextend.b	$$⊢\phi \to B\in P$$
	tgcgrextend.c	$$⊢\phi \to C\in P$$
	tgcgrextend.d	$$⊢\phi \to D\in P$$
	tgcgrextend.e	$$⊢\phi \to E\in P$$
	tgcgrextend.f	$$⊢\phi \to F\in P$$
	tgcgrextend.1	$$⊢\phi \to B\in \left(AIC\right)$$
	tgcgrextend.2	$$⊢\phi \to E\in \left(DIF\right)$$
	tgcgrextend.3	$$⊢\phi \to A\underset{\dot{}}{-}B=D\underset{\dot{}}{-}E$$
	tgcgrextend.4	$$⊢\phi \to B\underset{\dot{}}{-}C=E\underset{\dot{}}{-}F$$
Assertion	tgcgrextend	$$⊢\phi \to A\underset{\dot{}}{-}C=D\underset{\dot{}}{-}F$$

Proof

Step	Hyp	Ref	Expression
1		tkgeom.p	$$⊢P={\mathrm{Base}}_G$$
2		tkgeom.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		tkgeom.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tkgeom.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tgcgrextend.a	$$⊢\phi \to A\in P$$
6		tgcgrextend.b	$$⊢\phi \to B\in P$$
7		tgcgrextend.c	$$⊢\phi \to C\in P$$
8		tgcgrextend.d	$$⊢\phi \to D\in P$$
9		tgcgrextend.e	$$⊢\phi \to E\in P$$
10		tgcgrextend.f	$$⊢\phi \to F\in P$$
11		tgcgrextend.1	$$⊢\phi \to B\in \left(AIC\right)$$
12		tgcgrextend.2	$$⊢\phi \to E\in \left(DIF\right)$$
13		tgcgrextend.3	$$⊢\phi \to A\underset{\dot{}}{-}B=D\underset{\dot{}}{-}E$$
14		tgcgrextend.4	$$⊢\phi \to B\underset{\dot{}}{-}C=E\underset{\dot{}}{-}F$$
15	14	adantr	$$⊢\left(\phi \wedge A=B\right)\to B\underset{\dot{}}{-}C=E\underset{\dot{}}{-}F$$
16		simpr	$$⊢\left(\phi \wedge A=B\right)\to A=B$$
17	16	oveq1d	$$⊢\left(\phi \wedge A=B\right)\to A\underset{\dot{}}{-}C=B\underset{\dot{}}{-}C$$
18	4	adantr	$$⊢\left(\phi \wedge A=B\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
19	5	adantr	$$⊢\left(\phi \wedge A=B\right)\to A\in P$$
20	6	adantr	$$⊢\left(\phi \wedge A=B\right)\to B\in P$$
21	8	adantr	$$⊢\left(\phi \wedge A=B\right)\to D\in P$$
22	9	adantr	$$⊢\left(\phi \wedge A=B\right)\to E\in P$$
23	13	adantr	$$⊢\left(\phi \wedge A=B\right)\to A\underset{\dot{}}{-}B=D\underset{\dot{}}{-}E$$
24	1 2 3 18 19 20 21 22 23 16	tgcgreq	$$⊢\left(\phi \wedge A=B\right)\to D=E$$
25	24	oveq1d	$$⊢\left(\phi \wedge A=B\right)\to D\underset{\dot{}}{-}F=E\underset{\dot{}}{-}F$$
26	15 17 25	3eqtr4d	$$⊢\left(\phi \wedge A=B\right)\to A\underset{\dot{}}{-}C=D\underset{\dot{}}{-}F$$
27	4	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
28	7	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to C\in P$$
29	5	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to A\in P$$
30	10	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to F\in P$$
31	8	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to D\in P$$
32	6	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to B\in P$$
33	9	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to E\in P$$
34		simpr	$$⊢\left(\phi \wedge A\ne B\right)\to A\ne B$$
35	11	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to B\in \left(AIC\right)$$
36	12	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to E\in \left(DIF\right)$$
37	13	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to A\underset{\dot{}}{-}B=D\underset{\dot{}}{-}E$$
38	14	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to B\underset{\dot{}}{-}C=E\underset{\dot{}}{-}F$$
39	1 2 3 27 29 31	tgcgrtriv	$$⊢\left(\phi \wedge A\ne B\right)\to A\underset{\dot{}}{-}A=D\underset{\dot{}}{-}D$$
40	1 2 3 27 29 32 31 33 37	tgcgrcomlr	$$⊢\left(\phi \wedge A\ne B\right)\to B\underset{\dot{}}{-}A=E\underset{\dot{}}{-}D$$
41	1 2 3 27 29 32 28 31 33 30 29 31 34 35 36 37 38 39 40	axtg5seg	$$⊢\left(\phi \wedge A\ne B\right)\to C\underset{\dot{}}{-}A=F\underset{\dot{}}{-}D$$
42	1 2 3 27 28 29 30 31 41	tgcgrcomlr	$$⊢\left(\phi \wedge A\ne B\right)\to A\underset{\dot{}}{-}C=D\underset{\dot{}}{-}F$$
43	26 42	pm2.61dane	$$⊢\phi \to A\underset{\dot{}}{-}C=D\underset{\dot{}}{-}F$$