Definition df-inag

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinag	⊢ inA
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vp	⊢ 𝑝
4		vt	⊢ 𝑡
5	3	cv	⊢ 𝑝
6		cbs	⊢ Base
7	1	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( Base ‘ 𝑔 )
9	5 8	wcel	⊢ 𝑝 ∈ ( Base ‘ 𝑔 )
10	4	cv	⊢ 𝑡
11		cmap	⊢ ↑m
12		cc0	⊢ 0
13		cfzo	⊢ ..^
14		c3	⊢ 3
15	12 14 13	co	⊢ ( 0 ..^ 3 )
16	8 15 11	co	⊢ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) )
17	10 16	wcel	⊢ 𝑡 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) )
18	9 17	wa	⊢ ( 𝑝 ∈ ( Base ‘ 𝑔 ) ∧ 𝑡 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) )
19	12 10	cfv	⊢ ( 𝑡 ‘ 0 )
20		c1	⊢ 1
21	20 10	cfv	⊢ ( 𝑡 ‘ 1 )
22	19 21	wne	⊢ ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 )
23		c2	⊢ 2
24	23 10	cfv	⊢ ( 𝑡 ‘ 2 )
25	24 21	wne	⊢ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 )
26	5 21	wne	⊢ 𝑝 ≠ ( 𝑡 ‘ 1 )
27	22 25 26	w3a	⊢ ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) )
28		vx	⊢ 𝑥
29	28	cv	⊢ 𝑥
30		citv	⊢ Itv
31	7 30	cfv	⊢ ( Itv ‘ 𝑔 )
32	19 24 31	co	⊢ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) )
33	29 32	wcel	⊢ 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) )
34	29 21	wceq	⊢ 𝑥 = ( 𝑡 ‘ 1 )
35		chlg	⊢ hlG
36	7 35	cfv	⊢ ( hlG ‘ 𝑔 )
37	21 36	cfv	⊢ ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) )
38	29 5 37	wbr	⊢ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝
39	34 38	wo	⊢ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 )
40	33 39	wa	⊢ ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) )
41	40 28 8	wrex	⊢ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) )
42	27 41	wa	⊢ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) )
43	18 42	wa	⊢ ( ( 𝑝 ∈ ( Base ‘ 𝑔 ) ∧ 𝑡 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) )
44	43 3 4	copab	⊢ { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ ( Base ‘ 𝑔 ) ∧ 𝑡 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) }
45	1 2 44	cmpt	⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ ( Base ‘ 𝑔 ) ∧ 𝑡 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } )
46	0 45	wceq	⊢ inA = ( 𝑔 ∈ V ↦ { ⟨ 𝑝 , 𝑡 ⟩ ∣ ( ( 𝑝 ∈ ( Base ‘ 𝑔 ) ∧ 𝑡 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ) ∧ ( ( ( 𝑡 ‘ 0 ) ≠ ( 𝑡 ‘ 1 ) ∧ ( 𝑡 ‘ 2 ) ≠ ( 𝑡 ‘ 1 ) ∧ 𝑝 ≠ ( 𝑡 ‘ 1 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑥 ∈ ( ( 𝑡 ‘ 0 ) ( Itv ‘ 𝑔 ) ( 𝑡 ‘ 2 ) ) ∧ ( 𝑥 = ( 𝑡 ‘ 1 ) ∨ 𝑥 ( ( hlG ‘ 𝑔 ) ‘ ( 𝑡 ‘ 1 ) ) 𝑝 ) ) ) ) } )