Definition df-leag 25732

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	|- ≤∠ = ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x (inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> (cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } )

Distinct variable group:   a, b, g, x

Detailed syntax breakdown of Definition df-leag

Step	Hyp	Ref	Expression
1		cleag 25727	. 2 class ≤∠
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		va	. . . . . . . 8 setvar a
5	4	cv 1482	. . . . . . 7 class a
6	2	cv 1482	. . . . . . . . 9 class g
7		cbs 15857	. . . . . . . . 9 class Base
8	6, 7	cfv 5888	. . . . . . . 8 class ( Base ` g )
9		cc0 9936	. . . . . . . . 9 class 0
10		c3 11071	. . . . . . . . 9 class 3
11		cfzo 12465	. . . . . . . . 9 class ..^
12	9, 10, 11	co 6650	. . . . . . . 8 class ( 0..^ 3 )
13		cmap 7857	. . . . . . . 8 class ^m
14	8, 12, 13	co 6650	. . . . . . 7 class ( ( Base ` g ) ^m ( 0..^ 3 ) )
15	5, 14	wcel 1990	. . . . . 6 wff a e. ( ( Base ` g ) ^m ( 0..^ 3 ) )
16		vb	. . . . . . . 8 setvar b
17	16	cv 1482	. . . . . . 7 class b
18	17, 14	wcel 1990	. . . . . 6 wff b e. ( ( Base ` g ) ^m ( 0..^ 3 ) )
19	15, 18	wa 384	. . . . 5 wff ( a e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) )
20		vx	. . . . . . . . 9 setvar x
21	20	cv 1482	. . . . . . . 8 class x
22	9, 17	cfv 5888	. . . . . . . . 9 class ( b ` 0 )
23		c1 9937	. . . . . . . . . 10 class 1
24	23, 17	cfv 5888	. . . . . . . . 9 class ( b ` 1 )
25		c2 11070	. . . . . . . . . 10 class 2
26	25, 17	cfv 5888	. . . . . . . . 9 class ( b ` 2 )
27	22, 24, 26	cs3 13587	. . . . . . . 8 class <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) ">
28		cinag 25726	. . . . . . . . 9 class inA
29	6, 28	cfv 5888	. . . . . . . 8 class (inA ` g )
30	21, 27, 29	wbr 4653	. . . . . . 7 wff x (inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) ">
31	9, 5	cfv 5888	. . . . . . . . 9 class ( a ` 0 )
32	23, 5	cfv 5888	. . . . . . . . 9 class ( a ` 1 )
33	25, 5	cfv 5888	. . . . . . . . 9 class ( a ` 2 )
34	31, 32, 33	cs3 13587	. . . . . . . 8 class <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) ">
35	22, 24, 21	cs3 13587	. . . . . . . 8 class <" ( b ` 0 ) ( b ` 1 ) x ">
36		ccgra 25699	. . . . . . . . 9 class cgrA
37	6, 36	cfv 5888	. . . . . . . 8 class (cgrA ` g )
38	34, 35, 37	wbr 4653	. . . . . . 7 wff <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> (cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x ">
39	30, 38	wa 384	. . . . . 6 wff ( x (inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> (cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> )
40	39, 20, 8	wrex 2913	. . . . 5 wff E. x e. ( Base ` g ) ( x (inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> (cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> )
41	19, 40	wa 384	. . . 4 wff ( ( a e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x (inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> (cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) )
42	41, 4, 16	copab 4712	. . 3 class { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x (inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> (cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) }
43	2, 3, 42	cmpt 4729	. 2 class ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x (inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> (cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } )
44	1, 43	wceq 1483	1 wff ≤∠ = ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) /\ b e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ E. x e. ( Base ` g ) ( x (inA ` g ) <" ( b ` 0 ) ( b ` 1 ) ( b ` 2 ) "> /\ <" ( a ` 0 ) ( a ` 1 ) ( a ` 2 ) "> (cgrA ` g ) <" ( b ` 0 ) ( b ` 1 ) x "> ) ) } )

This definition is referenced by:  isleag  25733