inagcgratrgncol

Description: In-angle transport once the segment point J of isinag is on the ray E W : iscgrag normalizes the target arms and its two existentials are eliminated here, leaving inagcgratrgxfr to do the transfer. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	inagcgratrgncol.p	$⊢ P = {Base}_{G}$
	inagcgratrgncol.i	$⊢ I = Itv (G)$
	inagcgratrgncol.k	$⊢ K = {hl}_{𝒢} (G)$
	inagcgratrgncol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	inagcgratrgncol.d	$⊢ φ \to D \in P$
	inagcgratrgncol.e	$⊢ φ \to E \in P$
	inagcgratrgncol.f	$⊢ φ \to F \in P$
	inagcgratrgncol.w	$⊢ φ \to W \in P$
	inagcgratrgncol.x	$⊢ φ \to X \in P$
	inagcgratrgncol.y	$⊢ φ \to Y \in P$
	inagcgratrgncol.z	$⊢ φ \to Z \in P$
	inagcgratrgncol.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
	inagcgratrgncol.j	$⊢ φ \to J \in P$
	inagcgratrgncol.de	$⊢ φ \to D \neq E$
	inagcgratrgncol.1	$⊢ φ \to J \in (D I F)$
	inagcgratrgncol.jw	$⊢ φ \to J K (E) W$
Assertion	inagcgratrgncol	$⊢ φ \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		inagcgratrgncol.p	$⊢ P = {Base}_{G}$
2		inagcgratrgncol.i	$⊢ I = Itv (G)$
3		inagcgratrgncol.k	$⊢ K = {hl}_{𝒢} (G)$
4		inagcgratrgncol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		inagcgratrgncol.d	$⊢ φ \to D \in P$
6		inagcgratrgncol.e	$⊢ φ \to E \in P$
7		inagcgratrgncol.f	$⊢ φ \to F \in P$
8		inagcgratrgncol.w	$⊢ φ \to W \in P$
9		inagcgratrgncol.x	$⊢ φ \to X \in P$
10		inagcgratrgncol.y	$⊢ φ \to Y \in P$
11		inagcgratrgncol.z	$⊢ φ \to Z \in P$
12		inagcgratrgncol.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
13		inagcgratrgncol.j	$⊢ φ \to J \in P$
14		inagcgratrgncol.de	$⊢ φ \to D \neq E$
15		inagcgratrgncol.1	$⊢ φ \to J \in (D I F)$
16		inagcgratrgncol.jw	$⊢ φ \to J K (E) W$
17		eqid	$⊢ dist (G) = dist (G)$
18	1 2 3 17 4 5 6 7 9 10 11 12	iscgrag	$⊢ φ \to \exists x \in P \exists y \in P ((⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z) \land (Y dist (G) x = E dist (G) D \land Y dist (G) y = E dist (G) F))$
19		simpl	$⊢ ((⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z) \land (Y dist (G) x = E dist (G) D \land Y dist (G) y = E dist (G) F)) \to (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)$
20	19	reximi	$⊢ \exists y \in P ((⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z) \land (Y dist (G) x = E dist (G) D \land Y dist (G) y = E dist (G) F)) \to \exists y \in P (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)$
21	20	reximi	$⊢ \exists x \in P \exists y \in P ((⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z) \land (Y dist (G) x = E dist (G) D \land Y dist (G) y = E dist (G) F)) \to \exists x \in P \exists y \in P (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)$
22	18 21	syl	$⊢ φ \to \exists x \in P \exists y \in P (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)$
23		simpll	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to φ$
24	23 4	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to G \in 𝒢_{Tarski}$
25	23 5	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to D \in P$
26	23 6	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to E \in P$
27	23 7	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to F \in P$
28	23 8	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to W \in P$
29	23 9	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to X \in P$
30	23 10	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to Y \in P$
31	23 11	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to Z \in P$
32	23 13	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to J \in P$
33		simplr	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to (x \in P \land y \in P)$
34	33	simpld	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to x \in P$
35	33	simprd	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to y \in P$
36	23 14	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to D \neq E$
37	23 15	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to J \in (D I F)$
38	23 16	syl	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to J K (E) W$
39		simpr	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)$
40	39	simp2d	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to x K (Y) X$
41	39	simp3d	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to y K (Y) Z$
42	39	simp1d	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to ⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩$
43	1 2 3 24 25 26 27 28 29 30 31 32 34 35 36 37 38 40 41 42	inagcgratrgxfr	$⊢ ((φ \land (x \in P \land y \in P)) \land (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z)) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
44	43	ex	$⊢ (φ \land (x \in P \land y \in P)) \to ((⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩))$
45	44	rexlimdvva	$⊢ φ \to (\exists x \in P \exists y \in P (⟨“ D E F ”⟩ \sim_{𝒢} (G) ⟨“ x Y y ”⟩ \land x K (Y) X \land y K (Y) Z) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩))$
46	22 45	mpd	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$

Metamath Proof Explorer

Theorem inagcgratrgncol

Proof