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