Theorem islshpkrN

Description: The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be U = ( Kg ) or ( Kg ) = U as in lshpkrex ? Both standards seem to be used randomly throughout set.mm; we should decide on a preferred one. (Contributed by NM, 7-Oct-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lshpset2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lshpset2.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
	lshpset2.z	⊢ 0 = ( 0g ‘ 𝐷 )
	lshpset2.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
	lshpset2.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lshpset2.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
Assertion	islshpkrN	⊢ ( 𝑊 ∈ LVec → ( 𝑈 ∈ 𝐻 ↔ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑈 = ( 𝐾 ‘ 𝑔 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lshpset2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lshpset2.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3		lshpset2.z	⊢ 0 = ( 0g ‘ 𝐷 )
4		lshpset2.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
5		lshpset2.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6		lshpset2.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
7	1 2 3 4 5 6	lshpset2N	⊢ ( 𝑊 ∈ LVec → 𝐻 = { 𝑠 ∣ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) } )
8	7	eleq2d	⊢ ( 𝑊 ∈ LVec → ( 𝑈 ∈ 𝐻 ↔ 𝑈 ∈ { 𝑠 ∣ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) } ) )
9		elex	⊢ ( 𝑈 ∈ { 𝑠 ∣ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) } → 𝑈 ∈ V )
10	9	adantl	⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ { 𝑠 ∣ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) } ) → 𝑈 ∈ V )
11		fvex	⊢ ( 𝐾 ‘ 𝑔 ) ∈ V
12		eleq1	⊢ ( 𝑈 = ( 𝐾 ‘ 𝑔 ) → ( 𝑈 ∈ V ↔ ( 𝐾 ‘ 𝑔 ) ∈ V ) )
13	11 12	mpbiri	⊢ ( 𝑈 = ( 𝐾 ‘ 𝑔 ) → 𝑈 ∈ V )
14	13	adantl	⊢ ( ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑈 = ( 𝐾 ‘ 𝑔 ) ) → 𝑈 ∈ V )
15	14	rexlimivw	⊢ ( ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑈 = ( 𝐾 ‘ 𝑔 ) ) → 𝑈 ∈ V )
16	15	adantl	⊢ ( ( 𝑊 ∈ LVec ∧ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑈 = ( 𝐾 ‘ 𝑔 ) ) ) → 𝑈 ∈ V )
17		eqeq1	⊢ ( 𝑠 = 𝑈 → ( 𝑠 = ( 𝐾 ‘ 𝑔 ) ↔ 𝑈 = ( 𝐾 ‘ 𝑔 ) ) )
18	17	anbi2d	⊢ ( 𝑠 = 𝑈 → ( ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) ↔ ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑈 = ( 𝐾 ‘ 𝑔 ) ) ) )
19	18	rexbidv	⊢ ( 𝑠 = 𝑈 → ( ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑈 = ( 𝐾 ‘ 𝑔 ) ) ) )
20	19	elabg	⊢ ( 𝑈 ∈ V → ( 𝑈 ∈ { 𝑠 ∣ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) } ↔ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑈 = ( 𝐾 ‘ 𝑔 ) ) ) )
21	10 16 20	pm5.21nd	⊢ ( 𝑊 ∈ LVec → ( 𝑈 ∈ { 𝑠 ∣ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) } ↔ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑈 = ( 𝐾 ‘ 𝑔 ) ) ) )
22	8 21	bitrd	⊢ ( 𝑊 ∈ LVec → ( 𝑈 ∈ 𝐻 ↔ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑈 = ( 𝐾 ‘ 𝑔 ) ) ) )