Metamath Proof Explorer

Theorem inagcgratrgmain

Description: In-angle transport, the non-degenerate main case, with its three constructions carried as hypotheses: J the segment point from isinag , S and T the normalized target arms from iscgrag , and Q the transferred point from cgrgptxfr . Concludes the body of cgrainag 's existential at the witness Q . **No acopy and no half-plane fact**: the witness is the transferred point, not a fresh angle copy, which is what removes the non-collinearity obligations. (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 ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑄 ”⟩ )
inagcgratrgmain.m ⊢ − = ( dist ‘ 𝐺 )
Assertion inagcgratrgmain ( 𝜑 → ( 𝑄 ( 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 inagcgratrgmain.m ⊢ − = ( dist ‘ 𝐺 )
22 1 2 3 12 8 9 4 17 hlne1 ⊢ ( 𝜑 → 𝑆 ≠ 𝑌 )
23 1 2 3 13 10 9 4 18 hlne1 ⊢ ( 𝜑 → 𝑇 ≠ 𝑌 )
24 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
25 1 21 2 24 4 5 6 11 12 9 14 20 cgr3simp2 ⊢ ( 𝜑 → ( 𝐸 − 𝐽 ) = ( 𝑌 − 𝑄 ) )
26 1 2 3 11 7 6 4 16 hlne1 ⊢ ( 𝜑 → 𝐽 ≠ 𝐸 )
27 26 necomd ⊢ ( 𝜑 → 𝐸 ≠ 𝐽 )
28 1 21 2 4 6 11 9 14 25 27 tgcgrneq ⊢ ( 𝜑 → 𝑌 ≠ 𝑄 )
29 28 necomd ⊢ ( 𝜑 → 𝑄 ≠ 𝑌 )
30 1 2 3 14 14 9 4 29 hlid ⊢ ( 𝜑 → 𝑄 ( 𝐾 ‘ 𝑌 ) 𝑄 )
31 30 olcd ⊢ ( 𝜑 → ( 𝑄 = 𝑌 ∨ 𝑄 ( 𝐾 ‘ 𝑌 ) 𝑄 ) )
32 1 2 3 14 12 9 13 4 14 22 23 29 19 31 isinagd ⊢ ( 𝜑 → 𝑄 ( inA ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑇 ”⟩ )
33 1 2 3 12 8 9 4 17 hlcomd ⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝑌 ) 𝑆 )
34 1 2 3 13 10 9 4 18 hlcomd ⊢ ( 𝜑 → 𝑍 ( 𝐾 ‘ 𝑌 ) 𝑇 )
35 1 2 3 14 12 9 13 4 32 8 10 14 33 34 30 inaghl ⊢ ( 𝜑 → 𝑄 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
36 1 2 4 3 5 6 11 12 9 14 15 27 20 cgrcgra ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑆 𝑌 𝑄 ”⟩ )
37 1 2 3 4 5 6 11 12 9 14 36 8 33 cgrahl1 ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑄 ”⟩ )
38 1 2 4 3 5 6 11 8 9 14 37 cgracom ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑄 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐽 ”⟩ )
39 1 2 3 11 7 6 4 16 hlcomd ⊢ ( 𝜑 → 𝑊 ( 𝐾 ‘ 𝐸 ) 𝐽 )
40 1 2 3 4 8 9 14 5 6 11 38 7 39 cgrahl2 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑄 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑊 ”⟩ )
41 1 2 4 3 8 9 14 5 6 7 40 cgracom ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑄 ”⟩ )
42 35 41 jca ⊢ ( 𝜑 → ( 𝑄 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑄 ”⟩ ) )