Metamath Proof Explorer

Theorem lmodvsneg

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

Ref Expression
Hypotheses lmodvsneg.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
lmodvsneg.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lmodvsneg.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lmodvsneg.n ⊢ 𝑁 = ( invg ‘ 𝑊 )
lmodvsneg.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lmodvsneg.m ⊢ 𝑀 = ( invg ‘ 𝐹 )
lmodvsneg.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lmodvsneg.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
lmodvsneg.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
Assertion lmodvsneg ( 𝜑 → ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) = ( ( 𝑀 ‘ 𝑅 ) · 𝑋 ) )

Proof

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