Metamath Proof Explorer

Theorem inagcgrasubhl

Description: In-angle transport, degenerate branch (i): the sub-angle <" D E W "> is **null**, W lying on ray E D . The witness is not constructed -- it is X , the target's own first arm -- and cgrahlb supplies the copied angle from the two ray degeneracies. No GeoCoq counterpart: GeoCoq's branch only locates a witness supplied by its universal statement. (Contributed by JAG, 12-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 inagcgrasubhl.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 inagcgrasubhl.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 inagcgrasubhl.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 inagcgrasubhl.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 inagcgrasubhl.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
6 inagcgrasubhl.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
7 inagcgrasubhl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
8 inagcgrasubhl.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
9 inagcgrasubhl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
10 inagcgrasubhl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
11 inagcgrasubhl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
12 inagcgrasubhl.cgb ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
13 inagcgrasubhl.1 ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑊 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑣 = 𝑋 ) → 𝑣 = 𝑋 )
15 14 breq1d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝑋 ) → ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ↔ 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) )
16 eqidd ⊢ ( ( 𝜑 ∧ 𝑣 = 𝑋 ) → 𝑋 = 𝑋 )
17 eqidd ⊢ ( ( 𝜑 ∧ 𝑣 = 𝑋 ) → 𝑌 = 𝑌 )
18 16 17 14 s3eqd ⊢ ( ( 𝜑 ∧ 𝑣 = 𝑋 ) → ⟨“ 𝑋 𝑌 𝑣 ”⟩ = ⟨“ 𝑋 𝑌 𝑋 ”⟩ )
19 18 breq2d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝑋 ) → ( ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ↔ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) )
20 15 19 anbi12d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝑋 ) → ( ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ↔ ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) ) )
21 1 2 3 4 5 6 7 9 10 11 12 cgrane3 ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
22 21 necomd ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
23 1 2 3 4 5 6 7 9 10 11 12 cgrane4 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
24 23 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
25 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
26 1 25 2 4 9 11 tgbtwntriv1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 𝐼 𝑍 ) )
27 1 2 3 9 9 10 4 22 hlid ⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝑌 ) 𝑋 )
28 27 olcd ⊢ ( 𝜑 → ( 𝑋 = 𝑌 ∨ 𝑋 ( 𝐾 ‘ 𝑌 ) 𝑋 ) )
29 1 2 3 9 9 10 11 4 9 22 24 22 26 28 isinagd ⊢ ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
30 1 2 3 25 4 5 6 8 9 10 9 13 27 cgrahlb ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑋 ”⟩ )
31 29 30 jca ⊢ ( 𝜑 → ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) )
32 9 20 31 rspcedvd ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )