lkrin

Description: Intersection of the kernels of 2 functionals is included in the kernel of their sum. (Contributed by NM, 7-Jan-2015)

	Ref	Expression
Hypotheses	lkrin.f	$⊢ F = LFnl (W)$
	lkrin.k	$⊢ K = LKer (W)$
	lkrin.d	$⊢ D = LDual (W)$
	lkrin.p	$⊢ \underset{˙}{+} = +_{D}$
	lkrin.w	$⊢ φ \to W \in LMod$
	lkrin.e	$⊢ φ \to G \in F$
	lkrin.g	$⊢ φ \to H \in F$
Assertion	lkrin	$⊢ φ \to K (G) \cap K (H) \subseteq K (G \underset{˙}{+} H)$

Proof

Step	Hyp	Ref	Expression
1		lkrin.f	$⊢ F = LFnl (W)$
2		lkrin.k	$⊢ K = LKer (W)$
3		lkrin.d	$⊢ D = LDual (W)$
4		lkrin.p	$⊢ \underset{˙}{+} = +_{D}$
5		lkrin.w	$⊢ φ \to W \in LMod$
6		lkrin.e	$⊢ φ \to G \in F$
7		lkrin.g	$⊢ φ \to H \in F$
8		elin	$⊢ v \in (K (G) \cap K (H)) \leftrightarrow (v \in K (G) \land v \in K (H))$
9	5	adantr	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to W \in LMod$
10	6	adantr	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to G \in F$
11		simprl	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to v \in K (G)$
12		eqid	$⊢ {Base}_{W} = {Base}_{W}$
13	12 1 2	lkrcl	$⊢ (W \in LMod \land G \in F \land v \in K (G)) \to v \in {Base}_{W}$
14	9 10 11 13	syl3anc	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to v \in {Base}_{W}$
15		eqid	$⊢ Scalar (W) = Scalar (W)$
16		eqid	$⊢ +_{Scalar (W)} = +_{Scalar (W)}$
17	7	adantr	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to H \in F$
18	12 15 16 1 3 4 9 10 17 14	ldualvaddval	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to (G \underset{˙}{+} H) (v) = G (v) +_{Scalar (W)} H (v)$
19		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
20	15 19 1 2	lkrf0	$⊢ (W \in LMod \land G \in F \land v \in K (G)) \to G (v) = 0_{Scalar (W)}$
21	9 10 11 20	syl3anc	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to G (v) = 0_{Scalar (W)}$
22		simprr	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to v \in K (H)$
23	15 19 1 2	lkrf0	$⊢ (W \in LMod \land H \in F \land v \in K (H)) \to H (v) = 0_{Scalar (W)}$
24	9 17 22 23	syl3anc	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to H (v) = 0_{Scalar (W)}$
25	21 24	oveq12d	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to G (v) +_{Scalar (W)} H (v) = 0_{Scalar (W)} +_{Scalar (W)} 0_{Scalar (W)}$
26	15	lmodring	$⊢ W \in LMod \to Scalar (W) \in Ring$
27	5 26	syl	$⊢ φ \to Scalar (W) \in Ring$
28		ringgrp	$⊢ Scalar (W) \in Ring \to Scalar (W) \in Grp$
29	27 28	syl	$⊢ φ \to Scalar (W) \in Grp$
30		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
31	30 19	grpidcl	$⊢ Scalar (W) \in Grp \to 0_{Scalar (W)} \in {Base}_{Scalar (W)}$
32	30 16 19	grplid	$⊢ (Scalar (W) \in Grp \land 0_{Scalar (W)} \in {Base}_{Scalar (W)}) \to 0_{Scalar (W)} +_{Scalar (W)} 0_{Scalar (W)} = 0_{Scalar (W)}$
33	29 31 32	syl2anc2	$⊢ φ \to 0_{Scalar (W)} +_{Scalar (W)} 0_{Scalar (W)} = 0_{Scalar (W)}$
34	33	adantr	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to 0_{Scalar (W)} +_{Scalar (W)} 0_{Scalar (W)} = 0_{Scalar (W)}$
35	18 25 34	3eqtrd	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to (G \underset{˙}{+} H) (v) = 0_{Scalar (W)}$
36	1 3 4 5 6 7	ldualvaddcl	$⊢ φ \to G \underset{˙}{+} H \in F$
37	36	adantr	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to G \underset{˙}{+} H \in F$
38	12 15 19 1 2	ellkr	$⊢ (W \in LMod \land G \underset{˙}{+} H \in F) \to (v \in K (G \underset{˙}{+} H) \leftrightarrow (v \in {Base}_{W} \land (G \underset{˙}{+} H) (v) = 0_{Scalar (W)}))$
39	9 37 38	syl2anc	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to (v \in K (G \underset{˙}{+} H) \leftrightarrow (v \in {Base}_{W} \land (G \underset{˙}{+} H) (v) = 0_{Scalar (W)}))$
40	14 35 39	mpbir2and	$⊢ (φ \land (v \in K (G) \land v \in K (H))) \to v \in K (G \underset{˙}{+} H)$
41	40	ex	$⊢ φ \to ((v \in K (G) \land v \in K (H)) \to v \in K (G \underset{˙}{+} H))$
42	8 41	biimtrid	$⊢ φ \to (v \in (K (G) \cap K (H)) \to v \in K (G \underset{˙}{+} H))$
43	42	ssrdv	$⊢ φ \to K (G) \cap K (H) \subseteq K (G \underset{˙}{+} H)$

Metamath Proof Explorer

Theorem lkrin

Proof