Metamath Proof Explorer

Definition df-ray

Description: Define the Ray function. This function generates the set of all points that lie on the ray starting at p and passing through a . Definition 6.8 of Schwabhauser p. 44. (Contributed by Scott Fenton, 21-Oct-2013)

Ref Expression
Assertion df-ray 
|- Ray = { <. <. p , a >. , r >. | E. n e. NN ( ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a ) /\ r = { x e. ( EE ` n ) | p OutsideOf <. a , x >. } ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cray 
 |-  Ray
1 vp 
 |-  p
2 va 
 |-  a
3 vr 
 |-  r
4 vn 
 |-  n
5 cn 
 |-  NN
6 1 cv 
 |-  p
7 cee 
 |-  EE
8 4 cv 
 |-  n
9 8 7 cfv 
 |-  ( EE ` n )
10 6 9 wcel 
 |-  p e. ( EE ` n )
11 2 cv 
 |-  a
12 11 9 wcel 
 |-  a e. ( EE ` n )
13 6 11 wne 
 |-  p =/= a
14 10 12 13 w3a 
 |-  ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a )
15 3 cv 
 |-  r
16 vx 
 |-  x
17 coutsideof 
 |-  OutsideOf
18 16 cv 
 |-  x
19 11 18 cop 
 |-  <. a , x >.
20 6 19 17 wbr 
 |-  p OutsideOf <. a , x >.
21 20 16 9 crab 
 |-  { x e. ( EE ` n ) | p OutsideOf <. a , x >. }
22 15 21 wceq 
 |-  r = { x e. ( EE ` n ) | p OutsideOf <. a , x >. }
23 14 22 wa 
 |-  ( ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a ) /\ r = { x e. ( EE ` n ) | p OutsideOf <. a , x >. } )
24 23 4 5 wrex 
 |-  E. n e. NN ( ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a ) /\ r = { x e. ( EE ` n ) | p OutsideOf <. a , x >. } )
25 24 1 2 3 coprab 
 |-  { <. <. p , a >. , r >. | E. n e. NN ( ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a ) /\ r = { x e. ( EE ` n ) | p OutsideOf <. a , x >. } ) }
26 0 25 wceq 
 |-  Ray = { <. <. p , a >. , r >. | E. n e. NN ( ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a ) /\ r = { x e. ( EE ` n ) | p OutsideOf <. a , x >. } ) }