isinag

Description: Property for point X to lie in the angle <" A B C "> . Definition 11.23 of Schwabhauser p. 101. (Contributed by Thierry Arnoux, 15-Aug-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$
	isinag.g	$⊢ φ \to G \in V$
Assertion	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))))$

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		isinag.g	$⊢ φ \to G \in V$
9		simpr	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to t = ⟨“ A B C ”⟩$
10	9	fveq1d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to t (0) = ⟨“ A B C ”⟩ (0)$
11	9	fveq1d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to t (1) = ⟨“ A B C ”⟩ (1)$
12	10 11	neeq12d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to (t (0) \neq t (1) \leftrightarrow ⟨“ A B C ”⟩ (0) \neq ⟨“ A B C ”⟩ (1))$
13	9	fveq1d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to t (2) = ⟨“ A B C ”⟩ (2)$
14	13 11	neeq12d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to (t (2) \neq t (1) \leftrightarrow ⟨“ A B C ”⟩ (2) \neq ⟨“ A B C ”⟩ (1))$
15		simpl	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to p = X$
16	15 11	neeq12d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to (p \neq t (1) \leftrightarrow X \neq ⟨“ A B C ”⟩ (1))$
17	12 14 16	3anbi123d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \leftrightarrow (⟨“ A B C ”⟩ (0) \neq ⟨“ A B C ”⟩ (1) \land ⟨“ A B C ”⟩ (2) \neq ⟨“ A B C ”⟩ (1) \land X \neq ⟨“ A B C ”⟩ (1)))$
18	10 13	oveq12d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to t (0) I t (2) = ⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2)$
19	18	eleq2d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to (x \in (t (0) I t (2)) \leftrightarrow x \in (⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2)))$
20	11	eqeq2d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to (x = t (1) \leftrightarrow x = ⟨“ A B C ”⟩ (1))$
21		eqidd	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to x = x$
22	11	fveq2d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to K (t (1)) = K (⟨“ A B C ”⟩ (1))$
23	21 22 15	breq123d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to (x K (t (1)) p \leftrightarrow x K (⟨“ A B C ”⟩ (1)) X)$
24	20 23	orbi12d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to ((x = t (1) \lor x K (t (1)) p) \leftrightarrow (x = ⟨“ A B C ”⟩ (1) \lor x K (⟨“ A B C ”⟩ (1)) X))$
25	19 24	anbi12d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to ((x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p)) \leftrightarrow (x \in (⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2)) \land (x = ⟨“ A B C ”⟩ (1) \lor x K (⟨“ A B C ”⟩ (1)) X)))$
26	25	rexbidv	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to (\exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p)) \leftrightarrow \exists x \in P (x \in (⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2)) \land (x = ⟨“ A B C ”⟩ (1) \lor x K (⟨“ A B C ”⟩ (1)) X)))$
27	17 26	anbi12d	$⊢ (p = X \land t = ⟨“ A B C ”⟩) \to (((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))) \leftrightarrow ((⟨“ A B C ”⟩ (0) \neq ⟨“ A B C ”⟩ (1) \land ⟨“ A B C ”⟩ (2) \neq ⟨“ A B C ”⟩ (1) \land X \neq ⟨“ A B C ”⟩ (1)) \land \exists x \in P (x \in (⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2)) \land (x = ⟨“ A B C ”⟩ (1) \lor x K (⟨“ A B C ”⟩ (1)) X))))$
28		eqid	$⊢ \{⟨p, t⟩ \| ((p \in P \land t \in (P^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))))\} = \{⟨p, t⟩ \| ((p \in P \land t \in (P^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))))\}$
29	27 28	brab2a	$⊢ X \{⟨p, t⟩ \| ((p \in P \land t \in (P^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))))\} ⟨“ A B C ”⟩ \leftrightarrow ((X \in P \land ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})) \land ((⟨“ A B C ”⟩ (0) \neq ⟨“ A B C ”⟩ (1) \land ⟨“ A B C ”⟩ (2) \neq ⟨“ A B C ”⟩ (1) \land X \neq ⟨“ A B C ”⟩ (1)) \land \exists x \in P (x \in (⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2)) \land (x = ⟨“ A B C ”⟩ (1) \lor x K (⟨“ A B C ”⟩ (1)) X))))$
30		s3fv0	$⊢ A \in P \to ⟨“ A B C ”⟩ (0) = A$
31	5 30	syl	$⊢ φ \to ⟨“ A B C ”⟩ (0) = A$
32		s3fv1	$⊢ B \in P \to ⟨“ A B C ”⟩ (1) = B$
33	6 32	syl	$⊢ φ \to ⟨“ A B C ”⟩ (1) = B$
34	31 33	neeq12d	$⊢ φ \to (⟨“ A B C ”⟩ (0) \neq ⟨“ A B C ”⟩ (1) \leftrightarrow A \neq B)$
35		s3fv2	$⊢ C \in P \to ⟨“ A B C ”⟩ (2) = C$
36	7 35	syl	$⊢ φ \to ⟨“ A B C ”⟩ (2) = C$
37	36 33	neeq12d	$⊢ φ \to (⟨“ A B C ”⟩ (2) \neq ⟨“ A B C ”⟩ (1) \leftrightarrow C \neq B)$
38	33	neeq2d	$⊢ φ \to (X \neq ⟨“ A B C ”⟩ (1) \leftrightarrow X \neq B)$
39	34 37 38	3anbi123d	$⊢ φ \to ((⟨“ A B C ”⟩ (0) \neq ⟨“ A B C ”⟩ (1) \land ⟨“ A B C ”⟩ (2) \neq ⟨“ A B C ”⟩ (1) \land X \neq ⟨“ A B C ”⟩ (1)) \leftrightarrow (A \neq B \land C \neq B \land X \neq B))$
40	31 36	oveq12d	$⊢ φ \to ⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2) = A I C$
41	40	eleq2d	$⊢ φ \to (x \in (⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2)) \leftrightarrow x \in (A I C))$
42	33	eqeq2d	$⊢ φ \to (x = ⟨“ A B C ”⟩ (1) \leftrightarrow x = B)$
43	33	fveq2d	$⊢ φ \to K (⟨“ A B C ”⟩ (1)) = K (B)$
44	43	breqd	$⊢ φ \to (x K (⟨“ A B C ”⟩ (1)) X \leftrightarrow x K (B) X)$
45	42 44	orbi12d	$⊢ φ \to ((x = ⟨“ A B C ”⟩ (1) \lor x K (⟨“ A B C ”⟩ (1)) X) \leftrightarrow (x = B \lor x K (B) X))$
46	41 45	anbi12d	$⊢ φ \to ((x \in (⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2)) \land (x = ⟨“ A B C ”⟩ (1) \lor x K (⟨“ A B C ”⟩ (1)) X)) \leftrightarrow (x \in (A I C) \land (x = B \lor x K (B) X)))$
47	46	rexbidv	$⊢ φ \to (\exists x \in P (x \in (⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2)) \land (x = ⟨“ A B C ”⟩ (1) \lor x K (⟨“ A B C ”⟩ (1)) X)) \leftrightarrow \exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X)))$
48	39 47	anbi12d	$⊢ φ \to (((⟨“ A B C ”⟩ (0) \neq ⟨“ A B C ”⟩ (1) \land ⟨“ A B C ”⟩ (2) \neq ⟨“ A B C ”⟩ (1) \land X \neq ⟨“ A B C ”⟩ (1)) \land \exists x \in P (x \in (⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2)) \land (x = ⟨“ A B C ”⟩ (1) \lor x K (⟨“ A B C ”⟩ (1)) X))) \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))))$
49	48	anbi2d	$⊢ φ \to (((X \in P \land ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})) \land ((⟨“ A B C ”⟩ (0) \neq ⟨“ A B C ”⟩ (1) \land ⟨“ A B C ”⟩ (2) \neq ⟨“ A B C ”⟩ (1) \land X \neq ⟨“ A B C ”⟩ (1)) \land \exists x \in P (x \in (⟨“ A B C ”⟩ (0) I ⟨“ A B C ”⟩ (2)) \land (x = ⟨“ A B C ”⟩ (1) \lor x K (⟨“ A B C ”⟩ (1)) X)))) \leftrightarrow ((X \in P \land ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})) \land ((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)))))$
50	29 49	syl5bb	$⊢ φ \to (X \{⟨p, t⟩ \| ((p \in P \land t \in (P^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))))\} ⟨“ A B C ”⟩ \leftrightarrow ((X \in P \land ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})) \land ((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)))))$
51		elex	$⊢ G \in V \to G \in V$
52		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
53	52 1	eqtr4di	$⊢ g = G \to {Base}_{g} = P$
54	53	eleq2d	$⊢ g = G \to (p \in {Base}_{g} \leftrightarrow p \in P)$
55	53	oveq1d	$⊢ g = G \to {Base}_{g}^{(0 ..^3)} = P^{(0 ..^3)}$
56	55	eleq2d	$⊢ g = G \to (t \in ({Base}_{g}^{(0 ..^3)}) \leftrightarrow t \in (P^{(0 ..^3)}))$
57	54 56	anbi12d	$⊢ g = G \to ((p \in {Base}_{g} \land t \in ({Base}_{g}^{(0 ..^3)})) \leftrightarrow (p \in P \land t \in (P^{(0 ..^3)})))$
58		fveq2	$⊢ g = G \to Itv (g) = Itv (G)$
59	58 2	eqtr4di	$⊢ g = G \to Itv (g) = I$
60	59	oveqd	$⊢ g = G \to t (0) Itv (g) t (2) = t (0) I t (2)$
61	60	eleq2d	$⊢ g = G \to (x \in (t (0) Itv (g) t (2)) \leftrightarrow x \in (t (0) I t (2)))$
62		fveq2	$⊢ g = G \to {hl}_{𝒢} (g) = {hl}_{𝒢} (G)$
63	62 3	eqtr4di	$⊢ g = G \to {hl}_{𝒢} (g) = K$
64	63	fveq1d	$⊢ g = G \to {hl}_{𝒢} (g) (t (1)) = K (t (1))$
65	64	breqd	$⊢ g = G \to (x {hl}_{𝒢} (g) (t (1)) p \leftrightarrow x K (t (1)) p)$
66	65	orbi2d	$⊢ g = G \to ((x = t (1) \lor x {hl}_{𝒢} (g) (t (1)) p) \leftrightarrow (x = t (1) \lor x K (t (1)) p))$
67	61 66	anbi12d	$⊢ g = G \to ((x \in (t (0) Itv (g) t (2)) \land (x = t (1) \lor x {hl}_{𝒢} (g) (t (1)) p)) \leftrightarrow (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p)))$
68	53 67	rexeqbidv	$⊢ g = G \to (\exists x \in {Base}_{g} (x \in (t (0) Itv (g) t (2)) \land (x = t (1) \lor x {hl}_{𝒢} (g) (t (1)) p)) \leftrightarrow \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p)))$
69	68	anbi2d	$⊢ g = G \to (((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in {Base}_{g} (x \in (t (0) Itv (g) t (2)) \land (x = t (1) \lor x {hl}_{𝒢} (g) (t (1)) p))) \leftrightarrow ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))))$
70	57 69	anbi12d	$⊢ g = G \to (((p \in {Base}_{g} \land t \in ({Base}_{g}^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in {Base}_{g} (x \in (t (0) Itv (g) t (2)) \land (x = t (1) \lor x {hl}_{𝒢} (g) (t (1)) p)))) \leftrightarrow ((p \in P \land t \in (P^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p)))))$
71	70	opabbidv	$⊢ g = G \to \{⟨p, t⟩ \| ((p \in {Base}_{g} \land t \in ({Base}_{g}^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in {Base}_{g} (x \in (t (0) Itv (g) t (2)) \land (x = t (1) \lor x {hl}_{𝒢} (g) (t (1)) p))))\} = \{⟨p, t⟩ \| ((p \in P \land t \in (P^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))))\}$
72		df-inag	$⊢ \in_{𝒢}^{∠} = (g \in V ⟼ \{⟨p, t⟩ \| ((p \in {Base}_{g} \land t \in ({Base}_{g}^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in {Base}_{g} (x \in (t (0) Itv (g) t (2)) \land (x = t (1) \lor x {hl}_{𝒢} (g) (t (1)) p))))\})$
73	1	fvexi	$⊢ P \in V$
74		ovex	$⊢ P^{(0 ..^3)} \in V$
75	73 74	xpex	$⊢ P \times (P^{(0 ..^3)}) \in V$
76		opabssxp	$⊢ \{⟨p, t⟩ \| ((p \in P \land t \in (P^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))))\} \subseteq P \times (P^{(0 ..^3)})$
77	75 76	ssexi	$⊢ \{⟨p, t⟩ \| ((p \in P \land t \in (P^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))))\} \in V$
78	71 72 77	fvmpt	$⊢ G \in V \to \in_{𝒢}^{∠} (G) = \{⟨p, t⟩ \| ((p \in P \land t \in (P^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))))\}$
79	8 51 78	3syl	$⊢ φ \to \in_{𝒢}^{∠} (G) = \{⟨p, t⟩ \| ((p \in P \land t \in (P^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))))\}$
80	79	breqd	$⊢ φ \to (X \in_{𝒢}^{∠} (G) ⟨“ A B C ”⟩ \leftrightarrow X \{⟨p, t⟩ \| ((p \in P \land t \in (P^{(0 ..^3)})) \land ((t (0) \neq t (1) \land t (2) \neq t (1) \land p \neq t (1)) \land \exists x \in P (x \in (t (0) I t (2)) \land (x = t (1) \lor x K (t (1)) p))))\} ⟨“ A B C ”⟩)$
81	5 6 7	s3cld	$⊢ φ \to ⟨“ A B C ”⟩ \in Word P$
82		s3len	$⊢ \|⟨“ A B C ”⟩\| = 3$
83		3nn0	$⊢ 3 \in ℕ_{0}$
84		wrdmap	$⊢ (P \in V \land 3 \in ℕ_{0}) \to ((⟨“ A B C ”⟩ \in Word P \land \|⟨“ A B C ”⟩\| = 3) \leftrightarrow ⟨“ A B C ”⟩ \in (P^{(0 ..^3)}))$
85	73 83 84	mp2an	$⊢ (⟨“ A B C ”⟩ \in Word P \land \|⟨“ A B C ”⟩\| = 3) \leftrightarrow ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})$
86	81 82 85	sylanblc	$⊢ φ \to ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})$
87	4 86	jca	$⊢ φ \to (X \in P \land ⟨“ A B C ”⟩ \in (P^{(0 ..^3)}))$
88	87	biantrurd	$⊢ φ \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))) \leftrightarrow ((X \in P \land ⟨“ A B C ”⟩ \in (P^{(0 ..^3)})) \land ((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)))))$
89	50 80 88	3bitr4d	$⊢ φ \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))))$

Metamath Proof Explorer

Theorem isinag

Proof