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 | |
|
kercvrlsm.p | |
||
kercvrlsm.z | |
||
kercvrlsm.k | |
||
kercvrlsm.b | |
||
kercvrlsm.f | |
||
kercvrlsm.d | |
||
kercvrlsm.cv | |
||
Assertion | kercvrlsm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | kercvrlsm.u | |
|
2 | kercvrlsm.p | |
|
3 | kercvrlsm.z | |
|
4 | kercvrlsm.k | |
|
5 | kercvrlsm.b | |
|
6 | kercvrlsm.f | |
|
7 | kercvrlsm.d | |
|
8 | kercvrlsm.cv | |
|
9 | lmhmlmod1 | |
|
10 | 6 9 | syl | |
11 | 4 3 1 | lmhmkerlss | |
12 | 6 11 | syl | |
13 | 1 2 | lsmcl | |
14 | 10 12 7 13 | syl3anc | |
15 | 5 1 | lssss | |
16 | 14 15 | syl | |
17 | eqid | |
|
18 | 5 17 | lmhmf | |
19 | 6 18 | syl | |
20 | 19 | ffnd | |
21 | fnfvelrn | |
|
22 | 20 21 | sylan | |
23 | 8 | adantr | |
24 | 22 23 | eleqtrrd | |
25 | 20 | adantr | |
26 | 5 1 | lssss | |
27 | 7 26 | syl | |
28 | 27 | adantr | |
29 | fvelimab | |
|
30 | 25 28 29 | syl2anc | |
31 | 24 30 | mpbid | |
32 | lmodgrp | |
|
33 | 10 32 | syl | |
34 | 33 | adantr | |
35 | simprl | |
|
36 | 27 | sselda | |
37 | 36 | adantrl | |
38 | eqid | |
|
39 | eqid | |
|
40 | 5 38 39 | grpnpcan | |
41 | 34 35 37 40 | syl3anc | |
42 | 41 | adantr | |
43 | 10 | ad2antrr | |
44 | 5 1 | lssss | |
45 | 12 44 | syl | |
46 | 45 | ad2antrr | |
47 | 27 | ad2antrr | |
48 | eqcom | |
|
49 | lmghm | |
|
50 | 6 49 | syl | |
51 | 50 | adantr | |
52 | 5 3 4 39 | ghmeqker | |
53 | 51 35 37 52 | syl3anc | |
54 | 48 53 | syl5bb | |
55 | 54 | biimpa | |
56 | simplrr | |
|
57 | 5 38 2 | lsmelvalix | |
58 | 43 46 47 55 56 57 | syl32anc | |
59 | 42 58 | eqeltrrd | |
60 | 59 | ex | |
61 | 60 | anassrs | |
62 | 61 | rexlimdva | |
63 | 31 62 | mpd | |
64 | 16 63 | eqelssd | |