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	$⊢ V = {Base}_{W}$
	lkrlsp3.n	$⊢ N = LSpan (W)$
	lkrlsp3.f	$⊢ F = LFnl (W)$
	lkrlsp3.k	$⊢ K = LKer (W)$
Assertion	lkrlsp3	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to N (K (G) \cup \{X\}) = V$

Proof

Step	Hyp	Ref	Expression
1		lkrlsp3.v	$⊢ V = {Base}_{W}$
2		lkrlsp3.n	$⊢ N = LSpan (W)$
3		lkrlsp3.f	$⊢ F = LFnl (W)$
4		lkrlsp3.k	$⊢ K = LKer (W)$
5		lveclmod	$⊢ W \in LVec \to W \in LMod$
6	5	3ad2ant1	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to W \in LMod$
7		simp2r	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to G \in F$
8		eqid	$⊢ LSubSp (W) = LSubSp (W)$
9	3 4 8	lkrlss	$⊢ (W \in LMod \land G \in F) \to K (G) \in LSubSp (W)$
10	6 7 9	syl2anc	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to K (G) \in LSubSp (W)$
11	8 2	lspid	$⊢ (W \in LMod \land K (G) \in LSubSp (W)) \to N (K (G)) = K (G)$
12	6 10 11	syl2anc	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to N (K (G)) = K (G)$
13	12	uneq1d	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to N (K (G)) \cup N (\{X\}) = K (G) \cup N (\{X\})$
14	13	fveq2d	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to N (N (K (G)) \cup N (\{X\})) = N (K (G) \cup N (\{X\}))$
15	1 3 4 6 7	lkrssv	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to K (G) \subseteq V$
16		simp2l	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to X \in V$
17	16	snssd	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to \{X\} \subseteq V$
18	1 2	lspun	$⊢ (W \in LMod \land K (G) \subseteq V \land \{X\} \subseteq V) \to N (K (G) \cup \{X\}) = N (N (K (G)) \cup N (\{X\}))$
19	6 15 17 18	syl3anc	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to N (K (G) \cup \{X\}) = N (N (K (G)) \cup N (\{X\}))$
20	1 8 2	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
21	6 16 20	syl2anc	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to N (\{X\}) \in LSubSp (W)$
22		eqid	$⊢ LSSum (W) = LSSum (W)$
23	8 2 22	lsmsp	$⊢ (W \in LMod \land K (G) \in LSubSp (W) \land N (\{X\}) \in LSubSp (W)) \to K (G) LSSum (W) N (\{X\}) = N (K (G) \cup N (\{X\}))$
24	6 10 21 23	syl3anc	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to K (G) LSSum (W) N (\{X\}) = N (K (G) \cup N (\{X\}))$
25	14 19 24	3eqtr4d	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to N (K (G) \cup \{X\}) = K (G) LSSum (W) N (\{X\})$
26	1 2 22 3 4	lkrlsp2	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to K (G) LSSum (W) N (\{X\}) = V$
27	25 26	eqtrd	$⊢ (W \in LVec \land (X \in V \land G \in F) \land \neg X \in K (G)) \to N (K (G) \cup \{X\}) = V$

Metamath Proof Explorer

Theorem lkrlsp3

Proof