Step | Hyp | Ref
| Expression |
1 | | mapdh.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | mapdh.m |
. . . 4
β’ π = ((mapdβπΎ)βπ) |
3 | | mapdh.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
4 | | eqid 2733 |
. . . 4
β’
(LSubSpβπ) =
(LSubSpβπ) |
5 | | mapdh.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
6 | 1, 3, 5 | dvhlmod 39623 |
. . . . 5
β’ (π β π β LMod) |
7 | | mapdhe4.y |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
8 | 7 | eldifad 3926 |
. . . . . 6
β’ (π β π β π) |
9 | | mapdh.v |
. . . . . . 7
β’ π = (Baseβπ) |
10 | | mapdh.n |
. . . . . . 7
β’ π = (LSpanβπ) |
11 | 9, 4, 10 | lspsncl 20482 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
12 | 6, 8, 11 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{π}) β (LSubSpβπ)) |
13 | | mapdhe.z |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
14 | 13 | eldifad 3926 |
. . . . . 6
β’ (π β π β π) |
15 | 9, 4, 10 | lspsncl 20482 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
16 | 6, 14, 15 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{π}) β (LSubSpβπ)) |
17 | | eqid 2733 |
. . . . . 6
β’
(LSSumβπ) =
(LSSumβπ) |
18 | 4, 17 | lsmcl 20588 |
. . . . 5
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
19 | 6, 12, 16, 18 | syl3anc 1372 |
. . . 4
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
20 | | mapdhcl.x |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
21 | 20 | eldifad 3926 |
. . . . . . 7
β’ (π β π β π) |
22 | | mapdh.s |
. . . . . . . 8
β’ β =
(-gβπ) |
23 | 9, 22 | lmodvsubcl 20411 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β (π β π) β π) |
24 | 6, 21, 8, 23 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β π) β π) |
25 | 9, 4, 10 | lspsncl 20482 |
. . . . . 6
β’ ((π β LMod β§ (π β π) β π) β (πβ{(π β π)}) β (LSubSpβπ)) |
26 | 6, 24, 25 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{(π β π)}) β (LSubSpβπ)) |
27 | 9, 22 | lmodvsubcl 20411 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β (π β π) β π) |
28 | 6, 21, 14, 27 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β π) β π) |
29 | 9, 4, 10 | lspsncl 20482 |
. . . . . 6
β’ ((π β LMod β§ (π β π) β π) β (πβ{(π β π)}) β (LSubSpβπ)) |
30 | 6, 28, 29 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{(π β π)}) β (LSubSpβπ)) |
31 | 4, 17 | lsmcl 20588 |
. . . . 5
β’ ((π β LMod β§ (πβ{(π β π)}) β (LSubSpβπ) β§ (πβ{(π β π)}) β (LSubSpβπ)) β ((πβ{(π β π)})(LSSumβπ)(πβ{(π β π)})) β (LSubSpβπ)) |
32 | 6, 26, 30, 31 | syl3anc 1372 |
. . . 4
β’ (π β ((πβ{(π β π)})(LSSumβπ)(πβ{(π β π)})) β (LSubSpβπ)) |
33 | 1, 2, 3, 4, 5, 19,
32 | mapdin 40175 |
. . 3
β’ (π β (πβ(((πβ{π})(LSSumβπ)(πβ{π})) β© ((πβ{(π β π)})(LSSumβπ)(πβ{(π β π)})))) = ((πβ((πβ{π})(LSSumβπ)(πβ{π}))) β© (πβ((πβ{(π β π)})(LSSumβπ)(πβ{(π β π)}))))) |
34 | | mapdh.c |
. . . . . 6
β’ πΆ = ((LCDualβπΎ)βπ) |
35 | | eqid 2733 |
. . . . . 6
β’
(LSSumβπΆ) =
(LSSumβπΆ) |
36 | 1, 2, 3, 4, 17, 34, 35, 5, 12, 16 | mapdlsm 40177 |
. . . . 5
β’ (π β (πβ((πβ{π})(LSSumβπ)(πβ{π}))) = ((πβ(πβ{π}))(LSSumβπΆ)(πβ(πβ{π})))) |
37 | | mapdh.eg |
. . . . . . . 8
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) |
38 | | mapdh.q |
. . . . . . . . 9
β’ π = (0gβπΆ) |
39 | | mapdh.i |
. . . . . . . . 9
β’ πΌ = (π₯ β V β¦ if((2nd
βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))))) |
40 | | mapdhc.o |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
41 | | mapdh.d |
. . . . . . . . 9
β’ π· = (BaseβπΆ) |
42 | | mapdh.r |
. . . . . . . . 9
β’ π
= (-gβπΆ) |
43 | | mapdh.j |
. . . . . . . . 9
β’ π½ = (LSpanβπΆ) |
44 | | mapdhc.f |
. . . . . . . . 9
β’ (π β πΉ β π·) |
45 | | mapdh.mn |
. . . . . . . . 9
β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) |
46 | 1, 3, 5 | dvhlvec 39622 |
. . . . . . . . . . . . 13
β’ (π β π β LVec) |
47 | | mapdh.yz |
. . . . . . . . . . . . 13
β’ (π β (πβ{π}) β (πβ{π})) |
48 | | mapdh.xn |
. . . . . . . . . . . . 13
β’ (π β Β¬ π β (πβ{π, π})) |
49 | 9, 40, 10, 46, 8, 13, 21, 47, 48 | lspindp2 20641 |
. . . . . . . . . . . 12
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
50 | 49 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (πβ{π})) |
51 | 38, 39, 1, 2, 3, 9, 22, 40, 10, 34, 41, 42, 43, 5, 44, 45, 20, 8, 50 | mapdhcl 40240 |
. . . . . . . . . 10
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
52 | 37, 51 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΊ β π·) |
53 | 38, 39, 1, 2, 3, 9, 22, 40, 10, 34, 41, 42, 43, 5, 44, 45, 20, 7, 52, 50 | mapdheq 40241 |
. . . . . . . 8
β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β ((πβ(πβ{π})) = (π½β{πΊ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΊ)})))) |
54 | 37, 53 | mpbid 231 |
. . . . . . 7
β’ (π β ((πβ(πβ{π})) = (π½β{πΊ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΊ)}))) |
55 | 54 | simpld 496 |
. . . . . 6
β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) |
56 | | mapdh.ee |
. . . . . . . 8
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) |
57 | 9, 40, 10, 46, 7, 14, 21, 47, 48 | lspindp1 20639 |
. . . . . . . . . . . 12
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
58 | 57 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (πβ{π})) |
59 | 38, 39, 1, 2, 3, 9, 22, 40, 10, 34, 41, 42, 43, 5, 44, 45, 20, 14, 58 | mapdhcl 40240 |
. . . . . . . . . 10
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
60 | 56, 59 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΈ β π·) |
61 | 38, 39, 1, 2, 3, 9, 22, 40, 10, 34, 41, 42, 43, 5, 44, 45, 20, 13, 60, 58 | mapdheq 40241 |
. . . . . . . 8
β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΈ β ((πβ(πβ{π})) = (π½β{πΈ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΈ)})))) |
62 | 56, 61 | mpbid 231 |
. . . . . . 7
β’ (π β ((πβ(πβ{π})) = (π½β{πΈ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΈ)}))) |
63 | 62 | simpld 496 |
. . . . . 6
β’ (π β (πβ(πβ{π})) = (π½β{πΈ})) |
64 | 55, 63 | oveq12d 7379 |
. . . . 5
β’ (π β ((πβ(πβ{π}))(LSSumβπΆ)(πβ(πβ{π}))) = ((π½β{πΊ})(LSSumβπΆ)(π½β{πΈ}))) |
65 | 36, 64 | eqtrd 2773 |
. . . 4
β’ (π β (πβ((πβ{π})(LSSumβπ)(πβ{π}))) = ((π½β{πΊ})(LSSumβπΆ)(π½β{πΈ}))) |
66 | 1, 2, 3, 4, 17, 34, 35, 5, 26, 30 | mapdlsm 40177 |
. . . . 5
β’ (π β (πβ((πβ{(π β π)})(LSSumβπ)(πβ{(π β π)}))) = ((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{(π β π)})))) |
67 | 54 | simprd 497 |
. . . . . 6
β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΊ)})) |
68 | 62 | simprd 497 |
. . . . . 6
β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΈ)})) |
69 | 67, 68 | oveq12d 7379 |
. . . . 5
β’ (π β ((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{(π β π)}))) = ((π½β{(πΉπ
πΊ)})(LSSumβπΆ)(π½β{(πΉπ
πΈ)}))) |
70 | 66, 69 | eqtrd 2773 |
. . . 4
β’ (π β (πβ((πβ{(π β π)})(LSSumβπ)(πβ{(π β π)}))) = ((π½β{(πΉπ
πΊ)})(LSSumβπΆ)(π½β{(πΉπ
πΈ)}))) |
71 | 65, 70 | ineq12d 4177 |
. . 3
β’ (π β ((πβ((πβ{π})(LSSumβπ)(πβ{π}))) β© (πβ((πβ{(π β π)})(LSSumβπ)(πβ{(π β π)})))) = (((π½β{πΊ})(LSSumβπΆ)(π½β{πΈ})) β© ((π½β{(πΉπ
πΊ)})(LSSumβπΆ)(π½β{(πΉπ
πΈ)})))) |
72 | 33, 71 | eqtrd 2773 |
. 2
β’ (π β (πβ(((πβ{π})(LSSumβπ)(πβ{π})) β© ((πβ{(π β π)})(LSSumβπ)(πβ{(π β π)})))) = (((π½β{πΊ})(LSSumβπΆ)(π½β{πΈ})) β© ((π½β{(πΉπ
πΊ)})(LSSumβπΆ)(π½β{(πΉπ
πΈ)})))) |
73 | 9, 22, 40, 17, 10, 46, 21, 48, 47, 7, 13 | baerlem3 40226 |
. . 3
β’ (π β (πβ{(π β π)}) = (((πβ{π})(LSSumβπ)(πβ{π})) β© ((πβ{(π β π)})(LSSumβπ)(πβ{(π β π)})))) |
74 | 73 | fveq2d 6850 |
. 2
β’ (π β (πβ(πβ{(π β π)})) = (πβ(((πβ{π})(LSSumβπ)(πβ{π})) β© ((πβ{(π β π)})(LSSumβπ)(πβ{(π β π)}))))) |
75 | | eqid 2733 |
. . 3
β’
(0gβπΆ) = (0gβπΆ) |
76 | 1, 34, 5 | lcdlvec 40104 |
. . 3
β’ (π β πΆ β LVec) |
77 | 1, 2, 3, 9, 10, 34, 41, 43, 5, 44, 45, 21, 8, 52, 55, 14, 60, 63, 48 | mapdindp 40184 |
. . 3
β’ (π β Β¬ πΉ β (π½β{πΊ, πΈ})) |
78 | 1, 2, 3, 9, 10, 34, 41, 43, 5, 52, 55, 8, 14, 60, 63, 47 | mapdncol 40183 |
. . 3
β’ (π β (π½β{πΊ}) β (π½β{πΈ})) |
79 | 1, 2, 3, 9, 10, 34, 41, 43, 5, 52, 55, 40, 75, 7 | mapdn0 40182 |
. . 3
β’ (π β πΊ β (π· β {(0gβπΆ)})) |
80 | 1, 2, 3, 9, 10, 34, 41, 43, 5, 60, 63, 40, 75, 13 | mapdn0 40182 |
. . 3
β’ (π β πΈ β (π· β {(0gβπΆ)})) |
81 | 41, 42, 75, 35, 43, 76, 44, 77, 78, 79, 80 | baerlem3 40226 |
. 2
β’ (π β (π½β{(πΊπ
πΈ)}) = (((π½β{πΊ})(LSSumβπΆ)(π½β{πΈ})) β© ((π½β{(πΉπ
πΊ)})(LSSumβπΆ)(π½β{(πΉπ
πΈ)})))) |
82 | 72, 74, 81 | 3eqtr4d 2783 |
1
β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΊπ
πΈ)})) |