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 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑅 ) · 𝑋 ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )