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