Theorem tgaas1h

Description: tgaas1 with the constructed point H still explicit: the case split on F = H . Equal, and the side equality is a substitution; distinct, and tgaasne closes the branch. BOTH branches are proved -- assuming F = H would be assuming the theorem. (Contributed by JAG , 12-Aug-2026)

	Ref	Expression
Hypotheses	tgaascgra.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgaascgra.m	⊢ − = ( dist ‘ 𝐺 )
	tgaascgra.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgaascgra.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tgaascgra.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	tgaascgra.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgaascgra.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgaascgra.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgaascgra.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgaascgra.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	tgaascgra.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	tgaascgra.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	tgaascgra.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
	tgaascgra.ncol	⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
	tgaascgra.1	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
	tgaascgra.2	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
	tgaascgra.3	⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ )
	tgaascgra.4	⊢ ( 𝜑 → 𝐻 ( 𝐾 ‘ 𝐸 ) 𝐹 )
	tgaascgra.5	⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) )
Assertion	tgaas1h	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		tgaascgra.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgaascgra.m	⊢ − = ( dist ‘ 𝐺 )
3		tgaascgra.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgaascgra.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		tgaascgra.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
6		tgaascgra.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7		tgaascgra.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8		tgaascgra.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9		tgaascgra.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10		tgaascgra.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
11		tgaascgra.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
12		tgaascgra.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
13		tgaascgra.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
14		tgaascgra.ncol	⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
15		tgaascgra.1	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
16		tgaascgra.2	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
17		tgaascgra.3	⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐹 𝐷 ”⟩ )
18		tgaascgra.4	⊢ ( 𝜑 → 𝐻 ( 𝐾 ‘ 𝐸 ) 𝐹 )
19		tgaascgra.5	⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) )
20	19	eqcomd	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐻 ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝐹 = 𝐻 ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐻 ) )
22		simpr	⊢ ( ( 𝜑 ∧ 𝐹 = 𝐻 ) → 𝐹 = 𝐻 )
23	22	oveq2d	⊢ ( ( 𝜑 ∧ 𝐹 = 𝐻 ) → ( 𝐸 − 𝐹 ) = ( 𝐸 − 𝐻 ) )
24	23	eqcomd	⊢ ( ( 𝜑 ∧ 𝐹 = 𝐻 ) → ( 𝐸 − 𝐻 ) = ( 𝐸 − 𝐹 ) )
25	21 24	eqtrd	⊢ ( ( 𝜑 ∧ 𝐹 = 𝐻 ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
26	6	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) → 𝐺 ∈ TarskiG )
27	10	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) → 𝐷 ∈ 𝑃 )
28	11	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) → 𝐸 ∈ 𝑃 )
29	12	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) → 𝐹 ∈ 𝑃 )
30	13	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) → 𝐻 ∈ 𝑃 )
31	1 3 2 6 7 8 9 10 11 12 16 4 14	cgrancol	⊢ ( 𝜑 → ¬ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
32	1 4 3 6 10 11 12 31	ncolrot1	⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
34	18	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) → 𝐻 ( 𝐾 ‘ 𝐸 ) 𝐹 )
35		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) → 𝐹 ≠ 𝐻 )
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	tgaascgra	⊢ ( 𝜑 → ⟨“ 𝐷 𝐹 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐻 𝐸 ”⟩ )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) → ⟨“ 𝐷 𝐹 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐻 𝐸 ”⟩ )
38	1 2 3 4 5 26 27 28 29 30 33 34 35 37	tgaasne	⊢ ( ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
39	25 38	pm2.61dane	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )