Step | Hyp | Ref
| Expression |
1 | | preq2 4700 |
. . . . . 6
β’ ((π + π) = 0 β {π, (π + π)} = {π, 0 }) |
2 | 1 | fveq2d 6851 |
. . . . 5
β’ ((π + π) = 0 β (πβ{π, (π + π)}) = (πβ{π, 0 })) |
3 | | mapdindp1.v |
. . . . . 6
β’ π = (Baseβπ) |
4 | | mapdindp1.o |
. . . . . 6
β’ 0 =
(0gβπ) |
5 | | mapdindp1.n |
. . . . . 6
β’ π = (LSpanβπ) |
6 | | mapdindp1.w |
. . . . . . 7
β’ (π β π β LVec) |
7 | | lveclmod 20583 |
. . . . . . 7
β’ (π β LVec β π β LMod) |
8 | 6, 7 | syl 17 |
. . . . . 6
β’ (π β π β LMod) |
9 | | mapdindp1.x |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
10 | 9 | eldifad 3927 |
. . . . . 6
β’ (π β π β π) |
11 | 3, 4, 5, 8, 10 | lsppr0 20569 |
. . . . 5
β’ (π β (πβ{π, 0 }) = (πβ{π})) |
12 | 2, 11 | sylan9eqr 2799 |
. . . 4
β’ ((π β§ (π + π) = 0 ) β (πβ{π, (π + π)}) = (πβ{π})) |
13 | | mapdindp1.y |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
14 | 13 | eldifad 3927 |
. . . . . . 7
β’ (π β π β π) |
15 | | prssi 4786 |
. . . . . . 7
β’ ((π β π β§ π β π) β {π, π} β π) |
16 | 10, 14, 15 | syl2anc 585 |
. . . . . 6
β’ (π β {π, π} β π) |
17 | | snsspr1 4779 |
. . . . . . 7
β’ {π} β {π, π} |
18 | 17 | a1i 11 |
. . . . . 6
β’ (π β {π} β {π, π}) |
19 | 3, 5 | lspss 20461 |
. . . . . 6
β’ ((π β LMod β§ {π, π} β π β§ {π} β {π, π}) β (πβ{π}) β (πβ{π, π})) |
20 | 8, 16, 18, 19 | syl3anc 1372 |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π, π})) |
21 | 20 | adantr 482 |
. . . 4
β’ ((π β§ (π + π) = 0 ) β (πβ{π}) β (πβ{π, π})) |
22 | 12, 21 | eqsstrd 3987 |
. . 3
β’ ((π β§ (π + π) = 0 ) β (πβ{π, (π + π)}) β (πβ{π, π})) |
23 | | mapdindp1.f |
. . . 4
β’ (π β Β¬ π€ β (πβ{π, π})) |
24 | 23 | adantr 482 |
. . 3
β’ ((π β§ (π + π) = 0 ) β Β¬ π€ β (πβ{π, π})) |
25 | 22, 24 | ssneldd 3952 |
. 2
β’ ((π β§ (π + π) = 0 ) β Β¬ π€ β (πβ{π, (π + π)})) |
26 | 23 | adantr 482 |
. . 3
β’ ((π β§ (π + π) β 0 ) β Β¬ π€ β (πβ{π, π})) |
27 | | mapdindp1.p |
. . . . . 6
β’ + =
(+gβπ) |
28 | 6 | adantr 482 |
. . . . . 6
β’ ((π β§ (π + π) β 0 ) β π β LVec) |
29 | 9 | adantr 482 |
. . . . . 6
β’ ((π β§ (π + π) β 0 ) β π β (π β { 0 })) |
30 | 13 | adantr 482 |
. . . . . 6
β’ ((π β§ (π + π) β 0 ) β π β (π β { 0 })) |
31 | | mapdindp1.z |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
32 | 31 | adantr 482 |
. . . . . 6
β’ ((π β§ (π + π) β 0 ) β π β (π β { 0 })) |
33 | | mapdindp1.W |
. . . . . . 7
β’ (π β π€ β (π β { 0 })) |
34 | 33 | adantr 482 |
. . . . . 6
β’ ((π β§ (π + π) β 0 ) β π€ β (π β { 0 })) |
35 | | mapdindp1.e |
. . . . . . 7
β’ (π β (πβ{π}) = (πβ{π})) |
36 | 35 | adantr 482 |
. . . . . 6
β’ ((π β§ (π + π) β 0 ) β (πβ{π}) = (πβ{π})) |
37 | | mapdindp1.ne |
. . . . . . 7
β’ (π β (πβ{π}) β (πβ{π})) |
38 | 37 | adantr 482 |
. . . . . 6
β’ ((π β§ (π + π) β 0 ) β (πβ{π}) β (πβ{π})) |
39 | | simpr 486 |
. . . . . 6
β’ ((π β§ (π + π) β 0 ) β (π + π) β 0 ) |
40 | 3, 27, 4, 5, 28, 29, 30, 32, 34, 36, 38, 26, 39 | mapdindp0 40211 |
. . . . 5
β’ ((π β§ (π + π) β 0 ) β (πβ{(π + π)}) = (πβ{π})) |
41 | 40 | oveq2d 7378 |
. . . 4
β’ ((π β§ (π + π) β 0 ) β ((πβ{π})(LSSumβπ)(πβ{(π + π)})) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
42 | | eqid 2737 |
. . . . . 6
β’
(LSSumβπ) =
(LSSumβπ) |
43 | 31 | eldifad 3927 |
. . . . . . 7
β’ (π β π β π) |
44 | 3, 27 | lmodvacl 20352 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
45 | 8, 14, 43, 44 | syl3anc 1372 |
. . . . . 6
β’ (π β (π + π) β π) |
46 | 3, 5, 42, 8, 10, 45 | lsmpr 20566 |
. . . . 5
β’ (π β (πβ{π, (π + π)}) = ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
47 | 46 | adantr 482 |
. . . 4
β’ ((π β§ (π + π) β 0 ) β (πβ{π, (π + π)}) = ((πβ{π})(LSSumβπ)(πβ{(π + π)}))) |
48 | 3, 5, 42, 8, 10, 14 | lsmpr 20566 |
. . . . 5
β’ (π β (πβ{π, π}) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
49 | 48 | adantr 482 |
. . . 4
β’ ((π β§ (π + π) β 0 ) β (πβ{π, π}) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
50 | 41, 47, 49 | 3eqtr4d 2787 |
. . 3
β’ ((π β§ (π + π) β 0 ) β (πβ{π, (π + π)}) = (πβ{π, π})) |
51 | 26, 50 | neleqtrrd 2861 |
. 2
β’ ((π β§ (π + π) β 0 ) β Β¬ π€ β (πβ{π, (π + π)})) |
52 | 25, 51 | pm2.61dane 3033 |
1
β’ (π β Β¬ π€ β (πβ{π, (π + π)})) |