This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑤 ) ( 𝑡 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑢 ) ) ) } )