Theorem inagcgratrgmain

Description: In-angle transport, the non-degenerate main case, with its three constructions carried as hypotheses: J the segment point from isinag , S and T the normalized target arms from iscgrag , and Q the transferred point from cgrgptxfr . Concludes the body of cgrainag 's existential at the witness Q . **No acopy and no half-plane fact**: the witness is the transferred point, not a fresh angle copy, which is what removes the non-collinearity obligations. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	inagcgratrgmain.p	$$⊢P={\mathrm{Base}}_G$$
	inagcgratrgmain.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	inagcgratrgmain.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	inagcgratrgmain.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	inagcgratrgmain.d	$$⊢\phi \to D\in P$$
	inagcgratrgmain.e	$$⊢\phi \to E\in P$$
	inagcgratrgmain.w	$$⊢\phi \to W\in P$$
	inagcgratrgmain.x	$$⊢\phi \to X\in P$$
	inagcgratrgmain.y	$$⊢\phi \to Y\in P$$
	inagcgratrgmain.z	$$⊢\phi \to Z\in P$$
	inagcgratrgmain.j	$$⊢\phi \to J\in P$$
	inagcgratrgmain.s	$$⊢\phi \to S\in P$$
	inagcgratrgmain.t	$$⊢\phi \to T\in P$$
	inagcgratrgmain.q	$$⊢\phi \to Q\in P$$
	inagcgratrgmain.de	$$⊢\phi \to D\ne E$$
	inagcgratrgmain.jw	$$⊢\phi \to JK\left(E\right)W$$
	inagcgratrgmain.sx	$$⊢\phi \to SK\left(Y\right)X$$
	inagcgratrgmain.tz	$$⊢\phi \to TK\left(Y\right)Z$$
	inagcgratrgmain.q1	$$⊢\phi \to Q\in \left(SIT\right)$$
	inagcgratrgmain.sub	$$⊢\phi \to ⟨“DEJ”⟩{\sim }_{𝒢}\left(G\right)⟨“SYQ”⟩$$
	inagcgratrgmain.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
Assertion	inagcgratrgmain	$$⊢\phi \to \left(Q{\in }_{𝒢}^{\angle }\left(G\right)⟨“XYZ”⟩\wedge ⟨“DEW”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“XYQ”⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		inagcgratrgmain.p	$$⊢P={\mathrm{Base}}_G$$
2		inagcgratrgmain.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		inagcgratrgmain.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
4		inagcgratrgmain.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		inagcgratrgmain.d	$$⊢\phi \to D\in P$$
6		inagcgratrgmain.e	$$⊢\phi \to E\in P$$
7		inagcgratrgmain.w	$$⊢\phi \to W\in P$$
8		inagcgratrgmain.x	$$⊢\phi \to X\in P$$
9		inagcgratrgmain.y	$$⊢\phi \to Y\in P$$
10		inagcgratrgmain.z	$$⊢\phi \to Z\in P$$
11		inagcgratrgmain.j	$$⊢\phi \to J\in P$$
12		inagcgratrgmain.s	$$⊢\phi \to S\in P$$
13		inagcgratrgmain.t	$$⊢\phi \to T\in P$$
14		inagcgratrgmain.q	$$⊢\phi \to Q\in P$$
15		inagcgratrgmain.de	$$⊢\phi \to D\ne E$$
16		inagcgratrgmain.jw	$$⊢\phi \to JK\left(E\right)W$$
17		inagcgratrgmain.sx	$$⊢\phi \to SK\left(Y\right)X$$
18		inagcgratrgmain.tz	$$⊢\phi \to TK\left(Y\right)Z$$
19		inagcgratrgmain.q1	$$⊢\phi \to Q\in \left(SIT\right)$$
20		inagcgratrgmain.sub	$$⊢\phi \to ⟨“DEJ”⟩{\sim }_{𝒢}\left(G\right)⟨“SYQ”⟩$$
21		inagcgratrgmain.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
22	1 2 3 12 8 9 4 17	hlne1	$$⊢\phi \to S\ne Y$$
23	1 2 3 13 10 9 4 18	hlne1	$$⊢\phi \to T\ne Y$$
24		eqid	$$⊢{\sim }_{𝒢}\left(G\right)={\sim }_{𝒢}\left(G\right)$$
25	1 21 2 24 4 5 6 11 12 9 14 20	cgr3simp2	$$⊢\phi \to E\underset{\dot{}}{-}J=Y\underset{\dot{}}{-}Q$$
26	1 2 3 11 7 6 4 16	hlne1	$$⊢\phi \to J\ne E$$
27	26	necomd	$$⊢\phi \to E\ne J$$
28	1 21 2 4 6 11 9 14 25 27	tgcgrneq	$$⊢\phi \to Y\ne Q$$
29	28	necomd	$$⊢\phi \to Q\ne Y$$
30	1 2 3 14 14 9 4 29	hlid	$$⊢\phi \to QK\left(Y\right)Q$$
31	30	olcd	$$⊢\phi \to \left(Q=Y\vee QK\left(Y\right)Q\right)$$
32	1 2 3 14 12 9 13 4 14 22 23 29 19 31	isinagd	$$⊢\phi \to Q{\in }_{𝒢}^{\angle }\left(G\right)⟨“SYT”⟩$$
33	1 2 3 12 8 9 4 17	hlcomd	$$⊢\phi \to XK\left(Y\right)S$$
34	1 2 3 13 10 9 4 18	hlcomd	$$⊢\phi \to ZK\left(Y\right)T$$
35	1 2 3 14 12 9 13 4 32 8 10 14 33 34 30	inaghl	$$⊢\phi \to Q{\in }_{𝒢}^{\angle }\left(G\right)⟨“XYZ”⟩$$
36	1 2 4 3 5 6 11 12 9 14 15 27 20	cgrcgra	$$⊢\phi \to ⟨“DEJ”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“SYQ”⟩$$
37	1 2 3 4 5 6 11 12 9 14 36 8 33	cgrahl1	$$⊢\phi \to ⟨“DEJ”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“XYQ”⟩$$
38	1 2 4 3 5 6 11 8 9 14 37	cgracom	$$⊢\phi \to ⟨“XYQ”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEJ”⟩$$
39	1 2 3 11 7 6 4 16	hlcomd	$$⊢\phi \to WK\left(E\right)J$$
40	1 2 3 4 8 9 14 5 6 11 38 7 39	cgrahl2	$$⊢\phi \to ⟨“XYQ”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEW”⟩$$
41	1 2 4 3 8 9 14 5 6 7 40	cgracom	$$⊢\phi \to ⟨“DEW”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“XYQ”⟩$$
42	35 41	jca	$$⊢\phi \to \left(Q{\in }_{𝒢}^{\angle }\left(G\right)⟨“XYZ”⟩\wedge ⟨“DEW”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“XYQ”⟩\right)$$