Step | Hyp | Ref
| Expression |
1 | | hdmap1l6.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | hdmap1l6.m |
. . . 4
β’ π = ((mapdβπΎ)βπ) |
3 | | hdmap1l6.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
4 | | eqid 2733 |
. . . 4
β’
(LSubSpβπ) =
(LSubSpβπ) |
5 | | hdmap1l6.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
6 | 1, 3, 5 | dvhlmod 39619 |
. . . . 5
β’ (π β π β LMod) |
7 | | hdmap1l6e.y |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
8 | 7 | eldifad 3923 |
. . . . . 6
β’ (π β π β π) |
9 | | hdmap1l6.v |
. . . . . . 7
β’ π = (Baseβπ) |
10 | | hdmap1l6.n |
. . . . . . 7
β’ π = (LSpanβπ) |
11 | 9, 4, 10 | lspsncl 20453 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
12 | 6, 8, 11 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{π}) β (LSubSpβπ)) |
13 | | hdmap1l6e.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 | | hdmap1l6cl.x |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
21 | 20 | eldifad 3923 |
. . . . . . 7
β’ (π β π β π) |
22 | | hdmap1l6.p |
. . . . . . . . 9
β’ + =
(+gβπ) |
23 | 9, 22 | lmodvacl 20351 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
24 | 6, 8, 14, 23 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π + π) β π) |
25 | | hdmap1l6.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 | | hdmap1l6.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 | | hdmap1l6.fg |
. . . . . . . 8
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) |
39 | | hdmap1l6c.o |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
40 | | hdmap1l6.d |
. . . . . . . . 9
β’ π· = (BaseβπΆ) |
41 | | hdmap1l6.r |
. . . . . . . . 9
β’ π
= (-gβπΆ) |
42 | | hdmap1l6.l |
. . . . . . . . 9
β’ πΏ = (LSpanβπΆ) |
43 | | hdmap1l6.i |
. . . . . . . . 9
β’ πΌ = ((HDMap1βπΎ)βπ) |
44 | | hdmap1l6.f |
. . . . . . . . 9
β’ (π β πΉ β π·) |
45 | | hdmap1l6.mn |
. . . . . . . . . . 11
β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) |
46 | 1, 3, 5 | dvhlvec 39618 |
. . . . . . . . . . . . 13
β’ (π β π β LVec) |
47 | | hdmap1l6.yz |
. . . . . . . . . . . . 13
β’ (π β (πβ{π}) β (πβ{π})) |
48 | | hdmap1l6e.xn |
. . . . . . . . . . . . 13
β’ (π β Β¬ π β (πβ{π, π})) |
49 | 9, 39, 10, 46, 8, 13, 21, 47, 48 | lspindp2 20612 |
. . . . . . . . . . . 12
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
50 | 49 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (πβ{π})) |
51 | 1, 3, 9, 39, 10, 35, 40, 42, 2, 43, 5, 44, 45, 50, 20, 8 | hdmap1cl 40313 |
. . . . . . . . . 10
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
52 | 38, 51 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΊ β π·) |
53 | 1, 3, 9, 25, 39, 10, 35, 40, 41, 42, 2, 43, 5, 20, 44, 7, 52, 50, 45 | hdmap1eq 40310 |
. . . . . . . 8
β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β ((πβ(πβ{π})) = (πΏβ{πΊ}) β§ (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ
πΊ)})))) |
54 | 38, 53 | mpbid 231 |
. . . . . . 7
β’ (π β ((πβ(πβ{π})) = (πΏβ{πΊ}) β§ (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ
πΊ)}))) |
55 | 54 | simpld 496 |
. . . . . 6
β’ (π β (πβ(πβ{π})) = (πΏβ{πΊ})) |
56 | | hdmap1l6.fe |
. . . . . . . 8
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) |
57 | 9, 39, 10, 46, 7, 14, 21, 47, 48 | lspindp1 20610 |
. . . . . . . . . . . 12
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
58 | 57 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (πβ{π})) |
59 | 1, 3, 9, 39, 10, 35, 40, 42, 2, 43, 5, 44, 45, 58, 20, 14 | hdmap1cl 40313 |
. . . . . . . . . 10
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
60 | 56, 59 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΈ β π·) |
61 | 1, 3, 9, 25, 39, 10, 35, 40, 41, 42, 2, 43, 5, 20, 44, 13, 60, 58, 45 | hdmap1eq 40310 |
. . . . . . . 8
β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΈ β ((πβ(πβ{π})) = (πΏβ{πΈ}) β§ (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ
πΈ)})))) |
62 | 56, 61 | mpbid 231 |
. . . . . . 7
β’ (π β ((πβ(πβ{π})) = (πΏβ{πΈ}) β§ (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ
πΈ)}))) |
63 | 62 | simpld 496 |
. . . . . 6
β’ (π β (πβ(πβ{π})) = (πΏβ{πΈ})) |
64 | 55, 63 | oveq12d 7376 |
. . . . 5
β’ (π β ((πβ(πβ{π}))(LSSumβπΆ)(πβ(πβ{π}))) = ((πΏβ{πΊ})(LSSumβπΆ)(πΏβ{πΈ}))) |
65 | 37, 64 | eqtrd 2773 |
. . . 4
β’ (π β (πβ((πβ{π})(LSSumβπ)(πβ{π}))) = ((πΏβ{πΊ})(LSSumβπΆ)(πΏβ{πΈ}))) |
66 | 1, 2, 3, 4, 17, 35, 36, 5, 29, 31 | mapdlsm 40173 |
. . . . 5
β’ (π β (πβ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π}))) = ((πβ(πβ{(π β (π + π))}))(LSSumβπΆ)(πβ(πβ{π})))) |
67 | | hdmap1l6.a |
. . . . . . 7
β’ β =
(+gβπΆ) |
68 | | hdmap1l6.q |
. . . . . . 7
β’ π = (0gβπΆ) |
69 | 1, 3, 9, 22, 25, 39, 10, 35, 40, 67, 41, 68, 42, 2, 43, 5, 44, 20, 45, 7, 13, 48, 47, 38, 56 | hdmap1l6lem1 40316 |
. . . . . 6
β’ (π β (πβ(πβ{(π β (π + π))})) = (πΏβ{(πΉπ
(πΊ β πΈ))})) |
70 | 69, 45 | oveq12d 7376 |
. . . . 5
β’ (π β ((πβ(πβ{(π β (π + π))}))(LSSumβπΆ)(πβ(πβ{π}))) = ((πΏβ{(πΉπ
(πΊ β πΈ))})(LSSumβπΆ)(πΏβ{πΉ}))) |
71 | 66, 70 | eqtrd 2773 |
. . . 4
β’ (π β (πβ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π}))) = ((πΏβ{(πΉπ
(πΊ β πΈ))})(LSSumβπΆ)(πΏβ{πΉ}))) |
72 | 65, 71 | ineq12d 4174 |
. . 3
β’ (π β ((πβ((πβ{π})(LSSumβπ)(πβ{π}))) β© (πβ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π})))) = (((πΏβ{πΊ})(LSSumβπΆ)(πΏβ{πΈ})) β© ((πΏβ{(πΉπ
(πΊ β πΈ))})(LSSumβπΆ)(πΏβ{πΉ})))) |
73 | 34, 72 | eqtrd 2773 |
. 2
β’ (π β (πβ(((πβ{π})(LSSumβπ)(πβ{π})) β© ((πβ{(π β (π + π))})(LSSumβπ)(πβ{π})))) = (((πΏβ{πΊ})(LSSumβπΆ)(πΏβ{πΈ})) β© ((πΏβ{(πΉπ
(πΊ β πΈ))})(LSSumβπΆ)(πΏβ{πΉ})))) |
74 | 9, 25, 39, 17, 10, 46, 21, 48, 47, 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, 40, 42, 5, 44, 45, 21, 8, 52, 55, 14, 60, 63, 48 | mapdindp 40180 |
. . 3
β’ (π β Β¬ πΉ β (πΏβ{πΊ, πΈ})) |
78 | 1, 2, 3, 9, 10, 35, 40, 42, 5, 52, 55, 8, 14, 60, 63, 47 | mapdncol 40179 |
. . 3
β’ (π β (πΏβ{πΊ}) β (πΏβ{πΈ})) |
79 | 1, 2, 3, 9, 10, 35, 40, 42, 5, 52, 55, 39, 68, 7 | mapdn0 40178 |
. . 3
β’ (π β πΊ β (π· β {π})) |
80 | 1, 2, 3, 9, 10, 35, 40, 42, 5, 60, 63, 39, 68, 13 | mapdn0 40178 |
. . 3
β’ (π β πΈ β (π· β {π})) |
81 | 40, 41, 68, 36, 42, 76, 44, 77, 78, 79, 80, 67 | baerlem5b 40224 |
. 2
β’ (π β (πΏβ{(πΊ β πΈ)}) = (((πΏβ{πΊ})(LSSumβπΆ)(πΏβ{πΈ})) β© ((πΏβ{(πΉπ
(πΊ β πΈ))})(LSSumβπΆ)(πΏβ{πΉ})))) |
82 | 73, 75, 81 | 3eqtr4d 2783 |
1
β’ (π β (πβ(πβ{(π + π)})) = (πΏβ{(πΊ β πΈ)})) |