kercvrlsm

Description: The domain of a linear function is the subspace sum of the kernel and any subspace which covers the range. (Contributed by Stefan O'Rear, 24-Jan-2015) (Revised by Stefan O'Rear, 6-May-2015)

	Ref	Expression
Hypotheses	kercvrlsm.u	$⊢ U = LSubSp (S)$
	kercvrlsm.p	$⊢ \underset{˙}{\oplus} = LSSum (S)$
	kercvrlsm.z	$⊢ \underset{˙}{0} = 0_{T}$
	kercvrlsm.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
	kercvrlsm.b	$⊢ B = {Base}_{S}$
	kercvrlsm.f	$⊢ φ \to F \in (S LMHom T)$
	kercvrlsm.d	$⊢ φ \to D \in U$
	kercvrlsm.cv	$⊢ φ \to F [D] = ran F$
Assertion	kercvrlsm	$⊢ φ \to K \underset{˙}{\oplus} D = B$

Proof

Step	Hyp	Ref	Expression
1		kercvrlsm.u	$⊢ U = LSubSp (S)$
2		kercvrlsm.p	$⊢ \underset{˙}{\oplus} = LSSum (S)$
3		kercvrlsm.z	$⊢ \underset{˙}{0} = 0_{T}$
4		kercvrlsm.k	$⊢ K = F^{-1} [\{\underset{˙}{0}\}]$
5		kercvrlsm.b	$⊢ B = {Base}_{S}$
6		kercvrlsm.f	$⊢ φ \to F \in (S LMHom T)$
7		kercvrlsm.d	$⊢ φ \to D \in U$
8		kercvrlsm.cv	$⊢ φ \to F [D] = ran F$
9		lmhmlmod1	$⊢ F \in (S LMHom T) \to S \in LMod$
10	6 9	syl	$⊢ φ \to S \in LMod$
11	4 3 1	lmhmkerlss	$⊢ F \in (S LMHom T) \to K \in U$
12	6 11	syl	$⊢ φ \to K \in U$
13	1 2	lsmcl	$⊢ (S \in LMod \land K \in U \land D \in U) \to K \underset{˙}{\oplus} D \in U$
14	10 12 7 13	syl3anc	$⊢ φ \to K \underset{˙}{\oplus} D \in U$
15	5 1	lssss	$⊢ K \underset{˙}{\oplus} D \in U \to K \underset{˙}{\oplus} D \subseteq B$
16	14 15	syl	$⊢ φ \to K \underset{˙}{\oplus} D \subseteq B$
17		eqid	$⊢ {Base}_{T} = {Base}_{T}$
18	5 17	lmhmf	$⊢ F \in (S LMHom T) \to F : B ⟶ {Base}_{T}$
19	6 18	syl	$⊢ φ \to F : B ⟶ {Base}_{T}$
20	19	ffnd	$⊢ φ \to F Fn B$
21		fnfvelrn	$⊢ (F Fn B \land a \in B) \to F (a) \in ran F$
22	20 21	sylan	$⊢ (φ \land a \in B) \to F (a) \in ran F$
23	8	adantr	$⊢ (φ \land a \in B) \to F [D] = ran F$
24	22 23	eleqtrrd	$⊢ (φ \land a \in B) \to F (a) \in F [D]$
25	20	adantr	$⊢ (φ \land a \in B) \to F Fn B$
26	5 1	lssss	$⊢ D \in U \to D \subseteq B$
27	7 26	syl	$⊢ φ \to D \subseteq B$
28	27	adantr	$⊢ (φ \land a \in B) \to D \subseteq B$
29		fvelimab	$⊢ (F Fn B \land D \subseteq B) \to (F (a) \in F [D] \leftrightarrow \exists b \in D F (b) = F (a))$
30	25 28 29	syl2anc	$⊢ (φ \land a \in B) \to (F (a) \in F [D] \leftrightarrow \exists b \in D F (b) = F (a))$
31	24 30	mpbid	$⊢ (φ \land a \in B) \to \exists b \in D F (b) = F (a)$
32		lmodgrp	$⊢ S \in LMod \to S \in Grp$
33	10 32	syl	$⊢ φ \to S \in Grp$
34	33	adantr	$⊢ (φ \land (a \in B \land b \in D)) \to S \in Grp$
35		simprl	$⊢ (φ \land (a \in B \land b \in D)) \to a \in B$
36	27	sselda	$⊢ (φ \land b \in D) \to b \in B$
37	36	adantrl	$⊢ (φ \land (a \in B \land b \in D)) \to b \in B$
38		eqid	$⊢ +_{S} = +_{S}$
39		eqid	$⊢ -_{S} = -_{S}$
40	5 38 39	grpnpcan	$⊢ (S \in Grp \land a \in B \land b \in B) \to (a -_{S} b) +_{S} b = a$
41	34 35 37 40	syl3anc	$⊢ (φ \land (a \in B \land b \in D)) \to (a -_{S} b) +_{S} b = a$
42	41	adantr	$⊢ ((φ \land (a \in B \land b \in D)) \land F (b) = F (a)) \to (a -_{S} b) +_{S} b = a$
43	10	ad2antrr	$⊢ ((φ \land (a \in B \land b \in D)) \land F (b) = F (a)) \to S \in LMod$
44	5 1	lssss	$⊢ K \in U \to K \subseteq B$
45	12 44	syl	$⊢ φ \to K \subseteq B$
46	45	ad2antrr	$⊢ ((φ \land (a \in B \land b \in D)) \land F (b) = F (a)) \to K \subseteq B$
47	27	ad2antrr	$⊢ ((φ \land (a \in B \land b \in D)) \land F (b) = F (a)) \to D \subseteq B$
48		eqcom	$⊢ F (b) = F (a) \leftrightarrow F (a) = F (b)$
49		lmghm	$⊢ F \in (S LMHom T) \to F \in (S GrpHom T)$
50	6 49	syl	$⊢ φ \to F \in (S GrpHom T)$
51	50	adantr	$⊢ (φ \land (a \in B \land b \in D)) \to F \in (S GrpHom T)$
52	5 3 4 39	ghmeqker	$⊢ (F \in (S GrpHom T) \land a \in B \land b \in B) \to (F (a) = F (b) \leftrightarrow a -_{S} b \in K)$
53	51 35 37 52	syl3anc	$⊢ (φ \land (a \in B \land b \in D)) \to (F (a) = F (b) \leftrightarrow a -_{S} b \in K)$
54	48 53	bitrid	$⊢ (φ \land (a \in B \land b \in D)) \to (F (b) = F (a) \leftrightarrow a -_{S} b \in K)$
55	54	biimpa	$⊢ ((φ \land (a \in B \land b \in D)) \land F (b) = F (a)) \to a -_{S} b \in K$
56		simplrr	$⊢ ((φ \land (a \in B \land b \in D)) \land F (b) = F (a)) \to b \in D$
57	5 38 2	lsmelvalix	$⊢ ((S \in LMod \land K \subseteq B \land D \subseteq B) \land (a -_{S} b \in K \land b \in D)) \to (a -_{S} b) +_{S} b \in (K \underset{˙}{\oplus} D)$
58	43 46 47 55 56 57	syl32anc	$⊢ ((φ \land (a \in B \land b \in D)) \land F (b) = F (a)) \to (a -_{S} b) +_{S} b \in (K \underset{˙}{\oplus} D)$
59	42 58	eqeltrrd	$⊢ ((φ \land (a \in B \land b \in D)) \land F (b) = F (a)) \to a \in (K \underset{˙}{\oplus} D)$
60	59	ex	$⊢ (φ \land (a \in B \land b \in D)) \to (F (b) = F (a) \to a \in (K \underset{˙}{\oplus} D))$
61	60	anassrs	$⊢ ((φ \land a \in B) \land b \in D) \to (F (b) = F (a) \to a \in (K \underset{˙}{\oplus} D))$
62	61	rexlimdva	$⊢ (φ \land a \in B) \to (\exists b \in D F (b) = F (a) \to a \in (K \underset{˙}{\oplus} D))$
63	31 62	mpd	$⊢ (φ \land a \in B) \to a \in (K \underset{˙}{\oplus} D)$
64	16 63	eqelssd	$⊢ φ \to K \underset{˙}{\oplus} D = B$

Metamath Proof Explorer

Theorem kercvrlsm

Proof