Theorem lncgr

Description: Congruence rule for lines. Theorem 4.17 of Schwabhauser p. 37. (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)$$
	lncgr.1	$$⊢\phi \to X\ne Y$$
	lncgr.2	$$⊢\phi \to \left(Y\in \left(XLZ\right)\vee X=Z\right)$$
	lncgr.3	$$⊢\phi \to X\underset{\dot{}}{-}A=X\underset{\dot{}}{-}B$$
	lncgr.4	$$⊢\phi \to Y\underset{\dot{}}{-}A=Y\underset{\dot{}}{-}B$$
Assertion	lncgr	$$⊢\phi \to Z\underset{\dot{}}{-}A=Z\underset{\dot{}}{-}B$$

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		lncgr.1	$$⊢\phi \to X\ne Y$$
13		lncgr.2	$$⊢\phi \to \left(Y\in \left(XLZ\right)\vee X=Z\right)$$
14		lncgr.3	$$⊢\phi \to X\underset{\dot{}}{-}A=X\underset{\dot{}}{-}B$$
15		lncgr.4	$$⊢\phi \to Y\underset{\dot{}}{-}A=Y\underset{\dot{}}{-}B$$
16	1 11 3 8 4 5 6 7	cgr3id	$$⊢\phi \to ⟨“XYZ”⟩\underset{\dot{}}{\sim }⟨“XYZ”⟩$$
17	1 2 3 4 5 6 7 8 5 6 11 9 7 10 13 16 14 15 12	tgfscgr	$$⊢\phi \to Z\underset{\dot{}}{-}A=Z\underset{\dot{}}{-}B$$