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