Theorem inagcgratrgw

Description: inagcgratrgmain with the existential introduced at its own witness Q . Split out so that the substitution instance is built once, at the top level, rather than under the existential eliminations that produce S , T and Q . (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	inagcgratrgmain.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	inagcgratrgmain.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	inagcgratrgmain.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	inagcgratrgmain.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	inagcgratrgmain.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	inagcgratrgmain.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	inagcgratrgmain.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
	inagcgratrgmain.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	inagcgratrgmain.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	inagcgratrgmain.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	inagcgratrgmain.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
	inagcgratrgmain.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
	inagcgratrgmain.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
	inagcgratrgmain.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
	inagcgratrgmain.de	⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
	inagcgratrgmain.jw	⊢ ( 𝜑 → 𝐽 ( 𝐾 ‘ 𝐸 ) 𝑊 )
	inagcgratrgmain.sx	⊢ ( 𝜑 → 𝑆 ( 𝐾 ‘ 𝑌 ) 𝑋 )
	inagcgratrgmain.tz	⊢ ( 𝜑 → 𝑇 ( 𝐾 ‘ 𝑌 ) 𝑍 )
	inagcgratrgmain.q1	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑆 𝐼 𝑇 ) )
	inagcgratrgmain.sub	⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑄 ”⟩ )
Assertion	inagcgratrgw	⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		inagcgratrgmain.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		inagcgratrgmain.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		inagcgratrgmain.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
4		inagcgratrgmain.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		inagcgratrgmain.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
6		inagcgratrgmain.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
7		inagcgratrgmain.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
8		inagcgratrgmain.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
9		inagcgratrgmain.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
10		inagcgratrgmain.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
11		inagcgratrgmain.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
12		inagcgratrgmain.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
13		inagcgratrgmain.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
14		inagcgratrgmain.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
15		inagcgratrgmain.de	⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
16		inagcgratrgmain.jw	⊢ ( 𝜑 → 𝐽 ( 𝐾 ‘ 𝐸 ) 𝑊 )
17		inagcgratrgmain.sx	⊢ ( 𝜑 → 𝑆 ( 𝐾 ‘ 𝑌 ) 𝑋 )
18		inagcgratrgmain.tz	⊢ ( 𝜑 → 𝑇 ( 𝐾 ‘ 𝑌 ) 𝑍 )
19		inagcgratrgmain.q1	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑆 𝐼 𝑇 ) )
20		inagcgratrgmain.sub	⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑄 ”⟩ )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑣 = 𝑄 ) → 𝑣 = 𝑄 )
22	21	breq1d	⊢ ( ( 𝜑 ∧ 𝑣 = 𝑄 ) → ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ↔ 𝑄 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) )
23		eqidd	⊢ ( ( 𝜑 ∧ 𝑣 = 𝑄 ) → 𝑋 = 𝑋 )
24		eqidd	⊢ ( ( 𝜑 ∧ 𝑣 = 𝑄 ) → 𝑌 = 𝑌 )
25	23 24 21	s3eqd	⊢ ( ( 𝜑 ∧ 𝑣 = 𝑄 ) → ⟨“ 𝑋 𝑌 𝑣 ”⟩ = ⟨“ 𝑋 𝑌 𝑄 ”⟩ )
26	25	breq2d	⊢ ( ( 𝜑 ∧ 𝑣 = 𝑄 ) → ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ↔ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑄 ”⟩ ) )
27	22 26	anbi12d	⊢ ( ( 𝜑 ∧ 𝑣 = 𝑄 ) → ( ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ↔ ( 𝑄 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑄 ”⟩ ) ) )
28		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
29	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 28	inagcgratrgmain	⊢ ( 𝜑 → ( 𝑄 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑄 ”⟩ ) )
30	14 27 29	rspcedvd	⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )