Metamath Proof Explorer

Theorem 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 ⊢ + ˙ = + D
lkrin.w ⊢ φ → W ∈ LMod
lkrin.e ⊢ φ → G ∈ F
lkrin.g ⊢ φ → H ∈ F
Assertion lkrin ⊢ φ → K ⁡ G ∩ K ⁡ H ⊆ K ⁡ G + ˙ 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 ⊢ + ˙ = + D
5 lkrin.w ⊢ φ → W ∈ LMod
6 lkrin.e ⊢ φ → G ∈ F
7 lkrin.g ⊢ φ → H ∈ F
8 elin ⊢ v ∈ K ⁡ G ∩ K ⁡ H ↔ v ∈ K ⁡ G ∧ v ∈ K ⁡ H
9 5 adantr ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → W ∈ LMod
10 6 adantr ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → G ∈ F
11 simprl ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → v ∈ K ⁡ G
12 eqid ⊢ Base W = Base W
13 12 1 2 lkrcl ⊢ W ∈ LMod ∧ G ∈ F ∧ v ∈ K ⁡ G → v ∈ Base W
14 9 10 11 13 syl3anc ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → v ∈ Base W
15 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
16 eqid ⊢ + Scalar ⁡ W = + Scalar ⁡ W
17 7 adantr ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → H ∈ F
18 12 15 16 1 3 4 9 10 17 14 ldualvaddval ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → G + ˙ H ⁡ v = G ⁡ v + Scalar ⁡ W H ⁡ v
19 eqid ⊢ 0 Scalar ⁡ W = 0 Scalar ⁡ W
20 15 19 1 2 lkrf0 ⊢ W ∈ LMod ∧ G ∈ F ∧ v ∈ K ⁡ G → G ⁡ v = 0 Scalar ⁡ W
21 9 10 11 20 syl3anc ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → G ⁡ v = 0 Scalar ⁡ W
22 simprr ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → v ∈ K ⁡ H
23 15 19 1 2 lkrf0 ⊢ W ∈ LMod ∧ H ∈ F ∧ v ∈ K ⁡ H → H ⁡ v = 0 Scalar ⁡ W
24 9 17 22 23 syl3anc ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → H ⁡ v = 0 Scalar ⁡ W
25 21 24 oveq12d ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → G ⁡ v + Scalar ⁡ W H ⁡ v = 0 Scalar ⁡ W + Scalar ⁡ W 0 Scalar ⁡ W
26 15 lmodring ⊢ W ∈ LMod → Scalar ⁡ W ∈ Ring
27 5 26 syl ⊢ φ → Scalar ⁡ W ∈ Ring
28 ringgrp ⊢ Scalar ⁡ W ∈ Ring → Scalar ⁡ W ∈ Grp
29 27 28 syl ⊢ φ → Scalar ⁡ W ∈ Grp
30 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
31 30 19 grpidcl ⊢ Scalar ⁡ W ∈ Grp → 0 Scalar ⁡ W ∈ Base Scalar ⁡ W
32 30 16 19 grplid ⊢ Scalar ⁡ W ∈ Grp ∧ 0 Scalar ⁡ W ∈ Base Scalar ⁡ W → 0 Scalar ⁡ W + Scalar ⁡ W 0 Scalar ⁡ W = 0 Scalar ⁡ W
33 29 31 32 syl2anc2 ⊢ φ → 0 Scalar ⁡ W + Scalar ⁡ W 0 Scalar ⁡ W = 0 Scalar ⁡ W
34 33 adantr ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → 0 Scalar ⁡ W + Scalar ⁡ W 0 Scalar ⁡ W = 0 Scalar ⁡ W
35 18 25 34 3eqtrd ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → G + ˙ H ⁡ v = 0 Scalar ⁡ W
36 1 3 4 5 6 7 ldualvaddcl ⊢ φ → G + ˙ H ∈ F
37 36 adantr ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → G + ˙ H ∈ F
38 12 15 19 1 2 ellkr ⊢ W ∈ LMod ∧ G + ˙ H ∈ F → v ∈ K ⁡ G + ˙ H ↔ v ∈ Base W ∧ G + ˙ H ⁡ v = 0 Scalar ⁡ W
39 9 37 38 syl2anc ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → v ∈ K ⁡ G + ˙ H ↔ v ∈ Base W ∧ G + ˙ H ⁡ v = 0 Scalar ⁡ W
40 14 35 39 mpbir2and ⊢ φ ∧ v ∈ K ⁡ G ∧ v ∈ K ⁡ H → v ∈ K ⁡ G + ˙ H
41 40 ex ⊢ φ → v ∈ K ⁡ G ∧ v ∈ K ⁡ H → v ∈ K ⁡ G + ˙ H
42 8 41 syl5bi ⊢ φ → v ∈ K ⁡ G ∩ K ⁡ H → v ∈ K ⁡ G + ˙ H
43 42 ssrdv ⊢ φ → K ⁡ G ∩ K ⁡ H ⊆ K ⁡ G + ˙ H