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 39619 |
. . . . 5
β’ (π β π β LMod) |
7 | | mapdhe6.y |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
8 | 7 | eldifad 3923 |
. . . . . 6
β’ (π β π β π) |
9 | | mapdh.v |
. . . . . . 7
β’ π = (Baseβπ) |
10 | | mapdh.n |
. . . . . . 7
β’ π = (LSpanβπ) |
11 | 9, 4, 10 | lspsncl 20453 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
12 | 6, 8, 11 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{π}) β (LSubSpβπ)) |
13 | | mapdhe6.z |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
14 | 13 | eldifad 3923 |
. . . . . 6
β’ (π β π β π) |
15 | 9, 4, 10 | lspsncl 20453 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
16 | 6, 14, 15 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{π}) β (LSubSpβπ)) |
17 | | eqid 2733 |
. . . . . 6
β’
(LSSumβπ) =
(LSSumβπ) |
18 | 4, 17 | lsmcl 20559 |
. . . . 5
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
19 | 6, 12, 16, 18 | syl3anc 1372 |
. . . 4
β’ (π β ((πβ{π})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
20 | | mapdhcl.x |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
21 | 20 | eldifad 3923 |
. . . . . . 7
β’ (π β π β π) |
22 | | mapdh.p |
. . . . . . . . 9
β’ + =
(+gβπ) |
23 | 9, 22 | lmodvacl 20351 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
24 | 6, 8, 14, 23 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π + π) β π) |
25 | | mapdh.s |
. . . . . . . 8
β’ β =
(-gβπ) |
26 | 9, 25 | lmodvsubcl 20382 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ (π + π) β π) β (π β (π + π)) β π) |
27 | 6, 21, 24, 26 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β (π + π)) β π) |
28 | 9, 4, 10 | lspsncl 20453 |
. . . . . 6
β’ ((π β LMod β§ (π β (π + π)) β π) β (πβ{(π β (π + π))}) β (LSubSpβπ)) |
29 | 6, 27, 28 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{(π β (π + π))}) β (LSubSpβπ)) |
30 | 9, 4, 10 | lspsncl 20453 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
31 | 6, 21, 30 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{π}) β (LSubSpβπ)) |
32 | 4, 17 | lsmcl 20559 |
. . . . 5
β’ ((π β LMod β§ (πβ{(π β (π + π))}) β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
33 | 6, 29, 31, 32 | syl3anc 1372 |
. . . 4
β’ (π β ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
34 | 1, 2, 3, 4, 5, 19,
33 | mapdin 40171 |
. . 3
β’ (π β (πβ(((πβ{π})(LSSumβπ)(πβ{π})) β© ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π})))) = ((πβ((πβ{π})(LSSumβπ)(πβ{π}))) β© (πβ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π}))))) |
35 | | mapdh.c |
. . . . . 6
β’ πΆ = ((LCDualβπΎ)βπ) |
36 | | eqid 2733 |
. . . . . 6
β’
(LSSumβπΆ) =
(LSSumβπΆ) |
37 | 1, 2, 3, 4, 17, 35, 36, 5, 12, 16 | mapdlsm 40173 |
. . . . 5
β’ (π β (πβ((πβ{π})(LSSumβπ)(πβ{π}))) = ((πβ(πβ{π}))(LSSumβπΆ)(πβ(πβ{π})))) |
38 | | mapdh6.fg |
. . . . . . . 8
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) |
39 | | mapdh.q |
. . . . . . . . 9
β’ π = (0gβπΆ) |
40 | | mapdh.i |
. . . . . . . . 9
β’ πΌ = (π₯ β V β¦ if((2nd
βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))))) |
41 | | mapdhc.o |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
42 | | mapdh.d |
. . . . . . . . 9
β’ π· = (BaseβπΆ) |
43 | | mapdh.r |
. . . . . . . . 9
β’ π
= (-gβπΆ) |
44 | | mapdh.j |
. . . . . . . . 9
β’ π½ = (LSpanβπΆ) |
45 | | mapdhc.f |
. . . . . . . . 9
β’ (π β πΉ β π·) |
46 | | mapdh.mn |
. . . . . . . . 9
β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) |
47 | 1, 3, 5 | dvhlvec 39618 |
. . . . . . . . . . . . 13
β’ (π β π β LVec) |
48 | | mapdh6.yz |
. . . . . . . . . . . . 13
β’ (π β (πβ{π}) β (πβ{π})) |
49 | | mapdhe6.xn |
. . . . . . . . . . . . 13
β’ (π β Β¬ π β (πβ{π, π})) |
50 | 9, 41, 10, 47, 8, 13, 21, 48, 49 | lspindp2 20612 |
. . . . . . . . . . . 12
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
51 | 50 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (πβ{π})) |
52 | 39, 40, 1, 2, 3, 9, 25, 41, 10, 35, 42, 43, 44, 5, 45, 46, 20, 8, 51 | mapdhcl 40236 |
. . . . . . . . . 10
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
53 | 38, 52 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΊ β π·) |
54 | 39, 40, 1, 2, 3, 9, 25, 41, 10, 35, 42, 43, 44, 5, 45, 46, 20, 7, 53, 51 | mapdheq 40237 |
. . . . . . . 8
β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β ((πβ(πβ{π})) = (π½β{πΊ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΊ)})))) |
55 | 38, 54 | mpbid 231 |
. . . . . . 7
β’ (π β ((πβ(πβ{π})) = (π½β{πΊ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΊ)}))) |
56 | 55 | simpld 496 |
. . . . . 6
β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) |
57 | | mapdh6.fe |
. . . . . . . 8
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) |
58 | 9, 41, 10, 47, 7, 14, 21, 48, 49 | lspindp1 20610 |
. . . . . . . . . . . 12
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
59 | 58 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (πβ{π})) |
60 | 39, 40, 1, 2, 3, 9, 25, 41, 10, 35, 42, 43, 44, 5, 45, 46, 20, 14, 59 | mapdhcl 40236 |
. . . . . . . . . 10
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
61 | 57, 60 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΈ β π·) |
62 | 39, 40, 1, 2, 3, 9, 25, 41, 10, 35, 42, 43, 44, 5, 45, 46, 20, 13, 61, 59 | mapdheq 40237 |
. . . . . . . 8
β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΈ β ((πβ(πβ{π})) = (π½β{πΈ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΈ)})))) |
63 | 57, 62 | mpbid 231 |
. . . . . . 7
β’ (π β ((πβ(πβ{π})) = (π½β{πΈ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΈ)}))) |
64 | 63 | simpld 496 |
. . . . . 6
β’ (π β (πβ(πβ{π})) = (π½β{πΈ})) |
65 | 56, 64 | oveq12d 7376 |
. . . . 5
β’ (π β ((πβ(πβ{π}))(LSSumβπΆ)(πβ(πβ{π}))) = ((π½β{πΊ})(LSSumβπΆ)(π½β{πΈ}))) |
66 | 37, 65 | eqtrd 2773 |
. . . 4
β’ (π β (πβ((πβ{π})(LSSumβπ)(πβ{π}))) = ((π½β{πΊ})(LSSumβπΆ)(π½β{πΈ}))) |
67 | 1, 2, 3, 4, 17, 35, 36, 5, 29, 31 | mapdlsm 40173 |
. . . . 5
β’ (π β (πβ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π}))) = ((πβ(πβ{(π β (π + π))}))(LSSumβπΆ)(πβ(πβ{π})))) |
68 | | mapdh.a |
. . . . . . 7
β’ β =
(+gβπΆ) |
69 | 39, 40, 1, 2, 3, 9, 25, 41, 10, 35, 42, 43, 44, 5, 45, 46, 20, 22, 68, 7, 13, 49, 48, 38, 57 | mapdh6lem1N 40242 |
. . . . . 6
β’ (π β (πβ(πβ{(π β (π + π))})) = (π½β{(πΉπ
(πΊ β πΈ))})) |
70 | 69, 46 | oveq12d 7376 |
. . . . 5
β’ (π β ((πβ(πβ{(π β (π + π))}))(LSSumβπΆ)(πβ(πβ{π}))) = ((π½β{(πΉπ
(πΊ β πΈ))})(LSSumβπΆ)(π½β{πΉ}))) |
71 | 67, 70 | eqtrd 2773 |
. . . 4
β’ (π β (πβ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π}))) = ((π½β{(πΉπ
(πΊ β πΈ))})(LSSumβπΆ)(π½β{πΉ}))) |
72 | 66, 71 | ineq12d 4174 |
. . 3
β’ (π β ((πβ((πβ{π})(LSSumβπ)(πβ{π}))) β© (πβ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π})))) = (((π½β{πΊ})(LSSumβπΆ)(π½β{πΈ})) β© ((π½β{(πΉπ
(πΊ β πΈ))})(LSSumβπΆ)(π½β{πΉ})))) |
73 | 34, 72 | eqtrd 2773 |
. 2
β’ (π β (πβ(((πβ{π})(LSSumβπ)(πβ{π})) β© ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π})))) = (((π½β{πΊ})(LSSumβπΆ)(π½β{πΈ})) β© ((π½β{(πΉπ
(πΊ β πΈ))})(LSSumβπΆ)(π½β{πΉ})))) |
74 | 9, 25, 41, 17, 10, 47, 21, 49, 48, 7, 13, 22 | baerlem5b 40224 |
. . 3
β’ (π β (πβ{(π + π)}) = (((πβ{π})(LSSumβπ)(πβ{π})) β© ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π})))) |
75 | 74 | fveq2d 6847 |
. 2
β’ (π β (πβ(πβ{(π + π)})) = (πβ(((πβ{π})(LSSumβπ)(πβ{π})) β© ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π}))))) |
76 | 1, 35, 5 | lcdlvec 40100 |
. . 3
β’ (π β πΆ β LVec) |
77 | 1, 2, 3, 9, 10, 35, 42, 44, 5, 45, 46, 21, 8, 53, 56, 14, 61, 64, 49 | mapdindp 40180 |
. . 3
β’ (π β Β¬ πΉ β (π½β{πΊ, πΈ})) |
78 | 1, 2, 3, 9, 10, 35, 42, 44, 5, 53, 56, 8, 14, 61, 64, 48 | mapdncol 40179 |
. . 3
β’ (π β (π½β{πΊ}) β (π½β{πΈ})) |
79 | 1, 2, 3, 9, 10, 35, 42, 44, 5, 53, 56, 41, 39, 7 | mapdn0 40178 |
. . 3
β’ (π β πΊ β (π· β {π})) |
80 | 1, 2, 3, 9, 10, 35, 42, 44, 5, 61, 64, 41, 39, 13 | mapdn0 40178 |
. . 3
β’ (π β πΈ β (π· β {π})) |
81 | 42, 43, 39, 36, 44, 76, 45, 77, 78, 79, 80, 68 | baerlem5b 40224 |
. 2
β’ (π β (π½β{(πΊ β πΈ)}) = (((π½β{πΊ})(LSSumβπΆ)(π½β{πΈ})) β© ((π½β{(πΉπ
(πΊ β πΈ))})(LSSumβπΆ)(π½β{πΉ})))) |
82 | 73, 75, 81 | 3eqtr4d 2783 |
1
β’ (π β (πβ(πβ{(π + π)})) = (π½β{(πΊ β πΈ)})) |