Definition df-inag 28845

Description: Definition of the geometrical "in angle" relation. (Contributed by Thierry Arnoux, 15-Aug-2020.)

Assertion

Ref	Expression
df-inag	⊢ inA = (𝑔 ∈ V ↦ {⟨𝑝, 𝑡⟩ ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))})

Distinct variable group:   𝑔,𝑝,𝑡,𝑥

Detailed syntax breakdown of Definition df-inag

Step	Hyp	Ref	Expression
1		cinag 28843	. 2 class inA
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4		vp	. . . . . . . 8 setvar 𝑝
5	4	cv 1539	. . . . . . 7 class 𝑝
6	2	cv 1539	. . . . . . . 8 class 𝑔
7		cbs 17247	. . . . . . . 8 class Base
8	6, 7	cfv 6561	. . . . . . 7 class (Base‘𝑔)
9	5, 8	wcel 2108	. . . . . 6 wff 𝑝 ∈ (Base‘𝑔)
10		vt	. . . . . . . 8 setvar 𝑡
11	10	cv 1539	. . . . . . 7 class 𝑡
12		cc0 11155	. . . . . . . . 9 class 0
13		c3 12322	. . . . . . . . 9 class 3
14		cfzo 13694	. . . . . . . . 9 class ..^
15	12, 13, 14	co 7431	. . . . . . . 8 class (0..^3)
16		cmap 8866	. . . . . . . 8 class ↑m
17	8, 15, 16	co 7431	. . . . . . 7 class ((Base‘𝑔) ↑m (0..^3))
18	11, 17	wcel 2108	. . . . . 6 wff 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))
19	9, 18	wa 395	. . . . 5 wff (𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3)))
20	12, 11	cfv 6561	. . . . . . . 8 class (𝑡‘0)
21		c1 11156	. . . . . . . . 9 class 1
22	21, 11	cfv 6561	. . . . . . . 8 class (𝑡‘1)
23	20, 22	wne 2940	. . . . . . 7 wff (𝑡‘0) ≠ (𝑡‘1)
24		c2 12321	. . . . . . . . 9 class 2
25	24, 11	cfv 6561	. . . . . . . 8 class (𝑡‘2)
26	25, 22	wne 2940	. . . . . . 7 wff (𝑡‘2) ≠ (𝑡‘1)
27	5, 22	wne 2940	. . . . . . 7 wff 𝑝 ≠ (𝑡‘1)
28	23, 26, 27	w3a 1087	. . . . . 6 wff ((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1))
29		vx	. . . . . . . . . 10 setvar 𝑥
30	29	cv 1539	. . . . . . . . 9 class 𝑥
31		citv 28441	. . . . . . . . . . 11 class Itv
32	6, 31	cfv 6561	. . . . . . . . . 10 class (Itv‘𝑔)
33	20, 25, 32	co 7431	. . . . . . . . 9 class ((𝑡‘0)(Itv‘𝑔)(𝑡‘2))
34	30, 33	wcel 2108	. . . . . . . 8 wff 𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2))
35	30, 22	wceq 1540	. . . . . . . . 9 wff 𝑥 = (𝑡‘1)
36		chlg 28608	. . . . . . . . . . . 12 class hlG
37	6, 36	cfv 6561	. . . . . . . . . . 11 class (hlG‘𝑔)
38	22, 37	cfv 6561	. . . . . . . . . 10 class ((hlG‘𝑔)‘(𝑡‘1))
39	30, 5, 38	wbr 5143	. . . . . . . . 9 wff 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝
40	35, 39	wo 848	. . . . . . . 8 wff (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝)
41	34, 40	wa 395	. . . . . . 7 wff (𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))
42	41, 29, 8	wrex 3070	. . . . . 6 wff ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))
43	28, 42	wa 395	. . . . 5 wff (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝)))
44	19, 43	wa 395	. . . 4 wff ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))
45	44, 4, 10	copab 5205	. . 3 class {⟨𝑝, 𝑡⟩ ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))}
46	2, 3, 45	cmpt 5225	. 2 class (𝑔 ∈ V ↦ {⟨𝑝, 𝑡⟩ ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))})
47	1, 46	wceq 1540	1 wff inA = (𝑔 ∈ V ↦ {⟨𝑝, 𝑡⟩ ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))})

This definition is referenced by:  isinag  28846