Step | Hyp | Ref
| Expression |
1 | | hdmap1eulem.h |
. . 3
β’ π» = (LHypβπΎ) |
2 | | hdmap1eulem.u |
. . 3
β’ π = ((DVecHβπΎ)βπ) |
3 | | hdmap1eulem.v |
. . 3
β’ π = (Baseβπ) |
4 | | hdmap1eulem.s |
. . 3
β’ β =
(-gβπ) |
5 | | hdmap1eulem.o |
. . 3
β’ 0 =
(0gβπ) |
6 | | hdmap1eulem.n |
. . 3
β’ π = (LSpanβπ) |
7 | | hdmap1eulem.c |
. . 3
β’ πΆ = ((LCDualβπΎ)βπ) |
8 | | hdmap1eulem.d |
. . 3
β’ π· = (BaseβπΆ) |
9 | | hdmap1eulem.r |
. . 3
β’ π
= (-gβπΆ) |
10 | | hdmap1eulem.q |
. . 3
β’ π = (0gβπΆ) |
11 | | hdmap1eulem.j |
. . 3
β’ π½ = (LSpanβπΆ) |
12 | | hdmap1eulem.m |
. . 3
β’ π = ((mapdβπΎ)βπ) |
13 | | hdmap1eulem.l |
. . 3
β’ πΏ = (π₯ β V β¦ if((2nd
βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))))) |
14 | | hdmap1eulem.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
15 | | hdmap1eulem.f |
. . 3
β’ (π β πΉ β π·) |
16 | | hdmap1eulem.mn |
. . 3
β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) |
17 | | hdmap1eulem.x |
. . 3
β’ (π β π β (π β { 0 })) |
18 | | hdmap1eulem.y |
. . 3
β’ (π β π β π) |
19 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18 | mapdh9aOLDN 40303 |
. 2
β’ (π β β!π¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΏββ¨π§, (πΏββ¨π, πΉ, π§β©), πβ©))) |
20 | | hdmap1eulem.i |
. . . . . . . . . 10
β’ πΌ = ((HDMap1βπΎ)βπ) |
21 | 14 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πΎ β HL β§ π β π»)) |
22 | 17 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β (π β { 0 })) |
23 | 15 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β πΉ β π·) |
24 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π§ β π) |
25 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 20, 21, 22, 23, 24, 13 | hdmap1valc 40316 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πΌββ¨π, πΉ, π§β©) = (πΏββ¨π, πΉ, π§β©)) |
26 | 25 | oteq2d 4847 |
. . . . . . . 8
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β β¨π§, (πΌββ¨π, πΉ, π§β©), πβ© = β¨π§, (πΏββ¨π, πΉ, π§β©), πβ©) |
27 | 26 | fveq2d 6850 |
. . . . . . 7
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΌββ¨π§, (πΏββ¨π, πΉ, π§β©), πβ©)) |
28 | | eqid 2733 |
. . . . . . . . 9
β’
(LSubSpβπ) =
(LSubSpβπ) |
29 | 1, 2, 14 | dvhlmod 39623 |
. . . . . . . . . 10
β’ (π β π β LMod) |
30 | 29 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β LMod) |
31 | 17 | eldifad 3926 |
. . . . . . . . . . 11
β’ (π β π β π) |
32 | 3, 28, 6, 29, 31, 18 | lspprcl 20483 |
. . . . . . . . . 10
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
33 | 32 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πβ{π, π}) β (LSubSpβπ)) |
34 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β Β¬ π§ β (πβ{π, π})) |
35 | 5, 28, 30, 33, 24, 34 | lssneln0 20457 |
. . . . . . . 8
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π§ β (π β { 0 })) |
36 | 16 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πβ(πβ{π})) = (π½β{πΉ})) |
37 | 1, 2, 14 | dvhlvec 39622 |
. . . . . . . . . . . . 13
β’ (π β π β LVec) |
38 | 37 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β LVec) |
39 | 31 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β π) |
40 | 18 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β π β π) |
41 | 3, 6, 38, 24, 39, 40, 34 | lspindpi 20638 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β ((πβ{π§}) β (πβ{π}) β§ (πβ{π§}) β (πβ{π}))) |
42 | 41 | simpld 496 |
. . . . . . . . . 10
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πβ{π§}) β (πβ{π})) |
43 | 42 | necomd 2996 |
. . . . . . . . 9
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πβ{π}) β (πβ{π§})) |
44 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 21, 23, 36, 22, 24, 43 | mapdhcl 40240 |
. . . . . . . 8
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πΏββ¨π, πΉ, π§β©) β π·) |
45 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 20, 21, 35, 44, 40, 13 | hdmap1valc 40316 |
. . . . . . 7
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πΌββ¨π§, (πΏββ¨π, πΉ, π§β©), πβ©) = (πΏββ¨π§, (πΏββ¨π, πΉ, π§β©), πβ©)) |
46 | 27, 45 | eqtrd 2773 |
. . . . . 6
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) = (πΏββ¨π§, (πΏββ¨π, πΉ, π§β©), πβ©)) |
47 | 46 | eqeq2d 2744 |
. . . . 5
β’ (((π β§ π§ β π) β§ Β¬ π§ β (πβ{π, π})) β (π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©) β π¦ = (πΏββ¨π§, (πΏββ¨π, πΉ, π§β©), πβ©))) |
48 | 47 | pm5.74da 803 |
. . . 4
β’ ((π β§ π§ β π) β ((Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)) β (Β¬ π§ β (πβ{π, π}) β π¦ = (πΏββ¨π§, (πΏββ¨π, πΉ, π§β©), πβ©)))) |
49 | 48 | ralbidva 3169 |
. . 3
β’ (π β (βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)) β βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΏββ¨π§, (πΏββ¨π, πΉ, π§β©), πβ©)))) |
50 | 49 | reubidv 3370 |
. 2
β’ (π β (β!π¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©)) β β!π¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΏββ¨π§, (πΏββ¨π, πΉ, π§β©), πβ©)))) |
51 | 19, 50 | mpbird 257 |
1
β’ (π β β!π¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©))) |