Metamath Proof Explorer

Theorem inagcgratrgxfr

Description: In-angle transport with the target arms already normalized to S and T : cgrgptxfr transfers the segment point J to a point of ( S I T ) , and that one existential is eliminated here. (Contributed by JAG, 12-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 inagcgratrgxfr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 inagcgratrgxfr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 inagcgratrgxfr.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 inagcgratrgxfr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 inagcgratrgxfr.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
6 inagcgratrgxfr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
7 inagcgratrgxfr.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
8 inagcgratrgxfr.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
9 inagcgratrgxfr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
10 inagcgratrgxfr.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
11 inagcgratrgxfr.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
12 inagcgratrgxfr.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
13 inagcgratrgxfr.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
14 inagcgratrgxfr.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
15 inagcgratrgxfr.de ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
16 inagcgratrgxfr.1 ⊢ ( 𝜑 → 𝐽 ∈ ( 𝐷 𝐼 𝐹 ) )
17 inagcgratrgxfr.jw ⊢ ( 𝜑 → 𝐽 ( 𝐾 ‘ 𝐸 ) 𝑊 )
18 inagcgratrgxfr.sx ⊢ ( 𝜑 → 𝑆 ( 𝐾 ‘ 𝑌 ) 𝑋 )
19 inagcgratrgxfr.tz ⊢ ( 𝜑 → 𝑇 ( 𝐾 ‘ 𝑌 ) 𝑍 )
20 inagcgratrgxfr.2 ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑇 ”⟩ )
21 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
22 1 2 21 4 5 6 7 13 10 14 12 20 16 cgrgptxfr ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) )
23 simpl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝜑 )
24 23 4 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝐺 ∈ TarskiG )
25 23 5 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝐷 ∈ 𝑃 )
26 23 6 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝐸 ∈ 𝑃 )
27 23 8 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝑊 ∈ 𝑃 )
28 23 9 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝑋 ∈ 𝑃 )
29 23 10 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝑌 ∈ 𝑃 )
30 23 11 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝑍 ∈ 𝑃 )
31 23 12 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝐽 ∈ 𝑃 )
32 23 13 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝑆 ∈ 𝑃 )
33 23 14 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝑇 ∈ 𝑃 )
34 simpr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) )
35 34 simpld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝑦 ∈ 𝑃 )
36 23 15 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝐷 ≠ 𝐸 )
37 23 17 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝐽 ( 𝐾 ‘ 𝐸 ) 𝑊 )
38 23 18 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝑆 ( 𝐾 ‘ 𝑌 ) 𝑋 )
39 23 19 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝑇 ( 𝐾 ‘ 𝑌 ) 𝑍 )
40 34 simprd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) )
41 40 simpld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) )
42 41 simpld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) )
43 41 simprd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ )
44 1 2 3 24 25 26 27 28 29 30 31 32 33 35 36 37 38 39 42 43 inagcgratrgw ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑃 ∧ ( ( 𝑦 ∈ ( 𝑆 𝐼 𝑇 ) ∧ ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑦 ”⟩ ) ∧ ( ( 𝐷 ( dist ‘ 𝐺 ) 𝐽 ) = ( 𝑆 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐽 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑇 ) ) ) ) ) → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
45 22 44 rexlimddv ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )