Metamath Proof Explorer


Theorem lkrlsp3

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, 29-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 lkrlsp3.v 𝑉 = ( Base ‘ 𝑊 )
2 lkrlsp3.n 𝑁 = ( LSpan ‘ 𝑊 )
3 lkrlsp3.f 𝐹 = ( LFnl ‘ 𝑊 )
4 lkrlsp3.k 𝐾 = ( LKer ‘ 𝑊 )
5 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
6 5 3ad2ant1 ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → 𝑊 ∈ LMod )
7 simp2r ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → 𝐺𝐹 )
8 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9 3 4 8 lkrlss ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( 𝐾𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) )
10 6 7 9 syl2anc ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( 𝐾𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) )
11 8 2 lspid ( ( 𝑊 ∈ LMod ∧ ( 𝐾𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝐾𝐺 ) ) = ( 𝐾𝐺 ) )
12 6 10 11 syl2anc ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( 𝑁 ‘ ( 𝐾𝐺 ) ) = ( 𝐾𝐺 ) )
13 12 uneq1d ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( ( 𝑁 ‘ ( 𝐾𝐺 ) ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) = ( ( 𝐾𝐺 ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) )
14 13 fveq2d ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( 𝑁 ‘ ( ( 𝑁 ‘ ( 𝐾𝐺 ) ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) = ( 𝑁 ‘ ( ( 𝐾𝐺 ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) )
15 1 3 4 6 7 lkrssv ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( 𝐾𝐺 ) ⊆ 𝑉 )
16 simp2l ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → 𝑋𝑉 )
17 16 snssd ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → { 𝑋 } ⊆ 𝑉 )
18 1 2 lspun ( ( 𝑊 ∈ LMod ∧ ( 𝐾𝐺 ) ⊆ 𝑉 ∧ { 𝑋 } ⊆ 𝑉 ) → ( 𝑁 ‘ ( ( 𝐾𝐺 ) ∪ { 𝑋 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ ( 𝐾𝐺 ) ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) )
19 6 15 17 18 syl3anc ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( 𝑁 ‘ ( ( 𝐾𝐺 ) ∪ { 𝑋 } ) ) = ( 𝑁 ‘ ( ( 𝑁 ‘ ( 𝐾𝐺 ) ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) )
20 1 8 2 lspsncl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
21 6 16 20 syl2anc ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
22 eqid ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
23 8 2 22 lsmsp ( ( 𝑊 ∈ LMod ∧ ( 𝐾𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( 𝐾𝐺 ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑁 ‘ ( ( 𝐾𝐺 ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) )
24 6 10 21 23 syl3anc ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( ( 𝐾𝐺 ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑁 ‘ ( ( 𝐾𝐺 ) ∪ ( 𝑁 ‘ { 𝑋 } ) ) ) )
25 14 19 24 3eqtr4d ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( 𝑁 ‘ ( ( 𝐾𝐺 ) ∪ { 𝑋 } ) ) = ( ( 𝐾𝐺 ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) )
26 1 2 22 3 4 lkrlsp2 ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( ( 𝐾𝐺 ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )
27 25 26 eqtrd ( ( 𝑊 ∈ LVec ∧ ( 𝑋𝑉𝐺𝐹 ) ∧ ¬ 𝑋 ∈ ( 𝐾𝐺 ) ) → ( 𝑁 ‘ ( ( 𝐾𝐺 ) ∪ { 𝑋 } ) ) = 𝑉 )