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 affine space id est a vector space ( called the free vectors class ) together with a function . associates to each vector a bijection from a set (called the space) to itself (here is retrieved from the operation.) Technically speaking, 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 a unique point of through the "action" of a vector of 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 GrpOpHom
Distinct variable group:   ,,,,,

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