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 36193
 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 36195 for binary relation. (df-cv 30040 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 36192 . 2 class L
2 vw . . 3 setvar 𝑤
3 cvv 3471 . . 3 class V
4 vt . . . . . . . 8 setvar 𝑡
54cv 1537 . . . . . . 7 class 𝑡
62cv 1537 . . . . . . . 8 class 𝑤
7 clss 19678 . . . . . . . 8 class LSubSp
86, 7cfv 6328 . . . . . . 7 class (LSubSp‘𝑤)
95, 8wcel 2115 . . . . . 6 wff 𝑡 ∈ (LSubSp‘𝑤)
10 vu . . . . . . . 8 setvar 𝑢
1110cv 1537 . . . . . . 7 class 𝑢
1211, 8wcel 2115 . . . . . 6 wff 𝑢 ∈ (LSubSp‘𝑤)
139, 12wa 399 . . . . 5 wff (𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤))
145, 11wpss 3911 . . . . . 6 wff 𝑡𝑢
15 vs . . . . . . . . . . 11 setvar 𝑠
1615cv 1537 . . . . . . . . . 10 class 𝑠
175, 16wpss 3911 . . . . . . . . 9 wff 𝑡𝑠
1816, 11wpss 3911 . . . . . . . . 9 wff 𝑠𝑢
1917, 18wa 399 . . . . . . . 8 wff (𝑡𝑠𝑠𝑢)
2019, 15, 8wrex 3127 . . . . . . 7 wff 𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)
2120wn 3 . . . . . 6 wff ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)
2214, 21wa 399 . . . . 5 wff (𝑡𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢))
2313, 22wa 399 . . . 4 wff ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)))
2423, 4, 10copab 5101 . . 3 class {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)))}
252, 3, 24cmpt 5119 . 2 class (𝑤 ∈ V ↦ {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)))})
261, 25wceq 1538 1 wff L = (𝑤 ∈ V ↦ {⟨𝑡, 𝑢⟩ ∣ ((𝑡 ∈ (LSubSp‘𝑤) ∧ 𝑢 ∈ (LSubSp‘𝑤)) ∧ (𝑡𝑢 ∧ ¬ ∃𝑠 ∈ (LSubSp‘𝑤)(𝑡𝑠𝑠𝑢)))})
 Colors of variables: wff setvar class This definition is referenced by:  lcvfbr  36194
 Copyright terms: Public domain W3C validator