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 ⊢ P = Base G
isinag.i ⊢ I = Itv ⁡ G
isinag.k ⊢ K = hl 𝒢 ⁡ G
isinag.x ⊢ φ → X ∈ P
isinag.a ⊢ φ → A ∈ P
isinag.b ⊢ φ → B ∈ P
isinag.c ⊢ φ → C ∈ P
isinagd.g ⊢ φ → G ∈ V
isinagd.y ⊢ φ → Y ∈ P
isinagd.1 ⊢ φ → A ≠ B
isinagd.2 ⊢ φ → C ≠ B
isinagd.3 ⊢ φ → X ≠ B
isinagd.4 ⊢ φ → Y ∈ A I C
isinagd.5 ⊢ φ → Y = B ∨ Y K ⁡ B X
Assertion isinagd ⊢ φ → X ∈ 𝒢 ∠ ⁡ G ⟨“ ABC ”⟩

Proof

Step Hyp Ref Expression
1 isinag.p ⊢ P = Base G
2 isinag.i ⊢ I = Itv ⁡ G
3 isinag.k ⊢ K = hl 𝒢 ⁡ G
4 isinag.x ⊢ φ → X ∈ P
5 isinag.a ⊢ φ → A ∈ P
6 isinag.b ⊢ φ → B ∈ P
7 isinag.c ⊢ φ → C ∈ P
8 isinagd.g ⊢ φ → G ∈ V
9 isinagd.y ⊢ φ → Y ∈ P
10 isinagd.1 ⊢ φ → A ≠ B
11 isinagd.2 ⊢ φ → C ≠ B
12 isinagd.3 ⊢ φ → X ≠ B
13 isinagd.4 ⊢ φ → Y ∈ A I C
14 isinagd.5 ⊢ φ → Y = B ∨ Y K ⁡ B X
15 10 11 12 3jca ⊢ φ → A ≠ B ∧ C ≠ B ∧ X ≠ B
16 simpr ⊢ φ ∧ x = Y → x = Y
17 eqidd ⊢ φ ∧ x = Y → A I C = A I C
18 16 17 eleq12d ⊢ φ ∧ x = Y → x ∈ A I C ↔ Y ∈ A I C
19 eqidd ⊢ φ ∧ x = Y → B = B
20 16 19 eqeq12d ⊢ φ ∧ x = Y → x = B ↔ Y = B
21 16 breq1d ⊢ φ ∧ x = Y → x K ⁡ B X ↔ Y K ⁡ B X
22 20 21 orbi12d ⊢ φ ∧ x = Y → x = B ∨ x K ⁡ B X ↔ Y = B ∨ Y K ⁡ B X
23 18 22 anbi12d ⊢ φ ∧ x = Y → x ∈ A I C ∧ x = B ∨ x K ⁡ B X ↔ Y ∈ A I C ∧ Y = B ∨ Y K ⁡ B X
24 13 14 jca ⊢ φ → Y ∈ A I C ∧ Y = B ∨ Y K ⁡ B X
25 9 23 24 rspcedvd ⊢ φ → ∃ x ∈ P x ∈ A I C ∧ x = B ∨ x K ⁡ B X
26 15 25 jca ⊢ φ → A ≠ B ∧ C ≠ B ∧ X ≠ B ∧ ∃ x ∈ P x ∈ A I C ∧ x = B ∨ x K ⁡ B X
27 1 2 3 4 5 6 7 8 isinag ⊢ φ → X ∈ 𝒢 ∠ ⁡ G ⟨“ ABC ”⟩ ↔ A ≠ B ∧ C ≠ B ∧ X ≠ B ∧ ∃ x ∈ P x ∈ A I C ∧ x = B ∨ x K ⁡ B X
28 26 27 mpbird ⊢ φ → X ∈ 𝒢 ∠ ⁡ G ⟨“ ABC ”⟩