inagcgratrgn

Description: In-angle transport, non-collinear case: unfold isinag , eliminate its segment-point existential, and dispatch on the disjunct it carries -- x = E to inagcgrabtwn , x ( KE ) W to inagcgratrgncol . (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 ”⟩$
	inagcgratrgn.l	$⊢ L = {Line}_{𝒢} (G)$
	inagcgratrgn.in	$⊢ φ \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	inagcgratrgn.1	$⊢ φ \to \neg (W \in (D L E) \lor D = E)$
Assertion	inagcgratrgn	$⊢ φ \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		inagcgratrgn.l	$⊢ L = {Line}_{𝒢} (G)$
14		inagcgratrgn.in	$⊢ φ \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
15		inagcgratrgn.1	$⊢ φ \to \neg (W \in (D L E) \lor D = E)$
16	1 2 3 8 5 6 7 4	isinag	$⊢ φ \to (W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow ((D \neq E \land F \neq E \land W \neq E) \land \exists x \in P (x \in (D I F) \land (x = E \lor x K (E) W))))$
17	14 16	mpbid	$⊢ φ \to ((D \neq E \land F \neq E \land W \neq E) \land \exists x \in P (x \in (D I F) \land (x = E \lor x K (E) W)))$
18	17	simprd	$⊢ φ \to \exists x \in P (x \in (D I F) \land (x = E \lor x K (E) W))$
19		simpl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to φ$
20	19 4	syl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to G \in 𝒢_{Tarski}$
21	20	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to G \in 𝒢_{Tarski}$
22	19 5	syl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to D \in P$
23	22	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to D \in P$
24	19 6	syl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to E \in P$
25	24	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to E \in P$
26	19 7	syl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to F \in P$
27	26	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to F \in P$
28	19 8	syl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to W \in P$
29	28	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to W \in P$
30	19 9	syl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to X \in P$
31	30	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to X \in P$
32	19 10	syl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to Y \in P$
33	32	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to Y \in P$
34	19 11	syl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to Z \in P$
35	34	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to Z \in P$
36	19 12	syl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
37	36	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
38		simpr	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))$
39	38	simprd	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to (x \in (D I F) \land (x = E \lor x K (E) W))$
40	39	simpld	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to x \in (D I F)$
41	40	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to x \in (D I F)$
42		simpr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to x = E$
43	42	eleq1d	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to (x \in (D I F) \leftrightarrow E \in (D I F))$
44	41 43	mpbid	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to E \in (D I F)$
45	19 15	syl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to \neg (W \in (D L E) \lor D = E)$
46	45	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to \neg (W \in (D L E) \lor D = E)$
47	1 2 3 13 21 23 25 27 29 31 33 35 37 44 46	inagcgrabtwn	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x = E) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
48	20	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to G \in 𝒢_{Tarski}$
49	22	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to D \in P$
50	24	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to E \in P$
51	26	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to F \in P$
52	28	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to W \in P$
53	30	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to X \in P$
54	32	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to Y \in P$
55	34	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to Z \in P$
56	36	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
57	38	simpld	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to x \in P$
58	57	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to x \in P$
59	1 2 3 8 5 6 7 4 14	inagne1	$⊢ φ \to D \neq E$
60	19 59	syl	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to D \neq E$
61	60	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to D \neq E$
62	40	adantr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to x \in (D I F)$
63		simpr	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to x K (E) W$
64	1 2 3 48 49 50 51 52 53 54 55 56 58 61 62 63	inagcgratrgncol	$⊢ ((φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \land x K (E) W) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
65	39	simprd	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to (x = E \lor x K (E) W)$
66	47 64 65	mpjaodan	$⊢ (φ \land (x \in P \land (x \in (D I F) \land (x = E \lor x K (E) W)))) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
67	18 66	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 inagcgratrgn

Proof