Metamath Proof Explorer


Definition df-lshyp

Description: Define the set of all hyperplanes of a left module or left vector space. Also called co-atoms, these are subspaces that are one dimension less than the full space. (Contributed by NM, 29-Jun-2014)

Ref Expression
Assertion df-lshyp LSHyp = ( 𝑤 ∈ V ↦ { 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ∣ ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsh LSHyp
1 vw 𝑤
2 cvv V
3 vs 𝑠
4 clss LSubSp
5 1 cv 𝑤
6 5 4 cfv ( LSubSp ‘ 𝑤 )
7 3 cv 𝑠
8 cbs Base
9 5 8 cfv ( Base ‘ 𝑤 )
10 7 9 wne 𝑠 ≠ ( Base ‘ 𝑤 )
11 vv 𝑣
12 clspn LSpan
13 5 12 cfv ( LSpan ‘ 𝑤 )
14 11 cv 𝑣
15 14 csn { 𝑣 }
16 7 15 cun ( 𝑠 ∪ { 𝑣 } )
17 16 13 cfv ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) )
18 17 9 wceq ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 )
19 18 11 9 wrex 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 )
20 10 19 wa ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) )
21 20 3 6 crab { 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ∣ ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ) }
22 1 2 21 cmpt ( 𝑤 ∈ V ↦ { 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ∣ ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ) } )
23 0 22 wceq LSHyp = ( 𝑤 ∈ V ↦ { 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ∣ ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ) } )