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 syl5bi ( 𝜑 → ( 𝑣 ∈ ( ( 𝐾𝐺 ) ∩ ( 𝐾𝐻 ) ) → 𝑣 ∈ ( 𝐾 ‘ ( 𝐺 + 𝐻 ) ) ) )
43 42 ssrdv ( 𝜑 → ( ( 𝐾𝐺 ) ∩ ( 𝐾𝐻 ) ) ⊆ ( 𝐾 ‘ ( 𝐺 + 𝐻 ) ) )