Metamath Proof Explorer

Theorem kercvrlsm

Description: The domain of a linear function is the subspace sum of the kernel and any subspace which covers the range. (Contributed by Stefan O'Rear, 24-Jan-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses kercvrlsm.u 
|- U = ( LSubSp ` S )
kercvrlsm.p 
|- .(+) = ( LSSum ` S )
kercvrlsm.z 
|- .0. = ( 0g ` T )
kercvrlsm.k 
|- K = ( `' F " { .0. } )
kercvrlsm.b 
|- B = ( Base ` S )
kercvrlsm.f 
|- ( ph -> F e. ( S LMHom T ) )
kercvrlsm.d 
|- ( ph -> D e. U )
kercvrlsm.cv 
|- ( ph -> ( F " D ) = ran F )
Assertion kercvrlsm 
|- ( ph -> ( K .(+) D ) = B )

Proof

Step Hyp Ref Expression
1 kercvrlsm.u 
 |-  U = ( LSubSp ` S )
2 kercvrlsm.p 
 |-  .(+) = ( LSSum ` S )
3 kercvrlsm.z 
 |-  .0. = ( 0g ` T )
4 kercvrlsm.k 
 |-  K = ( `' F " { .0. } )
5 kercvrlsm.b 
 |-  B = ( Base ` S )
6 kercvrlsm.f 
 |-  ( ph -> F e. ( S LMHom T ) )
7 kercvrlsm.d 
 |-  ( ph -> D e. U )
8 kercvrlsm.cv 
 |-  ( ph -> ( F " D ) = ran F )
9 lmhmlmod1 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )
10 6 9 syl 
 |-  ( ph -> S e. LMod )
11 4 3 1 lmhmkerlss 
 |-  ( F e. ( S LMHom T ) -> K e. U )
12 6 11 syl 
 |-  ( ph -> K e. U )
13 1 2 lsmcl 
 |-  ( ( S e. LMod /\ K e. U /\ D e. U ) -> ( K .(+) D ) e. U )
14 10 12 7 13 syl3anc 
 |-  ( ph -> ( K .(+) D ) e. U )
15 5 1 lssss 
 |-  ( ( K .(+) D ) e. U -> ( K .(+) D ) C_ B )
16 14 15 syl 
 |-  ( ph -> ( K .(+) D ) C_ B )
17 eqid 
 |-  ( Base ` T ) = ( Base ` T )
18 5 17 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : B --> ( Base ` T ) )
19 6 18 syl 
 |-  ( ph -> F : B --> ( Base ` T ) )
20 19 ffnd 
 |-  ( ph -> F Fn B )
21 fnfvelrn 
 |-  ( ( F Fn B /\ a e. B ) -> ( F ` a ) e. ran F )
22 20 21 sylan 
 |-  ( ( ph /\ a e. B ) -> ( F ` a ) e. ran F )
23 8 adantr 
 |-  ( ( ph /\ a e. B ) -> ( F " D ) = ran F )
24 22 23 eleqtrrd 
 |-  ( ( ph /\ a e. B ) -> ( F ` a ) e. ( F " D ) )
25 20 adantr 
 |-  ( ( ph /\ a e. B ) -> F Fn B )
26 5 1 lssss 
 |-  ( D e. U -> D C_ B )
27 7 26 syl 
 |-  ( ph -> D C_ B )
28 27 adantr 
 |-  ( ( ph /\ a e. B ) -> D C_ B )
29 fvelimab 
 |-  ( ( F Fn B /\ D C_ B ) -> ( ( F ` a ) e. ( F " D ) <-> E. b e. D ( F ` b ) = ( F ` a ) ) )
30 25 28 29 syl2anc 
 |-  ( ( ph /\ a e. B ) -> ( ( F ` a ) e. ( F " D ) <-> E. b e. D ( F ` b ) = ( F ` a ) ) )
31 24 30 mpbid 
 |-  ( ( ph /\ a e. B ) -> E. b e. D ( F ` b ) = ( F ` a ) )
32 lmodgrp 
 |-  ( S e. LMod -> S e. Grp )
33 10 32 syl 
 |-  ( ph -> S e. Grp )
34 33 adantr 
 |-  ( ( ph /\ ( a e. B /\ b e. D ) ) -> S e. Grp )
35 simprl 
 |-  ( ( ph /\ ( a e. B /\ b e. D ) ) -> a e. B )
36 27 sselda 
 |-  ( ( ph /\ b e. D ) -> b e. B )
37 36 adantrl 
 |-  ( ( ph /\ ( a e. B /\ b e. D ) ) -> b e. B )
38 eqid 
 |-  ( +g ` S ) = ( +g ` S )
39 eqid 
 |-  ( -g ` S ) = ( -g ` S )
40 5 38 39 grpnpcan 
 |-  ( ( S e. Grp /\ a e. B /\ b e. B ) -> ( ( a ( -g ` S ) b ) ( +g ` S ) b ) = a )
41 34 35 37 40 syl3anc 
 |-  ( ( ph /\ ( a e. B /\ b e. D ) ) -> ( ( a ( -g ` S ) b ) ( +g ` S ) b ) = a )
42 41 adantr 
 |-  ( ( ( ph /\ ( a e. B /\ b e. D ) ) /\ ( F ` b ) = ( F ` a ) ) -> ( ( a ( -g ` S ) b ) ( +g ` S ) b ) = a )
43 10 ad2antrr 
 |-  ( ( ( ph /\ ( a e. B /\ b e. D ) ) /\ ( F ` b ) = ( F ` a ) ) -> S e. LMod )
44 5 1 lssss 
 |-  ( K e. U -> K C_ B )
45 12 44 syl 
 |-  ( ph -> K C_ B )
46 45 ad2antrr 
 |-  ( ( ( ph /\ ( a e. B /\ b e. D ) ) /\ ( F ` b ) = ( F ` a ) ) -> K C_ B )
47 27 ad2antrr 
 |-  ( ( ( ph /\ ( a e. B /\ b e. D ) ) /\ ( F ` b ) = ( F ` a ) ) -> D C_ B )
48 eqcom 
 |-  ( ( F ` b ) = ( F ` a ) <-> ( F ` a ) = ( F ` b ) )
49 lmghm 
 |-  ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
50 6 49 syl 
 |-  ( ph -> F e. ( S GrpHom T ) )
51 50 adantr 
 |-  ( ( ph /\ ( a e. B /\ b e. D ) ) -> F e. ( S GrpHom T ) )
52 5 3 4 39 ghmeqker 
 |-  ( ( F e. ( S GrpHom T ) /\ a e. B /\ b e. B ) -> ( ( F ` a ) = ( F ` b ) <-> ( a ( -g ` S ) b ) e. K ) )
53 51 35 37 52 syl3anc 
 |-  ( ( ph /\ ( a e. B /\ b e. D ) ) -> ( ( F ` a ) = ( F ` b ) <-> ( a ( -g ` S ) b ) e. K ) )
54 48 53 bitrid 
 |-  ( ( ph /\ ( a e. B /\ b e. D ) ) -> ( ( F ` b ) = ( F ` a ) <-> ( a ( -g ` S ) b ) e. K ) )
55 54 biimpa 
 |-  ( ( ( ph /\ ( a e. B /\ b e. D ) ) /\ ( F ` b ) = ( F ` a ) ) -> ( a ( -g ` S ) b ) e. K )
56 simplrr 
 |-  ( ( ( ph /\ ( a e. B /\ b e. D ) ) /\ ( F ` b ) = ( F ` a ) ) -> b e. D )
57 5 38 2 lsmelvalix 
 |-  ( ( ( S e. LMod /\ K C_ B /\ D C_ B ) /\ ( ( a ( -g ` S ) b ) e. K /\ b e. D ) ) -> ( ( a ( -g ` S ) b ) ( +g ` S ) b ) e. ( K .(+) D ) )
58 43 46 47 55 56 57 syl32anc 
 |-  ( ( ( ph /\ ( a e. B /\ b e. D ) ) /\ ( F ` b ) = ( F ` a ) ) -> ( ( a ( -g ` S ) b ) ( +g ` S ) b ) e. ( K .(+) D ) )
59 42 58 eqeltrrd 
 |-  ( ( ( ph /\ ( a e. B /\ b e. D ) ) /\ ( F ` b ) = ( F ` a ) ) -> a e. ( K .(+) D ) )
60 59 ex 
 |-  ( ( ph /\ ( a e. B /\ b e. D ) ) -> ( ( F ` b ) = ( F ` a ) -> a e. ( K .(+) D ) ) )
61 60 anassrs 
 |-  ( ( ( ph /\ a e. B ) /\ b e. D ) -> ( ( F ` b ) = ( F ` a ) -> a e. ( K .(+) D ) ) )
62 61 rexlimdva 
 |-  ( ( ph /\ a e. B ) -> ( E. b e. D ( F ` b ) = ( F ` a ) -> a e. ( K .(+) D ) ) )
63 31 62 mpd 
 |-  ( ( ph /\ a e. B ) -> a e. ( K .(+) D ) )
64 16 63 eqelssd 
 |-  ( ph -> ( K .(+) D ) = B )