Step | Hyp | Ref
| Expression |
1 | | hdmapval3.h |
. . 3
β’ π» = (LHypβπΎ) |
2 | | hdmapval3.u |
. . 3
β’ π = ((DVecHβπΎ)βπ) |
3 | | hdmapval3.v |
. . 3
β’ π = (Baseβπ) |
4 | | eqid 2733 |
. . 3
β’
(0gβπ) = (0gβπ) |
5 | | hdmapval3.n |
. . 3
β’ π = (LSpanβπ) |
6 | | hdmapval3.c |
. . 3
β’ πΆ = ((LCDualβπΎ)βπ) |
7 | | hdmapval3.d |
. . 3
β’ π· = (BaseβπΆ) |
8 | | eqid 2733 |
. . 3
β’
(LSpanβπΆ) =
(LSpanβπΆ) |
9 | | eqid 2733 |
. . 3
β’
((mapdβπΎ)βπ) = ((mapdβπΎ)βπ) |
10 | | hdmapval3.i |
. . 3
β’ πΌ = ((HDMap1βπΎ)βπ) |
11 | | hdmapval3.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
12 | | eqid 2733 |
. . . . . 6
β’
(0gβπΆ) = (0gβπΆ) |
13 | | hdmapval3.j |
. . . . . 6
β’ π½ = ((HVMapβπΎ)βπ) |
14 | | eqid 2733 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
15 | | eqid 2733 |
. . . . . . 7
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
16 | | hdmapval3.e |
. . . . . . 7
β’ πΈ = β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β© |
17 | 1, 14, 15, 2, 3, 4,
16, 11 | dvheveccl 39625 |
. . . . . 6
β’ (π β πΈ β (π β {(0gβπ)})) |
18 | 1, 2, 3, 4, 6, 7, 12, 13, 11, 17 | hvmapcl2 40279 |
. . . . 5
β’ (π β (π½βπΈ) β (π· β {(0gβπΆ)})) |
19 | 18 | eldifad 3926 |
. . . 4
β’ (π β (π½βπΈ) β π·) |
20 | 1, 2, 3, 4, 5, 6, 8, 9, 13, 11, 17 | mapdhvmap 40282 |
. . . 4
β’ (π β (((mapdβπΎ)βπ)β(πβ{πΈ})) = ((LSpanβπΆ)β{(π½βπΈ)})) |
21 | 1, 2, 11 | dvhlvec 39622 |
. . . . . . 7
β’ (π β π β LVec) |
22 | | hdmapval3lem.x |
. . . . . . 7
β’ (π β π₯ β π) |
23 | 17 | eldifad 3926 |
. . . . . . 7
β’ (π β πΈ β π) |
24 | | hdmapval3lem.t |
. . . . . . . 8
β’ (π β π β (π β {(0gβπ)})) |
25 | 24 | eldifad 3926 |
. . . . . . 7
β’ (π β π β π) |
26 | | hdmapval3lem.xn |
. . . . . . 7
β’ (π β Β¬ π₯ β (πβ{πΈ, π})) |
27 | 3, 5, 21, 22, 23, 25, 26 | lspindpi 20638 |
. . . . . 6
β’ (π β ((πβ{π₯}) β (πβ{πΈ}) β§ (πβ{π₯}) β (πβ{π}))) |
28 | 27 | simpld 496 |
. . . . 5
β’ (π β (πβ{π₯}) β (πβ{πΈ})) |
29 | 28 | necomd 2996 |
. . . 4
β’ (π β (πβ{πΈ}) β (πβ{π₯})) |
30 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 19, 20, 29, 17, 22 | hdmap1cl 40317 |
. . 3
β’ (π β (πΌββ¨πΈ, (π½βπΈ), π₯β©) β π·) |
31 | | eqidd 2734 |
. . . . 5
β’ (π β (πΌββ¨πΈ, (π½βπΈ), π₯β©) = (πΌββ¨πΈ, (π½βπΈ), π₯β©)) |
32 | | eqid 2733 |
. . . . . 6
β’
(-gβπ) = (-gβπ) |
33 | | eqid 2733 |
. . . . . 6
β’
(-gβπΆ) = (-gβπΆ) |
34 | | eqid 2733 |
. . . . . . 7
β’
(LSubSpβπ) =
(LSubSpβπ) |
35 | 1, 2, 11 | dvhlmod 39623 |
. . . . . . 7
β’ (π β π β LMod) |
36 | 3, 34, 5, 35, 23, 25 | lspprcl 20483 |
. . . . . . 7
β’ (π β (πβ{πΈ, π}) β (LSubSpβπ)) |
37 | 4, 34, 35, 36, 22, 26 | lssneln0 20457 |
. . . . . 6
β’ (π β π₯ β (π β {(0gβπ)})) |
38 | 1, 2, 3, 32, 4, 5,
6, 7, 33, 8, 9, 10, 11, 17, 19, 37, 30, 29, 20 | hdmap1eq 40314 |
. . . . 5
β’ (π β ((πΌββ¨πΈ, (π½βπΈ), π₯β©) = (πΌββ¨πΈ, (π½βπΈ), π₯β©) β ((((mapdβπΎ)βπ)β(πβ{π₯})) = ((LSpanβπΆ)β{(πΌββ¨πΈ, (π½βπΈ), π₯β©)}) β§ (((mapdβπΎ)βπ)β(πβ{(πΈ(-gβπ)π₯)})) = ((LSpanβπΆ)β{((π½βπΈ)(-gβπΆ)(πΌββ¨πΈ, (π½βπΈ), π₯β©))})))) |
39 | 31, 38 | mpbid 231 |
. . . 4
β’ (π β ((((mapdβπΎ)βπ)β(πβ{π₯})) = ((LSpanβπΆ)β{(πΌββ¨πΈ, (π½βπΈ), π₯β©)}) β§ (((mapdβπΎ)βπ)β(πβ{(πΈ(-gβπ)π₯)})) = ((LSpanβπΆ)β{((π½βπΈ)(-gβπΆ)(πΌββ¨πΈ, (π½βπΈ), π₯β©))}))) |
40 | 39 | simpld 496 |
. . 3
β’ (π β (((mapdβπΎ)βπ)β(πβ{π₯})) = ((LSpanβπΆ)β{(πΌββ¨πΈ, (π½βπΈ), π₯β©)})) |
41 | | hdmapval3.te |
. . . 4
β’ (π β (πβ{π}) β (πβ{πΈ})) |
42 | 41 | necomd 2996 |
. . 3
β’ (π β (πβ{πΈ}) β (πβ{π})) |
43 | | hdmapval3.s |
. . . . 5
β’ π = ((HDMapβπΎ)βπ) |
44 | 3, 5, 35, 23, 25 | lspprid1 20502 |
. . . . . . . 8
β’ (π β πΈ β (πβ{πΈ, π})) |
45 | 34, 5, 35, 36, 44 | lspsnel5a 20501 |
. . . . . . 7
β’ (π β (πβ{πΈ}) β (πβ{πΈ, π})) |
46 | 45, 45 | unssd 4150 |
. . . . . 6
β’ (π β ((πβ{πΈ}) βͺ (πβ{πΈ})) β (πβ{πΈ, π})) |
47 | 46, 26 | ssneldd 3951 |
. . . . 5
β’ (π β Β¬ π₯ β ((πβ{πΈ}) βͺ (πβ{πΈ}))) |
48 | 1, 16, 2, 3, 5, 6, 7, 13, 10, 43, 11, 23, 22, 47 | hdmapval2 40345 |
. . . 4
β’ (π β (πβπΈ) = (πΌββ¨π₯, (πΌββ¨πΈ, (π½βπΈ), π₯β©), πΈβ©)) |
49 | 1, 16, 13, 43, 11 | hdmapevec 40348 |
. . . 4
β’ (π β (πβπΈ) = (π½βπΈ)) |
50 | 48, 49 | eqtr3d 2775 |
. . 3
β’ (π β (πΌββ¨π₯, (πΌββ¨πΈ, (π½βπΈ), π₯β©), πΈβ©) = (π½βπΈ)) |
51 | 3, 5, 35, 23, 25 | lspprid2 20503 |
. . . . . . . 8
β’ (π β π β (πβ{πΈ, π})) |
52 | 34, 5, 35, 36, 51 | lspsnel5a 20501 |
. . . . . . 7
β’ (π β (πβ{π}) β (πβ{πΈ, π})) |
53 | 45, 52 | unssd 4150 |
. . . . . 6
β’ (π β ((πβ{πΈ}) βͺ (πβ{π})) β (πβ{πΈ, π})) |
54 | 53, 26 | ssneldd 3951 |
. . . . 5
β’ (π β Β¬ π₯ β ((πβ{πΈ}) βͺ (πβ{π}))) |
55 | 1, 16, 2, 3, 5, 6, 7, 13, 10, 43, 11, 25, 22, 54 | hdmapval2 40345 |
. . . 4
β’ (π β (πβπ) = (πΌββ¨π₯, (πΌββ¨πΈ, (π½βπΈ), π₯β©), πβ©)) |
56 | 55 | eqcomd 2739 |
. . 3
β’ (π β (πΌββ¨π₯, (πΌββ¨πΈ, (π½βπΈ), π₯β©), πβ©) = (πβπ)) |
57 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 30, 40, 37, 17, 24, 42, 26, 50, 56 | hdmap1eq4N 40319 |
. 2
β’ (π β (πΌββ¨πΈ, (π½βπΈ), πβ©) = (πβπ)) |
58 | 57 | eqcomd 2739 |
1
β’ (π β (πβπ) = (πΌββ¨πΈ, (π½βπΈ), πβ©)) |