inagcgratrgxfr

Description: In-angle transport with the target arms already normalized to S and T : cgrgptxfr transfers the segment point J to a point of ( S I T ) , and that one existential is eliminated here. (Contributed by JAG, 12-Aug-2026)

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

Metamath Proof Explorer

Theorem inagcgratrgxfr

Proof