inagbtwn

Description: A flat sub-angle forces the containing angle flat: if W is inside angle <" D E F "> and E lies between D and W , then E lies between D and F . This is GeoCoq bet__in__angle__bet. Proved by unfolding isinag and following its segment point. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	inagbtwn.p	$⊢ P = {Base}_{G}$
	inagbtwn.i	$⊢ I = Itv (G)$
	inagbtwn.k	$⊢ K = {hl}_{𝒢} (G)$
	inagbtwn.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	inagbtwn.d	$⊢ φ \to D \in P$
	inagbtwn.e	$⊢ φ \to E \in P$
	inagbtwn.f	$⊢ φ \to F \in P$
	inagbtwn.w	$⊢ φ \to W \in P$
	inagbtwn.in	$⊢ φ \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	inagbtwn.1	$⊢ φ \to E \in (D I W)$
Assertion	inagbtwn	$⊢ φ \to E \in (D I F)$

Proof

Step	Hyp	Ref	Expression
1		inagbtwn.p	$⊢ P = {Base}_{G}$
2		inagbtwn.i	$⊢ I = Itv (G)$
3		inagbtwn.k	$⊢ K = {hl}_{𝒢} (G)$
4		inagbtwn.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		inagbtwn.d	$⊢ φ \to D \in P$
6		inagbtwn.e	$⊢ φ \to E \in P$
7		inagbtwn.f	$⊢ φ \to F \in P$
8		inagbtwn.w	$⊢ φ \to W \in P$
9		inagbtwn.in	$⊢ φ \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
10		inagbtwn.1	$⊢ φ \to E \in (D I W)$
11		simpl	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x = E) \to ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W)))$
12		simpr	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to (x \in (D I F) \land (x = E \lor x K (E) W))$
13	12	simpld	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to x \in (D I F)$
14	11 13	syl	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x = E) \to x \in (D I F)$
15		simpr	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x = E) \to x = E$
16	15	eleq1d	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x = E) \to (x \in (D I F) \leftrightarrow E \in (D I F))$
17	14 16	mpbid	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x = E) \to E \in (D I F)$
18		eqid	$⊢ dist (G) = dist (G)$
19		simpl	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W)))$
20		simpll	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to φ$
21	20 4	syl	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to G \in 𝒢_{Tarski}$
22	19 21	syl	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to G \in 𝒢_{Tarski}$
23	20 5	syl	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to D \in P$
24	19 23	syl	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to D \in P$
25	20 6	syl	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to E \in P$
26	19 25	syl	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to E \in P$
27		simplr	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to x \in P$
28	19 27	syl	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to x \in P$
29	20 7	syl	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to F \in P$
30	19 29	syl	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to F \in P$
31		simpl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land x \in (E I W)) \to (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W)$
32	31 22	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land x \in (E I W)) \to G \in 𝒢_{Tarski}$
33	31 28	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land x \in (E I W)) \to x \in P$
34	31 26	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land x \in (E I W)) \to E \in P$
35	31 24	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land x \in (E I W)) \to D \in P$
36	20 8	syl	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to W \in P$
37	19 36	syl	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to W \in P$
38	31 37	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land x \in (E I W)) \to W \in P$
39		simpr	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land x \in (E I W)) \to x \in (E I W)$
40	20 10	syl	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to E \in (D I W)$
41	19 40	syl	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to E \in (D I W)$
42	31 41	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land x \in (E I W)) \to E \in (D I W)$
43	1 18 2 32 33 34 35 38 39 42	tgbtwnintr	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land x \in (E I W)) \to E \in (x I D)$
44	1 18 2 32 33 34 35 43	tgbtwncom	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land x \in (E I W)) \to E \in (D I x)$
45		simpl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land W \in (E I x)) \to (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W)$
46	45 22	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land W \in (E I x)) \to G \in 𝒢_{Tarski}$
47	45 24	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land W \in (E I x)) \to D \in P$
48	45 26	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land W \in (E I x)) \to E \in P$
49	45 37	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land W \in (E I x)) \to W \in P$
50	45 28	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land W \in (E I x)) \to x \in P$
51		simpr	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to x K (E) W$
52	1 2 3 28 37 26 22	ishlg	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to (x K (E) W \leftrightarrow (x \neq E \land W \neq E \land (x \in (E I W) \lor W \in (E I x))))$
53	51 52	mpbid	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to (x \neq E \land W \neq E \land (x \in (E I W) \lor W \in (E I x)))$
54	53	simp2d	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to W \neq E$
55	54	necomd	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to E \neq W$
56	45 55	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land W \in (E I x)) \to E \neq W$
57	45 41	syl	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land W \in (E I x)) \to E \in (D I W)$
58		simpr	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land W \in (E I x)) \to W \in (E I x)$
59	1 18 2 46 47 48 49 50 56 57 58	tgbtwnouttr	$⊢ ((((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \land W \in (E I x)) \to E \in (D I x)$
60	53	simp3d	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to (x \in (E I W) \lor W \in (E I x))$
61	44 59 60	mpjaodan	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to E \in (D I x)$
62	19 13	syl	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to x \in (D I F)$
63	1 18 2 22 24 26 28 30 61 62	tgbtwnexch	$⊢ (((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \land x K (E) W) \to E \in (D I F)$
64	12	simprd	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to (x = E \lor x K (E) W)$
65	17 63 64	mpjaodan	$⊢ ((φ \land x \in P) \land (x \in (D I F) \land (x = E \lor x K (E) W))) \to E \in (D I F)$
66	1 2 3 8 5 6 7 4	isinag	$⊢ φ \to (W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow ((D \neq E \land F \neq E \land W \neq E) \land \exists x \in P (x \in (D I F) \land (x = E \lor x K (E) W))))$
67	9 66	mpbid	$⊢ φ \to ((D \neq E \land F \neq E \land W \neq E) \land \exists x \in P (x \in (D I F) \land (x = E \lor x K (E) W)))$
68	67	simprd	$⊢ φ \to \exists x \in P (x \in (D I F) \land (x = E \lor x K (E) W))$
69	65 68	r19.29a	$⊢ φ \to E \in (D I F)$

Metamath Proof Explorer

Theorem inagbtwn

Proof