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 | | mapdhcl.x |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
8 | 7 | eldifad 3926 |
. . . . . . 7
β’ (π β π β π) |
9 | | mapdhe6.y |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
10 | 9 | eldifad 3926 |
. . . . . . 7
β’ (π β π β π) |
11 | | mapdh.v |
. . . . . . . 8
β’ π = (Baseβπ) |
12 | | mapdh.s |
. . . . . . . 8
β’ β =
(-gβπ) |
13 | 11, 12 | lmodvsubcl 20411 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β (π β π) β π) |
14 | 6, 8, 10, 13 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β π) β π) |
15 | | mapdh.n |
. . . . . . 7
β’ π = (LSpanβπ) |
16 | 11, 4, 15 | lspsncl 20482 |
. . . . . 6
β’ ((π β LMod β§ (π β π) β π) β (πβ{(π β π)}) β (LSubSpβπ)) |
17 | 6, 14, 16 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{(π β π)}) β (LSubSpβπ)) |
18 | | mapdhe6.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 | | mapdh.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 | | mapdh6.fg |
. . . . . . . 8
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) |
40 | | mapdh.q |
. . . . . . . . 9
β’ π = (0gβπΆ) |
41 | | mapdh.i |
. . . . . . . . 9
β’ πΌ = (π₯ β V β¦ if((2nd
βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st
β(1st βπ₯)) β (2nd
βπ₯))})) = (π½β{((2nd
β(1st βπ₯))π
β)}))))) |
42 | | mapdhc.o |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
43 | | mapdh.d |
. . . . . . . . 9
β’ π· = (BaseβπΆ) |
44 | | mapdh.r |
. . . . . . . . 9
β’ π
= (-gβπΆ) |
45 | | mapdh.j |
. . . . . . . . 9
β’ π½ = (LSpanβπΆ) |
46 | | mapdhc.f |
. . . . . . . . 9
β’ (π β πΉ β π·) |
47 | | mapdh.mn |
. . . . . . . . 9
β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) |
48 | 1, 3, 5 | dvhlvec 39622 |
. . . . . . . . . . . . 13
β’ (π β π β LVec) |
49 | | mapdh6.yz |
. . . . . . . . . . . . 13
β’ (π β (πβ{π}) β (πβ{π})) |
50 | | mapdhe6.xn |
. . . . . . . . . . . . 13
β’ (π β Β¬ π β (πβ{π, π})) |
51 | 11, 42, 15, 48, 10, 18, 8, 49, 50 | lspindp2 20641 |
. . . . . . . . . . . 12
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
52 | 51 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (πβ{π})) |
53 | 40, 41, 1, 2, 3, 11,
12, 42, 15, 34, 43, 44, 45, 5, 46, 47, 7, 10, 52 | mapdhcl 40240 |
. . . . . . . . . 10
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
54 | 39, 53 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΊ β π·) |
55 | 40, 41, 1, 2, 3, 11,
12, 42, 15, 34, 43, 44, 45, 5, 46, 47, 7, 9, 54, 52 | mapdheq 40241 |
. . . . . . . 8
β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β ((πβ(πβ{π})) = (π½β{πΊ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΊ)})))) |
56 | 39, 55 | mpbid 231 |
. . . . . . 7
β’ (π β ((πβ(πβ{π})) = (π½β{πΊ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΊ)}))) |
57 | 56 | simprd 497 |
. . . . . 6
β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΊ)})) |
58 | | mapdh6.fe |
. . . . . . . 8
β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) |
59 | 11, 42, 15, 48, 9, 19, 8, 49, 50 | lspindp1 20639 |
. . . . . . . . . . . 12
β’ (π β ((πβ{π}) β (πβ{π}) β§ Β¬ π β (πβ{π, π}))) |
60 | 59 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (πβ{π}) β (πβ{π})) |
61 | 40, 41, 1, 2, 3, 11,
12, 42, 15, 34, 43, 44, 45, 5, 46, 47, 7, 19, 60 | mapdhcl 40240 |
. . . . . . . . . 10
β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) |
62 | 58, 61 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΈ β π·) |
63 | 40, 41, 1, 2, 3, 11,
12, 42, 15, 34, 43, 44, 45, 5, 46, 47, 7, 18, 62, 60 | mapdheq 40241 |
. . . . . . . 8
β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΈ β ((πβ(πβ{π})) = (π½β{πΈ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΈ)})))) |
64 | 58, 63 | mpbid 231 |
. . . . . . 7
β’ (π β ((πβ(πβ{π})) = (π½β{πΈ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΈ)}))) |
65 | 64 | simpld 496 |
. . . . . 6
β’ (π β (πβ(πβ{π})) = (π½β{πΈ})) |
66 | 57, 65 | oveq12d 7379 |
. . . . 5
β’ (π β ((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π}))) = ((π½β{(πΉπ
πΊ)})(LSSumβπΆ)(π½β{πΈ}))) |
67 | 64 | simprd 497 |
. . . . . 6
β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΉπ
πΈ)})) |
68 | 56 | simpld 496 |
. . . . . 6
β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) |
69 | 67, 68 | oveq12d 7379 |
. . . . 5
β’ (π β ((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π}))) = ((π½β{(πΉπ
πΈ)})(LSSumβπΆ)(π½β{πΊ}))) |
70 | 66, 69 | ineq12d 4177 |
. . . 4
β’ (π β (((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π}))) β© ((πβ(πβ{(π β π)}))(LSSumβπΆ)(πβ(πβ{π})))) = (((π½β{(πΉπ
πΊ)})(LSSumβπΆ)(π½β{πΈ})) β© ((π½β{(πΉπ
πΈ)})(LSSumβπΆ)(π½β{πΊ})))) |
71 | 38, 70 | eqtrd 2773 |
. . 3
β’ (π β ((πβ((πβ{(π β π)})(LSSumβπ)(πβ{π}))) β© (πβ((πβ{(π β π)})(LSSumβπ)(πβ{π})))) = (((π½β{(πΉπ
πΊ)})(LSSumβπΆ)(π½β{πΈ})) β© ((π½β{(πΉπ
πΈ)})(LSSumβπΆ)(π½β{πΊ})))) |
72 | 33, 71 | eqtrd 2773 |
. 2
β’ (π β (πβ(((πβ{(π β π)})(LSSumβπ)(πβ{π})) β© ((πβ{(π β π)})(LSSumβπ)(πβ{π})))) = (((π½β{(πΉπ
πΊ)})(LSSumβπΆ)(π½β{πΈ})) β© ((π½β{(πΉπ
πΈ)})(LSSumβπΆ)(π½β{πΊ})))) |
73 | | mapdh.p |
. . . 4
β’ + =
(+gβπ) |
74 | 11, 12, 42, 22, 15, 48, 8, 50, 49, 9, 18, 73 | baerlem5a 40227 |
. . 3
β’ (π β (πβ{(π β (π + π))}) = (((πβ{(π β π)})(LSSumβπ)(πβ{π})) β© ((πβ{(π β π)})(LSSumβπ)(πβ{π})))) |
75 | 74 | fveq2d 6850 |
. 2
β’ (π β (πβ(πβ{(π β (π + π))})) = (πβ(((πβ{(π β π)})(LSSumβπ)(πβ{π})) β© ((πβ{(π β π)})(LSSumβπ)(πβ{π}))))) |
76 | 1, 34, 5 | lcdlvec 40104 |
. . 3
β’ (π β πΆ β LVec) |
77 | 1, 2, 3, 11, 15, 34, 43, 45, 5, 46, 47, 8, 10, 54, 68, 19, 62, 65, 50 | mapdindp 40184 |
. . 3
β’ (π β Β¬ πΉ β (π½β{πΊ, πΈ})) |
78 | 1, 2, 3, 11, 15, 34, 43, 45, 5, 54, 68, 10, 19, 62, 65, 49 | mapdncol 40183 |
. . 3
β’ (π β (π½β{πΊ}) β (π½β{πΈ})) |
79 | 1, 2, 3, 11, 15, 34, 43, 45, 5, 54, 68, 42, 40, 9 | mapdn0 40182 |
. . 3
β’ (π β πΊ β (π· β {π})) |
80 | 1, 2, 3, 11, 15, 34, 43, 45, 5, 62, 65, 42, 40, 18 | mapdn0 40182 |
. . 3
β’ (π β πΈ β (π· β {π})) |
81 | | mapdh.a |
. . 3
β’ β =
(+gβπΆ) |
82 | 43, 44, 40, 35, 45, 76, 46, 77, 78, 79, 80, 81 | baerlem5a 40227 |
. 2
β’ (π β (π½β{(πΉπ
(πΊ β πΈ))}) = (((π½β{(πΉπ
πΊ)})(LSSumβπΆ)(π½β{πΈ})) β© ((π½β{(πΉπ
πΈ)})(LSSumβπΆ)(π½β{πΊ})))) |
83 | 72, 75, 82 | 3eqtr4d 2783 |
1
β’ (π β (πβ(πβ{(π β (π + π))})) = (π½β{(πΉπ
(πΊ β πΈ))})) |