lkrshp3

Description: The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014)

	Ref	Expression
Hypotheses	lkrshp3.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lkrshp3.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
	lkrshp3.o	⊢ 0 = ( 0_g ‘ 𝐷 )
	lkrshp3.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
	lkrshp3.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkrshp3.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
	lkrshp3.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lkrshp3.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lkrshp3	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ↔ 𝐺 ≠ ( 𝑉 × { 0 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lkrshp3.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lkrshp3.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3		lkrshp3.o	⊢ 0 = ( 0_g ‘ 𝐷 )
4		lkrshp3.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
5		lkrshp3.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6		lkrshp3.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
7		lkrshp3.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
8		lkrshp3.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10	7 9	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
11	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → 𝑊 ∈ LMod )
12		simpr	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )
13	1 4 11 12	lshpne	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 )
14	2 3 1 5 6	lkr0f	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) )
15	10 8 14	syl2anc	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) )
17	16	necon3bid	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → ( ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 ↔ 𝐺 ≠ ( 𝑉 × { 0 } ) ) )
18	13 17	mpbid	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → 𝐺 ≠ ( 𝑉 × { 0 } ) )
19	7	adantr	⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → 𝑊 ∈ LVec )
20	8	adantr	⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → 𝐺 ∈ 𝐹 )
21		simpr	⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → 𝐺 ≠ ( 𝑉 × { 0 } ) )
22	1 2 3 4 5 6	lkrshp	⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )
23	19 20 21 22	syl3anc	⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )
24	18 23	impbida	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ↔ 𝐺 ≠ ( 𝑉 × { 0 } ) ) )

Metamath Proof Explorer

Theorem lkrshp3

Proof