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 = ( w e. _V |-> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsh
 |-  LSHyp
1 vw
 |-  w
2 cvv
 |-  _V
3 vs
 |-  s
4 clss
 |-  LSubSp
5 1 cv
 |-  w
6 5 4 cfv
 |-  ( LSubSp ` w )
7 3 cv
 |-  s
8 cbs
 |-  Base
9 5 8 cfv
 |-  ( Base ` w )
10 7 9 wne
 |-  s =/= ( Base ` w )
11 vv
 |-  v
12 clspn
 |-  LSpan
13 5 12 cfv
 |-  ( LSpan ` w )
14 11 cv
 |-  v
15 14 csn
 |-  { v }
16 7 15 cun
 |-  ( s u. { v } )
17 16 13 cfv
 |-  ( ( LSpan ` w ) ` ( s u. { v } ) )
18 17 9 wceq
 |-  ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w )
19 18 11 9 wrex
 |-  E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w )
20 10 19 wa
 |-  ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) )
21 20 3 6 crab
 |-  { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) }
22 1 2 21 cmpt
 |-  ( w e. _V |-> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } )
23 0 22 wceq
 |-  LSHyp = ( w e. _V |-> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } )