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=LSubSpS
kercvrlsm.p ˙=LSSumS
kercvrlsm.z 0˙=0T
kercvrlsm.k K=F-10˙
kercvrlsm.b B=BaseS
kercvrlsm.f φFSLMHomT
kercvrlsm.d φDU
kercvrlsm.cv φFD=ranF
Assertion kercvrlsm φK˙D=B

Proof

Step Hyp Ref Expression
1 kercvrlsm.u U=LSubSpS
2 kercvrlsm.p ˙=LSSumS
3 kercvrlsm.z 0˙=0T
4 kercvrlsm.k K=F-10˙
5 kercvrlsm.b B=BaseS
6 kercvrlsm.f φFSLMHomT
7 kercvrlsm.d φDU
8 kercvrlsm.cv φFD=ranF
9 lmhmlmod1 FSLMHomTSLMod
10 6 9 syl φSLMod
11 4 3 1 lmhmkerlss FSLMHomTKU
12 6 11 syl φKU
13 1 2 lsmcl SLModKUDUK˙DU
14 10 12 7 13 syl3anc φK˙DU
15 5 1 lssss K˙DUK˙DB
16 14 15 syl φK˙DB
17 eqid BaseT=BaseT
18 5 17 lmhmf FSLMHomTF:BBaseT
19 6 18 syl φF:BBaseT
20 19 ffnd φFFnB
21 fnfvelrn FFnBaBFaranF
22 20 21 sylan φaBFaranF
23 8 adantr φaBFD=ranF
24 22 23 eleqtrrd φaBFaFD
25 20 adantr φaBFFnB
26 5 1 lssss DUDB
27 7 26 syl φDB
28 27 adantr φaBDB
29 fvelimab FFnBDBFaFDbDFb=Fa
30 25 28 29 syl2anc φaBFaFDbDFb=Fa
31 24 30 mpbid φaBbDFb=Fa
32 lmodgrp SLModSGrp
33 10 32 syl φSGrp
34 33 adantr φaBbDSGrp
35 simprl φaBbDaB
36 27 sselda φbDbB
37 36 adantrl φaBbDbB
38 eqid +S=+S
39 eqid -S=-S
40 5 38 39 grpnpcan SGrpaBbBa-Sb+Sb=a
41 34 35 37 40 syl3anc φaBbDa-Sb+Sb=a
42 41 adantr φaBbDFb=Faa-Sb+Sb=a
43 10 ad2antrr φaBbDFb=FaSLMod
44 5 1 lssss KUKB
45 12 44 syl φKB
46 45 ad2antrr φaBbDFb=FaKB
47 27 ad2antrr φaBbDFb=FaDB
48 eqcom Fb=FaFa=Fb
49 lmghm FSLMHomTFSGrpHomT
50 6 49 syl φFSGrpHomT
51 50 adantr φaBbDFSGrpHomT
52 5 3 4 39 ghmeqker FSGrpHomTaBbBFa=Fba-SbK
53 51 35 37 52 syl3anc φaBbDFa=Fba-SbK
54 48 53 syl5bb φaBbDFb=Faa-SbK
55 54 biimpa φaBbDFb=Faa-SbK
56 simplrr φaBbDFb=FabD
57 5 38 2 lsmelvalix SLModKBDBa-SbKbDa-Sb+SbK˙D
58 43 46 47 55 56 57 syl32anc φaBbDFb=Faa-Sb+SbK˙D
59 42 58 eqeltrrd φaBbDFb=FaaK˙D
60 59 ex φaBbDFb=FaaK˙D
61 60 anassrs φaBbDFb=FaaK˙D
62 61 rexlimdva φaBbDFb=FaaK˙D
63 31 62 mpd φaBaK˙D
64 16 63 eqelssd φK˙D=B