Definition df-leag 28854

Description: Definition of the geometrical "angle less than" relation. Definition 11.27 of [Schwabhauser] p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020.)

Assertion

Ref	Expression
df-leag	⊢ ≤∠ = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))})

Distinct variable group:   𝑎,𝑏,𝑔,𝑥

Detailed syntax breakdown of Definition df-leag

Step	Hyp	Ref	Expression
1		cleag 28844	. 2 class ≤∠
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1539	. . . . . . 7 class 𝑎
6	2	cv 1539	. . . . . . . . 9 class 𝑔
7		cbs 17247	. . . . . . . . 9 class Base
8	6, 7	cfv 6561	. . . . . . . 8 class (Base‘𝑔)
9		cc0 11155	. . . . . . . . 9 class 0
10		c3 12322	. . . . . . . . 9 class 3
11		cfzo 13694	. . . . . . . . 9 class ..^
12	9, 10, 11	co 7431	. . . . . . . 8 class (0..^3)
13		cmap 8866	. . . . . . . 8 class ↑m
14	8, 12, 13	co 7431	. . . . . . 7 class ((Base‘𝑔) ↑m (0..^3))
15	5, 14	wcel 2108	. . . . . 6 wff 𝑎 ∈ ((Base‘𝑔) ↑m (0..^3))
16		vb	. . . . . . . 8 setvar 𝑏
17	16	cv 1539	. . . . . . 7 class 𝑏
18	17, 14	wcel 2108	. . . . . 6 wff 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))
19	15, 18	wa 395	. . . . 5 wff (𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3)))
20		vx	. . . . . . . . 9 setvar 𝑥
21	20	cv 1539	. . . . . . . 8 class 𝑥
22	9, 17	cfv 6561	. . . . . . . . 9 class (𝑏‘0)
23		c1 11156	. . . . . . . . . 10 class 1
24	23, 17	cfv 6561	. . . . . . . . 9 class (𝑏‘1)
25		c2 12321	. . . . . . . . . 10 class 2
26	25, 17	cfv 6561	. . . . . . . . 9 class (𝑏‘2)
27	22, 24, 26	cs3 14881	. . . . . . . 8 class ⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩
28		cinag 28843	. . . . . . . . 9 class inA
29	6, 28	cfv 6561	. . . . . . . 8 class (inA‘𝑔)
30	21, 27, 29	wbr 5143	. . . . . . 7 wff 𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩
31	9, 5	cfv 6561	. . . . . . . . 9 class (𝑎‘0)
32	23, 5	cfv 6561	. . . . . . . . 9 class (𝑎‘1)
33	25, 5	cfv 6561	. . . . . . . . 9 class (𝑎‘2)
34	31, 32, 33	cs3 14881	. . . . . . . 8 class ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩
35	22, 24, 21	cs3 14881	. . . . . . . 8 class ⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩
36		ccgra 28815	. . . . . . . . 9 class cgrA
37	6, 36	cfv 6561	. . . . . . . 8 class (cgrA‘𝑔)
38	34, 35, 37	wbr 5143	. . . . . . 7 wff ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩
39	30, 38	wa 395	. . . . . 6 wff (𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩)
40	39, 20, 8	wrex 3070	. . . . 5 wff ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩)
41	19, 40	wa 395	. . . 4 wff ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))
42	41, 4, 16	copab 5205	. . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))}
43	2, 3, 42	cmpt 5225	. 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))})
44	1, 43	wceq 1540	1 wff ≤∠ = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑m (0..^3)) ∧ 𝑏 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥(inA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)(𝑏‘2)”⟩ ∧ ⟨“(𝑎‘0)(𝑎‘1)(𝑎‘2)”⟩(cgrA‘𝑔)⟨“(𝑏‘0)(𝑏‘1)𝑥”⟩))})

This definition is referenced by:  isleag  28855