lkrlsp

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

	Ref	Expression
Hypotheses	lkrlsp.d	$⊢ D = Scalar (W)$
	lkrlsp.o	$⊢ \underset{˙}{0} = 0_{D}$
	lkrlsp.v	$⊢ V = {Base}_{W}$
	lkrlsp.n	$⊢ N = LSpan (W)$
	lkrlsp.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lkrlsp.f	$⊢ F = LFnl (W)$
	lkrlsp.k	$⊢ K = LKer (W)$
Assertion	lkrlsp	$⊢ (W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \to K (G) \underset{˙}{\oplus} N (\{X\}) = V$

Proof

Step	Hyp	Ref	Expression
1		lkrlsp.d	$⊢ D = Scalar (W)$
2		lkrlsp.o	$⊢ \underset{˙}{0} = 0_{D}$
3		lkrlsp.v	$⊢ V = {Base}_{W}$
4		lkrlsp.n	$⊢ N = LSpan (W)$
5		lkrlsp.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
6		lkrlsp.f	$⊢ F = LFnl (W)$
7		lkrlsp.k	$⊢ K = LKer (W)$
8		lveclmod	$⊢ W \in LVec \to W \in LMod$
9	8	3ad2ant1	$⊢ (W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \to W \in LMod$
10		simp2r	$⊢ (W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \to G \in F$
11		eqid	$⊢ LSubSp (W) = LSubSp (W)$
12	6 7 11	lkrlss	$⊢ (W \in LMod \land G \in F) \to K (G) \in LSubSp (W)$
13	9 10 12	syl2anc	$⊢ (W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \to K (G) \in LSubSp (W)$
14		simp2l	$⊢ (W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \to X \in V$
15	3 11 4	lspsncl	$⊢ (W \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (W)$
16	9 14 15	syl2anc	$⊢ (W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \to N (\{X\}) \in LSubSp (W)$
17	11 5	lsmcl	$⊢ (W \in LMod \land K (G) \in LSubSp (W) \land N (\{X\}) \in LSubSp (W)) \to K (G) \underset{˙}{\oplus} N (\{X\}) \in LSubSp (W)$
18	9 13 16 17	syl3anc	$⊢ (W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \to K (G) \underset{˙}{\oplus} N (\{X\}) \in LSubSp (W)$
19	3 11	lssss	$⊢ K (G) \underset{˙}{\oplus} N (\{X\}) \in LSubSp (W) \to K (G) \underset{˙}{\oplus} N (\{X\}) \subseteq V$
20	18 19	syl	$⊢ (W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \to K (G) \underset{˙}{\oplus} N (\{X\}) \subseteq V$
21		simpl1	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to W \in LVec$
22	21 8	syl	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to W \in LMod$
23		simpr	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to u \in V$
24	1	lmodring	$⊢ W \in LMod \to D \in Ring$
25	22 24	syl	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to D \in Ring$
26		simpl2r	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G \in F$
27		eqid	$⊢ {Base}_{D} = {Base}_{D}$
28	1 27 3 6	lflcl	$⊢ (W \in LVec \land G \in F \land u \in V) \to G (u) \in {Base}_{D}$
29	21 26 23 28	syl3anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G (u) \in {Base}_{D}$
30	1	lvecdrng	$⊢ W \in LVec \to D \in DivRing$
31	21 30	syl	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to D \in DivRing$
32		simpl2l	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to X \in V$
33	1 27 3 6	lflcl	$⊢ (W \in LVec \land G \in F \land X \in V) \to G (X) \in {Base}_{D}$
34	21 26 32 33	syl3anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G (X) \in {Base}_{D}$
35		simpl3	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G (X) \neq \underset{˙}{0}$
36		eqid	$⊢ {inv}_{r} (D) = {inv}_{r} (D)$
37	27 2 36	drnginvrcl	$⊢ (D \in DivRing \land G (X) \in {Base}_{D} \land G (X) \neq \underset{˙}{0}) \to {inv}_{r} (D) (G (X)) \in {Base}_{D}$
38	31 34 35 37	syl3anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to {inv}_{r} (D) (G (X)) \in {Base}_{D}$
39		eqid	$⊢ \cdot_{D} = \cdot_{D}$
40	27 39	ringcl	$⊢ (D \in Ring \land G (u) \in {Base}_{D} \land {inv}_{r} (D) (G (X)) \in {Base}_{D}) \to G (u) \cdot_{D} {inv}_{r} (D) (G (X)) \in {Base}_{D}$
41	25 29 38 40	syl3anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G (u) \cdot_{D} {inv}_{r} (D) (G (X)) \in {Base}_{D}$
42		eqid	$⊢ \cdot_{W} = \cdot_{W}$
43	3 1 42 27	lmodvscl	$⊢ (W \in LMod \land G (u) \cdot_{D} {inv}_{r} (D) (G (X)) \in {Base}_{D} \land X \in V) \to (G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X \in V$
44	22 41 32 43	syl3anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to (G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X \in V$
45		eqid	$⊢ +_{W} = +_{W}$
46		eqid	$⊢ -_{W} = -_{W}$
47	3 45 46	lmodvnpcan	$⊢ (W \in LMod \land u \in V \land (G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X \in V) \to (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X)) +_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) = u$
48	22 23 44 47	syl3anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X)) +_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) = u$
49	11	lsssssubg	$⊢ W \in LMod \to LSubSp (W) \subseteq SubGrp (W)$
50	22 49	syl	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to LSubSp (W) \subseteq SubGrp (W)$
51	13	adantr	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to K (G) \in LSubSp (W)$
52	50 51	sseldd	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to K (G) \in SubGrp (W)$
53	16	adantr	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to N (\{X\}) \in LSubSp (W)$
54	50 53	sseldd	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to N (\{X\}) \in SubGrp (W)$
55	3 46	lmodvsubcl	$⊢ (W \in LMod \land u \in V \land (G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X \in V) \to u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) \in V$
56	22 23 44 55	syl3anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) \in V$
57		eqid	$⊢ -_{D} = -_{D}$
58	1 57 3 46 6	lflsub	$⊢ (W \in LMod \land G \in F \land (u \in V \land (G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X \in V)) \to G (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X)) = G (u) -_{D} G ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X)$
59	22 26 23 44 58	syl112anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X)) = G (u) -_{D} G ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X)$
60	1 27 39 3 42 6	lflmul	$⊢ (W \in LMod \land G \in F \land (G (u) \cdot_{D} {inv}_{r} (D) (G (X)) \in {Base}_{D} \land X \in V)) \to G ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) = (G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{D} G (X)$
61	22 26 41 32 60	syl112anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) = (G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{D} G (X)$
62	27 39	ringass	$⊢ (D \in Ring \land (G (u) \in {Base}_{D} \land {inv}_{r} (D) (G (X)) \in {Base}_{D} \land G (X) \in {Base}_{D})) \to (G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{D} G (X) = G (u) \cdot_{D} ({inv}_{r} (D) (G (X)) \cdot_{D} G (X))$
63	25 29 38 34 62	syl13anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to (G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{D} G (X) = G (u) \cdot_{D} ({inv}_{r} (D) (G (X)) \cdot_{D} G (X))$
64		eqid	$⊢ 1_{D} = 1_{D}$
65	27 2 39 64 36	drnginvrl	$⊢ (D \in DivRing \land G (X) \in {Base}_{D} \land G (X) \neq \underset{˙}{0}) \to {inv}_{r} (D) (G (X)) \cdot_{D} G (X) = 1_{D}$
66	31 34 35 65	syl3anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to {inv}_{r} (D) (G (X)) \cdot_{D} G (X) = 1_{D}$
67	66	oveq2d	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G (u) \cdot_{D} ({inv}_{r} (D) (G (X)) \cdot_{D} G (X)) = G (u) \cdot_{D} 1_{D}$
68	27 39 64	ringridm	$⊢ (D \in Ring \land G (u) \in {Base}_{D}) \to G (u) \cdot_{D} 1_{D} = G (u)$
69	25 29 68	syl2anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G (u) \cdot_{D} 1_{D} = G (u)$
70	67 69	eqtrd	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G (u) \cdot_{D} ({inv}_{r} (D) (G (X)) \cdot_{D} G (X)) = G (u)$
71	61 63 70	3eqtrd	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) = G (u)$
72	71	oveq2d	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G (u) -_{D} G ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) = G (u) -_{D} G (u)$
73	1	lmodfgrp	$⊢ W \in LMod \to D \in Grp$
74	22 73	syl	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to D \in Grp$
75	27 2 57	grpsubid	$⊢ (D \in Grp \land G (u) \in {Base}_{D}) \to G (u) -_{D} G (u) = \underset{˙}{0}$
76	74 29 75	syl2anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G (u) -_{D} G (u) = \underset{˙}{0}$
77	59 72 76	3eqtrd	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to G (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X)) = \underset{˙}{0}$
78	3 1 2 6 7	ellkr	$⊢ (W \in LVec \land G \in F) \to (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) \in K (G) \leftrightarrow (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) \in V \land G (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X)) = \underset{˙}{0}))$
79	21 26 78	syl2anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) \in K (G) \leftrightarrow (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) \in V \land G (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X)) = \underset{˙}{0}))$
80	56 77 79	mpbir2and	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) \in K (G)$
81	3 42 1 27 4 22 41 32	lspsneli	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to (G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X \in N (\{X\})$
82	45 5	lsmelvali	$⊢ ((K (G) \in SubGrp (W) \land N (\{X\}) \in SubGrp (W)) \land (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) \in K (G) \land (G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X \in N (\{X\}))) \to (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X)) +_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) \in (K (G) \underset{˙}{\oplus} N (\{X\}))$
83	52 54 80 81 82	syl22anc	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to (u -_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X)) +_{W} ((G (u) \cdot_{D} {inv}_{r} (D) (G (X))) \cdot_{W} X) \in (K (G) \underset{˙}{\oplus} N (\{X\}))$
84	48 83	eqeltrrd	$⊢ ((W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \land u \in V) \to u \in (K (G) \underset{˙}{\oplus} N (\{X\}))$
85	20 84	eqelssd	$⊢ (W \in LVec \land (X \in V \land G \in F) \land G (X) \neq \underset{˙}{0}) \to K (G) \underset{˙}{\oplus} N (\{X\}) = V$

Metamath Proof Explorer

Theorem lkrlsp

Proof