Step | Hyp | Ref
| Expression |
1 | | lspsnneg.v |
. . . . . 6
β’ π = (Baseβπ) |
2 | | lspsnneg.m |
. . . . . 6
β’ π = (invgβπ) |
3 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
4 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
5 | | eqid 2733 |
. . . . . 6
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
6 | | eqid 2733 |
. . . . . 6
β’
(invgβ(Scalarβπ)) =
(invgβ(Scalarβπ)) |
7 | 1, 2, 3, 4, 5, 6 | lmodvneg1 20380 |
. . . . 5
β’ ((π β LMod β§ π β π) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π) = (πβπ)) |
8 | 7 | sneqd 4599 |
. . . 4
β’ ((π β LMod β§ π β π) β
{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π)} = {(πβπ)}) |
9 | 8 | fveq2d 6847 |
. . 3
β’ ((π β LMod β§ π β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)π)}) = (πβ{(πβπ)})) |
10 | | simpl 484 |
. . . 4
β’ ((π β LMod β§ π β π) β π β LMod) |
11 | 3 | lmodfgrp 20345 |
. . . . . 6
β’ (π β LMod β
(Scalarβπ) β
Grp) |
12 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
13 | 3, 12, 5 | lmod1cl 20364 |
. . . . . 6
β’ (π β LMod β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
14 | 12, 6 | grpinvcl 18803 |
. . . . . 6
β’
(((Scalarβπ)
β Grp β§ (1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
15 | 11, 13, 14 | syl2anc 585 |
. . . . 5
β’ (π β LMod β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
16 | 15 | adantr 482 |
. . . 4
β’ ((π β LMod β§ π β π) β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
17 | | simpr 486 |
. . . 4
β’ ((π β LMod β§ π β π) β π β π) |
18 | | lspsnneg.n |
. . . . 5
β’ π = (LSpanβπ) |
19 | 3, 12, 1, 4, 18 | lspsnvsi 20480 |
. . . 4
β’ ((π β LMod β§
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))
β§ π β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)π)}) β (πβ{π})) |
20 | 10, 16, 17, 19 | syl3anc 1372 |
. . 3
β’ ((π β LMod β§ π β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)π)}) β (πβ{π})) |
21 | 9, 20 | eqsstrrd 3984 |
. 2
β’ ((π β LMod β§ π β π) β (πβ{(πβπ)}) β (πβ{π})) |
22 | 1, 2 | lmodvnegcl 20378 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβπ) β π) |
23 | 1, 2, 3, 4, 5, 6 | lmodvneg1 20380 |
. . . . . . 7
β’ ((π β LMod β§ (πβπ) β π) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)(πβπ)) = (πβ(πβπ))) |
24 | 22, 23 | syldan 592 |
. . . . . 6
β’ ((π β LMod β§ π β π) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)(πβπ)) = (πβ(πβπ))) |
25 | | lmodgrp 20343 |
. . . . . . 7
β’ (π β LMod β π β Grp) |
26 | 1, 2 | grpinvinv 18819 |
. . . . . . 7
β’ ((π β Grp β§ π β π) β (πβ(πβπ)) = π) |
27 | 25, 26 | sylan 581 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (πβ(πβπ)) = π) |
28 | 24, 27 | eqtrd 2773 |
. . . . 5
β’ ((π β LMod β§ π β π) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)(πβπ)) = π) |
29 | 28 | sneqd 4599 |
. . . 4
β’ ((π β LMod β§ π β π) β
{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)(πβπ))} = {π}) |
30 | 29 | fveq2d 6847 |
. . 3
β’ ((π β LMod β§ π β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)(πβπ))}) = (πβ{π})) |
31 | 3, 12, 1, 4, 18 | lspsnvsi 20480 |
. . . 4
β’ ((π β LMod β§
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))
β§ (πβπ) β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)(πβπ))}) β (πβ{(πβπ)})) |
32 | 10, 16, 22, 31 | syl3anc 1372 |
. . 3
β’ ((π β LMod β§ π β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)(πβπ))}) β (πβ{(πβπ)})) |
33 | 30, 32 | eqsstrrd 3984 |
. 2
β’ ((π β LMod β§ π β π) β (πβ{π}) β (πβ{(πβπ)})) |
34 | 21, 33 | eqssd 3962 |
1
β’ ((π β LMod β§ π β π) β (πβ{(πβπ)}) = (πβ{π})) |