Metamath Proof Explorer


Definition df-lcv

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 A ( W ) B is read " B covers A " or " A is covered by B " , and it means that B is larger than A and there is nothing in between. See lcvbr for binary relation. ( df-cv analog.) (Contributed by NM, 7-Jan-2015)

Ref Expression
Assertion df-lcv L = ( 𝑤 ∈ V ↦ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡𝑠𝑠𝑢 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clcv L
1 vw 𝑤
2 cvv V
3 vt 𝑡
4 vu 𝑢
5 3 cv 𝑡
6 clss LSubSp
7 1 cv 𝑤
8 7 6 cfv ( LSubSp ‘ 𝑤 )
9 5 8 wcel 𝑡 ∈ ( LSubSp ‘ 𝑤 )
10 4 cv 𝑢
11 10 8 wcel 𝑢 ∈ ( LSubSp ‘ 𝑤 )
12 9 11 wa ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) )
13 5 10 wpss 𝑡𝑢
14 vs 𝑠
15 14 cv 𝑠
16 5 15 wpss 𝑡𝑠
17 15 10 wpss 𝑠𝑢
18 16 17 wa ( 𝑡𝑠𝑠𝑢 )
19 18 14 8 wrex 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡𝑠𝑠𝑢 )
20 19 wn ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡𝑠𝑠𝑢 )
21 13 20 wa ( 𝑡𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡𝑠𝑠𝑢 ) )
22 12 21 wa ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡𝑠𝑠𝑢 ) ) )
23 22 3 4 copab { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡𝑠𝑠𝑢 ) ) ) }
24 1 2 23 cmpt ( 𝑤 ∈ V ↦ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡𝑠𝑠𝑢 ) ) ) } )
25 0 24 wceq L = ( 𝑤 ∈ V ↦ { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑡 ∈ ( LSubSp ‘ 𝑤 ) ∧ 𝑢 ∈ ( LSubSp ‘ 𝑤 ) ) ∧ ( 𝑡𝑢 ∧ ¬ ∃ 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ( 𝑡𝑠𝑠𝑢 ) ) ) } )