Step | Hyp | Ref
| Expression |
1 | | mapdh.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
2 | | mapdh.c |
. . . . . 6
β’ πΆ = ((LCDualβπΎ)βπ) |
3 | | mapdh.k |
. . . . . 6
β’ (π β (πΎ β HL β§ π β π»)) |
4 | 1, 2, 3 | lcdlmod 40084 |
. . . . 5
β’ (π β πΆ β LMod) |
5 | | mapdh.q |
. . . . . 6
β’ π = (0gβπΆ) |
6 | | mapdh.i |
. . . . . 6
β’ πΌ = (π₯ β V β¦ if((2nd
βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))))) |
7 | | mapdh.m |
. . . . . 6
β’ π = ((mapdβπΎ)βπ) |
8 | | mapdh.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
9 | | mapdh.v |
. . . . . 6
β’ π = (Baseβπ) |
10 | | mapdh.s |
. . . . . 6
β’ β =
(-gβπ) |
11 | | mapdhc.o |
. . . . . 6
β’ 0 =
(0gβπ) |
12 | | mapdh.n |
. . . . . 6
β’ π = (LSpanβπ) |
13 | | mapdh.d |
. . . . . 6
β’ π· = (BaseβπΆ) |
14 | | mapdh.r |
. . . . . 6
β’ π
= (-gβπΆ) |
15 | | mapdh.j |
. . . . . 6
β’ π½ = (LSpanβπΆ) |
16 | | mapdhc.f |
. . . . . 6
β’ (π β πΉ β π·) |
17 | | mapdh.mn |
. . . . . 6
β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) |
18 | | mapdhcl.x |
. . . . . 6
β’ (π β π β (π β { 0 })) |
19 | | mapdh6d.w |
. . . . . . 7
β’ (π β π€ β (π β { 0 })) |
20 | 19 | eldifad 3927 |
. . . . . 6
β’ (π β π€ β π) |
21 | 1, 8, 3 | dvhlvec 39601 |
. . . . . . . . 9
β’ (π β π β LVec) |
22 | 18 | eldifad 3927 |
. . . . . . . . 9
β’ (π β π β π) |
23 | | mapdh6d.y |
. . . . . . . . . 10
β’ (π β π β (π β { 0 })) |
24 | 23 | eldifad 3927 |
. . . . . . . . 9
β’ (π β π β π) |
25 | | mapdh6d.wn |
. . . . . . . . 9
β’ (π β Β¬ π€ β (πβ{π, π})) |
26 | 9, 12, 21, 20, 22, 24, 25 | lspindpi 20609 |
. . . . . . . 8
β’ (π β ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))) |
27 | 26 | simpld 496 |
. . . . . . 7
β’ (π β (πβ{π€}) β (πβ{π})) |
28 | 27 | necomd 3000 |
. . . . . 6
β’ (π β (πβ{π}) β (πβ{π€})) |
29 | 5, 6, 1, 7, 8, 9, 10, 11, 12, 2, 13, 14, 15, 3, 16, 17, 18, 20, 28 | mapdhcl 40219 |
. . . . 5
β’ (π β (πΌββ¨π, πΉ, π€β©) β π·) |
30 | | mapdh.a |
. . . . . 6
β’ β =
(+gβπΆ) |
31 | 13, 30, 5 | lmod0vrid 20369 |
. . . . 5
β’ ((πΆ β LMod β§ (πΌββ¨π, πΉ, π€β©) β π·) β ((πΌββ¨π, πΉ, π€β©) β π) = (πΌββ¨π, πΉ, π€β©)) |
32 | 4, 29, 31 | syl2anc 585 |
. . . 4
β’ (π β ((πΌββ¨π, πΉ, π€β©) β π) = (πΌββ¨π, πΉ, π€β©)) |
33 | 32 | adantr 482 |
. . 3
β’ ((π β§ (π + π) = 0 ) β ((πΌββ¨π, πΉ, π€β©) β π) = (πΌββ¨π, πΉ, π€β©)) |
34 | | oteq3 4846 |
. . . . . 6
β’ ((π + π) = 0 β β¨π, πΉ, (π + π)β© = β¨π, πΉ, 0 β©) |
35 | 34 | fveq2d 6851 |
. . . . 5
β’ ((π + π) = 0 β (πΌββ¨π, πΉ, (π + π)β©) = (πΌββ¨π, πΉ, 0 β©)) |
36 | 5, 6, 11, 18, 16 | mapdhval0 40217 |
. . . . 5
β’ (π β (πΌββ¨π, πΉ, 0 β©) = π) |
37 | 35, 36 | sylan9eqr 2799 |
. . . 4
β’ ((π β§ (π + π) = 0 ) β (πΌββ¨π, πΉ, (π + π)β©) = π) |
38 | 37 | oveq2d 7378 |
. . 3
β’ ((π β§ (π + π) = 0 ) β ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©)) = ((πΌββ¨π, πΉ, π€β©) β π)) |
39 | | oveq2 7370 |
. . . . . 6
β’ ((π + π) = 0 β (π€ + (π + π)) = (π€ + 0 )) |
40 | 1, 8, 3 | dvhlmod 39602 |
. . . . . . 7
β’ (π β π β LMod) |
41 | | mapdh.p |
. . . . . . . 8
β’ + =
(+gβπ) |
42 | 9, 41, 11 | lmod0vrid 20369 |
. . . . . . 7
β’ ((π β LMod β§ π€ β π) β (π€ + 0 ) = π€) |
43 | 40, 20, 42 | syl2anc 585 |
. . . . . 6
β’ (π β (π€ + 0 ) = π€) |
44 | 39, 43 | sylan9eqr 2799 |
. . . . 5
β’ ((π β§ (π + π) = 0 ) β (π€ + (π + π)) = π€) |
45 | 44 | oteq3d 4849 |
. . . 4
β’ ((π β§ (π + π) = 0 ) β β¨π, πΉ, (π€ + (π + π))β© = β¨π, πΉ, π€β©) |
46 | 45 | fveq2d 6851 |
. . 3
β’ ((π β§ (π + π) = 0 ) β (πΌββ¨π, πΉ, (π€ + (π + π))β©) = (πΌββ¨π, πΉ, π€β©)) |
47 | 33, 38, 46 | 3eqtr4rd 2788 |
. 2
β’ ((π β§ (π + π) = 0 ) β (πΌββ¨π, πΉ, (π€ + (π + π))β©) = ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©))) |
48 | 3 | adantr 482 |
. . 3
β’ ((π β§ (π + π) β 0 ) β (πΎ β HL β§ π β π»)) |
49 | 16 | adantr 482 |
. . 3
β’ ((π β§ (π + π) β 0 ) β πΉ β π·) |
50 | 17 | adantr 482 |
. . 3
β’ ((π β§ (π + π) β 0 ) β (πβ(πβ{π})) = (π½β{πΉ})) |
51 | 18 | adantr 482 |
. . 3
β’ ((π β§ (π + π) β 0 ) β π β (π β { 0 })) |
52 | 19 | adantr 482 |
. . 3
β’ ((π β§ (π + π) β 0 ) β π€ β (π β { 0 })) |
53 | | mapdh6d.z |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
54 | 53 | eldifad 3927 |
. . . . . 6
β’ (π β π β π) |
55 | 9, 41 | lmodvacl 20352 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
56 | 40, 24, 54, 55 | syl3anc 1372 |
. . . . 5
β’ (π β (π + π) β π) |
57 | 56 | anim1i 616 |
. . . 4
β’ ((π β§ (π + π) β 0 ) β ((π + π) β π β§ (π + π) β 0 )) |
58 | | eldifsn 4752 |
. . . 4
β’ ((π + π) β (π β { 0 }) β ((π + π) β π β§ (π + π) β 0 )) |
59 | 57, 58 | sylibr 233 |
. . 3
β’ ((π β§ (π + π) β 0 ) β (π + π) β (π β { 0 })) |
60 | | mapdh6d.yz |
. . . . . . 7
β’ (π β (πβ{π}) = (πβ{π})) |
61 | | mapdh6d.xn |
. . . . . . . . 9
β’ (π β Β¬ π β (πβ{π, π})) |
62 | 9, 12, 21, 22, 24, 54, 61 | lspindpi 20609 |
. . . . . . . 8
β’ (π β ((πβ{π}) β (πβ{π}) β§ (πβ{π}) β (πβ{π}))) |
63 | 62 | simpld 496 |
. . . . . . 7
β’ (π β (πβ{π}) β (πβ{π})) |
64 | 9, 41, 11, 12, 21, 18, 23, 53, 19, 60, 63, 25 | mapdindp1 40212 |
. . . . . 6
β’ (π β (πβ{π}) β (πβ{(π + π)})) |
65 | 9, 41, 11, 12, 21, 18, 23, 53, 19, 60, 63, 25 | mapdindp2 40213 |
. . . . . 6
β’ (π β Β¬ π€ β (πβ{π, (π + π)})) |
66 | 9, 11, 12, 21, 18, 56, 20, 64, 65 | lspindp1 20610 |
. . . . 5
β’ (π β ((πβ{π€}) β (πβ{(π + π)}) β§ Β¬ π β (πβ{π€, (π + π)}))) |
67 | 66 | simprd 497 |
. . . 4
β’ (π β Β¬ π β (πβ{π€, (π + π)})) |
68 | 67 | adantr 482 |
. . 3
β’ ((π β§ (π + π) β 0 ) β Β¬ π β (πβ{π€, (π + π)})) |
69 | 26 | simprd 497 |
. . . . . . . . 9
β’ (π β (πβ{π€}) β (πβ{π})) |
70 | 9, 11, 12, 21, 19, 24, 69 | lspsnne1 20594 |
. . . . . . . 8
β’ (π β Β¬ π€ β (πβ{π})) |
71 | | eqid 2737 |
. . . . . . . . . 10
β’
(LSSumβπ) =
(LSSumβπ) |
72 | 9, 12, 71, 40, 24, 54 | lsmpr 20566 |
. . . . . . . . 9
β’ (π β (πβ{π, π}) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
73 | 60 | oveq2d 7378 |
. . . . . . . . 9
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) = ((πβ{π})(LSSumβπ)(πβ{π}))) |
74 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(LSubSpβπ) =
(LSubSpβπ) |
75 | 9, 74, 12 | lspsncl 20454 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
76 | 40, 24, 75 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (LSubSpβπ)) |
77 | 74 | lsssubg 20434 |
. . . . . . . . . . 11
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ)) β (πβ{π}) β (SubGrpβπ)) |
78 | 40, 76, 77 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (πβ{π}) β (SubGrpβπ)) |
79 | 71 | lsmidm 19452 |
. . . . . . . . . 10
β’ ((πβ{π}) β (SubGrpβπ) β ((πβ{π})(LSSumβπ)(πβ{π})) = (πβ{π})) |
80 | 78, 79 | syl 17 |
. . . . . . . . 9
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) = (πβ{π})) |
81 | 72, 73, 80 | 3eqtr2d 2783 |
. . . . . . . 8
β’ (π β (πβ{π, π}) = (πβ{π})) |
82 | 70, 81 | neleqtrrd 2861 |
. . . . . . 7
β’ (π β Β¬ π€ β (πβ{π, π})) |
83 | 9, 41, 12, 40, 24, 54, 20, 82 | lspindp4 20614 |
. . . . . 6
β’ (π β Β¬ π€ β (πβ{π, (π + π)})) |
84 | 9, 12, 21, 20, 24, 56, 83 | lspindpi 20609 |
. . . . 5
β’ (π β ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{(π + π)}))) |
85 | 84 | simprd 497 |
. . . 4
β’ (π β (πβ{π€}) β (πβ{(π + π)})) |
86 | 85 | adantr 482 |
. . 3
β’ ((π β§ (π + π) β 0 ) β (πβ{π€}) β (πβ{(π + π)})) |
87 | | eqidd 2738 |
. . 3
β’ ((π β§ (π + π) β 0 ) β (πΌββ¨π, πΉ, π€β©) = (πΌββ¨π, πΉ, π€β©)) |
88 | | eqidd 2738 |
. . 3
β’ ((π β§ (π + π) β 0 ) β (πΌββ¨π, πΉ, (π + π)β©) = (πΌββ¨π, πΉ, (π + π)β©)) |
89 | 5, 6, 1, 7, 8, 9, 10, 11, 12, 2, 13, 14, 15, 48, 49, 50, 51, 41, 30, 52, 59, 68, 86, 87, 88 | mapdh6aN 40227 |
. 2
β’ ((π β§ (π + π) β 0 ) β (πΌββ¨π, πΉ, (π€ + (π + π))β©) = ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©))) |
90 | 47, 89 | pm2.61dane 3033 |
1
β’ (π β (πΌββ¨π, πΉ, (π€ + (π + π))β©) = ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©))) |