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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	inagcgrabtwn.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	inagcgrabtwn.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	inagcgrabtwn.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	inagcgrabtwn.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	inagcgrabtwn.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	inagcgrabtwn.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	inagcgrabtwn.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	inagcgrabtwn.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
	inagcgrabtwn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	inagcgrabtwn.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	inagcgrabtwn.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	inagcgrabtwn.cgb	⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
	inagcgrabtwn.1	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
	inagcgrabtwn.2	⊢ ( 𝜑 → ¬ ( 𝑊 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
Assertion	inagcgrabtwn	⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		inagcgrabtwn.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		inagcgrabtwn.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		inagcgrabtwn.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
4		inagcgrabtwn.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		inagcgrabtwn.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		inagcgrabtwn.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
7		inagcgrabtwn.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
8		inagcgrabtwn.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
9		inagcgrabtwn.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
10		inagcgrabtwn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11		inagcgrabtwn.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
12		inagcgrabtwn.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
13		inagcgrabtwn.cgb	⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
14		inagcgrabtwn.1	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
15		inagcgrabtwn.2	⊢ ( 𝜑 → ¬ ( 𝑊 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
16		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑣 ∈ 𝑃 )
17		simpll	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) )
18		simpll	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝜑 )
19	18 10	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ 𝑃 )
20	17 19	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑋 ∈ 𝑃 )
21	18 11	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ 𝑃 )
22	17 21	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑌 ∈ 𝑃 )
23	18 12	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ∈ 𝑃 )
24	17 23	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑍 ∈ 𝑃 )
25	18 5	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
26	17 25	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝐺 ∈ TarskiG )
27	1 2 3 5 6 7 8 10 11 12 13	cgrane3	⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
28	27	necomd	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
29	18 28	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ≠ 𝑌 )
30	17 29	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑋 ≠ 𝑌 )
31	1 2 3 5 6 7 8 10 11 12 13	cgrane4	⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
32	31	necomd	⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
33	18 32	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑍 ≠ 𝑌 )
34	17 33	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑍 ≠ 𝑌 )
35	18 6	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝐷 ∈ 𝑃 )
36	17 35	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝐷 ∈ 𝑃 )
37	18 7	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝐸 ∈ 𝑃 )
38	17 37	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝐸 ∈ 𝑃 )
39	18 9	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑊 ∈ 𝑃 )
40	17 39	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑊 ∈ 𝑃 )
41		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) )
42	41	simpld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ )
43	1 2 3 26 36 38 40 20 22 16 42	cgrane4	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑌 ≠ 𝑣 )
44	43	necomd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑣 ≠ 𝑌 )
45		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
46	1 2 45 5 6 7 8 10 11 12 13 14	cgrabtwn	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
47	18 46	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
48	17 47	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
49		eqidd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑌 = 𝑌 )
50	49	orcd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → ( 𝑌 = 𝑌 ∨ 𝑌 ( 𝐾 ‘ 𝑌 ) 𝑣 ) )
51	1 2 3 16 20 22 24 26 22 30 34 44 48 50	isinagd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
52	51 42	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) ) → ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
53		simplr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑐 ∈ 𝑃 )
54	1 4 2 5 6 7 9 15	ncolrot1	⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝑊 ) ∨ 𝐸 = 𝑊 ) )
55	18 54	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝑊 ) ∨ 𝐸 = 𝑊 ) )
56		simpr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) )
57	29	neneqd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → ¬ 𝑋 = 𝑌 )
58	56 57	jca	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ∧ ¬ 𝑋 = 𝑌 ) )
59		ioran	⊢ ( ¬ ( 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) ↔ ( ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ∧ ¬ 𝑋 = 𝑌 ) )
60	58 59	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → ¬ ( 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
61	1 4 2 25 19 21 53 60	ncolrot1	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑐 ) ∨ 𝑌 = 𝑐 ) )
62	1 2 45 25 35 37 39 19 21 53 4 55 61	acopy	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → ∃ 𝑣 ∈ 𝑃 ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ∧ 𝑣 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑐 ) )
63	52 62	reximddv3	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) ) → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
64	1 4 2 5 6 7 9 15	ncoltgdim2	⊢ ( 𝜑 → 𝐺 Dim_TarskiG≥ 2 )
65	1 2 4 5 64 10 11 28	tglowdim2ln	⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ¬ 𝑐 ∈ ( 𝑋 𝐿 𝑌 ) )
66	63 65	r19.29a	⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )

Metamath Proof Explorer

Theorem inagcgrabtwn

Proof