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 ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lkrin.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
lkrin.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
lkrin.p ⊢ + = ( +g ‘ 𝐷 )
lkrin.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lkrin.e ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lkrin.g ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
Assertion lkrin ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∩ ( 𝐾 ‘ 𝐻 ) ) ⊆ ( 𝐾 ‘ ( 𝐺 + 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 lkrin.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 lkrin.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
3 lkrin.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
4 lkrin.p ⊢ + = ( +g ‘ 𝐷 )
5 lkrin.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
6 lkrin.e ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
7 lkrin.g ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
8 elin ⊢ ( 𝑣 ∈ ( ( 𝐾 ‘ 𝐺 ) ∩ ( 𝐾 ‘ 𝐻 ) ) ↔ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) )
9 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → 𝑊 ∈ LMod )
10 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → 𝐺 ∈ 𝐹 )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) )
12 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
13 12 1 2 lkrcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
14 9 10 11 13 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → 𝑣 ∈ ( Base ‘ 𝑊 ) )
15 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
16 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
17 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → 𝐻 ∈ 𝐹 )
18 12 15 16 1 3 4 9 10 17 14 ldualvaddval ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → ( ( 𝐺 + 𝐻 ) ‘ 𝑣 ) = ( ( 𝐺 ‘ 𝑣 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐻 ‘ 𝑣 ) ) )
19 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
20 15 19 1 2 lkrf0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( 𝐺 ‘ 𝑣 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
21 9 10 11 20 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → ( 𝐺 ‘ 𝑣 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
22 simprr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) )
23 15 19 1 2 lkrf0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) → ( 𝐻 ‘ 𝑣 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
24 9 17 22 23 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → ( 𝐻 ‘ 𝑣 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
25 21 24 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → ( ( 𝐺 ‘ 𝑣 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐻 ‘ 𝑣 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
26 15 lmodring ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Ring )
27 5 26 syl ⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ Ring )
28 ringgrp ⊢ ( ( Scalar ‘ 𝑊 ) ∈ Ring → ( Scalar ‘ 𝑊 ) ∈ Grp )
29 27 28 syl ⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ Grp )
30 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
31 30 19 grpidcl ⊢ ( ( Scalar ‘ 𝑊 ) ∈ Grp → ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
32 30 16 19 grplid ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
33 29 31 32 syl2anc2 ⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
35 18 25 34 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → ( ( 𝐺 + 𝐻 ) ‘ 𝑣 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
36 1 3 4 5 6 7 ldualvaddcl ⊢ ( 𝜑 → ( 𝐺 + 𝐻 ) ∈ 𝐹 )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → ( 𝐺 + 𝐻 ) ∈ 𝐹 )
38 12 15 19 1 2 ellkr ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐺 + 𝐻 ) ∈ 𝐹 ) → ( 𝑣 ∈ ( 𝐾 ‘ ( 𝐺 + 𝐻 ) ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝐺 + 𝐻 ) ‘ 𝑣 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
39 9 37 38 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → ( 𝑣 ∈ ( 𝐾 ‘ ( 𝐺 + 𝐻 ) ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝐺 + 𝐻 ) ‘ 𝑣 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
40 14 35 39 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) ) → 𝑣 ∈ ( 𝐾 ‘ ( 𝐺 + 𝐻 ) ) )
41 40 ex ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐻 ) ) → 𝑣 ∈ ( 𝐾 ‘ ( 𝐺 + 𝐻 ) ) ) )
42 8 41 biimtrid ⊢ ( 𝜑 → ( 𝑣 ∈ ( ( 𝐾 ‘ 𝐺 ) ∩ ( 𝐾 ‘ 𝐻 ) ) → 𝑣 ∈ ( 𝐾 ‘ ( 𝐺 + 𝐻 ) ) ) )
43 42 ssrdv ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∩ ( 𝐾 ‘ 𝐻 ) ) ⊆ ( 𝐾 ‘ ( 𝐺 + 𝐻 ) ) )