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 | | mapdhe6.y |
. . . 4
β’ (π β π β (π β { 0 })) |
21 | | mapdhe6.z |
. . . 4
β’ (π β π β (π β { 0 })) |
22 | | mapdhe6.xn |
. . . 4
β’ (π β Β¬ π β (πβ{π, π})) |
23 | | mapdh6.yz |
. . . 4
β’ (π β (πβ{π}) β (πβ{π})) |
24 | | mapdh6.fg |
. . . 4
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) |
25 | | mapdh6.fe |
. . . 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 | mapdh6lem2N 40226 |
. . 3
β’ (π β (πβ(πβ{(π + π)})) = (π½β{(πΊ β πΈ)})) |
27 | 24, 25 | oveq12d 7380 |
. . . . 5
β’ (π β ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)) = (πΊ β πΈ)) |
28 | 27 | sneqd 4603 |
. . . 4
β’ (π β {((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))} = {(πΊ β πΈ)}) |
29 | 28 | fveq2d 6851 |
. . 3
β’ (π β (π½β{((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))}) = (π½β{(πΊ β πΈ)})) |
30 | 26, 29 | eqtr4d 2780 |
. 2
β’ (π β (πβ(πβ{(π + π)})) = (π½β{((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))})) |
31 | 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 | mapdh6lem1N 40225 |
. . 3
β’ (π β (πβ(πβ{(π β (π + π))})) = (π½β{(πΉπ
(πΊ β πΈ))})) |
32 | 27 | oveq2d 7378 |
. . . . 5
β’ (π β (πΉπ
((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) = (πΉπ
(πΊ β πΈ))) |
33 | 32 | sneqd 4603 |
. . . 4
β’ (π β {(πΉπ
((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)))} = {(πΉπ
(πΊ β πΈ))}) |
34 | 33 | fveq2d 6851 |
. . 3
β’ (π β (π½β{(πΉπ
((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)))}) = (π½β{(πΉπ
(πΊ β πΈ))})) |
35 | 31, 34 | eqtr4d 2780 |
. 2
β’ (π β (πβ(πβ{(π β (π + π))})) = (π½β{(πΉπ
((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)))})) |
36 | 3, 5, 14 | dvhlmod 39602 |
. . . . 5
β’ (π β π β LMod) |
37 | 20 | eldifad 3927 |
. . . . 5
β’ (π β π β π) |
38 | 21 | eldifad 3927 |
. . . . 5
β’ (π β π β π) |
39 | 6, 18 | lmodvacl 20352 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
40 | 36, 37, 38, 39 | syl3anc 1372 |
. . . 4
β’ (π β (π + π) β π) |
41 | 6, 18, 8, 9, 36, 37, 38, 23 | lmodindp1 20491 |
. . . 4
β’ (π β (π + π) β 0 ) |
42 | | eldifsn 4752 |
. . . 4
β’ ((π + π) β (π β { 0 }) β ((π + π) β π β§ (π + π) β 0 )) |
43 | 40, 41, 42 | sylanbrc 584 |
. . 3
β’ (π β (π + π) β (π β { 0 })) |
44 | 3, 10, 14 | lcdlmod 40084 |
. . . 4
β’ (π β πΆ β LMod) |
45 | 3, 5, 14 | dvhlvec 39601 |
. . . . . . 7
β’ (π β π β LVec) |
46 | 17 | eldifad 3927 |
. . . . . . 7
β’ (π β π β π) |
47 | 6, 8, 9, 45, 37, 21, 46, 23, 22 | lspindp2 20612 |
. . . . . 6
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
48 | 47 | simpld 496 |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π})) |
49 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 37, 48 | mapdhcl 40219 |
. . . 4
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
50 | 6, 8, 9, 45, 20, 38, 46, 23, 22 | lspindp1 20610 |
. . . . . 6
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
51 | 50 | simpld 496 |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π})) |
52 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 38, 51 | mapdhcl 40219 |
. . . 4
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
53 | 11, 19 | lmodvacl 20352 |
. . . 4
β’ ((πΆ β LMod β§ (πΌββ¨π, πΉ, πβ©) β π· β§ (πΌββ¨π, πΉ, πβ©) β π·) β ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)) β π·) |
54 | 44, 49, 52, 53 | syl3anc 1372 |
. . 3
β’ (π β ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)) β π·) |
55 | | eqid 2737 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
56 | 6, 55, 9, 36, 37, 38 | lspprcl 20455 |
. . . . . 6
β’ (π β (πβ{π, π}) β (LSubSpβπ)) |
57 | 6, 18, 9, 36, 37, 38 | lspprvacl 20476 |
. . . . . 6
β’ (π β (π + π) β (πβ{π, π})) |
58 | 55, 9, 36, 56, 57 | lspsnel5a 20473 |
. . . . 5
β’ (π β (πβ{(π + π)}) β (πβ{π, π})) |
59 | 6, 55, 9, 36, 56, 46 | lspsnel5 20472 |
. . . . . 6
β’ (π β (π β (πβ{π, π}) β (πβ{π}) β (πβ{π, π}))) |
60 | 22, 59 | mtbid 324 |
. . . . 5
β’ (π β Β¬ (πβ{π}) β (πβ{π, π})) |
61 | | nssne2 4010 |
. . . . 5
β’ (((πβ{(π + π)}) β (πβ{π, π}) β§ Β¬ (πβ{π}) β (πβ{π, π})) β (πβ{(π + π)}) β (πβ{π})) |
62 | 58, 60, 61 | syl2anc 585 |
. . . 4
β’ (π β (πβ{(π + π)}) β (πβ{π})) |
63 | 62 | necomd 3000 |
. . 3
β’ (π β (πβ{π}) β (πβ{(π + π)})) |
64 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 43, 54, 63 | mapdheq 40220 |
. 2
β’ (π β ((πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)) β ((πβ(πβ{(π + π)})) = (π½β{((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))}) β§ (πβ(πβ{(π β (π + π))})) = (π½β{(πΉπ
((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©)))})))) |
65 | 30, 35, 64 | mpbir2and 712 |
1
β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) |