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 ) ) } )