Description: Two vectors whose zeroth coordinate is nonzero are equivalent if and only if they have the same representative in the (n-1)-dimensional affine subspace { x_0 = 1 } . For example, vectors in 3D space whose x coordinate is nonzero are equivalent iff they intersect at the plane x = 1 at the same point (also see section header). (Contributed by SN, 13-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prjspner01.e | |
|
prjspner01.f | |
||
prjspner01.b | |
||
prjspner01.w | |
||
prjspner01.t | |
||
prjspner01.s | |
||
prjspner01.0 | |
||
prjspner01.i | |
||
prjspner01.k | |
||
prjspner01.n | |
||
prjspner01.x | |
||
prjspner1.y | |
||
prjspner1.1 | |
||
prjspner1.2 | |
||
Assertion | prjspner1 | |