inagcgrabtwn

Description: In-angle transport, degenerate branch (iii): the containing angle is **flat** while the sub-angle is not. This is the x = E disjunct of isinag , which the non-degenerate spine cannot reach. Unlike branches (i) and (ii) the copied angle must be *constructed*: the congruence hypothesis relates W to nothing on the target side, and acopy needs a point off line X Y to pick a side, which the collinear Z cannot be. ncoltgdim2 takes the dimension from this branch's own non-collinearity and tglowdim2ln produces that point. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	inagcgrabtwn.p	$⊢ P = {Base}_{G}$
	inagcgrabtwn.i	$⊢ I = Itv (G)$
	inagcgrabtwn.k	$⊢ K = {hl}_{𝒢} (G)$
	inagcgrabtwn.l	$⊢ L = {Line}_{𝒢} (G)$
	inagcgrabtwn.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	inagcgrabtwn.d	$⊢ φ \to D \in P$
	inagcgrabtwn.e	$⊢ φ \to E \in P$
	inagcgrabtwn.f	$⊢ φ \to F \in P$
	inagcgrabtwn.w	$⊢ φ \to W \in P$
	inagcgrabtwn.x	$⊢ φ \to X \in P$
	inagcgrabtwn.y	$⊢ φ \to Y \in P$
	inagcgrabtwn.z	$⊢ φ \to Z \in P$
	inagcgrabtwn.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
	inagcgrabtwn.1	$⊢ φ \to E \in (D I F)$
	inagcgrabtwn.2	$⊢ φ \to \neg (W \in (D L E) \lor D = E)$
Assertion	inagcgrabtwn	$⊢ φ \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		inagcgrabtwn.p	$⊢ P = {Base}_{G}$
2		inagcgrabtwn.i	$⊢ I = Itv (G)$
3		inagcgrabtwn.k	$⊢ K = {hl}_{𝒢} (G)$
4		inagcgrabtwn.l	$⊢ L = {Line}_{𝒢} (G)$
5		inagcgrabtwn.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		inagcgrabtwn.d	$⊢ φ \to D \in P$
7		inagcgrabtwn.e	$⊢ φ \to E \in P$
8		inagcgrabtwn.f	$⊢ φ \to F \in P$
9		inagcgrabtwn.w	$⊢ φ \to W \in P$
10		inagcgrabtwn.x	$⊢ φ \to X \in P$
11		inagcgrabtwn.y	$⊢ φ \to Y \in P$
12		inagcgrabtwn.z	$⊢ φ \to Z \in P$
13		inagcgrabtwn.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
14		inagcgrabtwn.1	$⊢ φ \to E \in (D I F)$
15		inagcgrabtwn.2	$⊢ φ \to \neg (W \in (D L E) \lor D = E)$
16		simplr	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to v \in P$
17		simpll	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to ((φ \land c \in P) \land \neg c \in (X L Y))$
18		simpll	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to φ$
19	18 10	syl	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to X \in P$
20	17 19	syl	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to X \in P$
21	18 11	syl	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to Y \in P$
22	17 21	syl	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to Y \in P$
23	18 12	syl	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to Z \in P$
24	17 23	syl	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to Z \in P$
25	18 5	syl	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to G \in 𝒢_{Tarski}$
26	17 25	syl	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to G \in 𝒢_{Tarski}$
27	1 2 3 5 6 7 8 10 11 12 13	cgrane3	$⊢ φ \to Y \neq X$
28	27	necomd	$⊢ φ \to X \neq Y$
29	18 28	syl	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to X \neq Y$
30	17 29	syl	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to X \neq Y$
31	1 2 3 5 6 7 8 10 11 12 13	cgrane4	$⊢ φ \to Y \neq Z$
32	31	necomd	$⊢ φ \to Z \neq Y$
33	18 32	syl	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to Z \neq Y$
34	17 33	syl	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to Z \neq Y$
35	18 6	syl	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to D \in P$
36	17 35	syl	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to D \in P$
37	18 7	syl	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to E \in P$
38	17 37	syl	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to E \in P$
39	18 9	syl	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to W \in P$
40	17 39	syl	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to W \in P$
41		simpr	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)$
42	41	simpld	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩$
43	1 2 3 26 36 38 40 20 22 16 42	cgrane4	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to Y \neq v$
44	43	necomd	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to v \neq Y$
45		eqid	$⊢ dist (G) = dist (G)$
46	1 2 45 5 6 7 8 10 11 12 13 14	cgrabtwn	$⊢ φ \to Y \in (X I Z)$
47	18 46	syl	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to Y \in (X I Z)$
48	17 47	syl	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to Y \in (X I Z)$
49		eqidd	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to Y = Y$
50	49	orcd	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to (Y = Y \lor Y K (Y) v)$
51	1 2 3 16 20 22 24 26 22 30 34 44 48 50	isinagd	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
52	51 42	jca	$⊢ ((((φ \land c \in P) \land \neg c \in (X L Y)) \land v \in P) \land (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)) \to (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
53		simplr	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to c \in P$
54	1 4 2 5 6 7 9 15	ncolrot1	$⊢ φ \to \neg (D \in (E L W) \lor E = W)$
55	18 54	syl	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to \neg (D \in (E L W) \lor E = W)$
56		simpr	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to \neg c \in (X L Y)$
57	29	neneqd	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to \neg X = Y$
58	56 57	jca	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to (\neg c \in (X L Y) \land \neg X = Y)$
59		ioran	$⊢ \neg (c \in (X L Y) \lor X = Y) \leftrightarrow (\neg c \in (X L Y) \land \neg X = Y)$
60	58 59	sylibr	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to \neg (c \in (X L Y) \lor X = Y)$
61	1 4 2 25 19 21 53 60	ncolrot1	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to \neg (X \in (Y L c) \lor Y = c)$
62	1 2 45 25 35 37 39 19 21 53 4 55 61	acopy	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to \exists v \in P (⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩ \land v {hp}_{𝒢} (G) (X L Y) c)$
63	52 62	reximddv3	$⊢ ((φ \land c \in P) \land \neg c \in (X L Y)) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
64	1 4 2 5 6 7 9 15	ncoltgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
65	1 2 4 5 64 10 11 28	tglowdim2ln	$⊢ φ \to \exists c \in P \neg c \in (X L Y)$
66	63 65	r19.29a	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$

Metamath Proof Explorer

Theorem inagcgrabtwn

Proof