Step | Hyp | Ref
| Expression |
1 | | mapdh.q |
. . . 4
β’ π = (0gβπΆ) |
2 | | mapdh.i |
. . . 4
β’ πΌ = (π₯ β V β¦ if((2nd
βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))))) |
3 | | mapdh.h |
. . . 4
β’ π» = (LHypβπΎ) |
4 | | mapdh.m |
. . . 4
β’ π = ((mapdβπΎ)βπ) |
5 | | mapdh.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
6 | | mapdh.v |
. . . 4
β’ π = (Baseβπ) |
7 | | mapdh.s |
. . . 4
β’ β =
(-gβπ) |
8 | | mapdhc.o |
. . . 4
β’ 0 =
(0gβπ) |
9 | | mapdh.n |
. . . 4
β’ π = (LSpanβπ) |
10 | | mapdh.c |
. . . 4
β’ πΆ = ((LCDualβπΎ)βπ) |
11 | | mapdh.d |
. . . 4
β’ π· = (BaseβπΆ) |
12 | | mapdh.r |
. . . 4
β’ π
= (-gβπΆ) |
13 | | mapdh.j |
. . . 4
β’ π½ = (LSpanβπΆ) |
14 | | mapdh.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
15 | | mapdhc.f |
. . . 4
β’ (π β πΉ β π·) |
16 | | mapdh.mn |
. . . 4
β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) |
17 | | mapdhcl.x |
. . . 4
β’ (π β π β (π β { 0 })) |
18 | | mapdh.p |
. . . 4
β’ + =
(+gβπ) |
19 | | mapdh.a |
. . . 4
β’ β =
(+gβπΆ) |
20 | | mapdh6d.xn |
. . . 4
β’ (π β Β¬ π β (πβ{π, π})) |
21 | | mapdh6d.yz |
. . . 4
β’ (π β (πβ{π}) = (πβ{π})) |
22 | | mapdh6d.y |
. . . 4
β’ (π β π β (π β { 0 })) |
23 | | mapdh6d.z |
. . . 4
β’ (π β π β (π β { 0 })) |
24 | | mapdh6d.w |
. . . 4
β’ (π β π€ β (π β { 0 })) |
25 | | mapdh6d.wn |
. . . 4
β’ (π β Β¬ π€ β (πβ{π, π})) |
26 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25 | mapdh6gN 40251 |
. . 3
β’ (π β ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©)) = (((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, πβ©)) β (πΌββ¨π, πΉ, πβ©))) |
27 | 3, 10, 14 | lcdlmod 40101 |
. . . 4
β’ (π β πΆ β LMod) |
28 | 24 | eldifad 3923 |
. . . . 5
β’ (π β π€ β π) |
29 | 3, 5, 14 | dvhlvec 39618 |
. . . . . . . 8
β’ (π β π β LVec) |
30 | 17 | eldifad 3923 |
. . . . . . . 8
β’ (π β π β π) |
31 | 22 | eldifad 3923 |
. . . . . . . 8
β’ (π β π β π) |
32 | 6, 9, 29, 28, 30, 31, 25 | lspindpi 20609 |
. . . . . . 7
β’ (π β ((πβ{π€}) β (πβ{π}) β§ (πβ{π€}) β (πβ{π}))) |
33 | 32 | simpld 496 |
. . . . . 6
β’ (π β (πβ{π€}) β (πβ{π})) |
34 | 33 | necomd 2996 |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π€})) |
35 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 28, 34 | mapdhcl 40236 |
. . . 4
β’ (π β (πΌββ¨π, πΉ, π€β©) β π·) |
36 | 23 | eldifad 3923 |
. . . . . . 7
β’ (π β π β π) |
37 | 6, 9, 29, 30, 31, 36, 20 | lspindpi 20609 |
. . . . . 6
β’ (π β ((πβ{π}) β (πβ{π}) β§ (πβ{π}) β (πβ{π}))) |
38 | 37 | simpld 496 |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π})) |
39 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 31, 38 | mapdhcl 40236 |
. . . 4
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
40 | 37 | simprd 497 |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π})) |
41 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 36, 40 | mapdhcl 40236 |
. . . 4
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
42 | 11, 19 | lmodass 20352 |
. . . 4
β’ ((πΆ β LMod β§ ((πΌββ¨π, πΉ, π€β©) β π· β§ (πΌββ¨π, πΉ, πβ©) β π· β§ (πΌββ¨π, πΉ, πβ©) β π·)) β (((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, πβ©)) β (πΌββ¨π, πΉ, πβ©)) = ((πΌββ¨π, πΉ, π€β©) β ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)))) |
43 | 27, 35, 39, 41, 42 | syl13anc 1373 |
. . 3
β’ (π β (((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, πβ©)) β (πΌββ¨π, πΉ, πβ©)) = ((πΌββ¨π, πΉ, π€β©) β ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)))) |
44 | 26, 43 | eqtrd 2773 |
. 2
β’ (π β ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©)) = ((πΌββ¨π, πΉ, π€β©) β ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)))) |
45 | 3, 5, 14 | dvhlmod 39619 |
. . . . 5
β’ (π β π β LMod) |
46 | 6, 18 | lmodvacl 20351 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
47 | 45, 31, 36, 46 | syl3anc 1372 |
. . . 4
β’ (π β (π + π) β π) |
48 | 6, 18, 8, 9, 29, 17, 22, 23, 24, 21, 38, 25 | mapdindp1 40229 |
. . . 4
β’ (π β (πβ{π}) β (πβ{(π + π)})) |
49 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 47, 48 | mapdhcl 40236 |
. . 3
β’ (π β (πΌββ¨π, πΉ, (π + π)β©) β π·) |
50 | 11, 19 | lmodvacl 20351 |
. . . 4
β’ ((πΆ β LMod β§ (πΌββ¨π, πΉ, πβ©) β π· β§ (πΌββ¨π, πΉ, πβ©) β π·) β ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)) β π·) |
51 | 27, 39, 41, 50 | syl3anc 1372 |
. . 3
β’ (π β ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)) β π·) |
52 | 11, 19 | lmodlcan 20353 |
. . 3
β’ ((πΆ β LMod β§ ((πΌββ¨π, πΉ, (π + π)β©) β π· β§ ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)) β π· β§ (πΌββ¨π, πΉ, π€β©) β π·)) β (((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©)) = ((πΌββ¨π, πΉ, π€β©) β ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)))) |
53 | 27, 49, 51, 35, 52 | syl13anc 1373 |
. 2
β’ (π β (((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©)) = ((πΌββ¨π, πΉ, π€β©) β ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)))) |
54 | 44, 53 | mpbid 231 |
1
β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) |