Metamath Proof Explorer

Theorem inagcgrasubbtwn

Description: In-angle transport, degenerate branch (ii): the sub-angle <" D E W "> is **flat**, E lying between D and W . The witness is built beyond Y on the ray opposite Y X with axtgsegcon , and flatcgra supplies the copied angle from the two betweennesses. The in-angle conjunct goes through inagbtwn , which carries the flatness up to the containing angle, then cgrabtwn across the congruence and isinagd on the target. (Contributed by JAG, 12-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 inagcgrasubbtwn.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 inagcgrasubbtwn.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 inagcgrasubbtwn.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 inagcgrasubbtwn.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 inagcgrasubbtwn.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
6 inagcgrasubbtwn.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
7 inagcgrasubbtwn.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
8 inagcgrasubbtwn.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
9 inagcgrasubbtwn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
10 inagcgrasubbtwn.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
11 inagcgrasubbtwn.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
12 inagcgrasubbtwn.in ⊢ ( 𝜑 → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
13 inagcgrasubbtwn.cgb ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
14 inagcgrasubbtwn.1 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) )
15 simplr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑣 ∈ 𝑃 )
16 simpll ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝜑 )
17 16 9 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑋 ∈ 𝑃 )
18 16 10 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑌 ∈ 𝑃 )
19 16 11 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑍 ∈ 𝑃 )
20 16 4 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝐺 ∈ TarskiG )
21 1 2 3 4 5 6 7 9 10 11 13 cgrane3 ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
22 21 necomd ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
23 16 22 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑋 ≠ 𝑌 )
24 1 2 3 4 5 6 7 9 10 11 13 cgrane4 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
25 24 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
26 16 25 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑍 ≠ 𝑌 )
27 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
28 simpr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) )
29 28 simprd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) )
30 29 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) = ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) )
31 1 27 2 20 17 18 18 15 30 23 tgcgrneq ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑌 ≠ 𝑣 )
32 31 necomd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑣 ≠ 𝑌 )
33 1 2 3 4 5 6 7 8 12 14 inagbtwn ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
34 1 2 27 4 5 6 7 9 10 11 13 33 cgrabtwn ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
35 16 34 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
36 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑌 = 𝑌 )
37 36 orcd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑌 = 𝑌 ∨ 𝑌 ( 𝐾 ‘ 𝑌 ) 𝑣 ) )
38 1 2 3 15 17 18 19 20 18 23 26 32 35 37 isinagd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
39 16 5 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝐷 ∈ 𝑃 )
40 16 6 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝐸 ∈ 𝑃 )
41 16 8 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑊 ∈ 𝑃 )
42 16 14 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝑊 ) )
43 28 simpld ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) )
44 1 2 3 8 5 6 7 4 12 inagne1 ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
45 16 44 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝐷 ≠ 𝐸 )
46 1 2 3 8 5 6 7 4 12 inagne3 ⊢ ( 𝜑 → 𝑊 ≠ 𝐸 )
47 16 46 syl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → 𝑊 ≠ 𝐸 )
48 1 2 27 20 39 40 41 17 18 15 42 43 45 47 23 32 flatcgra ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ )
49 38 48 jca ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) ) → ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
50 1 27 2 4 9 10 9 10 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑣 ) ∧ ( 𝑌 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝑌 ) ) )
51 49 50 reximddv3 ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )