inagcgrasubbtwn

Description: In-angle transport, degenerate branch (ii): the sub-angle <" D E W "> is **flat**, E lying between D and W . The witness is built beyond Y on the ray opposite Y X with axtgsegcon , and flatcgra supplies the copied angle from the two betweennesses. The in-angle conjunct goes through inagbtwn , which carries the flatness up to the containing angle, then cgrabtwn across the congruence and isinagd on the target. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	inagcgrasubbtwn.p	$⊢ P = {Base}_{G}$
	inagcgrasubbtwn.i	$⊢ I = Itv (G)$
	inagcgrasubbtwn.k	$⊢ K = {hl}_{𝒢} (G)$
	inagcgrasubbtwn.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	inagcgrasubbtwn.d	$⊢ φ \to D \in P$
	inagcgrasubbtwn.e	$⊢ φ \to E \in P$
	inagcgrasubbtwn.f	$⊢ φ \to F \in P$
	inagcgrasubbtwn.w	$⊢ φ \to W \in P$
	inagcgrasubbtwn.x	$⊢ φ \to X \in P$
	inagcgrasubbtwn.y	$⊢ φ \to Y \in P$
	inagcgrasubbtwn.z	$⊢ φ \to Z \in P$
	inagcgrasubbtwn.in	$⊢ φ \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	inagcgrasubbtwn.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
	inagcgrasubbtwn.1	$⊢ φ \to E \in (D I W)$
Assertion	inagcgrasubbtwn	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$

Proof

Step	Hyp	Ref	Expression
1		inagcgrasubbtwn.p	$⊢ P = {Base}_{G}$
2		inagcgrasubbtwn.i	$⊢ I = Itv (G)$
3		inagcgrasubbtwn.k	$⊢ K = {hl}_{𝒢} (G)$
4		inagcgrasubbtwn.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		inagcgrasubbtwn.d	$⊢ φ \to D \in P$
6		inagcgrasubbtwn.e	$⊢ φ \to E \in P$
7		inagcgrasubbtwn.f	$⊢ φ \to F \in P$
8		inagcgrasubbtwn.w	$⊢ φ \to W \in P$
9		inagcgrasubbtwn.x	$⊢ φ \to X \in P$
10		inagcgrasubbtwn.y	$⊢ φ \to Y \in P$
11		inagcgrasubbtwn.z	$⊢ φ \to Z \in P$
12		inagcgrasubbtwn.in	$⊢ φ \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
13		inagcgrasubbtwn.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
14		inagcgrasubbtwn.1	$⊢ φ \to E \in (D I W)$
15		simplr	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to v \in P$
16		simpll	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to φ$
17	16 9	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to X \in P$
18	16 10	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to Y \in P$
19	16 11	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to Z \in P$
20	16 4	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to G \in 𝒢_{Tarski}$
21	1 2 3 4 5 6 7 9 10 11 13	cgrane3	$⊢ φ \to Y \neq X$
22	21	necomd	$⊢ φ \to X \neq Y$
23	16 22	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to X \neq Y$
24	1 2 3 4 5 6 7 9 10 11 13	cgrane4	$⊢ φ \to Y \neq Z$
25	24	necomd	$⊢ φ \to Z \neq Y$
26	16 25	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to Z \neq Y$
27		eqid	$⊢ dist (G) = dist (G)$
28		simpr	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)$
29	28	simprd	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to Y dist (G) v = X dist (G) Y$
30	29	eqcomd	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to X dist (G) Y = Y dist (G) v$
31	1 27 2 20 17 18 18 15 30 23	tgcgrneq	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to Y \neq v$
32	31	necomd	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to v \neq Y$
33	1 2 3 4 5 6 7 8 12 14	inagbtwn	$⊢ φ \to E \in (D I F)$
34	1 2 27 4 5 6 7 9 10 11 13 33	cgrabtwn	$⊢ φ \to Y \in (X I Z)$
35	16 34	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to Y \in (X I Z)$
36		eqidd	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to Y = Y$
37	36	orcd	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to (Y = Y \lor Y K (Y) v)$
38	1 2 3 15 17 18 19 20 18 23 26 32 35 37	isinagd	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
39	16 5	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to D \in P$
40	16 6	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to E \in P$
41	16 8	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to W \in P$
42	16 14	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to E \in (D I W)$
43	28	simpld	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to Y \in (X I v)$
44	1 2 3 8 5 6 7 4 12	inagne1	$⊢ φ \to D \neq E$
45	16 44	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to D \neq E$
46	1 2 3 8 5 6 7 4 12	inagne3	$⊢ φ \to W \neq E$
47	16 46	syl	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to W \neq E$
48	1 2 27 20 39 40 41 17 18 15 42 43 45 47 23 32	flatcgra	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩$
49	38 48	jca	$⊢ ((φ \land v \in P) \land (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)) \to (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
50	1 27 2 4 9 10 9 10	axtgsegcon	$⊢ φ \to \exists v \in P (Y \in (X I v) \land Y dist (G) v = X dist (G) Y)$
51	49 50	reximddv3	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$

Metamath Proof Explorer

Theorem inagcgrasubbtwn

Proof