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

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 ⊢ ( 𝑊 ∈ 𝑋 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑁 ‘ ( 𝑈 ∪ { 𝑣 } ) ) = 𝑉 ) ) )