Step | Hyp | Ref
| Expression |
1 | | mapdh8a.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | mapdh8a.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
3 | | mapdh8a.v |
. . . 4
β’ π = (Baseβπ) |
4 | | mapdh8a.s |
. . . 4
β’ β =
(-gβπ) |
5 | | mapdh8a.o |
. . . 4
β’ 0 =
(0gβπ) |
6 | | mapdh8a.n |
. . . 4
β’ π = (LSpanβπ) |
7 | | mapdh8a.c |
. . . 4
β’ πΆ = ((LCDualβπΎ)βπ) |
8 | | mapdh8a.d |
. . . 4
β’ π· = (BaseβπΆ) |
9 | | mapdh8a.r |
. . . 4
β’ π
= (-gβπΆ) |
10 | | mapdh8a.q |
. . . 4
β’ π = (0gβπΆ) |
11 | | mapdh8a.j |
. . . 4
β’ π½ = (LSpanβπΆ) |
12 | | mapdh8a.m |
. . . 4
β’ π = ((mapdβπΎ)βπ) |
13 | | mapdh8a.i |
. . . 4
β’ πΌ = (π₯ β V β¦ if((2nd
βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))))) |
14 | | mapdh8a.k |
. . . . 5
β’ (π β (πΎ β HL β§ π β π»)) |
15 | 14 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β (πΎ β HL β§ π β π»)) |
16 | | mapdh8b.eg |
. . . . . 6
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) |
17 | | mapdh8d.f |
. . . . . . 7
β’ (π β πΉ β π·) |
18 | | mapdh8d.mn |
. . . . . . 7
β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) |
19 | | mapdh8d.x |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
20 | | mapdh8d.y |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
21 | 20 | eldifad 3926 |
. . . . . . 7
β’ (π β π β π) |
22 | 1, 2, 14 | dvhlvec 39622 |
. . . . . . . . 9
β’ (π β π β LVec) |
23 | 19 | eldifad 3926 |
. . . . . . . . 9
β’ (π β π β π) |
24 | | mapdh8d.w |
. . . . . . . . . 10
β’ (π β π€ β (π β { 0 })) |
25 | 24 | eldifad 3926 |
. . . . . . . . 9
β’ (π β π€ β π) |
26 | | mapdh8d.xn |
. . . . . . . . 9
β’ (π β Β¬ π β (πβ{π, π€})) |
27 | 3, 6, 22, 23, 21, 25, 26 | lspindpi 20638 |
. . . . . . . 8
β’ (π β ((πβ{π}) β (πβ{π}) β§ (πβ{π}) β (πβ{π€}))) |
28 | 27 | simpld 496 |
. . . . . . 7
β’ (π β (πβ{π}) β (πβ{π})) |
29 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 14, 17, 18, 19, 21, 28 | mapdhcl 40240 |
. . . . . 6
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
30 | 16, 29 | eqeltrrd 2835 |
. . . . 5
β’ (π β πΊ β π·) |
31 | 30 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β πΊ β π·) |
32 | 10, 13, 1, 12, 2, 3,
4, 5, 6, 7,
8, 9, 11, 14, 17, 18, 19, 20, 30, 28 | mapdheq 40241 |
. . . . . . 7
β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β ((πβ(πβ{π})) = (π½β{πΊ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΊ)})))) |
33 | 16, 32 | mpbid 231 |
. . . . . 6
β’ (π β ((πβ(πβ{π})) = (π½β{πΊ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΊ)}))) |
34 | 33 | simpld 496 |
. . . . 5
β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) |
35 | 34 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β (πβ(πβ{π})) = (π½β{πΊ})) |
36 | | mapdh8d.vw |
. . . . . 6
β’ (π β (πβ{π}) β (πβ{π€})) |
37 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 17, 18, 16, 19, 20, 36, 24, 26 | mapdh8a 40288 |
. . . . 5
β’ (π β (πΌββ¨π, πΊ, π€β©) = (πΌββ¨π, πΉ, π€β©)) |
38 | 37 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β (πΌββ¨π, πΊ, π€β©) = (πΌββ¨π, πΉ, π€β©)) |
39 | 20 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β π β (π β { 0 })) |
40 | 24 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β π€ β (π β { 0 })) |
41 | | mapdh8d.wt |
. . . . 5
β’ (π β (πβ{π€}) β (πβ{π})) |
42 | 41 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β (πβ{π€}) β (πβ{π})) |
43 | | mapdh8d.xt |
. . . . 5
β’ (π β π β (π β { 0 })) |
44 | 43 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β π β (π β { 0 })) |
45 | 36 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β (πβ{π}) β (πβ{π€})) |
46 | | simpr 486 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β π β (πβ{π, π})) |
47 | 26 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β Β¬ π β (πβ{π, π€})) |
48 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 15, 31, 35, 38, 39, 40, 42, 44, 45, 46, 47 | mapdh8b 40293 |
. . 3
β’ ((π β§ π β (πβ{π, π})) β (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©) = (πΌββ¨π, πΊ, πβ©)) |
49 | 17 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β πΉ β π·) |
50 | 18 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β (πβ(πβ{π})) = (π½β{πΉ})) |
51 | | eqidd 2734 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β (πΌββ¨π, πΉ, π€β©) = (πΌββ¨π, πΉ, π€β©)) |
52 | 19 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β π β (π β { 0 })) |
53 | | mapdh8d.yz |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π})) |
54 | 53 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β (πβ{π}) β (πβ{π})) |
55 | | mapdh8d.ut |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π})) |
56 | 55 | adantr 482 |
. . . 4
β’ ((π β§ π β (πβ{π, π})) β (πβ{π}) β (πβ{π})) |
57 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 15, 49, 50, 51, 52, 39, 44, 54, 40, 42, 56, 45, 46, 47 | mapdh8c 40294 |
. . 3
β’ ((π β§ π β (πβ{π, π})) β (πΌββ¨π€, (πΌββ¨π, πΉ, π€β©), πβ©) = (πΌββ¨π, πΉ, πβ©)) |
58 | 48, 57 | eqtr3d 2775 |
. 2
β’ ((π β§ π β (πβ{π, π})) β (πΌββ¨π, πΊ, πβ©) = (πΌββ¨π, πΉ, πβ©)) |
59 | 14 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β (πβ{π, π})) β (πΎ β HL β§ π β π»)) |
60 | 17 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β (πβ{π, π})) β πΉ β π·) |
61 | 18 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β (πβ{π, π})) β (πβ(πβ{π})) = (π½β{πΉ})) |
62 | 16 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β (πβ{π, π})) β (πΌββ¨π, πΉ, πβ©) = πΊ) |
63 | 19 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β (πβ{π, π})) β π β (π β { 0 })) |
64 | 20 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β (πβ{π, π})) β π β (π β { 0 })) |
65 | 53 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β (πβ{π, π})) β (πβ{π}) β (πβ{π})) |
66 | 43 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β (πβ{π, π})) β π β (π β { 0 })) |
67 | | simpr 486 |
. . 3
β’ ((π β§ Β¬ π β (πβ{π, π})) β Β¬ π β (πβ{π, π})) |
68 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 59, 60, 61, 62, 63, 64, 65, 66, 67 | mapdh8a 40288 |
. 2
β’ ((π β§ Β¬ π β (πβ{π, π})) β (πΌββ¨π, πΊ, πβ©) = (πΌββ¨π, πΉ, πβ©)) |
69 | 58, 68 | pm2.61dan 812 |
1
β’ (π β (πΌββ¨π, πΊ, πβ©) = (πΌββ¨π, πΉ, πβ©)) |