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 39623 |
. . . . 5
β’ (π β π β LMod) |
7 | | hdmap1l6cl.x |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
8 | 7 | eldifad 3926 |
. . . . . . 7
β’ (π β π β π) |
9 | | hdmap1l6e.y |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
10 | 9 | eldifad 3926 |
. . . . . . 7
β’ (π β π β π) |
11 | | hdmap1l6.v |
. . . . . . . 8
β’ π = (Baseβπ) |
12 | | hdmap1l6.s |
. . . . . . . 8
β’ β =
(-gβπ) |
13 | 11, 12 | lmodvsubcl 20411 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β (π β π) β π) |
14 | 6, 8, 10, 13 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β π) β π) |
15 | | hdmap1l6.n |
. . . . . . 7
β’ π = (LSpanβπ) |
16 | 11, 4, 15 | lspsncl 20482 |
. . . . . 6
β’ ((π β LMod β§ (π β π) β π) β (πβ{(π β π)}) β (LSubSpβπ)) |
17 | 6, 14, 16 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{(π β π)}) β (LSubSpβπ)) |
18 | | hdmap1l6e.z |
. . . . . . 7
β’ (π β π β (π β { 0 })) |
19 | 18 | eldifad 3926 |
. . . . . 6
β’ (π β π β π) |
20 | 11, 4, 15 | lspsncl 20482 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
21 | 6, 19, 20 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{π}) β (LSubSpβπ)) |
22 | | eqid 2733 |
. . . . . 6
β’
(LSSumβπ) =
(LSSumβπ) |
23 | 4, 22 | lsmcl 20588 |
. . . . 5
β’ ((π β LMod β§ (πβ{(π β π)}) β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β ((πβ{(π β π)})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
24 | 6, 17, 21, 23 | syl3anc 1372 |
. . . 4
β’ (π β ((πβ{(π β π)})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
25 | 11, 12 | lmodvsubcl 20411 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β (π β π) β π) |
26 | 6, 8, 19, 25 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β π) β π) |
27 | 11, 4, 15 | lspsncl 20482 |
. . . . . 6
β’ ((π β LMod β§ (π β π) β π) β (πβ{(π β π)}) β (LSubSpβπ)) |
28 | 6, 26, 27 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{(π β π)}) β (LSubSpβπ)) |
29 | 11, 4, 15 | lspsncl 20482 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
30 | 6, 10, 29 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{π}) β (LSubSpβπ)) |
31 | 4, 22 | lsmcl 20588 |
. . . . 5
β’ ((π β LMod β§ (πβ{(π β π)}) β (LSubSpβπ) β§ (πβ{π}) β (LSubSpβπ)) β ((πβ{(π β π)})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
32 | 6, 28, 30, 31 | syl3anc 1372 |
. . . 4
β’ (π β ((πβ{(π β π)})(LSSumβπ)(πβ{π})) β (LSubSpβπ)) |
33 | 1, 2, 3, 4, 5, 24,
32 | mapdin 40175 |
. . 3
β’ (π β (πβ(((πβ{(π β π)})(LSSumβπ)(πβ{π})) β© ((πβ{(π β π)})(LSSumβπ)(πβ{π})))) = ((πβ((πβ{(π β π)})(LSSumβπ)(πβ{π}))) β© (πβ((πβ{(π β π)})(LSSumβπ)(πβ{π}))))) |
34 | | hdmap1l6.c |
. . . . . 6
β’ πΆ = ((LCDualβπΎ)βπ) |
35 | | eqid 2733 |
. . . . . 6
β’
(LSSumβπΆ) =
(LSSumβπΆ) |
36 | 1, 2, 3, 4, 22, 34, 35, 5, 17, 21 | mapdlsm 40177 |
. . . . 5
β’ (π β (πβ((πβ{(π β π)})(LSSumβπ)(πβ{π}))) = ((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π})))) |
37 | 1, 2, 3, 4, 22, 34, 35, 5, 28, 30 | mapdlsm 40177 |
. . . . 5
β’ (π β (πβ((πβ{(π β π)})(LSSumβπ)(πβ{π}))) = ((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π})))) |
38 | 36, 37 | ineq12d 4177 |
. . . 4
β’ (π β ((πβ((πβ{(π β π)})(LSSumβπ)(πβ{π}))) β© (πβ((πβ{(π β π)})(LSSumβπ)(πβ{π})))) = (((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π}))) β© ((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π}))))) |
39 | | hdmap1l6.fg |
. . . . . . . 8
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) |
40 | | hdmap1l6c.o |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
41 | | hdmap1l6.d |
. . . . . . . . 9
β’ π· = (BaseβπΆ) |
42 | | hdmap1l6.r |
. . . . . . . . 9
β’ π
= (-gβπΆ) |
43 | | hdmap1l6.l |
. . . . . . . . 9
β’ πΏ = (LSpanβπΆ) |
44 | | hdmap1l6.i |
. . . . . . . . 9
β’ πΌ = ((HDMap1βπΎ)βπ) |
45 | | hdmap1l6.f |
. . . . . . . . 9
β’ (π β πΉ β π·) |
46 | | hdmap1l6.mn |
. . . . . . . . . . 11
β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) |
47 | 1, 3, 5 | dvhlvec 39622 |
. . . . . . . . . . . . 13
β’ (π β π β LVec) |
48 | | hdmap1l6.yz |
. . . . . . . . . . . . 13
β’ (π β (πβ{π}) β (πβ{π})) |
49 | | hdmap1l6e.xn |
. . . . . . . . . . . . 13
β’ (π β Β¬ π β (πβ{π, π})) |
50 | 11, 40, 15, 47, 10, 18, 8, 48, 49 | lspindp2 20641 |
. . . . . . . . . . . 12
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
51 | 50 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (πβ{π})) |
52 | 1, 3, 11, 40, 15, 34, 41, 43, 2, 44, 5, 45, 46, 51, 7, 10 | hdmap1cl 40317 |
. . . . . . . . . 10
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
53 | 39, 52 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΊ β π·) |
54 | 1, 3, 11, 12, 40, 15, 34, 41, 42, 43, 2, 44, 5, 7, 45, 9, 53, 51, 46 | hdmap1eq 40314 |
. . . . . . . 8
β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β ((πβ(πβ{π})) = (πΏβ{πΊ}) β§ (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ
πΊ)})))) |
55 | 39, 54 | mpbid 231 |
. . . . . . 7
β’ (π β ((πβ(πβ{π})) = (πΏβ{πΊ}) β§ (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ
πΊ)}))) |
56 | 55 | simprd 497 |
. . . . . 6
β’ (π β (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ
πΊ)})) |
57 | | hdmap1l6.fe |
. . . . . . . 8
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) |
58 | 11, 40, 15, 47, 9, 19, 8, 48, 49 | lspindp1 20639 |
. . . . . . . . . . . 12
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
59 | 58 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (πβ{π})) |
60 | 1, 3, 11, 40, 15, 34, 41, 43, 2, 44, 5, 45, 46, 59, 7, 19 | hdmap1cl 40317 |
. . . . . . . . . 10
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
61 | 57, 60 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΈ β π·) |
62 | 1, 3, 11, 12, 40, 15, 34, 41, 42, 43, 2, 44, 5, 7, 45, 18, 61, 59, 46 | hdmap1eq 40314 |
. . . . . . . 8
β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΈ β ((πβ(πβ{π})) = (πΏβ{πΈ}) β§ (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ
πΈ)})))) |
63 | 57, 62 | mpbid 231 |
. . . . . . 7
β’ (π β ((πβ(πβ{π})) = (πΏβ{πΈ}) β§ (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ
πΈ)}))) |
64 | 63 | simpld 496 |
. . . . . 6
β’ (π β (πβ(πβ{π})) = (πΏβ{πΈ})) |
65 | 56, 64 | oveq12d 7379 |
. . . . 5
β’ (π β ((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π}))) = ((πΏβ{(πΉπ
πΊ)})(LSSumβπΆ)(πΏβ{πΈ}))) |
66 | 63 | simprd 497 |
. . . . . 6
β’ (π β (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ
πΈ)})) |
67 | 55 | simpld 496 |
. . . . . 6
β’ (π β (πβ(πβ{π})) = (πΏβ{πΊ})) |
68 | 66, 67 | oveq12d 7379 |
. . . . 5
β’ (π β ((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π}))) = ((πΏβ{(πΉπ
πΈ)})(LSSumβπΆ)(πΏβ{πΊ}))) |
69 | 65, 68 | ineq12d 4177 |
. . . 4
β’ (π β (((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π}))) β© ((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π})))) = (((πΏβ{(πΉπ
πΊ)})(LSSumβπΆ)(πΏβ{πΈ})) β© ((πΏβ{(πΉπ
πΈ)})(LSSumβπΆ)(πΏβ{πΊ})))) |
70 | 38, 69 | eqtrd 2773 |
. . 3
β’ (π β ((πβ((πβ{(π β π)})(LSSumβπ)(πβ{π}))) β© (πβ((πβ{(π β π)})(LSSumβπ)(πβ{π})))) = (((πΏβ{(πΉπ
πΊ)})(LSSumβπΆ)(πΏβ{πΈ})) β© ((πΏβ{(πΉπ
πΈ)})(LSSumβπΆ)(πΏβ{πΊ})))) |
71 | 33, 70 | eqtrd 2773 |
. 2
β’ (π β (πβ(((πβ{(π β π)})(LSSumβπ)(πβ{π})) β© ((πβ{(π β π)})(LSSumβπ)(πβ{π})))) = (((πΏβ{(πΉπ
πΊ)})(LSSumβπΆ)(πΏβ{πΈ})) β© ((πΏβ{(πΉπ
πΈ)})(LSSumβπΆ)(πΏβ{πΊ})))) |
72 | | hdmap1l6.p |
. . . 4
β’ + =
(+gβπ) |
73 | 11, 12, 40, 22, 15, 47, 8, 49, 48, 9, 18, 72 | baerlem5a 40227 |
. . 3
β’ (π β (πβ{(π β (π + π))}) = (((πβ{(π β π)})(LSSumβπ)(πβ{π})) β© ((πβ{(π β π)})(LSSumβπ)(πβ{π})))) |
74 | 73 | fveq2d 6850 |
. 2
β’ (π β (πβ(πβ{(π β (π + π))})) = (πβ(((πβ{(π β π)})(LSSumβπ)(πβ{π})) β© ((πβ{(π β π)})(LSSumβπ)(πβ{π}))))) |
75 | | hdmap1l6.q |
. . 3
β’ π = (0gβπΆ) |
76 | 1, 34, 5 | lcdlvec 40104 |
. . 3
β’ (π β πΆ β LVec) |
77 | 1, 2, 3, 11, 15, 34, 41, 43, 5, 45, 46, 8, 10, 53, 67, 19, 61, 64, 49 | mapdindp 40184 |
. . 3
β’ (π β Β¬ πΉ β (πΏβ{πΊ, πΈ})) |
78 | 1, 2, 3, 11, 15, 34, 41, 43, 5, 53, 67, 10, 19, 61, 64, 48 | mapdncol 40183 |
. . 3
β’ (π β (πΏβ{πΊ}) β (πΏβ{πΈ})) |
79 | 1, 2, 3, 11, 15, 34, 41, 43, 5, 53, 67, 40, 75, 9 | mapdn0 40182 |
. . 3
β’ (π β πΊ β (π· β {π})) |
80 | 1, 2, 3, 11, 15, 34, 41, 43, 5, 61, 64, 40, 75, 18 | mapdn0 40182 |
. . 3
β’ (π β πΈ β (π· β {π})) |
81 | | hdmap1l6.a |
. . 3
β’ β =
(+gβπΆ) |
82 | 41, 42, 75, 35, 43, 76, 45, 77, 78, 79, 80, 81 | baerlem5a 40227 |
. 2
β’ (π β (πΏβ{(πΉπ
(πΊ β πΈ))}) = (((πΏβ{(πΉπ
πΊ)})(LSSumβπΆ)(πΏβ{πΈ})) β© ((πΏβ{(πΉπ
πΈ)})(LSSumβπΆ)(πΏβ{πΊ})))) |
83 | 71, 74, 82 | 3eqtr4d 2783 |
1
β’ (π β (πβ(πβ{(π β (π + π))})) = (πΏβ{(πΉπ
(πΊ β πΈ))})) |