Step | Hyp | Ref
| Expression |
1 | | hdmap11.h |
. . 3
β’ π» = (LHypβπΎ) |
2 | | hdmap11.u |
. . 3
β’ π = ((DVecHβπΎ)βπ) |
3 | | hdmap11.v |
. . 3
β’ π = (Baseβπ) |
4 | | hdmap11.p |
. . 3
β’ + =
(+gβπ) |
5 | | hdmap11.o |
. . 3
β’ 0 =
(0gβπ) |
6 | | hdmap11.n |
. . 3
β’ π = (LSpanβπ) |
7 | | hdmap11.c |
. . 3
β’ πΆ = ((LCDualβπΎ)βπ) |
8 | | hdmap11.d |
. . 3
β’ π· = (BaseβπΆ) |
9 | | hdmap11.a |
. . 3
β’ β =
(+gβπΆ) |
10 | | hdmap11.l |
. . 3
β’ πΏ = (LSpanβπΆ) |
11 | | hdmap11.m |
. . 3
β’ π = ((mapdβπΎ)βπ) |
12 | | hdmap11.i |
. . 3
β’ πΌ = ((HDMap1βπΎ)βπ) |
13 | | hdmap11.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
14 | | eqid 2733 |
. . . . . 6
β’
(0gβπΆ) = (0gβπΆ) |
15 | | hdmap11.j |
. . . . . 6
β’ π½ = ((HVMapβπΎ)βπ) |
16 | | eqid 2733 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
17 | | eqid 2733 |
. . . . . . 7
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
18 | | hdmap11.e |
. . . . . . 7
β’ πΈ = β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β© |
19 | 1, 16, 17, 2, 3, 5,
18, 13 | dvheveccl 39621 |
. . . . . 6
β’ (π β πΈ β (π β { 0 })) |
20 | 1, 2, 3, 5, 7, 8, 14, 15, 13, 19 | hvmapcl2 40275 |
. . . . 5
β’ (π β (π½βπΈ) β (π· β {(0gβπΆ)})) |
21 | 20 | eldifad 3923 |
. . . 4
β’ (π β (π½βπΈ) β π·) |
22 | 1, 2, 3, 5, 6, 7, 10, 11, 15, 13, 19 | mapdhvmap 40278 |
. . . 4
β’ (π β (πβ(πβ{πΈ})) = (πΏβ{(π½βπΈ)})) |
23 | | hdmap11lem0.2a |
. . . . 5
β’ (π β (πβ{π§}) β (πβ{πΈ})) |
24 | 23 | necomd 2996 |
. . . 4
β’ (π β (πβ{πΈ}) β (πβ{π§})) |
25 | | hdmap11lem0.1a |
. . . 4
β’ (π β π§ β π) |
26 | 1, 2, 3, 5, 6, 7, 8, 10, 11, 12, 13, 21, 22, 24, 19, 25 | hdmap1cl 40313 |
. . 3
β’ (π β (πΌββ¨πΈ, (π½βπΈ), π§β©) β π·) |
27 | | eqid 2733 |
. . . 4
β’
(LSubSpβπ) =
(LSubSpβπ) |
28 | 1, 2, 13 | dvhlmod 39619 |
. . . 4
β’ (π β π β LMod) |
29 | | hdmap11.x |
. . . . 5
β’ (π β π β π) |
30 | | hdmap11.y |
. . . . 5
β’ (π β π β π) |
31 | 3, 27, 6, 28, 29, 30 | lspprcl 20454 |
. . . 4
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
32 | | hdmap11lem0.6 |
. . . 4
β’ (π β Β¬ π§ β (πβ{π, π})) |
33 | 5, 27, 28, 31, 25, 32 | lssneln0 20428 |
. . 3
β’ (π β π§ β (π β { 0 })) |
34 | | eqidd 2734 |
. . . . 5
β’ (π β (πΌββ¨πΈ, (π½βπΈ), π§β©) = (πΌββ¨πΈ, (π½βπΈ), π§β©)) |
35 | | eqid 2733 |
. . . . . 6
β’
(-gβπ) = (-gβπ) |
36 | | eqid 2733 |
. . . . . 6
β’
(-gβπΆ) = (-gβπΆ) |
37 | 1, 2, 3, 35, 5, 6,
7, 8, 36, 10, 11, 12, 13, 19, 21, 33, 26, 24, 22 | hdmap1eq 40310 |
. . . . 5
β’ (π β ((πΌββ¨πΈ, (π½βπΈ), π§β©) = (πΌββ¨πΈ, (π½βπΈ), π§β©) β ((πβ(πβ{π§})) = (πΏβ{(πΌββ¨πΈ, (π½βπΈ), π§β©)}) β§ (πβ(πβ{(πΈ(-gβπ)π§)})) = (πΏβ{((π½βπΈ)(-gβπΆ)(πΌββ¨πΈ, (π½βπΈ), π§β©))})))) |
38 | 34, 37 | mpbid 231 |
. . . 4
β’ (π β ((πβ(πβ{π§})) = (πΏβ{(πΌββ¨πΈ, (π½βπΈ), π§β©)}) β§ (πβ(πβ{(πΈ(-gβπ)π§)})) = (πΏβ{((π½βπΈ)(-gβπΆ)(πΌββ¨πΈ, (π½βπΈ), π§β©))}))) |
39 | 38 | simpld 496 |
. . 3
β’ (π β (πβ(πβ{π§})) = (πΏβ{(πΌββ¨πΈ, (π½βπΈ), π§β©)})) |
40 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 26, 33, 29, 30, 32, 39 | hdmap1l6 40330 |
. 2
β’ (π β (πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), (π + π)β©) = ((πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), πβ©) β (πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), πβ©))) |
41 | | hdmap11.s |
. . 3
β’ π = ((HDMapβπΎ)βπ) |
42 | 3, 4 | lmodvacl 20351 |
. . . 4
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
43 | 28, 29, 30, 42 | syl3anc 1372 |
. . 3
β’ (π β (π + π) β π) |
44 | 1, 2, 13 | dvhlvec 39618 |
. . . 4
β’ (π β π β LVec) |
45 | 19 | eldifad 3923 |
. . . 4
β’ (π β πΈ β π) |
46 | 3, 4, 6, 28, 29, 30 | lspprvacl 20475 |
. . . . . . 7
β’ (π β (π + π) β (πβ{π, π})) |
47 | 27, 6, 28, 31, 46 | lspsnel5a 20472 |
. . . . . 6
β’ (π β (πβ{(π + π)}) β (πβ{π, π})) |
48 | 47, 32 | ssneldd 3948 |
. . . . 5
β’ (π β Β¬ π§ β (πβ{(π + π)})) |
49 | 3, 6, 28, 25, 43, 48 | lspsnne2 20595 |
. . . 4
β’ (π β (πβ{π§}) β (πβ{(π + π)})) |
50 | 3, 6, 5, 44, 45, 43, 33, 23, 49 | hdmaplem4 40283 |
. . 3
β’ (π β Β¬ π§ β ((πβ{πΈ}) βͺ (πβ{(π + π)}))) |
51 | 1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 43, 25, 50 | hdmapval2 40341 |
. 2
β’ (π β (πβ(π + π)) = (πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), (π + π)β©)) |
52 | 3, 6, 44, 25, 29, 30, 32 | lspindpi 20609 |
. . . . . 6
β’ (π β ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) |
53 | 52 | simpld 496 |
. . . . 5
β’ (π β (πβ{π§}) β (πβ{π})) |
54 | 3, 6, 5, 44, 45, 29, 33, 23, 53 | hdmaplem4 40283 |
. . . 4
β’ (π β Β¬ π§ β ((πβ{πΈ}) βͺ (πβ{π}))) |
55 | 1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 29, 25, 54 | hdmapval2 40341 |
. . 3
β’ (π β (πβπ) = (πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), πβ©)) |
56 | 52 | simprd 497 |
. . . . 5
β’ (π β (πβ{π§}) β (πβ{π})) |
57 | 3, 6, 5, 44, 45, 30, 33, 23, 56 | hdmaplem4 40283 |
. . . 4
β’ (π β Β¬ π§ β ((πβ{πΈ}) βͺ (πβ{π}))) |
58 | 1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 30, 25, 57 | hdmapval2 40341 |
. . 3
β’ (π β (πβπ) = (πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), πβ©)) |
59 | 55, 58 | oveq12d 7376 |
. 2
β’ (π β ((πβπ) β (πβπ)) = ((πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), πβ©) β (πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), πβ©))) |
60 | 40, 51, 59 | 3eqtr4d 2783 |
1
β’ (π β (πβ(π + π)) = ((πβπ) β (πβπ))) |