Metamath Proof Explorer

Definition df-inag

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

Ref Expression
Assertion df-inag 
|- inA = ( g e. _V |-> { <. p , t >. | ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinag 
 |-  inA
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vp 
 |-  p
4 vt 
 |-  t
5 3 cv 
 |-  p
6 cbs 
 |-  Base
7 1 cv 
 |-  g
8 7 6 cfv 
 |-  ( Base ` g )
9 5 8 wcel 
 |-  p e. ( Base ` g )
10 4 cv 
 |-  t
11 cmap 
 |-  ^m
12 cc0 
 |-  0
13 cfzo 
 |-  ..^
14 c3 
 |-  3
15 12 14 13 co 
 |-  ( 0 ..^ 3 )
16 8 15 11 co 
 |-  ( ( Base ` g ) ^m ( 0 ..^ 3 ) )
17 10 16 wcel 
 |-  t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) )
18 9 17 wa 
 |-  ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) )
19 12 10 cfv 
 |-  ( t ` 0 )
20 c1 
 |-  1
21 20 10 cfv 
 |-  ( t ` 1 )
22 19 21 wne 
 |-  ( t ` 0 ) =/= ( t ` 1 )
23 c2 
 |-  2
24 23 10 cfv 
 |-  ( t ` 2 )
25 24 21 wne 
 |-  ( t ` 2 ) =/= ( t ` 1 )
26 5 21 wne 
 |-  p =/= ( t ` 1 )
27 22 25 26 w3a 
 |-  ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) )
28 vx 
 |-  x
29 28 cv 
 |-  x
30 citv 
 |-  Itv
31 7 30 cfv 
 |-  ( Itv ` g )
32 19 24 31 co 
 |-  ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) )
33 29 32 wcel 
 |-  x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) )
34 29 21 wceq 
 |-  x = ( t ` 1 )
35 chlg 
 |-  hlG
36 7 35 cfv 
 |-  ( hlG ` g )
37 21 36 cfv 
 |-  ( ( hlG ` g ) ` ( t ` 1 ) )
38 29 5 37 wbr 
 |-  x ( ( hlG ` g ) ` ( t ` 1 ) ) p
39 34 38 wo 
 |-  ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p )
40 33 39 wa 
 |-  ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) )
41 40 28 8 wrex 
 |-  E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) )
42 27 41 wa 
 |-  ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) )
43 18 42 wa 
 |-  ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) ) )
44 43 3 4 copab 
 |-  { <. p , t >. | ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) }
45 1 2 44 cmpt 
 |-  ( g e. _V |-> { <. p , t >. | ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) } )
46 0 45 wceq 
 |-  inA = ( g e. _V |-> { <. p , t >. | ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) ( Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( ( hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) } )