Definition df-leag

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cleag	⊢ ≤∠
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		va	⊢ 𝑎
4		vb	⊢ 𝑏
5	3	cv	⊢ 𝑎
6		cbs	⊢ Base
7	1	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( Base ‘ 𝑔 )
9		cmap	⊢ ↑m
10		cc0	⊢ 0
11		cfzo	⊢ ..^
12		c3	⊢ 3
13	10 12 11	co	⊢ ( 0 ..^ 3 )
14	8 13 9	co	⊢ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) )
15	5 14	wcel	⊢ 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) )
16	4	cv	⊢ 𝑏
17	16 14	wcel	⊢ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) )
18	15 17	wa	⊢ ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) )
19		vx	⊢ 𝑥
20	19	cv	⊢ 𝑥
21		cinag	⊢ inA
22	7 21	cfv	⊢ ( inA ‘ 𝑔 )
23	10 16	cfv	⊢ ( 𝑏 ‘ 0 )
24		c1	⊢ 1
25	24 16	cfv	⊢ ( 𝑏 ‘ 1 )
26		c2	⊢ 2
27	26 16	cfv	⊢ ( 𝑏 ‘ 2 )
28	23 25 27	cs3	⊢ ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩
29	20 28 22	wbr	⊢ 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩
30	10 5	cfv	⊢ ( 𝑎 ‘ 0 )
31	24 5	cfv	⊢ ( 𝑎 ‘ 1 )
32	26 5	cfv	⊢ ( 𝑎 ‘ 2 )
33	30 31 32	cs3	⊢ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩
34		ccgra	⊢ cgrA
35	7 34	cfv	⊢ ( cgrA ‘ 𝑔 )
36	23 25 20	cs3	⊢ ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩
37	33 36 35	wbr	⊢ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩
38	29 37	wa	⊢ ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ )
39	38 19 8	wrex	⊢ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ )
40	18 39	wa	⊢ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) )
41	40 3 4	copab	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) }
42	1 2 41	cmpt	⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } )
43	0 42	wceq	⊢ ≤∠ = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ( inA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) ( 𝑏 ‘ 2 ) ”⟩ ∧ ⟨“ ( 𝑎 ‘ 0 ) ( 𝑎 ‘ 1 ) ( 𝑎 ‘ 2 ) ”⟩ ( cgrA ‘ 𝑔 ) ⟨“ ( 𝑏 ‘ 0 ) ( 𝑏 ‘ 1 ) 𝑥 ”⟩ ) ) } )