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

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