Metamath Proof Explorer

Theorem lmodvsinv2

Description: Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses lmodvsinv2.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
lmodvsinv2.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lmodvsinv2.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lmodvsinv2.n ⊢ 𝑁 = ( invg ‘ 𝑊 )
lmodvsinv2.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion lmodvsinv2 ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 lmodvsinv2.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 lmodvsinv2.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 lmodvsinv2.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 lmodvsinv2.n ⊢ 𝑁 = ( invg ‘ 𝑊 )
5 lmodvsinv2.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
6 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝑊 ∈ LMod )
7 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
8 6 7 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝑊 ∈ Grp )
9 simp3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
10 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
11 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
12 1 10 11 4 grprinv ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) = ( 0g ‘ 𝑊 ) )
13 8 9 12 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) = ( 0g ‘ 𝑊 ) )
14 13 oveq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) ) = ( 𝑅 · ( 0g ‘ 𝑊 ) ) )
15 simp2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ 𝐾 )
16 1 4 grpinvcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
17 8 9 16 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
18 1 10 2 3 5 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ) ) → ( 𝑅 · ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) ) = ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ) )
19 6 15 9 17 18 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) ) = ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ) )
20 2 3 5 11 lmodvs0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) → ( 𝑅 · ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
21 6 15 20 syl2anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
22 14 19 21 3eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ) = ( 0g ‘ 𝑊 ) )
23 1 2 3 5 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · 𝑋 ) ∈ 𝐵 )
24 1 2 3 5 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐵 )
25 6 15 17 24 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐵 )
26 1 10 11 4 grpinvid1 ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑅 · 𝑋 ) ∈ 𝐵 ∧ ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐵 ) → ( ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) = ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ↔ ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ) = ( 0g ‘ 𝑊 ) ) )
27 8 23 25 26 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) = ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ↔ ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ) = ( 0g ‘ 𝑊 ) ) )
28 22 27 mpbird ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) = ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) )
29 28 eqcomd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )