Step | Hyp | Ref
| Expression |
1 | | hdmaprnlem1.v |
. . 3
β’ π = (Baseβπ) |
2 | | hdmaprnlem3e.p |
. . 3
β’ + =
(+gβπ) |
3 | | hdmaprnlem1.o |
. . 3
β’ 0 =
(0gβπ) |
4 | | hdmaprnlem1.n |
. . 3
β’ π = (LSpanβπ) |
5 | | eqid 2733 |
. . 3
β’
(LSAtomsβπ) =
(LSAtomsβπ) |
6 | | hdmaprnlem1.h |
. . . 4
β’ π» = (LHypβπΎ) |
7 | | hdmaprnlem1.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
8 | | hdmaprnlem1.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
9 | 6, 7, 8 | dvhlvec 39980 |
. . 3
β’ (π β π β LVec) |
10 | | hdmaprnlem1.m |
. . . 4
β’ π = ((mapdβπΎ)βπ) |
11 | | hdmaprnlem1.c |
. . . 4
β’ πΆ = ((LCDualβπΎ)βπ) |
12 | | eqid 2733 |
. . . 4
β’
(LSAtomsβπΆ) =
(LSAtomsβπΆ) |
13 | | hdmaprnlem1.d |
. . . . 5
β’ π· = (BaseβπΆ) |
14 | | hdmaprnlem1.l |
. . . . 5
β’ πΏ = (LSpanβπΆ) |
15 | | hdmaprnlem1.q |
. . . . 5
β’ π = (0gβπΆ) |
16 | 6, 11, 8 | lcdlmod 40463 |
. . . . 5
β’ (π β πΆ β LMod) |
17 | | hdmaprnlem1.s |
. . . . . . . 8
β’ π = ((HDMapβπΎ)βπ) |
18 | | hdmaprnlem1.ue |
. . . . . . . 8
β’ (π β π’ β π) |
19 | 6, 7, 1, 11, 13, 17, 8, 18 | hdmapcl 40701 |
. . . . . . 7
β’ (π β (πβπ’) β π·) |
20 | | hdmaprnlem1.se |
. . . . . . . 8
β’ (π β π β (π· β {π})) |
21 | 20 | eldifad 3961 |
. . . . . . 7
β’ (π β π β π·) |
22 | | hdmaprnlem1.a |
. . . . . . . 8
β’ β =
(+gβπΆ) |
23 | 13, 22 | lmodvacl 20486 |
. . . . . . 7
β’ ((πΆ β LMod β§ (πβπ’) β π· β§ π β π·) β ((πβπ’) β π ) β π·) |
24 | 16, 19, 21, 23 | syl3anc 1372 |
. . . . . 6
β’ (π β ((πβπ’) β π ) β π·) |
25 | | hdmaprnlem1.ve |
. . . . . . . 8
β’ (π β π£ β π) |
26 | | hdmaprnlem1.e |
. . . . . . . 8
β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) |
27 | | hdmaprnlem1.un |
. . . . . . . 8
β’ (π β Β¬ π’ β (πβ{π£})) |
28 | 6, 7, 1, 4, 11, 14, 10, 17, 8, 20, 25, 26, 18, 27 | hdmaprnlem1N 40720 |
. . . . . . 7
β’ (π β (πΏβ{(πβπ’)}) β (πΏβ{π })) |
29 | 13, 22, 15, 14, 16, 19, 21, 28 | lmodindp1 20625 |
. . . . . 6
β’ (π β ((πβπ’) β π ) β π) |
30 | | eldifsn 4791 |
. . . . . 6
β’ (((πβπ’) β π ) β (π· β {π}) β (((πβπ’) β π ) β π· β§ ((πβπ’) β π ) β π)) |
31 | 24, 29, 30 | sylanbrc 584 |
. . . . 5
β’ (π β ((πβπ’) β π ) β (π· β {π})) |
32 | 13, 14, 15, 12, 16, 31 | lsatlspsn 37863 |
. . . 4
β’ (π β (πΏβ{((πβπ’) β π )}) β (LSAtomsβπΆ)) |
33 | 6, 10, 7, 5, 11, 12, 8, 32 | mapdcnvatN 40537 |
. . 3
β’ (π β (β‘πβ(πΏβ{((πβπ’) β π )})) β (LSAtomsβπ)) |
34 | 6, 7, 1, 4, 11, 14, 10, 17, 8, 20, 25, 26, 18, 27, 13, 15, 3, 22 | hdmaprnlem3uN 40722 |
. . . 4
β’ (π β (πβ{π’}) β (β‘πβ(πΏβ{((πβπ’) β π )}))) |
35 | 34 | necomd 2997 |
. . 3
β’ (π β (β‘πβ(πΏβ{((πβπ’) β π )})) β (πβ{π’})) |
36 | 6, 7, 1, 4, 11, 14, 10, 17, 8, 20, 25, 26, 18, 27, 13, 15, 3, 22 | hdmaprnlem3N 40721 |
. . . 4
β’ (π β (πβ{π£}) β (β‘πβ(πΏβ{((πβπ’) β π )}))) |
37 | 36 | necomd 2997 |
. . 3
β’ (π β (β‘πβ(πΏβ{((πβπ’) β π )})) β (πβ{π£})) |
38 | | eqid 2733 |
. . . . . . 7
β’
(LSubSpβπΆ) =
(LSubSpβπΆ) |
39 | | eqid 2733 |
. . . . . . . . 9
β’
(LSubSpβπ) =
(LSubSpβπ) |
40 | 6, 7, 8 | dvhlmod 39981 |
. . . . . . . . . 10
β’ (π β π β LMod) |
41 | 1, 39, 4 | lspsncl 20588 |
. . . . . . . . . 10
β’ ((π β LMod β§ π’ β π) β (πβ{π’}) β (LSubSpβπ)) |
42 | 40, 18, 41 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πβ{π’}) β (LSubSpβπ)) |
43 | 6, 10, 7, 39, 11, 38, 8, 42 | mapdcl2 40527 |
. . . . . . . 8
β’ (π β (πβ(πβ{π’})) β (LSubSpβπΆ)) |
44 | 1, 39, 4 | lspsncl 20588 |
. . . . . . . . . 10
β’ ((π β LMod β§ π£ β π) β (πβ{π£}) β (LSubSpβπ)) |
45 | 40, 25, 44 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πβ{π£}) β (LSubSpβπ)) |
46 | 6, 10, 7, 39, 11, 38, 8, 45 | mapdcl2 40527 |
. . . . . . . 8
β’ (π β (πβ(πβ{π£})) β (LSubSpβπΆ)) |
47 | | eqid 2733 |
. . . . . . . . 9
β’
(LSSumβπΆ) =
(LSSumβπΆ) |
48 | 38, 47 | lsmcl 20694 |
. . . . . . . 8
β’ ((πΆ β LMod β§ (πβ(πβ{π’})) β (LSubSpβπΆ) β§ (πβ(πβ{π£})) β (LSubSpβπΆ)) β ((πβ(πβ{π’}))(LSSumβπΆ)(πβ(πβ{π£}))) β (LSubSpβπΆ)) |
49 | 16, 43, 46, 48 | syl3anc 1372 |
. . . . . . 7
β’ (π β ((πβ(πβ{π’}))(LSSumβπΆ)(πβ(πβ{π£}))) β (LSubSpβπΆ)) |
50 | 38 | lsssssubg 20569 |
. . . . . . . . . 10
β’ (πΆ β LMod β
(LSubSpβπΆ) β
(SubGrpβπΆ)) |
51 | 16, 50 | syl 17 |
. . . . . . . . 9
β’ (π β (LSubSpβπΆ) β (SubGrpβπΆ)) |
52 | 51, 43 | sseldd 3984 |
. . . . . . . 8
β’ (π β (πβ(πβ{π’})) β (SubGrpβπΆ)) |
53 | 51, 46 | sseldd 3984 |
. . . . . . . 8
β’ (π β (πβ(πβ{π£})) β (SubGrpβπΆ)) |
54 | 13, 14 | lspsnid 20604 |
. . . . . . . . . 10
β’ ((πΆ β LMod β§ (πβπ’) β π·) β (πβπ’) β (πΏβ{(πβπ’)})) |
55 | 16, 19, 54 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πβπ’) β (πΏβ{(πβπ’)})) |
56 | 6, 7, 1, 4, 11, 14, 10, 17, 8, 18 | hdmap10 40711 |
. . . . . . . . 9
β’ (π β (πβ(πβ{π’})) = (πΏβ{(πβπ’)})) |
57 | 55, 56 | eleqtrrd 2837 |
. . . . . . . 8
β’ (π β (πβπ’) β (πβ(πβ{π’}))) |
58 | | eqimss2 4042 |
. . . . . . . . . 10
β’ ((πβ(πβ{π£})) = (πΏβ{π }) β (πΏβ{π }) β (πβ(πβ{π£}))) |
59 | 26, 58 | syl 17 |
. . . . . . . . 9
β’ (π β (πΏβ{π }) β (πβ(πβ{π£}))) |
60 | 13, 38, 14, 16, 46, 21 | lspsnel5 20606 |
. . . . . . . . 9
β’ (π β (π β (πβ(πβ{π£})) β (πΏβ{π }) β (πβ(πβ{π£})))) |
61 | 59, 60 | mpbird 257 |
. . . . . . . 8
β’ (π β π β (πβ(πβ{π£}))) |
62 | 22, 47 | lsmelvali 19518 |
. . . . . . . 8
β’ ((((πβ(πβ{π’})) β (SubGrpβπΆ) β§ (πβ(πβ{π£})) β (SubGrpβπΆ)) β§ ((πβπ’) β (πβ(πβ{π’})) β§ π β (πβ(πβ{π£})))) β ((πβπ’) β π ) β ((πβ(πβ{π’}))(LSSumβπΆ)(πβ(πβ{π£})))) |
63 | 52, 53, 57, 61, 62 | syl22anc 838 |
. . . . . . 7
β’ (π β ((πβπ’) β π ) β ((πβ(πβ{π’}))(LSSumβπΆ)(πβ(πβ{π£})))) |
64 | 38, 14, 16, 49, 63 | lspsnel5a 20607 |
. . . . . 6
β’ (π β (πΏβ{((πβπ’) β π )}) β ((πβ(πβ{π’}))(LSSumβπΆ)(πβ(πβ{π£})))) |
65 | | eqid 2733 |
. . . . . . 7
β’
(LSSumβπ) =
(LSSumβπ) |
66 | 6, 10, 7, 39, 65, 11, 47, 8, 42, 45 | mapdlsm 40535 |
. . . . . 6
β’ (π β (πβ((πβ{π’})(LSSumβπ)(πβ{π£}))) = ((πβ(πβ{π’}))(LSSumβπΆ)(πβ(πβ{π£})))) |
67 | 64, 66 | sseqtrrd 4024 |
. . . . 5
β’ (π β (πΏβ{((πβπ’) β π )}) β (πβ((πβ{π’})(LSSumβπ)(πβ{π£})))) |
68 | 13, 38, 14 | lspsncl 20588 |
. . . . . . . 8
β’ ((πΆ β LMod β§ ((πβπ’) β π ) β π·) β (πΏβ{((πβπ’) β π )}) β (LSubSpβπΆ)) |
69 | 16, 24, 68 | syl2anc 585 |
. . . . . . 7
β’ (π β (πΏβ{((πβπ’) β π )}) β (LSubSpβπΆ)) |
70 | 6, 10, 11, 38, 8 | mapdrn2 40522 |
. . . . . . 7
β’ (π β ran π = (LSubSpβπΆ)) |
71 | 69, 70 | eleqtrrd 2837 |
. . . . . 6
β’ (π β (πΏβ{((πβπ’) β π )}) β ran π) |
72 | 39, 65 | lsmcl 20694 |
. . . . . . . 8
β’ ((π β LMod β§ (πβ{π’}) β (LSubSpβπ) β§ (πβ{π£}) β (LSubSpβπ)) β ((πβ{π’})(LSSumβπ)(πβ{π£})) β (LSubSpβπ)) |
73 | 40, 42, 45, 72 | syl3anc 1372 |
. . . . . . 7
β’ (π β ((πβ{π’})(LSSumβπ)(πβ{π£})) β (LSubSpβπ)) |
74 | 6, 10, 7, 39, 8, 73 | mapdcl 40524 |
. . . . . 6
β’ (π β (πβ((πβ{π’})(LSSumβπ)(πβ{π£}))) β ran π) |
75 | 6, 10, 8, 71, 74 | mapdcnvordN 40529 |
. . . . 5
β’ (π β ((β‘πβ(πΏβ{((πβπ’) β π )})) β (β‘πβ(πβ((πβ{π’})(LSSumβπ)(πβ{π£})))) β (πΏβ{((πβπ’) β π )}) β (πβ((πβ{π’})(LSSumβπ)(πβ{π£}))))) |
76 | 67, 75 | mpbird 257 |
. . . 4
β’ (π β (β‘πβ(πΏβ{((πβπ’) β π )})) β (β‘πβ(πβ((πβ{π’})(LSSumβπ)(πβ{π£}))))) |
77 | 1, 4, 65, 40, 18, 25 | lsmpr 20700 |
. . . . 5
β’ (π β (πβ{π’, π£}) = ((πβ{π’})(LSSumβπ)(πβ{π£}))) |
78 | 6, 10, 7, 39, 8, 73 | mapdcnvid1N 40525 |
. . . . 5
β’ (π β (β‘πβ(πβ((πβ{π’})(LSSumβπ)(πβ{π£})))) = ((πβ{π’})(LSSumβπ)(πβ{π£}))) |
79 | 77, 78 | eqtr4d 2776 |
. . . 4
β’ (π β (πβ{π’, π£}) = (β‘πβ(πβ((πβ{π’})(LSSumβπ)(πβ{π£}))))) |
80 | 76, 79 | sseqtrrd 4024 |
. . 3
β’ (π β (β‘πβ(πΏβ{((πβπ’) β π )})) β (πβ{π’, π£})) |
81 | 1, 2, 3, 4, 5, 9, 33, 18, 25, 35, 37, 80 | lsatfixedN 37879 |
. 2
β’ (π β βπ‘ β ((πβ{π£}) β { 0 })(β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) |
82 | | simpr 486 |
. . . . . 6
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) |
83 | 8 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β (πΎ β HL β§ π β π»)) |
84 | 40 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β π β LMod) |
85 | 18 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β π’ β π) |
86 | 20 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β π β (π· β {π})) |
87 | 25 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β π£ β π) |
88 | 26 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β (πβ(πβ{π£})) = (πΏβ{π })) |
89 | 27 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β Β¬ π’ β (πβ{π£})) |
90 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β π‘ β ((πβ{π£}) β { 0 })) |
91 | 6, 7, 1, 4, 11, 14, 10, 17, 83, 86, 87, 88, 85, 89, 13, 15, 3, 22, 90 | hdmaprnlem4tN 40723 |
. . . . . . . . 9
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β π‘ β π) |
92 | 1, 2 | lmodvacl 20486 |
. . . . . . . . 9
β’ ((π β LMod β§ π’ β π β§ π‘ β π) β (π’ + π‘) β π) |
93 | 84, 85, 91, 92 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β (π’ + π‘) β π) |
94 | 1, 39, 4 | lspsncl 20588 |
. . . . . . . 8
β’ ((π β LMod β§ (π’ + π‘) β π) β (πβ{(π’ + π‘)}) β (LSubSpβπ)) |
95 | 84, 93, 94 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β (πβ{(π’ + π‘)}) β (LSubSpβπ)) |
96 | 6, 10, 7, 39, 83, 95 | mapdcnvid1N 40525 |
. . . . . 6
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β (β‘πβ(πβ(πβ{(π’ + π‘)}))) = (πβ{(π’ + π‘)})) |
97 | 82, 96 | eqtr4d 2776 |
. . . . 5
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β (β‘πβ(πΏβ{((πβπ’) β π )})) = (β‘πβ(πβ(πβ{(π’ + π‘)})))) |
98 | 71 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β (πΏβ{((πβπ’) β π )}) β ran π) |
99 | 6, 10, 7, 39, 83, 95 | mapdcl 40524 |
. . . . . 6
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β (πβ(πβ{(π’ + π‘)})) β ran π) |
100 | 6, 10, 83, 98, 99 | mapdcnv11N 40530 |
. . . . 5
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β ((β‘πβ(πΏβ{((πβπ’) β π )})) = (β‘πβ(πβ(πβ{(π’ + π‘)}))) β (πΏβ{((πβπ’) β π )}) = (πβ(πβ{(π’ + π‘)})))) |
101 | 97, 100 | mpbid 231 |
. . . 4
β’ (((π β§ π‘ β ((πβ{π£}) β { 0 })) β§ (β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)})) β (πΏβ{((πβπ’) β π )}) = (πβ(πβ{(π’ + π‘)}))) |
102 | 101 | ex 414 |
. . 3
β’ ((π β§ π‘ β ((πβ{π£}) β { 0 })) β ((β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)}) β (πΏβ{((πβπ’) β π )}) = (πβ(πβ{(π’ + π‘)})))) |
103 | 102 | reximdva 3169 |
. 2
β’ (π β (βπ‘ β ((πβ{π£}) β { 0 })(β‘πβ(πΏβ{((πβπ’) β π )})) = (πβ{(π’ + π‘)}) β βπ‘ β ((πβ{π£}) β { 0 })(πΏβ{((πβπ’) β π )}) = (πβ(πβ{(π’ + π‘)})))) |
104 | 81, 103 | mpd 15 |
1
β’ (π β βπ‘ β ((πβ{π£}) β { 0 })(πΏβ{((πβπ’) β π )}) = (πβ(πβ{(π’ + π‘)}))) |