Metamath Proof Explorer

Theorem isinagd

Description: Sufficient conditions for in-angle relation, deduction version. (Contributed by Thierry Arnoux, 20-Oct-2020)

Ref Expression
Hypotheses isinag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isinag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
isinag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
isinag.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
isinag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
isinag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
isinag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
isinagd.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
isinagd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
isinagd.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
isinagd.2 ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
isinagd.3 ⊢ ( 𝜑 → 𝑋 ≠ 𝐵 )
isinagd.4 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 𝐼 𝐶 ) )
isinagd.5 ⊢ ( 𝜑 → ( 𝑌 = 𝐵 ∨ 𝑌 ( 𝐾 ‘ 𝐵 ) 𝑋 ) )
Assertion isinagd ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )

Proof

Step Hyp Ref Expression
1 isinag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isinag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 isinag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 isinag.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
5 isinag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 isinag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 isinag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 isinagd.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
9 isinagd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
10 isinagd.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
11 isinagd.2 ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
12 isinagd.3 ⊢ ( 𝜑 → 𝑋 ≠ 𝐵 )
13 isinagd.4 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 𝐼 𝐶 ) )
14 isinagd.5 ⊢ ( 𝜑 → ( 𝑌 = 𝐵 ∨ 𝑌 ( 𝐾 ‘ 𝐵 ) 𝑋 ) )
15 10 11 12 3jca ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → 𝑥 = 𝑌 )
17 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝐴 𝐼 𝐶 ) = ( 𝐴 𝐼 𝐶 ) )
18 16 17 eleq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ↔ 𝑌 ∈ ( 𝐴 𝐼 𝐶 ) ) )
19 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → 𝐵 = 𝐵 )
20 16 19 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝑥 = 𝐵 ↔ 𝑌 = 𝐵 ) )
21 16 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ↔ 𝑌 ( 𝐾 ‘ 𝐵 ) 𝑋 ) )
22 20 21 orbi12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ↔ ( 𝑌 = 𝐵 ∨ 𝑌 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) )
23 18 22 anbi12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ↔ ( 𝑌 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑌 = 𝐵 ∨ 𝑌 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) )
24 13 14 jca ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑌 = 𝐵 ∨ 𝑌 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) )
25 9 23 24 rspcedvd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) )
26 15 25 jca ⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) )
27 1 2 3 4 5 6 7 8 isinag ⊢ ( 𝜑 → ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ) )
28 26 27 mpbird ⊢ ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )