Theorem lkrlsp2

Description: The subspace sum of a kernel and the span of a vector not in the kernel is the whole vector space. (Contributed by NM, 12-May-2014)

	Ref	Expression
Hypotheses	lkrlsp2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lkrlsp2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lkrlsp2.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	lkrlsp2.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkrlsp2.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
Assertion	lkrlsp2	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( ( 𝐾 ‘ 𝐺 ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lkrlsp2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lkrlsp2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lkrlsp2.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
4		lkrlsp2.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
5		lkrlsp2.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
6		simp2l	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 ∈ 𝑉 )
7		simp3	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝐺 ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
8		simp1	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑊 ∈ LVec )
9		simp2r	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝐺 ∈ 𝐹 )
10		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
11		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
12	1 10 11 4 5	ellkr	⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
13	8 9 12	syl2anc	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
14	6 7 13	mpbir2and	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐺 ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) )
15	14	3expia	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ) → ( ( 𝐺 ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ) )
16	15	necon3bd	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ) → ( ¬ 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) → ( 𝐺 ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
17	16	3impia	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( 𝐺 ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
18	10 11 1 2 3 4 5	lkrlsp	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐺 ‘ 𝑋 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝐾 ‘ 𝐺 ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
19	17 18	syld3an3	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( ( 𝐾 ‘ 𝐺 ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )