Metamath Proof Explorer


Theorem islshp

Description: The predicate "is a hyperplane" (of a left module or left vector space). (Contributed by NM, 29-Jun-2014)

Ref Expression
Hypotheses lshpset.v 𝑉 = ( Base ‘ 𝑊 )
lshpset.n 𝑁 = ( LSpan ‘ 𝑊 )
lshpset.s 𝑆 = ( LSubSp ‘ 𝑊 )
lshpset.h 𝐻 = ( LSHyp ‘ 𝑊 )
Assertion islshp ( 𝑊𝑋 → ( 𝑈𝐻 ↔ ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 lshpset.v 𝑉 = ( Base ‘ 𝑊 )
2 lshpset.n 𝑁 = ( LSpan ‘ 𝑊 )
3 lshpset.s 𝑆 = ( LSubSp ‘ 𝑊 )
4 lshpset.h 𝐻 = ( LSHyp ‘ 𝑊 )
5 1 2 3 4 lshpset ( 𝑊𝑋𝐻 = { 𝑠𝑆 ∣ ( 𝑠𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) } )
6 5 eleq2d ( 𝑊𝑋 → ( 𝑈𝐻𝑈 ∈ { 𝑠𝑆 ∣ ( 𝑠𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) } ) )
7 neeq1 ( 𝑠 = 𝑈 → ( 𝑠𝑉𝑈𝑉 ) )
8 uneq1 ( 𝑠 = 𝑈 → ( 𝑠 ∪ { 𝑣 } ) = ( 𝑈 ∪ { 𝑣 } ) )
9 8 fveqeq2d ( 𝑠 = 𝑈 → ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ↔ ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) )
10 9 rexbidv ( 𝑠 = 𝑈 → ( ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ↔ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) )
11 7 10 anbi12d ( 𝑠 = 𝑈 → ( ( 𝑠𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) ↔ ( 𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
12 11 elrab ( 𝑈 ∈ { 𝑠𝑆 ∣ ( 𝑠𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) } ↔ ( 𝑈𝑆 ∧ ( 𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
13 3anass ( ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ↔ ( 𝑈𝑆 ∧ ( 𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
14 12 13 bitr4i ( 𝑈 ∈ { 𝑠𝑆 ∣ ( 𝑠𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) } ↔ ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) )
15 6 14 bitrdi ( 𝑊𝑋 → ( 𝑈𝐻 ↔ ( 𝑈𝑆𝑈𝑉 ∧ ∃ 𝑣𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )