inagcgrasubhl

Description: In-angle transport, degenerate branch (i): the sub-angle <" D E W "> is **null**, W lying on ray E D . The witness is not constructed -- it is X , the target's own first arm -- and cgrahlb supplies the copied angle from the two ray degeneracies. No GeoCoq counterpart: GeoCoq's branch only locates a witness supplied by its universal statement. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	inagcgrasubhl.p	$⊢ P = {Base}_{G}$
	inagcgrasubhl.i	$⊢ I = Itv (G)$
	inagcgrasubhl.k	$⊢ K = {hl}_{𝒢} (G)$
	inagcgrasubhl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	inagcgrasubhl.d	$⊢ φ \to D \in P$
	inagcgrasubhl.e	$⊢ φ \to E \in P$
	inagcgrasubhl.f	$⊢ φ \to F \in P$
	inagcgrasubhl.w	$⊢ φ \to W \in P$
	inagcgrasubhl.x	$⊢ φ \to X \in P$
	inagcgrasubhl.y	$⊢ φ \to Y \in P$
	inagcgrasubhl.z	$⊢ φ \to Z \in P$
	inagcgrasubhl.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
	inagcgrasubhl.1	$⊢ φ \to D K (E) W$
Assertion	inagcgrasubhl	$⊢ φ \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		inagcgrasubhl.p	$⊢ P = {Base}_{G}$
2		inagcgrasubhl.i	$⊢ I = Itv (G)$
3		inagcgrasubhl.k	$⊢ K = {hl}_{𝒢} (G)$
4		inagcgrasubhl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		inagcgrasubhl.d	$⊢ φ \to D \in P$
6		inagcgrasubhl.e	$⊢ φ \to E \in P$
7		inagcgrasubhl.f	$⊢ φ \to F \in P$
8		inagcgrasubhl.w	$⊢ φ \to W \in P$
9		inagcgrasubhl.x	$⊢ φ \to X \in P$
10		inagcgrasubhl.y	$⊢ φ \to Y \in P$
11		inagcgrasubhl.z	$⊢ φ \to Z \in P$
12		inagcgrasubhl.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
13		inagcgrasubhl.1	$⊢ φ \to D K (E) W$
14		simpr	$⊢ (φ \land v = X) \to v = X$
15	14	breq1d	$⊢ (φ \land v = X) \to (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \leftrightarrow X \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩)$
16		eqidd	$⊢ (φ \land v = X) \to X = X$
17		eqidd	$⊢ (φ \land v = X) \to Y = Y$
18	16 17 14	s3eqd	$⊢ (φ \land v = X) \to ⟨“ X Y v ”⟩ = ⟨“ X Y X ”⟩$
19	18	breq2d	$⊢ (φ \land v = X) \to (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \leftrightarrow ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y X ”⟩)$
20	15 19	anbi12d	$⊢ (φ \land v = X) \to ((v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩) \leftrightarrow (X \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y X ”⟩))$
21	1 2 3 4 5 6 7 9 10 11 12	cgrane3	$⊢ φ \to Y \neq X$
22	21	necomd	$⊢ φ \to X \neq Y$
23	1 2 3 4 5 6 7 9 10 11 12	cgrane4	$⊢ φ \to Y \neq Z$
24	23	necomd	$⊢ φ \to Z \neq Y$
25		eqid	$⊢ dist (G) = dist (G)$
26	1 25 2 4 9 11	tgbtwntriv1	$⊢ φ \to X \in (X I Z)$
27	1 2 3 9 9 10 4 22	hlid	$⊢ φ \to X K (Y) X$
28	27	olcd	$⊢ φ \to (X = Y \lor X K (Y) X)$
29	1 2 3 9 9 10 11 4 9 22 24 22 26 28	isinagd	$⊢ φ \to X \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
30	1 2 3 25 4 5 6 8 9 10 9 13 27	cgrahlb	$⊢ φ \to ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y X ”⟩$
31	29 30	jca	$⊢ φ \to (X \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y X ”⟩)$
32	9 20 31	rspcedvd	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$

Metamath Proof Explorer

Theorem inagcgrasubhl

Proof