Metamath Proof Explorer

Theorem lshpset

Description: The set of all hyperplanes of a left module or left vector space. The vector v is called a generating vector for the hyperplane. (Contributed by NM, 29-Jun-2014)

Ref Expression
Hypotheses lshpset.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lshpset.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lshpset.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lshpset.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
Assertion lshpset ( 𝑊 ∈ 𝑋 → 𝐻 = { 𝑠 ∈ 𝑆 ∣ ( 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) } )

Proof

Step Hyp Ref Expression
1 lshpset.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lshpset.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lshpset.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
4 lshpset.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
5 elex ⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
6 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = ( LSubSp ‘ 𝑊 ) )
7 6 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = 𝑆 )
8 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
9 8 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
10 9 neeq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑠 ≠ ( Base ‘ 𝑤 ) ↔ 𝑠 ≠ 𝑉 ) )
11 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = ( LSpan ‘ 𝑊 ) )
12 11 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = 𝑁 )
13 12 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) )
14 13 9 eqeq12d ⊢ ( 𝑤 = 𝑊 → ( ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ↔ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) )
15 9 14 rexeqbidv ⊢ ( 𝑤 = 𝑊 → ( ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ↔ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) )
16 10 15 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ) ↔ ( 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
17 7 16 rabeqbidv ⊢ ( 𝑤 = 𝑊 → { 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ∣ ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ) } = { 𝑠 ∈ 𝑆 ∣ ( 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) } )
18 df-lshyp ⊢ LSHyp = ( 𝑤 ∈ V ↦ { 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ∣ ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ) } )
19 3 fvexi ⊢ 𝑆 ∈ V
20 19 rabex ⊢ { 𝑠 ∈ 𝑆 ∣ ( 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) } ∈ V
21 17 18 20 fvmpt ⊢ ( 𝑊 ∈ V → ( LSHyp ‘ 𝑊 ) = { 𝑠 ∈ 𝑆 ∣ ( 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) } )
22 5 21 syl ⊢ ( 𝑊 ∈ 𝑋 → ( LSHyp ‘ 𝑊 ) = { 𝑠 ∈ 𝑆 ∣ ( 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) } )
23 4 22 syl5eq ⊢ ( 𝑊 ∈ 𝑋 → 𝐻 = { 𝑠 ∈ 𝑆 ∣ ( 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) } )