Step | Hyp | Ref
| Expression |
1 | | mapdpg.f |
. . 3
β’ πΉ = (BaseβπΆ) |
2 | | eqid 2733 |
. . 3
β’
(+gβπΆ) = (+gβπΆ) |
3 | | eqid 2733 |
. . 3
β’
(ScalarβπΆ) =
(ScalarβπΆ) |
4 | | eqid 2733 |
. . 3
β’
(Baseβ(ScalarβπΆ)) = (Baseβ(ScalarβπΆ)) |
5 | | mapdpglem26.t |
. . 3
β’ Β· = (
Β·π βπΆ) |
6 | | eqid 2733 |
. . 3
β’
(0gβπΆ) = (0gβπΆ) |
7 | | mapdpg.j |
. . 3
β’ π½ = (LSpanβπΆ) |
8 | | mapdpg.h |
. . . 4
β’ π» = (LHypβπΎ) |
9 | | mapdpg.c |
. . . 4
β’ πΆ = ((LCDualβπΎ)βπ) |
10 | | mapdpg.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
11 | 8, 9, 10 | lcdlvec 40104 |
. . 3
β’ (π β πΆ β LVec) |
12 | | mapdpg.g |
. . . 4
β’ (π β πΊ β πΉ) |
13 | | mapdpg.m |
. . . . 5
β’ π = ((mapdβπΎ)βπ) |
14 | | mapdpg.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
15 | | mapdpg.v |
. . . . 5
β’ π = (Baseβπ) |
16 | | mapdpg.s |
. . . . 5
β’ β =
(-gβπ) |
17 | | mapdpg.z |
. . . . 5
β’ 0 =
(0gβπ) |
18 | | mapdpg.n |
. . . . 5
β’ π = (LSpanβπ) |
19 | | mapdpg.r |
. . . . 5
β’ π
= (-gβπΆ) |
20 | | mapdpg.x |
. . . . 5
β’ (π β π β (π β { 0 })) |
21 | | mapdpg.y |
. . . . 5
β’ (π β π β (π β { 0 })) |
22 | | mapdpg.ne |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π})) |
23 | | mapdpg.e |
. . . . 5
β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) |
24 | 8, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23 | mapdpglem30a 40208 |
. . . 4
β’ (π β πΊ β (0gβπΆ)) |
25 | | eldifsn 4751 |
. . . 4
β’ (πΊ β (πΉ β {(0gβπΆ)}) β (πΊ β πΉ β§ πΊ β (0gβπΆ))) |
26 | 12, 24, 25 | sylanbrc 584 |
. . 3
β’ (π β πΊ β (πΉ β {(0gβπΆ)})) |
27 | | mapdpgem25.i1 |
. . . . 5
β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ
π)})))) |
28 | 27 | simpld 496 |
. . . 4
β’ (π β π β πΉ) |
29 | | mapdpgem25.h1 |
. . . . 5
β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ
β)})))) |
30 | 8, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23, 29, 27 | mapdpglem30b 40209 |
. . . 4
β’ (π β π β (0gβπΆ)) |
31 | | eldifsn 4751 |
. . . 4
β’ (π β (πΉ β {(0gβπΆ)}) β (π β πΉ β§ π β (0gβπΆ))) |
32 | 28, 30, 31 | sylanbrc 584 |
. . 3
β’ (π β π β (πΉ β {(0gβπΆ)})) |
33 | | mapdpglem28.ve |
. . . 4
β’ (π β π£ β π΅) |
34 | | mapdpglem26.a |
. . . . 5
β’ π΄ = (Scalarβπ) |
35 | | mapdpglem26.b |
. . . . 5
β’ π΅ = (Baseβπ΄) |
36 | 8, 14, 34, 35, 9, 3, 4, 10 | lcdsbase 40113 |
. . . 4
β’ (π β
(Baseβ(ScalarβπΆ)) = π΅) |
37 | 33, 36 | eleqtrrd 2837 |
. . 3
β’ (π β π£ β (Baseβ(ScalarβπΆ))) |
38 | 8, 14, 10 | dvhlmod 39623 |
. . . . . 6
β’ (π β π β LMod) |
39 | 34 | lmodring 20373 |
. . . . . 6
β’ (π β LMod β π΄ β Ring) |
40 | 38, 39 | syl 17 |
. . . . 5
β’ (π β π΄ β Ring) |
41 | | ringgrp 19977 |
. . . . . . 7
β’ (π΄ β Ring β π΄ β Grp) |
42 | 40, 41 | syl 17 |
. . . . . 6
β’ (π β π΄ β Grp) |
43 | | eqid 2733 |
. . . . . . . 8
β’
(1rβπ΄) = (1rβπ΄) |
44 | 35, 43 | ringidcl 19997 |
. . . . . . 7
β’ (π΄ β Ring β
(1rβπ΄)
β π΅) |
45 | 40, 44 | syl 17 |
. . . . . 6
β’ (π β (1rβπ΄) β π΅) |
46 | | eqid 2733 |
. . . . . . 7
β’
(invgβπ΄) = (invgβπ΄) |
47 | 35, 46 | grpinvcl 18806 |
. . . . . 6
β’ ((π΄ β Grp β§
(1rβπ΄)
β π΅) β
((invgβπ΄)β(1rβπ΄)) β π΅) |
48 | 42, 45, 47 | syl2anc 585 |
. . . . 5
β’ (π β
((invgβπ΄)β(1rβπ΄)) β π΅) |
49 | | eqid 2733 |
. . . . . 6
β’
(.rβπ΄) = (.rβπ΄) |
50 | 35, 49 | ringcl 19989 |
. . . . 5
β’ ((π΄ β Ring β§ π£ β π΅ β§ ((invgβπ΄)β(1rβπ΄)) β π΅) β (π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) β π΅) |
51 | 40, 33, 48, 50 | syl3anc 1372 |
. . . 4
β’ (π β (π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) β π΅) |
52 | 51, 36 | eleqtrrd 2837 |
. . 3
β’ (π β (π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) β
(Baseβ(ScalarβπΆ))) |
53 | 45, 36 | eleqtrrd 2837 |
. . 3
β’ (π β (1rβπ΄) β
(Baseβ(ScalarβπΆ))) |
54 | | mapdpglem28.ue |
. . . . 5
β’ (π β π’ β π΅) |
55 | 35, 49 | ringcl 19989 |
. . . . 5
β’ ((π΄ β Ring β§ π’ β π΅ β§ ((invgβπ΄)β(1rβπ΄)) β π΅) β (π’(.rβπ΄)((invgβπ΄)β(1rβπ΄))) β π΅) |
56 | 40, 54, 48, 55 | syl3anc 1372 |
. . . 4
β’ (π β (π’(.rβπ΄)((invgβπ΄)β(1rβπ΄))) β π΅) |
57 | 56, 36 | eleqtrrd 2837 |
. . 3
β’ (π β (π’(.rβπ΄)((invgβπ΄)β(1rβπ΄))) β
(Baseβ(ScalarβπΆ))) |
58 | | mapdpglem26.o |
. . . 4
β’ π = (0gβπ΄) |
59 | | mapdpglem28.u1 |
. . . 4
β’ (π β β = (π’ Β· π)) |
60 | | mapdpglem28.u2 |
. . . 4
β’ (π β (πΊπ
β) = (π£ Β· (πΊπ
π))) |
61 | 8, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23, 29, 27, 34, 35, 5, 58, 33, 59, 60 | mapdpglem29 40213 |
. . 3
β’ (π β (π½β{πΊ}) β (π½β{π})) |
62 | 8, 14, 34, 35, 49, 9, 1, 5, 10,
48, 54, 28 | lcdvsass 40120 |
. . . . 5
β’ (π β ((π’(.rβπ΄)((invgβπ΄)β(1rβπ΄))) Β· π) = (((invgβπ΄)β(1rβπ΄)) Β· (π’ Β· π))) |
63 | 62 | oveq2d 7377 |
. . . 4
β’ (π β
(((1rβπ΄)
Β·
πΊ)(+gβπΆ)((π’(.rβπ΄)((invgβπ΄)β(1rβπ΄))) Β· π)) = (((1rβπ΄) Β· πΊ)(+gβπΆ)(((invgβπ΄)β(1rβπ΄)) Β· (π’ Β· π)))) |
64 | 8, 14, 34, 35, 9, 1, 5, 10, 45, 12 | lcdvscl 40118 |
. . . . 5
β’ (π β
((1rβπ΄)
Β·
πΊ) β πΉ) |
65 | 8, 14, 34, 35, 9, 1, 5, 10, 54, 28 | lcdvscl 40118 |
. . . . 5
β’ (π β (π’ Β· π) β πΉ) |
66 | 8, 14, 34, 46, 43, 9, 1, 2, 5, 19, 10, 64, 65 | lcdvsub 40130 |
. . . 4
β’ (π β
(((1rβπ΄)
Β·
πΊ)π
(π’ Β· π)) = (((1rβπ΄) Β· πΊ)(+gβπΆ)(((invgβπ΄)β(1rβπ΄)) Β· (π’ Β· π)))) |
67 | 8, 14, 34, 35, 49, 9, 1, 5, 10,
48, 33, 28 | lcdvsass 40120 |
. . . . . 6
β’ (π β ((π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) Β· π) = (((invgβπ΄)β(1rβπ΄)) Β· (π£ Β· π))) |
68 | 67 | oveq2d 7377 |
. . . . 5
β’ (π β ((π£ Β· πΊ)(+gβπΆ)((π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) Β· π)) = ((π£ Β· πΊ)(+gβπΆ)(((invgβπ΄)β(1rβπ΄)) Β· (π£ Β· π)))) |
69 | 8, 14, 34, 35, 9, 1, 5, 10, 33, 12 | lcdvscl 40118 |
. . . . . 6
β’ (π β (π£ Β· πΊ) β πΉ) |
70 | 8, 14, 34, 35, 9, 1, 5, 10, 33, 28 | lcdvscl 40118 |
. . . . . 6
β’ (π β (π£ Β· π) β πΉ) |
71 | 8, 14, 34, 46, 43, 9, 1, 2, 5, 19, 10, 69, 70 | lcdvsub 40130 |
. . . . 5
β’ (π β ((π£ Β· πΊ)π
(π£ Β· π)) = ((π£ Β· πΊ)(+gβπΆ)(((invgβπ΄)β(1rβπ΄)) Β· (π£ Β· π)))) |
72 | 8, 13, 14, 15, 16, 17, 18, 9, 1, 19, 7, 10, 20, 21, 12, 22, 23, 29, 27, 34, 35, 5, 58, 33, 59, 60 | mapdpglem28 40214 |
. . . . . 6
β’ (π β ((π£ Β· πΊ)π
(π£ Β· π)) = (πΊπ
(π’ Β· π))) |
73 | | eqid 2733 |
. . . . . . . . . 10
β’
(1rβ(ScalarβπΆ)) =
(1rβ(ScalarβπΆ)) |
74 | 8, 14, 34, 43, 9, 3, 73, 10 | lcd1 40122 |
. . . . . . . . 9
β’ (π β
(1rβ(ScalarβπΆ)) = (1rβπ΄)) |
75 | 74 | oveq1d 7376 |
. . . . . . . 8
β’ (π β
((1rβ(ScalarβπΆ)) Β· πΊ) = ((1rβπ΄) Β· πΊ)) |
76 | 8, 9, 10 | lcdlmod 40105 |
. . . . . . . . 9
β’ (π β πΆ β LMod) |
77 | 1, 3, 5, 73 | lmodvs1 20394 |
. . . . . . . . 9
β’ ((πΆ β LMod β§ πΊ β πΉ) β
((1rβ(ScalarβπΆ)) Β· πΊ) = πΊ) |
78 | 76, 12, 77 | syl2anc 585 |
. . . . . . . 8
β’ (π β
((1rβ(ScalarβπΆ)) Β· πΊ) = πΊ) |
79 | 75, 78 | eqtr3d 2775 |
. . . . . . 7
β’ (π β
((1rβπ΄)
Β·
πΊ) = πΊ) |
80 | 79 | oveq1d 7376 |
. . . . . 6
β’ (π β
(((1rβπ΄)
Β·
πΊ)π
(π’ Β· π)) = (πΊπ
(π’ Β· π))) |
81 | 72, 80 | eqtr4d 2776 |
. . . . 5
β’ (π β ((π£ Β· πΊ)π
(π£ Β· π)) = (((1rβπ΄) Β· πΊ)π
(π’ Β· π))) |
82 | 68, 71, 81 | 3eqtr2rd 2780 |
. . . 4
β’ (π β
(((1rβπ΄)
Β·
πΊ)π
(π’ Β· π)) = ((π£ Β· πΊ)(+gβπΆ)((π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) Β· π))) |
83 | 63, 66, 82 | 3eqtr2rd 2780 |
. . 3
β’ (π β ((π£ Β· πΊ)(+gβπΆ)((π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) Β· π)) = (((1rβπ΄) Β· πΊ)(+gβπΆ)((π’(.rβπ΄)((invgβπ΄)β(1rβπ΄))) Β· π))) |
84 | 1, 2, 3, 4, 5, 6, 7, 11, 26, 32, 37, 52, 53, 57, 61, 83 | lvecindp2 20645 |
. 2
β’ (π β (π£ = (1rβπ΄) β§ (π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) = (π’(.rβπ΄)((invgβπ΄)β(1rβπ΄))))) |
85 | 35, 49, 43, 46, 40, 33 | ringnegr 20027 |
. . . . 5
β’ (π β (π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) =
((invgβπ΄)βπ£)) |
86 | 35, 49, 43, 46, 40, 54 | ringnegr 20027 |
. . . . 5
β’ (π β (π’(.rβπ΄)((invgβπ΄)β(1rβπ΄))) =
((invgβπ΄)βπ’)) |
87 | 85, 86 | eqeq12d 2749 |
. . . 4
β’ (π β ((π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) = (π’(.rβπ΄)((invgβπ΄)β(1rβπ΄))) β
((invgβπ΄)βπ£) = ((invgβπ΄)βπ’))) |
88 | 35, 46, 42, 33, 54 | grpinv11 18824 |
. . . 4
β’ (π β
(((invgβπ΄)βπ£) = ((invgβπ΄)βπ’) β π£ = π’)) |
89 | 87, 88 | bitrd 279 |
. . 3
β’ (π β ((π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) = (π’(.rβπ΄)((invgβπ΄)β(1rβπ΄))) β π£ = π’)) |
90 | 89 | anbi2d 630 |
. 2
β’ (π β ((π£ = (1rβπ΄) β§ (π£(.rβπ΄)((invgβπ΄)β(1rβπ΄))) = (π’(.rβπ΄)((invgβπ΄)β(1rβπ΄)))) β (π£ = (1rβπ΄) β§ π£ = π’))) |
91 | 84, 90 | mpbid 231 |
1
β’ (π β (π£ = (1rβπ΄) β§ π£ = π’)) |