Theorem lkrshpor

Description: The kernel of a functional is either a hyperplane or the full vector space. (Contributed by NM, 7-Oct-2014)

	Ref	Expression
Hypotheses	lkrshpor.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lkrshpor.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
	lkrshpor.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkrshpor.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
	lkrshpor.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lkrshpor.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lkrshpor	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ∨ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		lkrshpor.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lkrshpor.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
3		lkrshpor.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4		lkrshpor.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
5		lkrshpor.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lkrshpor.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
7		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
8	5 7	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
9		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
10		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
11	9 10 1 3 4	lkr0f	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
12	8 6 11	syl2anc	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
13	12	biimpar	⊢ ( ( 𝜑 ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝐾 ‘ 𝐺 ) = 𝑉 )
14	13	olcd	⊢ ( ( 𝜑 ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ∨ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )
15	5	adantr	⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝑊 ∈ LVec )
16	6	adantr	⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝐺 ∈ 𝐹 )
17		simpr	⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
18	1 9 10 2 3 4	lkrshp	⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )
19	15 16 17 18	syl3anc	⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )
20	19	orcd	⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ∨ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )
21	14 20	pm2.61dane	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ∨ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )