# Metamath Proof Explorer

## Theorem lmodvsinv

Description: Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Hypotheses lmodvsinv.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
lmodvsinv.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
lmodvsinv.s
lmodvsinv.n ${⊢}{N}={inv}_{g}\left({W}\right)$
lmodvsinv.m ${⊢}{M}={inv}_{g}\left({F}\right)$
lmodvsinv.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
Assertion lmodvsinv

### Proof

Step Hyp Ref Expression
1 lmodvsinv.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
2 lmodvsinv.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 lmodvsinv.s
4 lmodvsinv.n ${⊢}{N}={inv}_{g}\left({W}\right)$
5 lmodvsinv.m ${⊢}{M}={inv}_{g}\left({F}\right)$
6 lmodvsinv.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
7 simp1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {R}\in {K}\wedge {X}\in {B}\right)\to {W}\in \mathrm{LMod}$
8 2 lmodring ${⊢}{W}\in \mathrm{LMod}\to {F}\in \mathrm{Ring}$
9 8 3ad2ant1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {R}\in {K}\wedge {X}\in {B}\right)\to {F}\in \mathrm{Ring}$
10 ringgrp ${⊢}{F}\in \mathrm{Ring}\to {F}\in \mathrm{Grp}$
11 9 10 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge {R}\in {K}\wedge {X}\in {B}\right)\to {F}\in \mathrm{Grp}$
12 eqid ${⊢}{1}_{{F}}={1}_{{F}}$
13 6 12 ringidcl ${⊢}{F}\in \mathrm{Ring}\to {1}_{{F}}\in {K}$
14 9 13 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge {R}\in {K}\wedge {X}\in {B}\right)\to {1}_{{F}}\in {K}$
15 6 5 grpinvcl ${⊢}\left({F}\in \mathrm{Grp}\wedge {1}_{{F}}\in {K}\right)\to {M}\left({1}_{{F}}\right)\in {K}$
16 11 14 15 syl2anc ${⊢}\left({W}\in \mathrm{LMod}\wedge {R}\in {K}\wedge {X}\in {B}\right)\to {M}\left({1}_{{F}}\right)\in {K}$
17 simp2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {R}\in {K}\wedge {X}\in {B}\right)\to {R}\in {K}$
18 simp3 ${⊢}\left({W}\in \mathrm{LMod}\wedge {R}\in {K}\wedge {X}\in {B}\right)\to {X}\in {B}$
19 eqid ${⊢}{\cdot }_{{F}}={\cdot }_{{F}}$
20 1 2 3 6 19 lmodvsass
21 7 16 17 18 20 syl13anc
22 6 19 12 5 9 17 ringnegl ${⊢}\left({W}\in \mathrm{LMod}\wedge {R}\in {K}\wedge {X}\in {B}\right)\to {M}\left({1}_{{F}}\right){\cdot }_{{F}}{R}={M}\left({R}\right)$
23 22 oveq1d
24 1 2 3 6 lmodvscl
25 1 4 2 3 12 5 lmodvneg1
26 7 24 25 syl2anc
27 21 23 26 3eqtr3d