Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-line Structured version   Visualization version   GIF version

Definition df-line 45130
Description: Definition of lines passing through two different points in a left module (or any extended structure having a base set, an addition, and a scalar multiplication). (Contributed by AV, 14-Jan-2023.)
Assertion
Ref Expression
df-line LineM = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠𝑤)𝑥)(+g𝑤)(𝑡( ·𝑠𝑤)𝑦))}))
Distinct variable group:   𝑡,𝑝,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-line
StepHypRef Expression
1 cline 45128 . 2 class LineM
2 vw . . 3 setvar 𝑤
3 cvv 3444 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1537 . . . . 5 class 𝑤
7 cbs 16478 . . . . 5 class Base
86, 7cfv 6328 . . . 4 class (Base‘𝑤)
94cv 1537 . . . . . 6 class 𝑥
109csn 4528 . . . . 5 class {𝑥}
118, 10cdif 3881 . . . 4 class ((Base‘𝑤) ∖ {𝑥})
12 vp . . . . . . . 8 setvar 𝑝
1312cv 1537 . . . . . . 7 class 𝑝
14 csca 16563 . . . . . . . . . . . 12 class Scalar
156, 14cfv 6328 . . . . . . . . . . 11 class (Scalar‘𝑤)
16 cur 19247 . . . . . . . . . . 11 class 1r
1715, 16cfv 6328 . . . . . . . . . 10 class (1r‘(Scalar‘𝑤))
18 vt . . . . . . . . . . 11 setvar 𝑡
1918cv 1537 . . . . . . . . . 10 class 𝑡
20 csg 18100 . . . . . . . . . . 11 class -g
2115, 20cfv 6328 . . . . . . . . . 10 class (-g‘(Scalar‘𝑤))
2217, 19, 21co 7139 . . . . . . . . 9 class ((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)
23 cvsca 16564 . . . . . . . . . 10 class ·𝑠
246, 23cfv 6328 . . . . . . . . 9 class ( ·𝑠𝑤)
2522, 9, 24co 7139 . . . . . . . 8 class (((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠𝑤)𝑥)
265cv 1537 . . . . . . . . 9 class 𝑦
2719, 26, 24co 7139 . . . . . . . 8 class (𝑡( ·𝑠𝑤)𝑦)
28 cplusg 16560 . . . . . . . . 9 class +g
296, 28cfv 6328 . . . . . . . 8 class (+g𝑤)
3025, 27, 29co 7139 . . . . . . 7 class ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠𝑤)𝑥)(+g𝑤)(𝑡( ·𝑠𝑤)𝑦))
3113, 30wceq 1538 . . . . . 6 wff 𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠𝑤)𝑥)(+g𝑤)(𝑡( ·𝑠𝑤)𝑦))
3215, 7cfv 6328 . . . . . 6 class (Base‘(Scalar‘𝑤))
3331, 18, 32wrex 3110 . . . . 5 wff 𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠𝑤)𝑥)(+g𝑤)(𝑡( ·𝑠𝑤)𝑦))
3433, 12, 8crab 3113 . . . 4 class {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠𝑤)𝑥)(+g𝑤)(𝑡( ·𝑠𝑤)𝑦))}
354, 5, 8, 11, 34cmpo 7141 . . 3 class (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠𝑤)𝑥)(+g𝑤)(𝑡( ·𝑠𝑤)𝑦))})
362, 3, 35cmpt 5113 . 2 class (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠𝑤)𝑥)(+g𝑤)(𝑡( ·𝑠𝑤)𝑦))}))
371, 36wceq 1538 1 wff LineM = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ ((Base‘𝑤) ∖ {𝑥}) ↦ {𝑝 ∈ (Base‘𝑤) ∣ ∃𝑡 ∈ (Base‘(Scalar‘𝑤))𝑝 = ((((1r‘(Scalar‘𝑤))(-g‘(Scalar‘𝑤))𝑡)( ·𝑠𝑤)𝑥)(+g𝑤)(𝑡( ·𝑠𝑤)𝑦))}))
Colors of variables: wff setvar class
This definition is referenced by:  lines  45132
  Copyright terms: Public domain W3C validator