Theorem cgracgr

Description: First direction of proposition 11.4 of Schwabhauser p. 95. Again, this is "half" of the proposition, i.e. only two additional points are used, while Schwabhauser has four. (Contributed by Thierry Arnoux, 31-Jul-2020)

	Ref	Expression
Hypotheses	iscgra.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	iscgra.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	iscgra.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	iscgra.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	iscgra.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	iscgra.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	iscgra.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	iscgra.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	iscgra.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	iscgra.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	cgrahl1.2	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
	cgrahl1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	cgracgr.m	⊢ − = ( dist ‘ 𝐺 )
	cgracgr.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	cgracgr.1	⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐵 ) 𝐴 )
	cgracgr.2	⊢ ( 𝜑 → 𝑌 ( 𝐾 ‘ 𝐵 ) 𝐶 )
	cgracgr.3	⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) = ( 𝐸 − 𝐷 ) )
	cgracgr.4	⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) = ( 𝐸 − 𝐹 ) )
Assertion	cgracgr	⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝐷 − 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		iscgra.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		iscgra.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		iscgra.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
4		iscgra.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		iscgra.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		iscgra.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		iscgra.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		iscgra.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		iscgra.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10		iscgra.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11		cgrahl1.2	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
12		cgrahl1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
13		cgracgr.m	⊢ − = ( dist ‘ 𝐺 )
14		cgracgr.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
15		cgracgr.1	⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐵 ) 𝐴 )
16		cgracgr.2	⊢ ( 𝜑 → 𝑌 ( 𝐾 ‘ 𝐵 ) 𝐶 )
17		cgracgr.3	⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) = ( 𝐸 − 𝐷 ) )
18		cgracgr.4	⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) = ( 𝐸 − 𝐹 ) )
19		eqid	⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
20	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐺 ∈ TarskiG )
21	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐴 ∈ 𝑃 )
22	6	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐵 ∈ 𝑃 )
23	12	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑋 ∈ 𝑃 )
24		eqid	⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
25		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ∈ 𝑃 )
26	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ 𝑃 )
27	14	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑌 ∈ 𝑃 )
28	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ∈ 𝑃 )
29	10	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐹 ∈ 𝑃 )
30	1 2 3 12 5 6 4 15	hlne2	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
31	30	necomd	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
32	1 2 3 12 5 6 4 19 15	hlln	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝐵 ) )
33	1 2 19 4 6 5 12 31 32	lncom	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐴 ) )
34	33	orcd	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐴 ) ∨ 𝐵 = 𝐴 ) )
35	1 19 2 4 6 5 12 34	colrot1	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝑋 ) ∨ 𝐴 = 𝑋 ) )
36	35	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐵 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝑋 ) ∨ 𝐴 = 𝑋 ) )
37	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐶 ∈ 𝑃 )
38		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ∈ 𝑃 )
39		simpr1	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ )
40	1 13 2 24 20 21 22 37 25 26 38 39	cgr3simp1	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝐸 ) )
41	17	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐵 − 𝑋 ) = ( 𝐸 − 𝐷 ) )
42		eqid	⊢ ( ≤G ‘ 𝐺 ) = ( ≤G ‘ 𝐺 )
43		simpr2	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 )
44	1 2 3 25 28 26 20	ishlg	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ↔ ( 𝑥 ≠ 𝐸 ∧ 𝐷 ≠ 𝐸 ∧ ( 𝑥 ∈ ( 𝐸 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐸 𝐼 𝑥 ) ) ) ) )
45	43 44	mpbid	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑥 ≠ 𝐸 ∧ 𝐷 ≠ 𝐸 ∧ ( 𝑥 ∈ ( 𝐸 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐸 𝐼 𝑥 ) ) ) )
46	45	simp3d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑥 ∈ ( 𝐸 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐸 𝐼 𝑥 ) ) )
47	1 2 3 12 5 6 4	ishlg	⊢ ( 𝜑 → ( 𝑋 ( 𝐾 ‘ 𝐵 ) 𝐴 ↔ ( 𝑋 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑋 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝑋 ) ) ) ) )
48	15 47	mpbid	⊢ ( 𝜑 → ( 𝑋 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑋 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝑋 ) ) ) )
49	48	simp3d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝑋 ) ) )
50	49	orcomd	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝐵 𝐼 𝐴 ) ) )
51	50	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐴 ∈ ( 𝐵 𝐼 𝑋 ) ∨ 𝑋 ∈ ( 𝐵 𝐼 𝐴 ) ) )
52	40	eqcomd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑥 − 𝐸 ) = ( 𝐴 − 𝐵 ) )
53	1 13 2 20 25 26 21 22 52	tgcgrcomlr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) )
54	41	eqcomd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐸 − 𝐷 ) = ( 𝐵 − 𝑋 ) )
55	1 13 2 42 20 26 25 28 22 22 21 23 46 51 53 54	tgcgrsub2	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑥 − 𝐷 ) = ( 𝐴 − 𝑋 ) )
56	55	eqcomd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐴 − 𝑋 ) = ( 𝑥 − 𝐷 ) )
57	1 13 2 20 21 23 25 28 56	tgcgrcomlr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑋 − 𝐴 ) = ( 𝐷 − 𝑥 ) )
58	1 13 24 20 21 22 23 25 26 28 40 41 57	trgcgr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝐷 ”⟩ )
59	1 2 3 14 7 6 4 19 16	hlln	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝐵 ) )
60	59	orcd	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝐵 ) ∨ 𝐶 = 𝐵 ) )
61	1 19 2 4 7 6 14 60	colrot1	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝑌 ) ∨ 𝐵 = 𝑌 ) )
62	61	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐶 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝑌 ) ∨ 𝐵 = 𝑌 ) )
63	1 13 2 24 20 21 22 37 25 26 38 39	cgr3simp2	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝑦 ) )
64	1 2 3 14 7 6 4	ishlg	⊢ ( 𝜑 → ( 𝑌 ( 𝐾 ‘ 𝐵 ) 𝐶 ↔ ( 𝑌 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ ( 𝑌 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝑌 ) ) ) ) )
65	16 64	mpbid	⊢ ( 𝜑 → ( 𝑌 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ ( 𝑌 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝑌 ) ) ) )
66	65	simp3d	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝑌 ) ) )
67	66	orcomd	⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐵 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐵 𝐼 𝐶 ) ) )
68	67	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐶 ∈ ( 𝐵 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝐵 𝐼 𝐶 ) ) )
69		simpr3	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 )
70	1 2 3 38 29 26 20	ishlg	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ↔ ( 𝑦 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝑦 ) ) ) ) )
71	69 70	mpbid	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑦 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝑦 ) ) ) )
72	71	simp3d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝑦 ) ) )
73	18	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐵 − 𝑌 ) = ( 𝐸 − 𝐹 ) )
74	1 13 2 42 20 22 37 27 26 26 38 29 68 72 63 73	tgcgrsub2	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐶 − 𝑌 ) = ( 𝑦 − 𝐹 ) )
75	1 13 2 20 22 27 26 29 73	tgcgrcomlr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑌 − 𝐵 ) = ( 𝐹 − 𝐸 ) )
76	1 13 24 20 22 37 27 26 38 29 63 74 75	trgcgr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝐵 𝐶 𝑌 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝑦 𝐹 ”⟩ )
77	53	eqcomd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝑥 ) )
78	1 13 2 24 20 21 22 37 25 26 38 39	cgr3simp3	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐶 − 𝐴 ) = ( 𝑦 − 𝑥 ) )
79	1 2 3 4 5 6 7 8 9 10 11	cgrane2	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
80	79	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐵 ≠ 𝐶 )
81	1 19 2 20 22 37 27 24 26 38 13 21 29 25 62 76 77 78 80	tgfscgr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑌 − 𝐴 ) = ( 𝐹 − 𝑥 ) )
82	1 13 2 20 27 21 29 25 81	tgcgrcomlr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐴 − 𝑌 ) = ( 𝑥 − 𝐹 ) )
83	30	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐴 ≠ 𝐵 )
84	1 19 2 20 21 22 23 24 25 26 13 27 28 29 36 58 82 73 83	tgfscgr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑋 − 𝑌 ) = ( 𝐷 − 𝐹 ) )
85	1 2 3 4 5 6 7 8 9 10	iscgra	⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
86	11 85	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) )
87	84 86	r19.29vva	⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝐷 − 𝐹 ) )