Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-raffsp Unicode version

Definition df-raffsp 25603
Description: Define a  RR affine space id est a  RR vector space  x ( called the free vectors class ) together with a function  y.  y associates to each vector a bijection from a set  t (called the space) to itself (here  t is retrieved from the operation.) Technically speaking,  y is a faithful (i.e. injective) and transitive group action (id est a group homomorphism whose range is the underlying set of a symmetry group ). Informally speaking the aim of all of that is to associate to each point of  t a unique point of  t through the "action" of a vector of  x and thus to formalize the idea of translation. When we have embedded the idea of translation it is easy to define a repere and thus all the cartesian geometry is available. (Contributed by FL, 29-Aug-2010.)
Assertion
Ref Expression
df-raffsp  |-  RAffSp  =  { <. x ,  y >.  |  ( x  e. 
RVec  /\  E. t ( y  e.  ( ( 1st `  x ) GrpOpHom  ( SymGrp `  t )
)  /\  y : ran  ( 1st `  x
) -1-1-> t  /\  A. a  e.  t  A. b  e.  t  E. v  e.  ran  ( 1st `  x ) ( ( y `  v ) `
 a )  =  b ) ) }
Distinct variable group:    x, y, t, a, b, v

Detailed syntax breakdown of Definition df-raffsp
StepHypRef Expression
1 craffsp 25602 . 2  class  RAffSp
2 vx . . . . . 6  set  x
32cv 1631 . . . . 5  class  x
4 cvr 25592 . . . . 5  class  RVec
53, 4wcel 1696 . . . 4  wff  x  e. 
RVec
6 vy . . . . . . . 8  set  y
76cv 1631 . . . . . . 7  class  y
8 c1st 6136 . . . . . . . . 9  class  1st
93, 8cfv 5271 . . . . . . . 8  class  ( 1st `  x )
10 vt . . . . . . . . . 10  set  t
1110cv 1631 . . . . . . . . 9  class  t
12 csymg 14785 . . . . . . . . 9  class  SymGrp
1311, 12cfv 5271 . . . . . . . 8  class  ( SymGrp `  t )
14 cghom 21040 . . . . . . . 8  class GrpOpHom
159, 13, 14co 5874 . . . . . . 7  class  ( ( 1st `  x ) GrpOpHom  ( SymGrp `  t )
)
167, 15wcel 1696 . . . . . 6  wff  y  e.  ( ( 1st `  x
) GrpOpHom  ( SymGrp `  t )
)
179crn 4706 . . . . . . 7  class  ran  ( 1st `  x )
1817, 11, 7wf1 5268 . . . . . 6  wff  y : ran  ( 1st `  x
) -1-1-> t
19 va . . . . . . . . . . . 12  set  a
2019cv 1631 . . . . . . . . . . 11  class  a
21 vv . . . . . . . . . . . . 13  set  v
2221cv 1631 . . . . . . . . . . . 12  class  v
2322, 7cfv 5271 . . . . . . . . . . 11  class  ( y `
 v )
2420, 23cfv 5271 . . . . . . . . . 10  class  ( ( y `  v ) `
 a )
25 vb . . . . . . . . . . 11  set  b
2625cv 1631 . . . . . . . . . 10  class  b
2724, 26wceq 1632 . . . . . . . . 9  wff  ( ( y `  v ) `
 a )  =  b
2827, 21, 17wrex 2557 . . . . . . . 8  wff  E. v  e.  ran  ( 1st `  x
) ( ( y `
 v ) `  a )  =  b
2928, 25, 11wral 2556 . . . . . . 7  wff  A. b  e.  t  E. v  e.  ran  ( 1st `  x
) ( ( y `
 v ) `  a )  =  b
3029, 19, 11wral 2556 . . . . . 6  wff  A. a  e.  t  A. b  e.  t  E. v  e.  ran  ( 1st `  x
) ( ( y `
 v ) `  a )  =  b
3116, 18, 30w3a 934 . . . . 5  wff  ( y  e.  ( ( 1st `  x ) GrpOpHom  ( SymGrp `  t ) )  /\  y : ran  ( 1st `  x ) -1-1-> t  /\  A. a  e.  t  A. b  e.  t  E. v  e.  ran  ( 1st `  x ) ( ( y `  v ) `
 a )  =  b )
3231, 10wex 1531 . . . 4  wff  E. t
( y  e.  ( ( 1st `  x
) GrpOpHom  ( SymGrp `  t )
)  /\  y : ran  ( 1st `  x
) -1-1-> t  /\  A. a  e.  t  A. b  e.  t  E. v  e.  ran  ( 1st `  x ) ( ( y `  v ) `
 a )  =  b )
335, 32wa 358 . . 3  wff  ( x  e.  RVec  /\  E. t
( y  e.  ( ( 1st `  x
) GrpOpHom  ( SymGrp `  t )
)  /\  y : ran  ( 1st `  x
) -1-1-> t  /\  A. a  e.  t  A. b  e.  t  E. v  e.  ran  ( 1st `  x ) ( ( y `  v ) `
 a )  =  b ) )
3433, 2, 6copab 4092 . 2  class  { <. x ,  y >.  |  ( x  e.  RVec  /\  E. t ( y  e.  ( ( 1st `  x
) GrpOpHom  ( SymGrp `  t )
)  /\  y : ran  ( 1st `  x
) -1-1-> t  /\  A. a  e.  t  A. b  e.  t  E. v  e.  ran  ( 1st `  x ) ( ( y `  v ) `
 a )  =  b ) ) }
351, 34wceq 1632 1  wff  RAffSp  =  { <. x ,  y >.  |  ( x  e. 
RVec  /\  E. t ( y  e.  ( ( 1st `  x ) GrpOpHom  ( SymGrp `  t )
)  /\  y : ran  ( 1st `  x
) -1-1-> t  /\  A. a  e.  t  A. b  e.  t  E. v  e.  ran  ( 1st `  x ) ( ( y `  v ) `
 a )  =  b ) ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator