Theorem tgaasne

Description: Two DISTINCT points F and H on one half-line from E , subtending congruent angles at a point D off the line, are contradictory. ishlg unfolds the half-line to "one of them is strictly between E and the other" -- both sub-branches are proved, each by tgaasexc on its own triangle, and they are not permutations of one another: the second needs the non-collinearity transported to line E H by cgrancol . (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgaasne.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgaasne.m	⊢ − = ( dist ‘ 𝐺 )
	tgaasne.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgaasne.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tgaasne.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	tgaasne.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgaasne.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	tgaasne.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	tgaasne.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	tgaasne.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
	tgaasne.1	⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
	tgaasne.2	⊢ ( 𝜑 → 𝐻 ( 𝐾 ‘ 𝐸 ) 𝐹 )
	tgaasne.3	⊢ ( 𝜑 → 𝐹 ≠ 𝐻 )
	tgaasne.4	⊢ ( 𝜑 → ⟨“ 𝐷 𝐹 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐻 𝐸 ”⟩ )
Assertion	tgaasne	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		tgaasne.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgaasne.m	⊢ − = ( dist ‘ 𝐺 )
3		tgaasne.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgaasne.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		tgaasne.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
6		tgaasne.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7		tgaasne.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
8		tgaasne.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
9		tgaasne.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
10		tgaasne.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
11		tgaasne.1	⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
12		tgaasne.2	⊢ ( 𝜑 → 𝐻 ( 𝐾 ‘ 𝐸 ) 𝐹 )
13		tgaasne.3	⊢ ( 𝜑 → 𝐹 ≠ 𝐻 )
14		tgaasne.4	⊢ ( 𝜑 → ⟨“ 𝐷 𝐹 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐻 𝐸 ”⟩ )
15	6	adantr	⊢ ( ( 𝜑 ∧ 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐺 ∈ TarskiG )
16	7	adantr	⊢ ( ( 𝜑 ∧ 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐷 ∈ 𝑃 )
17	8	adantr	⊢ ( ( 𝜑 ∧ 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐸 ∈ 𝑃 )
18	10	adantr	⊢ ( ( 𝜑 ∧ 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐻 ∈ 𝑃 )
19	9	adantr	⊢ ( ( 𝜑 ∧ 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐹 ∈ 𝑃 )
20	11	adantr	⊢ ( ( 𝜑 ∧ 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ) → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
21		simpr	⊢ ( ( 𝜑 ∧ 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) )
22	1 3 5 10 9 8 6	ishlg	⊢ ( 𝜑 → ( 𝐻 ( 𝐾 ‘ 𝐸 ) 𝐹 ↔ ( 𝐻 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ ( 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) ) ) )
23	12 22	mpbid	⊢ ( 𝜑 → ( 𝐻 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ ( 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) ) )
24	23	simp1d	⊢ ( 𝜑 → 𝐻 ≠ 𝐸 )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐻 ≠ 𝐸 )
26	13	necomd	⊢ ( 𝜑 → 𝐻 ≠ 𝐹 )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝐻 ≠ 𝐹 )
28	14	adantr	⊢ ( ( 𝜑 ∧ 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ) → ⟨“ 𝐷 𝐹 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐻 𝐸 ”⟩ )
29	1 2 3 4 15 16 17 18 19 20 21 25 27 28	tgaasexc	⊢ ( ( 𝜑 ∧ 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ) → 𝜓 )
30	6	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) → 𝐺 ∈ TarskiG )
31	7	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) → 𝐷 ∈ 𝑃 )
32	8	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) → 𝐸 ∈ 𝑃 )
33	9	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) → 𝐹 ∈ 𝑃 )
34	10	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) → 𝐻 ∈ 𝑃 )
35	1 3 2 6 7 9 8 7 10 8 14	cgraswaplr	⊢ ( 𝜑 → ⟨“ 𝐸 𝐹 𝐷 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐻 𝐷 ”⟩ )
36	1 3 2 6 8 9 7 8 10 7 35 4 11	cgrancol	⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐻 ) ∨ 𝐸 = 𝐻 ) )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐻 ) ∨ 𝐸 = 𝐻 ) )
38		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) → 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) )
39	23	simp2d	⊢ ( 𝜑 → 𝐹 ≠ 𝐸 )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) → 𝐹 ≠ 𝐸 )
41	13	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) → 𝐹 ≠ 𝐻 )
42	1 3 6 5 7 9 8 7 10 8 14	cgracom	⊢ ( 𝜑 → ⟨“ 𝐷 𝐻 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝐸 ”⟩ )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) → ⟨“ 𝐷 𝐻 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝐸 ”⟩ )
44	1 2 3 4 30 31 32 33 34 37 38 40 41 43	tgaasexc	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) → 𝜓 )
45	23	simp3d	⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝐻 ) ) )
46	29 44 45	mpjaodan	⊢ ( 𝜑 → 𝜓 )