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	$⊢ P = {Base}_{G}$
	tgaasne.m	$⊢ \underset{˙}{-} = dist (G)$
	tgaasne.i	$⊢ I = Itv (G)$
	tgaasne.l	$⊢ L = {Line}_{𝒢} (G)$
	tgaasne.k	$⊢ K = {hl}_{𝒢} (G)$
	tgaasne.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgaasne.d	$⊢ φ \to D \in P$
	tgaasne.e	$⊢ φ \to E \in P$
	tgaasne.f	$⊢ φ \to F \in P$
	tgaasne.h	$⊢ φ \to H \in P$
	tgaasne.1	$⊢ φ \to \neg (D \in (E L F) \lor E = F)$
	tgaasne.2	$⊢ φ \to H K (E) F$
	tgaasne.3	$⊢ φ \to F \neq H$
	tgaasne.4	$⊢ φ \to ⟨“ D F E ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D H E ”⟩$
Assertion	tgaasne	$⊢ φ \to ψ$

Proof

Step	Hyp	Ref	Expression
1		tgaasne.p	$⊢ P = {Base}_{G}$
2		tgaasne.m	$⊢ \underset{˙}{-} = dist (G)$
3		tgaasne.i	$⊢ I = Itv (G)$
4		tgaasne.l	$⊢ L = {Line}_{𝒢} (G)$
5		tgaasne.k	$⊢ K = {hl}_{𝒢} (G)$
6		tgaasne.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		tgaasne.d	$⊢ φ \to D \in P$
8		tgaasne.e	$⊢ φ \to E \in P$
9		tgaasne.f	$⊢ φ \to F \in P$
10		tgaasne.h	$⊢ φ \to H \in P$
11		tgaasne.1	$⊢ φ \to \neg (D \in (E L F) \lor E = F)$
12		tgaasne.2	$⊢ φ \to H K (E) F$
13		tgaasne.3	$⊢ φ \to F \neq H$
14		tgaasne.4	$⊢ φ \to ⟨“ D F E ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D H E ”⟩$
15	6	adantr	$⊢ (φ \land H \in (E I F)) \to G \in 𝒢_{Tarski}$
16	7	adantr	$⊢ (φ \land H \in (E I F)) \to D \in P$
17	8	adantr	$⊢ (φ \land H \in (E I F)) \to E \in P$
18	10	adantr	$⊢ (φ \land H \in (E I F)) \to H \in P$
19	9	adantr	$⊢ (φ \land H \in (E I F)) \to F \in P$
20	11	adantr	$⊢ (φ \land H \in (E I F)) \to \neg (D \in (E L F) \lor E = F)$
21		simpr	$⊢ (φ \land H \in (E I F)) \to H \in (E I F)$
22	1 3 5 10 9 8 6	ishlg	$⊢ φ \to (H K (E) F \leftrightarrow (H \neq E \land F \neq E \land (H \in (E I F) \lor F \in (E I H))))$
23	12 22	mpbid	$⊢ φ \to (H \neq E \land F \neq E \land (H \in (E I F) \lor F \in (E I H)))$
24	23	simp1d	$⊢ φ \to H \neq E$
25	24	adantr	$⊢ (φ \land H \in (E I F)) \to H \neq E$
26	13	necomd	$⊢ φ \to H \neq F$
27	26	adantr	$⊢ (φ \land H \in (E I F)) \to H \neq F$
28	14	adantr	$⊢ (φ \land H \in (E I F)) \to ⟨“ D F E ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D H E ”⟩$
29	1 2 3 4 15 16 17 18 19 20 21 25 27 28	tgaasexc	$⊢ (φ \land H \in (E I F)) \to ψ$
30	6	adantr	$⊢ (φ \land F \in (E I H)) \to G \in 𝒢_{Tarski}$
31	7	adantr	$⊢ (φ \land F \in (E I H)) \to D \in P$
32	8	adantr	$⊢ (φ \land F \in (E I H)) \to E \in P$
33	9	adantr	$⊢ (φ \land F \in (E I H)) \to F \in P$
34	10	adantr	$⊢ (φ \land F \in (E I H)) \to H \in P$
35	1 3 2 6 7 9 8 7 10 8 14	cgraswaplr	$⊢ φ \to ⟨“ E F D ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ E H D ”⟩$
36	1 3 2 6 8 9 7 8 10 7 35 4 11	cgrancol	$⊢ φ \to \neg (D \in (E L H) \lor E = H)$
37	36	adantr	$⊢ (φ \land F \in (E I H)) \to \neg (D \in (E L H) \lor E = H)$
38		simpr	$⊢ (φ \land F \in (E I H)) \to F \in (E I H)$
39	23	simp2d	$⊢ φ \to F \neq E$
40	39	adantr	$⊢ (φ \land F \in (E I H)) \to F \neq E$
41	13	adantr	$⊢ (φ \land F \in (E I H)) \to F \neq H$
42	1 3 6 5 7 9 8 7 10 8 14	cgracom	$⊢ φ \to ⟨“ D H E ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D F E ”⟩$
43	42	adantr	$⊢ (φ \land F \in (E I H)) \to ⟨“ D H E ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D F E ”⟩$
44	1 2 3 4 30 31 32 33 34 37 38 40 41 43	tgaasexc	$⊢ (φ \land F \in (E I H)) \to ψ$
45	23	simp3d	$⊢ φ \to (H \in (E I F) \lor F \in (E I H))$
46	29 44 45	mpjaodan	$⊢ φ \to ψ$

Metamath Proof Explorer

Theorem tgaasne

Proof