This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( ( 𝐾 ‘ 𝐺 ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )