Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lcv Structured version   Visualization version   GIF version

Definition df-lcv 33123
Description: Define the covering relation for subspaces of a left vector space. Similar to Definition 3.2.18 of [PtakPulmannova] p. 68. Ptak/Pulmannova's notation 𝐴( ⋖L𝑊)𝐵 is read "𝐵 covers 𝐴 " or "𝐴 is covered by 𝐵 " , and it means that 𝐵 is larger than 𝐴 and there is nothing in between. See lcvbr 33125 for binary relation. (df-cv 28324 analog.) (Contributed by NM, 7-Jan-2015.)
Assertion
Ref Expression
df-lcv L = (𝑤 ∈ V ↦ {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)))})
Distinct variable group:   𝑡,𝑠,𝑢,𝑤

Detailed syntax breakdown of Definition df-lcv
StepHypRef Expression
1 clcv 33122 . 2 class L
2 vw . . 3 setvar 𝑤
3 cvv 3168 . . 3 class V
4 vt . . . . . . . 8 setvar 𝑡
54cv 1473 . . . . . . 7 class 𝑡
62cv 1473 . . . . . . . 8 class 𝑤
7 clss 18695 . . . . . . . 8 class LSubSp
86, 7cfv 5786 . . . . . . 7 class (LSubSp‘𝑤)
95, 8wcel 1975 . . . . . 6 wff 𝑡 ∈ (LSubSp‘𝑤)
10 vu . . . . . . . 8 setvar 𝑢
1110cv 1473 . . . . . . 7 class 𝑢
1211, 8wcel 1975 . . . . . 6 wff 𝑢 ∈ (LSubSp‘𝑤)
139, 12wa 382 . . . . 5 wff (𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤))
145, 11wpss 3536 . . . . . 6 wff 𝑡𝑢
15 vs . . . . . . . . . . 11 setvar 𝑠
1615cv 1473 . . . . . . . . . 10 class 𝑠
175, 16wpss 3536 . . . . . . . . 9 wff 𝑡𝑠
1816, 11wpss 3536 . . . . . . . . 9 wff 𝑠𝑢
1917, 18wa 382 . . . . . . . 8 wff (𝑡𝑠𝑠𝑢)
2019, 15, 8wrex 2892 . . . . . . 7 wff 𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)
2120wn 3 . . . . . 6 wff ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)
2214, 21wa 382 . . . . 5 wff (𝑡𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢))
2313, 22wa 382 . . . 4 wff ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)))
2423, 4, 10copab 4632 . . 3 class {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)))}
252, 3, 24cmpt 4633 . 2 class (𝑤 ∈ V ↦ {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)))})
261, 25wceq 1474 1 wff L = (𝑤 ∈ V ↦ {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)))})
Colors of variables: wff setvar class
This definition is referenced by:  lcvfbr  33124
  Copyright terms: Public domain W3C validator