Step | Hyp | Ref
| Expression |
1 | | mapdindp1.v |
. . 3
β’ π = (Baseβπ) |
2 | | mapdindp1.o |
. . 3
β’ 0 =
(0gβπ) |
3 | | mapdindp1.n |
. . 3
β’ π = (LSpanβπ) |
4 | | mapdindp1.w |
. . 3
β’ (π β π β LVec) |
5 | | mapdindp1.z |
. . 3
β’ (π β π β (π β { 0 })) |
6 | | lveclmod 20583 |
. . . . 5
β’ (π β LVec β π β LMod) |
7 | 4, 6 | syl 17 |
. . . 4
β’ (π β π β LMod) |
8 | | mapdindp1.W |
. . . . 5
β’ (π β π€ β (π β { 0 })) |
9 | 8 | eldifad 3927 |
. . . 4
β’ (π β π€ β π) |
10 | | mapdindp1.y |
. . . . 5
β’ (π β π β (π β { 0 })) |
11 | 10 | eldifad 3927 |
. . . 4
β’ (π β π β π) |
12 | | mapdindp1.p |
. . . . 5
β’ + =
(+gβπ) |
13 | 1, 12 | lmodvacl 20352 |
. . . 4
β’ ((π β LMod β§ π€ β π β§ π β π) β (π€ + π) β π) |
14 | 7, 9, 11, 13 | syl3anc 1372 |
. . 3
β’ (π β (π€ + π) β π) |
15 | | mapdindp1.x |
. . . 4
β’ (π β π β (π β { 0 })) |
16 | 15 | eldifad 3927 |
. . 3
β’ (π β π β π) |
17 | | mapdindp1.e |
. . . 4
β’ (π β (πβ{π}) = (πβ{π})) |
18 | | mapdindp1.f |
. . . . . . . . 9
β’ (π β Β¬ π€ β (πβ{π, π})) |
19 | 1, 3, 4, 9, 16, 11, 18 | lspindpi 20609 |
. . . . . . . 8
β’ (π β ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))) |
20 | 19 | simprd 497 |
. . . . . . 7
β’ (π β (πβ{π€}) β (πβ{π})) |
21 | 20 | necomd 3000 |
. . . . . 6
β’ (π β (πβ{π}) β (πβ{π€})) |
22 | 1, 12, 2, 3, 4, 11,
8, 21 | lspindp3 20613 |
. . . . 5
β’ (π β (πβ{π}) β (πβ{(π + π€)})) |
23 | 1, 12 | lmodcom 20384 |
. . . . . . . 8
β’ ((π β LMod β§ π€ β π β§ π β π) β (π€ + π) = (π + π€)) |
24 | 7, 9, 11, 23 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π€ + π) = (π + π€)) |
25 | 24 | sneqd 4603 |
. . . . . 6
β’ (π β {(π€ + π)} = {(π + π€)}) |
26 | 25 | fveq2d 6851 |
. . . . 5
β’ (π β (πβ{(π€ + π)}) = (πβ{(π + π€)})) |
27 | 22, 26 | neeqtrrd 3019 |
. . . 4
β’ (π β (πβ{π}) β (πβ{(π€ + π)})) |
28 | 17, 27 | eqnetrrd 3013 |
. . 3
β’ (π β (πβ{π}) β (πβ{(π€ + π)})) |
29 | | mapdindp1.ne |
. . . . . 6
β’ (π β (πβ{π}) β (πβ{π})) |
30 | 1, 2, 3, 4, 15, 11, 9, 29, 18 | lspindp1 20610 |
. . . . 5
β’ (π β ((πβ{π€}) β (πβ{π}) β§ Β¬ π β (πβ{π€, π}))) |
31 | 30 | simprd 497 |
. . . 4
β’ (π β Β¬ π β (πβ{π€, π})) |
32 | | eqid 2737 |
. . . . . 6
β’
(LSSumβπ) =
(LSSumβπ) |
33 | 5 | eldifad 3927 |
. . . . . 6
β’ (π β π β π) |
34 | 1, 3, 32, 7, 33, 14 | lsmpr 20566 |
. . . . 5
β’ (π β (πβ{π, (π€ + π)}) = ((πβ{π})(LSSumβπ)(πβ{(π€ + π)}))) |
35 | 1, 12 | lmodcom 20384 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π β§ π€ β π) β (π + π€) = (π€ + π)) |
36 | 7, 11, 9, 35 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π + π€) = (π€ + π)) |
37 | 36 | preq2d 4706 |
. . . . . . . 8
β’ (π β {π, (π + π€)} = {π, (π€ + π)}) |
38 | 37 | fveq2d 6851 |
. . . . . . 7
β’ (π β (πβ{π, (π + π€)}) = (πβ{π, (π€ + π)})) |
39 | 1, 12, 3, 7, 11, 9 | lspprabs 20572 |
. . . . . . 7
β’ (π β (πβ{π, (π + π€)}) = (πβ{π, π€})) |
40 | 1, 3, 32, 7, 11, 14 | lsmpr 20566 |
. . . . . . 7
β’ (π β (πβ{π, (π€ + π)}) = ((πβ{π})(LSSumβπ)(πβ{(π€ + π)}))) |
41 | 38, 39, 40 | 3eqtr3rd 2786 |
. . . . . 6
β’ (π β ((πβ{π})(LSSumβπ)(πβ{(π€ + π)})) = (πβ{π, π€})) |
42 | 17 | oveq1d 7377 |
. . . . . 6
β’ (π β ((πβ{π})(LSSumβπ)(πβ{(π€ + π)})) = ((πβ{π})(LSSumβπ)(πβ{(π€ + π)}))) |
43 | | prcom 4698 |
. . . . . . . 8
β’ {π, π€} = {π€, π} |
44 | 43 | fveq2i 6850 |
. . . . . . 7
β’ (πβ{π, π€}) = (πβ{π€, π}) |
45 | 44 | a1i 11 |
. . . . . 6
β’ (π β (πβ{π, π€}) = (πβ{π€, π})) |
46 | 41, 42, 45 | 3eqtr3d 2785 |
. . . . 5
β’ (π β ((πβ{π})(LSSumβπ)(πβ{(π€ + π)})) = (πβ{π€, π})) |
47 | 34, 46 | eqtrd 2777 |
. . . 4
β’ (π β (πβ{π, (π€ + π)}) = (πβ{π€, π})) |
48 | 31, 47 | neleqtrrd 2861 |
. . 3
β’ (π β Β¬ π β (πβ{π, (π€ + π)})) |
49 | 1, 2, 3, 4, 5, 14,
16, 28, 48 | lspindp1 20610 |
. 2
β’ (π β ((πβ{π}) β (πβ{(π€ + π)}) β§ Β¬ π β (πβ{π, (π€ + π)}))) |
50 | 49 | simprd 497 |
1
β’ (π β Β¬ π β (πβ{π, (π€ + π)})) |