| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lspsnneg.v |
. . . . . 6
β’ π = (Baseβπ) |
| 2 | | lspsnneg.m |
. . . . . 6
β’ π = (invgβπ) |
| 3 | | eqid 2730 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
| 4 | | eqid 2730 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
| 5 | | eqid 2730 |
. . . . . 6
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
| 6 | | eqid 2730 |
. . . . . 6
β’
(invgβ(Scalarβπ)) =
(invgβ(Scalarβπ)) |
| 7 | 1, 2, 3, 4, 5, 6 | lmodvneg1 20659 |
. . . . 5
β’ ((π β LMod β§ π β π) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π) = (πβπ)) |
| 8 | 7 | sneqd 4639 |
. . . 4
β’ ((π β LMod β§ π β π) β
{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π)} = {(πβπ)}) |
| 9 | 8 | fveq2d 6894 |
. . 3
β’ ((π β LMod β§ π β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)π)}) = (πβ{(πβπ)})) |
| 10 | | simpl 481 |
. . . 4
β’ ((π β LMod β§ π β π) β π β LMod) |
| 11 | 3 | lmodfgrp 20623 |
. . . . . 6
β’ (π β LMod β
(Scalarβπ) β
Grp) |
| 12 | | eqid 2730 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
| 13 | 3, 12, 5 | lmod1cl 20643 |
. . . . . 6
β’ (π β LMod β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
| 14 | 12, 6 | grpinvcl 18908 |
. . . . . 6
β’
(((Scalarβπ)
β Grp β§ (1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
| 15 | 11, 13, 14 | syl2anc 582 |
. . . . 5
β’ (π β LMod β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
| 16 | 15 | adantr 479 |
. . . 4
β’ ((π β LMod β§ π β π) β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
| 17 | | simpr 483 |
. . . 4
β’ ((π β LMod β§ π β π) β π β π) |
| 18 | | lspsnneg.n |
. . . . 5
β’ π = (LSpanβπ) |
| 19 | 3, 12, 1, 4, 18 | lspsnvsi 20759 |
. . . 4
β’ ((π β LMod β§
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))
β§ π β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)π)}) β (πβ{π})) |
| 20 | 10, 16, 17, 19 | syl3anc 1369 |
. . 3
β’ ((π β LMod β§ π β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)π)}) β (πβ{π})) |
| 21 | 9, 20 | eqsstrrd 4020 |
. 2
β’ ((π β LMod β§ π β π) β (πβ{(πβπ)}) β (πβ{π})) |
| 22 | 1, 2 | lmodvnegcl 20657 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβπ) β π) |
| 23 | 1, 2, 3, 4, 5, 6 | lmodvneg1 20659 |
. . . . . . 7
β’ ((π β LMod β§ (πβπ) β π) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)(πβπ)) = (πβ(πβπ))) |
| 24 | 22, 23 | syldan 589 |
. . . . . 6
β’ ((π β LMod β§ π β π) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)(πβπ)) = (πβ(πβπ))) |
| 25 | | lmodgrp 20621 |
. . . . . . 7
β’ (π β LMod β π β Grp) |
| 26 | 1, 2 | grpinvinv 18926 |
. . . . . . 7
β’ ((π β Grp β§ π β π) β (πβ(πβπ)) = π) |
| 27 | 25, 26 | sylan 578 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (πβ(πβπ)) = π) |
| 28 | 24, 27 | eqtrd 2770 |
. . . . 5
β’ ((π β LMod β§ π β π) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)(πβπ)) = π) |
| 29 | 28 | sneqd 4639 |
. . . 4
β’ ((π β LMod β§ π β π) β
{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)(πβπ))} = {π}) |
| 30 | 29 | fveq2d 6894 |
. . 3
β’ ((π β LMod β§ π β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)(πβπ))}) = (πβ{π})) |
| 31 | 3, 12, 1, 4, 18 | lspsnvsi 20759 |
. . . 4
β’ ((π β LMod β§
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))
β§ (πβπ) β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)(πβπ))}) β (πβ{(πβπ)})) |
| 32 | 10, 16, 22, 31 | syl3anc 1369 |
. . 3
β’ ((π β LMod β§ π β π) β (πβ{(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))( Β·π
βπ)(πβπ))}) β (πβ{(πβπ)})) |
| 33 | 30, 32 | eqsstrrd 4020 |
. 2
β’ ((π β LMod β§ π β π) β (πβ{π}) β (πβ{(πβπ)})) |
| 34 | 21, 33 | eqssd 3998 |
1
β’ ((π β LMod β§ π β π) β (πβ{(πβπ)}) = (πβ{π})) |
