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