# 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 𝐵 = ( Base ‘ 𝑊 )
lmodvsinv.f 𝐹 = ( Scalar ‘ 𝑊 )
lmodvsinv.s · = ( ·𝑠𝑊 )
lmodvsinv.n 𝑁 = ( invg𝑊 )
lmodvsinv.m 𝑀 = ( invg𝐹 )
lmodvsinv.k 𝐾 = ( Base ‘ 𝐹 )
Assertion lmodvsinv ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → ( ( 𝑀𝑅 ) · 𝑋 ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )

### Proof

Step Hyp Ref Expression
1 lmodvsinv.b 𝐵 = ( Base ‘ 𝑊 )
2 lmodvsinv.f 𝐹 = ( Scalar ‘ 𝑊 )
3 lmodvsinv.s · = ( ·𝑠𝑊 )
4 lmodvsinv.n 𝑁 = ( invg𝑊 )
5 lmodvsinv.m 𝑀 = ( invg𝐹 )
6 lmodvsinv.k 𝐾 = ( Base ‘ 𝐹 )
7 simp1 ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → 𝑊 ∈ LMod )
8 2 lmodring ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
9 8 3ad2ant1 ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → 𝐹 ∈ Ring )
10 ringgrp ( 𝐹 ∈ Ring → 𝐹 ∈ Grp )
11 9 10 syl ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → 𝐹 ∈ Grp )
12 eqid ( 1r𝐹 ) = ( 1r𝐹 )
13 6 12 ringidcl ( 𝐹 ∈ Ring → ( 1r𝐹 ) ∈ 𝐾 )
14 9 13 syl ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → ( 1r𝐹 ) ∈ 𝐾 )
15 6 5 grpinvcl ( ( 𝐹 ∈ Grp ∧ ( 1r𝐹 ) ∈ 𝐾 ) → ( 𝑀 ‘ ( 1r𝐹 ) ) ∈ 𝐾 )
16 11 14 15 syl2anc ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → ( 𝑀 ‘ ( 1r𝐹 ) ) ∈ 𝐾 )
17 simp2 ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → 𝑅𝐾 )
18 simp3 ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → 𝑋𝐵 )
19 eqid ( .r𝐹 ) = ( .r𝐹 )
20 1 2 3 6 19 lmodvsass ( ( 𝑊 ∈ LMod ∧ ( ( 𝑀 ‘ ( 1r𝐹 ) ) ∈ 𝐾𝑅𝐾𝑋𝐵 ) ) → ( ( ( 𝑀 ‘ ( 1r𝐹 ) ) ( .r𝐹 ) 𝑅 ) · 𝑋 ) = ( ( 𝑀 ‘ ( 1r𝐹 ) ) · ( 𝑅 · 𝑋 ) ) )
21 7 16 17 18 20 syl13anc ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → ( ( ( 𝑀 ‘ ( 1r𝐹 ) ) ( .r𝐹 ) 𝑅 ) · 𝑋 ) = ( ( 𝑀 ‘ ( 1r𝐹 ) ) · ( 𝑅 · 𝑋 ) ) )
22 6 19 12 5 9 17 ringnegl ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → ( ( 𝑀 ‘ ( 1r𝐹 ) ) ( .r𝐹 ) 𝑅 ) = ( 𝑀𝑅 ) )
23 22 oveq1d ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → ( ( ( 𝑀 ‘ ( 1r𝐹 ) ) ( .r𝐹 ) 𝑅 ) · 𝑋 ) = ( ( 𝑀𝑅 ) · 𝑋 ) )
24 1 2 3 6 lmodvscl ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → ( 𝑅 · 𝑋 ) ∈ 𝐵 )
25 1 4 2 3 12 5 lmodvneg1 ( ( 𝑊 ∈ LMod ∧ ( 𝑅 · 𝑋 ) ∈ 𝐵 ) → ( ( 𝑀 ‘ ( 1r𝐹 ) ) · ( 𝑅 · 𝑋 ) ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )
26 7 24 25 syl2anc ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → ( ( 𝑀 ‘ ( 1r𝐹 ) ) · ( 𝑅 · 𝑋 ) ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )
27 21 23 26 3eqtr3d ( ( 𝑊 ∈ LMod ∧ 𝑅𝐾𝑋𝐵 ) → ( ( 𝑀𝑅 ) · 𝑋 ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )