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	$⊢ φ \to X \in P$
	isinag.a	$⊢ φ \to A \in P$
	isinag.b	$⊢ φ \to B \in P$
	isinag.c	$⊢ φ \to C \in P$
	isinagd.g	$⊢ φ \to G \in V$
	isinagd.y	$⊢ φ \to Y \in P$
	isinagd.1	$⊢ φ \to A \neq B$
	isinagd.2	$⊢ φ \to C \neq B$
	isinagd.3	$⊢ φ \to X \neq B$
	isinagd.4	$⊢ φ \to Y \in (A I C)$
	isinagd.5	$⊢ φ \to (Y = B \lor Y K (B) X)$
Assertion	isinagd	$⊢ φ \to X \in_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$

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	$⊢ φ \to X \in P$
5		isinag.a	$⊢ φ \to A \in P$
6		isinag.b	$⊢ φ \to B \in P$
7		isinag.c	$⊢ φ \to C \in P$
8		isinagd.g	$⊢ φ \to G \in V$
9		isinagd.y	$⊢ φ \to Y \in P$
10		isinagd.1	$⊢ φ \to A \neq B$
11		isinagd.2	$⊢ φ \to C \neq B$
12		isinagd.3	$⊢ φ \to X \neq B$
13		isinagd.4	$⊢ φ \to Y \in (A I C)$
14		isinagd.5	$⊢ φ \to (Y = B \lor Y K (B) X)$
15	10 11 12	3jca	$⊢ φ \to (A \neq B \land C \neq B \land X \neq B)$
16		simpr	$⊢ (φ \land x = Y) \to x = Y$
17		eqidd	$⊢ (φ \land x = Y) \to A I C = A I C$
18	16 17	eleq12d	$⊢ (φ \land x = Y) \to (x \in (A I C) \leftrightarrow Y \in (A I C))$
19		eqidd	$⊢ (φ \land x = Y) \to B = B$
20	16 19	eqeq12d	$⊢ (φ \land x = Y) \to (x = B \leftrightarrow Y = B)$
21	16	breq1d	$⊢ (φ \land x = Y) \to (x K (B) X \leftrightarrow Y K (B) X)$
22	20 21	orbi12d	$⊢ (φ \land x = Y) \to ((x = B \lor x K (B) X) \leftrightarrow (Y = B \lor Y K (B) X))$
23	18 22	anbi12d	$⊢ (φ \land x = Y) \to ((x \in (A I C) \land (x = B \lor x K (B) X)) \leftrightarrow (Y \in (A I C) \land (Y = B \lor Y K (B) X)))$
24	13 14	jca	$⊢ φ \to (Y \in (A I C) \land (Y = B \lor Y K (B) X))$
25	9 23 24	rspcedvd	$⊢ φ \to \exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X))$
26	15 25	jca	$⊢ φ \to ((A \neq B \land C \neq B \land X \neq B) \land \exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X)))$
27	1 2 3 4 5 6 7 8	isinag	$⊢ φ \to (X \in_{𝒢}^{∠} (G) ⟨“ A B C ”⟩ \leftrightarrow ((A \neq B \land C \neq B \land X \neq B) \land \exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X))))$
28	26 27	mpbird	$⊢ φ \to X \in_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$

Metamath Proof Explorer

Theorem isinagd

Proof