Metamath Proof Explorer

Theorem inagcgratrgncol

Description: In-angle transport once the segment point J of isinag is on the ray E W : iscgrag normalizes the target arms and its two existentials are eliminated here, leaving inagcgratrgxfr to do the transfer. (Contributed by JAG, 12-Aug-2026)

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

Proof

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