Theorem tgidinside

Description: Law for finding a point inside a segment. Theorem 4.19 of Schwabhauser p. 38. (Contributed by Thierry Arnoux, 28-Apr-2019)

	Ref	Expression
Hypotheses	tglngval.p	$$⊢P={\mathrm{Base}}_G$$
	tglngval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	tglngval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tglngval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tglngval.x	$$⊢\phi \to X\in P$$
	tglngval.y	$$⊢\phi \to Y\in P$$
	tgcolg.z	$$⊢\phi \to Z\in P$$
	lnxfr.r	$$⊢\underset{\dot{}}{\sim }={\sim }_{𝒢}\left(G\right)$$
	lnxfr.a	$$⊢\phi \to A\in P$$
	lnxfr.b	$$⊢\phi \to B\in P$$
	lnxfr.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tgidinside.1	$$⊢\phi \to Z\in \left(XIY\right)$$
	tgidinside.2	$$⊢\phi \to X\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}A$$
	tgidinside.3	$$⊢\phi \to Y\underset{\dot{}}{-}Z=Y\underset{\dot{}}{-}A$$
Assertion	tgidinside	$$⊢\phi \to Z=A$$

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	$$⊢P={\mathrm{Base}}_G$$
2		tglngval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
3		tglngval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tglngval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tglngval.x	$$⊢\phi \to X\in P$$
6		tglngval.y	$$⊢\phi \to Y\in P$$
7		tgcolg.z	$$⊢\phi \to Z\in P$$
8		lnxfr.r	$$⊢\underset{\dot{}}{\sim }={\sim }_{𝒢}\left(G\right)$$
9		lnxfr.a	$$⊢\phi \to A\in P$$
10		lnxfr.b	$$⊢\phi \to B\in P$$
11		lnxfr.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
12		tgidinside.1	$$⊢\phi \to Z\in \left(XIY\right)$$
13		tgidinside.2	$$⊢\phi \to X\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}A$$
14		tgidinside.3	$$⊢\phi \to Y\underset{\dot{}}{-}Z=Y\underset{\dot{}}{-}A$$
15	4	adantr	$$⊢\left(\phi \wedge X=Y\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
16	5	adantr	$$⊢\left(\phi \wedge X=Y\right)\to X\in P$$
17	7	adantr	$$⊢\left(\phi \wedge X=Y\right)\to Z\in P$$
18	12	adantr	$$⊢\left(\phi \wedge X=Y\right)\to Z\in \left(XIY\right)$$
19		simpr	$$⊢\left(\phi \wedge X=Y\right)\to X=Y$$
20	19	oveq2d	$$⊢\left(\phi \wedge X=Y\right)\to XIX=XIY$$
21	18 20	eleqtrrd	$$⊢\left(\phi \wedge X=Y\right)\to Z\in \left(XIX\right)$$
22	1 11 3 15 16 17 21	axtgbtwnid	$$⊢\left(\phi \wedge X=Y\right)\to X=Z$$
23	9	adantr	$$⊢\left(\phi \wedge X=Y\right)\to A\in P$$
24	13	adantr	$$⊢\left(\phi \wedge X=Y\right)\to X\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}A$$
25	1 11 3 15 16 17 16 23 24 22	tgcgreq	$$⊢\left(\phi \wedge X=Y\right)\to X=A$$
26	22 25	eqtr3d	$$⊢\left(\phi \wedge X=Y\right)\to Z=A$$
27	4	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
28	5	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to X\in P$$
29	6	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to Y\in P$$
30	7	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to Z\in P$$
31	9	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to A\in P$$
32	10	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to B\in P$$
33		simpr	$$⊢\left(\phi \wedge X\ne Y\right)\to X\ne Y$$
34	1 2 3 4 5 7 6 12	btwncolg3	$$⊢\phi \to \left(Y\in \left(XLZ\right)\vee X=Z\right)$$
35	34	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to \left(Y\in \left(XLZ\right)\vee X=Z\right)$$
36	13	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to X\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}A$$
37	14	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to Y\underset{\dot{}}{-}Z=Y\underset{\dot{}}{-}A$$
38	1 2 3 27 28 29 30 8 31 32 11 33 35 36 37	lnid	$$⊢\left(\phi \wedge X\ne Y\right)\to Z=A$$
39	26 38	pm2.61dane	$$⊢\phi \to Z=A$$